From 59ec03d37d2ad51cf77e456622703c4c84780f48 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 2 Aug 2023 11:46:09 +0200
Subject: Make progress

---
 compiler/SymbolicAst.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 0e68d2fd..787fefc7 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;
-- 
cgit v1.2.3


From 931fabe3e8590815548d606b33fc8db31e9f6010 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Aug 2023 16:21:43 +0200
Subject: Fix an issue with the extraction of aggregated arrays

---
 compiler/SymbolicAst.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 787fefc7..7dc94dcd 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -167,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.
 
@@ -246,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
-- 
cgit v1.2.3