From 26c25bf375742cf4d5a0ab160b9646e90c067f18 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 18 Aug 2023 10:27:55 +0200
Subject: Update following the introduction of ConstantExpr

---
 compiler/InterpreterUtils.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 7bd37550..637f1b1e 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -255,7 +255,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
               raise Found
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate ->
+        | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate
+        | V.ConstGeneric ->
             ()
     end
   in
-- 
cgit v1.2.3


From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 31 Aug 2023 12:47:43 +0200
Subject: Start adding support for traits

---
 compiler/InterpreterUtils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 637f1b1e..1513465c 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -273,7 +273,7 @@ let rvalue_get_place (rv : E.rvalue) : E.place option =
   match rv with
   | Use (Copy p | Move p) -> Some p
   | Use (Constant _) -> None
-  | Ref (p, _) -> Some p
+  | RvRef (p, _) -> Some p
   | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
-- 
cgit v1.2.3


From c6b88a2e54b7697262ad3677ad7500471c68e332 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 10 Sep 2023 21:07:06 +0200
Subject: Add support for the trait associated constants

---
 compiler/InterpreterUtils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 1513465c..0986c53b 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -256,7 +256,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
         | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate
-        | V.ConstGeneric ->
+        | V.ConstGeneric | V.TraitConst ->
             ()
     end
   in
-- 
cgit v1.2.3


From 5921be8e2e8955db5101354d8bf29ae6a3693f48 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Sep 2023 06:35:07 +0200
Subject: Make progress on correctly handling trait method calls in the
 symbolic execution

---
 compiler/InterpreterUtils.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 0986c53b..8a7e8c52 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -38,6 +38,9 @@ let typed_value_to_string = PA.typed_value_to_string
 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 call_to_string = PA.call_to_string
+let trait_impl_to_string = PA.trait_impl_to_string
 let statement_to_string ctx = PA.statement_to_string ctx "" "  "
 let statement_to_string_with_tab ctx = PA.statement_to_string ctx "  " "  "
 let env_elem_to_string ctx = PA.env_elem_to_string ctx "" "  "
-- 
cgit v1.2.3


From 78a2731924aa13989998c6be4a5a6865ce5098aa Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Sep 2023 07:33:30 +0200
Subject: Make minor modifications

---
 compiler/InterpreterUtils.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 8a7e8c52..8525be29 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -39,8 +39,12 @@ 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 fun_decl_to_string = PA.fun_decl_to_string
 let call_to_string = PA.call_to_string
-let trait_impl_to_string = PA.trait_impl_to_string
+
+let trait_impl_to_string ctx =
+  PA.trait_impl_to_string { ctx with type_vars = []; const_generic_vars = [] }
+
 let statement_to_string ctx = PA.statement_to_string ctx "" "  "
 let statement_to_string_with_tab ctx = PA.statement_to_string ctx "  " "  "
 let env_elem_to_string ctx = PA.env_elem_to_string ctx "" "  "
-- 
cgit v1.2.3


From 60aa9ff5b31e47ecc2ac2dff55ee06582af62806 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Sep 2023 23:39:13 +0200
Subject: Fix some issues

---
 compiler/InterpreterUtils.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'compiler/InterpreterUtils.ml')

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
 
-- 
cgit v1.2.3


From 353a9627cf39290f2fe841a45e52726aa9fe6512 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 17 Sep 2023 06:58:17 +0200
Subject: Normalize the function signatures before translation to pure

---
 compiler/InterpreterUtils.ml | 105 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 105 insertions(+)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 6fde8d68..7aaee6ff 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -10,6 +10,11 @@ open TypesUtils
 module PA = Print.EvalCtxLlbcAst
 open Cps
 
