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/SymbolicToPure.ml | 49 ++++++++++++++++++++++++----------------------
 1 file changed, 26 insertions(+), 23 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3512270a..7dda1f22 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -201,29 +201,6 @@ type bs_ctx = {
 }
 [@@deriving show]
 
-let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
-  let env = VarId.Map.empty in
-  let ctx =
-    {
-      PureTypeCheck.type_decls = ctx.type_context.type_decls;
-      global_decls = ctx.global_context.llbc_global_decls;
-      env;
-    }
-  in
-  let _ = PureTypeCheck.check_typed_pattern ctx v in
-  ()
-
-let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
-  let env = VarId.Map.empty in
-  let ctx =
-    {
-      PureTypeCheck.type_decls = ctx.type_context.type_decls;
-      global_decls = ctx.global_context.llbc_global_decls;
-      env;
-    }
-  in
-  PureTypeCheck.check_texpression ctx e
-
 (* TODO: move *)
 let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
   Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
@@ -589,6 +566,31 @@ let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
   let type_infos = ctx.type_context.type_infos in
   translate_back_ty type_infos keep_region inside_mut ty
 
+let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
+  let const_generics =
+    T.ConstGenericVarId.Map.of_list
+      (List.map
+         (fun (cg : T.const_generic_var) ->
+           (cg.index, ctx_translate_fwd_ty ctx (T.Literal cg.ty)))
+         ctx.sg.const_generic_params)
+  in
+  let env = VarId.Map.empty in
+  {
+    PureTypeCheck.type_decls = ctx.type_context.type_decls;
+    global_decls = ctx.global_context.llbc_global_decls;
+    env;
+    const_generics;
+  }
+
+let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
+  let ctx = mk_type_check_ctx ctx in
+  let _ = PureTypeCheck.check_typed_pattern ctx v in
+  ()
+
+let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
+  let ctx = mk_type_check_ctx ctx in
+  PureTypeCheck.check_texpression ctx e
+
 (** List the ancestors of an abstraction *)
 let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs)
     (call_id : V.FunCallId.id) : V.AbstractionId.id list =
