diff options
Diffstat (limited to 'src/Values.ml')
-rw-r--r-- | src/Values.ml | 10 |
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]); |