+(* TODO: we should probably rename the file to ContextsUtils *)
+
+(** The local logger *)
+let log = L.interpreter_log
+
 (** Some utilities *)
 
 (** Auxiliary function - call a function which requires a continuation,
@@ -413,3 +418,103 @@ let compute_contexts_ids (ctxl : C.eval_ctx list) : ids_sets * ids_to_values =
 (** Compute the sets of ids found in a context. *)
 let compute_context_ids (ctx : C.eval_ctx) : ids_sets * ids_to_values =
   compute_contexts_ids [ 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) : C.eval_ctx =
+  C.reset_global_counters ();
+  let const_generic_vars_map =
+    T.ConstGenericVarId.Map.of_list
+      (List.map
+         (fun (cg : T.const_generic_var) ->
+           let ty = TypesUtils.ety_no_regions_to_rty (T.Literal cg.ty) in
+           let cv = mk_fresh_symbolic_typed_value V.ConstGeneric ty in
+           (cg.index, cv))
+         const_generic_vars)
+  in
+  {
+    C.type_context = ctx.type_ctx;
+    C.fun_context = ctx.fun_ctx;
+    C.global_context = ctx.global_ctx;
+    C.trait_decls_context = ctx.trait_decls_ctx;
+    C.trait_impls_context = ctx.trait_impls_ctx;
+    C.region_groups;
+    C.type_vars;
+    C.const_generic_vars;
+    C.const_generic_vars_map;
+    C.norm_trait_etypes = C.ETraitTypeRefMap.empty (* Empty for now *);
+    C.norm_trait_rtypes = C.RTraitTypeRefMap.empty (* Empty for now *);
+    C.norm_trait_stypes = C.STraitTypeRefMap.empty (* Empty for now *);
+    C.env = [ C.Frame ];
+    C.ended_regions = T.RegionId.Set.empty;
+  }
+
+(** Instantiate a function signature, introducing **fresh** abstraction ids and
+    region ids. This is mostly used in preparation of function calls (when
+    evaluating in symbolic mode).
+
+    Note: there are no region parameters, because they should be erased.
+ *)
+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 =
+    List.map
+      (fun rg ->
+        let abs_id = C.fresh_abstraction_id () in
+        (rg.T.id, abs_id))
+      sg.regions_hierarchy
+  in
+  let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t =
+    List.fold_left
+      (fun mp (rg_id, abs_id) -> T.RegionGroupId.Map.add rg_id abs_id mp)
+      T.RegionGroupId.Map.empty rg_abs_ids_bindings
+  in
+  let asubst (rg_id : T.RegionGroupId.id) : V.AbstractionId.id =
+    T.RegionGroupId.Map.find rg_id asubst_map
+  in
+  (* Generate fresh regions and their substitutions *)
+  let _, rsubst, _ = Subst.fresh_regions_with_substs sg.generics.regions in
+  (* Generate the type substitution
+   * Note that we need the substitution to map the type variables to
+   * {!rty} types (not {!ety}). In order to do that, we convert the
+   * type parameters to types with regions. This is possible only
+   * if those types don't contain any regions.
+   * This is a current limitation of the analysis: there is still some
+   * work to do to properly handle full type parametrization.
+   * *)
+  let rtype_params = List.map ety_no_regions_to_rty generics.types in
+  let tsubst = Subst.make_type_subst_from_vars sg.generics.types rtype_params in
+  let cgsubst =
+    Subst.make_const_generic_subst_from_vars sg.generics.const_generics
+      generics.const_generics
+  in
+  (* TODO: something annoying with the trait ref subst: we need to use region
+     types, but the arguments use erased regions. For now we use the fact
+     that no regions should appear inside. In the future: we should merge
+     ety and rty. *)
+  let trait_refs =
+    List.map TypesUtils.etrait_ref_no_regions_to_gr_trait_ref
+      generics.trait_refs
+  in
+  let tr_subst =
+    Subst.make_trait_subst_from_clauses sg.generics.trait_clauses trait_refs
+  in
+  (* Substitute the signature *)
+  let inst_sig =
+    AssociatedTypes.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst
+      tr_subst tr_self sg
+  in
+  (* Return *)
+  inst_sig
-- 
cgit v1.2.3


From f11d5186b467df318f7c09eedf8b5629c165b453 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 20 Oct 2023 15:05:00 +0200
Subject: Start updating to handle function pointers

---
 compiler/InterpreterUtils.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 7aaee6ff..6e08e553 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -46,6 +46,11 @@ 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 inst_fun_sig_to_string = PA.inst_fun_sig_to_string
+
+let fun_id_or_trait_method_ref_to_string =
+  PA.fun_id_or_trait_method_ref_to_string
+
 let fun_decl_to_string = PA.fun_decl_to_string
 let call_to_string = PA.call_to_string
 
-- 
cgit v1.2.3


From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 19:28:56 +0100
Subject: Remove the 'r type variable from the ty type definition

---
 compiler/InterpreterUtils.ml | 83 ++++++++++++++++++++------------------------
 1 file changed, 38 insertions(+), 45 deletions(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 6e08e553..6f62b577 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -31,8 +31,6 @@ let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx =
 
 let eval_ctx_to_string_no_filter = Print.Contexts.eval_ctx_to_string_no_filter
 let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
-let ety_to_string = PA.ety_to_string
-let rty_to_string = PA.rty_to_string
 let symbolic_value_to_string = PA.symbolic_value_to_string
 let borrow_content_to_string = PA.borrow_content_to_string
 let loan_content_to_string = PA.loan_content_to_string
@@ -43,8 +41,6 @@ let typed_value_to_string = PA.typed_value_to_string
 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 inst_fun_sig_to_string = PA.inst_fun_sig_to_string
 
@@ -66,8 +62,7 @@ let abs_to_string ctx = PA.abs_to_string ctx "" "  "
 let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
   sv0.V.sv_id = sv1.V.sv_id
 
-let mk_var (index : E.VarId.id) (name : string option) (var_ty : T.ety) : A.var
-    =
+let mk_var (index : E.VarId.id) (name : string option) (var_ty : T.ty) : A.var =
   { A.index; name; var_ty }
 
 (** Small helper - TODO: move *)
@@ -75,25 +70,32 @@ let mk_place_from_var_id (var_id : E.VarId.id) : E.place =
   { var_id; projection = [] }
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (sv_kind : V.sv_kind) (ty : T.rty) :
-    V.symbolic_value =
+let mk_fresh_symbolic_value (sv_kind : V.sv_kind) (ty : T.ty) : V.symbolic_value
+    =
+  (* Sanity check *)
+  assert (ty_is_rty ty);
   let sv_id = C.fresh_symbolic_value_id () in
   let svalue = { V.sv_kind; V.sv_id; V.sv_ty = ty } in
   svalue
 
+let mk_fresh_symbolic_value_from_no_regions_ty (sv_kind : V.sv_kind) (ty : T.ty)
+    : V.symbolic_value =
+  assert (ty_no_regions ty);
+  mk_fresh_symbolic_value sv_kind ty
+
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.rty) :
+let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.ty) :
     V.typed_value =
+  assert (ty_is_rty rty);
   let ty = Subst.erase_regions rty in
   (* Generate the fresh a symbolic value *)
   let value = mk_fresh_symbolic_value sv_kind rty in
   let value = V.Symbolic value in
   { V.value; V.ty }
 
-(** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value_from_ety (sv_kind : V.sv_kind) (ety : T.ety) :
-    V.typed_value =
-  let ty = TypesUtils.ety_no_regions_to_rty ety in
+let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : V.sv_kind)
+    (ty : T.ty) : V.typed_value =
+  assert (ty_no_regions ty);
   mk_fresh_symbolic_typed_value sv_kind ty
 
 (** Create a typed value from a symbolic value. *)
@@ -122,7 +124,8 @@ let mk_aproj_loans_value_from_symbolic_value (regions : T.RegionId.Set.t)
 
 (** Create a borrows projector from a symbolic value *)
 let mk_aproj_borrows_from_symbolic_value (proj_regions : T.RegionId.Set.t)
-    (svalue : V.symbolic_value) (proj_ty : T.rty) : V.aproj =
+    (svalue : V.symbolic_value) (proj_ty : T.ty) : V.aproj =
+  assert (ty_is_rty proj_ty);
   if ty_has_regions_in_set proj_regions proj_ty then
     V.AProjBorrows (svalue, proj_ty)
   else V.AIgnoredProjBorrows
@@ -193,7 +196,7 @@ exception FoundGBorrowContent of g_borrow_content
 exception FoundGLoanContent of g_loan_content
 
 (** Utility exception *)
-exception FoundAProjBorrows of V.symbolic_value * T.rty
+exception FoundAProjBorrows of V.symbolic_value * T.ty
 
 let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
     bool =
@@ -235,7 +238,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
 *)
 let symbolic_value_has_ended_regions (ended_regions : T.RegionId.Set.t)
     (s : V.symbolic_value) : bool =
