diff options
author | Son Ho | 2022-01-15 21:35:57 +0100 |
---|---|---|
committer | Son Ho | 2022-01-15 21:35:57 +0100 |
commit | e0248a4af4d9618ac3f75ff4282116643e2abe24 (patch) | |
tree | 8e74c9370d2243abbca54420cf946a381de8bfa9 /src/Values.ml | |
parent | 9564ad271a9d69ca58333ec33c778f3255ca1632 (diff) |
Introduce abs_kind, to keep track of abstractions' origins
Diffstat (limited to '')
-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]); |