summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Diverge/Base.lean65
-rw-r--r--backends/lean/Base/Diverge/Elab.lean2
-rw-r--r--backends/lean/Base/Diverge/ElabBase.lean8
-rw-r--r--backends/lean/Base/Primitives.lean25
4 files changed, 10 insertions, 90 deletions
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index a8503107..e22eb914 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -4,8 +4,7 @@ import Init.Data.List.Basic
import Mathlib.Tactic.RunCmd
import Mathlib.Tactic.Linarith
--- For debugging
-import Base.Diverge.ElabBase
+import Base.Primitives
/-
TODO:
@@ -35,68 +34,6 @@ set_option profiler.threshold 100
namespace Diverge
-namespace Primitives
-/-! # Copy-pasting from Primitives to make the file self-contained -/
-
-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
-
-def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β :=
- match x with
- | ret v => f v
- | fail v => fail v
- | div => div
-
-@[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]
-
--- 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_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]
-
-def div? {α: Type u} (r: Result α): Bool :=
- match r with
- | div => true
- | ret _ | fail _ => false
-
-end Primitives
-
namespace Fix
open Primitives
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index cc580265..41209021 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -174,7 +174,7 @@ private def list_nth_out_ty_inner (a :Type) (scrut1: @Sigma (List a) (fun (_ls :
(fun (_ls : List a) => Int)
(fun (_scrut1:@Sigma (List a) (fun (_ls : List a) => Int)) => Type)
scrut1
- (fun (_ls : List a) (_i : Int) => Diverge.Primitives.Result a)
+ (fun (_ls : List a) (_i : Int) => Primitives.Result a)
private def list_nth_out_ty_outer (scrut0 : @Sigma (Type) (fun (a:Type) =>
@Sigma (List a) (fun (_ls : List a) => Int))) :=
diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index fd95291e..1c1062c0 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -4,6 +4,7 @@ namespace Diverge
open Lean Elab Term Meta
+-- We can't define and use trace classes in the same file
initialize registerTraceClass `Diverge.elab
initialize registerTraceClass `Diverge.def
initialize registerTraceClass `Diverge.def.sigmas
@@ -11,8 +12,8 @@ initialize registerTraceClass `Diverge.def.genBody
initialize registerTraceClass `Diverge.def.valid
initialize registerTraceClass `Diverge.def.unfold
--- TODO: move
--- TODO: small helper
+-- Useful helper to explore definitions and figure out the variant
+-- of their sub-expressions.
def explore_term (incr : String) (e : Expr) : MetaM Unit :=
match e with
| .bvar _ => do logInfo m!"{incr}bvar: {e}"; return ()
@@ -81,8 +82,7 @@ private def test2 (x : Nat) : Nat := x
print_decl test1
print_decl test2
--- We adapted this from AbstractNestedProofs.visit
--- A map visitor function for expressions
+-- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`)
partial def mapVisit (k : Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do
let localInstances ← getLocalInstances
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 1185a07d..117f76a2 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -60,12 +60,12 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
/- HELPERS -/
-def ret? {α: Type} (r: Result α): Bool :=
+def ret? {α: Type u} (r: Result α): Bool :=
match r with
| ret _ => true
| fail _ | div => false
-def div? {α: Type} (r: Result α): Bool :=
+def div? {α: Type u} (r: Result α): Bool :=
match r with
| div => true
| ret _ | fail _ => false
@@ -73,14 +73,14 @@ def div? {α: Type} (r: Result α): Bool :=
def massert (b:Bool) : Result Unit :=
if b then ret () else fail assertionFailure
-def eval_global {α: Type} (x: Result α) (_: ret? x): α :=
+def eval_global {α: Type u} (x: Result α) (_: ret? x): α :=
match x with
| fail _ | div => by contradiction
| ret x => x
/- DO-DSL SUPPORT -/
-def bind (x: Result α) (f: α -> Result β) : Result β :=
+def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β :=
match x with
| ret v => f v
| fail v => fail v
@@ -111,23 +111,6 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
| fail e => fail e
| div => div
-macro "let" e:term " ⟵ " f:term : doElem =>
- `(doElem| let ⟨$e, h⟩ ← Result.attach $f)
-
--- TODO: any way to factorize both definitions?
-macro "let" e:term " <-- " f:term : doElem =>
- `(doElem| let ⟨$e, h⟩ ← Result.attach $f)
-
--- We call the hypothesis `h`, in effect making it unavailable to the user
--- (because too much shadowing). But in practice, once can use the French single
--- quote notation (input with f< and f>), where `‹ h ›` finds a suitable
--- hypothesis in the context, this is equivalent to `have x: h := by assumption in x`
-#eval do
- let y <-- .ret (0: Nat)
- let _: y = 0 := by cases ‹ ret 0 = ret y › ; decide
- let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩
- .ret r
-
@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
(do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]