-  let regions = rty_regions s.V.sv_ty in
+  let regions = ty_regions s.V.sv_ty in
   not (T.RegionId.Set.disjoint regions ended_regions)
 
 (** Check if a {!type:V.value} contains [⊥].
@@ -435,7 +438,7 @@ let initialize_eval_context (ctx : C.decls_ctx)
     T.ConstGenericVarId.Map.of_list
       (List.map
          (fun (cg : T.const_generic_var) ->
-           let ty = TypesUtils.ety_no_regions_to_rty (T.Literal cg.ty) in
+           let ty = T.TLiteral cg.ty in
            let cv = mk_fresh_symbolic_typed_value V.ConstGeneric ty in
            (cg.index, cv))
          const_generic_vars)
@@ -450,28 +453,27 @@ let initialize_eval_context (ctx : C.decls_ctx)
     C.type_vars;
     C.const_generic_vars;
     C.const_generic_vars_map;
-    C.norm_trait_etypes = C.ETraitTypeRefMap.empty (* Empty for now *);
-    C.norm_trait_rtypes = C.RTraitTypeRefMap.empty (* Empty for now *);
-    C.norm_trait_stypes = C.STraitTypeRefMap.empty (* Empty for now *);
-    C.env = [ C.Frame ];
+    C.norm_trait_types = C.TraitTypeRefMap.empty (* Empty for now *);
+    C.env = [ C.EFrame ];
     C.ended_regions = T.RegionId.Set.empty;
   }
 
 (** Instantiate a function signature, introducing **fresh** abstraction ids and
     region ids. This is mostly used in preparation of function calls (when
     evaluating in symbolic mode).
-
-    Note: there are no region parameters, because they should be erased.
  *)
-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 =
+let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
+    (tr_self : T.trait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
   log#ldebug
     (lazy
       ("instantiate_fun_sig:" ^ "\n- generics: "
-      ^ egeneric_args_to_string ctx generics
+      ^ PA.generic_args_to_string ctx generics
       ^ "\n- tr_self: "
-      ^ rtrait_instance_id_to_string ctx tr_self
+      ^ PA.trait_instance_id_to_string ctx tr_self
       ^ "\n- sg: " ^ fun_sig_to_string ctx sg));
+  (* Erase the regions in the generics we use for the instantiation *)
+  let generics = Subst.generic_args_erase_regions generics in
+  let tr_self = Subst.trait_instance_id_erase_regions tr_self in
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
@@ -492,29 +494,20 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args)
   (* Generate fresh regions and their substitutions *)
   let _, rsubst, _ = Subst.fresh_regions_with_substs sg.generics.regions in
   (* Generate the type substitution
-   * Note that we need the substitution to map the type variables to
-   * {!rty} types (not {!ety}). In order to do that, we convert the
-   * type parameters to types with regions. This is possible only
-   * if those types don't contain any regions.
-   * This is a current limitation of the analysis: there is still some
-   * work to do to properly handle full type parametrization.
-   * *)
-  let rtype_params = List.map ety_no_regions_to_rty generics.types in
-  let tsubst = Subst.make_type_subst_from_vars sg.generics.types rtype_params in
+     Note that for now we don't support instantiating the type parameters with
+     types containing regions. *)
+  assert (List.for_all TypesUtils.ty_no_regions generics.types);
+  assert (TypesUtils.trait_instance_id_no_regions tr_self);
+  let tsubst =
+    Subst.make_type_subst_from_vars sg.generics.types generics.types
+  in
   let cgsubst =
     Subst.make_const_generic_subst_from_vars sg.generics.const_generics
       generics.const_generics
   in
-  (* TODO: something annoying with the trait ref subst: we need to use region
-     types, but the arguments use erased regions. For now we use the fact
-     that no regions should appear inside. In the future: we should merge
-     ety and rty. *)
-  let trait_refs =
-    List.map TypesUtils.etrait_ref_no_regions_to_gr_trait_ref
-      generics.trait_refs
-  in
   let tr_subst =
-    Subst.make_trait_subst_from_clauses sg.generics.trait_clauses trait_refs
+    Subst.make_trait_subst_from_clauses sg.generics.trait_clauses
+      generics.trait_refs
   in
   (* Substitute the signature *)
   let inst_sig =
-- 
cgit v1.2.3


From 746239e8f29de85f848d14e44eac8690e2065a1d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 20:41:58 +0100
Subject: Add the "V" prefix to most variants related to values

---
 compiler/InterpreterUtils.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 6f62b577..60747b2a 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -90,7 +90,7 @@ let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.ty) :
   let ty = Subst.erase_regions rty in
   (* Generate the fresh a symbolic value *)
   let value = mk_fresh_symbolic_value sv_kind rty in
-  let value = V.Symbolic value in
+  let value = V.VSymbolic value in
   { V.value; V.ty }
 
 let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : V.sv_kind)
@@ -101,7 +101,7 @@ let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : V.sv_kind)
 (** Create a typed value from a symbolic value. *)
 let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
     V.typed_value =
-  let av = V.Symbolic svalue in
+  let av = V.VSymbolic svalue in
   let av : V.typed_value =
     { V.value = av; V.ty = Subst.erase_regions svalue.V.sv_ty }
   in
@@ -204,7 +204,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
     object
       inherit [_] C.iter_eval_ctx as super
 
-      method! visit_Symbolic _ sv =
+      method! visit_VSymbolic _ sv =
         if sv.V.sv_id = sv_id then raise Found else ()
 
       method! visit_aproj env aproj =
@@ -251,7 +251,7 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
   let obj =
     object
       inherit [_] V.iter_typed_value
-      method! visit_Bottom _ = raise Found
+      method! visit_VBottom _ = raise Found
 
       method! visit_symbolic_value _ s =
         if symbolic_value_has_ended_regions ended_regions s then raise Found
-- 
cgit v1.2.3


From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 13 Nov 2023 13:27:02 +0100
Subject: Add RegionsHierarchy.ml

---
 compiler/InterpreterUtils.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 60747b2a..5e2746c5 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -474,6 +474,11 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
   (* Erase the regions in the generics we use for the instantiation *)
   let generics = Subst.generic_args_erase_regions generics in
   let tr_self = Subst.trait_instance_id_erase_regions tr_self in
+  (* Compute the regions hierarchy *)
+  let regions_hierarchy =
+    RegionsHierarchy.compute_regions_hierarchy_for_sig
+      ctx.type_context.type_decls sg
+  in
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
@@ -481,7 +486,7 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
       (fun rg ->
         let abs_id = C.fresh_abstraction_id () in
         (rg.T.id, abs_id))
-      sg.regions_hierarchy
+      regions_hierarchy
   in
   let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t =
     List.fold_left
@@ -512,7 +517,7 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
   (* Substitute the signature *)
   let inst_sig =
     AssociatedTypes.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst
-      tr_subst tr_self sg
+      tr_subst tr_self sg regions_hierarchy
   in
   (* Return *)
   inst_sig
-- 
cgit v1.2.3


From cb179ba97d2eafac07ac1208ab1e6ab4446f89df Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 13 Nov 2023 14:17:55 +0100
Subject: Make minor modifications