@@ -2298,6 +2300,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
           { struct_id = Assumed Array; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
+    | ConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
   in
 
   (* Make the let-binding *)
-- 
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/SymbolicToPure.ml | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7dda1f22..6c2c049b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -52,6 +52,9 @@ type fun_context = {
 type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
 [@@deriving show]
 
+type trait_decls_context = A.trait_decl A.TraitDeclId.Map.t [@@deriving show]
+type trait_impls_context = A.trait_impl A.TraitImplId.Map.t [@@deriving show]
+
 (** Whenever we translate a function call or an ended abstraction, we
     store the related information (this is useful when translating ended
     children abstractions).
@@ -120,6 +123,8 @@ type bs_ctx = {
   type_context : type_context;
   fun_context : fun_context;
   global_context : global_context;
+  trait_decls_ctx : trait_decls_context;
+  trait_impls_ctx : trait_impls_context;
   fun_decl : A.fun_decl;
   bid : T.RegionGroupId.id option;  (** TODO: rename *)
   sg : fun_sig;
@@ -205,7 +210,7 @@ type bs_ctx = {
 let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
   Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
     ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls
-    ctx.fun_decl
+    ctx.trait_decls_ctx ctx.trait_impls_ctx ctx.fun_decl
 
 let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
   let rvar_to_string = Print.Types.region_var_id_to_string in
@@ -223,16 +228,19 @@ let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
     adt_variant_to_string = ast_fmt.adt_variant_to_string;
     var_id_to_string;
     adt_field_names = ast_fmt.adt_field_names;
+    trait_decl_id_to_string = ast_fmt.trait_decl_id_to_string;
+    trait_impl_id_to_string = ast_fmt.trait_impl_id_to_string;
+    trait_clause_id_to_string = ast_fmt.trait_clause_id_to_string;
   }
 
 let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
-  let type_params = ctx.fun_decl.signature.type_params in
-  let cg_params = ctx.fun_decl.signature.const_generic_params in
+  let generics = ctx.fun_decl.signature.generics in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
-  PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
-    cg_params
+  PrintPure.mk_ast_formatter type_decls fun_decls global_decls
+    ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
+    generics.const_generics
 
 let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
@@ -254,12 +262,11 @@ let rty_to_string (ctx : bs_ctx) (ty : T.rty) : string =
   Print.PT.rty_to_string fmt ty
 
 let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
-  let type_params = def.type_params in
-  let cg_params = def.const_generic_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
   let fmt =
-    PrintPure.mk_type_formatter type_decls global_decls type_params cg_params
+    PrintPure.mk_type_formatter type_decls global_decls ctx.trait_decls_ctx
+      ctx.trait_impls_ctx def.generics.types def.generics.const_generics
   in
   PrintPure.type_decl_to_string fmt def
 
-- 
cgit v1.2.3


From 33bb0b7dbdf5cce28b58793e5fb280668a644525 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 31 Aug 2023 16:56:26 +0200
Subject: Finish updating SymbolicToPure.ml

---
 compiler/SymbolicToPure.ml | 306 +++++++++++++++++++++++++++++----------------
 1 file changed, 196 insertions(+), 110 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6c2c049b..c827475b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -109,8 +109,7 @@ type loop_info = {
   loop_id : LoopId.id;
   input_vars : var list;
   input_svl : V.symbolic_value list;
-  type_args : ty list;
-  const_generic_args : const_generic list;
+  generics : generic_args;
   forward_inputs : texpression list option;
       (** The forward inputs are initialized at [None] *)
   forward_output_no_state_no_result : var option;
@@ -275,26 +274,27 @@ let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
   PrintPure.texpression_to_string fmt false "" "  " e
 
 let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
-  let type_params = sg.type_params in
-  let cg_params = sg.const_generic_params in
+  let type_params = sg.generics.types in
+  let cg_params = sg.generics.const_generics in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
   let fmt =
-    PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
-      cg_params
+    PrintPure.mk_ast_formatter type_decls fun_decls global_decls
+      ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
   in
   PrintPure.fun_sig_to_string fmt sg
 
 let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
-  let type_params = def.signature.type_params in
-  let cg_params = def.signature.const_generic_params in
+  let generics = def.signature.generics in
+  let type_params = generics.types in
+  let cg_params = generics.const_generics in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
   let fmt =
-    PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
-      cg_params
+    PrintPure.mk_ast_formatter type_decls fun_decls global_decls
+      ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
   in
   PrintPure.fun_decl_to_string fmt def
 
@@ -312,17 +312,18 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
   Print.Values.abs_to_string fmt verbose indent indent_incr abs
 
 let get_instantiated_fun_sig (fun_id : A.fun_id)
-    (back_id : T.RegionGroupId.id option) (tys : ty list)
-    (cgs : const_generic list) (ctx : bs_ctx) : inst_fun_sig =
+    (back_id : T.RegionGroupId.id option) (generics : generic_args)
+    (ctx : bs_ctx) : inst_fun_sig =
   (* Lookup the non-instantiated function signature *)
   let sg =
     (RegularFunIdNotLoopMap.find (fun_id, back_id) ctx.fun_context.fun_sigs).sg
   in
   (* Create the substitution *)
-  let tsubst = make_type_subst sg.type_params tys in
-  let cgsubst = make_const_generic_subst sg.const_generic_params cgs in
+  (* There shouldn't be any reference to Self *)
+  let tr_self = UnknownTrait __FUNCTION__ in
+  let subst = make_subst_from_generics sg.generics generics tr_self in
   (* Apply *)
-  fun_sig_substitute tsubst cgsubst sg
+  fun_sig_substitute subst sg
 
 let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
     T.type_decl =
@@ -375,37 +376,99 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
   (* Update the context and return *)
   ({ ctx with calls; abstractions }, fun_id)
 
+(* Some generic translation functions (we need to translate different "flavours"
+   of types: sty, forward types, backward types, etc.) *)
+let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
+    (generics : 'r T.generic_args) : generic_args =
+  (* Can't translate types with regions for now *)
+  assert (generics.regions = []);
+  let types = List.map translate_ty generics.types in
+  let const_generics = generics.const_generics in
+  let trait_refs =
+    List.map (translate_trait_ref translate_ty) generics.trait_refs
+  in
+  { types; const_generics; trait_refs }
+
+and translate_trait_ref (translate_ty : 'r T.ty -> ty) (tr : 'r T.trait_ref) :
+    trait_ref =
+  let trait_id = translate_trait_instance_id translate_ty tr.trait_id in
+  let generics = translate_generic_args translate_ty tr.generics in
+  { trait_id; generics }
+
+and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
+    (id : 'r T.trait_instance_id) : trait_instance_id =
+  let translate_trait_instance_id = translate_trait_instance_id translate_ty in
+  match id with
+  | T.Self -> Self
+  | TraitImpl id -> TraitImpl id
+  | BuiltinOrAuto _ ->
+      (* We should have eliminated those in the prepasses *)
+      raise (Failure "Unreachable")
+  | Clause id -> Clause id
+  | ParentClause (inst_id, clause_id) ->
+      let inst_id = translate_trait_instance_id inst_id in
+      ParentClause (inst_id, clause_id)
+  | ItemClause (inst_id, item_name, clause_id) ->
+      let inst_id = translate_trait_instance_id inst_id in
+      ItemClause (inst_id, item_name, clause_id)
+  | TraitRef tr -> TraitRef (translate_trait_ref translate_ty tr)
+  | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s))
+
 let rec translate_sty (ty : T.sty) : ty =
   let translate = translate_sty in
   match ty with
-  | T.Adt (type_id, regions, tys, cgs) -> (
-      (* Can't translate types with regions for now *)
-      assert (regions = []);
-      let tys = List.map translate tys in
+  | T.Adt (type_id, generics) -> (
+      let generics = translate_sgeneric_args generics in
       match type_id with
-      | T.AdtId adt_id -> Adt (AdtId adt_id, tys, cgs)
-      | T.Tuple -> mk_simpl_tuple_ty tys
+      | T.AdtId adt_id -> Adt (AdtId adt_id, generics)
+      | T.Tuple ->
+          assert (generics.const_generics = []);
+          mk_simpl_tuple_ty generics.types
       | T.Assumed aty -> (
           match aty with
-          | T.Vec -> Adt (Assumed Vec, tys, cgs)
-          | T.Option -> Adt (Assumed Option, tys, cgs)
+          | T.Vec -> Adt (Assumed Vec, generics)
+          | T.Option -> Adt (Assumed Option, generics)
           | T.Box -> (
               (* Eliminate the boxes *)
-              match tys with
+              match generics.types with
               | [ ty ] -> ty
               | _ ->
                   raise
                     (Failure
                        "Box/vec/option type with incorrect number of arguments")
               )
-          | T.Array -> Adt (Assumed Array, tys, cgs)
-          | T.Slice -> Adt (Assumed Slice, tys, cgs)
-          | T.Str -> Adt (Assumed Str, tys, cgs)
-          | T.Range -> Adt (Assumed Range, tys, cgs)))
+          | T.Array -> Adt (Assumed Array, generics)
+          | T.Slice -> Adt (Assumed Slice, generics)
+          | T.Str -> Adt (Assumed Str, generics)
+          | T.Range -> Adt (Assumed Range, generics)))
   | TypeVar vid -> TypeVar vid
   | Literal ty -> Literal ty
   | Never -> raise (Failure "Unreachable")
   | Ref (_, rty, _) -> translate rty
+  | TraitType (trait_ref, generics, type_name) ->
+      let trait_ref = translate_strait_ref trait_ref in
+      let generics = translate_sgeneric_args generics in
+      TraitType (trait_ref, generics, type_name)
+
+and translate_sgeneric_args (generics : T.sgeneric_args) : generic_args =
+  translate_generic_args translate_sty generics
+
+and translate_strait_ref (tr : T.strait_ref) : trait_ref =
+  translate_trait_ref translate_sty tr
+
+and translate_strait_instance_id (id : T.strait_instance_id) : trait_instance_id
+    =
+  translate_trait_instance_id translate_sty id
+
+let translate_trait_clause (clause : T.trait_clause) : trait_clause =
+  let { T.clause_id; meta = _; trait_id; generics } = clause in
+  let generics = translate_sgeneric_args generics in
+  { clause_id; trait_id; generics }
+
+let translate_generic_params (generics : T.generic_params) : generic_params =
+  let { T.regions = _; types; const_generics; trait_clauses } = generics in
+  let trait_clauses = List.map translate_trait_clause trait_clauses in
+  { types; const_generics; trait_clauses }
 
 let translate_field (f : T.field) : field =
   let field_name = f.field_name in
@@ -436,15 +499,15 @@ let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
     point of moving this definition for now.
  *)
 let translate_type_decl (def : T.type_decl) : type_decl =
-  (* Translate *)
   let def_id = def.T.def_id in
   let name = def.name in
+  let { T.regions; types; const_generics; trait_clauses } = def.generics in
   (* Can't translate types with regions for now *)
-  assert (def.region_params = []);
-  let type_params = def.type_params in
-  let const_generic_params = def.const_generic_params in
+  assert (regions = []);
+  let trait_clauses = List.map translate_trait_clause trait_clauses in
+  let generics = { types; const_generics; trait_clauses } in
   let kind = translate_type_decl_kind def.T.kind in
-  { def_id; name; type_params; const_generic_params; kind }
+  { def_id; name; generics; kind }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -472,28 +535,33 @@ let translate_type_id (id : T.type_id) : type_id =
 let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
   let translate = translate_fwd_ty type_infos in
   match ty with
-  | T.Adt (type_id, regions, tys, cgs) -> (
-      (* Can't translate types with regions for now *)
-      assert (regions = []);
-      (* Translate the type parameters *)
-      let t_tys = List.map translate tys in
+  | T.Adt (type_id, generics) -> (
+      let t_generics = translate_fwd_generic_args type_infos generics in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
       | AdtId _
       | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
           (* No general parametricity for now *)
-          assert (not (List.exists (TypesUtils.ty_has_borrows type_infos) tys));
+          assert (
+            not
+              (List.exists
+                 (TypesUtils.ty_has_borrows type_infos)
+                 generics.types));
           let type_id = translate_type_id type_id in
-          Adt (type_id, t_tys, cgs)
+          Adt (type_id, t_generics)
       | Tuple ->
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
-          mk_simpl_tuple_ty t_tys
+          mk_simpl_tuple_ty t_generics.types
       | T.Assumed T.Box -> (
           (* We eliminate boxes *)
           (* No general parametricity for now *)
-          assert (not (List.exists (TypesUtils.ty_has_borrows type_infos) tys));
-          match t_tys with
+          assert (
+            not
+              (List.exists
+                 (TypesUtils.ty_has_borrows type_infos)
+                 generics.types));
+          match t_generics.types with
           | [ bty ] -> bty
           | _ ->
               raise
@@ -504,12 +572,34 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
   | Never -> raise (Failure "Unreachable")
   | Literal lty -> Literal lty
   | Ref (_, rty, _) -> translate rty
+  | TraitType (trait_ref, generics, type_name) ->
+      let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
+      let generics = translate_fwd_generic_args type_infos generics in
+      TraitType (trait_ref, generics, type_name)
+
+and translate_fwd_generic_args (type_infos : TA.type_infos)
+    (generics : 'r T.generic_args) : generic_args =
+  translate_generic_args (translate_fwd_ty type_infos) generics
+
+and translate_fwd_trait_ref (type_infos : TA.type_infos) (tr : 'r T.trait_ref) :
+    trait_ref =
+  translate_trait_ref (translate_fwd_ty type_infos) tr
+
+and translate_fwd_trait_instance_id (type_infos : TA.type_infos)
+    (id : 'r T.trait_instance_id) : trait_instance_id =
+  translate_trait_instance_id (translate_fwd_ty type_infos) id
 
 (** Simply calls [translate_fwd_ty] *)
 let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : 'r T.ty) : ty =
   let type_infos = ctx.type_context.type_infos in
   translate_fwd_ty type_infos ty
 
+(** Simply calls [translate_fwd_generic_args] *)
+let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : 'r T.generic_args)
+    : generic_args =
+  let type_infos = ctx.type_context.type_infos in
+  translate_fwd_generic_args type_infos generics
+
 (** Translate a type, when some regions may have ended.
     
     We return an option, because the translated type may be empty.
@@ -522,7 +612,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   (* A small helper for "leave" types *)
   let wrap ty = if inside_mut then Some ty else None in
   match ty with
-  | T.Adt (type_id, _, tys, cgs) -> (
+  | T.Adt (type_id, generics) -> (
       match type_id with
       | T.AdtId _
       | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
@@ -530,22 +620,24 @@ let rec translate_back_ty (type_infos : TA.type_infos)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           let type_id = translate_type_id type_id in
           if inside_mut then
-            let tys_t = List.filter_map translate tys in
-            Some (Adt (type_id, tys_t, cgs))
+            (* We do not want to filter anything, so we translate the generics
+               as "forward" types *)
+            let generics = translate_fwd_generic_args type_infos generics in
+            Some (Adt (type_id, generics))
           else None
       | Assumed T.Box -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           (* Eliminate the box *)
-          match tys with
+          match generics.types with
           | [ bty ] -> translate bty
           | _ ->
               raise
                 (Failure "Unreachable: boxes receive exactly one type parameter")
           )
       | T.Tuple -> (
-          (* Tuples can contain borrows (which we eliminated) *)
-          let tys_t = List.filter_map translate tys in
+          (* Tuples can contain borrows (which we eliminate) *)
+          let tys_t = List.filter_map translate generics.types in
           match tys_t with
           | [] -> None
           | _ ->
@@ -566,6 +658,13 @@ let rec translate_back_ty (type_infos : TA.type_infos)
           if keep_region r then
             translate_back_ty type_infos keep_region inside_mut rty
           else None)
+  | TraitType (trait_ref, generics, type_name) ->
+      assert (generics.regions = []);
+      (* Translate the trait ref and the generics as "forward" generics -
+         we do not want to filter any type *)
+      let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
+      let generics = translate_fwd_generic_args type_infos generics in
+      Some (TraitType (trait_ref, generics, type_name))
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
@@ -579,7 +678,7 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
       (List.map
          (fun (cg : T.const_generic_var) ->
            (cg.index, ctx_translate_fwd_ty ctx (T.Literal cg.ty)))
-         ctx.sg.const_generic_params)
+         ctx.sg.generics.const_generics)
   in
   let env = VarId.Map.empty in
   {
@@ -682,7 +781,8 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     Note that the function also takes a list of names for the inputs, and
     computes, for every output for the backward functions, a corresponding
     name (outputs for backward functions come from borrows in the inputs
-    of the forward function) which we use as hints to generate pretty names.
+    of the forward function) which we use as hints to generate pretty names
+    in the extracted code.
  *)
 let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id) (type_infos : TA.type_infos) (sg : A.fun_sig)
@@ -815,9 +915,8 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     (* Wrap in a result type *)
     if effect_info.can_fail then mk_result_ty output else output
   in
-  (* Type/const generic parameters *)
-  let type_params = sg.type_params in
-  let const_generic_params = sg.const_generic_params in
+  (* Generic parameters *)
+  let generics = translate_generic_params sg.generics in
   (* Return *)
   let has_fuel = fuel <> [] in
   let num_fwd_inputs_no_state = List.length fwd_inputs in
@@ -845,9 +944,7 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
       effect_info;
     }
   in
-  let sg =
-    { type_params; const_generic_params; inputs; output; doutputs; info }
-  in
+  let sg = { generics; inputs; output; doutputs; info } in
   { sg; output_names }
 
 let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
@@ -926,7 +1023,7 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
 (** Peel boxes as long as the value is of the form [Box<T>] *)
 let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
   match (v.value, v.ty) with
-  | V.Adt av, T.Adt (T.Assumed T.Box, _, _, _) -> (
+  | V.Adt av, T.Adt (T.Assumed T.Box, _) -> (
       match av.field_values with
       | [ bv ] -> unbox_typed_value bv
       | _ -> raise (Failure "Unreachable"))
@@ -971,16 +1068,16 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
         let field_values = List.map translate av.field_values in
         (* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
         match v.ty with
-        | T.Adt (T.Tuple, _, _, _) ->
+        | T.Adt (T.Tuple, _) ->
             assert (variant_id = None);
             mk_simpl_tuple_texpression field_values
         | _ ->
-            (* Retrieve the type, the translated type arguments and the
-             * const generic arguments from the translated type (simpler this way) *)
-            let adt_id, type_args, const_generic_args = ty_as_adt ty in
+            (* Retrieve the type and the translated generics from the translated
+               type (simpler this way) *)
+            let adt_id, generics = ty_as_adt ty in
             (* Create the constructor *)
             let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in
-            let qualif = { id = qualif_id; type_args; const_generic_args } in
+            let qualif = { id = qualif_id; generics } in
             let cons_e = Qualif qualif in
             let field_tys =
               List.map (fun (v : texpression) -> v.ty) field_values
@@ -1047,7 +1144,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* Translate the field values *)
         let field_values = List.filter_map translate adt_v.field_values in
         (* For now, only tuples can contain borrows *)
-        let adt_id, _, _, _ = TypesUtils.ty_as_adt av.ty in
+        let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
         | T.AdtId _
         | T.Assumed
@@ -1194,7 +1291,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
         (* For now, only tuples can contain borrows - note that if we gave
          * something like a [&mut Vec] to a function, we give back the
          * vector value upon visiting the "abstraction borrow" node *)
-        let adt_id, _, _, _ = TypesUtils.ty_as_adt av.ty in
+        let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
         | T.AdtId _
         | T.Assumed
@@ -1467,8 +1564,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
 and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     texpression =
   (* Translate the function call *)
-  let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
-  let const_generic_args = call.const_generic_params in
+  let generics = ctx_translate_fwd_generic_args ctx call.generics in
   let args =
     let args = List.map (typed_value_to_texpression ctx call.ctx) call.args in
     let args_mplaces = List.map translate_opt_mplace call.args_places in
@@ -1570,7 +1666,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     | None -> dest
     | Some out_state -> mk_simpl_tuple_pattern [ out_state; dest ]
   in
-  let func = { id = FunOrOp fun_id; type_args; const_generic_args } in
+  let func = { id = FunOrOp fun_id; generics } in
   let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
   let ret_ty =
     if effect_info.can_fail then mk_result_ty dest_v.ty else dest_v.ty
@@ -1701,8 +1797,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
   let effect_info =
     get_fun_effect_info ctx.fun_context.fun_infos fun_id None (Some rg_id)
   in
-  let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
-  let const_generic_args = call.const_generic_params in
+  let generics = ctx_translate_fwd_generic_args ctx call.generics in
   (* Retrieve the original call and the parent abstractions *)
   let _forward, backwards = get_abs_ancestors ctx abs call_id in
   (* Retrieve the values consumed when we called the forward function and
@@ -1751,10 +1846,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
   in
   (* Sanity check: there is the proper number of inputs and outputs, and they have the proper type *)
   let _ =
-    let inst_sg =
-      get_instantiated_fun_sig fun_id (Some rg_id) type_args const_generic_args
-        ctx
-    in
+    let inst_sg = get_instantiated_fun_sig fun_id (Some rg_id) generics ctx in
     log#ldebug
       (lazy
         ("\n- fun_id: " ^ A.show_fun_id fun_id ^ "\n- inputs ("
@@ -1797,7 +1889,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     if effect_info.can_fail then mk_result_ty output.ty else output.ty
   in
   let func_ty = mk_arrows input_tys ret_ty in
-  let func = { id = FunOrOp func; type_args; const_generic_args } in
+  let func = { id = FunOrOp func; generics } in
   let func = { e = Qualif func; ty = func_ty } in
   let call = mk_apps func args in
   (* **Optimization**:
@@ -1920,8 +2012,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
           (Some rg_id)
       in
       let loop_info = LoopId.Map.find loop_id ctx.loops in
-      let type_args = loop_info.type_args in
-      let const_generic_args = loop_info.const_generic_args in
+      let generics = loop_info.generics in
       let fwd_inputs = Option.get loop_info.forward_inputs in
       (* Retrieve the additional backward inputs. Note that those are actually
          the backward inputs of the function we are synthesizing (and that we
@@ -1970,7 +2061,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       in
       let func_ty = mk_arrows input_tys ret_ty in
       let func = Fun (FromLlbc (fun_id, Some loop_id, Some rg_id)) in
-      let func = { id = FunOrOp func; type_args; const_generic_args } in
+      let func = { id = FunOrOp func; generics } in
       let func = { e = Qualif func; ty = func_ty } in
       let call = mk_apps func args in
       (* **Optimization**:
@@ -2030,9 +2121,7 @@ and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
     (e : S.expression) (ctx : bs_ctx) : texpression =
   let ctx, var = fresh_var_for_symbolic_value sval ctx in
   let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in
-  let global_expr =
-    { id = Global gid; type_args = []; const_generic_args = [] }
-  in
+  let global_expr = { id = Global gid; generics = empty_generic_args } in
   (* We use translate_fwd_ty to translate the global type *)
   let ty = ctx_translate_fwd_ty ctx decl.ty in
   let gval = { e = Qualif global_expr; ty } in
@@ -2046,11 +2135,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
   let v = typed_value_to_texpression ctx ectx v in
   let args = [ v ] in
   let func =
-    {
-      id = FunOrOp (Fun (Pure Assert));
-      type_args = [];
-      const_generic_args = [];
-    }
+    { id = FunOrOp (Fun (Pure Assert)); generics = empty_generic_args }
   in
   let func_ty = mk_arrow (Literal Bool) mk_unit_ty in
   let func = { e = Qualif func; ty = func_ty } in
@@ -2198,7 +2283,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
     (branch : S.expression) (ctx : bs_ctx) : texpression =
   (* TODO: always introduce a match, and use micro-passes to turn the
      the match into a let? *)
-  let type_id, _, _, _ = TypesUtils.ty_as_adt sv.V.sv_ty in
+  let type_id, _ = TypesUtils.ty_as_adt sv.V.sv_ty in
   let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
   let branch = translate_expression branch ctx in
   match type_id with
@@ -2233,10 +2318,10 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
          * field.
          * We use the [dest] variable in order not to have to recompute
          * the type of the result of the projection... *)
-        let adt_id, type_args, const_generic_args = ty_as_adt scrutinee.ty in
+        let adt_id, generics = ty_as_adt scrutinee.ty in
         let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression =
           let proj_kind = { adt_id; field_id } in
-          let qualif = { id = Proj proj_kind; type_args; const_generic_args } in
+          let qualif = { id = Proj proj_kind; generics } in
           let proj_e = Qualif qualif in
           let proj_ty = mk_arrow scrutinee.ty dest.ty in
           let proj = { e = proj_e; ty = proj_ty } in
@@ -2426,13 +2511,7 @@ and translate_forward_end (ectx : C.eval_ctx)
 
       let loop_call =
         let fun_id = Fun (FromLlbc (fid, Some loop_id, None)) in
-        let func =
-          {
-            id = FunOrOp fun_id;
-            type_args = loop_info.type_args;
-            const_generic_args = loop_info.const_generic_args;
-          }
-        in
+        let func = { id = FunOrOp fun_id; generics = loop_info.generics } in
         let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
         let ret_ty =
           if effect_info.can_fail then mk_result_ty out_pat.ty else out_pat.ty
@@ -2551,14 +2630,24 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
 
     (* Note that we will retrieve the input values later in the [ForwardEnd]
        (and will introduce the outputs at that moment, together with the actual
-       call to the loop forward function *)
-    let type_args =
-      List.map (fun (ty : T.type_var) -> TypeVar ty.T.index) ctx.sg.type_params
-    in
-    let const_generic_args =
-      List.map
-        (fun (cg : T.const_generic_var) -> T.ConstGenericVar cg.T.index)
-        ctx.sg.const_generic_params
+       call to the loop forward function) *)
+    let generics =
+      let { types; const_generics; trait_clauses } = ctx.sg.generics in
+      let types =
+        List.map (fun (ty : T.type_var) -> TypeVar ty.T.index) types
+      in
+      let const_generics =
+        List.map
+          (fun (cg : T.const_generic_var) -> T.ConstGenericVar cg.T.index)
+          const_generics
+      in
+      let trait_refs =
+        List.map
+          (fun (c : trait_clause) ->
+            { trait_id = Clause c.clause_id; generics = empty_generic_args })
+          trait_clauses
+      in
+      { types; const_generics; trait_refs }
     in
 
     let loop_info =
@@ -2566,8 +2655,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         loop_id;
         input_vars = inputs;
         input_svl = loop.input_svalues;
-        type_args;
-        const_generic_args;
+        generics;
         forward_inputs = None;
         forward_output_no_state_no_result = None;
       }
@@ -2658,8 +2746,7 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression)
         let func =
           {
             id = FunOrOp (Fun (Pure FuelEqZero));
-            type_args = [];
-            const_generic_args = [];
+            generics = empty_generic_args;
           }
         in
         let func_ty = mk_arrow mk_fuel_ty mk_bool_ty in
@@ -2671,8 +2758,7 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression)
         let func =
           {
             id = FunOrOp (Fun (Pure FuelDecrease));
-            type_args = [];
-            const_generic_args = [];
+            generics = empty_generic_args;
           }
         in
         let func_ty = mk_arrow mk_fuel_ty mk_fuel_ty in
-- 
cgit v1.2.3


From 0cafb31dd42c95f22e0b6680531c27fa0508e376 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 13:32:43 +0200
Subject: Make progress on the extraction

---
 compiler/SymbolicToPure.ml | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index c827475b..166f08a0 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -393,7 +393,15 @@ and translate_trait_ref (translate_ty : 'r T.ty -> ty) (tr : 'r T.trait_ref) :
     trait_ref =
   let trait_id = translate_trait_instance_id translate_ty tr.trait_id in
   let generics = translate_generic_args translate_ty tr.generics in
-  { trait_id; generics }
+  let trait_decl_ref =
+    translate_trait_decl_ref translate_ty tr.trait_decl_ref
+  in
+  { trait_id; generics; trait_decl_ref }
+
+and translate_trait_decl_ref (translate_ty : 'r T.ty -> ty)
+    (tr : 'r T.trait_decl_ref) : trait_decl_ref =
+  let decl_generics = translate_generic_args translate_ty tr.decl_generics in
+  { trait_decl_id = tr.trait_decl_id; decl_generics }
 
 and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
     (id : 'r T.trait_instance_id) : trait_instance_id =
@@ -405,12 +413,12 @@ and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
       (* We should have eliminated those in the prepasses *)
       raise (Failure "Unreachable")
   | Clause id -> Clause id
-  | ParentClause (inst_id, clause_id) ->
+  | ParentClause (inst_id, decl_id, clause_id) ->
       let inst_id = translate_trait_instance_id inst_id in
-      ParentClause (inst_id, clause_id)
-  | ItemClause (inst_id, item_name, clause_id) ->
+      ParentClause (inst_id, decl_id, clause_id)
+  | ItemClause (inst_id, decl_id, item_name, clause_id) ->
       let inst_id = translate_trait_instance_id inst_id in
-      ItemClause (inst_id, item_name, clause_id)
+      ItemClause (inst_id, decl_id, item_name, clause_id)
   | TraitRef tr -> TraitRef (translate_trait_ref translate_ty tr)
   | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s))
 
@@ -2644,7 +2652,14 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       let trait_refs =
         List.map
           (fun (c : trait_clause) ->
-            { trait_id = Clause c.clause_id; generics = empty_generic_args })
+            let trait_decl_ref =
+              { trait_decl_id = c.trait_id; decl_generics = empty_generic_args }
+            in
+            {
+              trait_id = Clause c.clause_id;
+              generics = empty_generic_args;
+              trait_decl_ref;
+            })
           trait_clauses
       in
       { types; const_generics; trait_refs }
-- 
cgit v1.2.3


From b42c0a8fa4708d6bf8424d63b6a7fe4964ba0e3d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 15:18:36 +0200
Subject: Make progress on the extraction

---
 compiler/SymbolicToPure.ml | 110 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 108 insertions(+), 2 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 166f08a0..1a981de1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -4,6 +4,7 @@ open Pure
 open PureUtils
 module Id = Identifiers
 module C = Contexts
+module A = LlbcAst
 module S = SymbolicAst
 module TA = TypesAnalysis
 module L = Logging
@@ -473,6 +474,20 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause =
   let generics = translate_sgeneric_args generics in
   { clause_id; trait_id; generics }
 
+let translate_strait_type_constraint (ttc : T.strait_type_constraint) :
+    trait_type_constraint =
+  let { T.trait_ref; generics; type_name; ty } = ttc in
+  let trait_ref = translate_strait_ref trait_ref in
+  let generics = translate_sgeneric_args generics in
+  let ty = translate_sty ty in
+  { trait_ref; generics; type_name; ty }
+
+let translate_predicates (preds : T.predicates) : predicates =
+  let trait_type_constraints =
+    List.map translate_strait_type_constraint preds.trait_type_constraints
+  in
+  { trait_type_constraints }
+
 let translate_generic_params (generics : T.generic_params) : generic_params =
   let { T.regions = _; types; const_generics; trait_clauses } = generics in
   let trait_clauses = List.map translate_trait_clause trait_clauses in
@@ -515,7 +530,8 @@ let translate_type_decl (def : T.type_decl) : type_decl =
   let trait_clauses = List.map translate_trait_clause trait_clauses in
   let generics = { types; const_generics; trait_clauses } in
   let kind = translate_type_decl_kind def.T.kind in
-  { def_id; name; generics; kind }
+  let preds = translate_predicates def.preds in
+  { def_id; name; generics; kind; preds }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -952,7 +968,8 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
       effect_info;
     }
   in
-  let sg = { generics; inputs; output; doutputs; info } in
+  let preds = translate_predicates sg.A.preds in
+  let sg = { generics; preds; inputs; output; doutputs; info } in
   { sg; output_names }
 
 let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
@@ -2932,6 +2949,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let def =
     {
       def_id;
+      kind = def.kind;
       num_loops;
       loop_id;
       back_id = bid;
@@ -3002,3 +3020,91 @@ let translate_fun_signatures (fun_infos : FA.fun_info A.FunDeclId.Map.t)
   List.fold_left
     (fun m (id, sg) -> RegularFunIdNotLoopMap.add id sg m)
     RegularFunIdNotLoopMap.empty translated
+
+let translate_trait_decl (type_infos : TA.type_infos)
+    (trait_decl : A.trait_decl) : trait_decl =
+  let {
+    A.def_id;
+    name;
+    generics;
+    preds;
+    all_trait_clauses;
+    consts;
+    types;
+    required_methods;
+    provided_methods;
+  } =
+    trait_decl
+  in
+  let generics = translate_generic_params generics in
+  let preds = translate_predicates preds in
+  let all_trait_clauses = List.map translate_trait_clause all_trait_clauses in
+  let consts =
+    List.map
+      (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
+      consts
+  in
+  let types =
+    List.map
+      (fun (name, (trait_clauses, ty)) ->
+        ( name,
+          ( List.map translate_trait_clause trait_clauses,
+            Option.map (translate_fwd_ty type_infos) ty ) ))
+      types
+  in
+  {
+    def_id;
+    name;
+    generics;
+    preds;
+    all_trait_clauses;
+    consts;
+    types;
+    required_methods;
+    provided_methods;
+  }
+
+let translate_trait_impl (type_infos : TA.type_infos)
+    (trait_impl : A.trait_impl) : trait_impl =
+  let {
+    A.def_id;
+    name;
+    impl_trait;
+    generics;
+    preds;
+    consts;
+    types;
+    required_methods;
+    provided_methods;
+  } =
+    trait_impl
+  in
+  let impl_trait =
+    translate_trait_decl_ref (translate_fwd_ty type_infos) impl_trait
+  in
+  let generics = translate_generic_params generics in
+  let preds = translate_predicates preds in
+  let consts =
+    List.map
+      (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
+      consts
+  in
+  let types =
+    List.map
+      (fun (name, (trait_refs, ty)) ->
+        ( name,
+          ( List.map (translate_fwd_trait_ref type_infos) trait_refs,
+            translate_fwd_ty type_infos ty ) ))
+      types
+  in
+  {
+    def_id;
+    name;
+    impl_trait;
+    generics;
+    preds;
+    consts;
+    types;
+    required_methods;
+    provided_methods;
+  }
-- 
cgit v1.2.3


From 3151e373d64f9bce6146a44cd2d3cc64cac84cbf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 4 Sep 2023 00:59:39 +0200
Subject: Fix minor issues

---
 compiler/SymbolicToPure.ml | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 1a981de1..46eef953 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -242,6 +242,12 @@ let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
     ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
     generics.const_generics
 
+let ctx_egeneric_args_to_string (ctx : bs_ctx) (args : T.egeneric_args) : string
+    =
+  let fmt = bs_ctx_to_ctx_formatter ctx in
+  let fmt = Print.PC.ctx_to_etype_formatter fmt in
+  Print.PT.egeneric_args_to_string fmt args
+
 let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
   let fmt = Print.PC.ctx_to_rtype_formatter fmt in
@@ -381,8 +387,8 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
    of types: sty, forward types, backward types, etc.) *)
 let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
     (generics : 'r T.generic_args) : generic_args =
-  (* Can't translate types with regions for now *)
-  assert (generics.regions = []);
+  (* We ignore the regions: if they didn't cause trouble for the symbolic execution,
+     then everything's fine *)
   let types = List.map translate_ty generics.types in
   let const_generics = generics.const_generics in
   let trait_refs =
@@ -1588,6 +1594,10 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
 
 and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     texpression =
+  log#ldebug
+    (lazy
+      ("translate_function_call:\n"
+      ^ ctx_egeneric_args_to_string ctx call.generics));
   (* Translate the function call *)
   let generics = ctx_translate_fwd_generic_args ctx call.generics in
   let args =
-- 
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/SymbolicToPure.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 46eef953..3312e22d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2411,8 +2411,9 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
 
-  (* Translate the value: there are two cases, depending on whether this
-     is a "regular" let-binding or an array aggregate.
+  (* Translate the value: there are several cases, depending on whether this
+     is a "regular" let-binding, an array aggregate, a const generic or
+     a trait associated constant.
   *)
   let v =
     match v with
@@ -2428,6 +2429,13 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
         in
         { e = StructUpdate su; ty = var.ty }
     | ConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | TraitConstValue (trait_ref, generics, const_name) ->
+        let type_infos = ctx.type_context.type_infos in
+        let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
+        let generics = translate_fwd_generic_args type_infos generics in
+        let qualif_id = TraitConst (trait_ref, generics, const_name) in
+        let qualif = { id = qualif_id; generics = empty_generic_args } in
+        { e = Qualif qualif; ty = var.ty }
   in
 
   (* Make the let-binding *)
-- 
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/SymbolicToPure.ml | 73 ++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 61 insertions(+), 12 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3312e22d..1da0521d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -727,6 +727,54 @@ let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
   let ctx = mk_type_check_ctx ctx in
   PureTypeCheck.check_texpression ctx e
 
+let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
+    (id : A.fun_id_or_trait_method_ref) : fun_id_or_trait_method_ref =
+  match id with
+  | A.FunId fun_id -> FunId fun_id
+  | TraitMethod (trait_ref, method_name, fun_decl_id) ->
+      let type_infos = ctx.type_context.type_infos in
+      let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
+      TraitMethod (trait_ref, method_name, fun_decl_id)
+
+let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
+    (args : texpression list) (ctx : bs_ctx) : bs_ctx =
+  let calls = ctx.calls in
+  assert (not (V.FunCallId.Map.mem call_id calls));
+  let info =
+    { forward; forward_inputs = args; backwards = T.RegionGroupId.Map.empty }
+  in
+  let calls = V.FunCallId.Map.add call_id info calls in
+  { ctx with calls }
+
+(** [back_args]: the *additional* list of inputs received by the backward function *)
+let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
+    (back_id : T.RegionGroupId.id) (back_args : texpression list) (ctx : bs_ctx)
+    : bs_ctx * fun_or_op_id =
+  (* Insert the abstraction in the call informations *)
+  let info = V.FunCallId.Map.find call_id ctx.calls in
+  assert (not (T.RegionGroupId.Map.mem back_id info.backwards));
+  let backwards =
+    T.RegionGroupId.Map.add back_id (abs, back_args) info.backwards
+  in
+  let info = { info with backwards } in
+  let calls = V.FunCallId.Map.add call_id info ctx.calls in
+  (* Insert the abstraction in the abstractions map *)
+  let abstractions = ctx.abstractions in
+  assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions));
+  let abstractions =
+    V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions
+  in
+  (* Retrieve the fun_id *)
+  let fun_id =
+    match info.forward.call_id with
+    | S.Fun (fid, _) ->
+        let fid = translate_fun_id_or_trait_method_ref ctx fid in
+        Fun (FromLlbc (fid, None, Some back_id))
+    | S.Unop _ | S.Binop _ -> raise (Failure "Unreachable")
+  in
+  (* Update the context and return *)
+  ({ ctx with calls; abstractions }, fun_id)
+
 (** List the ancestors of an abstraction *)
 let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs)
     (call_id : V.FunCallId.id) : V.AbstractionId.id list =
@@ -780,10 +828,10 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) :
 
 (** Small utility. *)
 let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
-    (fun_id : A.fun_id) (lid : V.LoopId.id option)
+    (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with
-  | A.Regular fid ->
+  | A.TraitMethod (_, _, fid) | A.FunId (A.Regular fid) ->
       let info = A.FunDeclId.Map.find fid fun_infos in
       let stateful_group = info.stateful in
       let stateful =
@@ -796,7 +844,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
         can_diverge = info.can_diverge;
         is_rec = info.is_rec || Option.is_some lid;
       }
-  | A.Assumed aid ->
+  | A.FunId (A.Assumed aid) ->
       assert (lid = None);
       {
         can_fail = Assumed.assumed_can_fail aid;
@@ -828,7 +876,7 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
   in
   (* Is the function stateful, and can it fail? *)
   let lid = None in
-  let effect_info = get_fun_effect_info fun_infos fun_id lid bid in
+  let effect_info = get_fun_effect_info fun_infos (A.FunId fun_id) lid bid in
   (* List the inputs for:
    * - the fuel
    * - the forward function
@@ -1615,7 +1663,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     match call.call_id with
     | S.Fun (fid, call_id) ->
         (* Regular function call *)
-        let func = Fun (FromLlbc (fid, None, None)) in
+        let fid_t = translate_fun_id_or_trait_method_ref ctx fid in
+        let func = Fun (FromLlbc (fid_t, None, None)) in
         (* Retrieve the effect information about this function (can fail,
          * takes a state as input, etc.) *)
         let effect_info =
@@ -2043,8 +2092,8 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
   | V.LoopCall ->
       let fun_id = A.Regular ctx.fun_decl.A.def_id in
       let effect_info =
-        get_fun_effect_info ctx.fun_context.fun_infos fun_id (Some vloop_id)
-          (Some rg_id)
+        get_fun_effect_info ctx.fun_context.fun_infos (A.FunId fun_id)
+          (Some vloop_id) (Some rg_id)
       in
       let loop_info = LoopId.Map.find loop_id ctx.loops in
       let generics = loop_info.generics in
@@ -2095,7 +2144,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
         if effect_info.can_fail then mk_result_ty output.ty else output.ty
       in
       let func_ty = mk_arrows input_tys ret_ty in
-      let func = Fun (FromLlbc (fun_id, Some loop_id, Some rg_id)) in
+      let func = Fun (FromLlbc (FunId fun_id, Some loop_id, Some rg_id)) in
       let func = { id = FunOrOp func; generics } in
       let func = { e = Qualif func; ty = func_ty } in
       let call = mk_apps func args in
@@ -2508,7 +2557,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       (* Lookup the effect info for the loop function *)
       let fid = A.Regular ctx.fun_decl.A.def_id in
       let effect_info =
-        get_fun_effect_info ctx.fun_context.fun_infos fid None ctx.bid
+        get_fun_effect_info ctx.fun_context.fun_infos (A.FunId fid) None ctx.bid
       in
 
       (* Introduce a fresh output value for the forward function *)
@@ -2553,7 +2602,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       let out_pat = mk_simpl_tuple_pattern out_pats in
 
       let loop_call =
-        let fun_id = Fun (FromLlbc (fid, Some loop_id, None)) in
+        let fun_id = Fun (FromLlbc (FunId fid, Some loop_id, None)) in
         let func = { id = FunOrOp fun_id; generics = loop_info.generics } in
         let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
         let ret_ty =
@@ -2873,8 +2922,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     | None -> None
     | Some body ->
         let effect_info =
-          get_fun_effect_info ctx.fun_context.fun_infos (Regular def_id) None
-            bid
+          get_fun_effect_info ctx.fun_context.fun_infos (FunId (Regular def_id))
+            None bid
         in
         let body = translate_expression body ctx in
         (* Add a match over the fuel, if necessary *)
-- 
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/SymbolicToPure.ml | 37 -------------------------------------
 1 file changed, 37 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 1da0521d..4c5b99c3 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -346,43 +346,6 @@ let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
   let id = (A.Regular def_id, back_id) in
   (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg
 
-let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
-    (args : texpression list) (ctx : bs_ctx) : bs_ctx =
-  let calls = ctx.calls in
-  assert (not (V.FunCallId.Map.mem call_id calls));
-  let info =
-    { forward; forward_inputs = args; backwards = T.RegionGroupId.Map.empty }
-  in
-  let calls = V.FunCallId.Map.add call_id info calls in
-  { ctx with calls }
-
-(** [back_args]: the *additional* list of inputs received by the backward function *)
-let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
-    (back_id : T.RegionGroupId.id) (back_args : texpression list) (ctx : bs_ctx)
-    : bs_ctx * fun_or_op_id =
-  (* Insert the abstraction in the call informations *)
-  let info = V.FunCallId.Map.find call_id ctx.calls in
-  assert (not (T.RegionGroupId.Map.mem back_id info.backwards));
-  let backwards =
-    T.RegionGroupId.Map.add back_id (abs, back_args) info.backwards
-  in
-  let info = { info with backwards } in
-  let calls = V.FunCallId.Map.add call_id info ctx.calls in
-  (* Insert the abstraction in the abstractions map *)
-  let abstractions = ctx.abstractions in
-  assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions));
-  let abstractions =
-    V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions
-  in
-  (* Retrieve the fun_id *)
-  let fun_id =
-    match info.forward.call_id with
-    | S.Fun (fid, _) -> Fun (FromLlbc (fid, None, Some back_id))
-    | S.Unop _ | S.Binop _ -> raise (Failure "Unreachable")
-  in
-  (* Update the context and return *)
-  ({ ctx with calls; abstractions }, fun_id)
-
 (* Some generic translation functions (we need to translate different "flavours"
    of types: sty, forward types, backward types, etc.) *)
 let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
-- 
cgit v1.2.3


From d556b2439ad858fbbf612f433d25363a8f4a7c83 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Sep 2023 18:43:23 +0200
Subject: Fix more issues

---
 compiler/SymbolicToPure.ml | 77 ++++++++++++++++++++++++++--------------------
 1 file changed, 43 insertions(+), 34 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4c5b99c3..2e0e9862 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -687,8 +687,9 @@ let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
   ()
 
 let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
-  let ctx = mk_type_check_ctx ctx in
-  PureTypeCheck.check_texpression ctx e
+  if !Config.type_check_pure_code then
+    let ctx = mk_type_check_ctx ctx in
+    PureTypeCheck.check_texpression ctx e
 
 let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
     (id : A.fun_id_or_trait_method_ref) : fun_id_or_trait_method_ref =
@@ -1817,9 +1818,11 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
   (* Group the two lists *)
   let variables_values = List.combine given_back_variables consumed_values in
   (* Sanity check: the two lists match (same types) *)
-  List.iter
-    (fun (var, v) -> assert ((var : var).ty = (v : texpression).ty))
-    variables_values;
+  (* TODO: normalize the types *)
+  if !Config.type_check_pure_code then
+    List.iter
+      (fun (var, v) -> assert ((var : var).ty = (v : texpression).ty))
+      variables_values;
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
   (* Generate the assignemnts *)
@@ -1892,31 +1895,35 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     | Some nstate -> mk_simpl_tuple_pattern [ nstate; output ]
   in
   (* Sanity check: there is the proper number of inputs and outputs, and they have the proper type *)
-  let _ =
-    let inst_sg = get_instantiated_fun_sig fun_id (Some rg_id) generics ctx in
-    log#ldebug
-      (lazy
-        ("\n- fun_id: " ^ A.show_fun_id fun_id ^ "\n- inputs ("
-        ^ string_of_int (List.length inputs)
-        ^ "): "
-        ^ String.concat ", " (List.map (texpression_to_string ctx) inputs)
-        ^ "\n- inst_sg.inputs ("
-        ^ string_of_int (List.length inst_sg.inputs)
-        ^ "): "
-        ^ String.concat ", " (List.map (ty_to_string ctx) inst_sg.inputs)));
-    List.iter
-      (fun (x, ty) -> assert ((x : texpression).ty = ty))
-      (List.combine inputs inst_sg.inputs);
-    log#ldebug
-      (lazy
-        ("\n- outputs: "
-        ^ string_of_int (List.length outputs)
-        ^ "\n- expected outputs: "
-        ^ string_of_int (List.length inst_sg.doutputs)));
-    List.iter
-      (fun (x, ty) -> assert ((x : typed_pattern).ty = ty))
-      (List.combine outputs inst_sg.doutputs)
-  in
+  (if (* TODO: normalize the types *) !Config.type_check_pure_code then
+     match fun_id with
+     | A.FunId fun_id ->
+         let inst_sg =
+           get_instantiated_fun_sig fun_id (Some rg_id) generics ctx
+         in
+         log#ldebug
+           (lazy
+             ("\n- fun_id: " ^ A.show_fun_id fun_id ^ "\n- inputs ("
+             ^ string_of_int (List.length inputs)
+             ^ "): "
+             ^ String.concat ", " (List.map (texpression_to_string ctx) inputs)
+             ^ "\n- inst_sg.inputs ("
+             ^ string_of_int (List.length inst_sg.inputs)
+             ^ "): "
+             ^ String.concat ", " (List.map (ty_to_string ctx) inst_sg.inputs)));
+         List.iter
+           (fun (x, ty) -> assert ((x : texpression).ty = ty))
+           (List.combine inputs inst_sg.inputs);
+         log#ldebug
+           (lazy
+             ("\n- outputs: "
+             ^ string_of_int (List.length outputs)
+             ^ "\n- expected outputs: "
+             ^ string_of_int (List.length inst_sg.doutputs)));
+         List.iter
+           (fun (x, ty) -> assert ((x : typed_pattern).ty = ty))
+           (List.combine outputs inst_sg.doutputs)
+     | _ -> (* TODO: trait methods *) ());
   (* Retrieve the function id, and register the function call in the context
    * if necessary *)
   let ctx, func =
@@ -2961,10 +2968,12 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
             ^ "\n- signature.inputs: "
             ^ String.concat ", " (List.map (ty_to_string ctx) signature.inputs)
             ));
-        assert (
-          List.for_all
-            (fun (var, ty) -> (var : var).ty = ty)
-            (List.combine inputs signature.inputs));
+        (* TODO: we need to normalize the types *)
+        if !Config.type_check_pure_code then
+          assert (
+            List.for_all
+              (fun (var, ty) -> (var : var).ty = ty)
+              (List.combine inputs signature.inputs));
         Some { inputs; inputs_lvs; body }
   in
 
-- 
cgit v1.2.3


From 80728093c432ba15eace9d6ce1cc9e3c56a80ff7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 17 Sep 2023 05:37:56 +0200
Subject: Make minor modifications

---
 compiler/SymbolicToPure.ml | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2e0e9862..be9b7261 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -826,10 +826,11 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     of the forward function) which we use as hints to generate pretty names
     in the extracted code.
  *)
-let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
-    (fun_id : A.fun_id) (type_infos : TA.type_infos) (sg : A.fun_sig)
-    (input_names : string option list) (bid : T.RegionGroupId.id option) :
-    fun_sig_named_outputs =
+let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
+    (sg : A.fun_sig) (input_names : string option list)
+    (bid : T.RegionGroupId.id option) : fun_sig_named_outputs =
+  let fun_infos = decls_ctx.fun_ctx.fun_infos in
+  let type_infos = decls_ctx.type_ctx.type_infos in
   (* Retrieve the list of parent backward functions *)
   let gid, parents =
     match bid with
@@ -3021,8 +3022,7 @@ let translate_type_decls (type_decls : T.type_decl list) : type_decl list =
     - optional names for the outputs values (we derive them for the backward
       functions)
  *)
-let translate_fun_signatures (fun_infos : FA.fun_info A.FunDeclId.Map.t)
-    (type_infos : TA.type_infos)
+let translate_fun_signatures (decls_ctx : C.decls_ctx)
     (functions : (A.fun_id * string option list * A.fun_sig) list) :
     fun_sig_named_outputs RegularFunIdNotLoopMap.t =
   (* For every function, translate the signatures of:
@@ -3033,17 +3033,14 @@ let translate_fun_signatures (fun_infos : FA.fun_info A.FunDeclId.Map.t)
       (sg : A.fun_sig) : (regular_fun_id_not_loop * fun_sig_named_outputs) list
       =
     (* The forward function *)
-    let fwd_sg =
-      translate_fun_sig fun_infos fun_id type_infos sg input_names None
-    in
+    let fwd_sg = translate_fun_sig decls_ctx fun_id sg input_names None in
     let fwd_id = (fun_id, None) in
     (* The backward functions *)
     let back_sgs =
       List.map
         (fun (rg : T.region_var_group) ->
           let tsg =
-            translate_fun_sig fun_infos fun_id type_infos sg input_names
-              (Some rg.id)
+            translate_fun_sig decls_ctx fun_id sg input_names (Some rg.id)
           in
           let id = (fun_id, Some rg.id) in
           (id, tsg))
-- 
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/SymbolicToPure.ml | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index be9b7261..429198ad 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -842,6 +842,33 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   (* Is the function stateful, and can it fail? *)
   let lid = None in
   let effect_info = get_fun_effect_info fun_infos (A.FunId fun_id) lid bid in
+  (* We need an evaluation context to normalize the types (to normalize the
+     associated types, etc. - for instance it may happen that the types
+     refer to the types associated to a trait ref, but where the trait ref
+     is a known impl). *)
+  (* Create the context *)
+  let ctx =
+    let region_groups =
+      List.map (fun (g : T.region_var_group) -> g.id) sg.regions_hierarchy
+    in
+    let ctx =
+      InterpreterUtils.initialize_eval_context decls_ctx region_groups
+        sg.generics.types sg.generics.const_generics
+    in
+    (* Compute the normalization map for the *sty* types and add it to the context *)
+    AssociatedTypes.ctx_add_norm_trait_stypes_from_preds ctx
+      sg.preds.trait_type_constraints
+  in
+
+  (* Normalize the signature *)
+  let sg =
+    let ({ A.inputs; output; _ } : A.fun_sig) = sg in
+    let norm = AssociatedTypes.ctx_normalize_sty ctx in
+    let inputs = List.map norm inputs in
+    let output = norm output in
+    { sg with A.inputs; output }
+  in
+
   (* List the inputs for:
    * - the fuel
    * - the forward function
-- 
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/SymbolicToPure.ml | 50 ++++++++++++++++++++++++++--------------------
 1 file changed, 28 insertions(+), 22 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 429198ad..54221cb1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -343,7 +343,7 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
 (* TODO: move *)
 let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
     (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
-  let id = (A.Regular def_id, back_id) in
+  let id = (E.Regular def_id, back_id) in
   (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg
 
 (* Some generic translation functions (we need to translate different "flavours"
@@ -390,6 +390,7 @@ and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
       let inst_id = translate_trait_instance_id inst_id in
       ItemClause (inst_id, decl_id, item_name, clause_id)
   | TraitRef tr -> TraitRef (translate_trait_ref translate_ty tr)
+  | FnPointer _ -> raise (Failure "TODO")
   | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s))
 
 let rec translate_sty (ty : T.sty) : ty =
@@ -427,6 +428,7 @@ let rec translate_sty (ty : T.sty) : ty =
       let trait_ref = translate_strait_ref trait_ref in
       let generics = translate_sgeneric_args generics in
       TraitType (trait_ref, generics, type_name)
+  | Arrow _ -> raise (Failure "TODO")
 
 and translate_sgeneric_args (generics : T.sgeneric_args) : generic_args =
   translate_generic_args translate_sty generics
@@ -569,6 +571,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
       TraitType (trait_ref, generics, type_name)
+  | Arrow _ -> raise (Failure "TODO")
 
 and translate_fwd_generic_args (type_infos : TA.type_infos)
     (generics : 'r T.generic_args) : generic_args =
@@ -658,6 +661,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
       Some (TraitType (trait_ref, generics, type_name))
+  | Arrow _ -> raise (Failure "TODO")
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
@@ -694,7 +698,7 @@ let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
 let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
     (id : A.fun_id_or_trait_method_ref) : fun_id_or_trait_method_ref =
   match id with
-  | A.FunId fun_id -> FunId fun_id
+  | FunId fun_id -> FunId fun_id
   | TraitMethod (trait_ref, method_name, fun_decl_id) ->
       let type_infos = ctx.type_context.type_infos in
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
@@ -795,7 +799,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with
-  | A.TraitMethod (_, _, fid) | A.FunId (A.Regular fid) ->
+  | TraitMethod (_, _, fid) | FunId (Regular fid) ->
       let info = A.FunDeclId.Map.find fid fun_infos in
       let stateful_group = info.stateful in
       let stateful =
@@ -808,7 +812,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
         can_diverge = info.can_diverge;
         is_rec = info.is_rec || Option.is_some lid;
       }
-  | A.FunId (A.Assumed aid) ->
+  | FunId (Assumed aid) ->
       assert (lid = None);
       {
         can_fail = Assumed.assumed_can_fail aid;
@@ -841,7 +845,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   in
   (* Is the function stateful, and can it fail? *)
   let lid = None in
-  let effect_info = get_fun_effect_info fun_infos (A.FunId fun_id) lid bid in
+  let effect_info = get_fun_effect_info fun_infos (FunId fun_id) lid bid in
   (* We need an evaluation context to normalize the types (to normalize the
      associated types, etc. - for instance it may happen that the types
      refer to the types associated to a trait ref, but where the trait ref
@@ -1706,18 +1710,20 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             in
             (ctx, Unop (Neg int_ty), effect_info, args, None)
         | _ -> raise (Failure "Unreachable"))
-    | S.Unop (E.Cast (src_ty, tgt_ty)) ->
-        (* Note that cast can fail *)
-        let effect_info =
-          {
-            can_fail = true;
-            stateful_group = false;
-            stateful = false;
-            can_diverge = false;
-            is_rec = false;
-          }
-        in
-        (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)
+    | S.Unop (E.Cast cast_kind) -> (
+        match cast_kind with
+        | CastInteger (src_ty, tgt_ty) ->
+            (* Note that cast can fail *)
+            let effect_info =
+              {
+                can_fail = true;
+                stateful_group = false;
+                stateful = false;
+                can_diverge = false;
+                is_rec = false;
+              }
+            in
+            (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None))
     | S.Binop binop -> (
         match args with
         | [ arg0; arg1 ] ->
@@ -1925,7 +1931,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
   (* Sanity check: there is the proper number of inputs and outputs, and they have the proper type *)
   (if (* TODO: normalize the types *) !Config.type_check_pure_code then
      match fun_id with
-     | A.FunId fun_id ->
+     | FunId fun_id ->
          let inst_sg =
            get_instantiated_fun_sig fun_id (Some rg_id) generics ctx
          in
@@ -2088,9 +2094,9 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       (* Actually the same case as [SynthInput] *)
       translate_end_abstraction_synth_input ectx abs e ctx rg_id
   | V.LoopCall ->
-      let fun_id = A.Regular ctx.fun_decl.A.def_id in
+      let fun_id = E.Regular ctx.fun_decl.A.def_id in
       let effect_info =
-        get_fun_effect_info ctx.fun_context.fun_infos (A.FunId fun_id)
+        get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
           (Some vloop_id) (Some rg_id)
       in
       let loop_info = LoopId.Map.find loop_id ctx.loops in
@@ -2553,9 +2559,9 @@ and translate_forward_end (ectx : C.eval_ctx)
       let org_args = args in
 
       (* Lookup the effect info for the loop function *)
-      let fid = A.Regular ctx.fun_decl.A.def_id in
+      let fid = E.Regular ctx.fun_decl.A.def_id in
       let effect_info =
-        get_fun_effect_info ctx.fun_context.fun_infos (A.FunId fid) None ctx.bid
+        get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
       in
 
       (* Introduce a fresh output value for the forward function *)
-- 
cgit v1.2.3


From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 23 Oct 2023 13:47:39 +0200
Subject: Remove some assumed types and add more support for builtin
 definitions

---
 compiler/SymbolicToPure.ml | 31 +++++++------------------------
 1 file changed, 7 insertions(+), 24 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 54221cb1..9c698b51 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -405,8 +405,6 @@ let rec translate_sty (ty : T.sty) : ty =
           mk_simpl_tuple_ty generics.types
       | T.Assumed aty -> (
           match aty with
-          | T.Vec -> Adt (Assumed Vec, generics)
-          | T.Option -> Adt (Assumed Option, generics)
           | T.Box -> (
               (* Eliminate the boxes *)
               match generics.types with
@@ -418,8 +416,7 @@ let rec translate_sty (ty : T.sty) : ty =
               )
           | T.Array -> Adt (Assumed Array, generics)
           | T.Slice -> Adt (Assumed Slice, generics)
-          | T.Str -> Adt (Assumed Str, generics)
-          | T.Range -> Adt (Assumed Range, generics)))
+          | T.Str -> Adt (Assumed Str, generics)))
   | TypeVar vid -> TypeVar vid
   | Literal ty -> Literal ty
   | Never -> raise (Failure "Unreachable")
@@ -510,12 +507,9 @@ let translate_type_id (id : T.type_id) : type_id =
   | T.Assumed aty ->
       let aty =
         match aty with
-        | T.Vec -> Vec
-        | T.Option -> Option
         | T.Array -> Array
         | T.Slice -> Slice
         | T.Str -> Str
-        | T.Range -> Range
         | T.Box ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
@@ -534,8 +528,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
       let t_generics = translate_fwd_generic_args type_infos generics in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _
-      | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+      | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) ->
           (* No general parametricity for now *)
           assert (
             not
@@ -610,8 +603,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   match ty with
   | T.Adt (type_id, generics) -> (
       match type_id with
-      | T.AdtId _
-      | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+      | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) ->
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           let type_id = translate_type_id type_id in
@@ -815,7 +807,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
   | FunId (Assumed aid) ->
       assert (lid = None);
       {
-        can_fail = Assumed.assumed_can_fail aid;
+        can_fail = Assumed.assumed_fun_can_fail aid;
         stateful_group = false;
         stateful = false;
         can_diverge = false;
@@ -1221,9 +1213,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* For now, only tuples can contain borrows *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _
-        | T.Assumed
-            (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+        | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
             assert (field_values = []);
             None
         | T.Tuple ->
@@ -1368,9 +1358,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
          * vector value upon visiting the "abstraction borrow" node *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _
-        | T.Assumed
-            (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+        | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
             assert (field_values = []);
             (ctx, None)
         | T.Tuple ->
@@ -2441,17 +2429,12 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_typed_pattern_from_var var None)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.Assumed (T.Vec | T.Array | T.Slice | T.Str) ->
+  | T.Assumed (T.Array | T.Slice | T.Str) ->
       (* We can't expand those values: we can access the fields only
        * through the functions provided by the API (note that we don't
        * know how to expand values like vectors or arrays, because they have a variable number
        * of fields!) *)
       raise (Failure "Attempt to expand a non-expandable value")
-  | T.Assumed Range -> raise (Failure "Unimplemented")
-  | T.Assumed T.Option ->
-      (* We shouldn't get there in the "one-branch" case: options have
-       * two variants *)
-      raise (Failure "Unreachable")
 
 and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
     (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression)
-- 
cgit v1.2.3


From ece74df70f12790bab7ecfe0c590c2c637e89801 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 11:40:31 +0200
Subject: Update following the addition of raw pointers

---
 compiler/SymbolicToPure.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 9c698b51..4ba5296f 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -421,6 +421,11 @@ let rec translate_sty (ty : T.sty) : ty =
   | Literal ty -> Literal ty
   | Never -> raise (Failure "Unreachable")
   | Ref (_, rty, _) -> translate rty
+  | RawPtr (ty, rkind) ->
+      let mut = match rkind with Mut -> Mut | Shared -> Const in
+      let ty = translate ty in
+      let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
+      Adt (Assumed (RawPtr mut), generics)
   | TraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_strait_ref trait_ref in
       let generics = translate_sgeneric_args generics in
@@ -560,6 +565,11 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
   | Never -> raise (Failure "Unreachable")
   | Literal lty -> Literal lty
   | Ref (_, rty, _) -> translate rty
+  | RawPtr (ty, rkind) ->
+      let mut = match rkind with Mut -> Mut | Shared -> Const in
+      let ty = translate ty in
+      let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
+      Adt (Assumed (RawPtr mut), generics)
   | TraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
@@ -646,6 +656,9 @@ let rec translate_back_ty (type_infos : TA.type_infos)
           if keep_region r then
             translate_back_ty type_infos keep_region inside_mut rty
           else None)
+  | RawPtr _ ->
+      (* TODO: not sure what to do here *)
+      None
   | TraitType (trait_ref, generics, type_name) ->
       assert (generics.regions = []);
       (* Translate the trait ref and the generics as "forward" generics -
-- 
cgit v1.2.3


From a41299c8543fe12f98ae2554bc9cefca6990af5f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 12:06:21 +0200
Subject: Fix some issues to make the array test succeed again

---
 compiler/SymbolicToPure.ml | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4ba5296f..885d2ba5 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -534,12 +534,6 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
       (* Eliminate boxes and simplify tuples *)
       match type_id with
       | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) ->
-          (* No general parametricity for now *)
-          assert (
-            not
-              (List.exists
-                 (TypesUtils.ty_has_borrows type_infos)
-                 generics.types));
           let type_id = translate_type_id type_id in
           Adt (type_id, t_generics)
       | Tuple ->
@@ -614,15 +608,24 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   | T.Adt (type_id, generics) -> (
       match type_id with
       | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) ->
-          (* Don't accept ADTs (which are not tuples) with borrows for now *)
-          assert (not (TypesUtils.ty_has_borrows type_infos ty));
           let type_id = translate_type_id type_id in
           if inside_mut then
             (* We do not want to filter anything, so we translate the generics
                as "forward" types *)
             let generics = translate_fwd_generic_args type_infos generics in
             Some (Adt (type_id, generics))
-          else None
+          else
+            (* If not inside a mutable reference: check if at least one
+               of the generics contains a mutable reference (i.e., is not
+               translated to `None`. If yes, keep the whole type, and
+               translate all the generics as "forward" types (the backward
+               function will extract the proper information from the ADT value)
+            *)
+            let types = List.filter_map translate generics.types in
+            if types <> [] then
+              let generics = translate_fwd_generic_args type_infos generics in
+              Some (Adt (type_id, generics))
+            else None
       | Assumed T.Box -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
-- 
cgit v1.2.3


From dc0032f6ce3b837ba2f431bbb5c9a92c625f629f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 30 Oct 2023 12:24:05 +0100
Subject: Make minor updates following changes in Charon

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

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 885d2ba5..c629a96f 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3092,21 +3092,19 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
 let translate_trait_decl (type_infos : TA.type_infos)
     (trait_decl : A.trait_decl) : trait_decl =
   let {
-    A.def_id;
+    def_id;
     name;
     generics;
     preds;
-    all_trait_clauses;
     consts;
     types;
     required_methods;
     provided_methods;
-  } =
+  } : A.trait_decl =
     trait_decl
   in
   let generics = translate_generic_params generics in
   let preds = translate_predicates preds in
-  let all_trait_clauses = List.map translate_trait_clause all_trait_clauses in
   let consts =
     List.map
       (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
@@ -3125,7 +3123,6 @@ let translate_trait_decl (type_infos : TA.type_infos)
     name;
     generics;
     preds;
-    all_trait_clauses;
     consts;
     types;
     required_methods;
-- 
cgit v1.2.3


From 4ba7d73fa3bfbf9ef41b2d9d5595f28fb67b8e47 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 6 Nov 2023 18:11:24 +0100
Subject: Update following some changes in Charon

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

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index c629a96f..46aa3b83 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3096,6 +3096,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
     name;
     generics;
     preds;
+    parent_clauses;
     consts;
     types;
     required_methods;
@@ -3105,6 +3106,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
   in
   let generics = translate_generic_params generics in
   let preds = translate_predicates preds in
+  let parent_clauses = List.map translate_trait_clause parent_clauses in
   let consts =
     List.map
       (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
@@ -3123,6 +3125,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
     name;
     generics;
     preds;
+    parent_clauses;
     consts;
     types;
     required_methods;
-- 
cgit v1.2.3


From ed788eec1d8be1656c0ad7dab25975ad3f5497c2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Nov 2023 10:40:27 +0100
Subject: Update the normalization of associated types

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

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 46aa3b83..2ce8c706 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3140,6 +3140,7 @@ let translate_trait_impl (type_infos : TA.type_infos)
     impl_trait;
     generics;
     preds;
+    parent_trait_refs;
     consts;
     types;
     required_methods;
@@ -3152,6 +3153,7 @@ let translate_trait_impl (type_infos : TA.type_infos)
   in
   let generics = translate_generic_params generics in
   let preds = translate_predicates preds in
+  let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in
   let consts =
     List.map
       (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
@@ -3171,6 +3173,7 @@ let translate_trait_impl (type_infos : TA.type_infos)
     impl_trait;
     generics;
     preds;
+    parent_trait_refs;
     consts;
     types;
     required_methods;
-- 
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/SymbolicToPure.ml | 219 +++++++++++++++++++++++----------------------
 1 file changed, 113 insertions(+), 106 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2ce8c706..97755438 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -213,14 +213,12 @@ let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
     ctx.trait_decls_ctx ctx.trait_impls_ctx ctx.fun_decl
 
 let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
-  let rvar_to_string = Print.Types.region_var_id_to_string in
-  let r_to_string = Print.Types.region_id_to_string in
+  let region_id_to_string = Print.Types.region_id_to_string in
   let type_var_id_to_string = Print.Types.type_var_id_to_string in
   let var_id_to_string = Print.Expressions.var_id_to_string in
   let ast_fmt = bs_ctx_to_ast_formatter ctx in
   {
-    Print.Values.rvar_to_string;
-    r_to_string;
+    Print.Values.region_id_to_string;
     type_var_id_to_string;
     type_decl_id_to_string = ast_fmt.type_decl_id_to_string;
     const_generic_var_id_to_string = ast_fmt.const_generic_var_id_to_string;
@@ -242,30 +240,29 @@ let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
     ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
     generics.const_generics
 
-let ctx_egeneric_args_to_string (ctx : bs_ctx) (args : T.egeneric_args) : string
-    =
+let ctx_generic_args_to_string (ctx : bs_ctx) (args : T.generic_args) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_etype_formatter fmt in
-  Print.PT.egeneric_args_to_string fmt args
+  let fmt = Print.PC.ctx_to_type_formatter fmt in
+  Print.PT.generic_args_to_string fmt args
 
 let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_rtype_formatter fmt in
+  let fmt = Print.PC.ctx_to_type_formatter fmt in
   Print.PV.symbolic_value_to_string fmt sv
 
 let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
   Print.PV.typed_value_to_string fmt v
 
-let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
+let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let fmt = bs_ctx_to_pp_ast_formatter ctx in
   let fmt = PrintPure.ast_to_type_formatter fmt in
   PrintPure.ty_to_string fmt false ty
 
-let rty_to_string (ctx : bs_ctx) (ty : T.rty) : string =
+let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_rtype_formatter fmt in
-  Print.PT.rty_to_string fmt ty
+  let fmt = Print.PC.ctx_to_type_formatter fmt in
+  Print.PT.ty_to_string fmt ty
 
 let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
   let type_decls = ctx.type_context.llbc_type_decls in
@@ -343,13 +340,13 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
 (* TODO: move *)
 let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
     (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
-  let id = (E.Regular def_id, back_id) in
+  let id = (E.FRegular def_id, back_id) in
   (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg
 
 (* Some generic translation functions (we need to translate different "flavours"
-   of types: sty, forward types, backward types, etc.) *)
-let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
-    (generics : 'r T.generic_args) : generic_args =
+   of types: forward types, backward types, etc.) *)
+let rec translate_generic_args (translate_ty : T.ty -> ty)
+    (generics : T.generic_args) : generic_args =
   (* We ignore the regions: if they didn't cause trouble for the symbolic execution,
      then everything's fine *)
   let types = List.map translate_ty generics.types in
@@ -359,7 +356,7 @@ let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
   in
   { types; const_generics; trait_refs }
 
-and translate_trait_ref (translate_ty : 'r T.ty -> ty) (tr : 'r T.trait_ref) :
+and translate_trait_ref (translate_ty : T.ty -> ty) (tr : T.trait_ref) :
     trait_ref =
   let trait_id = translate_trait_instance_id translate_ty tr.trait_id in
   let generics = translate_generic_args translate_ty tr.generics in
@@ -368,13 +365,13 @@ and translate_trait_ref (translate_ty : 'r T.ty -> ty) (tr : 'r T.trait_ref) :
   in
   { trait_id; generics; trait_decl_ref }
 
-and translate_trait_decl_ref (translate_ty : 'r T.ty -> ty)
-    (tr : 'r T.trait_decl_ref) : trait_decl_ref =
+and translate_trait_decl_ref (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref)
+    : trait_decl_ref =
   let decl_generics = translate_generic_args translate_ty tr.decl_generics in
   { trait_decl_id = tr.trait_decl_id; decl_generics }
 
-and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
-    (id : 'r T.trait_instance_id) : trait_instance_id =
+and translate_trait_instance_id (translate_ty : T.ty -> ty)
+    (id : T.trait_instance_id) : trait_instance_id =
   let translate_trait_instance_id = translate_trait_instance_id translate_ty in
   match id with
   | T.Self -> Self
@@ -393,19 +390,20 @@ and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
   | FnPointer _ -> raise (Failure "TODO")
   | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s))
 
-let rec translate_sty (ty : T.sty) : ty =
+(** Translate a signature type - TODO: factor out the different translation functions *)
+let rec translate_sty (ty : T.ty) : ty =
   let translate = translate_sty in
   match ty with
-  | T.Adt (type_id, generics) -> (
+  | T.TAdt (type_id, generics) -> (
       let generics = translate_sgeneric_args generics in
       match type_id with
-      | T.AdtId adt_id -> Adt (AdtId adt_id, generics)
+      | T.AdtId adt_id -> TAdt (AdtId adt_id, generics)
       | T.Tuple ->
           assert (generics.const_generics = []);
           mk_simpl_tuple_ty generics.types
-      | T.Assumed aty -> (
+      | T.TAssumed aty -> (
           match aty with
-          | T.Box -> (
+          | T.TBox -> (
               (* Eliminate the boxes *)
               match generics.types with
               | [ ty ] -> ty
@@ -414,31 +412,31 @@ let rec translate_sty (ty : T.sty) : ty =
                     (Failure
                        "Box/vec/option type with incorrect number of arguments")
               )
-          | T.Array -> Adt (Assumed Array, generics)
-          | T.Slice -> Adt (Assumed Slice, generics)
-          | T.Str -> Adt (Assumed Str, generics)))
+          | T.TArray -> TAdt (TAssumed Array, generics)
+          | T.TSlice -> TAdt (TAssumed Slice, generics)
+          | T.TStr -> TAdt (TAssumed Str, generics)))
   | TypeVar vid -> TypeVar vid
-  | Literal ty -> Literal ty
+  | TLiteral ty -> TLiteral ty
   | Never -> raise (Failure "Unreachable")
   | Ref (_, rty, _) -> translate rty
   | RawPtr (ty, rkind) ->
       let mut = match rkind with Mut -> Mut | Shared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
-      Adt (Assumed (RawPtr mut), generics)
+      TAdt (TAssumed (RawPtr mut), generics)
   | TraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_strait_ref trait_ref in
       let generics = translate_sgeneric_args generics in
       TraitType (trait_ref, generics, type_name)
   | Arrow _ -> raise (Failure "TODO")
 
-and translate_sgeneric_args (generics : T.sgeneric_args) : generic_args =
+and translate_sgeneric_args (generics : T.generic_args) : generic_args =
   translate_generic_args translate_sty generics
 
-and translate_strait_ref (tr : T.strait_ref) : trait_ref =
+and translate_strait_ref (tr : T.trait_ref) : trait_ref =
   translate_trait_ref translate_sty tr
 
-and translate_strait_instance_id (id : T.strait_instance_id) : trait_instance_id
+and translate_strait_instance_id (id : T.trait_instance_id) : trait_instance_id
     =
   translate_trait_instance_id translate_sty id
 
@@ -447,7 +445,7 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause =
   let generics = translate_sgeneric_args generics in
   { clause_id; trait_id; generics }
 
-let translate_strait_type_constraint (ttc : T.strait_type_constraint) :
+let translate_strait_type_constraint (ttc : T.trait_type_constraint) :
     trait_type_constraint =
   let { T.trait_ref; generics; type_name; ty } = ttc in
   let trait_ref = translate_strait_ref trait_ref in
@@ -509,38 +507,43 @@ let translate_type_decl (def : T.type_decl) : type_decl =
 let translate_type_id (id : T.type_id) : type_id =
   match id with
   | AdtId adt_id -> AdtId adt_id
-  | T.Assumed aty ->
+  | T.TAssumed aty ->
       let aty =
         match aty with
-        | T.Array -> Array
-        | T.Slice -> Slice
-        | T.Str -> Str
-        | T.Box ->
+        | T.TArray -> Array
+        | T.TSlice -> Slice
+        | T.TStr -> Str
+        | T.TBox ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
             raise (Failure "Unreachable")
       in
-      Assumed aty
+      TAssumed aty
   | T.Tuple -> Tuple
 
 (** Translate a type, seen as an input/output of a forward function
-    (preserve all borrows, etc.)
+    (preserve all borrows, etc.).
+
+    Remark: it doesn't matter whether the types has regions or erased regions
+    (both cases happen, actually).
+
+    TODO: factor out the various translation functions.
 *)
-let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
+let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
   let translate = translate_fwd_ty type_infos in
   match ty with
-  | T.Adt (type_id, generics) -> (
+  | T.TAdt (type_id, generics) -> (
       let t_generics = translate_fwd_generic_args type_infos generics in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) ->
+      | AdtId _ | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
           let type_id = translate_type_id type_id in
-          Adt (type_id, t_generics)
+          TAdt (type_id, t_generics)
       | Tuple ->
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
           mk_simpl_tuple_ty t_generics.types
-      | T.Assumed T.Box -> (
+      | T.TAssumed T.TBox -> (
           (* We eliminate boxes *)
           (* No general parametricity for now *)
           assert (
@@ -557,13 +560,13 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
                     parameter")))
   | TypeVar vid -> TypeVar vid
   | Never -> raise (Failure "Unreachable")
-  | Literal lty -> Literal lty
+  | TLiteral lty -> TLiteral lty
   | Ref (_, rty, _) -> translate rty
   | RawPtr (ty, rkind) ->
       let mut = match rkind with Mut -> Mut | Shared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
-      Adt (Assumed (RawPtr mut), generics)
+      TAdt (TAssumed (RawPtr mut), generics)
   | TraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
@@ -571,25 +574,25 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
   | Arrow _ -> raise (Failure "TODO")
 
 and translate_fwd_generic_args (type_infos : TA.type_infos)
-    (generics : 'r T.generic_args) : generic_args =
+    (generics : T.generic_args) : generic_args =
   translate_generic_args (translate_fwd_ty type_infos) generics
 
-and translate_fwd_trait_ref (type_infos : TA.type_infos) (tr : 'r T.trait_ref) :
+and translate_fwd_trait_ref (type_infos : TA.type_infos) (tr : T.trait_ref) :
     trait_ref =
   translate_trait_ref (translate_fwd_ty type_infos) tr
 
 and translate_fwd_trait_instance_id (type_infos : TA.type_infos)
-    (id : 'r T.trait_instance_id) : trait_instance_id =
+    (id : T.trait_instance_id) : trait_instance_id =
   translate_trait_instance_id (translate_fwd_ty type_infos) id
 
 (** Simply calls [translate_fwd_ty] *)
-let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : 'r T.ty) : ty =
+let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty =
   let type_infos = ctx.type_context.type_infos in
   translate_fwd_ty type_infos ty
 
 (** Simply calls [translate_fwd_generic_args] *)
-let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : 'r T.generic_args)
-    : generic_args =
+let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
+    generic_args =
   let type_infos = ctx.type_context.type_infos in
   translate_fwd_generic_args type_infos generics
 
@@ -600,20 +603,21 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : 'r T.generic_args)
     [inside_mut]: are we inside a mutable borrow?
  *)
 let rec translate_back_ty (type_infos : TA.type_infos)
-    (keep_region : 'r -> bool) (inside_mut : bool) (ty : 'r T.ty) : ty option =
+    (keep_region : T.region -> bool) (inside_mut : bool) (ty : T.ty) : ty option
+    =
   let translate = translate_back_ty type_infos keep_region inside_mut in
   (* A small helper for "leave" types *)
   let wrap ty = if inside_mut then Some ty else None in
   match ty with
-  | T.Adt (type_id, generics) -> (
+  | T.TAdt (type_id, generics) -> (
       match type_id with
-      | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) ->
+      | T.AdtId _ | TAssumed (T.TArray | T.TSlice | T.TStr) ->
           let type_id = translate_type_id type_id in
           if inside_mut then
             (* We do not want to filter anything, so we translate the generics
                as "forward" types *)
             let generics = translate_fwd_generic_args type_infos generics in
-            Some (Adt (type_id, generics))
+            Some (TAdt (type_id, generics))
           else
             (* If not inside a mutable reference: check if at least one
                of the generics contains a mutable reference (i.e., is not
@@ -624,9 +628,9 @@ let rec translate_back_ty (type_infos : TA.type_infos)
             let types = List.filter_map translate generics.types in
             if types <> [] then
               let generics = translate_fwd_generic_args type_infos generics in
-              Some (Adt (type_id, generics))
+              Some (TAdt (type_id, generics))
             else None
-      | Assumed T.Box -> (
+      | TAssumed T.TBox -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           (* Eliminate the box *)
@@ -647,7 +651,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               Some (mk_simpl_tuple_ty tys_t)))
   | TypeVar vid -> wrap (TypeVar vid)
   | Never -> raise (Failure "Unreachable")
-  | Literal lty -> wrap (Literal lty)
+  | TLiteral lty -> wrap (TLiteral lty)
   | Ref (r, rty, rkind) -> (
       match rkind with
       | T.Shared ->
@@ -673,7 +677,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
-    (inside_mut : bool) (ty : 'r T.ty) : ty option =
+    (inside_mut : bool) (ty : T.ty) : ty option =
   let type_infos = ctx.type_context.type_infos in
   translate_back_ty type_infos keep_region inside_mut ty
 
@@ -682,7 +686,7 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
     T.ConstGenericVarId.Map.of_list
       (List.map
          (fun (cg : T.const_generic_var) ->
-           (cg.index, ctx_translate_fwd_ty ctx (T.Literal cg.ty)))
+           (cg.index, ctx_translate_fwd_ty ctx (T.TLiteral cg.ty)))
          ctx.sg.generics.const_generics)
   in
   let env = VarId.Map.empty in
@@ -807,7 +811,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with
-  | TraitMethod (_, _, fid) | FunId (Regular fid) ->
+  | TraitMethod (_, _, fid) | FunId (FRegular fid) ->
       let info = A.FunDeclId.Map.find fid fun_infos in
       let stateful_group = info.stateful in
       let stateful =
@@ -820,7 +824,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
         can_diverge = info.can_diverge;
         is_rec = info.is_rec || Option.is_some lid;
       }
-  | FunId (Assumed aid) ->
+  | FunId (FAssumed aid) ->
       assert (lid = None);
       {
         can_fail = Assumed.assumed_fun_can_fail aid;
@@ -861,21 +865,21 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   (* Create the context *)
   let ctx =
     let region_groups =
-      List.map (fun (g : T.region_var_group) -> g.id) sg.regions_hierarchy
+      List.map (fun (g : T.region_group) -> g.id) sg.regions_hierarchy
     in
     let ctx =
       InterpreterUtils.initialize_eval_context decls_ctx region_groups
         sg.generics.types sg.generics.const_generics
     in
     (* Compute the normalization map for the *sty* types and add it to the context *)
-    AssociatedTypes.ctx_add_norm_trait_stypes_from_preds ctx
+    AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
       sg.preds.trait_type_constraints
   in
 
   (* Normalize the signature *)
   let sg =
     let ({ A.inputs; output; _ } : A.fun_sig) = sg in
-    let norm = AssociatedTypes.ctx_normalize_sty ctx in
+    let norm = AssociatedTypes.ctx_normalize_ty ctx in
     let inputs = List.map norm inputs in
     let output = norm output in
     { sg with A.inputs; output }
@@ -893,14 +897,14 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
    * so just check that there aren't parent regions *)
   assert (T.RegionGroupId.Set.is_empty parents);
   (* Small helper to translate types for backward functions *)
-  let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.sty -> ty option
-      =
+  let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.ty -> ty option =
     let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
-    let regions = T.RegionVarId.Set.of_list rg.regions in
+    let regions = T.RegionId.Set.of_list rg.regions in
     let keep_region r =
       match r with
-      | T.Static -> raise Unimplemented
-      | T.Var r -> T.RegionVarId.Set.mem r regions
+      | T.RStatic -> raise Unimplemented
+      | T.RErased -> raise (Failure "Unexpected erased region")
+      | T.RVar r -> T.RegionId.Set.mem r regions
     in
     let inside_mut = false in
     translate_back_ty type_infos keep_region inside_mut
@@ -1042,7 +1046,7 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
   (* Return *)
   (ctx, state_pat)
 
-let fresh_var_llbc_ty (basename : string option) (ty : 'r T.ty) (ctx : bs_ctx) :
+let fresh_var_llbc_ty (basename : string option) (ty : T.ty) (ctx : bs_ctx) :
     bs_ctx * var =
   (* Generate the fresh variable *)
   let id, var_counter = VarId.fresh ctx.var_counter in
@@ -1106,7 +1110,7 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
 (** Peel boxes as long as the value is of the form [Box<T>] *)
 let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
   match (v.value, v.ty) with
-  | V.Adt av, T.Adt (T.Assumed T.Box, _) -> (
+  | V.VAdt av, T.TAdt (T.TAssumed T.TBox, _) -> (
       match av.field_values with
       | [ bv ] -> unbox_typed_value bv
       | _ -> raise (Failure "Unreachable"))
@@ -1145,13 +1149,13 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
   (* Translate the value *)
   let value =
     match v.value with
-    | V.Literal cv -> { e = Const cv; ty }
-    | Adt av -> (
+    | V.VLiteral cv -> { e = Const cv; ty }
+    | VAdt av -> (
         let variant_id = av.variant_id in
         let field_values = List.map translate av.field_values in
         (* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
         match v.ty with
-        | T.Adt (T.Tuple, _) ->
+        | T.TAdt (T.Tuple, _) ->
             assert (variant_id = None);
             mk_simpl_tuple_texpression field_values
         | _ ->
@@ -1229,7 +1233,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* For now, only tuples can contain borrows *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
+        | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
             assert (field_values = []);
             None
         | T.Tuple ->
@@ -1374,7 +1378,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
          * vector value upon visiting the "abstraction borrow" node *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
+        | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
             assert (field_values = []);
             (ctx, None)
         | T.Tuple ->
@@ -1645,7 +1649,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
   log#ldebug
     (lazy
       ("translate_function_call:\n"
-      ^ ctx_egeneric_args_to_string ctx call.generics));
+      ^ ctx_generic_args_to_string ctx call.generics));
   (* Translate the function call *)
   let generics = ctx_translate_fwd_generic_args ctx call.generics in
   let args =
@@ -1845,11 +1849,12 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
       ("translate_end_abstraction_synth_input:"
      ^ "\n\n- given back variables types:\n"
       ^ Print.list_to_string
-          (fun (v : var) -> ty_to_string ctx v.ty)
+          (fun (v : var) -> pure_ty_to_string ctx v.ty)
           given_back_variables
       ^ "\n\n- consumed values:\n"
       ^ Print.list_to_string
-          (fun e -> texpression_to_string ctx e ^ " : " ^ ty_to_string ctx e.ty)
+          (fun e ->
+            texpression_to_string ctx e ^ " : " ^ pure_ty_to_string ctx e.ty)
           consumed_values
       ^ "\n"));
 
@@ -1948,7 +1953,8 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
              ^ "\n- inst_sg.inputs ("
              ^ string_of_int (List.length inst_sg.inputs)
              ^ "): "
-             ^ String.concat ", " (List.map (ty_to_string ctx) inst_sg.inputs)));
+             ^ String.concat ", "
+                 (List.map (pure_ty_to_string ctx) inst_sg.inputs)));
          List.iter
            (fun (x, ty) -> assert ((x : texpression).ty = ty))
            (List.combine inputs inst_sg.inputs);
@@ -2070,8 +2076,9 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
       log#ldebug
         (lazy
           ("\n- given_back ty: "
-          ^ ty_to_string ctx given_back.ty
-          ^ "\n- sig input ty: " ^ ty_to_string ctx input.ty));
+          ^ pure_ty_to_string ctx given_back.ty
+          ^ "\n- sig input ty: "
+          ^ pure_ty_to_string ctx input.ty));
       assert (given_back.ty = input.ty))
     given_back_inputs;
   (* Translate the next expression *)
@@ -2098,7 +2105,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       (* Actually the same case as [SynthInput] *)
       translate_end_abstraction_synth_input ectx abs e ctx rg_id
   | V.LoopCall ->
-      let fun_id = E.Regular ctx.fun_decl.A.def_id in
+      let fun_id = E.FRegular ctx.fun_decl.A.def_id in
       let effect_info =
         get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
           (Some vloop_id) (Some rg_id)
@@ -2229,7 +2236,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
   let func =
     { id = FunOrOp (Fun (Pure Assert)); generics = empty_generic_args }
   in
-  let func_ty = mk_arrow (Literal Bool) mk_unit_ty in
+  let func_ty = mk_arrow (TLiteral TBool) mk_unit_ty in
   let func = { e = Qualif func; ty = func_ty } in
   let assertion = mk_apps func args in
   mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e
@@ -2325,12 +2332,12 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
         (* We don't need to update the context: we don't introduce any
            * new values/variables *)
         let branch = translate_expression branch_e ctx in
-        let pat = mk_typed_pattern_from_literal (PV.Scalar v) in
+        let pat = mk_typed_pattern_from_literal (PV.VScalar v) in
         { pat; branch }
       in
       let branches = List.map translate_branch branches in
       let otherwise = translate_expression otherwise ctx in
-      let pat_ty = Literal (Integer int_ty) in
+      let pat_ty = TLiteral (TInteger int_ty) in
       let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in
       let otherwise : match_branch =
         { pat = otherwise_pat; branch = otherwise }
@@ -2433,7 +2440,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_simpl_tuple_pattern vars)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.Assumed T.Box ->
+  | T.TAssumed T.TBox ->
       (* There should be exactly one variable *)
       let var =
         match vars with [ v ] -> v | _ -> raise (Failure "Unreachable")
@@ -2445,7 +2452,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_typed_pattern_from_var var None)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.Assumed (T.Array | T.Slice | T.Str) ->
+  | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
       (* We can't expand those values: we can access the fields only
        * through the functions provided by the API (note that we don't
        * know how to expand values like vectors or arrays, because they have a variable number
@@ -2469,19 +2476,19 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
   *)
   let v =
     match v with
-    | SingleValue v -> typed_value_to_texpression ctx ectx v
-    | Array values ->
+    | VaSingleValue v -> typed_value_to_texpression ctx ectx v
+    | VaArray values ->
         (* We use a struct update to encode the array aggregate, in order
            to preserve the structure and allow generating code of the shape
            `[x0, ...., xn]` *)
         let values = List.map (typed_value_to_texpression ctx ectx) values in
         let values = FieldId.mapi (fun fid v -> (fid, v)) values in
         let su : struct_update =
-          { struct_id = Assumed Array; init = None; updates = values }
+          { struct_id = TAssumed Array; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
-    | ConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
-    | TraitConstValue (trait_ref, generics, const_name) ->
+    | VaConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | VaTraitConstValue (trait_ref, generics, const_name) ->
         let type_infos = ctx.type_context.type_infos in
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
         let generics = translate_fwd_generic_args type_infos generics in
@@ -2558,7 +2565,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       let org_args = args in
 
       (* Lookup the effect info for the loop function *)
-      let fid = E.Regular ctx.fun_decl.A.def_id in
+      let fid = E.FRegular ctx.fun_decl.A.def_id in
       let effect_info =
         get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
       in
@@ -2661,7 +2668,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         ^ T.RegionGroupId.Map.show
             (fun (rids, tys) ->
               "(" ^ T.RegionId.Set.show rids ^ ", "
-              ^ Print.list_to_string (rty_to_string ctx) tys
+              ^ Print.list_to_string (ty_to_string ctx) tys
               ^ ")")
             loop.rg_to_given_back_tys
         ^ "\n"));
@@ -2925,8 +2932,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     | None -> None
     | Some body ->
         let effect_info =
-          get_fun_effect_info ctx.fun_context.fun_infos (FunId (Regular def_id))
-            None bid
+          get_fun_effect_info ctx.fun_context.fun_infos
+            (FunId (FRegular def_id)) None bid
         in
         let body = translate_expression body ctx in
         (* Add a match over the fuel, if necessary *)
@@ -2999,8 +3006,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
             ^ "\n- back_state: "
             ^ String.concat ", " (List.map show_var back_state)
             ^ "\n- signature.inputs: "
-            ^ String.concat ", " (List.map (ty_to_string ctx) signature.inputs)
-            ));
+            ^ String.concat ", "
+                (List.map (pure_ty_to_string ctx) signature.inputs)));
         (* TODO: we need to normalize the types *)
         if !Config.type_check_pure_code then
           assert (
@@ -3070,7 +3077,7 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
     (* The backward functions *)
     let back_sgs =
       List.map
-        (fun (rg : T.region_var_group) ->
+        (fun (rg : T.region_group) ->
           let tsg =
             translate_fun_sig decls_ctx fun_id sg input_names (Some rg.id)
           in
-- 
cgit v1.2.3


From 0a5859fbb7bcd99bfa221eaf1af029ff660bf963 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 19:35:24 +0100
Subject: Rename some variants

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

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 97755438..91edbf04 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2487,7 +2487,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
           { struct_id = TAssumed Array; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
-    | VaConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
     | VaTraitConstValue (trait_ref, generics, const_name) ->
         let type_infos = ctx.type_context.type_infos in
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
@@ -2740,7 +2740,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       in
       let const_generics =
         List.map
-          (fun (cg : T.const_generic_var) -> T.ConstGenericVar cg.T.index)
+          (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
           const_generics
       in
       let trait_refs =
-- 
cgit v1.2.3


From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 20:04:11 +0100
Subject: Prefix variants related to types with "T"

---
 compiler/SymbolicToPure.ml | 104 ++++++++++++++++++++++-----------------------
 1 file changed, 51 insertions(+), 53 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 91edbf04..60020d9a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -397,8 +397,8 @@ let rec translate_sty (ty : T.ty) : ty =
   | T.TAdt (type_id, generics) -> (
       let generics = translate_sgeneric_args generics in
       match type_id with
-      | T.AdtId adt_id -> TAdt (AdtId adt_id, generics)
-      | T.Tuple ->
+      | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics)
+      | T.TTuple ->
           assert (generics.const_generics = []);
           mk_simpl_tuple_ty generics.types
       | T.TAssumed aty -> (
@@ -412,23 +412,23 @@ let rec translate_sty (ty : T.ty) : ty =
                     (Failure
                        "Box/vec/option type with incorrect number of arguments")
               )
-          | T.TArray -> TAdt (TAssumed Array, generics)
-          | T.TSlice -> TAdt (TAssumed Slice, generics)
-          | T.TStr -> TAdt (TAssumed Str, generics)))
-  | TypeVar vid -> TypeVar vid
+          | T.TArray -> TAdt (TAssumed TArray, generics)
+          | T.TSlice -> TAdt (TAssumed TSlice, generics)
+          | T.TStr -> TAdt (TAssumed TStr, generics)))
+  | TVar vid -> TVar vid
   | TLiteral ty -> TLiteral ty
-  | Never -> raise (Failure "Unreachable")
-  | Ref (_, rty, _) -> translate rty
-  | RawPtr (ty, rkind) ->
+  | TNever -> raise (Failure "Unreachable")
+  | TRef (_, rty, _) -> translate rty
+  | TRawPtr (ty, rkind) ->
       let mut = match rkind with Mut -> Mut | Shared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
-      TAdt (TAssumed (RawPtr mut), generics)
-  | TraitType (trait_ref, generics, type_name) ->
+      TAdt (TAssumed (TRawPtr mut), generics)
+  | TTraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_strait_ref trait_ref in
       let generics = translate_sgeneric_args generics in
-      TraitType (trait_ref, generics, type_name)
-  | Arrow _ -> raise (Failure "TODO")
+      TTraitType (trait_ref, generics, type_name)
+  | TArrow _ -> raise (Failure "TODO")
 
 and translate_sgeneric_args (generics : T.generic_args) : generic_args =
   translate_generic_args translate_sty generics
@@ -506,20 +506,20 @@ let translate_type_decl (def : T.type_decl) : type_decl =
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
-  | AdtId adt_id -> AdtId adt_id
-  | T.TAssumed aty ->
+  | TAdtId adt_id -> TAdtId adt_id
+  | TAssumed aty ->
       let aty =
         match aty with
-        | T.TArray -> Array
-        | T.TSlice -> Slice
-        | T.TStr -> Str
+        | T.TArray -> TArray
+        | T.TSlice -> TSlice
+        | T.TStr -> TStr
         | T.TBox ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
             raise (Failure "Unreachable")
       in
       TAssumed aty
-  | T.Tuple -> Tuple
+  | TTuple -> TTuple
 
 (** Translate a type, seen as an input/output of a forward function
     (preserve all borrows, etc.).
@@ -536,14 +536,14 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
       let t_generics = translate_fwd_generic_args type_infos generics in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _ | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
+      | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
           let type_id = translate_type_id type_id in
           TAdt (type_id, t_generics)
-      | Tuple ->
+      | TTuple ->
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
           mk_simpl_tuple_ty t_generics.types
-      | T.TAssumed T.TBox -> (
+      | TAssumed TBox -> (
           (* We eliminate boxes *)
           (* No general parametricity for now *)
           assert (
@@ -558,20 +558,20 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
                 (Failure
                    "Unreachable: box/vec/option receives exactly one type \
                     parameter")))
-  | TypeVar vid -> TypeVar vid
-  | Never -> raise (Failure "Unreachable")
+  | TVar vid -> TVar vid
+  | TNever -> raise (Failure "Unreachable")
   | TLiteral lty -> TLiteral lty
-  | Ref (_, rty, _) -> translate rty
-  | RawPtr (ty, rkind) ->
+  | TRef (_, rty, _) -> translate rty
+  | TRawPtr (ty, rkind) ->
       let mut = match rkind with Mut -> Mut | Shared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
-      TAdt (TAssumed (RawPtr mut), generics)
-  | TraitType (trait_ref, generics, type_name) ->
+      TAdt (TAssumed (TRawPtr mut), generics)
+  | TTraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
-      TraitType (trait_ref, generics, type_name)
-  | Arrow _ -> raise (Failure "TODO")
+      TTraitType (trait_ref, generics, type_name)
+  | TArrow _ -> raise (Failure "TODO")
 
 and translate_fwd_generic_args (type_infos : TA.type_infos)
     (generics : T.generic_args) : generic_args =
@@ -611,7 +611,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   match ty with
   | T.TAdt (type_id, generics) -> (
       match type_id with
-      | T.AdtId _ | TAssumed (T.TArray | T.TSlice | T.TStr) ->
+      | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
           let type_id = translate_type_id type_id in
           if inside_mut then
             (* We do not want to filter anything, so we translate the generics
@@ -630,7 +630,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               let generics = translate_fwd_generic_args type_infos generics in
               Some (TAdt (type_id, generics))
             else None
-      | TAssumed T.TBox -> (
+      | TAssumed TBox -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           (* Eliminate the box *)
@@ -640,7 +640,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               raise
                 (Failure "Unreachable: boxes receive exactly one type parameter")
           )
-      | T.Tuple -> (
+      | TTuple -> (
           (* Tuples can contain borrows (which we eliminate) *)
           let tys_t = List.filter_map translate generics.types in
           match tys_t with
@@ -649,10 +649,10 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               (* Note that if there is exactly one type, [mk_simpl_tuple_ty]
                * is the identity *)
               Some (mk_simpl_tuple_ty tys_t)))
-  | TypeVar vid -> wrap (TypeVar vid)
-  | Never -> raise (Failure "Unreachable")
+  | TVar vid -> wrap (TVar vid)
+  | TNever -> raise (Failure "Unreachable")
   | TLiteral lty -> wrap (TLiteral lty)
-  | Ref (r, rty, rkind) -> (
+  | TRef (r, rty, rkind) -> (
       match rkind with
       | T.Shared ->
           (* Ignore shared references, unless we are below a mutable borrow *)
@@ -663,17 +663,17 @@ let rec translate_back_ty (type_infos : TA.type_infos)
           if keep_region r then
             translate_back_ty type_infos keep_region inside_mut rty
           else None)
-  | RawPtr _ ->
+  | TRawPtr _ ->
       (* TODO: not sure what to do here *)
       None
-  | TraitType (trait_ref, generics, type_name) ->
+  | TTraitType (trait_ref, generics, type_name) ->
       assert (generics.regions = []);
       (* Translate the trait ref and the generics as "forward" generics -
          we do not want to filter any type *)
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
-      Some (TraitType (trait_ref, generics, type_name))
-  | Arrow _ -> raise (Failure "TODO")
+      Some (TTraitType (trait_ref, generics, type_name))
+  | TArrow _ -> raise (Failure "TODO")
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
@@ -1155,7 +1155,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
         let field_values = List.map translate av.field_values in
         (* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
         match v.ty with
-        | T.TAdt (T.Tuple, _) ->
+        | TAdt (TTuple, _) ->
             assert (variant_id = None);
             mk_simpl_tuple_texpression field_values
         | _ ->
@@ -1233,10 +1233,10 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* For now, only tuples can contain borrows *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
+        | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
             assert (field_values = []);
             None
-        | T.Tuple ->
+        | TTuple ->
             (* Return *)
             if field_values = [] then None
             else
@@ -1378,10 +1378,10 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
          * vector value upon visiting the "abstraction borrow" node *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
+        | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
             assert (field_values = []);
             (ctx, None)
-        | T.Tuple ->
+        | TTuple ->
             (* Return *)
             let variant_id = adt_v.variant_id in
             assert (variant_id = None);
@@ -2386,7 +2386,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
   let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
   let branch = translate_expression branch ctx in
   match type_id with
-  | T.AdtId adt_id ->
+  | TAdtId adt_id ->
       (* Detect if this is an enumeration or not *)
       let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
       let is_enum = TypesUtils.type_decl_is_enum tdef in
@@ -2433,14 +2433,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
             let field_proj = gen_field_proj fid var in
             mk_let monadic (mk_typed_pattern_from_var var None) field_proj e)
           id_var_pairs branch
-  | T.Tuple ->
+  | TTuple ->
       let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in
       let monadic = false in
       mk_let monadic
         (mk_simpl_tuple_pattern vars)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.TAssumed T.TBox ->
+  | TAssumed TBox ->
       (* There should be exactly one variable *)
       let var =
         match vars with [ v ] -> v | _ -> raise (Failure "Unreachable")
@@ -2452,7 +2452,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_typed_pattern_from_var var None)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
+  | TAssumed (TArray | TSlice | TStr) ->
       (* We can't expand those values: we can access the fields only
        * through the functions provided by the API (note that we don't
        * know how to expand values like vectors or arrays, because they have a variable number
@@ -2484,7 +2484,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
         let values = List.map (typed_value_to_texpression ctx ectx) values in
         let values = FieldId.mapi (fun fid v -> (fid, v)) values in
         let su : struct_update =
-          { struct_id = TAssumed Array; init = None; updates = values }
+          { struct_id = TAssumed TArray; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
     | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
@@ -2735,9 +2735,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
        call to the loop forward function) *)
     let generics =
       let { types; const_generics; trait_clauses } = ctx.sg.generics in
-      let types =
-        List.map (fun (ty : T.type_var) -> TypeVar ty.T.index) types
-      in
+      let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
       let const_generics =
         List.map
           (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
-- 
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/SymbolicToPure.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 60020d9a..258b1cf2 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1149,7 +1149,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
   (* Translate the value *)
   let value =
     match v.value with
-    | V.VLiteral cv -> { e = Const cv; ty }
+    | VLiteral cv -> { e = Const cv; ty }
     | VAdt av -> (
         let variant_id = av.variant_id in
         let field_values = List.map translate av.field_values in
@@ -1173,27 +1173,27 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
             let cons = { e = cons_e; ty = cons_ty } in
             (* Apply the constructor *)
             mk_apps cons field_values)
-    | Bottom -> raise (Failure "Unreachable")
-    | Loan lc -> (
+    | VBottom -> raise (Failure "Unreachable")
+    | VLoan lc -> (
         match lc with
-        | SharedLoan (_, v) -> translate v
-        | MutLoan _ -> raise (Failure "Unreachable"))
-    | Borrow bc -> (
+        | VSharedLoan (_, v) -> translate v
+        | VMutLoan _ -> raise (Failure "Unreachable"))
+    | VBorrow bc -> (
         match bc with
-        | V.SharedBorrow bid ->
+        | VSharedBorrow bid ->
             (* Lookup the shared value in the context, and continue *)
             let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
             translate sv
-        | V.ReservedMutBorrow bid ->
+        | VReservedMutBorrow bid ->
             (* Same as for shared borrows. However, note that we use reserved borrows
              * only in *meta-data*: a value *actually used* in the translation can't come
              * from an unpromoted reserved borrow *)
             let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
             translate sv
-        | V.MutBorrow (_, v) ->
+        | VMutBorrow (_, v) ->
             (* Borrows are the identity in the extraction *)
             translate v)
-    | Symbolic sv -> symbolic_value_to_texpression ctx sv
+    | VSymbolic sv -> symbolic_value_to_texpression ctx sv
   in
   (* Debugging *)
   log#ldebug
-- 
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/SymbolicToPure.ml | 25 ++++++++++++++++++-------
 1 file changed, 18 insertions(+), 7 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 258b1cf2..922aa307 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -47,6 +47,7 @@ type fun_context = {
   llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.t;  (** *)
   fun_infos : FA.fun_info A.FunDeclId.Map.t;
+  regions_hierarchies : T.region_groups FunIdMap.t;
 }
 [@@deriving show]
 
@@ -441,8 +442,8 @@ and translate_strait_instance_id (id : T.trait_instance_id) : trait_instance_id
   translate_trait_instance_id translate_sty id
 
 let translate_trait_clause (clause : T.trait_clause) : trait_clause =
-  let { T.clause_id; meta = _; trait_id; generics } = clause in
-  let generics = translate_sgeneric_args generics in
+  let { T.clause_id; meta = _; trait_id; clause_generics } = clause in
+  let generics = translate_sgeneric_args clause_generics in
   { clause_id; trait_id; generics }
 
 let translate_strait_type_constraint (ttc : T.trait_type_constraint) :
@@ -848,11 +849,14 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   let fun_infos = decls_ctx.fun_ctx.fun_infos in
   let type_infos = decls_ctx.type_ctx.type_infos in
   (* Retrieve the list of parent backward functions *)
+  let regions_hierarchy =
+    FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies
+  in
   let gid, parents =
     match bid with
     | None -> (None, T.RegionGroupId.Set.empty)
     | Some bid ->
-        let parents = list_ancestor_region_groups sg bid in
+        let parents = list_ancestor_region_groups regions_hierarchy bid in
         (Some bid, parents)
   in
   (* Is the function stateful, and can it fail? *)
@@ -865,7 +869,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   (* Create the context *)
   let ctx =
     let region_groups =
-      List.map (fun (g : T.region_group) -> g.id) sg.regions_hierarchy
+      List.map (fun (g : T.region_group) -> g.id) regions_hierarchy
     in
     let ctx =
       InterpreterUtils.initialize_eval_context decls_ctx region_groups
@@ -898,7 +902,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   assert (T.RegionGroupId.Set.is_empty parents);
   (* Small helper to translate types for backward functions *)
   let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.ty -> ty option =
-    let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
+    let rg = T.RegionGroupId.nth regions_hierarchy gid in
     let regions = T.RegionId.Set.of_list rg.regions in
     let keep_region r =
       match r with
@@ -2924,6 +2928,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let basename = def.name in
   (* Retrieve the signature *)
   let signature = ctx.sg in
+  let regions_hierarchy =
+    FunIdMap.find (FRegular def_id) ctx.fun_context.regions_hierarchies
+  in
   (* Translate the body, if there is *)
   let body =
     match body with
@@ -2965,7 +2972,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
           | None -> []
           | Some back_id ->
               let parents_ids =
-                list_ordered_ancestor_region_groups def.signature back_id
+                list_ordered_ancestor_region_groups regions_hierarchy back_id
               in
               let backward_ids = List.append parents_ids [ back_id ] in
               List.concat
@@ -3069,6 +3076,10 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
   let translate_one (fun_id : A.fun_id) (input_names : string option list)
       (sg : A.fun_sig) : (regular_fun_id_not_loop * fun_sig_named_outputs) list
       =
+    (* Retrieve the regions hierarchy *)
+    let regions_hierarchy =
+      FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies
+    in
     (* The forward function *)
     let fwd_sg = translate_fun_sig decls_ctx fun_id sg input_names None in
     let fwd_id = (fun_id, None) in
@@ -3081,7 +3092,7 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
           in
           let id = (fun_id, Some rg.id) in
           (id, tsg))
-        sg.regions_hierarchy
+        regions_hierarchy
     in
     (* Return *)
     (fwd_id, fwd_sg) :: back_sgs
-- 
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/SymbolicToPure.ml | 214 ++++++++++++++++++++++-----------------------
 1 file changed, 107 insertions(+), 107 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 922aa307..2460e040 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2,18 +2,19 @@ open Utils
 open LlbcAstUtils
 open Pure
 open PureUtils
+open PrimitiveValues
+module T = Types
 module Id = Identifiers
 module C = Contexts
 module A = LlbcAst
 module S = SymbolicAst
 module TA = TypesAnalysis
-module L = Logging
 module PP = PrintPure
 module FA = FunsAnalysis
 module IU = InterpreterUtils
 
 (** The local logger *)
-let log = L.symbolic_to_pure_log
+let log = Logging.symbolic_to_pure_log
 
 type type_context = {
   llbc_type_decls : T.type_decl TypeDeclId.Map.t;
@@ -208,113 +209,92 @@ type bs_ctx = {
 [@@deriving show]
 
 (* TODO: move *)
-let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
-  Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
-    ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls
-    ctx.trait_decls_ctx ctx.trait_impls_ctx ctx.fun_decl
-
-let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
-  let region_id_to_string = Print.Types.region_id_to_string in
-  let type_var_id_to_string = Print.Types.type_var_id_to_string in
-  let var_id_to_string = Print.Expressions.var_id_to_string in
-  let ast_fmt = bs_ctx_to_ast_formatter ctx in
+let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
+  let type_decls = ctx.type_context.llbc_type_decls in
+  let fun_decls = ctx.fun_context.llbc_fun_decls in
+  let global_decls = ctx.global_context.llbc_global_decls in
+  let trait_decls = ctx.trait_decls_ctx in
+  let trait_impls = ctx.trait_impls_ctx in
+  let generics = ctx.fun_decl.signature.generics in
+  let preds = ctx.fun_decl.signature.preds in
   {
-    Print.Values.region_id_to_string;
-    type_var_id_to_string;
-    type_decl_id_to_string = ast_fmt.type_decl_id_to_string;
-    const_generic_var_id_to_string = ast_fmt.const_generic_var_id_to_string;
-    global_decl_id_to_string = ast_fmt.global_decl_id_to_string;
-    adt_variant_to_string = ast_fmt.adt_variant_to_string;
-    var_id_to_string;
-    adt_field_names = ast_fmt.adt_field_names;
-    trait_decl_id_to_string = ast_fmt.trait_decl_id_to_string;
-    trait_impl_id_to_string = ast_fmt.trait_impl_id_to_string;
-    trait_clause_id_to_string = ast_fmt.trait_clause_id_to_string;
+    type_decls;
+    fun_decls;
+    global_decls;
+    trait_decls;
+    trait_impls;
+    generics;
+    preds;
+    locals = [];
   }
 
-let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
-  let generics = ctx.fun_decl.signature.generics in
+let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env =
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
-  PrintPure.mk_ast_formatter type_decls fun_decls global_decls
-    ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
-    generics.const_generics
+  let trait_decls = ctx.trait_decls_ctx in
+  let trait_impls = ctx.trait_impls_ctx in
+  let generics = ctx.sg.generics in
+  {
+    type_decls;
+    fun_decls;
+    global_decls;
+    trait_decls;
+    trait_impls;
+    generics;
+    locals = [];
+  }
 
 let ctx_generic_args_to_string (ctx : bs_ctx) (args : T.generic_args) : string =
-  let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_type_formatter fmt in
-  Print.PT.generic_args_to_string fmt args
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Types.generic_args_to_string env args
+
+let name_to_string (ctx : bs_ctx) =
+  Print.Types.name_to_string (bs_ctx_to_fmt_env ctx)
 
 let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
-  let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_type_formatter fmt in
-  Print.PV.symbolic_value_to_string fmt sv
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Values.symbolic_value_to_string env sv
 
 let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
-  let fmt = bs_ctx_to_ctx_formatter ctx in
-  Print.PV.typed_value_to_string fmt v
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Values.typed_value_to_string env v
 
 let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
-  let fmt = bs_ctx_to_pp_ast_formatter ctx in
-  let fmt = PrintPure.ast_to_type_formatter fmt in
-  PrintPure.ty_to_string fmt false ty
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.ty_to_string env false ty
 
 let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string =
-  let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_type_formatter fmt in
-  Print.PT.ty_to_string fmt ty
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Types.ty_to_string env ty
 
 let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
-  let type_decls = ctx.type_context.llbc_type_decls in
-  let global_decls = ctx.global_context.llbc_global_decls in
-  let fmt =
-    PrintPure.mk_type_formatter type_decls global_decls ctx.trait_decls_ctx
-      ctx.trait_impls_ctx def.generics.types def.generics.const_generics
-  in
-  PrintPure.type_decl_to_string fmt def
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.type_decl_to_string env def
 
 let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
-  let fmt = bs_ctx_to_pp_ast_formatter ctx in
-  PrintPure.texpression_to_string fmt false "" "  " e
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.texpression_to_string env false "" "  " e
 
 let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
-  let type_params = sg.generics.types in
-  let cg_params = sg.generics.const_generics in
-  let type_decls = ctx.type_context.llbc_type_decls in
-  let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let global_decls = ctx.global_context.llbc_global_decls in
-  let fmt =
-    PrintPure.mk_ast_formatter type_decls fun_decls global_decls
-      ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
-  in
-  PrintPure.fun_sig_to_string fmt sg
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.fun_sig_to_string env sg
 
 let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
-  let generics = def.signature.generics in
-  let type_params = generics.types in
-  let cg_params = generics.const_generics in
-  let type_decls = ctx.type_context.llbc_type_decls in
-  let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let global_decls = ctx.global_context.llbc_global_decls in
-  let fmt =
-    PrintPure.mk_ast_formatter type_decls fun_decls global_decls
-      ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
-  in
-  PrintPure.fun_decl_to_string fmt def
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.fun_decl_to_string env def
 
 let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
-  let fmt = bs_ctx_to_pp_ast_formatter ctx in
-  PrintPure.typed_pattern_to_string fmt p
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.typed_pattern_to_string env p
 
 (* TODO: move *)
 let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
-  let fmt = bs_ctx_to_ast_formatter ctx in
-  let fmt = Print.Contexts.ast_to_value_formatter fmt in
+  let env = bs_ctx_to_fmt_env ctx in
   let verbose = false in
   let indent = "" in
   let indent_incr = "  " in
-  Print.Values.abs_to_string fmt verbose indent indent_incr abs
+  Print.Values.abs_to_string env verbose indent indent_incr abs
 
 let get_instantiated_fun_sig (fun_id : A.fun_id)
     (back_id : T.RegionGroupId.id option) (generics : generic_args)
@@ -421,7 +401,7 @@ let rec translate_sty (ty : T.ty) : ty =
   | TNever -> raise (Failure "Unreachable")
   | TRef (_, rty, _) -> translate rty
   | TRawPtr (ty, rkind) ->
-      let mut = match rkind with Mut -> Mut | Shared -> Const in
+      let mut = match rkind with RMut -> Mut | RShared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
       TAdt (TAssumed (TRawPtr mut), generics)
@@ -481,21 +461,24 @@ let translate_variant (v : T.variant) : variant =
 let translate_variants (vl : T.variant list) : variant list =
   List.map translate_variant vl
 
-(** Translate a type def kind to IM *)
+(** Translate a type def kind from LLBC *)
 let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
   match kind with
   | T.Struct fields -> Struct (translate_fields fields)
   | T.Enum variants -> Enum (translate_variants variants)
   | T.Opaque -> Opaque
 
-(** Translate a type definition from IM 
+(** Translate a type definition from LLBC
 
-    TODO: this is not symbolic to pure but IM to pure. Still, I don't see the
-    point of moving this definition for now.
+    Remark: this is not symbolic to pure but LLBC to pure. Still,
+    I don't see the point of moving this definition for now.
  *)
-let translate_type_decl (def : T.type_decl) : type_decl =
+let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
+    type_decl =
+  let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
   let def_id = def.T.def_id in
-  let name = def.name in
+  let llbc_name = def.name in
+  let name = Print.Types.name_to_string env def.name in
   let { T.regions; types; const_generics; trait_clauses } = def.generics in
   (* Can't translate types with regions for now *)
   assert (regions = []);
@@ -503,7 +486,7 @@ let translate_type_decl (def : T.type_decl) : type_decl =
   let generics = { types; const_generics; trait_clauses } in
   let kind = translate_type_decl_kind def.T.kind in
   let preds = translate_predicates def.preds in
-  { def_id; name; generics; kind; preds }
+  { def_id; llbc_name; name; generics; kind; preds }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -564,7 +547,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
   | TLiteral lty -> TLiteral lty
   | TRef (_, rty, _) -> translate rty
   | TRawPtr (ty, rkind) ->
-      let mut = match rkind with Mut -> Mut | Shared -> Const in
+      let mut = match rkind with RMut -> Mut | RShared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
       TAdt (TAssumed (TRawPtr mut), generics)
@@ -655,10 +638,10 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   | TLiteral lty -> wrap (TLiteral lty)
   | TRef (r, rty, rkind) -> (
       match rkind with
-      | T.Shared ->
+      | RShared ->
           (* Ignore shared references, unless we are below a mutable borrow *)
           if inside_mut then translate rty else None
-      | T.Mut ->
+      | RMut ->
           (* Dive in, remembering the fact that we are inside a mutable borrow *)
           let inside_mut = true in
           if keep_region r then
@@ -1034,7 +1017,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
       effect_info;
     }
   in
-  let preds = translate_predicates sg.A.preds in
+  let preds = translate_predicates sg.preds in
   let sg = { generics; preds; inputs; output; doutputs; info } in
   { sg; output_names }
 
@@ -1795,7 +1778,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
   log#ldebug
     (lazy
       ("translate_end_abstraction_synth_input:" ^ "\n- function: "
-      ^ Print.name_to_string ctx.fun_decl.name
+      ^ name_to_string ctx ctx.fun_decl.name
       ^ "\n- rg_id: "
       ^ T.RegionGroupId.to_string rg_id
       ^ "\n- loop_id: "
@@ -2109,7 +2092,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       (* Actually the same case as [SynthInput] *)
       translate_end_abstraction_synth_input ectx abs e ctx rg_id
   | V.LoopCall ->
-      let fun_id = E.FRegular ctx.fun_decl.A.def_id in
+      let fun_id = E.FRegular ctx.fun_decl.def_id in
       let effect_info =
         get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
           (Some vloop_id) (Some rg_id)
@@ -2336,7 +2319,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
         (* We don't need to update the context: we don't introduce any
            * new values/variables *)
         let branch = translate_expression branch_e ctx in
-        let pat = mk_typed_pattern_from_literal (PV.VScalar v) in
+        let pat = mk_typed_pattern_from_literal (VScalar v) in
         { pat; branch }
       in
       let branches = List.map translate_branch branches in
@@ -2569,7 +2552,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       let org_args = args in
 
       (* Lookup the effect info for the loop function *)
-      let fid = E.FRegular ctx.fun_decl.A.def_id in
+      let fid = E.FRegular ctx.fun_decl.def_id in
       let effect_info =
         get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
       in
@@ -2918,14 +2901,15 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   log#ldebug
     (lazy
       ("SymbolicToPure.translate_fun_decl: "
-      ^ Print.fun_name_to_string def.A.name
+      ^ name_to_string ctx def.name
       ^ " ("
       ^ Print.option_to_string T.RegionGroupId.to_string bid
       ^ ")\n"));
 
   (* Translate the declaration *)
-  let def_id = def.A.def_id in
-  let basename = def.name in
+  let def_id = def.def_id in
+  let llbc_name = def.name in
+  let name = name_to_string ctx llbc_name in
   (* Retrieve the signature *)
   let signature = ctx.sg in
   let regions_hierarchy =
@@ -2999,7 +2983,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
         log#ldebug
           (lazy
             ("SymbolicToPure.translate_fun_decl: "
-            ^ Print.fun_name_to_string def.A.name
+            ^ name_to_string ctx def.name
             ^ " ("
             ^ Print.option_to_string T.RegionGroupId.to_string bid
             ^ ")" ^ "\n- forward_inputs: "
@@ -3030,14 +3014,15 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let loop_id = None in
 
   (* Assemble the declaration *)
-  let def =
+  let def : fun_decl =
     {
       def_id;
       kind = def.kind;
       num_loops;
       loop_id;
       back_id = bid;
-      basename;
+      llbc_name;
+      name;
       signature;
       is_global_decl_body = def.is_global_decl_body;
       body;
@@ -3051,8 +3036,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   (* return *)
   def
 
-let translate_type_decls (type_decls : T.type_decl list) : type_decl list =
-  List.map translate_type_decl type_decls
+let translate_type_decls (ctx : Contexts.decls_ctx)
+    (type_decls : T.type_decl list) : type_decl list =
+  List.map (translate_type_decl ctx) type_decls
 
 (** Translates function signatures.
 
@@ -3105,11 +3091,11 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
     (fun m (id, sg) -> RegularFunIdNotLoopMap.add id sg m)
     RegularFunIdNotLoopMap.empty translated
 
-let translate_trait_decl (type_infos : TA.type_infos)
-    (trait_decl : A.trait_decl) : trait_decl =
+let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
+    : trait_decl =
   let {
     def_id;
-    name;
+    name = llbc_name;
     generics;
     preds;
     parent_clauses;
@@ -3120,6 +3106,12 @@ let translate_trait_decl (type_infos : TA.type_infos)
   } : A.trait_decl =
     trait_decl
   in
+  let type_infos = ctx.type_ctx.type_infos in
+  let name =
+    Print.Types.name_to_string
+      (Print.Contexts.decls_ctx_to_fmt_env ctx)
+      llbc_name
+  in
   let generics = translate_generic_params generics in
   let preds = translate_predicates preds in
   let parent_clauses = List.map translate_trait_clause parent_clauses in
@@ -3138,6 +3130,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
   in
   {
     def_id;
+    llbc_name;
     name;
     generics;
     preds;
@@ -3148,11 +3141,11 @@ let translate_trait_decl (type_infos : TA.type_infos)
     provided_methods;
   }
 
-let translate_trait_impl (type_infos : TA.type_infos)
-    (trait_impl : A.trait_impl) : trait_impl =
+let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
+    : trait_impl =
   let {
     A.def_id;
-    name;
+    name = llbc_name;
     impl_trait;
     generics;
     preds;
@@ -3164,9 +3157,15 @@ let translate_trait_impl (type_infos : TA.type_infos)
   } =
     trait_impl
   in
+  let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
     translate_trait_decl_ref (translate_fwd_ty type_infos) impl_trait
   in
+  let name =
+    Print.Types.name_to_string
+      (Print.Contexts.decls_ctx_to_fmt_env ctx)
+      llbc_name
+  in
   let generics = translate_generic_params generics in
   let preds = translate_predicates preds in
   let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in
@@ -3185,6 +3184,7 @@ let translate_trait_impl (type_infos : TA.type_infos)
   in
   {
     def_id;
+    llbc_name;
     name;
     impl_trait;
     generics;
-- 
cgit v1.2.3


From a27efd1ed08bc9583752445d9eda7a693c0c7379 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 16 Nov 2023 10:13:28 +0100
Subject: Finish propagating the changes to the names and cleaning

---
 compiler/SymbolicToPure.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2460e040..4e12d31e 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3036,9 +3036,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   (* return *)
   def
 
-let translate_type_decls (ctx : Contexts.decls_ctx)
-    (type_decls : T.type_decl list) : type_decl list =
-  List.map (translate_type_decl ctx) type_decls
+let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
+  List.map (translate_type_decl ctx)
+    (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
 (** Translates function signatures.
 
-- 
cgit v1.2.3


From 0757cdee8c6b8a8020d4b96a44a3017944c9a808 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 16 Nov 2023 10:57:08 +0100
Subject: Do more cleanup

---
 compiler/SymbolicToPure.ml | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4e12d31e..7dad54e1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3,6 +3,9 @@ open LlbcAstUtils
 open Pure
 open PureUtils
 open PrimitiveValues
+open InterpreterUtils
+open FunsAnalysis
+open TypesAnalysis
 module T = Types
 module Id = Identifiers
 module C = Contexts
@@ -10,8 +13,6 @@ module A = LlbcAst
 module S = SymbolicAst
 module TA = TypesAnalysis
 module PP = PrintPure
-module FA = FunsAnalysis
-module IU = InterpreterUtils
 
 (** The local logger *)
 let log = Logging.symbolic_to_pure_log
@@ -24,7 +25,7 @@ type type_context = {
           This map is empty when we translate the types, then contains all
           the translated types when we translate the functions.
        *)
-  type_infos : TA.type_infos;
+  type_infos : type_infos;
   recursive_decls : T.TypeDeclId.Set.t;
 }
 [@@deriving show]
@@ -47,7 +48,7 @@ type fun_sig_named_outputs = {
 type fun_context = {
   llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.t;  (** *)
-  fun_infos : FA.fun_info A.FunDeclId.Map.t;
+  fun_infos : fun_info A.FunDeclId.Map.t;
   regions_hierarchies : T.region_groups FunIdMap.t;
 }
 [@@deriving show]
@@ -513,7 +514,7 @@ let translate_type_id (id : T.type_id) : type_id =
 
     TODO: factor out the various translation functions.
 *)
-let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
+let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty =
   let translate = translate_fwd_ty type_infos in
   match ty with
   | T.TAdt (type_id, generics) -> (
@@ -557,15 +558,15 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
       TTraitType (trait_ref, generics, type_name)
   | TArrow _ -> raise (Failure "TODO")
 
-and translate_fwd_generic_args (type_infos : TA.type_infos)
+and translate_fwd_generic_args (type_infos : type_infos)
     (generics : T.generic_args) : generic_args =
   translate_generic_args (translate_fwd_ty type_infos) generics
 
-and translate_fwd_trait_ref (type_infos : TA.type_infos) (tr : T.trait_ref) :
+and translate_fwd_trait_ref (type_infos : type_infos) (tr : T.trait_ref) :
     trait_ref =
   translate_trait_ref (translate_fwd_ty type_infos) tr
 
-and translate_fwd_trait_instance_id (type_infos : TA.type_infos)
+and translate_fwd_trait_instance_id (type_infos : type_infos)
     (id : T.trait_instance_id) : trait_instance_id =
   translate_trait_instance_id (translate_fwd_ty type_infos) id
 
@@ -586,7 +587,7 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
     
     [inside_mut]: are we inside a mutable borrow?
  *)
-let rec translate_back_ty (type_infos : TA.type_infos)
+let rec translate_back_ty (type_infos : type_infos)
     (keep_region : T.region -> bool) (inside_mut : bool) (ty : T.ty) : ty option
     =
   let translate = translate_back_ty type_infos keep_region inside_mut in
@@ -791,7 +792,7 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) :
   if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else []
 
 (** Small utility. *)
-let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
+let get_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with
@@ -1783,8 +1784,8 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
       ^ T.RegionGroupId.to_string rg_id
       ^ "\n- loop_id: "
       ^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id
-      ^ "\n- eval_ctx:\n" ^ IU.eval_ctx_to_string ectx ^ "\n- abs:\n"
-      ^ IU.abs_to_string ectx abs ^ "\n"));
+      ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ectx ^ "\n- abs:\n"
+      ^ abs_to_string ctx abs ^ "\n"));
 
   (* When we end an input abstraction, this input abstraction gets back
    * the borrows which it introduced in the context through the input
-- 
cgit v1.2.3


From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 20 Nov 2023 21:58:25 +0100
Subject: Use the name matcher implemented in Charon

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

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7dad54e1..69ff4df1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2475,7 +2475,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
           { struct_id = TAssumed TArray; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
-    | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
     | VaTraitConstValue (trait_ref, generics, const_name) ->
         let type_infos = ctx.type_context.type_infos in
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
@@ -2726,7 +2726,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
       let const_generics =
         List.map
-          (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
+          (fun (cg : T.const_generic_var) -> T.CgVar cg.T.index)
           const_generics
       in
       let trait_refs =
-- 
cgit v1.2.3


From 00882b8fe6d8ef1d9b7a03cd5949f909d58a2da9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 11:30:43 +0100
Subject: Make a minor modification

---
 compiler/SymbolicToPure.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 69ff4df1..6983a0e8 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -269,7 +269,11 @@ let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string =
   let env = bs_ctx_to_fmt_env ctx in
   Print.Types.ty_to_string env ty
 
-let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
+let type_decl_to_string (ctx : bs_ctx) (def : T.type_decl) : string =
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Types.type_decl_to_string env def
+
+let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
   let env = bs_ctx_to_pure_fmt_env ctx in
   PrintPure.type_decl_to_string env def
 
@@ -476,6 +480,12 @@ let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
  *)
 let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
     type_decl =
+  log#ldebug
+    (lazy
+      (let ctx = Print.Contexts.decls_ctx_to_fmt_env ctx in
+       "translate_type_decl:\n\n"
+       ^ Print.Types.type_decl_to_string ctx def
+       ^ "\n"));
   let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
   let def_id = def.T.def_id in
   let llbc_name = def.name in
-- 
cgit v1.2.3


From f852e1a1334b7506c0baf366b9e75cd01b9c843e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 12:15:37 +0100
Subject: Rename PrimitiveValues to Values

---
 compiler/SymbolicToPure.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6983a0e8..f25ff2f6 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2,16 +2,14 @@ open Utils
 open LlbcAstUtils
 open Pure
 open PureUtils
-open PrimitiveValues
 open InterpreterUtils
 open FunsAnalysis
 open TypesAnalysis
 module T = Types
-module Id = Identifiers
+module V = Values
 module C = Contexts
 module A = LlbcAst
 module S = SymbolicAst
-module TA = TypesAnalysis
 module PP = PrintPure
 
 (** The local logger *)
-- 
cgit v1.2.3


From e94cd72ffa63dbc5fc40c7c1a422c1a70ba4a7e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 13:55:46 +0100
Subject: Add an `is_local` field to declarations

---
 compiler/SymbolicToPure.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index f25ff2f6..9899a0c6 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -495,7 +495,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let generics = { types; const_generics; trait_clauses } in
   let kind = translate_type_decl_kind def.T.kind in
   let preds = translate_predicates def.preds in
-  { def_id; llbc_name; name; generics; kind; preds }
+  let is_local = def.is_local in
+  { def_id; is_local; llbc_name; name; generics; kind; preds }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -3026,6 +3027,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let def : fun_decl =
     {
       def_id;
+      is_local = def.is_local;
       kind = def.kind;
       num_loops;
       loop_id;
@@ -3104,6 +3106,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     : trait_decl =
   let {
     def_id;
+    is_local;
     name = llbc_name;
     generics;
     preds;
@@ -3139,6 +3142,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
   in
   {
     def_id;
+    is_local;
     llbc_name;
     name;
     generics;
@@ -3154,6 +3158,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     : trait_impl =
   let {
     A.def_id;
+    is_local;
     name = llbc_name;
     impl_trait;
     generics;
@@ -3193,6 +3198,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   in
   {
     def_id;
+    is_local;
     llbc_name;
     name;
     impl_trait;
-- 
cgit v1.2.3


From 77ba13b371cccbe8098e432ebd287108d5373666 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 14:43:12 +0100
Subject: Add span information to the generated code

---
 compiler/SymbolicToPure.ml | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 9899a0c6..5dee23db 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -496,7 +496,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let kind = translate_type_decl_kind def.T.kind in
   let preds = translate_predicates def.preds in
   let is_local = def.is_local in
-  { def_id; is_local; llbc_name; name; generics; kind; preds }
+  let meta = def.meta in
+  { def_id; is_local; llbc_name; name; meta; generics; kind; preds }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -1489,11 +1490,11 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
   (call_info.forward, abs_ancestors)
 
 (** Add meta-information to an expression *)
-let mk_meta_symbolic_assignments (vars : var list) (values : texpression list)
+let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list)
     (e : texpression) : texpression =
   let var_values = List.combine vars values in
   List.fold_right
-    (fun (var, arg) e -> mk_meta (SymbolicAssignment (var_get_id var, arg)) e)
+    (fun (var, arg) e -> mk_emeta (SymbolicAssignment (var_get_id var, arg)) e)
     var_values e
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -1509,7 +1510,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
   | IntroSymbolic (ectx, p, sv, v, e) ->
       translate_intro_symbolic ectx p sv v e ctx
-  | Meta (meta, e) -> translate_meta meta e ctx
+  | Meta (meta, e) -> translate_emeta meta e ctx
   | ForwardEnd (ectx, loop_input_values, e, back_e) ->
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
@@ -2206,7 +2207,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
                 var_values
             in
             let vars, values = List.split var_values in
-            mk_meta_symbolic_assignments vars values next_e
+            mk_emeta_symbolic_assignments vars values next_e
           else next_e
         in
 
@@ -2637,7 +2638,7 @@ and translate_forward_end (ectx : C.eval_ctx)
          We then remove all the meta information from the body *before* calling
          {!PureMicroPasses.decompose_loops}.
       *)
-      mk_meta_symbolic_assignments loop_info.input_vars org_args e
+      mk_emeta_symbolic_assignments loop_info.input_vars org_args e
 
 and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in
@@ -2795,6 +2796,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       {
         fun_end;
         loop_id;
+        meta = loop.meta;
         fuel0 = ctx.fuel0;
         fuel = ctx.fuel;
         input_state;
@@ -2810,7 +2812,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let ty = fun_end.ty in
   { e = loop; ty }
 
-and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
+and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) :
     texpression =
   let next_e = translate_expression e ctx in
   let meta =
@@ -3028,6 +3030,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     {
       def_id;
       is_local = def.is_local;
+      meta = def.meta;
       kind = def.kind;
       num_loops;
       loop_id;
@@ -3108,6 +3111,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     def_id;
     is_local;
     name = llbc_name;
+    meta;
     generics;
     preds;
     parent_clauses;
@@ -3145,6 +3149,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     is_local;
     llbc_name;
     name;
+    meta;
     generics;
     preds;
     parent_clauses;
@@ -3160,6 +3165,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     A.def_id;
     is_local;
     name = llbc_name;
+    meta;
     impl_trait;
     generics;
     preds;
@@ -3201,6 +3207,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     is_local;
     llbc_name;
     name;
+    meta;
     impl_trait;
     generics;
     preds;
-- 
cgit v1.2.3


From ba66f35a0e196c17757e06187cf2563abec253e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 22 Nov 2023 09:09:46 +0100
Subject: Improve further the generation of parent clause/trait clause names

---
 compiler/SymbolicToPure.ml | 44 ++++++++++++++++++++++++++++++++++----------
 1 file changed, 34 insertions(+), 10 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 5dee23db..4df3ee73 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -497,7 +497,17 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let preds = translate_predicates def.preds in
   let is_local = def.is_local in
   let meta = def.meta in
-  { def_id; is_local; llbc_name; name; meta; generics; kind; preds }
+  {
+    def_id;
+    is_local;
+    llbc_name;
+    name;
+    meta;
+    generics;
+    llbc_generics = def.generics;
+    kind;
+    preds;
+  }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -1029,7 +1039,17 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
     }
   in
   let preds = translate_predicates sg.preds in
-  let sg = { generics; preds; inputs; output; doutputs; info } in
+  let sg =
+    {
+      generics;
+      llbc_generics = sg.generics;
+      preds;
+      inputs;
+      output;
+      doutputs;
+      info;
+    }
+  in
   { sg; output_names }
 
 let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
@@ -3112,9 +3132,9 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     is_local;
     name = llbc_name;
     meta;
-    generics;
+    generics = llbc_generics;
     preds;
-    parent_clauses;
+    parent_clauses = llbc_parent_clauses;
     consts;
     types;
     required_methods;
@@ -3128,9 +3148,9 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics = translate_generic_params generics in
+  let generics = translate_generic_params llbc_generics in
   let preds = translate_predicates preds in
-  let parent_clauses = List.map translate_trait_clause parent_clauses in
+  let parent_clauses = List.map translate_trait_clause llbc_parent_clauses in
   let consts =
     List.map
       (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
@@ -3151,8 +3171,10 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     name;
     meta;
     generics;
+    llbc_generics;
     preds;
     parent_clauses;
+    llbc_parent_clauses;
     consts;
     types;
     required_methods;
@@ -3166,8 +3188,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     is_local;
     name = llbc_name;
     meta;
-    impl_trait;
-    generics;
+    impl_trait = llbc_impl_trait;
+    generics = llbc_generics;
     preds;
     parent_trait_refs;
     consts;
@@ -3179,14 +3201,14 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   in
   let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
-    translate_trait_decl_ref (translate_fwd_ty type_infos) impl_trait
+    translate_trait_decl_ref (translate_fwd_ty type_infos) llbc_impl_trait
   in
   let name =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics = translate_generic_params generics in
+  let generics = translate_generic_params llbc_generics in
   let preds = translate_predicates preds in
   let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in
   let consts =
@@ -3209,7 +3231,9 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     name;
     meta;
     impl_trait;
+    llbc_impl_trait;
     generics;
+    llbc_generics;
     preds;
     parent_trait_refs;
     consts;
-- 
cgit v1.2.3