Lean: Fixing struct of enums

src/sail_lean_backend/pretty_print_lean.ml

@@ -88,7 +88,7 @@ let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) =
   let env = env_of_annot annot in
   let identity body = body in
   match (paux, typs) with
-  | P_tuple [], _ ->
+  | P_tuple [], _ | P_lit (L_aux (L_unit, _)), _ ->
       let annot = (l, mk_tannot Env.empty unit_typ) in
       ([(P_aux (P_lit (mk_lit L_unit), annot), unit_typ)], identity)
   (* The type checker currently has a special case for a single arg type; if
@@ -104,8 +104,6 @@ let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) =
       let argexp = E_aux (E_tuple argexps, annot) in
       let bindargs (E_aux (_, bannot) as body) = E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
       (argpats, bindargs)
-  (* TODO Occurrences of the unit literal are removed right now, in order to be able to compile `initialize_registers`. *)
-  | P_lit (L_aux (L_unit, _)), _ -> ([], identity)
   | _, [typ] -> ([(pat, typ)], identity)
   | _, _ -> unreachable l __POS__ "Unexpected pattern/type combination"
 
@@ -445,8 +443,7 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
   | E_ref id -> string "Reg " ^^ doc_id_ctor id
   | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.")
 
-and doc_fexp with_arrow ctx (FE_aux (FE_fexp (field, e), _)) =
-  doc_id_ctor field ^^ string " := " ^^ wrap_with_left_arrow with_arrow (doc_exp false ctx e)
+and doc_fexp with_arrow ctx (FE_aux (FE_fexp (field, e), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp false ctx e
 
 let doc_binder ctx i t =
   let paranthesizer =

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/struct_of_enum.expected.lean

@@ -0,0 +1,31 @@
+import Out.Sail.Sail
+
+open Sail
+
+inductive e_test where | VAL
+  deriving Inhabited
+open e_test
+
+structure s_test where
+  f : e_test
+
+abbrev SailM := StateM Unit
+
+def undefined_e_test (lit : Unit) : SailM e_test := do
+  sorry
+
+/-- Type quantifiers: arg_ : Int, 0 ≤ arg_ ∧ arg_ ≤ 0 -/
+def e_test_of_num (arg_ : Nat) : e_test :=
+  match arg_ with
+  | _ => VAL
+
+def num_of_e_test (arg_ : e_test) : Int :=
+  match arg_ with
+  | VAL => 0
+
+def undefined_s_test (lit : Unit) : SailM s_test := do
+  (pure { f := (← (undefined_e_test ())) })
+
+def initialize_registers (lit : Unit) : Unit :=
+  ()
+

test/lean/struct_of_enum.sail

@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+enum e_test = {
+  VAL,
+}
+
+struct s_test = {
+  f : e_test
+}

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 :=
   ()