Fix some issues

7 files changed, 81 insertions, 16 deletions

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index bce0fb11..92cd464e 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -136,7 +136,7 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty =
           ("ctx_normalize_ty: trait type: " ^ ctx.ty_to_string ty
          ^ "\n- trait_ref: "
           ^ ctx.trait_ref_to_string trait_ref
-          ^ "\n- raw trait ref: "
+          ^ "\n- raw trait ref:\n"
           ^ T.show_trait_ref ctx.pp_r trait_ref));
       (* Normalize and attempt to project the type from the trait ref *)
       let trait_ref = ctx_normalize_trait_ref ctx trait_ref in
@@ -197,7 +197,7 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty =
                 ("ctx_normalize_ty: trait type: not a trait ref: "
                ^ ctx.ty_to_string ty ^ "\n- trait_ref: "
                 ^ ctx.trait_ref_to_string trait_ref
-                ^ "\n- raw trait ref: "
+                ^ "\n- raw trait ref:\n"
                 ^ T.show_trait_ref ctx.pp_r trait_ref));
             (* We can't project *)
             assert (trait_instance_id_is_local_clause trait_ref.trait_id);
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index df77959e..65760d94 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -5,6 +5,7 @@ open LlbcAst
 module V = Values
 open ValuesUtils
 open Identifiers
+module L = Logging
 
 (** The [Id] module for dummy variables.
 
@@ -17,6 +18,9 @@ IdGen ()
 
 type dummy_var_id = DummyVarId.id [@@deriving show, ord]
 
+(** The local logger *)
+let log = L.contexts_log
+
 (** Some global counters.
 
   Note that those counters were initially stored in {!eval_ctx} values,
@@ -449,6 +453,15 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
 *)
 let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
     =
+  log#ldebug
+    (lazy
+      ("push_vars:\n"
+      ^ String.concat "\n"
+          (List.map
+             (fun (var, value) ->
+               (* We can unfortunately not use Print because it depends on Contexts... *)
+               show_var var ^ " -> " ^ V.show_typed_value value)
+             vars)));
   assert (
     List.for_all
       (fun (var, (value : typed_value)) -> var.var_ty = value.ty)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index b5e9fcb9..4ce6dae8 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -64,15 +64,39 @@ let initialize_eval_context (ctx : C.decls_ctx)
     C.ended_regions = T.RegionId.Set.empty;
   }
 
-(** Instantiate a function signature for a symbolic execution *)
-let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (fdef : A.fun_decl) :
+(** Small helper.
+
+    Normalize an instantiated function signature provided we used this signature
+    to compute a normalization map (for the associated types) and that we added
+    it in the context.
+ *)
+let normalize_inst_fun_sig (ctx : C.eval_ctx) (sg : A.inst_fun_sig) :
     A.inst_fun_sig =
+  let { A.regions_hierarchy = _; trait_type_constraints = _; inputs; output } =
+    sg
+  in
+  let norm = AssociatedTypes.ctx_normalize_rty ctx in
+  let inputs = List.map norm inputs in
+  let output = norm output in
+  { sg with A.inputs; output }
+
+(** Instantiate a function signature for a symbolic execution.
+
+    We return a new context because we compute and add the type normalization
+    map in the same step.
+
+    **WARNING**: this doesn't normalize the types. This step has to be done
+    separately. Remark: we need to normalize essentially because of the where
+    clauses (we are not considering a function call, so we don't need to
+    normalize because a trait clause was instantiated with a specific trait ref).
+ *)
+let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (fdef : A.fun_decl) :
+    C.eval_ctx * A.inst_fun_sig =
   let sg = fdef.signature in
   let tr_self =
     match fdef.kind with
     | RegularKind | TraitMethodImpl _ -> T.UnknownTrait __FUNCTION__
-    | TraitMethodDecl _ | TraitMethodProvided _ ->
-        raise (Failure "Unimplemented")
+    | TraitMethodDecl _ | TraitMethodProvided _ -> T.Self
   in
   let generics =
     let { T.regions; types; const_generics; trait_clauses } = sg.generics in
@@ -98,12 +122,27 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (fdef : A.fun_decl) :
           let { T.trait_id = trait_decl_id; generics; _ } = c in
           let generics = Subst.generic_args_substitute subst generics in
           let trait_decl_ref = { T.trait_decl_id; decl_generics = generics } in
-          { T.trait_id = T.Clause c.clause_id; generics; trait_decl_ref })
+          (* Note that because we directly refer to the clause, we give it
+             empty generics *)
+          {
+            T.trait_id = T.Clause c.clause_id;
+            generics = TypesUtils.mk_empty_generic_args;
+            trait_decl_ref;
+          })
         trait_clauses
     in
     { T.regions; types; const_generics; trait_refs }
   in
