1 files changed, 38 insertions, 2 deletions
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index b9bad7c9..1a30687c 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -49,7 +49,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
             assert (otherwise_see = None);
             (* Return *)
             ExpandInt (int_ty, branches, otherwise)
-        | T.Adt (adt_id, regions, types) -> (
+        | T.Adt (_, _, _) -> (
             (* An ADT expansion can lead to branching: check if this is the case *)
             match ls with
             | [] -> failwith "Ill-formed ADT expansion"
@@ -72,7 +72,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
                     ls
                 in
                 ExpandEnum exp)
-        | T.Ref (r, ty, rkind) -> (
+        | T.Ref (_, _, _) -> (
             (* Reference expansion: there should be one branch *)
             match ls with
             | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
@@ -87,3 +87,39 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
     =
   let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
   synthesize_symbolic_expansion sv [ Some see ] exprl
+
+let synthesize_function_call (call_id : call_id) (type_params : T.ety list)
+    (args : V.typed_value list) (dest : V.symbolic_value)
+    (expr : expression option) : expression option =
+  match expr with
+  | None -> None
+  | Some expr ->
+      let call = { call_id; type_params; args; dest } in
+      Some (FunCall (call, expr))
+
+let synthesize_regular_function_call (fun_id : A.fun_id)
+    (call_id : V.FunCallId.id) (type_params : T.ety list)
+    (args : V.typed_value list) (dest : V.symbolic_value)
+    (expr : expression option) : expression option =
+  synthesize_function_call (Fun (fun_id, call_id)) type_params args dest expr
+
+let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
+    (dest : V.symbolic_value) (expr : expression option) : expression option =
+  synthesize_function_call (Unop unop) [] [ arg ] dest expr
+
+let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
+    (arg1 : V.typed_value) (dest : V.symbolic_value) (expr : expression option)
+    : expression option =
+  synthesize_function_call (Binop binop) [] [ arg0; arg1 ] dest expr
+
+let synthesize_aggregated_value (aggr_v : V.typed_value)
+    (expr : expression option) : expression option =
+  match expr with
+  | None -> None
+  | Some expr -> Some (Meta (Aggregate aggr_v, expr))
+
+let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
+    expression option =
+  match expr with
+  | None -> None
+  | Some expr -> Some (EndAbstraction (abs, expr))