From a03373dc9e0449575771f920e419f5cd40420fb0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 8 Feb 2024 14:12:32 +0100
Subject: Make minor updates

---
 compiler/InterpreterStatements.ml | 15 ++++++++-------
 compiler/InterpreterUtils.ml      |  2 ++
 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
-- 
cgit v1.2.3