diff options
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 19 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 21 |
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 |