Update to new substitution API

AeneasVerif · Dec 11, 2024 · 1dc1fb7 · 1dc1fb7
1 parent 5987ef4
commit 1dc1fb7
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 23 deletions.
diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml
@@ -287,13 +287,8 @@ let get_builtin_function_return_type (span : Meta.span) (ctx : eval_ctx)
   (* There shouldn't be any reference to Self *)
   let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
   let generics = Subst.generic_args_erase_regions generics in
-  let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
-    Subst.make_subst_from_generics sg.generics generics tr_self
-  in
-  let ty =
-    Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
-      sg.output
-  in
+  let subst = Subst.make_subst_from_generics sg.generics generics tr_self in
+  let ty = Subst.erase_regions_substitute_types subst sg.output in
   AssociatedTypes.ctx_normalize_erase_ty span ctx ty
 
 let move_return_value (config : config) (span : Meta.span)
@@ -845,13 +840,8 @@ let eval_global_as_fresh_symbolic_value (span : Meta.span)
   (* There shouldn't be any reference to Self *)
   let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
   let generics = Subst.generic_args_erase_regions generics in
-  let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
-    Subst.make_subst_from_generics global.generics generics tr_self
-  in
-  let ty =
-    Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
-      global.ty
-  in
+  let subst = Subst.make_subst_from_generics global.generics generics tr_self in
+  let ty = Subst.erase_regions_substitute_types subst global.ty in
   mk_fresh_symbolic_value span ty
 
 (** Evaluate a statement *)

diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml
@@ -38,21 +38,21 @@ let fresh_regions_with_substs_from_vars (region_vars : region_var list)
     **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)
-    (cg_subst : ConstGenericVarId.id -> const_generic)
-    (tr_subst : TraitClauseId.id -> trait_instance_id)
-    (tr_self : trait_instance_id) (sg : fun_sig)
+    (r_id_subst : RegionId.id -> RegionId.id) (ty_sb_subst : TypeVarId.id -> ty)
+    (cg_sb_subst : ConstGenericVarId.id -> const_generic)
+    (tr_sb_subst : TraitClauseId.id -> trait_instance_id)
+    (tr_sb_self : trait_instance_id) (sg : fun_sig)
     (regions_hierarchy : region_var_groups) : inst_fun_sig =
-  let r_subst' = function
-    | Bound _ as var -> RVar var
-    | Free id -> RVar (Free (r_subst id))
+  let r_sb_subst id = RVar (Free (r_id_subst id)) in
+  let subst =
+    subst_free_vars
+      { r_sb_subst; ty_sb_subst; cg_sb_subst; tr_sb_subst; tr_sb_self }
   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_var_group) : abs_region_group =
     let id = asubst rg.id in
-    let regions = List.map r_subst rg.regions in
+    let regions = List.map r_id_subst rg.regions in
     let parents = List.map asubst rg.parents in
     ({ id; regions; parents } : abs_region_group)
   in