diff options
| -rw-r--r-- | src/InterpreterExpressions.ml | 8 | ||||
| -rw-r--r-- | src/PrintPure.ml | 3 | ||||
| -rw-r--r-- | src/Pure.ml | 4 | ||||
| -rw-r--r-- | src/SymbolicAst.ml | 2 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 4 | ||||
| -rw-r--r-- | src/SynthesizeSymbolic.ml | 6 |
6 files changed, 3 insertions, 24 deletions
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 |