Merge remote-tracking branch 'origin/main' into son_merge_back2

2 files changed, 22 insertions, 336 deletions

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index e28f005d..dbd310b7 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -2,120 +2,12 @@
     function bodies, etc.
  *)
 
+include Charon.Substitute
 open Types
-open TypesUtils
 open Values
-open Expressions
 open LlbcAst
 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 *)
-  tr_subst : TraitClauseId.id -> trait_instance_id;
-      (** Substitution for the [Self] trait instance *)
-  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 (self)
-    inherit [_] map_statement
-    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] *)
-      raise (Failure "Unexpected")
-
-    method! visit_CgVar _ 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 (subst : subst) id = subst.tr_subst id
-    method! visit_Self (subst : subst) = subst.tr_self
-  end
-
-(** Substitute types variables and regions in a type.
-
-    **IMPORTANT**: this doesn't normalize the types.
- *)
-let ty_substitute (subst : subst) (ty : ty) : ty =
-  let visitor = st_substitute_visitor subst in
-  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 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 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 subst g
-
-let predicates_substitute (subst : subst) (p : predicates) : predicates =
-  let visitor = st_substitute_visitor subst in
-  visitor#visit_predicates subst p
-
-let erase_regions_subst : subst =
-  {
-    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;
-  }
-
-(** 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 =
-  trait_ref_substitute erase_regions_subst tr
-
-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 : generic_args) : 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
@@ -157,152 +49,6 @@ let fresh_regions_with_substs_from_vars ~(fail_if_not_found : bool)
   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)
