summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Interpreter.ml2
-rw-r--r--compiler/InterpreterBorrows.ml60
-rw-r--r--compiler/InterpreterExpansion.ml41
-rw-r--r--compiler/InterpreterExpressions.ml14
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml24
-rw-r--r--compiler/InterpreterStatements.ml4
-rw-r--r--compiler/InterpreterUtils.ml32
-rw-r--r--compiler/Values.ml44
8 files changed, 63 insertions, 158 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 4ecafd31..76432faa 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -206,7 +206,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
in
(* Create fresh symbolic values for the inputs *)
let input_svs =
- List.map (fun ty -> mk_fresh_symbolic_value SynthInput ty) inst_sg.inputs
+ List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
in
(* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
let call_id = fresh_fun_call_id () in
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 6a7ac095..19b9fd3b 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -444,13 +444,6 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
(ctx : eval_ctx) : eval_ctx =
(* Sanity checks *)
assert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty);
- (match nsv.sv_kind with
- | SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
- ->
- ()
- | FunCallRet | SynthInput | Global | KindConstGeneric | LoopOutput | LoopJoin
- | Aggregate | ConstGeneric | TraitConst ->
- raise (Failure "Unreachable"));
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = nsv in
(* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -459,31 +452,20 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
let _ = raise Utils.Unimplemented in
(* Compute the projection over the given back value *)
let child_proj =
- match nsv.sv_kind with
- | SynthRetGivenBack ->
- (* The given back value comes from the return value of the function
- we are currently synthesizing (as it is given back, it means
- we ended one of the regions appearing in the signature: we are
- currently synthesizing one of the backward functions).
-
- As we don't allow borrow overwrites on returned value, we can
- (and MUST) forget the borrows *)
- AIgnoredProjBorrows
- | FunCallGivenBack ->
- (* TODO: there is something wrong here.
- Consider this:
- {[
- abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
- abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
- ]}
-
- Upon ending abs1, we give back some fresh symbolic value [s1],
- that we reinsert where the loan for [s0] is. However, the mutable
- borrow in the type [&'a mut T] was ended: we give back a value of
- type [T]! We thus *mustn't* introduce a projector here.
- *)
- AProjBorrows (nsv, sv.sv_ty)
- | _ -> raise (Failure "Unreachable")
+ (* TODO: there is something wrong here.
+ Consider this:
+ {[
+ abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
+ abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
+ ]}
+
+ Upon ending abs1, we give back some fresh symbolic value [s1],
+ that we reinsert where the loan for [s0] is. However, the mutable
+ borrow in the type [&'a mut T] was ended: we give back a value of
+ type [T]! We thus *mustn't* introduce a projector here.
+ *)
+ (* AProjBorrows (nsv, sv.sv_ty) *)
+ raise (Failure "TODO")
in
AProjLoans (sv, (mv, child_proj) :: local_given_back)
in
@@ -739,17 +721,7 @@ let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id)
*)
let convert_avalue_to_given_back_value (abs_kind : abs_kind) (av : typed_avalue)
: symbolic_value =
- let sv_kind =
- match abs_kind with
- | FunCall _ -> FunCallGivenBack
- | SynthRet _ -> SynthRetGivenBack
- | SynthInput _ -> SynthInputGivenBack
- | Loop _ -> LoopGivenBack
- | Identity ->
- (* Identity abstractions give back nothing *)
- raise (Failure "Unreachable")
- in
- mk_fresh_symbolic_value sv_kind av.ty
+ mk_fresh_symbolic_value av.ty
(** Auxiliary function: see {!end_borrow_aux}.
@@ -1239,7 +1211,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
("end_abstraction_borrows: found aproj borrows: "
^ aproj_to_string ctx (AProjBorrows (sv, proj_ty))));
(* Generate a fresh symbolic value *)
- let nsv = mk_fresh_symbolic_value FunCallGivenBack proj_ty in
+ let nsv = mk_fresh_symbolic_value proj_ty in
(* Replace the proj_borrows - there should be exactly one *)
let ended_borrow = AEndedProjBorrows nsv in
let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index d7f5fcd5..bbf4d9d5 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -209,8 +209,8 @@ let apply_symbolic_expansion_non_borrow (config : config)
doesn't allow the expansion of enumerations *containing several variants*.
*)
let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
- (kind : sv_kind) (def_id : TypeDeclId.id) (generics : generic_args)
- (ctx : eval_ctx) : symbolic_expansion list =
+ (def_id : TypeDeclId.id) (generics : generic_args) (ctx : eval_ctx) :
+ symbolic_expansion list =
(* Lookup the definition and check if it is an enumeration with several
* variants *)
let def = ctx_lookup_type_decl ctx def_id in
@@ -227,7 +227,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
symbolic_expansion =
let field_values =
- List.map (fun (ty : rty) -> mk_fresh_symbolic_value kind ty) field_types
+ List.map (fun (ty : rty) -> mk_fresh_symbolic_value ty) field_types
in
let see = SeAdt (variant_id, field_values) in
see
@@ -235,20 +235,19 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
(* Initialize all the expanded values of all the variants *)
List.map initialize variants_fields_types
-let compute_expanded_symbolic_tuple_value (kind : sv_kind)
- (field_types : rty list) : symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (field_types : rty list) :
+ symbolic_expansion =
(* Generate the field values *)
let field_values =
- List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types
+ 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
see
-let compute_expanded_symbolic_box_value (kind : sv_kind) (boxed_ty : rty) :
- symbolic_expansion =
+let compute_expanded_symbolic_box_value (boxed_ty : rty) : symbolic_expansion =
(* Introduce a fresh symbolic value *)
- let boxed_value = mk_fresh_symbolic_value kind boxed_ty in
+ let boxed_value = mk_fresh_symbolic_value boxed_ty in
let see = SeAdt (None, [ boxed_value ]) in
see
@@ -262,16 +261,15 @@ let compute_expanded_symbolic_box_value (kind : sv_kind) (boxed_ty : rty) :
doesn't allow the expansion of enumerations *containing several variants*.
*)
let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
- (kind : sv_kind) (adt_id : type_id) (generics : generic_args)
- (ctx : eval_ctx) : symbolic_expansion list =
+ (adt_id : type_id) (generics : generic_args) (ctx : eval_ctx) :
+ symbolic_expansion list =
match (adt_id, generics.regions, generics.types) with
| TAdtId def_id, _, _ ->
- compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind
- def_id generics ctx
- | TTuple, [], _ ->
- [ compute_expanded_symbolic_tuple_value kind generics.types ]
+ compute_expanded_symbolic_non_assumed_adt_value expand_enumerations def_id
+ generics ctx
+ | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value generics.types ]
| TAssumed TBox, [], [ boxed_ty ] ->
- [ compute_expanded_symbolic_box_value kind boxed_ty ]
+ [ compute_expanded_symbolic_box_value boxed_ty ]
| _ ->
raise
(Failure "compute_expanded_symbolic_adt_value: unexpected combination")
@@ -313,7 +311,7 @@ let expand_symbolic_value_shared_borrow (config : config)
else None
in
(* The fresh symbolic value for the shared value *)
- let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
+ let shared_sv = mk_fresh_symbolic_value ref_ty in
(* Visitor to replace the projectors on borrows *)
let obj =
object (self)
@@ -403,7 +401,7 @@ let expand_symbolic_value_borrow (config : config)
| RMut ->
(* Simple case: simply create a fresh symbolic value and a fresh
* borrow id *)
- let sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
+ let sv = mk_fresh_symbolic_value ref_ty in
let bid = fresh_borrow_id () in
let see = SeMutRef (bid, sv) in
(* Expand the symbolic values - we simply perform a substitution (and
@@ -524,8 +522,8 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
(* Compute the expanded value *)
let allow_branching = false in
let seel =
- compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
- generics ctx
+ compute_expanded_symbolic_adt_value allow_branching adt_id generics
+ ctx
in
(* There should be exacly one branch *)
let see = Collections.List.to_cons_nil seel in
@@ -581,8 +579,7 @@ let expand_symbolic_adt (config : config) (sv : symbolic_value)
let allow_branching = true in
(* Compute the expanded value *)
let seel =
- compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
- generics ctx
+ compute_expanded_symbolic_adt_value allow_branching adt_id generics ctx
in
(* Apply *)
let seel = List.map (fun see -> (Some see, cf_branches)) seel in
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index af545fb9..9f117933 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -283,7 +283,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
List.find (fun (name, _) -> name = const_name) trait_decl.consts
in
(* Introduce a fresh symbolic value *)
- let v = mk_fresh_symbolic_typed_value TraitConst ty in
+ let v = mk_fresh_symbolic_typed_value ty in
(* Continue the evaluation *)
let e = cf v ctx in
(* We have to wrap the generated expression *)
@@ -315,7 +315,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
copy_value allow_adt_copy config ctx cv
| SymbolicMode ->
(* We use the looked up value only for its type *)
- let v = mk_fresh_symbolic_typed_value KindConstGeneric cv.ty in
+ let v = mk_fresh_symbolic_typed_value cv.ty in
(ctx, v)
in
(* Continue *)
@@ -464,9 +464,7 @@ let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
| Cast (CastInteger (_, tgt_ty)), _ -> TLiteral (TInteger tgt_ty)
| _ -> raise (Failure "Invalid input for unop")
in
- let res_sv =
- { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty }
- in
+ let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
(* Call the continuation *)
let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
(* Synthesize the symbolic AST *)
@@ -603,9 +601,7 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
| Ne | Eq -> raise (Failure "Unreachable"))
| _ -> raise (Failure "Invalid inputs for binop")
in
- let res_sv =
- { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty }
- in
+ let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
(* Call the continuattion *)
let v = mk_typed_value_from_symbolic_value res_sv in
let expr = cf (Ok v) ctx in
@@ -769,7 +765,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
array we introduce here might be duplicated in the generated
code: by introducing a symbolic value we introduce a let-binding
in the generated code. *)
- let saggregated = mk_fresh_symbolic_typed_value Aggregate ty in
+ let saggregated = mk_fresh_symbolic_typed_value ty in
(* Call the continuation *)
match cf saggregated ctx with
| None -> None
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index c21dab71..90559c29 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -389,7 +389,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let match_distinct_literals (ty : ety) (_ : literal) (_ : literal) :
typed_value =
- mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin ty
+ mk_fresh_symbolic_typed_value_from_no_regions_ty ty
let match_distinct_adts (ty : ety) (adt0 : adt_value) (adt1 : adt_value) :
typed_value =
@@ -418,7 +418,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
check_loans false adt1.field_values;
(* No borrows, no loans: we can introduce a symbolic value *)
- mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin ty
+ mk_fresh_symbolic_typed_value_from_no_regions_ty ty
let match_shared_borrows _ (ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) :
borrow_id =
@@ -435,9 +435,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Generate a fresh symbolic value for the shared value *)
let _, bv_ty, kind = ty_as_ref ty in
- let sv =
- mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin bv_ty
- in
+ let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty bv_ty in
let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
@@ -582,9 +580,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Generate a fresh symbolic value for the borrowed value *)
let _, bv_ty, kind = ty_as_ref ty in
- let sv =
- mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin bv_ty
- in
+ let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty bv_ty in
let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
@@ -664,7 +660,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
borrows *)
assert (not (ty_has_borrows S.ctx.type_context.type_infos sv0.sv_ty));
(* We simply introduce a fresh symbolic value *)
- mk_fresh_symbolic_value LoopJoin sv0.sv_ty)
+ mk_fresh_symbolic_value sv0.sv_ty)
let match_symbolic_with_other (left : bool) (sv : symbolic_value)
(v : typed_value) : typed_value =
@@ -685,7 +681,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
if value_is_left then raise (ValueMatchFailure (LoanInLeft id))
else raise (ValueMatchFailure (LoanInRight id)));
(* Return a fresh symbolic value *)
- mk_fresh_symbolic_typed_value LoopJoin sv.sv_ty
+ mk_fresh_symbolic_typed_value sv.sv_ty
let match_bottom_with_other (left : bool) (v : typed_value) : typed_value =
(* If there are outer loans in the non-bottom value, raise an exception.
@@ -834,7 +830,7 @@ struct
let match_distinct_literals (ty : ety) (_ : literal) (_ : literal) :
typed_value =
- mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin ty
+ mk_fresh_symbolic_typed_value_from_no_regions_ty ty
let match_distinct_adts (_ty : ety) (_adt0 : adt_value) (_adt1 : adt_value) :
typed_value =
@@ -904,11 +900,7 @@ struct
GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1
in
let sv_ty = match_rtys sv0.sv_ty sv1.sv_ty in
- let sv_kind =
- if sv0.sv_kind = sv1.sv_kind then sv0.sv_kind
- else raise (Distinct "match_symbolic_values: sv_kind")
- in
- let sv = { sv_id; sv_ty; sv_kind } in
+ let sv = { sv_id; sv_ty } in
sv
else (
(* Check: fixed values are fixed *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 437b358a..66b8492a 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1008,7 +1008,7 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) :
(* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
* defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
assert (ty_no_regions global.ty);
- let sval = mk_fresh_symbolic_value Global global.ty in
+ let sval = mk_fresh_symbolic_value global.ty in
let cc =
assign_to_place config (mk_typed_value_from_symbolic_value sval) dest
in
@@ -1312,7 +1312,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
(* Generate a fresh symbolic value for the return value *)
let ret_sv_ty = inst_sg.output in
- let ret_spc = mk_fresh_symbolic_value FunCallRet ret_sv_ty 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 regions =
mk_aproj_loans_value_from_symbolic_value regions ret_spc
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index d3f8f4fa..e04a6b90 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -74,31 +74,29 @@ let mk_place_from_var_id (var_id : VarId.id) : place =
{ var_id; projection = [] }
(** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (sv_kind : sv_kind) (ty : ty) : symbolic_value =
+let mk_fresh_symbolic_value (ty : ty) : symbolic_value =
(* Sanity check *)
assert (ty_is_rty ty);
let sv_id = fresh_symbolic_value_id () in
- let svalue = { sv_kind; sv_id; sv_ty = ty } in
+ let svalue = { sv_id; sv_ty = ty } in
svalue
-let mk_fresh_symbolic_value_from_no_regions_ty (sv_kind : sv_kind) (ty : ty) :
- symbolic_value =
+let mk_fresh_symbolic_value_from_no_regions_ty (ty : ty) : symbolic_value =
assert (ty_no_regions ty);
- mk_fresh_symbolic_value sv_kind ty
+ mk_fresh_symbolic_value ty
(** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value (sv_kind : sv_kind) (rty : ty) : typed_value =
+let mk_fresh_symbolic_typed_value (rty : ty) : typed_value =
assert (ty_is_rty rty);
let ty = Substitute.erase_regions rty in
(* Generate the fresh a symbolic value *)
- let value = mk_fresh_symbolic_value sv_kind rty in
+ let value = mk_fresh_symbolic_value rty in
let value = VSymbolic value in
{ value; ty }
-let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : sv_kind)
- (ty : ty) : typed_value =
+let mk_fresh_symbolic_typed_value_from_no_regions_ty (ty : ty) : typed_value =
assert (ty_no_regions ty);
- mk_fresh_symbolic_typed_value sv_kind ty
+ mk_fresh_symbolic_typed_value ty
(** Create a typed value from a symbolic value. *)
let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value =
@@ -267,15 +265,9 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx)
inherit [_] iter_typed_value
method! visit_symbolic_value _ s =
- match s.sv_kind with
- | FunCallRet | LoopOutput | LoopJoin ->
- if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
- raise Found
- else ()
- | SynthInput | SynthInputGivenBack | FunCallGivenBack
- | SynthRetGivenBack | Global | KindConstGeneric | LoopGivenBack
- | Aggregate | ConstGeneric | TraitConst ->
- ()
+ if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
+ raise Found
+ else ()
end
in
(* We use exceptions *)
@@ -430,7 +422,7 @@ let initialize_eval_context (ctx : decls_ctx)
(List.map
(fun (cg : const_generic_var) ->
let ty = TLiteral cg.ty in
- let cv = mk_fresh_symbolic_typed_value ConstGeneric ty in
+ let cv = mk_fresh_symbolic_typed_value ty in
(cg.index, cv))
const_generic_vars)
in
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 60cbcc8b..5473ce3e 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -15,47 +15,6 @@ module LoopId = IdGen ()
type symbolic_value_id = SymbolicValueId.id [@@deriving show, ord]
type symbolic_value_id_set = SymbolicValueId.Set.t [@@deriving show, ord]
type loop_id = LoopId.id [@@deriving show, ord]
-
-(** The kind of a symbolic value, which precises how the value was generated.
-
- TODO: remove? This is not useful anymore.
- *)
-type sv_kind =
- | FunCallRet (** The value is the return value of a function call *)
- | FunCallGivenBack
- (** The value is a borrowed value given back by an abstraction
- (happens when giving a borrow to a function: when the abstraction
- introduced to model the function call ends we reintroduce a symbolic
- value in the context for the value modified by the abstraction through
- the borrow).
- *)
- | SynthInput
- (** The value is an input value of the function whose body we are
- currently synthesizing.
- *)
- | SynthRetGivenBack
- (** The value is a borrowed value that the function whose body we are
- synthesizing returned, and which was given back because we ended
- one of the lifetimes of this function (we do this to synthesize
- the backward functions).
- *)
- | SynthInputGivenBack
- (** The value was given back upon ending one of the input abstractions *)
- | Global (** The value is a global *)
- | KindConstGeneric (** The value is a const generic *)
- | LoopOutput (** The output of a loop (seen as a forward computation) *)
- | LoopGivenBack
- (** A value given back by a loop (when ending abstractions while going backwards) *)
- | LoopJoin
- (** The result of a loop join (when computing loop fixed points) *)
- | Aggregate
- (** A symbolic value we introduce in place of an aggregate value *)
- | ConstGeneric
- (** A symbolic value we introduce when using a const generic as a value *)
- | TraitConst
- (** A symbolic value we introduce when evaluating a trait associated constant *)
-[@@deriving show, ord]
-
type borrow_id = BorrowId.id [@@deriving show, ord]
type borrow_id_set = BorrowId.Set.t [@@deriving show, ord]
type loan_id = BorrowId.id [@@deriving show, ord]
@@ -65,7 +24,6 @@ type loan_id_set = BorrowId.Set.t [@@deriving show, ord]
class ['self] iter_typed_value_base =
object (self : 'self)
inherit [_] iter_ty
- method visit_sv_kind : 'env -> sv_kind -> unit = fun _ _ -> ()
method visit_symbolic_value_id : 'env -> symbolic_value_id -> unit =
fun _ _ -> ()
@@ -85,7 +43,6 @@ class ['self] iter_typed_value_base =
class ['self] map_typed_value_base =
object (self : 'self)
inherit [_] map_ty
- method visit_sv_kind : 'env -> sv_kind -> sv_kind = fun _ x -> x
method visit_symbolic_value_id
: 'env -> symbolic_value_id -> symbolic_value_id =
@@ -104,7 +61,6 @@ class ['self] map_typed_value_base =
(** A symbolic value *)
type symbolic_value = {
- sv_kind : sv_kind;
sv_id : symbolic_value_id;
sv_ty : ty; (** This should be a type with regions *)
}