Compute the normalized trait types maps and update Interpreter

1 files changed, 58 insertions, 30 deletions

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index eb66013d..b5e9fcb9 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -32,10 +32,12 @@ let compute_contexts (m : A.crate) : C.decls_ctx =
   let trait_impls_ctx = { C.trait_impls } in
   { C.type_ctx; fun_ctx; global_ctx; trait_decls_ctx; trait_impls_ctx }
 
+(** **WARNING**: this function doesn't compute the normalized types
+    (for the trait type aliases). This should be computed afterwards.
+ *)
 let initialize_eval_context (ctx : C.decls_ctx)
     (region_groups : T.RegionGroupId.id list) (type_vars : T.type_var list)
-    (const_generic_vars : T.const_generic_var list)
-    (trait_clauses : T.etrait_ref list) : C.eval_ctx =
+    (const_generic_vars : T.const_generic_var list) : C.eval_ctx =
   C.reset_global_counters ();
   let const_generic_vars_map =
     T.ConstGenericVarId.Map.of_list
@@ -56,11 +58,53 @@ let initialize_eval_context (ctx : C.decls_ctx)
     C.type_vars;
     C.const_generic_vars;
     C.const_generic_vars_map;
-    C.trait_clauses;
+    C.norm_trait_etypes = C.ETraitTypeRefMap.empty (* Empty for now *);
+    C.norm_trait_rtypes = C.RTraitTypeRefMap.empty (* Empty for now *);
     C.env = [ C.Frame ];
     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) :
+    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")
+  in
+  let generics =
+    let { T.regions; types; const_generics; trait_clauses } = sg.generics in
+    let regions = List.map (fun _ -> T.Erased) regions in
+    let types = List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) types in
+    let const_generics =
+      List.map
+        (fun (v : T.const_generic_var) -> T.ConstGenericVar v.T.index)
+        const_generics
+    in
+    (* Annoying that we have to generate this substitution here *)
+    let r_subst _ = raise (Failure "Unexpected region") in
+    let ty_subst = Subst.make_type_subst_from_vars sg.generics.types types in
+    let cg_subst =
+      Subst.make_const_generic_subst_from_vars sg.generics.const_generics
+        const_generics
+    in
+    let tr_subst _ = raise (Failure "Unexpected local trait clause") in
+    let subst = { Subst.r_subst; ty_subst; cg_subst; tr_subst; tr_self } in
+    let trait_refs =
+      List.map
+        (fun (c : T.trait_clause) ->
+          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 })
+        trait_clauses
+    in
+    { T.regions; types; const_generics; trait_refs }
+  in
+  instantiate_fun_sig ctx generics tr_self sg
+
 (** Initialize an evaluation context to execute a function.
 
     Introduces local variables initialized in the following manner:
@@ -94,18 +138,15 @@ let initialize_symbolic_context_for_fun (ctx : C.decls_ctx) (fdef : A.fun_decl)
   in
   let ctx =
     initialize_eval_context ctx region_groups sg.generics.types
-      sg.generics.const_generics sg.generics.trait_clauses
+      sg.generics.const_generics
   in
   (* Instantiate the signature *)
-  let type_params =
-    List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) sg.type_params
-  in
-  let cg_params =
-    List.map
-      (fun (v : T.const_generic_var) -> T.ConstGenericVar v.T.index)
-      sg.const_generic_params
+  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
-  let inst_sg = instantiate_fun_sig type_params cg_params sg 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
@@ -180,15 +221,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 type_params =
-    List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) sg.type_params
-  in
-  let cg_params =
-    List.map
-      (fun (v : T.const_generic_var) -> T.ConstGenericVar v.T.index)
-      sg.const_generic_params
-  in
-  let ret_inst_sg = instantiate_fun_sig type_params cg_params sg 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
@@ -362,19 +395,14 @@ let evaluate_function_symbolic_synthesize_backward_from_return
       for the synthesis)
     - the symbolic AST generated by the symbolic execution
  *)
-let evaluate_function_symbolic (synthesize : bool)
-    (type_context : C.type_context) (fun_context : C.fun_context)
-    (global_context : C.global_context) (fdef : A.fun_decl) :
-    V.symbolic_value list * SA.expression option =
+let evaluate_function_symbolic (synthesize : bool) (ctx : C.decls_ctx)
+    (fdef : A.fun_decl) : V.symbolic_value list * SA.expression option =
   (* Debug *)
   let name_to_string () = Print.fun_name_to_string fdef.A.name in
   log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ()));
 
   (* Create the evaluation context *)
-  let ctx, input_svs, inst_sg =
-    initialize_symbolic_context_for_fun type_context fun_context global_context
-      fdef
-  in
+  let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in
 
   (* Create the continuation to finish the evaluation *)
   let config = C.mk_config C.SymbolicMode in
@@ -518,7 +546,7 @@ module Test = struct
 
     (* Create the evaluation context *)
     let decls_ctx = compute_contexts crate in
-    let ctx = initialize_eval_context decls_ctx [] [] [] [] in
+    let ctx = initialize_eval_context decls_ctx [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
     let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in