From b4ecf513020b2d5bfdfb7b9e2a721feab6e6998e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 28 Jan 2022 00:04:22 +0100
Subject: Remove the Aggregated variant from SymbolicAst.meta as it is included
 in the Assignment variant

---
 src/InterpreterExpressions.ml | 8 ++------
 src/PrintPure.ml              | 3 ---
 src/Pure.ml                   | 4 +---
 src/SymbolicAst.ml            | 2 --
 src/SymbolicToPure.ml         | 4 ----
 src/SynthesizeSymbolic.ml     | 6 ------
 6 files changed, 3 insertions(+), 24 deletions(-)

(limited to 'src')

diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 34bfd574..ce9489a9 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -592,9 +592,7 @@ let eval_rvalue_aggregate (config : C.config)
         let ty = T.Adt (T.Tuple, [], tys) in
         let aggregated : V.typed_value = { V.value = v; ty } in
         (* Call the continuation *)
-        let expr = cf aggregated ctx in
-        (* Synthesize the symbolic AST *)
-        S.synthesize_aggregated_value aggregated None expr
+        cf aggregated ctx
     | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
         (* Sanity checks *)
         let type_def = C.ctx_lookup_type_def ctx def_id in
@@ -613,9 +611,7 @@ let eval_rvalue_aggregate (config : C.config)
         let aty = T.Adt (T.AdtId def_id, regions, types) in
         let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
         (* Call the continuation *)
-        let expr = cf aggregated ctx in
-        (* Synthesize the symbolic AST *)
-        S.synthesize_aggregated_value aggregated None expr
+        cf aggregated ctx
   in
   (* Compose and apply *)
   comp eval_ops compute cf
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 5223fb21..f78e4a97 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -340,9 +340,6 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
 let meta_to_string (fmt : ast_formatter) (meta : meta) : string =
   let meta =
     match meta with
-    | Aggregate (p, rv) ->
-        let p = match p with None -> "_" | Some p -> mplace_to_string fmt p in
-        "@aggregate(" ^ p ^ " := " ^ typed_rvalue_to_string fmt rv ^ ")"
     | Assignment (p, rv) ->
         "@assign(" ^ mplace_to_string fmt p ^ " := "
         ^ typed_rvalue_to_string fmt rv
diff --git a/src/Pure.ml b/src/Pure.ml
index 89748bdd..7e5aca47 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -201,9 +201,7 @@ type let_bindings =
        *)
 
 (** Meta-information stored in the AST *)
-type meta =
-  | Aggregate of mplace option * typed_rvalue
-  | Assignment of mplace * typed_rvalue
+type meta = Assignment of mplace * typed_rvalue
 
 (** **Rk.:** here, [expression] is not at all equivalent to the expressions
     used in CFIM. They are lambda-calculus expressions, and are thus actually
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 07afd914..4eca712a 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -50,8 +50,6 @@ type call = {
  *)
 
 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) *)
 
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 4fa8e54c..8b31bffa 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1246,10 +1246,6 @@ and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
   let e = translate_expression e ctx in
   let meta =
     match meta with
-    | S.Aggregate (p, rv) ->
-        let p = translate_opt_mplace p in
-        let rv = typed_value_to_rvalue ctx rv in
-        Aggregate (p, rv)
     | S.Assignment (p, rv) ->
         let p = translate_mplace p in
         let rv = typed_value_to_rvalue ctx rv in
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index f86d40f0..c1dcff87 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -139,12 +139,6 @@ let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
   synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ]
     [ arg0_place; arg1_place ] dest dest_place expr
 
-let synthesize_aggregated_value (aggr_v : V.typed_value) (place : mplace option)
-    (expr : expression option) : expression option =
-  match expr with
-  | None -> None
-  | Some expr -> Some (Meta (Aggregate (place, aggr_v), expr))
-
 let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
     expression option =
   match expr with
-- 
cgit v1.2.3