summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Base.lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Primitives/Base.lean')
-rw-r--r--backends/lean/Base/Primitives/Base.lean30
1 files changed, 15 insertions, 15 deletions
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 0c64eca1..4c5b2795 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -41,7 +41,7 @@ deriving Repr, BEq
open Error
inductive Result (α : Type u) where
- | ret (v: α): Result α
+ | ok (v: α): Result α
| fail (e: Error): Result α
| div
deriving Repr, BEq
@@ -56,31 +56,31 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
/- HELPERS -/
-def ret? {α: Type u} (r: Result α): Bool :=
+def ok? {α: Type u} (r: Result α): Bool :=
match r with
- | ret _ => true
+ | ok _ => true
| fail _ | div => false
def div? {α: Type u} (r: Result α): Bool :=
match r with
| div => true
- | ret _ | fail _ => false
+ | ok _ | fail _ => false
def massert (b:Bool) : Result Unit :=
- if b then ret () else fail assertionFailure
+ if b then ok () else fail assertionFailure
macro "prove_eval_global" : tactic => `(tactic| first | apply Eq.refl | decide)
-def eval_global {α: Type u} (x: Result α) (_: ret? x := by prove_eval_global) : α :=
+def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) : α :=
match x with
| fail _ | div => by contradiction
- | ret x => x
+ | ok x => x
/- DO-DSL SUPPORT -/
def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
match x with
- | ret v => f v
+ | ok v => f v
| fail v => fail v
| div => div
@@ -88,11 +88,11 @@ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Resu
instance : Bind Result where
bind := bind
--- Allows using return x in do-blocks
+-- Allows using pure x in do-blocks
instance : Pure Result where
- pure := fun x => ret x
+ pure := fun x => ok x
-@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
+@[simp] theorem bind_ok (x : α) (f : α → Result β) : bind (.ok 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]
@@ -103,14 +103,14 @@ instance : Pure Result where
-- 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 } :=
+def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } :=
match o with
- | ret x => ret ⟨x, rfl⟩
+ | ok x => ok ⟨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_ok (x : α) (f : α → Result β) :
+ (do let y ← .ok 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]