-    (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 : 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) -> RegionVarId.Map.add k v mp)
-      RegionVarId.Map.empty ls
-  in
-  fun r ->
-    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 =
-  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 : 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) -> TypeVarId.Map.add k v mp)
-      TypeVarId.Map.empty ls
-  in
-  fun id -> TypeVarId.Map.find id mp
-
-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 : 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) -> ConstGenericVarId.Map.add k v mp)
-      ConstGenericVarId.Map.empty ls
-  in
-  fun id -> ConstGenericVarId.Map.find id mp
-
-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 : 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 : 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) -> TraitClauseId.Map.add k (TraitRef v) mp)
-      TraitClauseId.Map.empty ls
-  in
-  fun id -> TraitClauseId.Map.find id mp
-
-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 : trait_clause) -> x.clause_id) clauses)
-    trs
-
-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.const_generics args.const_generics
-  in
-  let tr_subst =
-    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 : 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 _ -> RErased) }
-
-(** 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_types (def : type_decl)
-    (generics : generic_args) : (VariantId.id option * ty list) list =
-  (* There shouldn't be any reference to Self *)
-  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: "
-            ^ show_name def.name))
-  in
-  List.map
-    (fun (id, 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
-    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_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 = 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.
 
@@ -341,52 +87,6 @@ let ctx_adt_value_get_instantiated_field_types (ctx : eval_ctx)
           (* Those types don't have fields *)
           raise (Failure "Unreachable"))
 
-(** 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 subst p
-
-(** Apply a type substitution to an operand *)
-let operand_substitute (subst : subst) (op : operand) : operand =
-  (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 subst rv
-
-(** Apply a type substitution to an assertion *)
-let assertion_substitute (subst : subst) (a : assertion) : assertion =
-  (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 subst call
-
-(** Apply a type substitution to a statement *)
-let statement_substitute (subst : subst) (st : statement) : statement =
-  (st_substitute_visitor subst)#visit_statement subst 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 : fun_body) :
-    var list * statement =
-  let locals =
-    List.map
-      (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 : 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 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
     associated to that signature.
 
@@ -420,20 +120,6 @@ let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id)
   in
   { inputs; output; regions_hierarchy; trait_type_constraints }
 
-(** Substitute variable identifiers in a type *)
-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
-      method visit_'r _ r = r
-      method! visit_type_var_id _ id = ty_subst id
-      method! visit_const_generic_var_id _ id = cg_subst id
-    end
-  in
-
-  visitor#visit_ty () ty
-
 let subst_ids_visitor (r_subst : RegionId.id -> RegionId.id)
     (ty_subst : TypeVarId.id -> TypeVarId.id)
     (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id)
diff --git a/flake.lock b/flake.lock
index 4437f543..94159200 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1701959392,
-        "narHash": "sha256-R38NTAxnQVeMoFnaA0uZJX+WZpZ9hW+nI2GU7Cu2aCs=",
+        "lastModified": 1702401937,
+        "narHash": "sha256-PHm8BLp2S5Q1iaKOJOrn6/5nuQfxzwUcIFEgXJzNhBM=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "6130c2d04fe72e4873a8c69569f6cb8a2a698a0a",
+        "rev": "45fd166933d7d30e73eae8150192ff4cc1e123df",
         "type": "github"
       },
       "original": {
@@ -131,11 +131,11 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1701837164,
-        "narHash": "sha256-xmrOPtQ+s6h255lE56i1NSD/gLQH1QkmGmuKfFyZqNY=",
+        "lastModified": 1702080800,
+        "narHash": "sha256-PbuXUutqI5iE0ZFCJPWjgfxYjonX9Pkw/qtpLMLwXuI=",
         "owner": "fstarlang",
         "repo": "fstar",
-        "rev": "b67ab3287ddd1585f1e7c2828867c3e60664c6b2",
+        "rev": "178e0f872b6a7540d6024b49c7c04ba451f7c4c7",
         "type": "github"
       },
       "original": {
@@ -164,11 +164,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1701873981,
-        "narHash": "sha256-ljpSstynhXnNKNyix2mEKnc+knECK9h0oQxl3Fl3dsU=",
+        "lastModified": 1701972757,
+        "narHash": "sha256-sfzmasc8uIc2COYC8xm1bchmNAV5+W8gkflUVzzBDms=",
         "owner": "hacl-star",
         "repo": "hacl-star",
-        "rev": "397295a9749107052c0104140a5a8f5304fe63ee",
+        "rev": "f280ff8fe0f285edcc25c35a811dea0c233e3482",
         "type": "github"
       },
       "original": {
@@ -194,11 +194,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1701911783,
-        "narHash": "sha256-9n1cGWBaT/iak4b/XX3cgzMp9m4YcNfGXOTW2Sd/wLA=",
+        "lastModified": 1702084487,
+        "narHash": "sha256-4P2DOWqCbx5lcMdU6gMskIs9gvOiO3ZpGBMeqNhrva0=",
         "owner": "hacl-star",
         "repo": "hacl-nix",
-        "rev": "18736d6bed1efbafdff4cfb1150d0fd3d9f20f63",
+        "rev": "44aad8f5d2880e8b8fac54e4ba9cbdb315282751",
         "type": "github"
       },
       "original": {
@@ -223,11 +223,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1701663122,
-        "narHash": "sha256-iGIl1cFVIC24o/5zrOzqGrLr3GF1+ktLba8j3/UeNQA=",
+        "lastModified": 1701984397,
+        "narHash": "sha256-uR77IRrczr80J7LyFIeTrfueh8+AfBecZDDo+Pfl/a4=",
         "owner": "fstarlang",
         "repo": "karamel",
-        "rev": "0644e20d7c24958e5de3aeedc47bcda0fd2bf85d",
+        "rev": "ed6d9729569515ce55c683ebd10449543610624e",
         "type": "github"
       },
       "original": {
@@ -265,11 +265,11 @@
         "nixpkgs": "nixpkgs_4"
       },
       "locked": {
-        "lastModified": 1701940126,
-        "narHash": "sha256-evKYwrUG78vAFkRxOB5KoUX+UiI7Z6z73VAlF9l4IQQ=",
+        "lastModified": 1702429677,
+        "narHash": "sha256-i618pOqR5RdWmDdUvOCVn7MlyiF3REouq2W/SkXYHeo=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "f2a92f3331aff91540be44a3c7288b3d647934c6",
+        "rev": "2f216b52550e7b12b342d6b1717897ad3630ae63",
         "type": "github"
       },
       "original": {
@@ -318,11 +318,11 @@
         "nixpkgs": "nixpkgs_7"
       },
       "locked": {
-        "lastModified": 1701940126,
-        "narHash": "sha256-evKYwrUG78vAFkRxOB5KoUX+UiI7Z6z73VAlF9l4IQQ=",
+        "lastModified": 1702429677,
+        "narHash": "sha256-i618pOqR5RdWmDdUvOCVn7MlyiF3REouq2W/SkXYHeo=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "f2a92f3331aff91540be44a3c7288b3d647934c6",
+        "rev": "2f216b52550e7b12b342d6b1717897ad3630ae63",
         "type": "github"
       },
       "original": {