diff options
| author | Son HO | 2024-03-17 05:10:36 +0100 |
|---|---|---|
| committer | GitHub | 2024-03-17 05:10:36 +0100 |
| commit | d56946242859e0d375c1d44585b9da6d5fbe94cb (patch) | |
| tree | 4589586257210809913e225192a15464cb91851f /compiler/InterpreterStatements.ml | |
| parent | c33a9807cf6aa21b2364449ee756ebf93de19eca (diff) | |
| parent | ee3e26e7b639bc7282d0c3777f9460e975ef232f (diff) | |
Merge pull request #91 from AeneasVerif/son/hax
Prepare the merge in hax
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterStatements.ml | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 0cf8b88a..eef9e2c9 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -769,12 +769,8 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) ("trait method call:\n- call: " ^ call_to_string ctx call ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" ^ generic_args_to_string ctx func.generics - ^ "\n- trait and method generics:\n" - ^ generic_args_to_string ctx - (Option.get func.trait_and_method_generic_args))); - (* When instantiating, we need to group the generics for the trait ref - and the method *) - let generics = Option.get func.trait_and_method_generic_args in + ^ "\n- trait_ref.trait_decl_ref: " + ^ trait_decl_ref_to_string ctx trait_ref.trait_decl_ref)); (* Lookup the trait method signature - there are several possibilities depending on whethere we call a top-level trait method impl or the method from a local clause *) @@ -794,6 +790,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) | Some (_, id) -> (* This is a required method *) let method_def = ctx_lookup_fun_decl ctx id in + (* We have to concatenate the generics for the impl + and the generics for the method *) + let generics = + merge_generic_args trait_ref.generics func.generics + in (* Instantiate *) let tr_self = TraitRef trait_ref in let fid : fun_id = FRegular id in @@ -898,6 +899,12 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) + (* When instantiating, we need to group the generics for the + trait ref and the generics for the method *) + let generics = + TypesUtils.merge_generic_args + trait_ref.trait_decl_ref.decl_generics func.generics + in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies @@ -1025,7 +1032,6 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) : { func = FunId (FRegular global.body); generics = TypesUtils.empty_generic_args; - trait_and_method_generic_args = None; } in let call = { func = FnOpRegular func; args = []; dest } in |