summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon Ho2023-07-04 12:13:09 +0200
committerSon Ho2023-07-04 12:13:09 +0200
commit40e21034fa9e955734351b78a8cc5f16315418bd (patch)
tree8a6ce8b44db023be2ccd23c75f470f5366ffaaef /backends/lean/Base
parent75fae6384716f24fe137283d4a41836782b9aec7 (diff)
Add an implemented_by attribute to fix
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Diverge/Base.lean29
1 files changed, 18 insertions, 11 deletions
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 89365d25..a8503107 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -57,6 +57,12 @@ 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
@@ -156,7 +162,14 @@ namespace Fix
(x : a) (n : Nat) : Prop :=
fix_fuel_pred f x n
- noncomputable
+ partial
+ def fixImpl (f : ((x:a) → Result (b x)) → (x:a) → Result (b x)) (x : a) : Result (b x) :=
+ f (fixImpl f) x
+
+ -- The fact that `fix` is implemented by `fixImpl` allows us to not mark the
+ -- functions defined with the fixed-point as noncomputable. One big advantage
+ -- is that it allows us to evaluate those functions, for instance with #eval.
+ @[implemented_by fixImpl]
def fix (f : ((x:a) → Result (b x)) → (x:a) → Result (b x)) (x : a) : Result (b x) :=
fix_fuel (least (fix_fuel_P f x)) f x
@@ -548,7 +561,7 @@ namespace FixI
def is_valid (f : ((i:id) → (x:a i) → Result (b i x)) → (i:id) → (x:a i) → Result (b i x)) : Prop :=
∀ k i x, is_valid_p k (λ k => f k i x)
- noncomputable def fix
+ def fix
(f : ((i:id) → (x:a i) → Result (b i x)) → (i:id) → (x:a i) → Result (b i x)) :
(i:id) → (x:a i) → Result (b i x) :=
kk_of_gen (Fix.fix (k_to_gen f))
@@ -808,7 +821,6 @@ namespace Ex1
split <;> simp
split <;> simp
- noncomputable
def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i)
-- The unfolding equation - diverges if `i < 0`
@@ -851,7 +863,6 @@ namespace Ex2
split <;> simp
apply is_valid_p_bind <;> intros <;> simp_all
- noncomputable
def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i)
-- The unfolding equation - diverges if `i < 0`
@@ -932,7 +943,6 @@ namespace Ex3
apply is_valid_p_bind; simp
intros; split <;> simp
- noncomputable
def is_even (i : Int): Result Bool :=
do
let r ← fix is_even_is_odd_body (.inl i)
@@ -940,7 +950,6 @@ namespace Ex3
| .inl b => .ret b
| .inr _ => .fail .panic
- noncomputable
def is_odd (i : Int): Result Bool :=
do
let r ← fix is_even_is_odd_body (.inr i)
@@ -1032,8 +1041,8 @@ namespace Ex4
theorem body_fix_eq : fix body = body (fix body) :=
is_valid_fix_fixed_eq body_is_valid
- noncomputable def is_even (i : Int) : Result Bool := fix body 0 i
- noncomputable def is_odd (i : Int) : Result Bool := fix body 1 i
+ def is_even (i : Int) : Result Bool := fix body 0 i
+ def is_odd (i : Int) : Result Bool := fix body 1 i
theorem is_even_eq (i : Int) : is_even i =
(if i = 0
@@ -1052,7 +1061,6 @@ namespace Ex4
.ret b) := by
simp [is_even, is_odd];
conv => lhs; rw [body_fix_eq]
-
end Ex4
namespace Ex5
@@ -1109,7 +1117,7 @@ namespace Ex5
intro k x
simp only [is_valid_p_same, is_valid_p_rec]
- noncomputable def id (t : Tree a) := fix id_body t
+ def id (t : Tree a) := fix id_body t
-- The unfolding equation
theorem id_eq (t : Tree a) :
@@ -1183,7 +1191,6 @@ namespace Ex6
Funs.is_valid_p_is_valid_p tys k bodies
(And.intro (list_nth_body_is_valid' k) (Funs.is_valid_p_Nil k))
- noncomputable
def list_nth {a: Type u} (ls : List a) (i : Int) : Result a :=
fix body 0 ⟨ a, ls , i ⟩