Lean: compat between early return and exception

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

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
+

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

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

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

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

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

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

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

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
-}
+}
+
+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
+}
+

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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