Fixing tests

test/lean/atom_bool.expected.lean

@@ -4,9 +4,9 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def foo : Bool :=
+def foo (lit : Unit) : Bool :=
   true
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/bitfield.expected.lean

@@ -83,6 +83,6 @@ def _set_cr_type_LT (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 1
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_LT r v)
 
-def initialize_registers : SailM Unit := do
+def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg R (← (undefined_cr_type ()))
 

test/lean/bitvec_operation.expected.lean

@@ -52,6 +52,6 @@ def bitvector_unsigned (x : (BitVec 16)) : Nat :=
 def bitvector_signed (x : (BitVec 16)) : Int :=
   (BitVec.toInt x)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/enum.expected.lean

@@ -8,7 +8,7 @@ open E
 
 abbrev SailM := StateM Unit
 
-def undefined_E : SailM E := do
+def undefined_E (lit : Unit) : SailM E := do
   sorry
 
 /-- Type quantifiers: arg_ : Int, 0 ≤ arg_ ∧ arg_ ≤ 2 -/
@@ -24,6 +24,6 @@ def num_of_E (arg_ : E) : Int :=
   | B => 1
   | C => 2
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/extern.expected.lean

@@ -4,42 +4,42 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def extern_add : Int :=
+def extern_add (lit : Unit) : Int :=
   (Int.add 5 4)
 
-def extern_sub : Int :=
+def extern_sub (lit : Unit) : Int :=
   (Int.sub 5 (-4))
 
-def extern_tdiv : Int :=
+def extern_tdiv (lit : Unit) : Int :=
   (Int.tdiv 5 4)
 
-def extern_tmod : Int :=
+def extern_tmod (lit : Unit) : Int :=
   (Int.tmod 5 4)
 
-def extern_tmod_positive : Int :=
+def extern_tmod_positive (lit : Unit) : Int :=
   (Int.tmod 5 4)
 
-def extern_negate : Int :=
+def extern_negate (lit : Unit) : Int :=
   (Int.neg (-5))
 
-def extern_mult : Int :=
+def extern_mult (lit : Unit) : Int :=
   (Int.mul 5 (-4))
 
-def extern_and : Bool :=
+def extern_and (lit : Unit) : Bool :=
   (Bool.and true false)
 
-def extern_and_no_flow : Bool :=
+def extern_and_no_flow (lit : Unit) : Bool :=
   (Bool.and true false)
 
-def extern_or : Bool :=
+def extern_or (lit : Unit) : Bool :=
   (Bool.or true false)
 
-def extern_eq_bool : Bool :=
+def extern_eq_bool (lit : Unit) : Bool :=
   (Eq true false)
 
