Skip to content

Commit 479e75a

Browse files
ineolineol
authored
Lean: compat between early return and exception (rems-project#1553)
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`.
1 parent 0bfd9c0 commit 479e75a

38 files changed

+112
-34
lines changed

‎src/sail_lean_backend/Sail/Sail.lean‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -603,9 +603,50 @@ def sailTryCatchE (e : ExceptT β (PreSailM RegisterType c ue) α) (h : ue → E
603603

604604
end Regs
605605

606+
section SailME
607+
608+
variable {Register : Type} {RT : Register → Type} [DecidableEq Register] [Hashable Register]
609+
610+
variable (RT) in
611+
abbrev PreSailME c ue α := ExceptT (Error ue ⊕ α) (PreSailM RT c ue)
612+
613+
instance: MonadExceptOf (Error ue) (PreSailME RT c ue α) where
614+
throw e := MonadExcept.throw (.inl e)
615+
tryCatch x h := MonadExcept.tryCatch x (fun e => match e with | .inl e => h e | .inr _ => MonadExcept.throw e)
616+
617+
def PreSailME.run (m : PreSailME RT c ue α α) : PreSailM RT c ue α := do
618+
match (← ExceptT.run m) with
619+
| .error (.inr e) => pure e
620+
| .error (.inl e) => throw e
621+
| .ok e => pure e
622+
623+
def _root_.ExceptT.map_error [Monad m] (e : ExceptT ε m α) (f : ε → ε') : ExceptT ε' m α :=
624+
ExceptT.mk <| do
625+
match ← e.run with
626+
| .ok x => pure $ .ok x
627+
| .error e => pure $ .error (f e)
628+
629+
instance [∀ x, CoeT α x α'] :
630+
CoeT (PreSailME RT c ue α β) e (PreSailME RT c ue α' β) where
631+
coe := e.map_error (fun x => match x with | .inl e => .inl e | .inr e => .inr e)
632+
633+
def PreSailME.throw (e : α) : PreSailME RT c ue α β :=
634+
MonadExceptOf.throw (Sum.inr (α := Error ue) e)
635+
636+
instance : Inhabited (PreSail.SequentialState RT trivialChoiceSource) where
637+
default := ⟨default, (), default, default, default, default⟩
638+
639+
end SailME
606640

607641
end PreSail
608642

643+
abbrev ExceptM α := ExceptT α Id
644+
645+
def ExceptM.run (m : ExceptM α α) : α :=
646+
match (ExceptT.run m) with
647+
| .error e => e
648+
| .ok e => e
649+
609650
namespace Sail
610651

611652
open PreSail

‎src/sail_lean_backend/Sail/Specialization.lean‎

Lines changed: 3 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -77,39 +77,16 @@ abbrev print_bits_effect {w : Nat} (str : String) (x : BitVec w) : SailM Unit :=
7777

7878
abbrev print_endline_effect (str : String) : SailM Unit := PreSail.print_endline_effect str
7979

80-
abbrev SailME α := ExceptT α SailM
80+
def SailME.run (m : SailME α α) : SailM α := PreSail.PreSailME.run m
8181

82-
def SailME.run (m : SailME α α) : SailM α := do
83-
match (← ExceptT.run m) with
84-
| .error e => pure e
85-
| .ok e => pure e
86-
87-
def _root_.ExceptT.map_error [Monad m] (e : ExceptT ε m α) (f : ε → ε') : ExceptT ε' m α :=
88-
ExceptT.mk <| do
89-
match ← e.run with
90-
| .ok x => pure $ .ok x
91-
| .error e => pure $ .error (f e)
92-
93-
instance [∀ x, CoeT α x α'] : CoeT (SailME α β) e (SailME α' β) where
94-
coe := e.map_error (fun x => x)
95-
96-
def SailME.throw (e : α) : SailME α β := MonadExcept.throw e
97-
98-
abbrev ExceptM α := ExceptT α Id
99-
100-
def ExceptM.run (m : ExceptM α α) : α :=
101-
match (ExceptT.run m) with
102-
| .error e => e
103-
| .ok e => e
82+
def SailME.throw (e : α) : SailME α β := PreSail.PreSailME.throw e
10483

10584
abbrev sailTryCatchE (e : SailME β α) (h : exception → SailME β α) : SailME β α := PreSail.sailTryCatchE e h
10685

107-
instance : Inhabited (PreSail.SequentialState RegisterType trivialChoiceSource) where
108-
default := ⟨default, (), default, default, default, default⟩
109-
11086
def unwrapValue [Inhabited α] (x : SailM α) : α :=
11187
match x.run default with
11288
| .ok x _ => x
11389
| _ => default
11490

11591
end Sail
92+

‎src/sail_lean_backend/pretty_print_lean.ml‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1470,8 +1470,12 @@ let doc_monad_abbrev defs (has_registers : bool) =
14701470
in
14711471
let excdef = find_exc_typ defs in
14721472
let pp_register_type = string "PreSailM RegisterType trivialChoiceSource exception" in
1473-
let monad = separate space [string "abbrev"; string "SailM"; coloneq; pp_register_type] ^^ hardline ^^ hardline in
1474-
separate hardline (remove_empties [excdef; monad])
1473+
let pp_register_type_e = string "PreSailME RegisterType trivialChoiceSource exception" in
1474+
let monad = separate space [string "abbrev"; string "SailM"; coloneq; pp_register_type] in
1475+
let monad_e =
1476+
separate space [string "abbrev"; string "SailME"; coloneq; pp_register_type_e] ^^ hardline ^^ hardline
1477+
in
1478+
separate hardline (remove_empties [excdef; monad; monad_e])
14751479

14761480
let doc_instantiations ctx env =
14771481
let params = Monad_params.find_monad_parameters env in

‎test/lean/SailTinyArm.expected.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -447,6 +447,7 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 64)) where
447447
abbrev exception := Unit
448448

449449
abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
450+
abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
450451

451452
instance : Arch where
452453
va_size := 64

‎test/lean/append.expected.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
2626
abbrev exception := Unit
2727

2828
abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
29+
abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
2930

3031

3132
XXXXXXXXX

‎test/lean/atom_bool.expected.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
1616
abbrev exception := Unit
1717

1818
abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
19+
abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
1920

2021

2122
XXXXXXXXX

‎test/lean/bitfield.expected.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ instance : Inhabited (RegisterRef RegisterType (BitVec 8)) where
3535
abbrev exception := Unit
3636

3737
abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
38+
abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
3839

3940

4041
XXXXXXXXX

‎test/lean/bitvec_operation.expected.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ abbrev RegisterType : Register -> Type := PEmpty.elim
2626
abbrev exception := Unit
2727

2828
abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
29+
abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
2930

3031

3132
XXXXXXXXX

‎test/lean/early_return.expected.lean‎

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
4444
abbrev exception := Unit
4545

4646
abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
47+
abbrev SailME := PreSailME RegisterType trivialChoiceSource exception
4748

4849

4950
XXXXXXXXX
@@ -68,7 +69,7 @@ open option
6869
open Register
6970
open E
7071

71-
/-- Type quantifiers: k_ex2332_ : Bool, k_ex2331_ : Bool -/
72+
/-- Type quantifiers: k_ex2346_ : Bool, k_ex2345_ : Bool -/
7273
def neq_bool (x : Bool) (y : Bool) : Bool :=
7374
(! (x == y))
7475

@@ -446,7 +447,7 @@ def match_early_return_loop (x : E) : SailM E := SailME.run do
446447
| C => writeReg r_C A
447448
readReg r_B
448449

449-
/-- Type quantifiers: k_ex2648_ : Bool -/
450+
/-- Type quantifiers: k_ex2662_ : Bool -/
450451
def ite_early_return (x : Bool) : SailM E := SailME.run do
451452
writeReg r_A (← readReg r_C)
452453
let y ← (( do
@@ -457,7 +458,7 @@ def ite_early_return (x : Bool) : SailM E := SailME.run do
457458
else readReg r_B ) : SailME E E )
458459
readReg r_B
459460

460-
/-- Type quantifiers: k_ex2650_ : Bool -/
461+
/-- Type quantifiers: k_ex2664_ : Bool -/
461462
def ite_early_return_inloop (x : Bool) : SailM E := SailME.run do
462463
let loop_i_lower := 0
463464
let loop_i_upper := 10
@@ -476,7 +477,7 @@ def ite_early_return_inloop (x : Bool) : SailM E := SailME.run do
476477
(pure loop_vars)
477478
readReg r_B
478479

479-
/-- Type quantifiers: k_ex2654_ : Bool -/
480+
/-- Type quantifiers: k_ex2668_ : Bool -/
480481
def ite_early_return_loop (x : Bool) : SailM E := SailME.run do
481482
if (x : Bool)
482483
then
@@ -496,7 +497,7 @@ def ite_early_return_loop (x : Bool) : SailM E := SailME.run do
496497
def unit_type (x : E) : SailM Unit := do
497498
writeReg r_A x
498499

499-
/-- Type quantifiers: k_ex2658_ : Bool -/
500+
/-- Type quantifiers: k_ex2672_ : Bool -/
500501
def ite_early_return_seq (x : Bool) : SailM E := SailME.run do
501502
writeReg r_A (← readReg r_C)
502503
let y ← (( do
@@ -508,6 +509,20 @@ def ite_early_return_seq (x : Bool) : SailM E := SailME.run do
508509
else readReg r_B ) : SailME E E )
509510
readReg r_B
510511

512+
/-- Type quantifiers: k_ex2674_ : Bool -/
513+
def ite_early_return_exit (x : Bool) : SailM E := SailME.run do
514+
writeReg r_A (← readReg r_C)
515+
let y ← (( do
516+
if (x : Bool)
517+
then
518+
SailME.throw (← do
519+
readReg r_A)
520+
else readReg r_B ) : SailME E E )
521+
if (x : Bool)
522+
then throw Error.Exit
523+
else (pure ())
524+
readReg r_B
525+
511526
def initialize_registers (_ : Unit) : SailM Unit := do
512527
writeReg r_A (← (undefined_E ()))
513528
writeReg r_B (← (undefined_E ()))

‎test/lean/early_return.sail‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -202,4 +202,12 @@ function ite_early_return_seq(x : bool) -> E = {
202202
r_A = r_C;
203203
let y : E = if x then {unit_type(A); return r_A} else r_B;
204204
r_B
205-
}
205+
}
206+
207+
function ite_early_return_exit(x : bool) -> E = {
208+
r_A = r_C;
209+
let y : E = if x then return r_A else r_B;
210+
if x then exit();
211+
r_B
212+
}
213+

0 commit comments

Comments
 (0)