Skip to content

Commit

Permalink
Merge pull request #662 from hacspec/clauses-661
Browse files Browse the repository at this point in the history
Refactor of clauses
  • Loading branch information
W95Psp committed May 15, 2024
2 parents 1e3a524 + e259b17 commit 4d4812a
Show file tree
Hide file tree
Showing 13 changed files with 171 additions and 154 deletions.
1 change: 1 addition & 0 deletions cli/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@
);
frontend-docs = craneLib.cargoDoc (commonArgs // {
preBuildPhases = ["addRustcDocs"];
cargoDocExtraArgs = "--document-private-items";
addRustcDocs = ''
mkdir -p target/doc
cp --no-preserve=mode -rf ${rustc.passthru.availableComponents.rustc-docs}/share/doc/rust/html/rustc/* target/doc/
Expand Down
17 changes: 9 additions & 8 deletions engine/lib/concrete_ident/impl_infos.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ type t = {
[impl] block is an {{: https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations } inherent [impl]}.
*)
typ : Ast.Rust.ty; (** The type implemented by the [impl] block. *)
predicates : Ast.Rust.trait_goal list;
(** The predicates that constraint this [impl] block. *)
clauses : Ast.Rust.trait_goal list;
(** The clauses that constraint this [impl] block. *)
}
(** metadata of an [impl] block *)

Expand All @@ -20,17 +20,18 @@ issue 363}, when looking up certain identifiers generated by the
engine, this function may return [None] even though the supplied
identifier points to an [Impl] block. *)
let lookup span (impl : Concrete_ident.t) : t option =
let* Types.{ generics = _; predicates; typ; trait_ref } =
let* Types.{ generics = _; clauses; typ; trait_ref } =
Concrete_ident.lookup_raw_impl_info impl
in
let trait_goal =
Option.map ~f:(Import_thir.import_trait_ref span) trait_ref
in
let typ = Import_thir.import_ty span typ in
let predicates =
let f (binder : Types.binder_for__predicate_kind) =
Import_thir.import_predicate_kind span binder.value
let clauses =
let f ((binder : Types.clause), span) =
Import_thir.import_clause span binder
in
List.filter_map ~f predicates
List.filter_map ~f clauses
|> List.map ~f:(fun (i : Ast.Rust.impl_ident) -> i.goal)
in
Some { trait_goal; typ; predicates }
Some { trait_goal; typ; clauses }
39 changes: 20 additions & 19 deletions engine/lib/import_thir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,6 @@ module type EXPR = sig
val c_param : Thir.span -> Thir.param -> param
val c_trait_item' : Thir.trait_item -> Thir.trait_item_kind -> trait_item'
val c_trait_ref : Thir.span -> Thir.trait_ref -> trait_goal
val c_predicate_kind : Thir.span -> Thir.predicate_kind -> trait_goal option
val c_impl_expr : Thir.span -> Thir.impl_expr -> impl_expr
val c_clause : Thir.span -> Thir.clause -> impl_ident option
end
Expand Down Expand Up @@ -983,24 +982,30 @@ end) : EXPR = struct
let browse_path (impl : impl_expr) (chunk : Thir.impl_expr_path_chunk) =
match chunk with
| AssocItem
{ item; predicate = { value = { trait_ref; _ }; _ }; clause_id; _ } ->
let ident = { goal = c_trait_ref span trait_ref; name = clause_id } in
{ item; predicate = { value = { trait_ref; _ }; _ }; predicate_id; _ }
->
let ident =
{ goal = c_trait_ref span trait_ref; name = predicate_id }
in
let kind : Concrete_ident.Kind.t =
match item.kind with Const | Fn -> Value | Type -> Type
in
let item = Concrete_ident.of_def_id kind item.def_id in
Projection { impl; ident; item }
| Parent { predicate = { value = { trait_ref; _ }; _ }; clause_id; _ } ->
let ident = { goal = c_trait_ref span trait_ref; name = clause_id } in
| Parent { predicate = { value = { trait_ref; _ }; _ }; predicate_id; _ }
->
let ident =
{ goal = c_trait_ref span trait_ref; name = predicate_id }
in
Parent { impl; ident }
in
match ie with
| Concrete { id; generics } ->
let trait = Concrete_ident.of_def_id Impl id in
let args = List.map ~f:(c_generic_value span) generics in
Concrete { trait; args }
| LocalBound { clause_id; path; _ } ->
let init = LocalBound { id = clause_id } in
| LocalBound { predicate_id; path; _ } ->
let init = LocalBound { id = predicate_id } in
List.fold ~init ~f:browse_path path
| Dyn -> Dyn
| SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path
Expand Down Expand Up @@ -1057,20 +1062,17 @@ end) : EXPR = struct
let attrs = c_attrs param.attributes in
{ ident; span; attrs; kind }

let c_clause span (p : Thir.clause) : impl_ident option =
let ({ kind; id } : Thir.clause) = p in
let c_clause_kind span id (kind : Thir.clause_kind) : impl_ident option =
match kind with
| Trait { is_positive = true; is_const = _; trait_ref } ->
let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in
let trait = Concrete_ident.of_def_id Trait trait_ref.def_id in
Some { goal = { trait; args }; name = id }
| _ -> None

let c_predicate_kind' span (p : Thir.predicate_kind) : impl_ident option =
match p with Clause clause -> c_clause span clause | _ -> None

let c_predicate_kind span (p : Thir.predicate_kind) : trait_goal option =
c_predicate_kind' span p |> Option.map ~f:(fun (x : impl_ident) -> x.goal)
let c_clause span (p : Thir.clause) : impl_ident option =
let ({ kind; id } : Thir.clause) = p in
c_clause_kind span id kind.value

let list_dedup (equal : 'a -> 'a -> bool) : 'a list -> 'a list =
let rec aux (seen : 'a list) (todo : 'a list) : 'a list =
Expand All @@ -1084,7 +1086,7 @@ end) : EXPR = struct

let c_generics (generics : Thir.generics) : generics =
let bounds =
List.filter_map ~f:(c_predicate_kind' generics.span) generics.bounds
List.filter_map ~f:(c_clause generics.span) generics.bounds
|> List.map ~f:(fun impl_ident -> GCType impl_ident)
in
{
Expand Down Expand Up @@ -1113,7 +1115,7 @@ end) : EXPR = struct
in
TIFn (TArrow (inputs, output))
| Type (bounds, None) ->
let bounds = List.filter_map ~f:(c_predicate_kind' span) bounds in
let bounds = List.filter_map ~f:(c_clause span) bounds in
TIType bounds
| Type (_, Some _) ->
unimplemented [ span ]
Expand All @@ -1130,9 +1132,8 @@ include struct
let import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal =
c_trait_ref

let import_predicate_kind :
Types.span -> Types.predicate_kind -> Ast.Rust.trait_goal option =
c_predicate_kind
let import_clause : Types.span -> Types.clause -> Ast.Rust.impl_ident option =
c_clause
end

(** Instantiate the functor for translating expressions. The crate
Expand Down
4 changes: 1 addition & 3 deletions engine/lib/import_thir.mli
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
val import_ty : Types.span -> Types.ty -> Ast.Rust.ty
val import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal

val import_predicate_kind :
Types.span -> Types.predicate_kind -> Ast.Rust.trait_goal option
val import_clause : Types.span -> Types.clause -> Ast.Rust.impl_ident option

val import_item :
drop_body:bool ->
Expand Down
1 change: 1 addition & 0 deletions frontend/exporter/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
#![allow(incomplete_features)]
#![feature(specialization)]
#![feature(return_position_impl_trait_in_trait)]
#![allow(rustdoc::private_intra_doc_links)]

extern crate rustc_abi;
extern crate rustc_ast;
Expand Down
10 changes: 2 additions & 8 deletions frontend/exporter/src/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -236,7 +236,7 @@ pub trait UnderOwnerState<'tcx> = BaseState<'tcx> + HasOwnerId;
#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)]
pub struct ImplInfos {
pub generics: TyGenerics,
pub predicates: Vec<Predicate>,
pub clauses: Vec<(Clause, Span)>,
pub typ: Ty,
pub trait_ref: Option<TraitRef>,
}
Expand All @@ -246,17 +246,11 @@ impl ImplInfos {
let tcx = base.tcx;
let s = &with_owner_id(base, (), (), did);

let predicates = tcx
.predicates_defined_on(did)
.predicates
.iter()
.map(|(clause, _)| clause.as_predicate().sinto(s))
.collect();
Self {
generics: tcx.generics_of(did).sinto(s),
typ: tcx.type_of(did).subst_identity().sinto(s),
trait_ref: tcx.impl_trait_ref(did).sinto(s),
predicates,
clauses: tcx.predicates_defined_on(did).predicates.sinto(s),
}
}
}
Expand Down
74 changes: 15 additions & 59 deletions frontend/exporter/src/traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,12 @@ pub enum ImplExprPathChunk {
AssocItem {
item: AssocItem,
predicate: Binder<TraitPredicate>,
clause_id: u64,
predicate_id: PredicateId,
index: usize,
},
Parent {
predicate: Binder<TraitPredicate>,
clause_id: u64,
predicate_id: PredicateId,
index: usize,
},
}
Expand All @@ -32,7 +32,7 @@ pub enum ImplExprAtom {
},
/// A context-bound clause like `where T: Trait`.
LocalBound {
clause_id: u64,
predicate_id: PredicateId,
r#trait: Binder<TraitRef>,
path: Vec<ImplExprPathChunk>,
},
Expand Down Expand Up @@ -70,9 +70,11 @@ pub struct ImplExpr {
pub args: Vec<ImplExpr>,
}

mod search_clause {
// FIXME: this has visibility `pub(crate)` only because of https://github.com/rust-lang/rust/issues/83049
pub(crate) mod search_clause {
use crate::prelude::UnderOwnerState;
use crate::rustc_utils::*;
use crate::{IntoPredicateId, PredicateId};
use rustc_middle::ty::*;

fn predicates_to_poly_trait_predicates<'tcx>(
Expand All @@ -90,12 +92,12 @@ mod search_clause {
AssocItem {
item: AssocItem,
predicate: PolyTraitPredicate<'tcx>,
clause_id: u64,
predicate_id: PredicateId,
index: usize,
},
Parent {
predicate: PolyTraitPredicate<'tcx>,
clause_id: u64,
predicate_id: PredicateId,
index: usize,
},
}
Expand Down Expand Up @@ -224,10 +226,7 @@ mod search_clause {
cons(
PathChunk::Parent {
predicate: p,
clause_id: {
use rustc_middle::ty::ToPredicate;
crate::clause_id_of_predicate(s, p.to_predicate(s.base().tcx))
},
predicate_id: p.predicate_id(s),
index,
},
path,
Expand All @@ -244,13 +243,7 @@ mod search_clause {
cons(
PathChunk::AssocItem {
item,
clause_id: {
use rustc_middle::ty::ToPredicate;
crate::clause_id_of_predicate(
s,
p.to_predicate(s.base().tcx),
)
},
predicate_id: p.predicate_id(s),
predicate: p,
index,
},
Expand Down Expand Up @@ -374,7 +367,7 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
.with_args(impl_exprs(s, &nested), trait_ref)
} else {
ImplExprAtom::LocalBound {
clause_id: clause_id_of_predicate(s, apred.predicate),
predicate_id: apred.predicate.predicate_id(s),
r#trait,
path,
}
Expand Down Expand Up @@ -410,59 +403,22 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
let impl_trait_ref = tcx
.impl_trait_ref(impl_did)
.map(|binder| rustc_middle::ty::Binder::dummy(binder.subst_identity()))?;
let original_clause_id = {
let original_predicate_id = {
// We don't want the id of the substituted clause id, but the
// original clause id (with, i.e., `Self`)
let s = &with_owner_id(s.base(), (), (), impl_trait_ref.def_id());
// We compute the id of the clause without binder.
let clause: Clause = clause.kind().skip_binder().sinto(s);
clause.id
clause.predicate_id(s)
};
let new_clause = clause.subst_supertrait(tcx, &impl_trait_ref);
let impl_expr = new_clause
.as_predicate()
.to_opt_poly_trait_pred()?
.impl_expr(s, get_param_env(s));
// Build the new clause, again without binder.
let mut new_clause_no_binder: Clause = new_clause.kind().skip_binder().sinto(s);
new_clause_no_binder.id = original_clause_id;
let mut new_clause_no_binder = new_clause.sinto(s);
new_clause_no_binder.id = original_predicate_id;
Some((new_clause_no_binder, impl_expr, span.sinto(s)))
}

fn deterministic_hash<T: std::hash::Hash>(x: &T) -> u64 {
use crate::deterministic_hash::DeterministicHasher;
use std::collections::hash_map::DefaultHasher;
use std::hash::Hasher;
let mut hasher = DeterministicHasher::new(DefaultHasher::new());
x.hash(&mut hasher);
hasher.finish()
}

/// Crafts a unique identifier for a predicate by hashing it. The hash
/// is non-trivial because we need stable identifiers: two hax
/// extraction of a same predicate should result in the same
/// identifier. Rustc's stable hash is not doing what we want here: it
/// is sensible to the environment. Instead, we convert the (rustc)
/// predicate to `crate::Predicate` and hash from there.
#[tracing::instrument(level = "trace", skip(s))]
pub fn clause_id_of_predicate<'tcx, S: UnderOwnerState<'tcx>>(
s: &S,
predicate: rustc_middle::ty::Predicate<'tcx>,
) -> u64 {
let predicate = predicate.sinto(s);
match &predicate.value {
// Instead of recursively hashing the clause, we reuse the already-computed id.
PredicateKind::Clause(clause) => clause.id,
_ => deterministic_hash(&(1u8, predicate)),
}
}

/// Used when building a `crate::Clause`. See [`clause_id_of_predicate`] for what we're doing here.
#[tracing::instrument(level = "trace")]
pub fn clause_id_of_bound_clause_kind(binder: &Binder<ClauseKind>) -> u64 {
deterministic_hash(&(0u8, binder))
}

#[tracing::instrument(level = "trace", skip(s))]
pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>(
s: &S,
Expand Down
Loading

0 comments on commit 4d4812a

Please sign in to comment.