---
 compiler/InterpreterUtils.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 5e2746c5..e5a5b2ea 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -463,7 +463,8 @@ let initialize_eval_context (ctx : C.decls_ctx)
     evaluating in symbolic mode).
  *)
 let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
-    (tr_self : T.trait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+    (tr_self : T.trait_instance_id) (sg : A.fun_sig)
+    (regions_hierarchy : T.region_groups) : A.inst_fun_sig =
   log#ldebug
     (lazy
       ("instantiate_fun_sig:" ^ "\n- generics: "
@@ -474,11 +475,6 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
   (* Erase the regions in the generics we use for the instantiation *)
   let generics = Subst.generic_args_erase_regions generics in
   let tr_self = Subst.trait_instance_id_erase_regions tr_self in
-  (* Compute the regions hierarchy *)
-  let regions_hierarchy =
-    RegionsHierarchy.compute_regions_hierarchy_for_sig
-      ctx.type_context.type_decls sg
-  in
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
-- 
cgit v1.2.3


From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 15 Nov 2023 22:03:21 +0100
Subject: Start updating the name type, cleanup the names and the module
 abbrevs

---
 compiler/InterpreterUtils.ml | 367 +++++++++++++++++++++----------------------
 1 file changed, 179 insertions(+), 188 deletions(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index e5a5b2ea..ecd8f53f 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -1,25 +1,22 @@
-module T = Types
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module A = LlbcAst
-module L = Logging
+open Types
+open Values
+open Expressions
+open Contexts
+open LlbcAst
 open Utils
 open TypesUtils
-module PA = Print.EvalCtxLlbcAst
 open Cps
 
 (* TODO: we should probably rename the file to ContextsUtils *)
 
 (** The local logger *)
-let log = L.interpreter_log
+let log = Logging.interpreter_log
 
 (** Some utilities *)
 
 (** Auxiliary function - call a function which requires a continuation,
     and return the let context given to the continuation *)
-let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx =
+let get_cf_ctx_no_synth (f : cm_fun) (ctx : eval_ctx) : eval_ctx =
   let nctx = ref None in
   let cf ctx =
     assert (!nctx = None);
@@ -31,120 +28,120 @@ let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx =
 
 let eval_ctx_to_string_no_filter = Print.Contexts.eval_ctx_to_string_no_filter
 let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
-let symbolic_value_to_string = PA.symbolic_value_to_string
-let borrow_content_to_string = PA.borrow_content_to_string
-let loan_content_to_string = PA.loan_content_to_string
-let aborrow_content_to_string = PA.aborrow_content_to_string
-let aloan_content_to_string = PA.aloan_content_to_string
-let aproj_to_string = PA.aproj_to_string
-let typed_value_to_string = PA.typed_value_to_string
-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 fun_sig_to_string = PA.fun_sig_to_string
-let inst_fun_sig_to_string = PA.inst_fun_sig_to_string
+let name_to_string = Print.EvalCtx.name_to_string
+let symbolic_value_to_string = Print.EvalCtx.symbolic_value_to_string
+let borrow_content_to_string = Print.EvalCtx.borrow_content_to_string
+let loan_content_to_string = Print.EvalCtx.loan_content_to_string
+let aborrow_content_to_string = Print.EvalCtx.aborrow_content_to_string
+let aloan_content_to_string = Print.EvalCtx.aloan_content_to_string
+let aproj_to_string = Print.EvalCtx.aproj_to_string
+let typed_value_to_string = Print.EvalCtx.typed_value_to_string
+let typed_avalue_to_string = Print.EvalCtx.typed_avalue_to_string
+let place_to_string = Print.EvalCtx.place_to_string
+let operand_to_string = Print.EvalCtx.operand_to_string
+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 fun_id_or_trait_method_ref_to_string =
-  PA.fun_id_or_trait_method_ref_to_string
+  Print.EvalCtx.fun_id_or_trait_method_ref_to_string
 
-let fun_decl_to_string = PA.fun_decl_to_string
-let call_to_string = PA.call_to_string
+let fun_decl_to_string = Print.EvalCtx.fun_decl_to_string
+let call_to_string = Print.EvalCtx.call_to_string
 
 let trait_impl_to_string ctx =
-  PA.trait_impl_to_string { ctx with type_vars = []; const_generic_vars = [] }
+  Print.EvalCtx.trait_impl_to_string
+    { ctx with type_vars = []; const_generic_vars = [] }
 
-let statement_to_string ctx = PA.statement_to_string ctx "" "  "
-let statement_to_string_with_tab ctx = PA.statement_to_string ctx "  " "  "
-let env_elem_to_string ctx = PA.env_elem_to_string ctx "" "  "
+let statement_to_string ctx = Print.EvalCtx.statement_to_string ctx "" "  "
+
+let statement_to_string_with_tab ctx =
+  Print.EvalCtx.statement_to_string ctx "  " "  "
+
+let env_elem_to_string ctx = Print.EvalCtx.env_elem_to_string ctx "" "  "
 let env_to_string ctx env = eval_ctx_to_string { ctx with env }
-let abs_to_string ctx = PA.abs_to_string ctx "" "  "
+let abs_to_string ctx = Print.EvalCtx.abs_to_string ctx "" "  "
 
-let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
-  sv0.V.sv_id = sv1.V.sv_id
+let same_symbolic_id (sv0 : symbolic_value) (sv1 : symbolic_value) : bool =
+  sv0.sv_id = sv1.sv_id
 
-let mk_var (index : E.VarId.id) (name : string option) (var_ty : T.ty) : A.var =
-  { A.index; name; var_ty }
+let mk_var (index : VarId.id) (name : string option) (var_ty : ty) : var =
+  { index; name; var_ty }
 
 (** Small helper - TODO: move *)
-let mk_place_from_var_id (var_id : E.VarId.id) : E.place =
+let mk_place_from_var_id (var_id : VarId.id) : place =
   { var_id; projection = [] }
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (sv_kind : V.sv_kind) (ty : T.ty) : V.symbolic_value
-    =
+let mk_fresh_symbolic_value (sv_kind : sv_kind) (ty : ty) : symbolic_value =
   (* Sanity check *)
   assert (ty_is_rty ty);
-  let sv_id = C.fresh_symbolic_value_id () in
-  let svalue = { V.sv_kind; V.sv_id; V.sv_ty = ty } in
+  let sv_id = fresh_symbolic_value_id () in
+  let svalue = { sv_kind; sv_id; sv_ty = ty } in
   svalue
 
-let mk_fresh_symbolic_value_from_no_regions_ty (sv_kind : V.sv_kind) (ty : T.ty)
-    : V.symbolic_value =
+let mk_fresh_symbolic_value_from_no_regions_ty (sv_kind : sv_kind) (ty : ty) :
+    symbolic_value =
   assert (ty_no_regions ty);
   mk_fresh_symbolic_value sv_kind ty
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.ty) :
-    V.typed_value =
+let mk_fresh_symbolic_typed_value (sv_kind : sv_kind) (rty : ty) : typed_value =
   assert (ty_is_rty rty);
-  let ty = Subst.erase_regions rty in
+  let ty = Substitute.erase_regions rty in
   (* Generate the fresh a symbolic value *)
   let value = mk_fresh_symbolic_value sv_kind rty in
-  let value = V.VSymbolic value in
-  { V.value; V.ty }
+  let value = VSymbolic value in
+  { value; ty }
 
-let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : V.sv_kind)
-    (ty : T.ty) : V.typed_value =
+let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : sv_kind)
+    (ty : ty) : typed_value =
   assert (ty_no_regions ty);
   mk_fresh_symbolic_typed_value sv_kind ty
 
 (** Create a typed value from a symbolic value. *)
-let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
-    V.typed_value =
-  let av = V.VSymbolic svalue in
-  let av : V.typed_value =
-    { V.value = av; V.ty = Subst.erase_regions svalue.V.sv_ty }
+let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value =
+  let av = VSymbolic svalue in
+  let av : typed_value =
+    { value = av; ty = Substitute.erase_regions svalue.sv_ty }
   in
   av
 
 (** Create a loans projector value from a symbolic value.
     
     Checks if the projector will actually project some regions. If not,
-    returns {!V.AIgnored} ([_]).
+    returns {!AIgnored} ([_]).
     
     TODO: update to handle 'static
  *)
-let mk_aproj_loans_value_from_symbolic_value (regions : T.RegionId.Set.t)
-    (svalue : V.symbolic_value) : V.typed_avalue =
+let mk_aproj_loans_value_from_symbolic_value (regions : RegionId.Set.t)
+    (svalue : symbolic_value) : typed_avalue =
   if ty_has_regions_in_set regions svalue.sv_ty then
-    let av = V.ASymbolic (V.AProjLoans (svalue, [])) in
-    let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in
+    let av = ASymbolic (AProjLoans (svalue, [])) in
+    let av : typed_avalue = { value = av; ty = svalue.sv_ty } in
     av
-  else { V.value = V.AIgnored; ty = svalue.V.sv_ty }
+  else { value = AIgnored; ty = svalue.sv_ty }
 
 (** Create a borrows projector from a symbolic value *)
-let mk_aproj_borrows_from_symbolic_value (proj_regions : T.RegionId.Set.t)
-    (svalue : V.symbolic_value) (proj_ty : T.ty) : V.aproj =
+let mk_aproj_borrows_from_symbolic_value (proj_regions : RegionId.Set.t)
+    (svalue : symbolic_value) (proj_ty : ty) : aproj =
   assert (ty_is_rty proj_ty);
   if ty_has_regions_in_set proj_regions proj_ty then
-    V.AProjBorrows (svalue, proj_ty)
-  else V.AIgnoredProjBorrows
+    AProjBorrows (svalue, proj_ty)
+  else AIgnoredProjBorrows
 
 (** TODO: move *)
-let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool
-    =
-  match asb with
-  | V.AsbBorrow bid' -> bid' = bid
-  | V.AsbProjReborrows _ -> false
+let borrow_is_asb (bid : BorrowId.id) (asb : abstract_shared_borrow) : bool =
+  match asb with AsbBorrow bid' -> bid' = bid | AsbProjReborrows _ -> false
 
 (** TODO: move *)
-let borrow_in_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrows) : bool
-    =
+let borrow_in_asb (bid : BorrowId.id) (asb : abstract_shared_borrows) : bool =
   List.exists (borrow_is_asb bid) asb
 
 (** TODO: move *)
