Preliminary support for parent clauses #25
Conversation
| let m = build_trait_clause_mapping env [ parent_clause ] in | ||
| List.map (fun ((clause_id, m), v) -> | ||
| (* This is the parent clause `i` of `clause_id` -- see comments in charon/types.rs *) | ||
| let id = C.(ParentClause (clause_id, trait_id, TraitClauseId.of_int i)) in |
There was a problem hiding this comment.
slightly strange that I have to rebuild this myself, please check that I'm doing the right thing
There was a problem hiding this comment.
I'm surprised too, what happens if you use the existing TraitClauseIds? If they're out of sync this is a bug in Charon.
There was a problem hiding this comment.
well I'm recursing into the parent clause and it has its own clause id relative to itself, without the ParentClause around it
| [] | ||
| in | ||
| types @ type_args, clause_const_generics @ const_generics @ const_generic_args, trait_refs' @ trait_refs | ||
| types @ type_args, const_generics @ const_generic_args, trait_refs' @ trait_refs |
There was a problem hiding this comment.
this is an unrelated change that removes dead code
| @@ -1025,57 +1026,68 @@ let rec expression_of_fn_ptr env depth (fn_ptr: C.fn_ptr) = | |||
| anyhow. *) | |||
| [] | |||
| else | |||
| List.concat_map (fun (trait_ref: C.trait_ref) -> | |||
| let name = string_of_name env (env.get_nth_trait_decl trait_ref.trait_decl_ref.trait_decl_id).name in | |||
| (* MUST have the same structure as build_trait_clause_mapping *) | |||
There was a problem hiding this comment.
this populates the trait method references at call-site, so we need to materialize function pointers exactly as expected by the signature, which is determined by build_trait_clause_mapping
| let fn_ptr = fst3 (expression_of_fn_ptr env (depth ^ " ") fn_ptr) in | ||
| fn_ptr | ||
| ) (trait_impl.required_methods @ trait_impl.provided_methods) @ | ||
| build_trait_ref_mapping (" " ^ depth) trait_ref.generics.trait_refs |
There was a problem hiding this comment.
here, the idea is that after filling out required and provided methods, this should match what is done in build_trait_clause_mapping for the parent clauses -- but I'm not sure this is the right way, so please check!
There was a problem hiding this comment.
So the assumption is that the list of trait_refs clauses matches the required list of clause arguments to the trait? That feels correct. I've been wanting to provide a better API for things like that but I'm not sure how yet.
There was a problem hiding this comment.
ok, well I believe this should provide a good use-case for that :-)
| (* Caller it itself polymorphic and refers to one of its own clauses to synthesize | ||
| the clause arguments at call-site. We must pass whatever is relevant for this | ||
| clause, *transitively* (this means all the reachable parents). *) | ||
| let rec relevant = function |
There was a problem hiding this comment.
insofar as I understand, when the caller is clause-polymorphic, and the callee is clause-polymorphic too, then I only see a single Clause _ reference at call-site, and it's up to me to remember that this trait bound requires parent bounds too, and materialize method references for the parent, too
There was a problem hiding this comment.
Mm yes, charon models a clause as "containing" its parent clauses, so we don't mention the parent clauses at call site. I think you should never think of a clause without its parents, so a given clause should list all of its methods including parent ones, no?
There was a problem hiding this comment.
I think it's fine, yes
| @@ -1582,13 +1594,6 @@ let decls_of_declarations (env: env) (d: C.declaration_group): K.decl list = | |||
| let clause_mapping = build_trait_clause_mapping env signature.C.generics.trait_clauses in | |||
| debug_trait_clause_mapping env clause_mapping; | |||
|
|
|||
| (* In definition fn f<T: Foo<42>>, associates [ 42 ] to clause Foo *) | |||
There was a problem hiding this comment.
just removing dead code
|
The next phase requires a little more work: I need to be handle trait clause bounds in trait impl methods, which is non-trivial (see test/where_clauses), so I'm going to leave it at this for now -- I cannot handle trait instances of the form Parent(Self, ...) yet. So let's merge this since it already improves the state of things, once I get a green-light that what I'm doing vaguely makes sense. |
|
Thanks for the comments @Nadrieril it's good to know my assumptions are correct. I'll merge this for now, and ping me if you want to discuss this ParentClause business a little bit more (but the more I think about it, the more I think there's nothing wrong on the Charon side) |
This should be enough to unblock cryspen/libcrux#308
This is not enough to make test-where_clauses go through, so I still want to leave this open until I get my testcase to work