Make substantial simplifications to the pure AST

1 files changed, 41 insertions, 28 deletions

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index d46d8386..7fd72926 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -24,11 +24,22 @@ let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
   { value; ty }
 
 (* TODO: move *)
-let mk_typed_lvalue_from_var (v : var) : typed_lvalue =
-  let value = LvVar (Var v) in
+let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue =
+  let value = LvVar (Var (v, mp)) in
   let ty = v.ty in
   { value; ty }
 
+let mk_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue =
+  let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in
+  let ty = Adt (T.Tuple, tys) in
+  let value = LvAdt { variant_id = None; field_values = vl } in
+  { value; ty }
+
+let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id)
+    (vl : typed_lvalue list) : typed_lvalue =
+  let value = LvAdt { variant_id = Some variant_id; field_values = vl } in
+  { value; ty = adt_ty }
+
 let ty_as_integer (t : ty) : T.integer_type =
   match t with Integer int_ty -> int_ty | _ -> failwith "Unreachable"
 
@@ -786,7 +797,7 @@ let rec typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) :
           assert (variant_id = None);
           if field_values = [] then (ctx, None)
           else
-            let value = LvTuple field_values in
+            let value = LvAdt { variant_id = None; field_values } in
             let ty = ctx_translate_fwd_ty ctx av.ty in
             let lv : typed_lvalue = { value; ty } in
             (ctx, Some lv))
@@ -822,7 +833,7 @@ and aborrow_content_to_given_back (bc : V.aborrow_content) (ctx : bs_ctx) :
   | AEndedMutBorrow (mv, _) ->
       (* Return the meta-value *)
       let ctx, var = fresh_var_for_symbolic_value mv ctx in
-      (ctx, Some (mk_typed_lvalue_from_var var))
+      (ctx, Some (mk_typed_lvalue_from_var var None))
   | AEndedIgnoredMutBorrow _ ->
       (* This happens with nested borrows: we need to dive in *)
       raise Unimplemented
@@ -844,7 +855,7 @@ and aproj_to_given_back (aproj : V.aproj) (ctx : bs_ctx) :
   | AEndedProjBorrows mv ->
       (* Return the meta-value *)
       let ctx, var = fresh_var_for_symbolic_value mv ctx in
-      (ctx, Some (mk_typed_lvalue_from_var var))
+      (ctx, Some (mk_typed_lvalue_from_var var None))
   | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
       failwith "Unreachable"
 
@@ -947,7 +958,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
   (* Translate the next expression *)
   let e = translate_expression e ctx in
   (* Put together *)
-  Let (Call ([ (mk_typed_lvalue_from_var dest, dest_mplace) ], call), e)
+  Let (Call (mk_typed_lvalue_from_var dest dest_mplace, call), e)
 
 and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
     expression =
@@ -1002,7 +1013,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       (* Generate the assignemnts *)
       List.fold_right
         (fun (var, value) e ->
-          Let (Assign (mk_typed_lvalue_from_var var, None, value, None), e))
+          Let (Assign (mk_typed_lvalue_from_var var None, value, None), e))
         variables_values e
   | V.FunCall ->
       let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
@@ -1026,6 +1037,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       (* Retrieve the values given back by this function: those are the output
        * values *)
       let ctx, outputs = abs_to_given_back abs ctx in
+      let output = mk_tuple_lvalue outputs in
       (* Sanity check: the inputs and outputs have the proper number and the proper type *)
       let fun_id =
         match call.call_id with
@@ -1057,8 +1069,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       (* Put everything together *)
       let args_mplaces = List.map (fun _ -> None) inputs in
       let call = { func; type_params; args = inputs; args_mplaces } in
-      let outputs = List.map (fun x -> (x, None)) outputs in
-      Let (Call (outputs, call), e)
+      Let (Call (output, call), e)
   | V.SynthRet ->
       (* If we end the abstraction which consumed the return value of the function
        * we are synthesizing, we get back the borrows which were inside. Those borrows
@@ -1111,9 +1122,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       (* Generate the assignments *)
       List.fold_right
         (fun (given_back, input_var) e ->
-          Let
-            ( Assign (given_back, None, mk_typed_rvalue_from_var input_var, None),
-              e ))
+          Let (Assign (given_back, mk_typed_rvalue_from_var input_var, None), e))
         given_back_inputs e
 
 and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
@@ -1137,7 +1146,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
           let e = translate_expression e ctx in
           Let
             ( Assign
-                (mk_typed_lvalue_from_var var, None, scrutinee, scrutinee_mplace),
+                (mk_typed_lvalue_from_var var None, scrutinee, scrutinee_mplace),
               e )
       | SeAdt _ ->
           (* Should be in the [ExpandAdt] case *)
@@ -1158,14 +1167,11 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
               if is_enum then
                 (* This is an enumeration: introduce an [ExpandEnum] let-binding *)
                 let variant_id = Option.get variant_id in
-                let vars = List.map (fun x -> (Var x, None)) vars in
-                Let
-                  ( Deconstruct
-                      ( vars,
-                        Some (adt_id, variant_id),
-                        scrutinee,
-                        scrutinee_mplace ),
-                    branch )
+                let lvars =
+                  List.map (fun v -> mk_typed_lvalue_from_var v None) vars
+                in
+                let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in
+                Let (Assign (lv, scrutinee, scrutinee_mplace), branch)
               else
                 (* This is not an enumeration: introduce let-bindings for every
                  * field.
@@ -1187,12 +1193,16 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
                     let field_proj = gen_field_proj fid var in
                     Let
                       ( Assign
-                          (mk_typed_lvalue_from_var var, None, field_proj, None),
+                          (mk_typed_lvalue_from_var var None, field_proj, None),
                         e ))
                   id_var_pairs branch
           | T.Tuple ->
-              let vars = List.map (fun x -> (Var x, None)) vars in
-              Let (Deconstruct (vars, None, scrutinee, scrutinee_mplace), branch)
+              let vars =
+                List.map (fun x -> mk_typed_lvalue_from_var x None) vars
+              in
+              Let
+                ( Assign (mk_tuple_lvalue vars, scrutinee, scrutinee_mplace),
+                  branch )
           | T.Assumed T.Box ->
               (* There should be exactly one variable *)
               let var =
@@ -1202,8 +1212,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
                * identity when extracted (`box a == a`) *)
               Let
                 ( Assign
-                    ( mk_typed_lvalue_from_var var,
-                      None,
+                    ( mk_typed_lvalue_from_var var None,
                       scrutinee,
                       scrutinee_mplace ),
                   branch ))
@@ -1214,9 +1223,13 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
             (* There *must* be a variant id - otherwise there can't be several branches *)
             let variant_id = Option.get variant_id in
             let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
-            let vars = List.map (fun x -> Var x) vars in
+            let vars =
+              List.map (fun x -> mk_typed_lvalue_from_var x None) vars
+            in
+            let pat_ty = scrutinee.ty in
+            let pat = mk_adt_lvalue pat_ty variant_id vars in
             let branch = translate_expression branch ctx in
-            { variant_id; vars; branch }
+            { pat; branch }
           in
           let branches =
             List.map (fun (vid, svl, e) -> translate_branch vid svl e) branches