add monad declaration in files without register use

src/sail_lean_backend/pretty_print_lean.ml

@@ -641,27 +641,29 @@ let inhabit_enum ctx typ_map =
 
 let doc_reg_info env global registers =
   let ctx = initial_context env global in
-
   let type_map = List.fold_left add_reg_typ Bindings.empty registers in
   let type_map = Bindings.bindings type_map in
-
   separate hardline
     [
       register_enums registers;
       type_enum ctx registers;
-      string "abbrev SailM := PreSailM RegisterType";
-      empty;
       string "open RegisterRef";
       inhabit_enum ctx type_map;
       empty;
-      empty;
     ]
+
+
+let doc_monad_abbrev (has_registers : bool) =
+  let pp_register_type = if has_registers then string "PreSailM RegisterType" else string "StateM Unit" in
+  separate space [string "abbrev"; string "SailM"; coloneq; pp_register_type] ^^ hardline ^^ hardline
 
 let pp_ast_lean (env : Type_check.env) effect_info ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o =
   let defs = remove_imports defs 0 in
   let regs = State.find_registers defs in
   let global = { effect_info } in
-  let register_refs = match regs with [] -> empty | _ -> doc_reg_info env global regs in
+  let has_registers = List.length regs > 0 in
+  let register_refs = if has_registers then doc_reg_info env global regs else empty in
+  let monad = doc_monad_abbrev has_registers in
   let types, fundefs = doc_defs (initial_context env global) defs in
-  print o (types ^^ register_refs ^^ fundefs);
+  print o (types ^^ register_refs ^^ monad ^^ fundefs);
   ()

test/lean/atom_bool.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 def foo : Bool :=
   true
 

test/lean/bitfield.expected.lean

@@ -12,11 +12,10 @@ open Register
 abbrev RegisterType : Register → Type
   | .R => (BitVec 8)
 
-abbrev SailM := PreSailM RegisterType
-
 open RegisterRef
 instance : Inhabited (RegisterRef RegisterType (BitVec 8)) where
   default := .Reg R
+abbrev SailM := PreSailM RegisterType
 
 def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do
   sorry

test/lean/bitvec_operation.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 def bitvector_eq (x : (BitVec 16)) (y : (BitVec 16)) : Bool :=
   (Eq x y)
 

test/lean/enum.expected.lean

@@ -6,6 +6,8 @@ inductive E where | A | B | C
   deriving Inhabited
 open E
 
+abbrev SailM := StateM Unit
+
 def undefined_E : SailM E := do
   sorry
 

test/lean/extern.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 def extern_add : Int :=
   (Int.add 5 4)
 

test/lean/extern_bitvec.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 def extern_const : (BitVec 64) :=
   (0xFFFF000012340000 : (BitVec 64))
 

test/lean/ite.expected.lean

@@ -12,13 +12,12 @@ abbrev RegisterType : Register → Type
   | .B => Bool
   | .R => Nat
 
-abbrev SailM := PreSailM RegisterType
-
 open RegisterRef
 instance : Inhabited (RegisterRef RegisterType Bool) where
   default := .Reg B
 instance : Inhabited (RegisterRef RegisterType Nat) where
   default := .Reg R
+abbrev SailM := PreSailM RegisterType
 
 /-- Type quantifiers: n : Int, 0 ≤ n -/
 def elif (n : Nat) : (BitVec 1) :=

test/lean/let.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 def foo : (BitVec 16) :=
   let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)

test/lean/match.expected.lean

@@ -6,6 +6,8 @@ inductive E where | A | B | C
   deriving Inhabited
 open E
 
+abbrev SailM := StateM Unit
+
 def undefined_E : SailM E := do
   sorry
 

test/lean/range.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 /-- Type quantifiers: x : Int, 0 ≤ x ∧ x ≤ 31 -/
 def f_int (x : Nat) : Int :=
   0

test/lean/register_vector.expected.lean

@@ -74,11 +74,10 @@ abbrev RegisterType : Register → Type
   | .R30 => (BitVec 64)
   | ._PC => (BitVec 64)
 
-abbrev SailM := PreSailM RegisterType
-
 open RegisterRef
 instance : Inhabited (RegisterRef RegisterType (BitVec 64)) where
   default := .Reg _PC
+abbrev SailM := PreSailM RegisterType
 
 def GPRs : Vector (RegisterRef RegisterType (BitVec 64)) 31 :=
   #v[Reg R30, Reg R29, Reg R28, Reg R27, Reg R26, Reg R25, Reg R24, Reg R23, Reg R22, Reg R21,

test/lean/registers.expected.lean

@@ -20,8 +20,6 @@ abbrev RegisterType : Register → Type
   | .R1 => (BitVec 64)
   | .R0 => (BitVec 64)
 
-abbrev SailM := PreSailM RegisterType
-
 open RegisterRef
 instance : Inhabited (RegisterRef RegisterType (BitVec 1)) where
   default := .Reg BIT
@@ -33,6 +31,7 @@ instance : Inhabited (RegisterRef RegisterType Int) where
   default := .Reg INT
 instance : Inhabited (RegisterRef RegisterType Nat) where
   default := .Reg NAT
+abbrev SailM := PreSailM RegisterType
 
 def test : SailM Int := do
   writeReg INT (HAdd.hAdd (← readReg INT) 1)

test/lean/struct.expected.lean

@@ -14,11 +14,10 @@ open Register
 abbrev RegisterType : Register → Type
   | .r => My_struct
 
-abbrev SailM := PreSailM RegisterType
-
 open RegisterRef
 instance : Inhabited (RegisterRef RegisterType My_struct) where
   default := .Reg r
+abbrev SailM := PreSailM RegisterType
 
 def undefined_My_struct (lit : Unit) : SailM My_struct := do
   (pure { field1 := (← sorry)

test/lean/trivial.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 def foo (y : Unit) : Unit :=
   y
 

test/lean/tuples.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 def tuple1 : (Int × Int × ((BitVec 2) × Unit)) :=
   (3, 5, ((0b10 : (BitVec 2)), ()))
 

test/lean/type_kid.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 /-- Type quantifiers: k_a : Type -/
 def foo (x : k_a) : (k_a × k_a) :=
   (x, x)

test/lean/typedef.expected.lean

@@ -8,6 +8,8 @@ abbrev xlen_bytes : Int := 8
 
 abbrev xlenbits := (BitVec 64)
 
+abbrev SailM := StateM Unit
+
 /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
 def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
   (Sail.BitVec.zeroExtend v m)

test/lean/typquant.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+abbrev SailM := StateM Unit
+
 /-- Type quantifiers: n : Int -/
 def foo (n : Int) : (BitVec 4) :=
   (0xF : (BitVec 4))

test/lean/union.expected.lean

@@ -21,6 +21,8 @@ inductive my_option where
 
 open my_option
 
+abbrev SailM := StateM Unit
+
 def undefined_rectangle (lit : Unit) : SailM rectangle := do
   (pure { width := (← sorry)
           height := (← sorry) })