summaryrefslogtreecommitdiff
path: root/src/SymbolicAst.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/SymbolicAst.ml20
1 files changed, 10 insertions, 10 deletions
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 3148f833..07afd914 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -45,6 +45,16 @@ type call = {
dest_place : mplace option; (** Meta information *)
}
+(** Meta information, not necessary for synthesis but useful to guide it to
+ generate a pretty output.
+ *)
+
+type meta =
+ | Aggregate of mplace option * V.typed_value
+ (** We generated an aggregate value *)
+ | Assignment of mplace * V.typed_value
+ (** We generated an assignment (destination, assigned value) *)
+
(** **Rk.:** here, [expression] is not at all equivalent to the expressions
used in CFIM: they are a first step towards lambda-calculus expressions.
*)
@@ -87,13 +97,3 @@ and expansion =
T.integer_type * (V.scalar_value * expression) list * expression
(** An integer expansion (i.e, a switch over an integer). The last
expression is for the "otherwise" branch. *)
-
-(** Meta information, not necessary for synthesis but useful to guide it to
- generate a pretty output.
- *)
-
-and meta =
- | Aggregate of mplace option * V.typed_value
- (** We generated an aggregate value *)
- | Assignment of mplace * V.typed_value
- (** We generated an assignment (destination, assigned value) *)