summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Contexts.ml63
-rw-r--r--src/Identifiers.ml11
-rw-r--r--src/Interpreter.ml11
-rw-r--r--src/InterpreterBorrows.ml9
-rw-r--r--src/InterpreterExpansion.ml65
-rw-r--r--src/InterpreterExpressions.ml8
-rw-r--r--src/InterpreterPaths.ml2
-rw-r--r--src/InterpreterProjectors.ml8
-rw-r--r--src/InterpreterStatements.ml12
-rw-r--r--src/InterpreterUtils.ml7
-rw-r--r--src/Substitute.ml12
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)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 19:51:17 +0000