diff options
Diffstat (limited to 'src/SymbolicAst.ml')
-rw-r--r-- | src/SymbolicAst.ml | 20 |
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) *) |