summaryrefslogtreecommitdiff
path: root/src/Values.ml
diff options
context:
space:
mode:
authorSon Ho2021-12-01 18:04:08 +0100
committerSon Ho2021-12-01 18:04:08 +0100
commit3562ff88d2c65d018b473fc2fb07359f95e6b2f9 (patch)
treed071ffc857fc0c59c7413f6d05850b76bbfa23f2 /src/Values.ml
parentc943e63156ebe2df4f0819ecbb4597966e116868 (diff)
Merge the ADTs, tuples and assumed types in the type and value
definitions
Diffstat (limited to 'src/Values.ml')
-rw-r--r--src/Values.ml26
1 files changed, 3 insertions, 23 deletions
diff --git a/src/Values.ml b/src/Values.ml
index 2ee2bdf5..f95cbc07 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -76,14 +76,10 @@ type symbolic_proj_comp = {
Can be specialized for "regular" values or values in abstractions *)
type ('r, 'sv, 'bc, 'lc) g_value =
| Concrete of constant_value (** Concrete (non-symbolic) value *)
- | Adt of ('r, 'sv, 'bc, 'lc) g_adt_value (** Enumerations and structures *)
- | Tuple of ('r, 'sv, 'bc, 'lc) g_typed_value list
- (** Tuple - note that units are encoded as 0-tuples
- TODO: merge with Adt?
- *)
+ | Adt of ('r, 'sv, 'bc, 'lc) g_adt_value
+ (** Enumerations, structures, tuples, assumed types. Note that units
+ are encoded as 0-tuples *)
| Bottom (** No value (uninitialized or moved value) *)
- | Assumed of ('r, 'sv, 'bc, 'lc) g_assumed_value
- (** Value of an abstract type (Box, Vec, Cell...) *)
| Borrow of 'bc (** A borrowed value *)
| Loan of 'lc (** A loaned value *)
| Symbolic of 'sv (** Unknown value *)
@@ -96,10 +92,6 @@ and ('r, 'sv, 'bc, 'lc) g_adt_value = {
[@@deriving show]
(** "Generic" ADT value (not "GADT" value) *)
-and ('r, 'sv, 'bc, 'lc) g_assumed_value =
- | Box of ('r, 'sv, 'bc, 'lc) g_typed_value
-[@@deriving show]
-
and ('r, 'sv, 'bc, 'lc) g_typed_value = {
value : ('r, 'sv, 'bc, 'lc) g_value;
ty : 'r ty;
@@ -115,14 +107,6 @@ and adt_value =
(erased_region, symbolic_proj_comp, borrow_content, loan_content) g_adt_value
[@@deriving show]
-and assumed_value =
- ( erased_region,
- symbolic_proj_comp,
- borrow_content,
- loan_content )
- g_assumed_value
-[@@deriving show]
-
and typed_value =
( erased_region,
symbolic_proj_comp,
@@ -177,10 +161,6 @@ type avalue =
and aadt_value =
(RegionVarId.id region, aproj, aborrow_content, aloan_content) g_adt_value
-and aassumed_value =
- (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_assumed_value
-[@@deriving show]
-
and typed_avalue =
(RegionVarId.id region, aproj, aborrow_content, aloan_content) g_typed_value
[@@deriving show]