Merge pull request #32 from AeneasVerif/son_arrays

Add support for arrays/slices and const generics

1 files changed, 11 insertions, 1 deletions

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 0e68d2fd..7dc94dcd 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -43,7 +43,10 @@ type call = {
           borrows (we need to perform lookups).
        *)
   abstractions : V.AbstractionId.id list;
+  (* TODO: rename to "...args" *)
   type_params : T.ety list;
+  (* TODO: rename to "...args" *)
+  const_generic_params : T.const_generic list;
   args : V.typed_value list;
   args_places : mplace option list;  (** Meta information *)
   dest : V.symbolic_value;
@@ -164,7 +167,7 @@ type expression =
       Contexts.eval_ctx
       * mplace option
       * V.symbolic_value
-      * V.typed_value
+      * value_aggregate
       * expression
       (** We introduce a new symbolic value, equal to some other value.
 
@@ -243,6 +246,13 @@ 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. *)
+
+(* Remark: this type doesn't have to be mutually recursive with the other
+   types, but it makes it easy to generate the visitors *)
+and value_aggregate =
+  | SingleValue of V.typed_value  (** Regular case *)
+  | Array of V.typed_value list
+      (** This is used when introducing array aggregates *)
 [@@deriving
   show,
     visitors