diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterStatements.ml | 15 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/Print.ml | 4 |
3 files changed, 14 insertions, 7 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index c17c1563..eef9e2c9 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -769,9 +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))); + ^ "\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 *) @@ -900,9 +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 method *) - let generics = Option.get func.trait_and_method_generic_args in + (* 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 @@ -1030,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 diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 667c5080..243cf67b 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -43,6 +43,8 @@ let fun_sig_to_string = Print.EvalCtx.fun_sig_to_string let inst_fun_sig_to_string = Print.EvalCtx.inst_fun_sig_to_string let ty_to_string = Print.EvalCtx.ty_to_string let generic_args_to_string = Print.EvalCtx.generic_args_to_string +let trait_ref_to_string = Print.EvalCtx.trait_ref_to_string +let trait_decl_ref_to_string = Print.EvalCtx.trait_decl_ref_to_string let fun_id_or_trait_method_ref_to_string = Print.EvalCtx.fun_id_or_trait_method_ref_to_string diff --git a/compiler/Print.ml b/compiler/Print.ml index 0c69bd05..36aa2cb9 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -531,6 +531,10 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in trait_ref_to_string env x + let trait_decl_ref_to_string (ctx : eval_ctx) (x : trait_decl_ref) : string = + let env = eval_ctx_to_fmt_env ctx in + trait_decl_ref_to_string env x + let trait_instance_id_to_string (ctx : eval_ctx) (x : trait_instance_id) : string = let env = eval_ctx_to_fmt_env ctx in |