diff options
| -rw-r--r-- | compiler/Interpreter.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 60 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 41 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 14 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 24 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 32 | ||||
| -rw-r--r-- | compiler/Values.ml | 44 |
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 *) } |