diff options
| -rw-r--r-- | src/Values.ml | 50 |
1 files changed, 37 insertions, 13 deletions
diff --git a/src/Values.ml b/src/Values.ml index 92f1491b..f1fdfd6c 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -65,28 +65,56 @@ type symbolic_proj_comp = { regions *but* the ones which are listed in the projector. *) -(** An untyped value, used in the environments *) -type value = +(** A generic, untyped value, used in the environments. + + Parameterized by: + - 'ty: type + - 'bc: borrow content + - 'lc: loan content + + Can be specialized for "regular" values or values in abstractions *) +type ('ty, 'bc, 'lc) g_value = | Concrete of constant_value (** Concrete (non-symbolic) value *) - | Adt of adt_value (** Enumerations and structures *) - | Tuple of typed_value list + | Adt of ('ty, 'bc, 'lc) g_adt_value (** Enumerations and structures *) + | Tuple of ('ty, 'bc, 'lc) g_typed_value list (** Tuple - note that units are encoded as 0-tuples TODO: merge with Adt? *) | Bottom (** No value (uninitialized or moved value) *) - | Assumed of assumed_value + | Assumed of ('ty, 'bc, 'lc) g_assumed_value (** Value of an abstract type (Box, Vec, Cell...) *) - | Borrow of borrow_content (** A borrowed value *) - | Loan of loan_content (** A loaned value *) + | Borrow of 'bc (** A borrowed value *) + | Loan of 'lc (** A loaned value *) | Symbolic of symbolic_proj_comp (** Unknown value *) [@@deriving show] -and adt_value = { +and ('ty, 'bc, 'lc) g_adt_value = { variant_id : VariantId.id option; - field_values : typed_value list; + field_values : ('ty, 'bc, 'lc) g_typed_value list; +} +[@@deriving show] +(** "Generic" ADT value (not "GADT" value) *) + +and ('ty, 'bc, 'lc) g_assumed_value = Box of ('ty, 'bc, 'lc) g_typed_value +[@@deriving show] + +and ('ty, 'bc, 'lc) g_typed_value = { + value : ('ty, 'bc, 'lc) g_value; + ty : 'ty; } [@@deriving show] +type value = (ety, borrow_content, loan_content) g_value [@@deriving show] + +and adt_value = (ety, borrow_content, loan_content) g_adt_value +[@@deriving show] + +and assumed_value = (ety, borrow_content, loan_content) g_assumed_value +[@@deriving show] + +and typed_value = (ety, borrow_content, loan_content) g_typed_value +[@@deriving show] + and borrow_content = | SharedBorrow of BorrowId.id (** A shared value *) | MutBorrow of BorrowId.id * typed_value (** A mutably borrowed value *) @@ -108,10 +136,6 @@ and loan_content = | MutLoan of BorrowId.id [@@deriving show] -and assumed_value = Box of typed_value [@@deriving show] - -and typed_value = { value : value; ty : ety } [@@deriving show] - type abstract_shared_borrows = | AsbSet of BorrowId.set_t | AsbProjReborrows of symbolic_value * rty |