summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Progress/Base.lean19
-rw-r--r--backends/lean/Base/Progress/Progress.lean21
2 files changed, 35 insertions, 5 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 0032c33d..785b9362 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -211,9 +211,28 @@ initialize pspecClassAttr : PSpecClassAttr ← do
def PSpecAttr.find? (s : PSpecAttr) (name : Name) : MetaM (Option Name) := do
return (s.ext.getState (← getEnv)).find? name
+def PSpecAttr.getState (s : PSpecAttr) : MetaM (NameMap Name) := do
+ pure (s.ext.getState (← getEnv))
+
def PSpecClassAttr.find? (s : PSpecClassAttr) (className argName : Name) : MetaM (Option Name) := do
match (s.ext.getState (← getEnv)).find? className with
| none => return none
| some map => return map.find? argName
+def PSpecClassAttr.getState (s : PSpecClassAttr) : MetaM (NameMap (NameMap Name)) := do
+ pure (s.ext.getState (← getEnv))
+
+def showStoredPSpec : MetaM Unit := do
+ let st ← pspecAttr.getState
+ let s := st.toList.foldl (fun s (f, th) => f!"{s}\n{f} → {th}") f!""
+ IO.println s
+
+def showStoredPSpecClass : MetaM Unit := do
+ let st ← pspecClassAttr.getState
+ let s := st.toList.foldl (fun s (f, m) =>
+ let ms := m.toList.foldl (fun s (f, th) =>
+ f!"{s}\n {f} → {th}") f!""
+ f!"{s}\n{f} → [{ms}]") f!""
+ IO.println s
+
end Progress
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 64d1c14a..9c75ee3c 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -208,7 +208,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
catch _ => none
| none =>
trace[Progress] "Could not find a pspec theorem for {fName}"
- throwError "TODO"
+ pure none
match res with
| some .Ok => return ()
| some (.Error msg) => throwError msg
@@ -228,7 +228,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
pure (some res)
catch _ => none
| none =>
- trace[Progress] "Could not find a pspec theorem for {fName}"
+ trace[Progress] "Could not find a class pspec theorem for ({fName}, {argName})"
pure none
match res with
| some .Ok => return ()
@@ -287,11 +287,22 @@ elab "progress" args:progressArgs : tactic =>
/-
-- TODO: remove
namespace Test
- open Primitives
+ open Primitives Result
set_option trace.Progress true
- set_option pp.rawOnError true
+ -- #eval do pspecClassAttr.getState
+ -- #eval showStoredPSpec
+ -- #eval showStoredPSpecClass
+
+/- theorem Scalar.add_spec {ty} {x y : Scalar ty}
+ (hmin : Scalar.min ty ≤ x.val + y.val)
+ (hmax : x.val + y.val ≤ Scalar.max ty) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+ progress
+ simp [*] -/
+
+/-
@[pspec]
theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
∃ (x: α), v.index α i = .ret x := by
@@ -299,7 +310,7 @@ namespace Test
simp
set_option trace.Progress false
-
+-/
end Test -/
end Progress