make unit literals anonymous

src/sail_lean_backend/pretty_print_lean.ml

@@ -66,6 +66,7 @@ let pat_is_plain_binder env (P_aux (p, _)) =
   | P_tuple _ -> Some (Some (Id_aux (Id "tuple", Unknown)), None)
   | P_list _ -> Some (Some (Id_aux (Id "list", Unknown)), None)
   | P_cons (_, _) -> Some (Some (Id_aux (Id "cons", Unknown)), None)
+  | P_lit (L_aux (L_unit, _)) -> Some (Some (Id_aux (Id "_", Unknown)), None)
   | P_lit _ -> Some (Some (Id_aux (Id "lit", Unknown)), None)
   | _ -> None
 

test/lean/atom_bool.expected.lean

@@ -4,9 +4,9 @@ open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
-def foo (lit : Unit) : Bool :=
+def foo (_ : Unit) : Bool :=
   true
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/bitfield.expected.lean

@@ -17,7 +17,7 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 8)) where
   default := .Reg R
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
-def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do
+def undefined_cr_type (_ : Unit) : SailM (BitVec 8) := do
   (undefined_bitvector 8)
 
 def Mk_cr_type (v : (BitVec 8)) : (BitVec 8) :=
@@ -83,6 +83,6 @@ def _set_cr_type_LT (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec
   let r := (← (reg_deref r_ref))
   writeRegRef r_ref (_update_cr_type_LT r v)
 
-def initialize_registers (lit : Unit) : SailM Unit := do
+def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg R (← (undefined_cr_type ()))
 

test/lean/bitvec_operation.expected.lean

@@ -60,6 +60,6 @@ def bitvector_access' (x : (BitVec 16)) (i : Nat) : (BitVec 1) :=
 def bitvector_plus_int (x : (BitVec 16)) (i : Int) : (BitVec 16) :=
   (BitVec.addInt x i)
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/enum.expected.lean

@@ -9,7 +9,7 @@ open E
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
-def undefined_E (lit : Unit) : SailM E := do
+def undefined_E (_ : Unit) : SailM E := do
   (internal_pick [A, B, C])
 
 /-- Type quantifiers: arg_ : Nat, 0 ≤ arg_ ∧ arg_ ≤ 2 -/
@@ -25,6 +25,6 @@ def num_of_E (arg_ : E) : Int :=
   | B => 1
   | C => 2
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/errors.expected.lean

@@ -26,6 +26,6 @@ def test_assert (b : Bool) : SailM (BitVec 1) := do
   assert b "b is false"
   (pure 1#1)
 
-def initialize_registers (lit : Unit) : SailM Unit := do
+def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg dummy (← (undefined_bit ()))
 

test/lean/extern.expected.lean

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

test/lean/extern_bitvec.expected.lean

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

test/lean/implicit.expected.lean

@@ -11,6 +11,6 @@ def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
 def foo (x : (BitVec 8)) : (BitVec 16) :=
   (EXTZ x)
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : 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 (lit : Unit) : SailM Unit := do
+def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg R (← (undefined_nat ()))
   writeReg B (← (undefined_bool ()))
 

test/lean/let.expected.lean

@@ -4,14 +4,14 @@ open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
-def foo (lit : Unit) : (BitVec 16) :=
+def foo (_ : Unit) : (BitVec 16) :=
   let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)
 
-def bar (lit : Unit) : (BitVec 16) :=
+def bar (_ : Unit) : (BitVec 16) :=
   let z : (BitVec 16) := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/match.expected.lean

@@ -24,7 +24,7 @@ instance : Inhabited (RegisterRef RegisterType E) where
   default := .Reg r_A
 abbrev SailM := PreSailM RegisterType trivialChoiceSource
 
-def undefined_E (lit : Unit) : SailM E := do
+def undefined_E (_ : Unit) : SailM E := do
   (internal_pick [A, B, C])
 
 def match_enum (x : E) : (BitVec 1) :=
@@ -55,7 +55,7 @@ def match_reg (x : E) : SailM E := do
   | B => readReg r_B
   | C => readReg r_C
 
-def initialize_registers (lit : Unit) : SailM Unit := do
+def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg r_A (← (undefined_E ()))
   writeReg r_B (← (undefined_E ()))
   writeReg r_C (← (undefined_E ()))

test/lean/option.expected.lean

@@ -14,6 +14,6 @@ def option_match (x : (Option Unit)) (y : (BitVec 1)) : (Option (BitVec 1)) :=
   | some () => (some y)
   | none => none
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : 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 (lit : Unit) : Unit :=
+def initialize_registers (_ : 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 (lit : Unit) : SailM (BitVec 64) := do
+def rPC (_ : 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 (lit : Unit) : SailM Unit := do
+def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg _PC (← (undefined_bitvector 64))
   writeReg R30 (← (undefined_bitvector 64))
   writeReg R29 (← (undefined_bitvector 64))

test/lean/registers.expected.lean

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

test/lean/struct.expected.lean

@@ -21,7 +21,7 @@ structure Mem_write_request
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
-def undefined_My_struct (lit : Unit) : SailM My_struct := do
+def undefined_My_struct (_ : Unit) : SailM My_struct := do
   (pure { field1 := (← (undefined_int ()))
           field2 := (← (undefined_bit ())) })
 
@@ -43,6 +43,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 (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/struct_of_enum.expected.lean

@@ -13,7 +13,7 @@ structure s_test where
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
-def undefined_e_test (lit : Unit) : SailM e_test := do
+def undefined_e_test (_ : Unit) : SailM e_test := do
   (internal_pick [VAL])
 
 /-- Type quantifiers: arg_ : Nat, 0 ≤ arg_ ∧ arg_ ≤ 0 -/
@@ -25,9 +25,9 @@ def num_of_e_test (arg_ : e_test) : Int :=
   match arg_ with
   | VAL => 0
 
-def undefined_s_test (lit : Unit) : SailM s_test := do
+def undefined_s_test (_ : Unit) : SailM s_test := do
   (pure { f := (← (undefined_e_test ())) })
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/trivial.expected.lean

@@ -7,6 +7,6 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 def foo (y : Unit) : Unit :=
   y
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/tuples.expected.lean

@@ -4,12 +4,12 @@ open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
-def tuple1 (lit : Unit) : (Int × Int × ((BitVec 2) × Unit)) :=
+def tuple1 (_ : Unit) : (Int × Int × ((BitVec 2) × Unit)) :=
   (3, 5, ((0b10 : (BitVec 2)), ()))
 
-def tuple2 (lit : Unit) : SailM (Int × Int) := do
+def tuple2 (_ : Unit) : SailM (Int × Int) := do
   (pure ((← (undefined_int ())), (← (undefined_int ()))))
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/type_kid.expected.lean

@@ -8,6 +8,6 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 def foo (x : k_a) : (k_a × k_a) :=
   (x, x)
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : 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 (lit : Unit) : Unit :=
+def initialize_registers (_ : 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 (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/undefined.expected.lean

@@ -9,6 +9,6 @@ def foo (n : Int) : SailM (Bool × (BitVec 1) × Int × Nat × (BitVec 3)) := do
   (pure ((← (undefined_bool ())), (← (undefined_bit ())), (← (undefined_int ())), (← (undefined_nat
         ())), (← (undefined_bitvector 3))))
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/union.expected.lean

@@ -28,11 +28,11 @@ open my_option
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
-def undefined_rectangle (lit : Unit) : SailM rectangle := do
+def undefined_rectangle (_ : Unit) : SailM rectangle := do
   (pure { width := (← (undefined_int ()))
           height := (← (undefined_int ())) })
 
-def undefined_circle (lit : Unit) : SailM circle := do
+def undefined_circle (_ : Unit) : SailM circle := do
   (pure { radius := (← (undefined_int ())) })
 
 /-- Type quantifiers: k_a : Type -/
@@ -45,6 +45,6 @@ def is_none (opt : my_option k_a) : Bool :=
 def use_is_none (opt : my_option k_a) : Bool :=
   (is_none opt)
 
-def initialize_registers (lit : Unit) : Unit :=
+def initialize_registers (_ : Unit) : Unit :=
   ()