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/Substitute.ml | 443 +++++++++++++++++++++++++++++--------------------
 1 file changed, 260 insertions(+), 183 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 38850243..64e7716a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -9,51 +9,53 @@ module E = Expressions
 module A = LlbcAst
 module C = Contexts
 
-(** Substitute types variables and regions in a type. *)
-let ty_substitute (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : 'r1 T.ty) :
-    'r2 T.ty =
-  let open T in
-  let visitor =
-    object
-      inherit [_] map_ty
-      method visit_'r _ r = rsubst r
-      method! visit_TypeVar _ id = tsubst id
-
-      method! visit_type_var_id _ _ =
-        (* We should never get here because we reimplemented [visit_TypeVar] *)
-        raise (Failure "Unexpected")
+type ('r1, 'r2) subst = {
+  r_subst : 'r1 -> 'r2;
+  ty_subst : T.TypeVarId.id -> 'r2 T.ty;
+  cg_subst : T.ConstGenericVarId.id -> T.const_generic;
+      (** Substitution from *local* trait clause to trait instance *)
+  tr_subst : T.TraitClauseId.id -> 'r2 T.trait_instance_id;
+      (** Substitution for the [Self] trait instance *)
+  tr_self : 'r2 T.trait_instance_id;
+}
+
+let ty_substitute_visitor (subst : ('r1, 'r2) subst) =
+  object
+    inherit [_] T.map_ty
+    method visit_'r _ r = subst.r_subst r
+    method! visit_TypeVar _ id = subst.ty_subst id
 
-      method! visit_ConstGenericVar _ id = cgsubst id
+    method! visit_type_var_id _ _ =
+      (* We should never get here because we reimplemented [visit_TypeVar] *)
+      raise (Failure "Unexpected")
 
-      method! visit_const_generic_var_id _ _ =
-        (* We should never get here because we reimplemented [visit_Var] *)
-        raise (Failure "Unexpected")
-    end
-  in
+    method! visit_ConstGenericVar _ id = subst.cg_subst id
 
-  visitor#visit_ty () ty
+    method! visit_const_generic_var_id _ _ =
+      (* We should never get here because we reimplemented [visit_Var] *)
+      raise (Failure "Unexpected")
 
-let rty_substitute (rsubst : T.RegionId.id -> T.RegionId.id)
-    (tsubst : T.TypeVarId.id -> T.rty)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : T.rty) : T.rty =
-  let rsubst r =
-    match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
-  in
-  ty_substitute rsubst tsubst cgsubst ty
+    method! visit_Clause _ id = subst.tr_subst id
+    method! visit_Self _ = subst.tr_self
+  end
 
