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/Progress.lean | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

(limited to 'backends/lean/Base/Progress/Progress.lean')

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