Merge branch 'rems-project:sail2' into lean/Arch-class

rems-project · Feb 10, 2025 · e971e3e · e971e3e
2 parents 71badc2 + 31eba37
commit e971e3e
Show file tree

Hide file tree

Showing 19 changed files with 21 additions and 19 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -741,7 +741,9 @@ let doc_reg_info env global registers =
     [register_enums registers; type_enum ctx registers; string "open RegisterRef"; inhabit_enum ctx type_map; empty]
 
 let doc_monad_abbrev (has_registers : bool) =
-  let pp_register_type = if has_registers then string "PreSailM RegisterType" else string "StateM Unit" in
+  let pp_register_type =
+    if has_registers then string "PreSailM RegisterType" else string "PreSailM (fun (x : PEmpty.{1}) => nomatch x)"
+  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 =

diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml
@@ -73,7 +73,7 @@ let opt_lean_output_dir : string option ref = ref None
 
 let opt_lean_force_output : bool ref = ref false
 
-let lean_version : string = "lean4:nightly-2025-01-22"
+let lean_version : string = "lean4:nightly-2025-02-05"
 
 let lean_options =
   [

diff --git a/test/lean/atom_bool.expected.lean b/test/lean/atom_bool.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def foo (lit : Unit) : Bool :=
   true

diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def bitvector_eq (x : (BitVec 16)) (y : (BitVec 16)) : Bool :=
   (Eq x y)

diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
@@ -7,7 +7,7 @@ inductive E where | A | B | C
 
 open E
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def undefined_E (lit : Unit) : SailM E := do
   sorry

diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def extern_add (lit : Unit) : Int :=
   (Int.add 5 4)

diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def extern_const (lit : Unit) : (BitVec 64) :=
   (0xFFFF000012340000 : (BitVec 64))

diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
 def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=

diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def foo (lit : Unit) : (BitVec 16) :=
   let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))

diff --git a/test/lean/option.expected.lean b/test/lean/option.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def match_option (x : (Option (BitVec 1))) : (BitVec 1) :=
   match x with

diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 /-- Type quantifiers: x : Nat, 0 ≤ x ∧ x ≤ 31 -/
 def f_int (x : Nat) : Int :=

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -19,7 +19,7 @@ structure Mem_write_request
   value : (Option (BitVec (8 * k_n)))
   tag : (Option Bool)
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def undefined_My_struct (lit : Unit) : SailM My_struct := do
   (pure { field1 := sorry

diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean
@@ -11,7 +11,7 @@ open e_test
 structure s_test where
   f : e_test
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def undefined_e_test (lit : Unit) : SailM e_test := do
   sorry

diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def foo (y : Unit) : Unit :=
   y

diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def tuple1 (lit : Unit) : (Int × Int × ((BitVec 2) × Unit)) :=
   (3, 5, ((0b10 : (BitVec 2)), ()))

diff --git a/test/lean/type_kid.expected.lean b/test/lean/type_kid.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 /-- Type quantifiers: k_a : Type -/
 def foo (x : k_a) : (k_a × k_a) :=

diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
@@ -8,7 +8,7 @@ abbrev xlen_bytes : Int := 8
 
 abbrev xlenbits := (BitVec 64)
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
 def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=

diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 /-- Type quantifiers: n : Int -/
 def foo (n : Int) : (BitVec 4) :=

diff --git a/test/lean/union.expected.lean b/test/lean/union.expected.lean
@@ -26,7 +26,7 @@ inductive my_option (k_a : Type) where
 
 open my_option
 
-abbrev SailM := StateM Unit
+abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
 
 def undefined_rectangle (lit : Unit) : SailM rectangle := do
   (pure { width := sorry
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,7 +7,7 @@ inductive E where | A | B | C @@
     open E
-    abbrev SailM := StateM Unit
+    abbrev SailM := PreSailM (fun (x : PEmpty.{1}) => nomatch x)
     def undefined_E (lit : Unit) : SailM E := do
       sorry
@@ Expand Down @@