-let ety_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : T.ety) : T.ety =
-  let rsubst r = r in
-  ty_substitute rsubst tsubst cgsubst ty
+(** Substitute types variables and regions in a type. *)
+let ty_substitute (subst : ('r1, 'r2) subst) (ty : 'r1 T.ty) : 'r2 T.ty =
+  let visitor = ty_substitute_visitor subst in
+  visitor#visit_ty () ty
 
 (** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
 let erase_regions (ty : T.rty) : T.ety =
-  ty_substitute
-    (fun _ -> T.Erased)
-    (fun vid -> T.TypeVar vid)
-    (fun id -> T.ConstGenericVar id)
-    ty
+  let subst =
+    {
+      r_subst = (fun _ -> T.Erased);
+      ty_subst = (fun vid -> T.TypeVar vid);
+      cg_subst = (fun id -> T.ConstGenericVar id);
+      tr_subst = (fun id -> T.Clause id);
+      tr_self = T.Self;
+    }
+  in
+  ty_substitute subst ty
 
 (** Generate fresh regions for region variables.
 
@@ -78,18 +80,20 @@ let fresh_regions_with_substs (region_vars : T.region_var list) :
   (* Generate the substitution from region var id to region *)
   let rid_subst id = T.RegionVarId.Map.find id rid_map in
   (* Generate the substitution from region to region *)
-  let rsubst r =
+  let r_subst r =
     match r with T.Static -> T.Static | T.Var id -> T.Var (rid_subst id)
   in
   (* Return *)
-  (fresh_region_ids, rid_subst, rsubst)
+  (fresh_region_ids, rid_subst, r_subst)
 
-(** Erase the regions in a type and substitute the type variables *)
-let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic)
-    (ty : 'r T.region T.ty) : T.ety =
-  let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in
-  ty_substitute rsubst tsubst cgsubst ty
+(** Erase the regions in a type and perform a substitution *)
+let erase_regions_substitute_types (ty_subst : T.TypeVarId.id -> T.ety)
+    (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
+    (tr_subst : T.TraitClauseId.id -> T.etrait_instance_id)
+    (tr_self : T.etrait_instance_id) (ty : 'r T.ty) : T.ety =
+  let r_subst (_ : 'r) : T.erased_region = T.Erased in
+  let subst = { r_subst; ty_subst; cg_subst; tr_subst; tr_self } in
+  ty_substitute subst ty
 
 (** Create a region substitution from a list of region variable ids and a list of
     regions (with which to substitute the region variable ids *)
@@ -146,16 +150,62 @@ let make_const_generic_subst_from_vars (vars : T.const_generic_var list)
     (List.map (fun (x : T.const_generic_var) -> x.T.index) vars)
     cgs
 
-(** Instantiate the type variables in an ADT definition, and return, for
-    every variant, the list of the types of its fields *)
-let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (cgs : T.const_generic list) : (T.VariantId.id option * T.rty list) list =
-  let r_subst = make_region_subst_from_vars def.T.region_params regions in
-  let ty_subst = make_type_subst_from_vars def.T.type_params types in
+(** Create a trait substitution from a list of trait clause ids and a list of
+    trait refs *)
+let make_trait_subst (clause_ids : T.TraitClauseId.id list)
+    (trs : 'r T.trait_ref list) : T.TraitClauseId.id -> 'r T.trait_instance_id =
+  let ls = List.combine clause_ids trs in
+  let mp =
+    List.fold_left
+      (fun mp (k, v) -> T.TraitClauseId.Map.add k (T.TraitRef v) mp)
+      T.TraitClauseId.Map.empty ls
+  in
+  fun id -> T.TraitClauseId.Map.find id mp
+
+let make_trait_subst_from_clauses (clauses : T.trait_clause list)
+    (trs : 'r T.trait_ref list) : T.TraitClauseId.id -> 'r T.trait_instance_id =
+  make_trait_subst
+    (List.map (fun (x : T.trait_clause) -> x.T.clause_id) clauses)
+    trs
+
+let make_subst_from_generics (params : T.generic_params)
+    (args : 'r T.generic_args) (tr_self : 'r T.trait_instance_id) :
+    (T.region_var_id T.region, 'r) subst =
+  let r_subst = make_region_subst_from_vars params.T.regions args.T.regions in
+  let ty_subst = make_type_subst_from_vars params.T.types args.T.types in
+  let cg_subst =
+    make_const_generic_subst_from_vars params.T.const_generics
+      args.T.const_generics
+  in
+  let tr_subst =
+    make_trait_subst_from_clauses params.T.trait_clauses args.T.trait_refs
+  in
+  { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
+
+let make_esubst_from_generics (params : T.generic_params)
+    (generics : T.egeneric_args) (tr_self : T.etrait_instance_id) =
+  let r_subst _ = T.Erased in
+  let ty_subst = make_type_subst_from_vars params.types generics.T.types in
   let cg_subst =
-    make_const_generic_subst_from_vars def.T.const_generic_params cgs
+    make_const_generic_subst_from_vars params.const_generics
+      generics.T.const_generics
   in
+  let tr_subst =
+    make_trait_subst_from_clauses params.trait_clauses generics.T.trait_refs
+  in
+  { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
+
+(** Instantiate the type variables in an ADT definition, and return, for
+    every variant, the list of the types of its fields.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+*)
+let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
+    (generics : T.rgeneric_args) : (T.VariantId.id option * T.rty list) list =
+  (* There shouldn't be any reference to Self *)
+  let tr_self = T.UnknownTrait __FUNCTION__ in
+  let subst = make_subst_from_generics def.T.generics generics tr_self in
   let (variants_fields : (T.VariantId.id option * T.field list) list) =
     match def.T.kind with
     | T.Enum variants ->
@@ -171,191 +221,218 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
   in
   List.map
     (fun (id, fields) ->
-      ( id,
-        List.map
-          (fun f -> ty_substitute r_subst ty_subst cg_subst f.T.field_ty)
-          fields ))
+      (id, List.map (fun f -> ty_substitute subst f.T.field_ty) fields))
     variants_fields
 
 (** Instantiate the type variables in an ADT definition, and return the list
-    of types of the fields for the chosen variant *)
+    of types of the fields for the chosen variant.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+*)
 let type_decl_get_instantiated_field_rtypes (def : T.type_decl)
-    (opt_variant_id : T.VariantId.id option)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (cgs : T.const_generic list) : T.rty list =
-  let r_subst = make_region_subst_from_vars def.T.region_params regions in
-  let ty_subst = make_type_subst_from_vars def.T.type_params types in
-  let cg_subst =
-    make_const_generic_subst_from_vars def.T.const_generic_params cgs
-  in
+    (opt_variant_id : T.VariantId.id option) (generics : T.rgeneric_args) :
+    T.rty list =
+  (* For now, check that there are no clauses - otherwise we might need
+     to normalize the types *)
+  assert (def.generics.trait_clauses = []);
+  (* There shouldn't be any reference to Self *)
+  let tr_self = T.UnknownTrait __FUNCTION__ in
+  let subst = make_subst_from_generics def.T.generics generics tr_self in
   let fields = TU.type_decl_get_fields def opt_variant_id in
-  List.map
-    (fun f -> ty_substitute r_subst ty_subst cg_subst f.T.field_ty)
-    fields
+  List.map (fun f -> ty_substitute subst f.T.field_ty) fields
 
 (** Return the types of the properly instantiated ADT's variant, provided a
-    context *)
+    context.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+*)
 let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx)
     (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (cgs : T.const_generic list) : T.rty list =
+    (generics : T.rgeneric_args) : T.rty list =
   let def = C.ctx_lookup_type_decl ctx def_id in
-  type_decl_get_instantiated_field_rtypes def opt_variant_id regions types cgs
+  type_decl_get_instantiated_field_rtypes def opt_variant_id generics
 
 (** Return the types of the properly instantiated ADT value (note that
-    here, ADT is understood in its broad meaning: ADT, assumed value or tuple) *)
+    here, ADT is understood in its broad meaning: ADT, assumed value or tuple).
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+ *)
 let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
-    (adt : V.adt_value) (id : T.type_id)
-    (region_params : T.RegionId.id T.region list) (type_params : T.rty list)
-    (cg_params : T.const_generic list) : T.rty list =
+    (adt : V.adt_value) (id : T.type_id) (generics : T.rgeneric_args) :
+    T.rty list =
   match id with
   | T.AdtId id ->
       (* Retrieve the types of the fields *)
-      ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id
-        region_params type_params cg_params
+      ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id generics
   | T.Tuple ->
-      assert (List.length region_params = 0);
-      type_params
+      assert (generics.regions = []);
+      generics.types
   | T.Assumed aty -> (
       match aty with
       | T.Box | T.Vec ->
-          assert (List.length region_params = 0);
-          assert (List.length type_params = 1);
-          assert (List.length cg_params = 0);
-          type_params
+          assert (generics.regions = []);
+          assert (List.length generics.types = 1);
+          assert (generics.const_generics = []);
+          generics.types
       | T.Option ->
-          assert (List.length region_params = 0);
-          assert (List.length type_params = 1);
-          assert (List.length cg_params = 0);
-          if adt.V.variant_id = Some T.option_some_id then type_params
+          assert (generics.regions = []);
+          assert (List.length generics.types = 1);
+          assert (generics.const_generics = []);
+          if adt.V.variant_id = Some T.option_some_id then generics.types
           else if adt.V.variant_id = Some T.option_none_id then []
           else raise (Failure "Unreachable")
       | T.Range ->
-          assert (List.length region_params = 0);
-          assert (List.length type_params = 1);
-          assert (List.length cg_params = 0);
-          type_params
+          assert (generics.regions = []);
+          assert (List.length generics.types = 1);
+          assert (generics.const_generics = []);
+          generics.types
       | T.Array | T.Slice | T.Str ->
           (* Those types don't have fields *)
           raise (Failure "Unreachable"))
 
 (** Instantiate the type variables in an ADT definition, and return the list
-    of types of the fields for the chosen variant *)
+    of types of the fields for the chosen variant.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+*)
 let type_decl_get_instantiated_field_etypes (def : T.type_decl)
-    (opt_variant_id : T.VariantId.id option) (types : T.ety list)
-    (cgs : T.const_generic list) : T.ety list =
-  let ty_subst = make_type_subst_from_vars def.T.type_params types in
-  let cg_subst =
-    make_const_generic_subst_from_vars def.T.const_generic_params cgs
+    (opt_variant_id : T.VariantId.id option) (generics : T.egeneric_args) :
+    T.ety list =
+  (* For now, check that there are no clauses - otherwise we might need
+     to normalize the types *)
+  assert (def.generics.trait_clauses = []);
+  (* There shouldn't be any reference to Self *)
+  let tr_self : T.erased_region T.trait_instance_id =
+    T.UnknownTrait __FUNCTION__
+  in
+  let { r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
+    make_esubst_from_generics def.T.generics generics tr_self
   in
   let fields = TU.type_decl_get_fields def opt_variant_id in
   List.map
-    (fun f -> erase_regions_substitute_types ty_subst cg_subst f.T.field_ty)
+    (fun (f : T.field) ->
+      erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
+        f.T.field_ty)
     fields
 
 (** Return the types of the properly instantiated ADT's variant, provided a
-    context *)
+    context.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+ *)
 let ctx_adt_get_instantiated_field_etypes (ctx : C.eval_ctx)
     (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (types : T.ety list) (cgs : T.const_generic list) : T.ety list =
+    (generics : T.egeneric_args) : T.ety list =
   let def = C.ctx_lookup_type_decl ctx def_id in
-  type_decl_get_instantiated_field_etypes def opt_variant_id types cgs
+  type_decl_get_instantiated_field_etypes def opt_variant_id generics
 
-let statement_substitute_visitor (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) =
+let statement_substitute_visitor
+    (subst : (T.erased_region, T.erased_region) subst) =
+  (* Keep in synch with [ty_substitute_visitor] *)
   object
     inherit [_] A.map_statement
-    method! visit_ety _ ty = ety_substitute tsubst cgsubst ty
-    method! visit_ConstGenericVar _ id = cgsubst id
+    method! visit_'r _ r = subst.r_subst r
+    method! visit_TypeVar _ id = subst.ty_subst id
+
+    method! visit_type_var_id _ _ =
+      (* We should never get here because we reimplemented [visit_TypeVar] *)
+      raise (Failure "Unexpected")
+
+    method! visit_ConstGenericVar _ id = subst.cg_subst id
 
     method! visit_const_generic_var_id _ _ =
       (* We should never get here because we reimplemented [visit_Var] *)
       raise (Failure "Unexpected")
+
+    method! visit_Clause _ id = subst.tr_subst id
+    method! visit_Self _ = subst.tr_self
   end
 
 (** Apply a type substitution to a place *)
-let place_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (p : E.place) :
-    E.place =
+let place_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (p : E.place) : E.place =
   (* There is in fact nothing to do *)
-  (statement_substitute_visitor tsubst cgsubst)#visit_place () p
+  (statement_substitute_visitor subst)#visit_place () p
 
 (** Apply a type substitution to an operand *)
-let operand_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (op : E.operand) :
-    E.operand =
-  (statement_substitute_visitor tsubst cgsubst)#visit_operand () op
+let operand_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (op : E.operand) : E.operand =
+  (statement_substitute_visitor subst)#visit_operand () op
 
 (** Apply a type substitution to an rvalue *)
-let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (rv : E.rvalue) :
-    E.rvalue =
-  (statement_substitute_visitor tsubst cgsubst)#visit_rvalue () rv
+let rvalue_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (rv : E.rvalue) : E.rvalue =
+  (statement_substitute_visitor subst)#visit_rvalue () rv
 
 (** Apply a type substitution to an assertion *)
-let assertion_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (a : A.assertion) :
-    A.assertion =
-  (statement_substitute_visitor tsubst cgsubst)#visit_assertion () a
+let assertion_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (a : A.assertion) : A.assertion =
+  (statement_substitute_visitor subst)#visit_assertion () a
 
 (** Apply a type substitution to a call *)
-let call_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (call : A.call) :
-    A.call =
-  (statement_substitute_visitor tsubst cgsubst)#visit_call () call
+let call_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (call : A.call) : A.call =
+  (statement_substitute_visitor subst)#visit_call () call
 
 (** Apply a type substitution to a statement *)
-let statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (st : A.statement) :
-    A.statement =
-  (statement_substitute_visitor tsubst cgsubst)#visit_statement () st
+let statement_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (st : A.statement) : A.statement =
+  (statement_substitute_visitor subst)#visit_statement () st
 
 (** Apply a type substitution to a function body. Return the local variables
     and the body. *)
-let fun_body_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (body : A.fun_body) :
+let fun_body_substitute_in_body
+    (subst : (T.erased_region, T.erased_region) subst) (body : A.fun_body) :
     A.var list * A.statement =
-  let rsubst r = r in
   let locals =
     List.map
-      (fun (v : A.var) ->
-        { v with A.var_ty = ty_substitute rsubst tsubst cgsubst v.A.var_ty })
+      (fun (v : A.var) -> { v with A.var_ty = ty_substitute subst v.A.var_ty })
       body.A.locals
   in
-  let body = statement_substitute tsubst cgsubst body.body in
+  let body = statement_substitute subst body.body in
   (locals, body)
 
-(** Substitute a function signature *)
+(** Substitute a function signature.
+
+    **IMPORTANT:** this function doesn't normalize the types.
+ *)
 let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
-    (rsubst : T.RegionVarId.id -> T.RegionId.id)
-    (tsubst : T.TypeVarId.id -> T.rty)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (sg : A.fun_sig) :
-    A.inst_fun_sig =
-  let rsubst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
-    match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
+    (r_subst : T.RegionVarId.id -> T.RegionId.id)
+    (ty_subst : T.TypeVarId.id -> T.rty)
+    (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
+    (tr_subst : T.TraitClauseId.id -> T.rtrait_instance_id)
+    (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+  let r_subst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
+    match r with T.Static -> T.Static | T.Var rid -> T.Var (r_subst rid)
   in
-  let inputs = List.map (ty_substitute rsubst' tsubst cgsubst) sg.A.inputs in
-  let output = ty_substitute rsubst' tsubst cgsubst sg.A.output in
+  let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in
+  let inputs = List.map (ty_substitute subst) sg.A.inputs in
+  let output = ty_substitute subst sg.A.output in
   let subst_region_group (rg : T.region_var_group) : A.abs_region_group =
     let id = asubst rg.id in
-    let regions = List.map rsubst rg.regions in
+    let regions = List.map r_subst rg.regions in
     let parents = List.map asubst rg.parents in
     { id; regions; parents }
   in
   let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
   { A.regions_hierarchy; inputs; output }
 
-(** Substitute type variable identifiers in a type *)
-let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : 'r T.ty)
+(** Substitute variable identifiers in a type *)
+let ty_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : 'r T.ty)
     : 'r T.ty =
   let open T in
   let visitor =
     object
       inherit [_] map_ty
       method visit_'r _ r = r
-      method! visit_type_var_id _ id = tsubst id
-      method! visit_const_generic_var_id _ id = cgsubst id
+      method! visit_type_var_id _ id = ty_subst id
+      method! visit_const_generic_var_id _ id = cg_subst id
     end
   in
 
@@ -371,10 +448,10 @@ let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
    [visit_'r] if we define a class which visits objects of types [ety] and [rty]
    while inheriting a class which visit [ty]...
 *)
-let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
+let subst_ids_visitor (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) =
@@ -383,10 +460,10 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
       inherit [_] T.map_ty
 
       method visit_'r _ r =
-        match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
+        match r with T.Static -> T.Static | T.Var rid -> T.Var (r_subst rid)
 
-      method! visit_type_var_id _ id = tsubst id
-      method! visit_const_generic_var_id _ id = cgsubst id
+      method! visit_type_var_id _ id = ty_subst id
+      method! visit_const_generic_var_id _ id = cg_subst id
     end
   in
 
@@ -395,7 +472,7 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
       inherit [_] C.map_env
       method! visit_borrow_id _ bid = bsubst bid
       method! visit_loan_id _ bid = bsubst bid
-      method! visit_ety _ ty = ty_substitute_ids tsubst cgsubst ty
+      method! visit_ety _ ty = ty_substitute_ids ty_subst cg_subst ty
       method! visit_rty env ty = subst_rty#visit_ty env ty
       method! visit_symbolic_value_id _ id = ssubst id
 
@@ -405,7 +482,7 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
       (** We *do* visit meta-values *)
       method! visit_mvalue env v = self#visit_typed_value env v
 
-      method! visit_region_id _ id = rsubst id
+      method! visit_region_id _ id = r_subst id
       method! visit_region_var_id _ id = rvsubst id
       method! visit_abstraction_id _ id = asubst id
     end
@@ -425,20 +502,20 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
     method visit_env (env : C.env) : C.env = visitor#visit_env () env
   end
 
-let typed_value_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+let typed_value_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_value) :
     V.typed_value =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
     #visit_typed_value v
 
-let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
+let typed_value_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
     (v : V.typed_value) : V.typed_value =
-  typed_value_subst_ids rsubst
+  typed_value_subst_ids r_subst
     (fun x -> x)
     (fun x -> x)
     (fun x -> x)
@@ -446,41 +523,41 @@ let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
     (fun x -> x)
     v
 
-let typed_avalue_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+let typed_avalue_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_avalue) :
     V.typed_avalue =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
     #visit_typed_avalue v
 
-let abs_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+let abs_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : V.abs) : V.abs =
-  (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
     #visit_abs x
 
-let env_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+let env_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : C.env) : C.env =
-  (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
     #visit_env x
 
-let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
+let typed_avalue_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
     (x : V.typed_avalue) : V.typed_avalue =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor rsubst
+  (subst_ids_visitor r_subst
      (fun x -> x)
      (fun x -> x)
      (fun x -> x)
@@ -490,9 +567,9 @@ let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
     #visit_typed_avalue
     x
 
-let env_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id) (x : C.env) : C.env
-    =
-  (subst_ids_visitor rsubst
+let env_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id) (x : C.env) :
+    C.env =
+  (subst_ids_visitor r_subst
      (fun x -> x)
      (fun x -> x)
      (fun x -> x)
-- 
cgit v1.2.3


From 06360698561019d7f480dcb4263e2099d9a03ca5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 1 Sep 2023 12:01:03 +0200
Subject: Implement the normalization functions in AssociatedTypes

---
 compiler/Substitute.ml | 36 ++++++++++++++++++++++++++++++++----
 1 file changed, 32 insertions(+), 4 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 64e7716a..fe88faea 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -39,13 +39,22 @@ let ty_substitute_visitor (subst : ('r1, 'r2) subst) =
     method! visit_Self _ = subst.tr_self
   end
 
-(** Substitute types variables and regions in a type. *)
+(** Substitute types variables and regions in a type.
+
+    **IMPORTANT**: this doesn't normalize the type.
+ *)
 let ty_substitute (subst : ('r1, 'r2) subst) (ty : 'r1 T.ty) : 'r2 T.ty =
   let visitor = ty_substitute_visitor subst in
   visitor#visit_ty () ty
 
+(** **IMPORTANT**: this doesn't normalize the trait ref. *)
+let trait_ref_substitute (subst : ('r1, 'r2) subst) (tr : 'r1 T.trait_ref) :
+    'r2 T.trait_ref =
+  let visitor = ty_substitute_visitor subst in
+  visitor#visit_trait_ref () tr
+
 (** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
-let erase_regions (ty : T.rty) : T.ety =
+let erase_regions (ty : 'r T.ty) : T.ety =
   let subst =
     {
       r_subst = (fun _ -> T.Erased);
@@ -169,8 +178,9 @@ let make_trait_subst_from_clauses (clauses : T.trait_clause list)
     trs
 
 let make_subst_from_generics (params : T.generic_params)
-    (args : 'r T.generic_args) (tr_self : 'r T.trait_instance_id) :
-    (T.region_var_id T.region, 'r) subst =
+    (args : 'r T.region T.generic_args)
+    (tr_self : 'r T.region T.trait_instance_id) :
+    (T.region_var_id T.region, 'r T.region) subst =
   let r_subst = make_region_subst_from_vars params.T.regions args.T.regions in
   let ty_subst = make_type_subst_from_vars params.T.types args.T.types in
   let cg_subst =
@@ -182,6 +192,24 @@ let make_subst_from_generics (params : T.generic_params)
   in
   { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
 
+let make_subst_from_generics_no_regions :
+      'r.
+      T.generic_params ->
+      'r T.generic_args ->
+      'r T.trait_instance_id ->
+      (T.region_var_id T.region, 'r) subst =
+ fun params args tr_self ->
+  let r_subst _ = raise (Failure "Unexpected region") in
+  let ty_subst = make_type_subst_from_vars params.T.types args.T.types in
+  let cg_subst =
+    make_const_generic_subst_from_vars params.T.const_generics
+      args.T.const_generics
+  in
+  let tr_subst =
+    make_trait_subst_from_clauses params.T.trait_clauses args.T.trait_refs
+  in
+  { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
+
 let make_esubst_from_generics (params : T.generic_params)
     (generics : T.egeneric_args) (tr_self : T.etrait_instance_id) =
   let r_subst _ = T.Erased in
-- 
cgit v1.2.3


From 1e39985a44646f1c352def6e4b29365a113a5dee Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 1 Sep 2023 14:43:11 +0200
Subject: Compute the normalized trait types maps and update Interpreter

---
 compiler/Substitute.ml | 47 +++++++++++++++++++++++++++++++++--------------
 1 file changed, 33 insertions(+), 14 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index fe88faea..b1680282 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -41,30 +41,35 @@ let ty_substitute_visitor (subst : ('r1, 'r2) subst) =
 
 (** Substitute types variables and regions in a type.
 
-    **IMPORTANT**: this doesn't normalize the type.
+    **IMPORTANT**: this doesn't normalize the types.
  *)
 let ty_substitute (subst : ('r1, 'r2) subst) (ty : 'r1 T.ty) : 'r2 T.ty =
   let visitor = ty_substitute_visitor subst in
   visitor#visit_ty () ty
 
-(** **IMPORTANT**: this doesn't normalize the trait ref. *)
+(** **IMPORTANT**: this doesn't normalize the types. *)
 let trait_ref_substitute (subst : ('r1, 'r2) subst) (tr : 'r1 T.trait_ref) :
     'r2 T.trait_ref =
   let visitor = ty_substitute_visitor subst in
   visitor#visit_trait_ref () tr
 
+(** **IMPORTANT**: this doesn't normalize the types. *)
+let generic_args_substitute (subst : ('r1, 'r2) subst) (g : 'r1 T.generic_args)
+    : 'r2 T.generic_args =
+  let visitor = ty_substitute_visitor subst in
+  visitor#visit_generic_args () g
+
+let erase_regions_subst : ('r, T.erased_region) subst =
+  {
+    r_subst = (fun _ -> T.Erased);
+    ty_subst = (fun vid -> T.TypeVar vid);
+    cg_subst = (fun id -> T.ConstGenericVar id);
+    tr_subst = (fun id -> T.Clause id);
+    tr_self = T.Self;
+  }
+
 (** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
-let erase_regions (ty : 'r T.ty) : T.ety =
-  let subst =
-    {
-      r_subst = (fun _ -> T.Erased);
-      ty_subst = (fun vid -> T.TypeVar vid);
-      cg_subst = (fun id -> T.ConstGenericVar id);
-      tr_subst = (fun id -> T.Clause id);
-      tr_self = T.Self;
-    }
-  in
-  ty_substitute subst ty
+let erase_regions (ty : 'r T.ty) : T.ety = ty_substitute erase_regions_subst ty
 
 (** Generate fresh regions for region variables.
 
@@ -425,6 +430,15 @@ let fun_body_substitute_in_body
   let body = statement_substitute subst body.body in
   (locals, body)
 
+let trait_type_constraint_substitute (subst : ('r1, 'r2) subst)
+    (ttc : 'r1 T.trait_type_constraint) : 'r2 T.trait_type_constraint =
+  let { T.trait_ref; generics; type_name; ty } = ttc in
+  let visitor = ty_substitute_visitor subst in
+  let trait_ref = visitor#visit_trait_ref () trait_ref in
+  let generics = visitor#visit_generic_args () generics in
+  let ty = visitor#visit_ty () ty in
+  { T.trait_ref; generics; type_name; ty }
+
 (** Substitute a function signature.
 
     **IMPORTANT:** this function doesn't normalize the types.
@@ -448,7 +462,12 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
     { id; regions; parents }
   in
   let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
-  { A.regions_hierarchy; inputs; output }
+  let trait_type_constraints =
+    List.map
+      (trait_type_constraint_substitute subst)
+      sg.preds.trait_type_constraints
+  in
+  { A.inputs; output; regions_hierarchy; trait_type_constraints }
 
 (** Substitute variable identifiers in a type *)
 let ty_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
-- 
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/Substitute.ml | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index b1680282..6d9b9e15 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -305,19 +305,7 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
       generics.types
   | T.Assumed aty -> (
       match aty with
-      | T.Box | T.Vec ->
-          assert (generics.regions = []);
-          assert (List.length generics.types = 1);
-          assert (generics.const_generics = []);
-          generics.types
-      | T.Option ->
-          assert (generics.regions = []);
-          assert (List.length generics.types = 1);
-          assert (generics.const_generics = []);
-          if adt.V.variant_id = Some T.option_some_id then generics.types
-          else if adt.V.variant_id = Some T.option_none_id then []
-          else raise (Failure "Unreachable")
-      | T.Range ->
+      | T.Box ->
           assert (generics.regions = []);
           assert (List.length generics.types = 1);
           assert (generics.const_generics = []);
-- 
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/Substitute.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 6d9b9e15..23f618e2 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -71,6 +71,9 @@ let erase_regions_subst : ('r, T.erased_region) subst =
 (** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
 let erase_regions (ty : 'r T.ty) : T.ety = ty_substitute erase_regions_subst ty
 
+let trait_ref_erase_regions (tr : 'r T.trait_ref) : T.etrait_ref =
+  trait_ref_substitute erase_regions_subst tr
+
 (** Generate fresh regions for region variables.
 
     Return the list of new regions and appropriate substitutions from the
-- 
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/Substitute.ml | 426 ++++++++++++++++++-------------------------------
 1 file changed, 152 insertions(+), 274 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 23f618e2..b4eee9f8 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -9,20 +9,20 @@ module E = Expressions
 module A = LlbcAst
 module C = Contexts
 
-type ('r1, 'r2) subst = {
-  r_subst : 'r1 -> 'r2;
-  ty_subst : T.TypeVarId.id -> 'r2 T.ty;
+type subst = {
+  r_subst : T.region -> T.region;
+  ty_subst : T.TypeVarId.id -> T.ty;
   cg_subst : T.ConstGenericVarId.id -> T.const_generic;
       (** Substitution from *local* trait clause to trait instance *)
-  tr_subst : T.TraitClauseId.id -> 'r2 T.trait_instance_id;
+  tr_subst : T.TraitClauseId.id -> T.trait_instance_id;
       (** Substitution for the [Self] trait instance *)
-  tr_self : 'r2 T.trait_instance_id;
+  tr_self : T.trait_instance_id;
 }
 
-let ty_substitute_visitor (subst : ('r1, 'r2) subst) =
+let st_substitute_visitor (subst : subst) =
   object
-    inherit [_] T.map_ty
-    method visit_'r _ r = subst.r_subst r
+    inherit [_] A.map_statement
+    method! visit_region _ r = subst.r_subst r
     method! visit_TypeVar _ id = subst.ty_subst id
 
     method! visit_type_var_id _ _ =
@@ -43,25 +43,30 @@ let ty_substitute_visitor (subst : ('r1, 'r2) subst) =
 
     **IMPORTANT**: this doesn't normalize the types.
  *)
-let ty_substitute (subst : ('r1, 'r2) subst) (ty : 'r1 T.ty) : 'r2 T.ty =
-  let visitor = ty_substitute_visitor subst in
+let ty_substitute (subst : subst) (ty : T.ty) : T.ty =
+  let visitor = st_substitute_visitor subst in
   visitor#visit_ty () ty
 
 (** **IMPORTANT**: this doesn't normalize the types. *)
-let trait_ref_substitute (subst : ('r1, 'r2) subst) (tr : 'r1 T.trait_ref) :
-    'r2 T.trait_ref =
-  let visitor = ty_substitute_visitor subst in
+let trait_ref_substitute (subst : subst) (tr : T.trait_ref) : T.trait_ref =
+  let visitor = st_substitute_visitor subst in
   visitor#visit_trait_ref () tr
 
 (** **IMPORTANT**: this doesn't normalize the types. *)
-let generic_args_substitute (subst : ('r1, 'r2) subst) (g : 'r1 T.generic_args)
-    : 'r2 T.generic_args =
-  let visitor = ty_substitute_visitor subst in
+let trait_instance_id_substitute (subst : subst) (tr : T.trait_instance_id) :
+    T.trait_instance_id =
+  let visitor = st_substitute_visitor subst in
+  visitor#visit_trait_instance_id () tr
+
+(** **IMPORTANT**: this doesn't normalize the types. *)
+let generic_args_substitute (subst : subst) (g : T.generic_args) :
+    T.generic_args =
+  let visitor = st_substitute_visitor subst in
   visitor#visit_generic_args () g
 
-let erase_regions_subst : ('r, T.erased_region) subst =
+let erase_regions_subst : subst =
   {
-    r_subst = (fun _ -> T.Erased);
+    r_subst = (fun _ -> T.RErased);
     ty_subst = (fun vid -> T.TypeVar vid);
     cg_subst = (fun id -> T.ConstGenericVar id);
     tr_subst = (fun id -> T.Clause id);
@@ -69,11 +74,18 @@ let erase_regions_subst : ('r, T.erased_region) subst =
   }
 
 (** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
-let erase_regions (ty : 'r T.ty) : T.ety = ty_substitute erase_regions_subst ty
+let erase_regions (ty : T.ty) : T.ty = ty_substitute erase_regions_subst ty
 
-let trait_ref_erase_regions (tr : 'r T.trait_ref) : T.etrait_ref =
+let trait_ref_erase_regions (tr : T.trait_ref) : T.trait_ref =
   trait_ref_substitute erase_regions_subst tr
 
+let trait_instance_id_erase_regions (tr : T.trait_instance_id) :
+    T.trait_instance_id =
+  trait_instance_id_substitute erase_regions_subst tr
+
+let generic_args_erase_regions (tr : T.generic_args) : T.generic_args =
+  generic_args_substitute erase_regions_subst tr
+
 (** Generate fresh regions for region variables.
 
     Return the list of new regions and appropriate substitutions from the
@@ -83,60 +95,62 @@ let trait_ref_erase_regions (tr : 'r T.trait_ref) : T.etrait_ref =
   *)
 let fresh_regions_with_substs (region_vars : T.region_var list) :
     T.RegionId.id list
-    * (T.RegionVarId.id -> T.RegionId.id)
-    * (T.RegionVarId.id T.region -> T.RegionId.id T.region) =
+    * (T.RegionId.id -> T.RegionId.id)
+    * (T.region -> T.region) =
   (* Generate fresh regions *)
   let fresh_region_ids = List.map (fun _ -> C.fresh_region_id ()) region_vars in
   (* Generate the map from region var ids to regions *)
   let ls = List.combine region_vars fresh_region_ids in
   let rid_map =
     List.fold_left
-      (fun mp ((k : T.region_var), v) -> T.RegionVarId.Map.add k.T.index v mp)
-      T.RegionVarId.Map.empty ls
+      (fun mp ((k : T.region_var), v) -> T.RegionId.Map.add k.T.index v mp)
+      T.RegionId.Map.empty ls
   in
   (* Generate the substitution from region var id to region *)
-  let rid_subst id = T.RegionVarId.Map.find id rid_map in
+  let rid_subst id = T.RegionId.Map.find id rid_map in
   (* Generate the substitution from region to region *)
-  let r_subst r =
-    match r with T.Static -> T.Static | T.Var id -> T.Var (rid_subst id)
+  let r_subst (r : T.region) =
+    match r with
+    | T.RStatic | T.RErased -> r
+    | T.RVar id -> T.RVar (rid_subst id)
   in
   (* Return *)
   (fresh_region_ids, rid_subst, r_subst)
 
 (** Erase the regions in a type and perform a substitution *)
-let erase_regions_substitute_types (ty_subst : T.TypeVarId.id -> T.ety)
+let erase_regions_substitute_types (ty_subst : T.TypeVarId.id -> T.ty)
     (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
-    (tr_subst : T.TraitClauseId.id -> T.etrait_instance_id)
-    (tr_self : T.etrait_instance_id) (ty : 'r T.ty) : T.ety =
-  let r_subst (_ : 'r) : T.erased_region = T.Erased in
+    (tr_subst : T.TraitClauseId.id -> T.trait_instance_id)
+    (tr_self : T.trait_instance_id) (ty : T.ty) : T.ty =
+  let r_subst (_ : T.region) : T.region = T.RErased in
   let subst = { r_subst; ty_subst; cg_subst; tr_subst; tr_self } in
   ty_substitute subst ty
 
 (** Create a region substitution from a list of region variable ids and a list of
     regions (with which to substitute the region variable ids *)
-let make_region_subst (var_ids : T.RegionVarId.id list)
-    (regions : 'r T.region list) : T.RegionVarId.id T.region -> 'r T.region =
+let make_region_subst (var_ids : T.RegionId.id list) (regions : T.region list) :
+    T.region -> T.region =
   let ls = List.combine var_ids regions in
   let mp =
     List.fold_left
-      (fun mp (k, v) -> T.RegionVarId.Map.add k v mp)
-      T.RegionVarId.Map.empty ls
+      (fun mp (k, v) -> T.RegionId.Map.add k v mp)
+      T.RegionId.Map.empty ls
   in
   fun r ->
     match r with
-    | T.Static -> T.Static
-    | T.Var id -> T.RegionVarId.Map.find id mp
+    | T.RStatic | T.RErased -> r
+    | T.RVar id -> T.RegionId.Map.find id mp
 
 let make_region_subst_from_vars (vars : T.region_var list)
-    (regions : 'r T.region list) : T.RegionVarId.id T.region -> 'r T.region =
+    (regions : T.region list) : T.region -> T.region =
   make_region_subst
     (List.map (fun (x : T.region_var) -> x.T.index) vars)
     regions
 
 (** Create a type substitution from a list of type variable ids and a list of
     types (with which to substitute the type variable ids) *)
-let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
-    T.TypeVarId.id -> 'r T.ty =
+let make_type_subst (var_ids : T.TypeVarId.id list) (tys : T.ty list) :
+    T.TypeVarId.id -> T.ty =
   let ls = List.combine var_ids tys in
   let mp =
     List.fold_left
@@ -145,8 +159,8 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
   in
   fun id -> T.TypeVarId.Map.find id mp
 
-let make_type_subst_from_vars (vars : T.type_var list) (tys : 'r T.ty list) :
-    T.TypeVarId.id -> 'r T.ty =
+let make_type_subst_from_vars (vars : T.type_var list) (tys : T.ty list) :
+    T.TypeVarId.id -> T.ty =
   make_type_subst (List.map (fun (x : T.type_var) -> x.T.index) vars) tys
 
 (** Create a const generic substitution from a list of const generic variable ids and a list of
@@ -170,7 +184,7 @@ let make_const_generic_subst_from_vars (vars : T.const_generic_var list)
 (** Create a trait substitution from a list of trait clause ids and a list of
     trait refs *)
 let make_trait_subst (clause_ids : T.TraitClauseId.id list)
-    (trs : 'r T.trait_ref list) : T.TraitClauseId.id -> 'r T.trait_instance_id =
+    (trs : T.trait_ref list) : T.TraitClauseId.id -> T.trait_instance_id =
   let ls = List.combine clause_ids trs in
   let mp =
     List.fold_left
@@ -180,15 +194,13 @@ let make_trait_subst (clause_ids : T.TraitClauseId.id list)
   fun id -> T.TraitClauseId.Map.find id mp
 
 let make_trait_subst_from_clauses (clauses : T.trait_clause list)
-    (trs : 'r T.trait_ref list) : T.TraitClauseId.id -> 'r T.trait_instance_id =
+    (trs : T.trait_ref list) : T.TraitClauseId.id -> T.trait_instance_id =
   make_trait_subst
     (List.map (fun (x : T.trait_clause) -> x.T.clause_id) clauses)
     trs
 
-let make_subst_from_generics (params : T.generic_params)
-    (args : 'r T.region T.generic_args)
-    (tr_self : 'r T.region T.trait_instance_id) :
-    (T.region_var_id T.region, 'r T.region) subst =
+let make_subst_from_generics (params : T.generic_params) (args : T.generic_args)
+    (tr_self : T.trait_instance_id) : subst =
   let r_subst = make_region_subst_from_vars params.T.regions args.T.regions in
   let ty_subst = make_type_subst_from_vars params.T.types args.T.types in
   let cg_subst =
@@ -200,36 +212,12 @@ let make_subst_from_generics (params : T.generic_params)
   in
   { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
 
-let make_subst_from_generics_no_regions :
-      'r.
-      T.generic_params ->
-      'r T.generic_args ->
-      'r T.trait_instance_id ->
-      (T.region_var_id T.region, 'r) subst =
- fun params args tr_self ->
-  let r_subst _ = raise (Failure "Unexpected region") in
-  let ty_subst = make_type_subst_from_vars params.T.types args.T.types in
-  let cg_subst =
-    make_const_generic_subst_from_vars params.T.const_generics
-      args.T.const_generics
-  in
-  let tr_subst =
-    make_trait_subst_from_clauses params.T.trait_clauses args.T.trait_refs
-  in
-  { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
-
-let make_esubst_from_generics (params : T.generic_params)
-    (generics : T.egeneric_args) (tr_self : T.etrait_instance_id) =
-  let r_subst _ = T.Erased in
-  let ty_subst = make_type_subst_from_vars params.types generics.T.types in
-  let cg_subst =
-    make_const_generic_subst_from_vars params.const_generics
-      generics.T.const_generics
-  in
-  let tr_subst =
-    make_trait_subst_from_clauses params.trait_clauses generics.T.trait_refs
-  in
-  { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
+let make_subst_from_generics_erase_regions (params : T.generic_params)
+    (generics : T.generic_args) (tr_self : T.trait_instance_id) =
+  let generics = generic_args_erase_regions generics in
+  let tr_self = trait_instance_id_erase_regions tr_self in
+  let subst = make_subst_from_generics params generics tr_self in
+  { subst with r_subst = (fun _ -> T.RErased) }
 
 (** Instantiate the type variables in an ADT definition, and return, for
     every variant, the list of the types of its fields.
@@ -237,8 +225,8 @@ let make_esubst_from_generics (params : T.generic_params)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
 *)
-let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
-    (generics : T.rgeneric_args) : (T.VariantId.id option * T.rty list) list =
+let type_decl_get_instantiated_variants_fields_types (def : T.type_decl)
+    (generics : T.generic_args) : (T.VariantId.id option * T.ty list) list =
   (* There shouldn't be any reference to Self *)
   let tr_self = T.UnknownTrait __FUNCTION__ in
   let subst = make_subst_from_generics def.T.generics generics tr_self in
@@ -266,9 +254,9 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
 *)
-let type_decl_get_instantiated_field_rtypes (def : T.type_decl)
-    (opt_variant_id : T.VariantId.id option) (generics : T.rgeneric_args) :
-    T.rty list =
+let type_decl_get_instantiated_field_types (def : T.type_decl)
+    (opt_variant_id : T.VariantId.id option) (generics : T.generic_args) :
+    T.ty list =
   (* For now, check that there are no clauses - otherwise we might need
      to normalize the types *)
   assert (def.generics.trait_clauses = []);
@@ -284,11 +272,11 @@ let type_decl_get_instantiated_field_rtypes (def : T.type_decl)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
 *)
-let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx)
+let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx)
     (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (generics : T.rgeneric_args) : T.rty list =
+    (generics : T.generic_args) : T.ty list =
   let def = C.ctx_lookup_type_decl ctx def_id in
-  type_decl_get_instantiated_field_rtypes def opt_variant_id generics
+  type_decl_get_instantiated_field_types def opt_variant_id generics
 
 (** Return the types of the properly instantiated ADT value (note that
     here, ADT is understood in its broad meaning: ADT, assumed value or tuple).
@@ -296,122 +284,55 @@ let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
  *)
-let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
-    (adt : V.adt_value) (id : T.type_id) (generics : T.rgeneric_args) :
-    T.rty list =
+let ctx_adt_value_get_instantiated_field_types (ctx : C.eval_ctx)
+    (adt : V.adt_value) (id : T.type_id) (generics : T.generic_args) : T.ty list
+    =
   match id with
   | T.AdtId id ->
       (* Retrieve the types of the fields *)
-      ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id generics
+      ctx_adt_get_instantiated_field_types ctx id adt.V.variant_id generics
   | T.Tuple ->
       assert (generics.regions = []);
       generics.types
-  | T.Assumed aty -> (
+  | T.TAssumed aty -> (
       match aty with
-      | T.Box ->
+      | T.TBox ->
           assert (generics.regions = []);
           assert (List.length generics.types = 1);
           assert (generics.const_generics = []);
           generics.types
-      | T.Array | T.Slice | T.Str ->
+      | T.TArray | T.TSlice | T.TStr ->
           (* Those types don't have fields *)
           raise (Failure "Unreachable"))
 
-(** Instantiate the type variables in an ADT definition, and return the list
-    of types of the fields for the chosen variant.
-
-    **IMPORTANT**: this function doesn't normalize the types, you may want to
-    use the [AssociatedTypes] equivalent instead.
-*)
-let type_decl_get_instantiated_field_etypes (def : T.type_decl)
-    (opt_variant_id : T.VariantId.id option) (generics : T.egeneric_args) :
-    T.ety list =
-  (* For now, check that there are no clauses - otherwise we might need
-     to normalize the types *)
-  assert (def.generics.trait_clauses = []);
-  (* There shouldn't be any reference to Self *)
-  let tr_self : T.erased_region T.trait_instance_id =
-    T.UnknownTrait __FUNCTION__
-  in
-  let { r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
-    make_esubst_from_generics def.T.generics generics tr_self
-  in
-  let fields = TU.type_decl_get_fields def opt_variant_id in
-  List.map
-    (fun (f : T.field) ->
-      erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
-        f.T.field_ty)
-    fields
-
-(** Return the types of the properly instantiated ADT's variant, provided a
-    context.
-
-    **IMPORTANT**: this function doesn't normalize the types, you may want to
-    use the [AssociatedTypes] equivalent instead.
- *)
-let ctx_adt_get_instantiated_field_etypes (ctx : C.eval_ctx)
-    (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (generics : T.egeneric_args) : T.ety list =
-  let def = C.ctx_lookup_type_decl ctx def_id in
-  type_decl_get_instantiated_field_etypes def opt_variant_id generics
-
-let statement_substitute_visitor
-    (subst : (T.erased_region, T.erased_region) subst) =
-  (* Keep in synch with [ty_substitute_visitor] *)
-  object
-    inherit [_] A.map_statement
-    method! visit_'r _ r = subst.r_subst r
-    method! visit_TypeVar _ id = subst.ty_subst id
-
-    method! visit_type_var_id _ _ =
-      (* We should never get here because we reimplemented [visit_TypeVar] *)
-      raise (Failure "Unexpected")
-
-    method! visit_ConstGenericVar _ id = subst.cg_subst id
-
-    method! visit_const_generic_var_id _ _ =
-      (* We should never get here because we reimplemented [visit_Var] *)
-      raise (Failure "Unexpected")
-
-    method! visit_Clause _ id = subst.tr_subst id
-    method! visit_Self _ = subst.tr_self
-  end
-
 (** Apply a type substitution to a place *)
-let place_substitute (subst : (T.erased_region, T.erased_region) subst)
-    (p : E.place) : E.place =
+let place_substitute (subst : subst) (p : E.place) : E.place =
   (* There is in fact nothing to do *)
-  (statement_substitute_visitor subst)#visit_place () p
+  (st_substitute_visitor subst)#visit_place () p
 
 (** Apply a type substitution to an operand *)
-let operand_substitute (subst : (T.erased_region, T.erased_region) subst)
-    (op : E.operand) : E.operand =
-  (statement_substitute_visitor subst)#visit_operand () op
+let operand_substitute (subst : subst) (op : E.operand) : E.operand =
+  (st_substitute_visitor subst)#visit_operand () op
 
 (** Apply a type substitution to an rvalue *)
-let rvalue_substitute (subst : (T.erased_region, T.erased_region) subst)
-    (rv : E.rvalue) : E.rvalue =
-  (statement_substitute_visitor subst)#visit_rvalue () rv
+let rvalue_substitute (subst : subst) (rv : E.rvalue) : E.rvalue =
+  (st_substitute_visitor subst)#visit_rvalue () rv
 
 (** Apply a type substitution to an assertion *)
-let assertion_substitute (subst : (T.erased_region, T.erased_region) subst)
-    (a : A.assertion) : A.assertion =
-  (statement_substitute_visitor subst)#visit_assertion () a
+let assertion_substitute (subst : subst) (a : A.assertion) : A.assertion =
+  (st_substitute_visitor subst)#visit_assertion () a
 
 (** Apply a type substitution to a call *)
-let call_substitute (subst : (T.erased_region, T.erased_region) subst)
-    (call : A.call) : A.call =
-  (statement_substitute_visitor subst)#visit_call () call
+let call_substitute (subst : subst) (call : A.call) : A.call =
+  (st_substitute_visitor subst)#visit_call () call
 
 (** Apply a type substitution to a statement *)
-let statement_substitute (subst : (T.erased_region, T.erased_region) subst)
-    (st : A.statement) : A.statement =
-  (statement_substitute_visitor subst)#visit_statement () st
+let statement_substitute (subst : subst) (st : A.statement) : A.statement =
+  (st_substitute_visitor subst)#visit_statement () st
 
 (** Apply a type substitution to a function body. Return the local variables
     and the body. *)
-let fun_body_substitute_in_body
-    (subst : (T.erased_region, T.erased_region) subst) (body : A.fun_body) :
+let fun_body_substitute_in_body (subst : subst) (body : A.fun_body) :
     A.var list * A.statement =
   let locals =
     List.map
@@ -421,10 +342,10 @@ let fun_body_substitute_in_body
   let body = statement_substitute subst body.body in
   (locals, body)
 
-let trait_type_constraint_substitute (subst : ('r1, 'r2) subst)
-    (ttc : 'r1 T.trait_type_constraint) : 'r2 T.trait_type_constraint =
+let trait_type_constraint_substitute (subst : subst)
+    (ttc : T.trait_type_constraint) : T.trait_type_constraint =
   let { T.trait_ref; generics; type_name; ty } = ttc in
-  let visitor = ty_substitute_visitor subst in
+  let visitor = st_substitute_visitor subst in
   let trait_ref = visitor#visit_trait_ref () trait_ref in
   let generics = visitor#visit_generic_args () generics in
   let ty = visitor#visit_ty () ty in
@@ -435,22 +356,24 @@ let trait_type_constraint_substitute (subst : ('r1, 'r2) subst)
     **IMPORTANT:** this function doesn't normalize the types.
  *)
 let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
-    (r_subst : T.RegionVarId.id -> T.RegionId.id)
-    (ty_subst : T.TypeVarId.id -> T.rty)
+    (r_subst : T.RegionId.id -> T.RegionId.id)
+    (ty_subst : T.TypeVarId.id -> T.ty)
     (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
-    (tr_subst : T.TraitClauseId.id -> T.rtrait_instance_id)
-    (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
-  let r_subst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
-    match r with T.Static -> T.Static | T.Var rid -> T.Var (r_subst rid)
+    (tr_subst : T.TraitClauseId.id -> T.trait_instance_id)
+    (tr_self : T.trait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+  let r_subst' (r : T.region) : T.region =
+    match r with
+    | T.RStatic | T.RErased -> r
+    | T.RVar rid -> T.RVar (r_subst rid)
   in
   let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in
   let inputs = List.map (ty_substitute subst) sg.A.inputs in
   let output = ty_substitute subst sg.A.output in
-  let subst_region_group (rg : T.region_var_group) : A.abs_region_group =
+  let subst_region_group (rg : T.region_group) : A.abs_region_group =
     let id = asubst rg.id in
     let regions = List.map r_subst rg.regions in
     let parents = List.map asubst rg.parents in
-    { id; regions; parents }
+    ({ id; regions; parents } : A.abs_region_group)
   in
   let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
   let trait_type_constraints =
@@ -461,9 +384,9 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
   { A.inputs; output; regions_hierarchy; trait_type_constraints }
 
 (** Substitute variable identifiers in a type *)
-let ty_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : 'r T.ty)
-    : 'r T.ty =
+let statement_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : T.ty) :
+    T.ty =
   let open T in
   let visitor =
     object
@@ -476,80 +399,39 @@ let ty_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
 
   visitor#visit_ty () ty
 
-(* This visitor is a mess...
-
-   We want to write a class which visits abstractions, values, etc. *and their
-   types* to substitute identifiers.
-
-   The issue is that we derive two specialized types (ety and rty) from a
-   polymorphic type (ty). Because of this, there are typing issues with
-   [visit_'r] if we define a class which visits objects of types [ety] and [rty]
-   while inheriting a class which visit [ty]...
-*)
 let subst_ids_visitor (r_subst : T.RegionId.id -> T.RegionId.id)
-    (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
     (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
     (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) =
-  let subst_rty =
-    object
-      inherit [_] T.map_ty
-
-      method visit_'r _ r =
-        match r with T.Static -> T.Static | T.Var rid -> T.Var (r_subst rid)
-
-      method! visit_type_var_id _ id = ty_subst id
-      method! visit_const_generic_var_id _ id = cg_subst id
-    end
-  in
-
-  let visitor =
-    object (self : 'self)
-      inherit [_] C.map_env
-      method! visit_borrow_id _ bid = bsubst bid
-      method! visit_loan_id _ bid = bsubst bid
-      method! visit_ety _ ty = ty_substitute_ids ty_subst cg_subst ty
-      method! visit_rty env ty = subst_rty#visit_ty env ty
-      method! visit_symbolic_value_id _ id = ssubst id
-
-      (** We *do* visit meta-values *)
-      method! visit_msymbolic_value env sv = self#visit_symbolic_value env sv
-
-      (** We *do* visit meta-values *)
-      method! visit_mvalue env v = self#visit_typed_value env v
-
-      method! visit_region_id _ id = r_subst id
-      method! visit_region_var_id _ id = rvsubst id
-      method! visit_abstraction_id _ id = asubst id
-    end
-  in
-
-  object
-    method visit_ety (x : T.ety) : T.ety = visitor#visit_ety () x
-    method visit_rty (x : T.rty) : T.rty = visitor#visit_rty () x
-
-    method visit_typed_value (x : V.typed_value) : V.typed_value =
-      visitor#visit_typed_value () x
-
-    method visit_typed_avalue (x : V.typed_avalue) : V.typed_avalue =
-      visitor#visit_typed_avalue () x
-
-    method visit_abs (x : V.abs) : V.abs = visitor#visit_abs () x
-    method visit_env (env : C.env) : C.env = visitor#visit_env () env
+  object (self : 'self)
+    inherit [_] C.map_env
+    method! visit_type_var_id _ id = ty_subst id
+    method! visit_const_generic_var_id _ id = cg_subst id
+    method! visit_region_id _ rid = r_subst rid
+    method! visit_borrow_id _ bid = bsubst bid
+    method! visit_loan_id _ bid = bsubst bid
+    method! visit_symbolic_value_id _ id = ssubst id
+
+    (** We *do* visit meta-values *)
+    method! visit_msymbolic_value env sv = self#visit_symbolic_value env sv
+
+    (** We *do* visit meta-values *)
+    method! visit_mvalue env v = self#visit_typed_value env v
+
+    method! visit_abstraction_id _ id = asubst id
   end
 
 let typed_value_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
     (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
     (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_value) :
     V.typed_value =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
-    #visit_typed_value v
+  let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
+  vis#visit_typed_value () v
 
 let typed_value_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
     (v : V.typed_value) : V.typed_value =
@@ -558,61 +440,57 @@ let typed_value_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
     (fun x -> x)
     (fun x -> x)
     (fun x -> x)
-    (fun x -> x)
     v
 
 let typed_avalue_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
     (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
     (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_avalue) :
     V.typed_avalue =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
-    #visit_typed_avalue v
+  let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
+  vis#visit_typed_avalue () v
 
 let abs_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
     (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
     (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : V.abs) : V.abs =
-  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
-    #visit_abs x
+  let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
+  vis#visit_abs () x
 
 let env_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
     (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
     (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : C.env) : C.env =
-  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
-    #visit_env x
+  let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
+  vis#visit_env () x
 
 let typed_avalue_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
     (x : V.typed_avalue) : V.typed_avalue =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor r_subst
-     (fun x -> x)
-     (fun x -> x)
-     (fun x -> x)
-     (fun x -> x)
-     (fun x -> x)
-     asubst)
-    #visit_typed_avalue
-    x
+  let vis =
+    subst_ids_visitor r_subst
+      (fun x -> x)
+      (fun x -> x)
+      (fun x -> x)
+      (fun x -> x)
+      asubst
+  in
+  vis#visit_typed_avalue () x
 
 let env_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id) (x : C.env) :
     C.env =
-  (subst_ids_visitor r_subst
-     (fun x -> x)
-     (fun x -> x)
-     (fun x -> x)
-     (fun x -> x)
-     (fun x -> x)
-     (fun x -> x))
-    #visit_env
-    x
+  let vis =
+    subst_ids_visitor r_subst
+      (fun x -> x)
+      (fun x -> x)
+      (fun x -> x)
+      (fun x -> x)
+      (fun x -> x)
+  in
+  vis#visit_env () x
-- 
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/Substitute.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index b4eee9f8..490574a2 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -29,7 +29,7 @@ let st_substitute_visitor (subst : subst) =
       (* We should never get here because we reimplemented [visit_TypeVar] *)
       raise (Failure "Unexpected")
 
-    method! visit_ConstGenericVar _ id = subst.cg_subst id
+    method! visit_CGVar _ id = subst.cg_subst id
 
     method! visit_const_generic_var_id _ _ =
       (* We should never get here because we reimplemented [visit_Var] *)
@@ -68,7 +68,7 @@ let erase_regions_subst : subst =
   {
     r_subst = (fun _ -> T.RErased);
     ty_subst = (fun vid -> T.TypeVar vid);
-    cg_subst = (fun id -> T.ConstGenericVar id);
+    cg_subst = (fun id -> T.CGVar id);
     tr_subst = (fun id -> T.Clause id);
     tr_self = T.Self;
   }
-- 
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/Substitute.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 490574a2..166c237a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -23,7 +23,7 @@ let st_substitute_visitor (subst : subst) =
   object
     inherit [_] A.map_statement
     method! visit_region _ r = subst.r_subst r
-    method! visit_TypeVar _ id = subst.ty_subst id
+    method! visit_TVar _ id = subst.ty_subst id
 
     method! visit_type_var_id _ _ =
       (* We should never get here because we reimplemented [visit_TypeVar] *)
@@ -67,7 +67,7 @@ let generic_args_substitute (subst : subst) (g : T.generic_args) :
 let erase_regions_subst : subst =
   {
     r_subst = (fun _ -> T.RErased);
-    ty_subst = (fun vid -> T.TypeVar vid);
+    ty_subst = (fun vid -> T.TVar vid);
     cg_subst = (fun id -> T.CGVar id);
     tr_subst = (fun id -> T.Clause id);
     tr_self = T.Self;
@@ -288,10 +288,10 @@ let ctx_adt_value_get_instantiated_field_types (ctx : C.eval_ctx)
     (adt : V.adt_value) (id : T.type_id) (generics : T.generic_args) : T.ty list
     =
   match id with
-  | T.AdtId id ->
+  | T.TAdtId id ->
       (* Retrieve the types of the fields *)
       ctx_adt_get_instantiated_field_types ctx id adt.V.variant_id generics
-  | T.Tuple ->
+  | T.TTuple ->
       assert (generics.regions = []);
       generics.types
   | T.TAssumed aty -> (
-- 
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/Substitute.ml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 166c237a..45edc602 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -64,6 +64,10 @@ let generic_args_substitute (subst : subst) (g : T.generic_args) :
   let visitor = st_substitute_visitor subst in
   visitor#visit_generic_args () g
 
+let predicates_substitute (subst : subst) (p : T.predicates) : T.predicates =
+  let visitor = st_substitute_visitor subst in
+  visitor#visit_predicates () p
+
 let erase_regions_subst : subst =
   {
     r_subst = (fun _ -> T.RErased);
@@ -351,7 +355,8 @@ let trait_type_constraint_substitute (subst : subst)
   let ty = visitor#visit_ty () ty in
   { T.trait_ref; generics; type_name; ty }
 
-(** Substitute a function signature.
+(** Substitute a function signature, together with the regions hierarchy
+    associated to that signature.
 
     **IMPORTANT:** this function doesn't normalize the types.
  *)
@@ -360,7 +365,8 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
     (ty_subst : T.TypeVarId.id -> T.ty)
     (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
     (tr_subst : T.TraitClauseId.id -> T.trait_instance_id)
-    (tr_self : T.trait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+    (tr_self : T.trait_instance_id) (sg : A.fun_sig)
+    (regions_hierarchy : T.region_groups) : A.inst_fun_sig =
   let r_subst' (r : T.region) : T.region =
     match r with
     | T.RStatic | T.RErased -> r
@@ -375,7 +381,7 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
     let parents = List.map asubst rg.parents in
     ({ id; regions; parents } : A.abs_region_group)
   in
-  let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
+  let regions_hierarchy = List.map subst_region_group regions_hierarchy in
   let trait_type_constraints =
     List.map
       (trait_type_constraint_substitute subst)
-- 
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/Substitute.ml | 374 +++++++++++++++++++++++--------------------------
 1 file changed, 176 insertions(+), 198 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 45edc602..01509dec 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -2,26 +2,26 @@
     function bodies, etc.
  *)
 
-module T = Types
-module TU = TypesUtils
-module V = Values
-module E = Expressions
-module A = LlbcAst
-module C = Contexts
+open Types
+open TypesUtils
+open Values
+open Expressions
+open LlbcAst
+open Contexts
 
 type subst = {
-  r_subst : T.region -> T.region;
-  ty_subst : T.TypeVarId.id -> T.ty;
-  cg_subst : T.ConstGenericVarId.id -> T.const_generic;
+  r_subst : region -> region;
+  ty_subst : TypeVarId.id -> ty;
+  cg_subst : ConstGenericVarId.id -> const_generic;
       (** Substitution from *local* trait clause to trait instance *)
-  tr_subst : T.TraitClauseId.id -> T.trait_instance_id;
+  tr_subst : TraitClauseId.id -> trait_instance_id;
       (** Substitution for the [Self] trait instance *)
-  tr_self : T.trait_instance_id;
+  tr_self : trait_instance_id;
 }
 
 let st_substitute_visitor (subst : subst) =
   object
-    inherit [_] A.map_statement
+    inherit [_] map_statement
     method! visit_region _ r = subst.r_subst r
     method! visit_TVar _ id = subst.ty_subst id
 
@@ -43,51 +43,50 @@ let st_substitute_visitor (subst : subst) =
 
     **IMPORTANT**: this doesn't normalize the types.
  *)
-let ty_substitute (subst : subst) (ty : T.ty) : T.ty =
+let ty_substitute (subst : subst) (ty : ty) : ty =
   let visitor = st_substitute_visitor subst in
   visitor#visit_ty () ty
 
 (** **IMPORTANT**: this doesn't normalize the types. *)
-let trait_ref_substitute (subst : subst) (tr : T.trait_ref) : T.trait_ref =
+let trait_ref_substitute (subst : subst) (tr : trait_ref) : trait_ref =
   let visitor = st_substitute_visitor subst in
   visitor#visit_trait_ref () tr
 
 (** **IMPORTANT**: this doesn't normalize the types. *)
-let trait_instance_id_substitute (subst : subst) (tr : T.trait_instance_id) :
-    T.trait_instance_id =
+let trait_instance_id_substitute (subst : subst) (tr : trait_instance_id) :
+    trait_instance_id =
   let visitor = st_substitute_visitor subst in
   visitor#visit_trait_instance_id () tr
 
 (** **IMPORTANT**: this doesn't normalize the types. *)
-let generic_args_substitute (subst : subst) (g : T.generic_args) :
-    T.generic_args =
+let generic_args_substitute (subst : subst) (g : generic_args) : generic_args =
   let visitor = st_substitute_visitor subst in
   visitor#visit_generic_args () g
 
-let predicates_substitute (subst : subst) (p : T.predicates) : T.predicates =
+let predicates_substitute (subst : subst) (p : predicates) : predicates =
   let visitor = st_substitute_visitor subst in
   visitor#visit_predicates () p
 
 let erase_regions_subst : subst =
   {
-    r_subst = (fun _ -> T.RErased);
-    ty_subst = (fun vid -> T.TVar vid);
-    cg_subst = (fun id -> T.CGVar id);
-    tr_subst = (fun id -> T.Clause id);
-    tr_self = T.Self;
+    r_subst = (fun _ -> RErased);
+    ty_subst = (fun vid -> TVar vid);
+    cg_subst = (fun id -> CGVar id);
+    tr_subst = (fun id -> Clause id);
+    tr_self = Self;
   }
 
-(** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
-let erase_regions (ty : T.ty) : T.ty = ty_substitute erase_regions_subst ty
+(** Convert an {!rty} to an {!ety} by erasing the region variables *)
+let erase_regions (ty : ty) : ty = ty_substitute erase_regions_subst ty
 
-let trait_ref_erase_regions (tr : T.trait_ref) : T.trait_ref =
+let trait_ref_erase_regions (tr : trait_ref) : trait_ref =
   trait_ref_substitute erase_regions_subst tr
 
-let trait_instance_id_erase_regions (tr : T.trait_instance_id) :
-    T.trait_instance_id =
+let trait_instance_id_erase_regions (tr : trait_instance_id) : trait_instance_id
+    =
   trait_instance_id_substitute erase_regions_subst tr
 
-let generic_args_erase_regions (tr : T.generic_args) : T.generic_args =
+let generic_args_erase_regions (tr : generic_args) : generic_args =
   generic_args_substitute erase_regions_subst tr
 
 (** Generate fresh regions for region variables.
@@ -95,133 +94,124 @@ let generic_args_erase_regions (tr : T.generic_args) : T.generic_args =
     Return the list of new regions and appropriate substitutions from the
     original region variables to the fresh regions.
     
-    TODO: simplify? we only need the subst [T.RegionVarId.id -> T.RegionId.id]
+    TODO: simplify? we only need the subst [RegionVarId.id -> RegionId.id]
   *)
-let fresh_regions_with_substs (region_vars : T.region_var list) :
-    T.RegionId.id list
-    * (T.RegionId.id -> T.RegionId.id)
-    * (T.region -> T.region) =
+let fresh_regions_with_substs (region_vars : region_var list) :
+    RegionId.id list * (RegionId.id -> RegionId.id) * (region -> region) =
   (* Generate fresh regions *)
-  let fresh_region_ids = List.map (fun _ -> C.fresh_region_id ()) region_vars in
+  let fresh_region_ids = List.map (fun _ -> fresh_region_id ()) region_vars in
   (* Generate the map from region var ids to regions *)
   let ls = List.combine region_vars fresh_region_ids in
   let rid_map =
     List.fold_left
-      (fun mp ((k : T.region_var), v) -> T.RegionId.Map.add k.T.index v mp)
-      T.RegionId.Map.empty ls
+      (fun mp ((k : region_var), v) -> RegionId.Map.add k.index v mp)
+      RegionId.Map.empty ls
   in
   (* Generate the substitution from region var id to region *)
-  let rid_subst id = T.RegionId.Map.find id rid_map in
+  let rid_subst id = RegionId.Map.find id rid_map in
   (* Generate the substitution from region to region *)
-  let r_subst (r : T.region) =
-    match r with
-    | T.RStatic | T.RErased -> r
-    | T.RVar id -> T.RVar (rid_subst id)
+  let r_subst (r : region) =
+    match r with RStatic | RErased -> r | RVar id -> RVar (rid_subst id)
   in
   (* Return *)
   (fresh_region_ids, rid_subst, r_subst)
 
 (** Erase the regions in a type and perform a substitution *)
-let erase_regions_substitute_types (ty_subst : T.TypeVarId.id -> T.ty)
-    (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
-    (tr_subst : T.TraitClauseId.id -> T.trait_instance_id)
-    (tr_self : T.trait_instance_id) (ty : T.ty) : T.ty =
-  let r_subst (_ : T.region) : T.region = T.RErased in
+let erase_regions_substitute_types (ty_subst : TypeVarId.id -> ty)
+    (cg_subst : ConstGenericVarId.id -> const_generic)
+    (tr_subst : TraitClauseId.id -> trait_instance_id)
+    (tr_self : trait_instance_id) (ty : ty) : ty =
+  let r_subst (_ : region) : region = RErased in
   let subst = { r_subst; ty_subst; cg_subst; tr_subst; tr_self } in
   ty_substitute subst ty
 
 (** Create a region substitution from a list of region variable ids and a list of
     regions (with which to substitute the region variable ids *)
-let make_region_subst (var_ids : T.RegionId.id list) (regions : T.region list) :
-    T.region -> T.region =
+let make_region_subst (var_ids : RegionId.id list) (regions : region list) :
+    region -> region =
   let ls = List.combine var_ids regions in
   let mp =
     List.fold_left
-      (fun mp (k, v) -> T.RegionId.Map.add k v mp)
-      T.RegionId.Map.empty ls
+      (fun mp (k, v) -> RegionId.Map.add k v mp)
+      RegionId.Map.empty ls
   in
   fun r ->
-    match r with
-    | T.RStatic | T.RErased -> r
-    | T.RVar id -> T.RegionId.Map.find id mp
+    match r with RStatic | RErased -> r | RVar id -> RegionId.Map.find id mp
 
-let make_region_subst_from_vars (vars : T.region_var list)
-    (regions : T.region list) : T.region -> T.region =
-  make_region_subst
-    (List.map (fun (x : T.region_var) -> x.T.index) vars)
-    regions
+let make_region_subst_from_vars (vars : region_var list) (regions : region list)
+    : region -> region =
+  make_region_subst (List.map (fun (x : region_var) -> x.index) vars) regions
 
 (** Create a type substitution from a list of type variable ids and a list of
     types (with which to substitute the type variable ids) *)
-let make_type_subst (var_ids : T.TypeVarId.id list) (tys : T.ty list) :
-    T.TypeVarId.id -> T.ty =
+let make_type_subst (var_ids : TypeVarId.id list) (tys : ty list) :
+    TypeVarId.id -> ty =
   let ls = List.combine var_ids tys in
   let mp =
     List.fold_left
-      (fun mp (k, v) -> T.TypeVarId.Map.add k v mp)
-      T.TypeVarId.Map.empty ls
+      (fun mp (k, v) -> TypeVarId.Map.add k v mp)
+      TypeVarId.Map.empty ls
   in
-  fun id -> T.TypeVarId.Map.find id mp
+  fun id -> TypeVarId.Map.find id mp
 
-let make_type_subst_from_vars (vars : T.type_var list) (tys : T.ty list) :
-    T.TypeVarId.id -> T.ty =
-  make_type_subst (List.map (fun (x : T.type_var) -> x.T.index) vars) tys
+let make_type_subst_from_vars (vars : type_var list) (tys : ty list) :
+    TypeVarId.id -> ty =
+  make_type_subst (List.map (fun (x : type_var) -> x.index) vars) tys
 
 (** Create a const generic substitution from a list of const generic variable ids and a list of
     const generics (with which to substitute the const generic variable ids) *)
-let make_const_generic_subst (var_ids : T.ConstGenericVarId.id list)
-    (cgs : T.const_generic list) : T.ConstGenericVarId.id -> T.const_generic =
+let make_const_generic_subst (var_ids : ConstGenericVarId.id list)
+    (cgs : const_generic list) : ConstGenericVarId.id -> const_generic =
   let ls = List.combine var_ids cgs in
   let mp =
     List.fold_left
-      (fun mp (k, v) -> T.ConstGenericVarId.Map.add k v mp)
-      T.ConstGenericVarId.Map.empty ls
+      (fun mp (k, v) -> ConstGenericVarId.Map.add k v mp)
+      ConstGenericVarId.Map.empty ls
   in
-  fun id -> T.ConstGenericVarId.Map.find id mp
+  fun id -> ConstGenericVarId.Map.find id mp
 
-let make_const_generic_subst_from_vars (vars : T.const_generic_var list)
-    (cgs : T.const_generic list) : T.ConstGenericVarId.id -> T.const_generic =
+let make_const_generic_subst_from_vars (vars : const_generic_var list)
+    (cgs : const_generic list) : ConstGenericVarId.id -> const_generic =
   make_const_generic_subst
-    (List.map (fun (x : T.const_generic_var) -> x.T.index) vars)
+    (List.map (fun (x : const_generic_var) -> x.index) vars)
     cgs
 
 (** Create a trait substitution from a list of trait clause ids and a list of
     trait refs *)
-let make_trait_subst (clause_ids : T.TraitClauseId.id list)
-    (trs : T.trait_ref list) : T.TraitClauseId.id -> T.trait_instance_id =
+let make_trait_subst (clause_ids : TraitClauseId.id list) (trs : trait_ref list)
+    : TraitClauseId.id -> trait_instance_id =
   let ls = List.combine clause_ids trs in
   let mp =
     List.fold_left
-      (fun mp (k, v) -> T.TraitClauseId.Map.add k (T.TraitRef v) mp)
-      T.TraitClauseId.Map.empty ls
+      (fun mp (k, v) -> TraitClauseId.Map.add k (TraitRef v) mp)
+      TraitClauseId.Map.empty ls
   in
-  fun id -> T.TraitClauseId.Map.find id mp
+  fun id -> TraitClauseId.Map.find id mp
 
-let make_trait_subst_from_clauses (clauses : T.trait_clause list)
-    (trs : T.trait_ref list) : T.TraitClauseId.id -> T.trait_instance_id =
+let make_trait_subst_from_clauses (clauses : trait_clause list)
+    (trs : trait_ref list) : TraitClauseId.id -> trait_instance_id =
   make_trait_subst
-    (List.map (fun (x : T.trait_clause) -> x.T.clause_id) clauses)
+    (List.map (fun (x : trait_clause) -> x.clause_id) clauses)
     trs
 
-let make_subst_from_generics (params : T.generic_params) (args : T.generic_args)
-    (tr_self : T.trait_instance_id) : subst =
-  let r_subst = make_region_subst_from_vars params.T.regions args.T.regions in
-  let ty_subst = make_type_subst_from_vars params.T.types args.T.types in
+let make_subst_from_generics (params : generic_params) (args : generic_args)
+    (tr_self : trait_instance_id) : subst =
+  let r_subst = make_region_subst_from_vars params.regions args.regions in
+  let ty_subst = make_type_subst_from_vars params.types args.types in
   let cg_subst =
-    make_const_generic_subst_from_vars params.T.const_generics
-      args.T.const_generics
+    make_const_generic_subst_from_vars params.const_generics args.const_generics
   in
   let tr_subst =
-    make_trait_subst_from_clauses params.T.trait_clauses args.T.trait_refs
+    make_trait_subst_from_clauses params.trait_clauses args.trait_refs
   in
   { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
 
-let make_subst_from_generics_erase_regions (params : T.generic_params)
-    (generics : T.generic_args) (tr_self : T.trait_instance_id) =
+let make_subst_from_generics_erase_regions (params : generic_params)
+    (generics : generic_args) (tr_self : trait_instance_id) =
   let generics = generic_args_erase_regions generics in
   let tr_self = trait_instance_id_erase_regions tr_self in
   let subst = make_subst_from_generics params generics tr_self in
-  { subst with r_subst = (fun _ -> T.RErased) }
+  { subst with r_subst = (fun _ -> RErased) }
 
 (** Instantiate the type variables in an ADT definition, and return, for
     every variant, the list of the types of its fields.
@@ -229,27 +219,25 @@ let make_subst_from_generics_erase_regions (params : T.generic_params)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
 *)
-let type_decl_get_instantiated_variants_fields_types (def : T.type_decl)
-    (generics : T.generic_args) : (T.VariantId.id option * T.ty list) list =
+let type_decl_get_instantiated_variants_fields_types (def : type_decl)
+    (generics : generic_args) : (VariantId.id option * ty list) list =
   (* There shouldn't be any reference to Self *)
-  let tr_self = T.UnknownTrait __FUNCTION__ in
-  let subst = make_subst_from_generics def.T.generics generics tr_self in
-  let (variants_fields : (T.VariantId.id option * T.field list) list) =
-    match def.T.kind with
-    | T.Enum variants ->
-        List.mapi
-          (fun i v -> (Some (T.VariantId.of_int i), v.T.fields))
-          variants
-    | T.Struct fields -> [ (None, fields) ]
-    | T.Opaque ->
+  let tr_self = UnknownTrait __FUNCTION__ in
+  let subst = make_subst_from_generics def.generics generics tr_self in
+  let (variants_fields : (VariantId.id option * field list) list) =
+    match def.kind with
+    | Enum variants ->
+        List.mapi (fun i v -> (Some (VariantId.of_int i), v.fields)) variants
+    | Struct fields -> [ (None, fields) ]
+    | Opaque ->
         raise
           (Failure
              ("Can't retrieve the variants of an opaque type: "
-             ^ Names.name_to_string def.name))
+            ^ show_name def.name))
   in
   List.map
     (fun (id, fields) ->
-      (id, List.map (fun f -> ty_substitute subst f.T.field_ty) fields))
+      (id, List.map (fun f -> ty_substitute subst f.field_ty) fields))
     variants_fields
 
 (** Instantiate the type variables in an ADT definition, and return the list
@@ -258,17 +246,16 @@ let type_decl_get_instantiated_variants_fields_types (def : T.type_decl)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
 *)
-let type_decl_get_instantiated_field_types (def : T.type_decl)
-    (opt_variant_id : T.VariantId.id option) (generics : T.generic_args) :
-    T.ty list =
+let type_decl_get_instantiated_field_types (def : type_decl)
+    (opt_variant_id : VariantId.id option) (generics : generic_args) : ty list =
   (* For now, check that there are no clauses - otherwise we might need
      to normalize the types *)
   assert (def.generics.trait_clauses = []);
   (* There shouldn't be any reference to Self *)
-  let tr_self = T.UnknownTrait __FUNCTION__ in
-  let subst = make_subst_from_generics def.T.generics generics tr_self in
-  let fields = TU.type_decl_get_fields def opt_variant_id in
-  List.map (fun f -> ty_substitute subst f.T.field_ty) fields
+  let tr_self = UnknownTrait __FUNCTION__ in
+  let subst = make_subst_from_generics def.generics generics tr_self in
+  let fields = type_decl_get_fields def opt_variant_id in
+  List.map (fun f -> ty_substitute subst f.field_ty) fields
 
 (** Return the types of the properly instantiated ADT's variant, provided a
     context.
@@ -276,10 +263,10 @@ let type_decl_get_instantiated_field_types (def : T.type_decl)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
 *)
-let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx)
-    (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (generics : T.generic_args) : T.ty list =
-  let def = C.ctx_lookup_type_decl ctx def_id in
+let ctx_adt_get_instantiated_field_types (ctx : eval_ctx)
+    (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option)
+    (generics : generic_args) : ty list =
+  let def = ctx_lookup_type_decl ctx def_id in
   type_decl_get_instantiated_field_types def opt_variant_id generics
 
 (** Return the types of the properly instantiated ADT value (note that
@@ -288,98 +275,94 @@ let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
  *)
-let ctx_adt_value_get_instantiated_field_types (ctx : C.eval_ctx)
-    (adt : V.adt_value) (id : T.type_id) (generics : T.generic_args) : T.ty list
-    =
+let ctx_adt_value_get_instantiated_field_types (ctx : eval_ctx)
+    (adt : adt_value) (id : type_id) (generics : generic_args) : ty list =
   match id with
-  | T.TAdtId id ->
+  | TAdtId id ->
       (* Retrieve the types of the fields *)
-      ctx_adt_get_instantiated_field_types ctx id adt.V.variant_id generics
-  | T.TTuple ->
+      ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics
+  | TTuple ->
       assert (generics.regions = []);
       generics.types
-  | T.TAssumed aty -> (
+  | TAssumed aty -> (
       match aty with
-      | T.TBox ->
+      | TBox ->
           assert (generics.regions = []);
           assert (List.length generics.types = 1);
           assert (generics.const_generics = []);
           generics.types
-      | T.TArray | T.TSlice | T.TStr ->
+      | TArray | TSlice | TStr ->
           (* Those types don't have fields *)
           raise (Failure "Unreachable"))
 
 (** Apply a type substitution to a place *)
-let place_substitute (subst : subst) (p : E.place) : E.place =
+let place_substitute (subst : subst) (p : place) : place =
   (* There is in fact nothing to do *)
   (st_substitute_visitor subst)#visit_place () p
 
 (** Apply a type substitution to an operand *)
-let operand_substitute (subst : subst) (op : E.operand) : E.operand =
+let operand_substitute (subst : subst) (op : operand) : operand =
   (st_substitute_visitor subst)#visit_operand () op
 
 (** Apply a type substitution to an rvalue *)
-let rvalue_substitute (subst : subst) (rv : E.rvalue) : E.rvalue =
+let rvalue_substitute (subst : subst) (rv : rvalue) : rvalue =
   (st_substitute_visitor subst)#visit_rvalue () rv
 
 (** Apply a type substitution to an assertion *)
-let assertion_substitute (subst : subst) (a : A.assertion) : A.assertion =
+let assertion_substitute (subst : subst) (a : assertion) : assertion =
   (st_substitute_visitor subst)#visit_assertion () a
 
 (** Apply a type substitution to a call *)
-let call_substitute (subst : subst) (call : A.call) : A.call =
+let call_substitute (subst : subst) (call : call) : call =
   (st_substitute_visitor subst)#visit_call () call
 
 (** Apply a type substitution to a statement *)
-let statement_substitute (subst : subst) (st : A.statement) : A.statement =
+let statement_substitute (subst : subst) (st : statement) : statement =
   (st_substitute_visitor subst)#visit_statement () st
 
 (** Apply a type substitution to a function body. Return the local variables
     and the body. *)
-let fun_body_substitute_in_body (subst : subst) (body : A.fun_body) :
-    A.var list * A.statement =
+let fun_body_substitute_in_body (subst : subst) (body : fun_body) :
+    var list * statement =
   let locals =
     List.map
-      (fun (v : A.var) -> { v with A.var_ty = ty_substitute subst v.A.var_ty })
-      body.A.locals
+      (fun (v : var) -> { v with var_ty = ty_substitute subst v.var_ty })
+      body.locals
   in
   let body = statement_substitute subst body.body in
   (locals, body)
 
 let trait_type_constraint_substitute (subst : subst)
-    (ttc : T.trait_type_constraint) : T.trait_type_constraint =
-  let { T.trait_ref; generics; type_name; ty } = ttc in
+    (ttc : trait_type_constraint) : trait_type_constraint =
+  let { trait_ref; generics; type_name; ty } = ttc in
   let visitor = st_substitute_visitor subst in
   let trait_ref = visitor#visit_trait_ref () trait_ref in
   let generics = visitor#visit_generic_args () generics in
   let ty = visitor#visit_ty () ty in
-  { T.trait_ref; generics; type_name; ty }
+  { trait_ref; generics; type_name; ty }
 
 (** Substitute a function signature, together with the regions hierarchy
     associated to that signature.
 
     **IMPORTANT:** this function doesn't normalize the types.
  *)
-let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
-    (r_subst : T.RegionId.id -> T.RegionId.id)
-    (ty_subst : T.TypeVarId.id -> T.ty)
-    (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
-    (tr_subst : T.TraitClauseId.id -> T.trait_instance_id)
-    (tr_self : T.trait_instance_id) (sg : A.fun_sig)
-    (regions_hierarchy : T.region_groups) : A.inst_fun_sig =
-  let r_subst' (r : T.region) : T.region =
-    match r with
-    | T.RStatic | T.RErased -> r
-    | T.RVar rid -> T.RVar (r_subst rid)
+let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id)
+    (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
+    (cg_subst : ConstGenericVarId.id -> const_generic)
+    (tr_subst : TraitClauseId.id -> trait_instance_id)
+    (tr_self : trait_instance_id) (sg : fun_sig)
+    (regions_hierarchy : region_groups) : inst_fun_sig =
+  let r_subst' (r : region) : region =
+    match r with RStatic | RErased -> r | RVar rid -> RVar (r_subst rid)
   in
   let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in
-  let inputs = List.map (ty_substitute subst) sg.A.inputs in
-  let output = ty_substitute subst sg.A.output in
-  let subst_region_group (rg : T.region_group) : A.abs_region_group =
+  let inputs = List.map (ty_substitute subst) sg.inputs in
+  let output = ty_substitute subst sg.output in
+  let subst_region_group (rg : region_group) : abs_region_group =
     let id = asubst rg.id in
     let regions = List.map r_subst rg.regions in
     let parents = List.map asubst rg.parents in
-    ({ id; regions; parents } : A.abs_region_group)
+    ({ id; regions; parents } : abs_region_group)
   in
   let regions_hierarchy = List.map subst_region_group regions_hierarchy in
   let trait_type_constraints =
@@ -387,13 +370,11 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
       (trait_type_constraint_substitute subst)
       sg.preds.trait_type_constraints
   in
-  { A.inputs; output; regions_hierarchy; trait_type_constraints }
+  { inputs; output; regions_hierarchy; trait_type_constraints }
 
 (** Substitute variable identifiers in a type *)
-let statement_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : T.ty) :
-    T.ty =
-  let open T in
+let statement_substitute_ids (ty_subst : TypeVarId.id -> TypeVarId.id)
+    (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ty : ty) : ty =
   let visitor =
     object
       inherit [_] map_ty
@@ -405,14 +386,14 @@ let statement_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
 
   visitor#visit_ty () ty
 
-let subst_ids_visitor (r_subst : T.RegionId.id -> T.RegionId.id)
-    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
-    (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
-    (bsubst : V.BorrowId.id -> V.BorrowId.id)
-    (asubst : V.AbstractionId.id -> V.AbstractionId.id) =
+let subst_ids_visitor (r_subst : RegionId.id -> RegionId.id)
+    (ty_subst : TypeVarId.id -> TypeVarId.id)
+    (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id)
+    (ssubst : SymbolicValueId.id -> SymbolicValueId.id)
+    (bsubst : BorrowId.id -> BorrowId.id)
+    (asubst : AbstractionId.id -> AbstractionId.id) =
   object (self : 'self)
-    inherit [_] C.map_env
+    inherit [_] map_env
     method! visit_type_var_id _ id = ty_subst id
     method! visit_const_generic_var_id _ id = cg_subst id
     method! visit_region_id _ rid = r_subst rid
@@ -429,18 +410,17 @@ let subst_ids_visitor (r_subst : T.RegionId.id -> T.RegionId.id)
     method! visit_abstraction_id _ id = asubst id
   end
 
-let typed_value_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
-    (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
-    (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_value) :
-    V.typed_value =
+let typed_value_subst_ids (r_subst : RegionId.id -> RegionId.id)
+    (ty_subst : TypeVarId.id -> TypeVarId.id)
+    (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id)
+    (ssubst : SymbolicValueId.id -> SymbolicValueId.id)
+    (bsubst : BorrowId.id -> BorrowId.id) (v : typed_value) : typed_value =
   let asubst _ = raise (Failure "Unreachable") in
   let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
   vis#visit_typed_value () v
 
-let typed_value_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (v : V.typed_value) : V.typed_value =
+let typed_value_subst_rids (r_subst : RegionId.id -> RegionId.id)
+    (v : typed_value) : typed_value =
   typed_value_subst_ids r_subst
     (fun x -> x)
     (fun x -> x)
@@ -448,36 +428,35 @@ let typed_value_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
     (fun x -> x)
     v
 
-let typed_avalue_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
-    (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
-    (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_avalue) :
-    V.typed_avalue =
+let typed_avalue_subst_ids (r_subst : RegionId.id -> RegionId.id)
+    (ty_subst : TypeVarId.id -> TypeVarId.id)
+    (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id)
+    (ssubst : SymbolicValueId.id -> SymbolicValueId.id)
+    (bsubst : BorrowId.id -> BorrowId.id) (v : typed_avalue) : typed_avalue =
   let asubst _ = raise (Failure "Unreachable") in
   let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
   vis#visit_typed_avalue () v
 
-let abs_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
-    (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
-    (bsubst : V.BorrowId.id -> V.BorrowId.id)
-    (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : V.abs) : V.abs =
+let abs_subst_ids (r_subst : RegionId.id -> RegionId.id)
+    (ty_subst : TypeVarId.id -> TypeVarId.id)
+    (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id)
+    (ssubst : SymbolicValueId.id -> SymbolicValueId.id)
+    (bsubst : BorrowId.id -> BorrowId.id)
+    (asubst : AbstractionId.id -> AbstractionId.id) (x : abs) : abs =
   let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
   vis#visit_abs () x
 
-let env_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
-    (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
-    (bsubst : V.BorrowId.id -> V.BorrowId.id)
-    (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : C.env) : C.env =
+let env_subst_ids (r_subst : RegionId.id -> RegionId.id)
+    (ty_subst : TypeVarId.id -> TypeVarId.id)
+    (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id)
+    (ssubst : SymbolicValueId.id -> SymbolicValueId.id)
+    (bsubst : BorrowId.id -> BorrowId.id)
+    (asubst : AbstractionId.id -> AbstractionId.id) (x : env) : env =
   let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
   vis#visit_env () x
 
-let typed_avalue_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
-    (x : V.typed_avalue) : V.typed_avalue =
+let typed_avalue_subst_rids (r_subst : RegionId.id -> RegionId.id)
+    (x : typed_avalue) : typed_avalue =
   let asubst _ = raise (Failure "Unreachable") in
   let vis =
     subst_ids_visitor r_subst
@@ -489,8 +468,7 @@ let typed_avalue_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
   in
   vis#visit_typed_avalue () x
 
-let env_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id) (x : C.env) :
-    C.env =
+let env_subst_rids (r_subst : RegionId.id -> RegionId.id) (x : env) : env =
   let vis =
     subst_ids_visitor r_subst
       (fun x -> x)
-- 
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/Substitute.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 01509dec..73e7f71d 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -29,7 +29,7 @@ let st_substitute_visitor (subst : subst) =
       (* We should never get here because we reimplemented [visit_TypeVar] *)
       raise (Failure "Unexpected")
 
-    method! visit_CGVar _ id = subst.cg_subst id
+    method! visit_CgVar _ id = subst.cg_subst id
 
     method! visit_const_generic_var_id _ _ =
       (* We should never get here because we reimplemented [visit_Var] *)
@@ -71,7 +71,7 @@ let erase_regions_subst : subst =
   {
     r_subst = (fun _ -> RErased);
     ty_subst = (fun vid -> TVar vid);
-    cg_subst = (fun id -> CGVar id);
+    cg_subst = (fun id -> CgVar id);
     tr_subst = (fun id -> Clause id);
     tr_self = Self;
   }
-- 
cgit v1.2.3


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

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

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 73e7f71d..a05b2c5a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -76,7 +76,7 @@ let erase_regions_subst : subst =
     tr_self = Self;
   }
 
-(** Convert an {!rty} to an {!ety} by erasing the region variables *)
+(** Erase the region variables in a type *)
 let erase_regions (ty : ty) : ty = ty_substitute erase_regions_subst ty
 
 let trait_ref_erase_regions (tr : trait_ref) : trait_ref =
-- 
cgit v1.2.3


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

---
 compiler/Substitute.ml | 120 ++++++++++++++++++++++++++++++++++---------------
 1 file changed, 84 insertions(+), 36 deletions(-)

(limited to 'compiler/Substitute.ml')

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index a05b2c5a..e28f005d 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -11,6 +11,9 @@ open Contexts
 
 type subst = {
   r_subst : region -> region;
+      (** Remark: this might be called with bound regions with a negative
+          DeBruijn index. A negative DeBruijn index means that the region
+          is locally bound. *)
   ty_subst : TypeVarId.id -> ty;
   cg_subst : ConstGenericVarId.id -> const_generic;
       (** Substitution from *local* trait clause to trait instance *)
@@ -19,11 +22,35 @@ type subst = {
   tr_self : trait_instance_id;
 }
 
+let empty_subst : subst =
+  {
+    r_subst = (fun x -> x);
+    ty_subst = (fun id -> TVar id);
+    cg_subst = (fun id -> CgVar id);
+    tr_subst = (fun id -> Clause id);
+    tr_self = Self;
+  }
+
 let st_substitute_visitor (subst : subst) =
-  object
+  object (self)
     inherit [_] map_statement
-    method! visit_region _ r = subst.r_subst r
-    method! visit_TVar _ id = subst.ty_subst id
+    method! visit_region (subst : subst) r = subst.r_subst r
+
+    (** We need to properly handle the DeBruijn indices *)
+    method! visit_TArrow subst regions inputs output =
+      (* Decrement the DeBruijn indices before calling the substitution *)
+      let r_subst r =
+        match r with
+        | RBVar (db, rid) -> subst.r_subst (RBVar (db - 1, rid))
+        | _ -> subst.r_subst r
+      in
+      let subst = { subst with r_subst } in
+      (* Note that we ignore the bound regions variables *)
+      let inputs = List.map (self#visit_ty subst) inputs in
+      let output = self#visit_ty subst output in
+      TArrow (regions, inputs, output)
+
+    method! visit_TVar (subst : subst) id = subst.ty_subst id
 
     method! visit_type_var_id _ _ =
       (* We should never get here because we reimplemented [visit_TypeVar] *)
@@ -35,8 +62,8 @@ let st_substitute_visitor (subst : subst) =
       (* We should never get here because we reimplemented [visit_Var] *)
       raise (Failure "Unexpected")
 
-    method! visit_Clause _ id = subst.tr_subst id
-    method! visit_Self _ = subst.tr_self
+    method! visit_Clause (subst : subst) id = subst.tr_subst id
+    method! visit_Self (subst : subst) = subst.tr_self
   end
 
 (** Substitute types variables and regions in a type.
@@ -45,27 +72,27 @@ let st_substitute_visitor (subst : subst) =
  *)
 let ty_substitute (subst : subst) (ty : ty) : ty =
   let visitor = st_substitute_visitor subst in
-  visitor#visit_ty () ty
+  visitor#visit_ty subst ty
 
 (** **IMPORTANT**: this doesn't normalize the types. *)
 let trait_ref_substitute (subst : subst) (tr : trait_ref) : trait_ref =
   let visitor = st_substitute_visitor subst in
-  visitor#visit_trait_ref () tr
+  visitor#visit_trait_ref subst tr
 
 (** **IMPORTANT**: this doesn't normalize the types. *)
 let trait_instance_id_substitute (subst : subst) (tr : trait_instance_id) :
     trait_instance_id =
   let visitor = st_substitute_visitor subst in
-  visitor#visit_trait_instance_id () tr
+  visitor#visit_trait_instance_id subst tr
 
 (** **IMPORTANT**: this doesn't normalize the types. *)
 let generic_args_substitute (subst : subst) (g : generic_args) : generic_args =
   let visitor = st_substitute_visitor subst in
-  visitor#visit_generic_args () g
+  visitor#visit_generic_args subst g
 
 let predicates_substitute (subst : subst) (p : predicates) : predicates =
   let visitor = st_substitute_visitor subst in
-  visitor#visit_predicates () p
+  visitor#visit_predicates subst p
 
 let erase_regions_subst : subst =
   {
@@ -96,26 +123,40 @@ let generic_args_erase_regions (tr : generic_args) : generic_args =
     
     TODO: simplify? we only need the subst [RegionVarId.id -> RegionId.id]
   *)
-let fresh_regions_with_substs (region_vars : region_var list) :
-    RegionId.id list * (RegionId.id -> RegionId.id) * (region -> region) =
+let fresh_regions_with_substs ~(fail_if_not_found : bool)
+    (region_vars : RegionVarId.id list) :
+    RegionId.id list
+    * (RegionVarId.id -> RegionId.id option)
+    * (region -> region) =
   (* Generate fresh regions *)
   let fresh_region_ids = List.map (fun _ -> fresh_region_id ()) region_vars in
   (* Generate the map from region var ids to regions *)
   let ls = List.combine region_vars fresh_region_ids in
-  let rid_map =
-    List.fold_left
-      (fun mp ((k : region_var), v) -> RegionId.Map.add k.index v mp)
-      RegionId.Map.empty ls
-  in
+  let rid_map = RegionVarId.Map.of_list ls in
   (* Generate the substitution from region var id to region *)
-  let rid_subst id = RegionId.Map.find id rid_map in
+  let rid_subst id = RegionVarId.Map.find_opt id rid_map in
   (* Generate the substitution from region to region *)
   let r_subst (r : region) =
-    match r with RStatic | RErased -> r | RVar id -> RVar (rid_subst id)
+    match r with
+    | RStatic | RErased | RFVar _ -> r
+    | RBVar (bdid, id) ->
+        if bdid = 0 then
+          match rid_subst id with
+          | None -> if fail_if_not_found then raise Not_found else r
+          | Some r -> RFVar r
+        else r
   in
   (* Return *)
   (fresh_region_ids, rid_subst, r_subst)
 
+let fresh_regions_with_substs_from_vars ~(fail_if_not_found : bool)
+    (region_vars : region_var list) :
+    RegionId.id list
+    * (RegionVarId.id -> RegionId.id option)
+    * (region -> region) =
+  fresh_regions_with_substs ~fail_if_not_found
+    (List.map (fun (r : region_var) -> r.index) region_vars)
+
 (** Erase the regions in a type and perform a substitution *)
 let erase_regions_substitute_types (ty_subst : TypeVarId.id -> ty)
     (cg_subst : ConstGenericVarId.id -> const_generic)
@@ -127,16 +168,21 @@ let erase_regions_substitute_types (ty_subst : TypeVarId.id -> ty)
 
 (** Create a region substitution from a list of region variable ids and a list of
     regions (with which to substitute the region variable ids *)
-let make_region_subst (var_ids : RegionId.id list) (regions : region list) :
+let make_region_subst (var_ids : RegionVarId.id list) (regions : region list) :
     region -> region =
   let ls = List.combine var_ids regions in
   let mp =
     List.fold_left
-      (fun mp (k, v) -> RegionId.Map.add k v mp)
-      RegionId.Map.empty ls
+      (fun mp (k, v) -> RegionVarId.Map.add k v mp)
+      RegionVarId.Map.empty ls
   in
   fun r ->
-    match r with RStatic | RErased -> r | RVar id -> RegionId.Map.find id mp
+    match r with
+    | RStatic | RErased -> r
+    | RFVar _ -> raise (Failure "Unexpected")
+    | RBVar (bdid, id) ->
+        (* Only substitute the bound regions with DeBruijn index equal to 0 *)
+        if bdid = 0 then RegionVarId.Map.find id mp else r
 
 let make_region_subst_from_vars (vars : region_var list) (regions : region list)
     : region -> region =
@@ -298,27 +344,27 @@ let ctx_adt_value_get_instantiated_field_types (ctx : eval_ctx)
 (** Apply a type substitution to a place *)
 let place_substitute (subst : subst) (p : place) : place =
   (* There is in fact nothing to do *)
-  (st_substitute_visitor subst)#visit_place () p
+  (st_substitute_visitor subst)#visit_place subst p
 
 (** Apply a type substitution to an operand *)
 let operand_substitute (subst : subst) (op : operand) : operand =
-  (st_substitute_visitor subst)#visit_operand () op
+  (st_substitute_visitor subst)#visit_operand subst op
 
 (** Apply a type substitution to an rvalue *)
 let rvalue_substitute (subst : subst) (rv : rvalue) : rvalue =
-  (st_substitute_visitor subst)#visit_rvalue () rv
+  (st_substitute_visitor subst)#visit_rvalue subst rv
 
 (** Apply a type substitution to an assertion *)
 let assertion_substitute (subst : subst) (a : assertion) : assertion =
-  (st_substitute_visitor subst)#visit_assertion () a
+  (st_substitute_visitor subst)#visit_assertion subst a
 
 (** Apply a type substitution to a call *)
 let call_substitute (subst : subst) (call : call) : call =
-  (st_substitute_visitor subst)#visit_call () call
+  (st_substitute_visitor subst)#visit_call subst call
 
 (** Apply a type substitution to a statement *)
 let statement_substitute (subst : subst) (st : statement) : statement =
-  (st_substitute_visitor subst)#visit_statement () st
+  (st_substitute_visitor subst)#visit_statement subst st
 
 (** Apply a type substitution to a function body. Return the local variables
     and the body. *)
@@ -336,9 +382,9 @@ let trait_type_constraint_substitute (subst : subst)
     (ttc : trait_type_constraint) : trait_type_constraint =
   let { trait_ref; generics; type_name; ty } = ttc in
   let visitor = st_substitute_visitor subst in
-  let trait_ref = visitor#visit_trait_ref () trait_ref in
-  let generics = visitor#visit_generic_args () generics in
-  let ty = visitor#visit_ty () ty in
+  let trait_ref = visitor#visit_trait_ref subst trait_ref in
+  let generics = visitor#visit_generic_args subst generics in
+  let ty = visitor#visit_ty subst ty in
   { trait_ref; generics; type_name; ty }
 
 (** Substitute a function signature, together with the regions hierarchy
@@ -347,18 +393,20 @@ let trait_type_constraint_substitute (subst : subst)
     **IMPORTANT:** this function doesn't normalize the types.
  *)
 let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id)
-    (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
+    (r_subst : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
     (cg_subst : ConstGenericVarId.id -> const_generic)
     (tr_subst : TraitClauseId.id -> trait_instance_id)
     (tr_self : trait_instance_id) (sg : fun_sig)
-    (regions_hierarchy : region_groups) : inst_fun_sig =
+    (regions_hierarchy : region_var_groups) : inst_fun_sig =
   let r_subst' (r : region) : region =
-    match r with RStatic | RErased -> r | RVar rid -> RVar (r_subst rid)
+    match r with
+    | RStatic | RErased | RFVar _ -> r
+    | RBVar (bdid, rid) -> if bdid = 0 then RFVar (r_subst rid) else r
   in
   let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in
   let inputs = List.map (ty_substitute subst) sg.inputs in
   let output = ty_substitute subst sg.output in
-  let subst_region_group (rg : region_group) : abs_region_group =
+  let subst_region_group (rg : region_var_group) : abs_region_group =
     let id = asubst rg.id in
     let regions = List.map r_subst rg.regions in
     let parents = List.map asubst rg.parents in
-- 
cgit v1.2.3