Improve tuple handling in remove_e_assign rewrite

- don't rewrite unnecessarily
- add type information where possible

Author: bacam

src/lib/rewrites.ml

@@ -2974,7 +2974,7 @@ let rec rewrite_var_updates (E_aux (expaux, ((l, _) as annot)) as exp) =
          we would introduce a new variable rather than using a wildcard and unit literal
       *)
       let is_trivial = function E_aux ((E_id _ | E_lit _), _) -> true | _ -> false in
-      if List.for_all is_trivial exps then exp
+      if find_updated_vars exp |> IdSet.is_empty then exp
       else (
         let tuple_typ = typ_of exp in
         let typs =
@@ -3004,7 +3004,7 @@ let rec rewrite_var_updates (E_aux (expaux, ((l, _) as annot)) as exp) =
               else (
                 let lb =
                   if is_unit_typ typ then LB_aux (LB_val (P_aux (P_wild, swaptyp typ annot), exp), annot)
-                  else LB_aux (LB_val (P_aux (P_id id, swaptyp typ annot), exp), annot)
+                  else LB_aux (LB_val (add_p_typ env typ (P_aux (P_id id, swaptyp typ annot)), exp), annot)
                 in
                 E_aux (E_let (lb, tup), annot)
               )

test/lean/match.expected.lean

@@ -181,21 +181,18 @@ def match_read (x : E) : SailM Unit := do
     | C => readReg r_C)
 
 def const16 (_ : Unit) : ((BitVec 16) × Bool) :=
-  let t__4 := (0xFFFF : (BitVec 16))
-  (t__4, true)
+  ((0xFFFF : (BitVec 16)), true)
 
 def const32 (_ : Unit) : ((BitVec 32) × Bool) :=
-  let t__2 := (0xEEEEEEEE : (BitVec 32))
-  (t__2, false)
+  ((0xEEEEEEEE : (BitVec 32)), false)
 
 /-- Type quantifiers: k_n : Nat, k_n ≥ 0 -/
 def match_width (x : (BitVec k_n)) : (BitVec (2 * k_n)) :=
   let (foo, _) : ((BitVec k_n) × Bool) :=
     match (Sail.BitVec.length x) with
     | 16 => (const16 ())
     | 32 => (const32 ())
-    | n => (let t__0 := (BitVec.zero n)
-      (t__0, false))
+    | n => ((BitVec.zero n), false)
   (foo ++ foo)
 
 def initialize_registers (_ : Unit) : SailM Unit := do

test/lean/tuples.expected.lean

@@ -35,24 +35,21 @@ open Sail
 
 namespace Out.Functions
 
-def let5 := (20, 300000000000000000000000)
+def let0 := (20, 300000000000000000000000)
 
 def y :=
-  let (y, z) := let5
+  let (y, z) := let0
   y
 
 def z :=
-  let (y, z) := let5
+  let (y, z) := let0
   z
 
 def tuple1 (_ : Unit) : (Int × Int × ((BitVec 2) × Unit)) :=
-  let t__4 := ((0b10 : (BitVec 2)), ())
-  (3, 5, t__4)
+  (3, 5, ((0b10 : (BitVec 2)), ()))
 
 def tuple2 (_ : Unit) : SailM (Int × Int) := do
-  let t__0 ← do (undefined_int ())
-  let t__1 ← do (undefined_int ())
-  (pure (t__0, t__1))
+  (pure ((← (undefined_int ())), (← (undefined_int ()))))
 
 def initialize_registers (_ : Unit) : Unit :=
   ()

test/lean/typquant.expected.lean

@@ -158,8 +158,7 @@ def hex_bits_signed2_forwards (bv : (BitVec k_nn)) : (Nat × String) :=
     bif (BEq.beq (BitVec.access bv (len -i 1)) 1#1)
     then "stub1"
     else "stub2"
-  let t__3 := (Sail.BitVec.length bv)
-  (t__3, s)
+  ((Sail.BitVec.length bv), s)
 
 /-- Type quantifiers: k_nn : Nat, k_nn > 0 -/
 def hex_bits_signed2_forwards_matches (bv : (BitVec k_nn)) : Bool :=

test/lean/undefined.expected.lean

@@ -37,12 +37,8 @@ namespace Out.Functions
 
 /-- Type quantifiers: n : Int -/
 def foo (n : Int) : SailM (Bool × (BitVec 1) × Int × Nat × (BitVec 3)) := do
-  let t__0 ← do (undefined_bool ())
-  let t__1 ← do (undefined_bit ())
-  let t__2 ← do (undefined_int ())
-  let t__3 ← do (undefined_nat ())
-  let t__4 ← do (undefined_bitvector 3)
-  (pure (t__0, t__1, t__2, t__3, t__4))
+  (pure ((← (undefined_bool ())), (← (undefined_bit ())), (← (undefined_int ())), (← (undefined_nat
+        ())), (← (undefined_bitvector 3))))
 
 /-- Type quantifiers: n : Int -/
 def bar (n : Int) : SailM (Vector Int 4) := do

test/typecheck/pass/tuple_cons_assign.sail

@@ -0,0 +1,14 @@
+default Order dec
+$include <prelude.sail>
+
+/* The remove_e_assign rewrite was lifting out the subexpressions from the tuple,
+   but failing to include enough typing information.
+
+   Note that this test is really for the Rocq and Lem backends; plain type
+   checking should be straightforward.
+   */
+
+function test(xs : list(int), ys : list(int)) -> (list(int), list(int)) = {
+  var x : int = 1;
+  (({x = x + 1; x}) :: xs, 3 :: ys)
+}

test/typecheck/pass/tuple_cons_simple.sail

@@ -0,0 +1,13 @@
+default Order dec
+$include <prelude.sail>
+
+/* The remove_e_assign rewrite was lifting out the subexpressions from the tuple,
+   but failing to include enough typing information.  This simple case ought to
+   be left alone.
+
+   Note that this test is really for the Rocq and Lem backends; plain type
+   checking should be straightforward.
+   */
+
+function test(xs : list(int), ys : list(int)) -> (list(int), list(int)) =
+  (5 :: xs, 3 :: ys)