From f3982cbe9782405b50b04c948ba7cb0bd89ef85f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 18:20:24 +0100
Subject: Make the symbolic, borrow, region and abstration counters global and
 stateful

---
 src/Contexts.ml               | 63 ++++++++++++++++++++++++++---------------
 src/Identifiers.ml            | 11 ++++++++
 src/Interpreter.ml            | 11 ++------
 src/InterpreterBorrows.ml     |  9 +++---
 src/InterpreterExpansion.ml   | 65 +++++++++++++++++++------------------------
 src/InterpreterExpressions.ml |  8 +++---
 src/InterpreterPaths.ml       |  2 +-
 src/InterpreterProjectors.ml  |  8 +-----
 src/InterpreterStatements.ml  | 12 ++++----
 src/InterpreterUtils.ml       |  7 ++---
 src/Substitute.ml             | 12 +++-----
 11 files changed, 104 insertions(+), 104 deletions(-)

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 5225645c..f8a7b56b 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -3,6 +3,46 @@ open Values
 open CfimAst
 module V = Values
 
+(** Some global counters.
+ *
+ * Note that those counters were initially stored in [eval_ctx] values,
+ * but it proved better to make them global and stateful:
+ * - when branching (and thus executing on several paths with different
+ *   contexts) it is better to really have unique ids everywhere (and
+ *   not have fresh ids shared by several contexts even though introduced
+ *   after the branching) because at some point we might need to merge the
+ *   different contexts
+ * - also, it is a lot more convenient to not store those counters in contexts
+ *   objects
+ *)
+
+let symbolic_value_id_counter, fresh_symbolic_value_id =
+  SymbolicValueId.fresh_stateful_generator ()
+
+let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator ()
+
+let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()
+
+let abstraction_id_counter, fresh_abstraction_id =
+  AbstractionId.fresh_stateful_generator ()
+
+(** We shouldn't need to reset the global counters, but it might be good to
+    to it from time to time, every time we evaluate/synthesize a function for
+    instance.
+    
+    The reasons are manifold:
+    - it might prevent the counters from overflowing (although this seems
+      extremely unlikely - as a side node: we have overflow checks to make
+      sure the synthesis doesn't get impacted by potential overflows)
+    - most importantly, it allows to always manipulate low values, which
+      is always a lot more readable when debugging
+ *)
+let reset_global_counters () =
+  symbolic_value_id_counter := SymbolicValueId.generator_zero;
+  borrow_id_counter := BorrowId.generator_zero;
+  region_id_counter := RegionId.generator_zero;
+  abstraction_id_counter := AbstractionId.generator_zero
+
 type binder = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;  (** Possible name *)
@@ -68,33 +108,10 @@ type eval_ctx = {
   type_vars : type_var list;
   env : env;
   ended_regions : RegionId.set_t;
-  symbolic_counter : SymbolicValueId.generator;
-  (* TODO: make this global? *)
-  borrow_counter : BorrowId.generator;
-  (* TODO: make this global? *)
-  region_counter : RegionId.generator;
-  (* TODO: make this global? *)
-  abstraction_counter : AbstractionId.generator; (* TODO: make this global? *)
 }
 [@@deriving show]
 (** Evaluation context *)
 
-let fresh_symbolic_value_id (ctx : eval_ctx) : eval_ctx * SymbolicValueId.id =
-  let id, counter' = SymbolicValueId.fresh ctx.symbolic_counter in
-  ({ ctx with symbolic_counter = counter' }, id)
-
-let fresh_borrow_id (ctx : eval_ctx) : eval_ctx * BorrowId.id =
-  let id, counter' = BorrowId.fresh ctx.borrow_counter in
-  ({ ctx with borrow_counter = counter' }, id)
-
-let fresh_region_id (ctx : eval_ctx) : eval_ctx * RegionId.id =
-  let id, counter' = RegionId.fresh ctx.region_counter in
-  ({ ctx with region_counter = counter' }, id)
-
-let fresh_abstraction_id (ctx : eval_ctx) : eval_ctx * AbstractionId.id =
-  let id, counter' = AbstractionId.fresh ctx.abstraction_counter in
-  ({ ctx with abstraction_counter = counter' }, id)
-
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 345ce058..d3e5b83e 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -16,6 +16,8 @@ module type Id = sig
 
   val generator_zero : generator
 
+  val fresh_stateful_generator : unit -> generator ref * (unit -> id)
+
   (* TODO: this is stateful! - but we may want to be able to duplicate contexts... *)
   val fresh : generator -> id * generator
   (* TODO: change the order of the returned types *)
@@ -84,6 +86,15 @@ module IdGen () : Id = struct
      * they happen *)
     if x == max_int then raise (Errors.IntegerOverflow ()) else x + 1
 
+  let fresh_stateful_generator () =
+    let g = ref 0 in
+    let fresh () =
+      let id = !g in
+      g := incr id;
+      id
+    in
+    (g, fresh)
+
   let fresh gen = (gen, incr gen)
 
   let to_string = string_of_int
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 54911d85..ec15093d 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -25,16 +25,13 @@ open InterpreterStatements
 module Test = struct
   let initialize_context (type_context : C.type_context)
       (fun_defs : A.fun_def list) (type_vars : T.type_var list) : C.eval_ctx =
+    C.reset_global_counters ();
     {
       C.type_context;
       C.fun_context = fun_defs;
       C.type_vars;
       C.env = [];
       C.ended_regions = T.RegionId.Set.empty;
-      C.symbolic_counter = V.SymbolicValueId.generator_zero;
-      C.borrow_counter = V.BorrowId.generator_zero;
-      C.region_counter = T.RegionId.generator_zero;
-      C.abstraction_counter = V.AbstractionId.generator_zero;
     }
 
   (** Initialize an evaluation context to execute a function.
@@ -67,10 +64,8 @@ module Test = struct
     in
     let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in
     (* Create fresh symbolic values for the inputs *)
-    let ctx, input_svs =
-      List.fold_left_map
-        (fun ctx ty -> mk_fresh_symbolic_value ty ctx)
-        ctx inst_sg.inputs
+    let input_svs =
+      List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
     in
     (* Create the abstractions and insert them in the context *)
     let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 3cfa78e0..a18ccefb 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -619,15 +619,14 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
     be expanded (because expanding this symbolic value would require expanding
     a reference whose region has already ended).
  *)
-let convert_avalue_to_value (av : V.typed_avalue) (ctx : C.eval_ctx) :
-    C.eval_ctx * V.typed_value =
+let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value =
   (* Convert the type *)
   let ty = Subst.erase_regions av.V.ty in
   (* Generate the fresh a symbolic value *)
-  let ctx, sv_id = C.fresh_symbolic_value_id ctx in
+  let sv_id = C.fresh_symbolic_value_id () in
   let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in
   let value = V.Symbolic svalue in
-  (ctx, { V.value; V.ty })
+  { V.value; V.ty }
 
 (** End a borrow identified by its borrow id in a context
     
@@ -901,7 +900,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
       match bc with
       | V.AMutBorrow (bid, av) ->
           (* First, convert the avalue to a (fresh symbolic) value *)
-          let ctx, v = convert_avalue_to_value av ctx in
+          let v = convert_avalue_to_value av in
           give_back_value config bid v ctx
       | V.ASharedBorrow bid -> give_back_shared config bid ctx
       | V.AProjSharedBorrow _ ->
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 24ec018e..2de06f24 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -183,16 +183,15 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
 
 (** Compute the expansion of an adt value.
 
-    The function might return a list of contexts and values if the symbolic
-    value to expand is an enumeration.
+    The function might return a list of values if the symbolic value to expand
+    is an enumeration.
     
     `expand_enumerations` controls the expansion of enumerations: if false, it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
     (def_id : T.TypeDefId.id) (regions : T.RegionId.id T.region list)
-    (types : T.rty list) (ctx : C.eval_ctx) :
-    (C.eval_ctx * symbolic_expansion) list =
+    (types : T.rty list) (ctx : C.eval_ctx) : symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = C.ctx_lookup_type_def ctx def_id in
@@ -205,38 +204,34 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
   if List.length variants_fields_types > 1 && not expand_enumerations then
     failwith "Not allowed to expand enumerations with several variants";
   (* Initialize the expanded value for a given variant *)
-  let initialize (ctx : C.eval_ctx)
+  let initialize
       ((variant_id, field_types) : T.VariantId.id option * T.rty list) :
-      C.eval_ctx * symbolic_expansion =
-    let ctx, field_values =
-      List.fold_left_map
-        (fun ctx (ty : T.rty) -> mk_fresh_symbolic_value ty ctx)
-        ctx field_types
+      symbolic_expansion =
+    let field_values =
+      List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value ty) field_types
     in
     let see = SeAdt (variant_id, field_values) in
-    (ctx, see)
+    see
   in
   (* Initialize all the expanded values of all the variants *)
-  List.map (initialize ctx) variants_fields_types
+  List.map initialize variants_fields_types
 
-let compute_expanded_symbolic_tuple_value (field_types : T.rty list)
-    (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (field_types : T.rty list) :
+    symbolic_expansion =
   (* Generate the field values *)
-  let ctx, field_values =
-    List.fold_left_map
-      (fun ctx sv_ty -> mk_fresh_symbolic_value sv_ty ctx)
-      ctx field_types
+  let field_values =
+    List.map (fun sv_ty -> mk_fresh_symbolic_value sv_ty) field_types
   in
   let variant_id = None in
   let see = SeAdt (variant_id, field_values) in
-  (ctx, see)
+  see
 
-let compute_expanded_symbolic_box_value (boxed_ty : T.rty) (ctx : C.eval_ctx) :
-    C.eval_ctx * symbolic_expansion =
+let compute_expanded_symbolic_box_value (boxed_ty : T.rty) : symbolic_expansion
+    =
   (* Introduce a fresh symbolic value *)
-  let ctx, boxed_value = mk_fresh_symbolic_value boxed_ty ctx in
+  let boxed_value = mk_fresh_symbolic_value boxed_ty in
   let see = SeAdt (None, [ boxed_value ]) in
-  (ctx, see)
+  see
 
 let expand_symbolic_value_shared_borrow (config : C.config)
     (original_sv : V.symbolic_value) (ref_ty : T.rty) (ctx : C.eval_ctx) :
@@ -247,10 +242,8 @@ let expand_symbolic_value_shared_borrow (config : C.config)
    * one fresh borrow id per instance.
    *)
   let borrows = ref V.BorrowId.Set.empty in
-  let borrow_counter = ref ctx.C.borrow_counter in
   let fresh_borrow () =
-    let bid', cnt' = V.BorrowId.fresh !borrow_counter in
-    borrow_counter := cnt';
+    let bid' = C.fresh_borrow_id () in
     borrows := V.BorrowId.Set.add bid' !borrows;
     bid'
   in
@@ -318,11 +311,10 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   in
   (* Call the visitor *)
   let ctx = obj#visit_eval_ctx None ctx in
-  let ctx = { ctx with C.borrow_counter = !borrow_counter } in
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
   assert (not (V.BorrowId.Set.is_empty bids));
-  let ctx, shared_sv = mk_fresh_symbolic_value ref_ty ctx in
+  let shared_sv = mk_fresh_symbolic_value ref_ty in
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
@@ -344,8 +336,8 @@ let expand_symbolic_value_borrow (config : C.config)
   | T.Mut ->
       (* Simple case: simply create a fresh symbolic value and a fresh
        * borrow id *)
-      let ctx, sv = mk_fresh_symbolic_value ref_ty ctx in
-      let ctx, bid = C.fresh_borrow_id ctx in
+      let sv = mk_fresh_symbolic_value ref_ty in
+      let bid = C.fresh_borrow_id () in
       let see = SeMutRef (bid, sv) in
       (* Expand the symbolic values - we simply perform a substitution (and
        * check that we perform exactly one substitution) *)
@@ -392,7 +384,7 @@ let expand_symbolic_value_no_branching (config : C.config)
           compute_expanded_symbolic_adt_value expand_enumerations def_id regions
             types ctx
         with
-        | [ (ctx, see) ] ->
+        | [ see ] ->
             (* Apply in the context *)
             let ctx =
               apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -406,7 +398,7 @@ let expand_symbolic_value_no_branching (config : C.config)
     | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
         assert (arity = List.length tys);
         (* Generate the field values *)
-        let ctx, see = compute_expanded_symbolic_tuple_value tys ctx in
+        let see = compute_expanded_symbolic_tuple_value tys in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -417,7 +409,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         ctx
     (* Boxes *)
     | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
-        let ctx, see = compute_expanded_symbolic_box_value boxed_ty ctx in
+        let see = compute_expanded_symbolic_box_value boxed_ty in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -454,15 +446,14 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
       (* Compute the expanded value - there should be exactly one because we
        * don't allow to expand enumerations with strictly more than one variant *)
       let expand_enumerations = true in
-      let res =
+      let seel =
         compute_expanded_symbolic_adt_value expand_enumerations def_id regions
           types ctx
       in
       (* Update the synthesized program *)
-      let seel = List.map (fun (_, x) -> x) res in
       S.synthesize_symbolic_expansion_enum_branching original_sv seel;
       (* Apply in the context *)
-      let apply (ctx, see) : C.eval_ctx =
+      let apply see : C.eval_ctx =
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
         in
@@ -471,5 +462,5 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
         (* Return *)
         ctx
       in
-      List.map apply res
+      List.map apply seel
   | _ -> failwith "Unexpected"
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index f9b1ab3c..0b4bc90f 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -157,7 +157,7 @@ let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
   (* Evaluate the operand *)
   let ctx, v = eval_operand config ctx op in
   (* Generate a fresh symbolic value to store the result *)
-  let ctx, res_sv_id = C.fresh_symbolic_value_id ctx in
+  let res_sv_id = C.fresh_symbolic_value_id () in
   let res_sv_ty =
     match (unop, v.V.ty) with
     | E.Not, T.Bool -> T.Bool
@@ -258,7 +258,7 @@ let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
   (* Evaluate the operands *)
   let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
   (* Generate a fresh symbolic value to store the result *)
-  let ctx, res_sv_id = C.fresh_symbolic_value_id ctx in
+  let res_sv_id = C.fresh_symbolic_value_id () in
   let res_sv_ty =
     if binop = Eq || binop = Ne then (
       (* Equality operations *)
@@ -343,7 +343,7 @@ let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
       let access = if bkind = E.Shared then Read else Write in
       let ctx, v = prepare_rplace config access p ctx in
       (* Compute the rvalue - simply a shared borrow with a fresh id *)
-      let ctx, bid = C.fresh_borrow_id ctx in
+      let bid = C.fresh_borrow_id () in
       (* Note that the reference is *mutable* if we do a two-phase borrow *)
       let rv_ty =
         T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
@@ -374,7 +374,7 @@ let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
       let access = Write in
       let ctx, v = prepare_rplace config access p ctx in
       (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
-      let ctx, bid = C.fresh_borrow_id ctx in
+      let bid = C.fresh_borrow_id () in
       let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
       let rv : V.typed_value =
         { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index bfe877ab..07c615a0 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -756,7 +756,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
       | SharedBorrow bid ->
           (* We need to create a new borrow id for the copied borrow, and
            * update the context accordingly *)
-          let ctx, bid' = C.fresh_borrow_id ctx in
+          let bid' = C.fresh_borrow_id () in
           let ctx = reborrow_shared bid bid' ctx in
           (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
       | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow"
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 21c9e034..3fa824ab 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -475,12 +475,10 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool)
     (ctx : C.eval_ctx) :
     (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) =
   let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
-  let borrow_counter = ref ctx.C.borrow_counter in
   (* The function to generate and register fresh reborrows *)
   let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id =
     if allow_reborrows then (
-      let bid', cnt' = V.BorrowId.fresh !borrow_counter in
-      borrow_counter := cnt';
+      let bid' = C.fresh_borrow_id () in
       reborrows := (bid, bid') :: !reborrows;
       bid')
     else failwith "Unexpected reborrow"
@@ -489,13 +487,9 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool)
   let apply_registered_reborrows (ctx : C.eval_ctx) : C.eval_ctx =
     match config.C.mode with
     | C.ConcreteMode ->
-        (* Reborrows are introduced when applying projections in symbolic mode *)
-        assert (!borrow_counter = ctx.C.borrow_counter);
         assert (!reborrows = []);
         ctx
     | C.SymbolicMode ->
-        (* Update the borrow counter *)
-        let ctx = { ctx with C.borrow_counter = !borrow_counter } in
         (* Apply the reborrows *)
         apply_reborrows !reborrows ctx
   in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index c4bbdf23..36d11a9e 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -362,9 +362,9 @@ let eval_box_deref_mut_or_shared_inst_sig (region_params : T.erased_region list)
      `&'a (mut) Box<T> -> &'a (mut) T`
      where T is the type param
   *)
-  let ctx, rid = C.fresh_region_id ctx in
+  let rid = C.fresh_region_id () in
   let r = T.Var rid in
-  let ctx, abs_id = C.fresh_abstraction_id ctx in
+  let abs_id = C.fresh_abstraction_id () in
   match (region_params, type_params) with
   | [], [ ty_param ] ->
       let ty_param = ety_no_regions_to_rty ty_param in
@@ -477,7 +477,7 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
   let ctx, rg_abs_ids_bindings =
     List.fold_left_map
       (fun ctx rg ->
-        let ctx, abs_id = C.fresh_abstraction_id ctx in
+        let abs_id = C.fresh_abstraction_id () in
         (ctx, (rg.A.id, abs_id)))
       ctx sg.regions_hierarchy
   in
@@ -490,9 +490,7 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
     A.RegionGroupId.Map.find rg_id asubst_map
   in
   (* Generate fresh regions and their substitutions *)
-  let ctx, _, rsubst, _ =
-    Subst.fresh_regions_with_substs sg.region_params ctx
-  in
+  let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in
   (* Generate the type substitution
    * Note that we need the substitution to map the type variables to
    * [rty] types (not [ety]). In order to do that, we convert the
@@ -804,7 +802,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (args : E.operand list) (dest : E.place) : C.eval_ctx =
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.A.output in
-  let ctx, ret_spc = mk_fresh_symbolic_value ret_sv_ty ctx in
+  let ret_spc = mk_fresh_symbolic_value ret_sv_ty in
   let ret_value = mk_typed_value_from_symbolic_value ret_spc in
   let ret_av = mk_aproj_loans_from_symbolic_value ret_spc in
   (* Evaluate the input operands *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index fcc6050f..40ef0d05 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -45,11 +45,10 @@ let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
   { var_id; projection = [] }
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (ty : T.rty) (ctx : C.eval_ctx) :
-    C.eval_ctx * V.symbolic_value =
-  let ctx, sv_id = C.fresh_symbolic_value_id ctx in
+let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value =
+  let sv_id = C.fresh_symbolic_value_id () in
   let svalue = { V.sv_id; V.sv_ty = ty } in
-  (ctx, svalue)
+  svalue
 
 (** Create a typed value from a symbolic value. *)
 let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 1b6003bb..62a737ad 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -42,16 +42,12 @@ let erase_regions (ty : T.rty) : T.ety =
     
     TODO: simplify? we only need the subst `T.RegionVarId.id -> T.RegionId.id`
   *)
-let fresh_regions_with_substs (region_vars : T.region_var list)
-    (ctx : C.eval_ctx) :
-    C.eval_ctx
-    * T.RegionId.id list
+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) =
   (* Generate fresh regions *)
-  let ctx, fresh_region_ids =
-    List.fold_left_map (fun ctx _ -> C.fresh_region_id ctx) ctx region_vars
-  in
+  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 =
@@ -66,7 +62,7 @@ let fresh_regions_with_substs (region_vars : T.region_var list)
     match r with T.Static -> T.Static | T.Var id -> T.Var (rid_subst id)
   in
   (* Return *)
-  (ctx, fresh_region_ids, rid_subst, rsubst)
+  (fresh_region_ids, rid_subst, rsubst)
 
 (** Erase the regions in a type and substitute the type variables *)
 let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
-- 
cgit v1.2.3