summaryrefslogtreecommitdiff
path: root/src/Values.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Values.ml10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Values.ml b/src/Values.ml
index 856ccb6f..a64d4467 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -623,8 +623,18 @@ and typed_avalue = { value : avalue; ty : rty }
concrete = true;
}]
+(** The kind of an abstraction, which keeps track of its origin *)
+type abs_kind =
+ | FunCall (** The abstraction was introduced because of a function call *)
+ | Synth
+ (** The abstraction is used to keep track of the input/return value of
+ the function we are currently synthesizing.
+ *)
+[@@deriving show]
+
type abs = {
abs_id : (AbstractionId.id[@opaque]);
+ kind : (abs_kind[@opaque]);
parents : (AbstractionId.Set.t[@opaque]); (** The parent abstractions *)
regions : (RegionId.Set.t[@opaque]); (** Regions owned by this abstraction *)
ancestors_regions : (RegionId.Set.t[@opaque]);