-def extern_eq_bit : Bool :=
+def extern_eq_bit (lit : Unit) : Bool :=
   (Eq 0#1 1#1)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/extern_bitvec.expected.lean

@@ -4,12 +4,12 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def extern_const : (BitVec 64) :=
+def extern_const (lit : Unit) : (BitVec 64) :=
   (0xFFFF000012340000 : (BitVec 64))
 
-def extern_add : (BitVec 16) :=
+def extern_add (lit : Unit) : (BitVec 16) :=
   (HAdd.hAdd (0xFFFF : (BitVec 16)) (0x1234 : (BitVec 16)))
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/ite.expected.lean

@@ -42,7 +42,7 @@ def monadic_lines (n : Nat) : SailM Unit := do
        writeReg B b
   else writeReg B b
 
-def initialize_registers : SailM Unit := do
+def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg R sorry
   writeReg B sorry
 

test/lean/let.expected.lean

@@ -4,10 +4,10 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def foo : (BitVec 16) :=
+def foo (lit : Unit) : (BitVec 16) :=
   let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/match.expected.lean

@@ -8,7 +8,7 @@ open E
 
 abbrev SailM := StateM Unit
 
-def undefined_E : SailM E := do
+def undefined_E (lit : Unit) : SailM E := do
   sorry
 
 def match_enum (x : E) : (BitVec 1) :=
@@ -33,6 +33,6 @@ def match_pair (arg0 : Int) (arg1 : Int) : Int :=
   match x with
   | (a, b) => (HAdd.hAdd a b)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/range.expected.lean

@@ -24,6 +24,6 @@ def f_nnegvar (x : Nat) : Nat :=
 def f_unkn (x : Int) : Int :=
   x
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/register_vector.expected.lean

@@ -96,7 +96,7 @@ def rX (n : Nat) : SailM (BitVec 64) := do
   then (reg_deref (vectorAccess GPRs n))
   else (pure (0x0000000000000000 : (BitVec 64)))
 
-def rPC : SailM (BitVec 64) := do
+def rPC (lit : Unit) : SailM (BitVec 64) := do
   readReg _PC
 
 def wPC (pc : (BitVec 64)) : SailM Unit := do
@@ -110,7 +110,7 @@ def monad_test (r : Nat) : SailM (BitVec 1) := do
        then (pure 1#1)
        else (pure 0#1)
 
-def initialize_registers : SailM Unit := do
+def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg _PC sorry
   writeReg R30 sorry
   writeReg R29 sorry

test/lean/registers.expected.lean

@@ -33,11 +33,11 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
   default := .Reg NAT
 abbrev SailM := PreSailM RegisterType
 
-def test : SailM Int := do
+def test (lit : Unit) : SailM Int := do
   writeReg INT (HAdd.hAdd (← readReg INT) 1)
   readReg INT
 
-def initialize_registers : SailM Unit := do
+def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg R0 sorry
   writeReg R1 sorry
   writeReg INT sorry

test/lean/struct.expected.lean

@@ -9,8 +9,8 @@ structure My_struct where
 abbrev SailM := StateM Unit
 
 def undefined_My_struct (lit : Unit) : SailM My_struct := do
-  (pure { field1 := (← sorry)
-          field2 := (← sorry) })
+  (pure { field1 := sorry
+          field2 := sorry })
 
 def struct_field2 (s : My_struct) : (BitVec 1) :=
   s.field2
@@ -30,6 +30,6 @@ def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
 def undef_struct (x : (BitVec 1)) : SailM My_struct := do
   ((undefined_My_struct ()) : SailM My_struct)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/trivial.expected.lean

@@ -7,6 +7,6 @@ abbrev SailM := StateM Unit
 def foo (y : Unit) : Unit :=
   y
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/tuples.expected.lean

@@ -4,12 +4,12 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-def tuple1 : (Int × Int × ((BitVec 2) × Unit)) :=
+def tuple1 (lit : Unit) : (Int × Int × ((BitVec 2) × Unit)) :=
   (3, 5, ((0b10 : (BitVec 2)), ()))
 
-def tuple2 : SailM (Int × Int) := do
+def tuple2 (lit : Unit) : SailM (Int × Int) := do
   (pure ((← sorry), (← sorry)))
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/type_kid.expected.lean

@@ -8,6 +8,6 @@ abbrev SailM := StateM Unit
 def foo (x : k_a) : (k_a × k_a) :=
   (x, x)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/typedef.expected.lean

@@ -18,6 +18,6 @@ def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
 def EXTS {m : _} (v : (BitVec k_n)) : (BitVec m) :=
   (Sail.BitVec.signExtend v m)
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/typquant.expected.lean

@@ -12,6 +12,6 @@ def foo (n : Int) : (BitVec 4) :=
 def bar (x : (BitVec k_n)) : (BitVec k_n) :=
   x
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()
 

test/lean/union.expected.lean

@@ -24,18 +24,18 @@ open my_option
 abbrev SailM := StateM Unit
 
 def undefined_rectangle (lit : Unit) : SailM rectangle := do
-  (pure { width := (← sorry)
-          height := (← sorry) })
+  (pure { width := sorry
+          height := sorry })
 
 def undefined_circle (lit : Unit) : SailM circle := do
-  (pure { radius := (← sorry) })
+  (pure { radius := sorry })
 
 /-- Type quantifiers: k_a : Type -/
 def is_none (opt : my_option) : Bool :=
   match opt with
   | MySome _ => false
   | MyNone () => true
 
-def initialize_registers : Unit :=
+def initialize_registers (lit : Unit) : Unit :=
   ()