-let remove_borrow_from_asb (bid : V.BorrowId.id)
-    (asb : V.abstract_shared_borrows) : V.abstract_shared_borrows =
+let remove_borrow_from_asb (bid : BorrowId.id) (asb : abstract_shared_borrows) :
+    abstract_shared_borrows =
   let removed = ref 0 in
   let asb =
     List.filter
@@ -168,26 +165,26 @@ type ('a, 'b) concrete_or_abs = Concrete of 'a | Abstract of 'b
 [@@deriving show]
 
 (** Generic loan content: concrete or abstract *)
-type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
+type g_loan_content = (loan_content, aloan_content) concrete_or_abs
 [@@deriving show]
 
 (** Generic borrow content: concrete or abstract *)
-type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
+type g_borrow_content = (borrow_content, aborrow_content) concrete_or_abs
 [@@deriving show]
 
 type abs_or_var_id =
-  | AbsId of V.AbstractionId.id
-  | VarId of E.VarId.id
-  | DummyVarId of C.DummyVarId.id
+  | AbsId of AbstractionId.id
+  | VarId of VarId.id
+  | DummyVarId of DummyVarId.id
 
 (** Utility exception *)
-exception FoundBorrowContent of V.borrow_content
+exception FoundBorrowContent of borrow_content
 
 (** Utility exception *)
-exception FoundLoanContent of V.loan_content
+exception FoundLoanContent of loan_content
 
 (** Utility exception *)
-exception FoundABorrowContent of V.aborrow_content
+exception FoundABorrowContent of aborrow_content
 
 (** Utility exception *)
 exception FoundGBorrowContent of g_borrow_content
@@ -196,30 +193,30 @@ exception FoundGBorrowContent of g_borrow_content
 exception FoundGLoanContent of g_loan_content
 
 (** Utility exception *)
-exception FoundAProjBorrows of V.symbolic_value * T.ty
+exception FoundAProjBorrows of symbolic_value * ty
 
-let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
+let symbolic_value_id_in_ctx (sv_id : SymbolicValueId.id) (ctx : eval_ctx) :
     bool =
   let obj =
     object
-      inherit [_] C.iter_eval_ctx as super
+      inherit [_] iter_eval_ctx as super
 
       method! visit_VSymbolic _ sv =
-        if sv.V.sv_id = sv_id then raise Found else ()
+        if sv.sv_id = sv_id then raise Found else ()
 
       method! visit_aproj env aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            if sv.V.sv_id = sv_id then raise Found else ()
+            if sv.sv_id = sv_id then raise Found else ()
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj env aproj
 
       method! visit_abstract_shared_borrows _ asb =
