From 536972c8b94e136c25ec77b00ff4c185f228f1b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= <leo.lveb@gmail.com>
Date: Sat, 29 Nov 2025 14:08:49 +0000
Subject: [PATCH] Lean: compat between early return and exception

Early returns are encoded using an exception monad in Lean, and it did
not allow to throw exceptions. As a by-product, we move some definitions
from `Specialization.lean` to `Sail.lean`.
---
 src/sail_lean_backend/Sail/Sail.lean          | 41 +++++++++++++++++++
 .../Sail/Specialization.lean                  | 29 ++-----------
 src/sail_lean_backend/pretty_print_lean.ml    |  8 +++-
 test/lean/SailTinyArm.expected.lean           |  1 +
 test/lean/append.expected.lean                |  1 +
 test/lean/atom_bool.expected.lean             |  1 +
 test/lean/bitfield.expected.lean              |  1 +
 test/lean/bitvec_operation.expected.lean      |  1 +
 test/lean/early_return.expected.lean          | 25 ++++++++---
 test/lean/early_return.sail                   | 10 ++++-
 test/lean/enum.expected.lean                  |  1 +
 test/lean/errors.expected.lean                |  1 +
 test/lean/extern.expected.lean                |  1 +
 test/lean/extern_bitvec.expected.lean         |  1 +
 test/lean/implicit.expected.lean              |  1 +
 test/lean/ite.expected.lean                   |  1 +
 test/lean/let.expected.lean                   |  1 +
 test/lean/loop.expected.lean                  |  1 +
 test/lean/map_tactics.expected.lean           |  1 +
 test/lean/mapping.expected.lean               |  1 +
 test/lean/match.expected.lean                 |  1 +
 test/lean/match_bv.expected.lean              |  1 +
 test/lean/option.expected.lean                |  1 +
 test/lean/range.expected.lean                 |  1 +
 test/lean/register_vector.expected.lean       |  1 +
 test/lean/registers.expected.lean             |  1 +
 test/lean/riscv_duopod.expected.lean          |  1 +
 test/lean/string.expected.lean                |  1 +
 test/lean/struct.expected.lean                |  1 +
 test/lean/struct_of_enum.expected.lean        |  1 +
 test/lean/termination.expected.lean           |  1 +
 test/lean/trivial.expected.lean               |  1 +
 test/lean/tuples.expected.lean                |  1 +
 test/lean/type_kid.expected.lean              |  1 +
 test/lean/typedef.expected.lean               |  1 +
 test/lean/typquant.expected.lean              |  1 +
 test/lean/undefined.expected.lean             |  1 +
 test/lean/union.expected.lean                 |  1 +
 38 files changed, 112 insertions(+), 34 deletions(-)

diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
index a9298a304..288fdc6a8 100644
--- a/src/sail_lean_backend/Sail/Sail.lean
+++ b/src/sail_lean_backend/Sail/Sail.lean
@@ -603,9 +603,50 @@ def sailTryCatchE (e : ExceptT β (PreSailM RegisterType c ue) α) (h : ue → E
 
 end Regs
 
+section SailME
+
+variable {Register : Type} {RT : Register → Type} [DecidableEq Register] [Hashable Register]
+
+variable (RT) in
+abbrev PreSailME c ue α := ExceptT (Error ue ⊕ α) (PreSailM RT c ue)
+
+instance: MonadExceptOf (Error ue) (PreSailME RT c ue α) where
+  throw e := MonadExcept.throw (.inl e)
+  tryCatch x h := MonadExcept.tryCatch x (fun e => match e with | .inl e => h e | .inr _ => MonadExcept.throw e)
+
+def PreSailME.run (m : PreSailME RT c ue α α) : PreSailM RT c ue α := do
+  match (← ExceptT.run m) with
+    | .error (.inr e) => pure e
+    | .error (.inl e) => throw e
+    | .ok e => pure e
+
+def _root_.ExceptT.map_error [Monad m] (e : ExceptT ε m α) (f : ε → ε') : ExceptT ε' m α :=
+  ExceptT.mk <| do
+    match ← e.run with
+    | .ok x => pure $ .ok x
+    | .error e => pure $ .error (f e)
+
+instance [∀ x, CoeT α x α'] :
+    CoeT (PreSailME RT c ue α β) e (PreSailME RT c ue α' β) where
+  coe := e.map_error (fun x => match x with | .inl e => .inl e | .inr e => .inr e)
+
+def PreSailME.throw (e : α) : PreSailME RT c ue α β :=
+    MonadExceptOf.throw (Sum.inr (α := Error ue) e)
+
+instance : Inhabited (PreSail.SequentialState RT trivialChoiceSource) where
+  default := ⟨default, (), default, default, default, default⟩
+
+end SailME
 
 end PreSail
 
+abbrev ExceptM α := ExceptT α Id
+
+def ExceptM.run (m : ExceptM α α) : α :=
+  match (ExceptT.run m) with
+    | .error e => e
+    | .ok e => e
+
 namespace Sail
 
 open PreSail
diff --git a/src/sail_lean_backend/Sail/Specialization.lean b/src/sail_lean_backend/Sail/Specialization.lean
index ecb6758e9..7734a0c35 100644
--- a/src/sail_lean_backend/Sail/Specialization.lean
+++ b/src/sail_lean_backend/Sail/Specialization.lean
@@ -77,39 +77,16 @@ abbrev print_bits_effect {w : Nat} (str : String) (x : BitVec w) : SailM Unit :=
 
 abbrev print_endline_effect (str : String) : SailM Unit := PreSail.print_endline_effect str
 
-abbrev SailME α := ExceptT α SailM
+def SailME.run (m : SailME α α) : SailM α := PreSail.PreSailME.run m
 
-def SailME.run (m : SailME α α) : SailM α := do
-  match (← ExceptT.run m) with
-    | .error e => pure e
-    | .ok e => pure e
-
-def _root_.ExceptT.map_error [Monad m] (e : ExceptT ε m α) (f : ε → ε') : ExceptT ε' m α :=
-  ExceptT.mk <| do
-    match ← e.run with
-    | .ok x => pure $ .ok x
-    | .error e => pure $ .error (f e)
-
-instance [∀ x, CoeT α x α'] : CoeT (SailME α β) e (SailME α' β) where
-  coe := e.map_error (fun x => x)
-
-def SailME.throw (e : α) : SailME α β := MonadExcept.throw e
-
-abbrev ExceptM α := ExceptT α Id
-
-def ExceptM.run (m : ExceptM α α) : α :=
-  match (ExceptT.run m) with
-    | .error e => e
-    | .ok e => e
+def SailME.throw (e : α) : SailME α β := PreSail.PreSailME.throw e
 
 abbrev sailTryCatchE (e : SailME β α) (h : exception → SailME β α) : SailME β α := PreSail.sailTryCatchE e h
 
-instance : Inhabited (PreSail.SequentialState RegisterType trivialChoiceSource) where
-  default := ⟨default, (), default, default, default, default⟩
-
 def unwrapValue [Inhabited α] (x : SailM α) : α :=
   match x.run default with
   | .ok x _ => x
   | _ => default
 
 end Sail
+
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index b9468714b..55b008d0e 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -1470,8 +1470,12 @@ let doc_monad_abbrev defs (has_registers : bool) =
   in
   let excdef = find_exc_typ defs in
   let pp_register_type = string "PreSailM RegisterType trivialChoiceSource exception" in
-  let monad = separate space [string "abbrev"; string "SailM"; coloneq; pp_register_type] ^^ hardline ^^ hardline in
-  separate hardline (remove_empties [excdef; monad])
+  let pp_register_type_e = string "PreSailME RegisterType trivialChoiceSource exception" in
+  let monad = separate space [string "abbrev"; string "SailM"; coloneq; pp_register_type] in
+  let monad_e =
+    separate space [string "abbrev"; string "SailME"; coloneq; pp_register_type_e] ^^ hardline ^^ hardline
+  in
+  separate hardline (remove_empties [excdef; monad; monad_e])
 
 let doc_instantiations ctx env =
   let params = Monad_params.find_monad_parameters env in
diff --git a/test/lean/SailTinyArm.expected.lean b/test/lean/SailTinyArm.expected.lean
index 70401e0bc..9872e3392 100644
--- a/test/lean/SailTinyArm.expected.lean
+++ b/test/lean/SailTinyArm.expected.lean
@@ -447,6 +447,7 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 64)) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 instance : Arch where
   va_size := 64
diff --git a/test/lean/append.expected.lean b/test/lean/append.expected.lean
index fc01ff779..d1b28ac76 100644
--- a/test/lean/append.expected.lean
+++ b/test/lean/append.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/atom_bool.expected.lean b/test/lean/atom_bool.expected.lean
index d97afca12..af548a3fd 100644
--- a/test/lean/atom_bool.expected.lean
+++ b/test/lean/atom_bool.expected.lean
@@ -16,6 +16,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
index f57499e6b..b8e907c4f 100644
--- a/test/lean/bitfield.expected.lean
+++ b/test/lean/bitfield.expected.lean
@@ -35,6 +35,7 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 8)) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
index 54b0d3d38..5ee0190d7 100644
--- a/test/lean/bitvec_operation.expected.lean
+++ b/test/lean/bitvec_operation.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/early_return.expected.lean b/test/lean/early_return.expected.lean
index a5e8877c0..49374e5df 100644
--- a/test/lean/early_return.expected.lean
+++ b/test/lean/early_return.expected.lean
@@ -44,6 +44,7 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
@@ -68,7 +69,7 @@ open option
 open Register
 open E
 
-/-- Type quantifiers: k_ex2332_ : Bool, k_ex2331_ : Bool -/
+/-- Type quantifiers: k_ex2346_ : Bool, k_ex2345_ : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (! (x == y))
 
@@ -446,7 +447,7 @@ def match_early_return_loop (x : E) : SailM E := SailME.run do
   | C => writeReg r_C A
   readReg r_B
 
-/-- Type quantifiers: k_ex2648_ : Bool -/
+/-- Type quantifiers: k_ex2662_ : Bool -/
 def ite_early_return (x : Bool) : SailM E := SailME.run do
   writeReg r_A (← readReg r_C)
   let y ← (( do
@@ -457,7 +458,7 @@ def ite_early_return (x : Bool) : SailM E := SailME.run do
     else readReg r_B ) : SailME E E )
   readReg r_B
 
-/-- Type quantifiers: k_ex2650_ : Bool -/
+/-- Type quantifiers: k_ex2664_ : Bool -/
 def ite_early_return_inloop (x : Bool) : SailM E := SailME.run do
   let loop_i_lower := 0
   let loop_i_upper := 10
@@ -476,7 +477,7 @@ def ite_early_return_inloop (x : Bool) : SailM E := SailME.run do
   (pure loop_vars)
   readReg r_B
 
-/-- Type quantifiers: k_ex2654_ : Bool -/
+/-- Type quantifiers: k_ex2668_ : Bool -/
 def ite_early_return_loop (x : Bool) : SailM E := SailME.run do
   if (x : Bool)
   then
@@ -496,7 +497,7 @@ def ite_early_return_loop (x : Bool) : SailM E := SailME.run do
 def unit_type (x : E) : SailM Unit := do
   writeReg r_A x
 
-/-- Type quantifiers: k_ex2658_ : Bool -/
+/-- Type quantifiers: k_ex2672_ : Bool -/
 def ite_early_return_seq (x : Bool) : SailM E := SailME.run do
   writeReg r_A (← readReg r_C)
   let y ← (( do
@@ -508,6 +509,20 @@ def ite_early_return_seq (x : Bool) : SailM E := SailME.run do
     else readReg r_B ) : SailME E E )
   readReg r_B
 
+/-- Type quantifiers: k_ex2674_ : Bool -/
+def ite_early_return_exit (x : Bool) : SailM E := SailME.run do
+  writeReg r_A (← readReg r_C)
+  let y ← (( do
+    if (x : Bool)
+    then
+      SailME.throw (← do
+          readReg r_A)
+    else readReg r_B ) : SailME E E )
+  if (x : Bool)
+  then throw Error.Exit
+  else (pure ())
+  readReg r_B
+
 def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg r_A (← (undefined_E ()))
   writeReg r_B (← (undefined_E ()))
diff --git a/test/lean/early_return.sail b/test/lean/early_return.sail
index 81f8663bc..6a3cfedcf 100644
--- a/test/lean/early_return.sail
+++ b/test/lean/early_return.sail
@@ -202,4 +202,12 @@ function ite_early_return_seq(x : bool) -> E = {
   r_A = r_C;
   let y : E = if x then {unit_type(A); return r_A} else r_B;
   r_B
-}
\ No newline at end of file
+}
+
+function ite_early_return_exit(x : bool) -> E = {
+  r_A = r_C;
+  let y : E = if x then return r_A else r_B;
+  if x then exit();
+  r_B
+}
+
diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
index 1bacddfb2..fbd0430c7 100644
--- a/test/lean/enum.expected.lean
+++ b/test/lean/enum.expected.lean
@@ -29,6 +29,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/errors.expected.lean b/test/lean/errors.expected.lean
index a65d86aee..26e75e752 100644
--- a/test/lean/errors.expected.lean
+++ b/test/lean/errors.expected.lean
@@ -33,6 +33,7 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 1)) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
index 6eb870e8b..cef480616 100644
--- a/test/lean/extern.expected.lean
+++ b/test/lean/extern.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
index 5630fe03f..9d146cb12 100644
--- a/test/lean/extern_bitvec.expected.lean
+++ b/test/lean/extern_bitvec.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
index 10ffe68ee..667d43dfa 100644
--- a/test/lean/implicit.expected.lean
+++ b/test/lean/implicit.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean
index 1a39de036..0f3113699 100644
--- a/test/lean/ite.expected.lean
+++ b/test/lean/ite.expected.lean
@@ -37,6 +37,7 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
index 4597031b4..d9ababce1 100644
--- a/test/lean/let.expected.lean
+++ b/test/lean/let.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/loop.expected.lean b/test/lean/loop.expected.lean
index bf13090f7..03d4328af 100644
--- a/test/lean/loop.expected.lean
+++ b/test/lean/loop.expected.lean
@@ -33,6 +33,7 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/map_tactics.expected.lean b/test/lean/map_tactics.expected.lean
index 1c548f65e..674be6c56 100644
--- a/test/lean/map_tactics.expected.lean
+++ b/test/lean/map_tactics.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/mapping.expected.lean b/test/lean/mapping.expected.lean
index 775a67dd7..25b67711e 100644
--- a/test/lean/mapping.expected.lean
+++ b/test/lean/mapping.expected.lean
@@ -29,6 +29,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
index 6a84ee7d0..821d5ede3 100644
--- a/test/lean/match.expected.lean
+++ b/test/lean/match.expected.lean
@@ -40,6 +40,7 @@ instance : Inhabited (RegisterRef RegisterType E) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/match_bv.expected.lean b/test/lean/match_bv.expected.lean
index 129f89bd6..17110e531 100644
--- a/test/lean/match_bv.expected.lean
+++ b/test/lean/match_bv.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/option.expected.lean b/test/lean/option.expected.lean
index 1132803d6..0ff6fc447 100644
--- a/test/lean/option.expected.lean
+++ b/test/lean/option.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean
index 8d651b79c..81edf6bfc 100644
--- a/test/lean/range.expected.lean
+++ b/test/lean/range.expected.lean
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
index bd0a0c41a..b9f16f2ed 100644
--- a/test/lean/register_vector.expected.lean
+++ b/test/lean/register_vector.expected.lean
@@ -97,6 +97,7 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 64)) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean
index e2f780985..660e5eacb 100644
--- a/test/lean/registers.expected.lean
+++ b/test/lean/registers.expected.lean
@@ -56,6 +56,7 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/riscv_duopod.expected.lean b/test/lean/riscv_duopod.expected.lean
index 7b90872ad..03729ea48 100644
--- a/test/lean/riscv_duopod.expected.lean
+++ b/test/lean/riscv_duopod.expected.lean
@@ -55,6 +55,7 @@ instance : Inhabited (RegisterRef RegisterType (Vector (BitVec 64) 32)) where
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/string.expected.lean b/test/lean/string.expected.lean
index 7833018ad..82693e340 100644
--- a/test/lean/string.expected.lean
+++ b/test/lean/string.expected.lean
@@ -18,6 +18,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
index 008f531c5..edc7e6941 100644
--- a/test/lean/struct.expected.lean
+++ b/test/lean/struct.expected.lean
@@ -43,6 +43,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean
index eaa7d7d32..d176c8073 100644
--- a/test/lean/struct_of_enum.expected.lean
+++ b/test/lean/struct_of_enum.expected.lean
@@ -33,6 +33,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/termination.expected.lean b/test/lean/termination.expected.lean
index fd902f944..a33047809 100644
--- a/test/lean/termination.expected.lean
+++ b/test/lean/termination.expected.lean
@@ -29,6 +29,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean
index 33d25304c..22d1d8840 100644
--- a/test/lean/trivial.expected.lean
+++ b/test/lean/trivial.expected.lean
@@ -16,6 +16,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean
index 2bc58c2fb..d292f7607 100644
--- a/test/lean/tuples.expected.lean
+++ b/test/lean/tuples.expected.lean
@@ -16,6 +16,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/type_kid.expected.lean b/test/lean/type_kid.expected.lean
index 2d582e9bd..26caf31ab 100644
--- a/test/lean/type_kid.expected.lean
+++ b/test/lean/type_kid.expected.lean
@@ -16,6 +16,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
index c21433a7a..96cfce3ff 100644
--- a/test/lean/typedef.expected.lean
+++ b/test/lean/typedef.expected.lean
@@ -36,6 +36,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
index dabd7dea3..d11076f94 100644
--- a/test/lean/typquant.expected.lean
+++ b/test/lean/typquant.expected.lean
@@ -30,6 +30,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/undefined.expected.lean b/test/lean/undefined.expected.lean
index 5a6cb715d..7f3d6ffd4 100644
--- a/test/lean/undefined.expected.lean
+++ b/test/lean/undefined.expected.lean
@@ -18,6 +18,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX
diff --git a/test/lean/union.expected.lean b/test/lean/union.expected.lean
index 0077d497d..24b9d75a1 100644
--- a/test/lean/union.expected.lean
+++ b/test/lean/union.expected.lean
@@ -36,6 +36,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
 abbrev exception := Unit
 
 abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
+abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
 
 
 XXXXXXXXX