summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Values.ml50
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