-        let visit (asb : V.abstract_shared_borrow) : unit =
+        let visit (asb : abstract_shared_borrow) : unit =
           match asb with
-          | V.AsbBorrow _ -> ()
-          | V.AsbProjReborrows (sv, _) ->
-              if sv.V.sv_id = sv_id then raise Found else ()
+          | AsbBorrow _ -> ()
+          | AsbProjReborrows (sv, _) ->
+              if sv.sv_id = sv_id then raise Found else ()
         in
         List.iter visit asb
     end
@@ -236,21 +233,20 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
     check that the set of ended regions doesn't intersect the set of
     regions used in the type (this is more general).
 *)
-let symbolic_value_has_ended_regions (ended_regions : T.RegionId.Set.t)
-    (s : V.symbolic_value) : bool =
-  let regions = ty_regions s.V.sv_ty in
-  not (T.RegionId.Set.disjoint regions ended_regions)
+let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t)
+    (s : symbolic_value) : bool =
+  let regions = ty_regions s.sv_ty in
+  not (RegionId.Set.disjoint regions ended_regions)
 
-(** Check if a {!type:V.value} contains [⊥].
+(** Check if a {!type:value} contains [⊥].
 
     Note that this function is very general: it also checks wether
     symbolic values contain already ended regions.
  *)
-let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
-    bool =
+let bottom_in_value (ended_regions : RegionId.Set.t) (v : typed_value) : bool =
   let obj =
     object
-      inherit [_] V.iter_typed_value
+      inherit [_] iter_typed_value
       method! visit_VBottom _ = raise Found
 
       method! visit_symbolic_value _ s =
@@ -264,21 +260,21 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
     false
   with Found -> true
 
-let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
-    (v : V.typed_value) : bool =
+let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx)
+    (v : typed_value) : bool =
   let obj =
     object
-      inherit [_] V.iter_typed_value
+      inherit [_] iter_typed_value
 
       method! visit_symbolic_value _ s =
         match s.sv_kind with
-        | V.FunCallRet | V.LoopOutput | V.LoopJoin ->
+        | FunCallRet | LoopOutput | LoopJoin ->
             if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
               raise Found
             else ()
-        | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate
-        | V.ConstGeneric | V.TraitConst ->
+        | SynthInput | SynthInputGivenBack | FunCallGivenBack
+        | SynthRetGivenBack | Global | LoopGivenBack | Aggregate | ConstGeneric
+        | TraitConst ->
             ()
     end
   in
@@ -291,7 +287,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
 (** Return the place used in an rvalue, if that makes sense.
     This is used to compute meta-data, to find pretty names.
  *)
-let rvalue_get_place (rv : E.rvalue) : E.place option =
+let rvalue_get_place (rv : rvalue) : place option =
   match rv with
   | Use (Copy p | Move p) -> Some p
   | Use (Constant _) -> None
@@ -299,30 +295,29 @@ let rvalue_get_place (rv : E.rvalue) : E.place option =
   | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
-let symbolic_value_has_borrows (ctx : C.eval_ctx) (sv : V.symbolic_value) : bool
-    =
+let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool =
   ValuesUtils.symbolic_value_has_borrows ctx.type_context.type_infos sv
 
 (** See {!ValuesUtils.value_has_borrows}. *)
-let value_has_borrows (ctx : C.eval_ctx) (v : V.value) : bool =
+let value_has_borrows (ctx : eval_ctx) (v : value) : bool =
   ValuesUtils.value_has_borrows ctx.type_context.type_infos v
 
 (** See {!ValuesUtils.value_has_loans_or_borrows}. *)
-let value_has_loans_or_borrows (ctx : C.eval_ctx) (v : V.value) : bool =
+let value_has_loans_or_borrows (ctx : eval_ctx) (v : value) : bool =
   ValuesUtils.value_has_loans_or_borrows ctx.type_context.type_infos v
 
 (** See {!ValuesUtils.value_has_loans}. *)
-let value_has_loans (v : V.value) : bool = ValuesUtils.value_has_loans v
+let value_has_loans (v : value) : bool = ValuesUtils.value_has_loans v
 
 (** See {!compute_typed_value_ids}, {!compute_context_ids}, etc. *)
 type ids_sets = {
-  aids : V.AbstractionId.Set.t;
-  blids : V.BorrowId.Set.t;  (** All the borrow/loan ids *)
-  borrow_ids : V.BorrowId.Set.t;  (** Only the borrow ids *)
-  loan_ids : V.BorrowId.Set.t;  (** Only the loan ids *)
-  dids : C.DummyVarId.Set.t;
-  rids : T.RegionId.Set.t;
-  sids : V.SymbolicValueId.Set.t;
+  aids : AbstractionId.Set.t;
+  blids : BorrowId.Set.t;  (** All the borrow/loan ids *)
+  borrow_ids : BorrowId.Set.t;  (** Only the borrow ids *)
+  loan_ids : BorrowId.Set.t;  (** Only the loan ids *)
+  dids : DummyVarId.Set.t;
+  rids : RegionId.Set.t;
+  sids : SymbolicValueId.Set.t;
 }
 [@@deriving show]
 
@@ -330,19 +325,17 @@ type ids_sets = {
 
     TODO: there misses information.
  *)
-type ids_to_values = {
-  sids_to_values : V.symbolic_value V.SymbolicValueId.Map.t;
-}
+type ids_to_values = { sids_to_values : symbolic_value SymbolicValueId.Map.t }
 
 let compute_ids () =
