summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorJonathan Protzenko2023-01-30 18:05:21 -0800
committerSon HO2023-06-04 21:44:33 +0200
commit9804a5f28cedc79ac89d3b97ec6addb42752df3d (patch)
tree3549c94a08498578f3cfd145475891f45d4ba422 /backends/lean
parent1d6742c059cf53e73c9bc66cec7ac1f857830e78 (diff)
Fix some printing bits, proper syntax for terminates and decreases clauses
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/primitives.lean33
1 files changed, 30 insertions, 3 deletions
diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean
index dc2314fc..6a41d1f4 100644
--- a/backends/lean/primitives.lean
+++ b/backends/lean/primitives.lean
@@ -6,6 +6,8 @@ import Lean
-- Results & monadic combinators
+-- TODO: use syntactic conventions and capitalize error, result, etc.
+
inductive error where
| assertionFailure: error
| integerOverflow: error
@@ -23,17 +25,24 @@ deriving Repr, BEq
open result
+/- HELPERS -/
+
-- TODO: is there automated syntax for these discriminators?
def is_ret {α: Type} (r: result α): Bool :=
match r with
| result.ret _ => true
| result.fail _ => false
-def eval_global {α: Type} (x: result α) (h: is_ret x): α :=
+def massert (b:Bool) : result Unit :=
+ if b then .ret () else fail assertionFailure
+
+def eval_global {α: Type} (x: result α) (_: is_ret x): α :=
match x with
| result.fail _ => by contradiction
| result.ret x => x
+/- DO-DSL SUPPORT -/
+
def bind (x: result α) (f: α -> result β) : result β :=
match x with
| ret v => f v
@@ -47,8 +56,26 @@ instance : Bind result where
instance : Pure result where
pure := fun x => ret x
-def massert (b:Bool) : result Unit :=
- if b then return () else fail assertionFailure
+/- 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 : (o : result α) → result { x : α // o = ret x }
+ | .ret x => .ret ⟨x, rfl⟩
+ | .fail e => .fail e
+
+macro "let" h:ident " : " e:term " <-- " f:term : doElem =>
+ `(doElem| let ⟨$e, $h⟩ ← result.attach $f)
+
+-- Silly example of the kind of reasoning that this notation enables
+#eval do
+ let h: y <-- .ret (0: Nat)
+ let _: y = 0 := by cases h; simp
+ let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩
+ .ret r
----------------------
-- MACHINE INTEGERS --