Fixing tests

src/sail_lean_backend/pretty_print_lean.ml

@@ -151,7 +151,8 @@ let rec doc_typ ctx (Typ_aux (t, _) as typ) =
     ->
       parens (string "BitVec " ^^ doc_nexp ctx m)
   | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp x, _)]) -> if provably_nneg ctx x then string "Nat" else string "Int"
-  | Typ_app (Id_aux (Id "register", _), t_app) -> string "RegisterRef Register " ^^ separate_map comma (doc_typ_app ctx) t_app
+  | Typ_app (Id_aux (Id "register", _), t_app) ->
+      string "RegisterRef Register " ^^ separate_map comma (doc_typ_app ctx) t_app
   | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) ->
       underscore (* TODO check if the type of implicit arguments can really be always inferred *)
   | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctx) ts)
@@ -536,11 +537,16 @@ let doc_typdef ctx (TD_aux (td, tannot) as full_typdef) =
       nest 2 (flow (break 1) [string "def"; string id; colon; string "Int"; coloneq; doc_nexp ctx ne])
   | _ -> failwith ("Type definition " ^ string_of_type_def_con full_typdef ^ " not translatable yet.")
 
-let doc_def ctx (DEF_aux (aux, def_annot) as def) =
-  match aux with
-  | DEF_fundef fdef -> group (doc_fundef ctx fdef) ^/^ hardline
-  | DEF_type tdef -> group (doc_typdef ctx tdef) ^/^ hardline
-  | _ -> empty
+let rec doc_defs_aux ctx defs types fundefs =
+  match defs with
+  | [] -> (types, fundefs)
+  | DEF_aux (DEF_fundef fdef, _) :: defs' ->
+      doc_defs_aux ctx defs' types (fundefs ^^ group (doc_fundef ctx fdef) ^/^ hardline)
+  | DEF_aux (DEF_type tdef, _) :: defs' ->
+      doc_defs_aux ctx defs' (types ^^ group (doc_typdef ctx tdef) ^/^ hardline) fundefs
+  | _ :: defs' -> doc_defs_aux ctx defs' types fundefs
+
+let doc_defs ctx defs = doc_defs_aux ctx defs empty empty
 
 (* Remove all imports for now, they will be printed in other files. Probably just for testing. *)
 let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.env) def list) depth =
@@ -706,6 +712,8 @@ let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check.
   let defs = remove_imports defs 0 in
   let regs = State.find_registers defs in
   let register_refs = doc_reg_info env regs in
-  let output : document = separate_map empty (doc_def (initial_context env)) defs in
-  print o (register_refs ^^ hardline ^^ hardline ^^ output);
+  let types, fundefs = doc_defs (initial_context env) defs in
+  (* let types = separate empty types in
+     let fundefs = separate empty fundefs in *)
+  print o (types ^^ register_refs ^^ hardline ^^ hardline ^^ fundefs);
   ()

test/lean/bitfield.expected.lean

@@ -2,6 +2,8 @@ import Out.Sail.Sail
 
 open Sail
 
+def cr_type := (BitVec 8)
+
 
 def Register (T : Type) := T
 abbrev Regstate := Unit
@@ -12,8 +14,6 @@ def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @registe
 def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
 def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
 
-def cr_type := (BitVec 8)
-
 def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do
   sorry
 

test/lean/bitvec_operation.expected.lean

@@ -2,6 +2,16 @@ import Out.Sail.Sail
 
 open Sail
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 def bitvector_eq (x : (BitVec 16)) (y : (BitVec 16)) : Bool :=
   (Eq x y)
 

test/lean/enum.expected.lean

@@ -5,6 +5,16 @@ open Sail
 inductive E where | A | B | C
   deriving Inhabited
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 def undefined_E : SailM E := do
   sorry
 

test/lean/extern.expected.lean

@@ -2,6 +2,16 @@ import Out.Sail.Sail
 
 open Sail
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 def extern_add : Int :=
   (Int.add 5 4)
 

test/lean/extern_bitvec.expected.lean

@@ -2,6 +2,16 @@ import Out.Sail.Sail
 
 open Sail
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 def extern_const : (BitVec 64) :=
   (0xFFFF000012340000 : (BitVec 64))
 

test/lean/let.expected.lean

@@ -2,6 +2,16 @@ import Out.Sail.Sail
 
 open Sail
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 def foo : (BitVec 16) :=
   let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)

test/lean/range.expected.lean

@@ -2,6 +2,16 @@ import Out.Sail.Sail
 
 open Sail
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 /-- Type quantifiers: x : Int, 0 ≤ x ∧ x ≤ 31 -/
 def f_int (x : Nat) : Int :=
   0

test/lean/struct.expected.lean

@@ -6,6 +6,16 @@ structure My_struct where
   field1 : Int
   field2 : (BitVec 1)
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 def undefined_My_struct (lit : Unit) : SailM My_struct := do
   (pure { field1 := (← sorry)
           field2 := (← sorry) })

test/lean/trivial.expected.lean

@@ -2,6 +2,16 @@ import Out.Sail.Sail
 
 open Sail
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 def foo (y : Unit) : Unit :=
   y
 

test/lean/tuples.expected.lean

@@ -2,6 +2,16 @@ import Out.Sail.Sail
 
 open Sail
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 def tuple1 : (Int × Int × ((BitVec 2) × Unit)) :=
   (3, 5, ((0b10 : (BitVec 2)), ()))
 

test/lean/typedef.expected.lean

@@ -8,6 +8,16 @@ def xlen_bytes : Int := 8
 
 def xlenbits := (BitVec 64)
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 /-- 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,16 @@ import Out.Sail.Sail
 
 open Sail
 
+
+def Register (T : Type) := T
+abbrev Regstate := Unit
+def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
+def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
+abbrev SailM := PreSailM Regstate
+def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
+def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
+def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg
+
 /-- Type quantifiers: n : Int -/
 def foo (n : Int) : (BitVec 4) :=
   (0xF : (BitVec 4))