-  let blids = ref V.BorrowId.Set.empty in
-  let borrow_ids = ref V.BorrowId.Set.empty in
-  let loan_ids = ref V.BorrowId.Set.empty in
-  let aids = ref V.AbstractionId.Set.empty in
-  let dids = ref C.DummyVarId.Set.empty in
-  let rids = ref T.RegionId.Set.empty in
-  let sids = ref V.SymbolicValueId.Set.empty in
-  let sids_to_values = ref V.SymbolicValueId.Map.empty in
+  let blids = ref BorrowId.Set.empty in
+  let borrow_ids = ref BorrowId.Set.empty in
+  let loan_ids = ref BorrowId.Set.empty in
+  let aids = ref AbstractionId.Set.empty in
+  let dids = ref DummyVarId.Set.empty in
+  let rids = ref RegionId.Set.empty in
+  let sids = ref SymbolicValueId.Set.empty in
+  let sids_to_values = ref SymbolicValueId.Map.empty in
 
   let get_ids () =
     {
@@ -358,156 +351,154 @@ let compute_ids () =
   let get_ids_to_values () = { sids_to_values = !sids_to_values } in
   let obj =
     object
-      inherit [_] C.iter_eval_ctx as super
-      method! visit_dummy_var_id _ did = dids := C.DummyVarId.Set.add did !dids
+      inherit [_] iter_eval_ctx as super
+      method! visit_dummy_var_id _ did = dids := DummyVarId.Set.add did !dids
 
       method! visit_borrow_id _ id =
-        blids := V.BorrowId.Set.add id !blids;
-        borrow_ids := V.BorrowId.Set.add id !borrow_ids
+        blids := BorrowId.Set.add id !blids;
+        borrow_ids := BorrowId.Set.add id !borrow_ids
 
       method! visit_loan_id _ id =
-        blids := V.BorrowId.Set.add id !blids;
-        loan_ids := V.BorrowId.Set.add id !loan_ids
+        blids := BorrowId.Set.add id !blids;
+        loan_ids := BorrowId.Set.add id !loan_ids
 
-      method! visit_abstraction_id _ id =
-        aids := V.AbstractionId.Set.add id !aids
-
-      method! visit_region_id _ id = rids := T.RegionId.Set.add id !rids
+      method! visit_abstraction_id _ id = aids := AbstractionId.Set.add id !aids
+      method! visit_region_id _ id = rids := RegionId.Set.add id !rids
 
       method! visit_symbolic_value env sv =
-        sids := V.SymbolicValueId.Set.add sv.sv_id !sids;
-        sids_to_values := V.SymbolicValueId.Map.add sv.sv_id sv !sids_to_values;
+        sids := SymbolicValueId.Set.add sv.sv_id !sids;
+        sids_to_values := SymbolicValueId.Map.add sv.sv_id sv !sids_to_values;
         super#visit_symbolic_value env sv
 
       method! visit_symbolic_value_id _ id =
         (* TODO: can we get there without going through [visit_symbolic_value] first? *)
-        sids := V.SymbolicValueId.Set.add id !sids
+        sids := SymbolicValueId.Set.add id !sids
     end
   in
   (obj, get_ids, get_ids_to_values)
 
 (** Compute the sets of ids found in a list of typed values. *)
-let compute_typed_values_ids (xl : V.typed_value list) :
-    ids_sets * ids_to_values =
+let compute_typed_values_ids (xl : typed_value list) : ids_sets * ids_to_values
+    =
   let compute, get_ids, get_ids_to_values = compute_ids () in
   List.iter (compute#visit_typed_value ()) xl;
   (get_ids (), get_ids_to_values ())
 
 (** Compute the sets of ids found in a typed value. *)
-let compute_typed_value_ids (x : V.typed_value) : ids_sets * ids_to_values =
+let compute_typed_value_ids (x : typed_value) : ids_sets * ids_to_values =
   compute_typed_values_ids [ x ]
 
 (** Compute the sets of ids found in a list of abstractions. *)
-let compute_absl_ids (xl : V.abs list) : ids_sets * ids_to_values =
+let compute_absl_ids (xl : abs list) : ids_sets * ids_to_values =
   let compute, get_ids, get_ids_to_values = compute_ids () in
   List.iter (compute#visit_abs ()) xl;
   (get_ids (), get_ids_to_values ())
 
 (** Compute the sets of ids found in an abstraction. *)
-let compute_abs_ids (x : V.abs) : ids_sets * ids_to_values =
+let compute_abs_ids (x : abs) : ids_sets * ids_to_values =
   compute_absl_ids [ x ]
 
 (** Compute the sets of ids found in an environment. *)
-let compute_env_ids (x : C.env) : ids_sets * ids_to_values =
+let compute_env_ids (x : env) : ids_sets * ids_to_values =
   let compute, get_ids, get_ids_to_values = compute_ids () in
   compute#visit_env () x;
   (get_ids (), get_ids_to_values ())
 
 (** Compute the sets of ids found in an environment element. *)
-let compute_env_elem_ids (x : C.env_elem) : ids_sets * ids_to_values =
+let compute_env_elem_ids (x : env_elem) : ids_sets * ids_to_values =
   compute_env_ids [ x ]
 
 (** Compute the sets of ids found in a list of contexts. *)
-let compute_contexts_ids (ctxl : C.eval_ctx list) : ids_sets * ids_to_values =
+let compute_contexts_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values =
   let compute, get_ids, get_ids_to_values = compute_ids () in
   List.iter (compute#visit_eval_ctx ()) ctxl;
   (get_ids (), get_ids_to_values ())
 
 (** Compute the sets of ids found in a context. *)
-let compute_context_ids (ctx : C.eval_ctx) : ids_sets * ids_to_values =
+let compute_context_ids (ctx : eval_ctx) : ids_sets * ids_to_values =
   compute_contexts_ids [ 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) : C.eval_ctx =
-  C.reset_global_counters ();
+let initialize_eval_context (ctx : decls_ctx)
+    (region_groups : RegionGroupId.id list) (type_vars : type_var list)
+    (const_generic_vars : const_generic_var list) : eval_ctx =
+  reset_global_counters ();
   let const_generic_vars_map =
-    T.ConstGenericVarId.Map.of_list
+    ConstGenericVarId.Map.of_list
       (List.map
-         (fun (cg : T.const_generic_var) ->
-           let ty = T.TLiteral cg.ty in
-           let cv = mk_fresh_symbolic_typed_value V.ConstGeneric ty in
+         (fun (cg : const_generic_var) ->
+           let ty = TLiteral cg.ty in
+           let cv = mk_fresh_symbolic_typed_value ConstGeneric ty in
            (cg.index, cv))
          const_generic_vars)
   in
   {
-    C.type_context = ctx.type_ctx;
-    C.fun_context = ctx.fun_ctx;
-    C.global_context = ctx.global_ctx;
-    C.trait_decls_context = ctx.trait_decls_ctx;
-    C.trait_impls_context = ctx.trait_impls_ctx;
-    C.region_groups;
-    C.type_vars;
-    C.const_generic_vars;
-    C.const_generic_vars_map;
-    C.norm_trait_types = C.TraitTypeRefMap.empty (* Empty for now *);
-    C.env = [ C.EFrame ];
-    C.ended_regions = T.RegionId.Set.empty;
+    type_context = ctx.type_ctx;
+    fun_context = ctx.fun_ctx;
+    global_context = ctx.global_ctx;
+    trait_decls_context = ctx.trait_decls_ctx;
+    trait_impls_context = ctx.trait_impls_ctx;
+    region_groups;
+    type_vars;
+    const_generic_vars;
+    const_generic_vars_map;
+    norm_trait_types = TraitTypeRefMap.empty (* Empty for now *);
+    env = [ EFrame ];
+    ended_regions = RegionId.Set.empty;
   }
 
 (** Instantiate a function signature, introducing **fresh** abstraction ids and
     region ids. This is mostly used in preparation of function calls (when
     evaluating in symbolic mode).
  *)
-let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
-    (tr_self : T.trait_instance_id) (sg : A.fun_sig)
-    (regions_hierarchy : T.region_groups) : A.inst_fun_sig =
+let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args)
+    (tr_self : trait_instance_id) (sg : fun_sig)
+    (regions_hierarchy : region_groups) : inst_fun_sig =
   log#ldebug
     (lazy
       ("instantiate_fun_sig:" ^ "\n- generics: "
-      ^ PA.generic_args_to_string ctx generics
+      ^ Print.EvalCtx.generic_args_to_string ctx generics
       ^ "\n- tr_self: "
-      ^ PA.trait_instance_id_to_string ctx tr_self
+      ^ Print.EvalCtx.trait_instance_id_to_string ctx tr_self
       ^ "\n- sg: " ^ fun_sig_to_string ctx sg));
   (* Erase the regions in the generics we use for the instantiation *)
-  let generics = Subst.generic_args_erase_regions generics in
-  let tr_self = Subst.trait_instance_id_erase_regions tr_self in
+  let generics = Substitute.generic_args_erase_regions generics in
+  let tr_self = Substitute.trait_instance_id_erase_regions tr_self in
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
     List.map
       (fun rg ->
-        let abs_id = C.fresh_abstraction_id () in
-        (rg.T.id, abs_id))
+        let abs_id = fresh_abstraction_id () in
+        (rg.id, abs_id))
       regions_hierarchy
   in
-  let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t =
+  let asubst_map : AbstractionId.id RegionGroupId.Map.t =
     List.fold_left
-      (fun mp (rg_id, abs_id) -> T.RegionGroupId.Map.add rg_id abs_id mp)
-      T.RegionGroupId.Map.empty rg_abs_ids_bindings
+      (fun mp (rg_id, abs_id) -> RegionGroupId.Map.add rg_id abs_id mp)
+      RegionGroupId.Map.empty rg_abs_ids_bindings
   in
-  let asubst (rg_id : T.RegionGroupId.id) : V.AbstractionId.id =
-    T.RegionGroupId.Map.find rg_id asubst_map
+  let asubst (rg_id : RegionGroupId.id) : AbstractionId.id =
+    RegionGroupId.Map.find rg_id asubst_map
   in
   (* Generate fresh regions and their substitutions *)
-  let _, rsubst, _ = Subst.fresh_regions_with_substs sg.generics.regions in
+  let _, rsubst, _ = Substitute.fresh_regions_with_substs sg.generics.regions in
   (* Generate the type substitution
      Note that for now we don't support instantiating the type parameters with
      types containing regions. *)
   assert (List.for_all TypesUtils.ty_no_regions generics.types);
   assert (TypesUtils.trait_instance_id_no_regions tr_self);
   let tsubst =
-    Subst.make_type_subst_from_vars sg.generics.types generics.types
+    Substitute.make_type_subst_from_vars sg.generics.types generics.types
   in
   let cgsubst =
-    Subst.make_const_generic_subst_from_vars sg.generics.const_generics
+    Substitute.make_const_generic_subst_from_vars sg.generics.const_generics
       generics.const_generics
   in
   let tr_subst =
-    Subst.make_trait_subst_from_clauses sg.generics.trait_clauses
+    Substitute.make_trait_subst_from_clauses sg.generics.trait_clauses
       generics.trait_refs
   in
   (* Substitute the signature *)
-- 
cgit v1.2.3


From 6f8f1213e056804eda4c521922cdf45f4e92a509 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 15:57:55 +0100
Subject: Fix the issues with the cross-references for OCaml doc

---
 compiler/InterpreterUtils.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index ecd8f53f..bba88e9f 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -111,7 +111,7 @@ let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value =
 (** Create a loans projector value from a symbolic value.
     
     Checks if the projector will actually project some regions. If not,
-    returns {!AIgnored} ([_]).
+    returns {!Values.AIgnored} ([_]).
     
     TODO: update to handle 'static
  *)
@@ -238,7 +238,7 @@ let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t)
   let regions = ty_regions s.sv_ty in
   not (RegionId.Set.disjoint regions ended_regions)
 
-(** Check if a {!type:value} contains [⊥].
+(** Check if a {!type:Values.value} contains [⊥].
 
     Note that this function is very general: it also checks wether
     symbolic values contain already ended regions.
-- 
cgit v1.2.3


From 60ce69b83cbd749781543bb16becb5357f0e1a0a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 5 Dec 2023 15:00:46 +0100
Subject: Update following changes in Charon

---
 compiler/InterpreterUtils.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index bba88e9f..612d6903 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -455,7 +455,7 @@ let initialize_eval_context (ctx : decls_ctx)
  *)
 let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args)
     (tr_self : trait_instance_id) (sg : fun_sig)
-    (regions_hierarchy : region_groups) : inst_fun_sig =
+    (regions_hierarchy : region_var_groups) : inst_fun_sig =
   log#ldebug
     (lazy
       ("instantiate_fun_sig:" ^ "\n- generics: "
@@ -484,7 +484,11 @@ let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args)
     RegionGroupId.Map.find rg_id asubst_map
   in
   (* Generate fresh regions and their substitutions *)
-  let _, rsubst, _ = Substitute.fresh_regions_with_substs sg.generics.regions in
+  let _, rsubst, _ =
+    Substitute.fresh_regions_with_substs_from_vars ~fail_if_not_found:true
+      sg.generics.regions
+  in
+  let rsubst r = Option.get (rsubst r) in
   (* Generate the type substitution
      Note that for now we don't support instantiating the type parameters with
      types containing regions. *)
-- 
cgit v1.2.3


From df3587d14b1137d0961f5607b3d8309eddbe69ce Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 5 Dec 2023 16:01:30 +0100
Subject: Fix a minor issue with the use of const generics

---
 compiler/InterpreterUtils.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 612d6903..d3f8f4fa 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -273,8 +273,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx)
               raise Found
             else ()
         | SynthInput | SynthInputGivenBack | FunCallGivenBack
-        | SynthRetGivenBack | Global | LoopGivenBack | Aggregate | ConstGeneric
-        | TraitConst ->
+        | SynthRetGivenBack | Global | KindConstGeneric | LoopGivenBack
+        | Aggregate | ConstGeneric | TraitConst ->
             ()
     end
   in
-- 
cgit v1.2.3