From abee28555eb9f95b1c548cc17b9fe746bc982b56 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 18:50:19 +0200
Subject: Add some utilities for progress

---
 backends/lean/Base/Progress/Base.lean     | 19 +++++++++++++++++++
 backends/lean/Base/Progress/Progress.lean | 21 ++++++++++++++++-----
 2 files changed, 35 insertions(+), 5 deletions(-)

(limited to 'backends')

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
-- 
cgit v1.2.3