-  instantiate_fun_sig ctx generics tr_self sg
+  let inst_sg = instantiate_fun_sig ctx generics tr_self sg in
+  (* Compute the normalization maps *)
+  let ctx =
+    AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
+      inst_sg.trait_type_constraints
+  in
+  (* Normalize the signature *)
+  let inst_sg = normalize_inst_fun_sig ctx inst_sg in
+  (* Return *)
+  (ctx, inst_sg)
 
 (** Initialize an evaluation context to execute a function.
 
@@ -140,13 +179,10 @@ let initialize_symbolic_context_for_fun (ctx : C.decls_ctx) (fdef : A.fun_decl)
     initialize_eval_context ctx region_groups sg.generics.types
       sg.generics.const_generics
   in
-  (* Instantiate the signature *)
-  let inst_sg = symbolic_instantiate_fun_sig ctx fdef in
-  (* Compute the normalization maps *)
-  let ctx =
-    AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
-      inst_sg.trait_type_constraints
-  in
+  (* Instantiate the signature. This updates the context because we compute
+     at the same time the normalization map for the associated types.
+  *)
+  let ctx, inst_sg = symbolic_instantiate_fun_sig ctx fdef in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
     List.map (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) inst_sg.inputs
@@ -221,7 +257,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
    * an instantiation of the signature, so that we use fresh
    * region ids for the return abstractions. *)
   let sg = fdef.signature in
-  let ret_inst_sg = symbolic_instantiate_fun_sig ctx fdef in
+  let _, ret_inst_sg = symbolic_instantiate_fun_sig ctx fdef in
   let ret_rty = ret_inst_sg.output in
   (* Move the return value out of the return variable *)
   let pop_return_value = is_regular_return in
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 97fb80f4..88e20a92 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -664,6 +664,13 @@ let eval_assumed_function_call_concrete (config : C.config)
 
 let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args)
     (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+  log#ldebug
+    (lazy
+      ("instantiate_fun_sig:" ^ "\n- generics: "
+      ^ egeneric_args_to_string ctx generics
+      ^ "\n- tr_self: "
+      ^ rtrait_instance_id_to_string ctx tr_self
+      ^ "\n- sg: " ^ fun_sig_to_string ctx sg));
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 8525be29..6fde8d68 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -39,6 +39,8 @@ let typed_avalue_to_string = PA.typed_avalue_to_string
 let place_to_string = PA.place_to_string
 let operand_to_string = PA.operand_to_string
 let egeneric_args_to_string = PA.egeneric_args_to_string
+let rtrait_instance_id_to_string = PA.rtrait_instance_id_to_string
+let fun_sig_to_string = PA.fun_sig_to_string
 let fun_decl_to_string = PA.fun_decl_to_string
 let call_to_string = PA.call_to_string
 
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index d0f5b0c5..59abbfc7 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -9,6 +9,9 @@ let pre_passes_log = L.get_logger "MainLogger.PrePasses"
 (** Logger for Translate *)
 let translate_log = L.get_logger "MainLogger.Translate"
 
+(** Logger for Contexts *)
+let contexts_log = L.get_logger "MainLogger.Contexts"
+
 (** Logger for PureUtils *)
 let pure_utils_log = L.get_logger "MainLogger.PureUtils"
 
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 93a1f970..522d9fdd 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -732,6 +732,10 @@ module EvalCtxLlbcAst = struct
     let fmt = PC.eval_ctx_to_ast_formatter ctx in
     PA.fun_decl_to_string fmt "" "  " f
 
+  let fun_sig_to_string (ctx : C.eval_ctx) (x : A.fun_sig) : string =
+    let fmt = PC.eval_ctx_to_ast_formatter ctx in
+    PA.fun_sig_to_string fmt "" "  " x
+
   let statement_to_string (ctx : C.eval_ctx) (indent : string)
       (indent_incr : string) (e : A.statement) : string =
     let fmt = PC.eval_ctx_to_ast_formatter ctx in