blob: 7c0fa3bb22158d39a2c714042662868d5fb0a25b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
import Lean
namespace Primitives
--------------------
-- ASSERT COMMAND --Std.
--------------------
open Lean Elab Command Term Meta
syntax (name := assert) "#assert" term: command
@[command_elab assert]
unsafe
def assertImpl : CommandElab := fun (_stx: Syntax) => do
runTermElabM (fun _ => do
let r ← evalTerm Bool (mkConst ``Bool) _stx[1]
if not r then
logInfo ("Assertion failed for:\n" ++ _stx[1])
throwError ("Expression reduced to false:\n" ++ _stx[1])
pure ())
#eval 2 == 2
#assert (2 == 2)
-------------
-- PRELUDE --
-------------
-- Results & monadic combinators
inductive Error where
| assertionFailure: Error
| integerOverflow: Error
| divisionByZero: Error
| arrayOutOfBounds: Error
| maximumSizeExceeded: Error
| panic: Error
deriving Repr, BEq
open Error
inductive Result (α : Type u) where
| ret (v: α): Result α
| fail (e: Error): Result α
| div
deriving Repr, BEq
open Result
instance Result_Inhabited (α : Type u) : Inhabited (Result α) :=
Inhabited.mk (fail panic)
instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
Nonempty.intro div
/- HELPERS -/
def ret? {α: Type u} (r: Result α): Bool :=
match r with
| ret _ => true
| fail _ | div => false
def div? {α: Type u} (r: Result α): Bool :=
match r with
| div => true
| ret _ | fail _ => false
def massert (b:Bool) : Result Unit :=
if b then ret () else fail assertionFailure
def eval_global {α: Type u} (x: Result α) (_: ret? x): α :=
match x with
| fail _ | div => by contradiction
| ret x => x
/- DO-DSL SUPPORT -/
def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
match x with
| ret v => f v
| fail v => fail v
| div => div
-- Allows using Result in do-blocks
instance : Bind Result where
bind := bind
-- Allows using return x in do-blocks
instance : Pure Result where
pure := fun x => ret x
@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
@[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
@[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
/- CUSTOM-DSL SUPPORT -/
-- Let-binding the Result of a monadic operation is oftentimes not sufficient,
-- because we may need a hypothesis for equational reasoning in the scope. We
-- rely on subtype, and a custom let-binding operator, in effect recreating our
-- own variant of the do-dsl
def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
match o with
| ret x => ret ⟨x, rfl⟩
| fail e => fail e
| div => div
@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
(do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]
@[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
(do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
@[simp] theorem bind_tc_div (f : α → Result β) :
(do let y ← div; f y) = div := by simp [Bind.bind, bind]
----------
-- MISC --
----------
@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x
@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
Use with `simp [ aeneas ]` -/
register_simp_attr aeneas
end Primitives
|
