From 821b09b14794ebc2fe7b7047fc60fd56fb2cd107 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 19:03:17 +0200
Subject: Fix a small issue with the persistent state of progress

---
 backends/lean/Base/Progress/Base.lean     | 9 +++++++++
 backends/lean/Base/Progress/Progress.lean | 9 ++++-----
 2 files changed, 13 insertions(+), 5 deletions(-)

(limited to 'backends')

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 785b9362..72438d40 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -153,6 +153,15 @@ structure PSpecClassAttr where
   ext  : MapDeclarationExtension (NameMap Name)
   deriving Inhabited
 
+-- TODO: the original function doesn't define correctly the `addImportedFn`. Do a PR?
+def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
+  registerSimplePersistentEnvExtension {
+    name          := name,
+    addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insert k v) s) RBMap.empty,
+    addEntryFn    := fun s n => s.insert n.1 n.2 ,
+    toArrayFn     := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
+  }
+
 /- The persistent map from function to pspec theorems. -/
 initialize pspecAttr : PSpecAttr ← do
   let ext ← mkMapDeclarationExtension `pspecMap
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 9c75ee3c..84053150 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -291,16 +291,15 @@ namespace Test
 
   set_option trace.Progress true
 
-  -- #eval do pspecClassAttr.getState
-  -- #eval showStoredPSpec
-  -- #eval showStoredPSpecClass
+  #eval showStoredPSpec
+  #eval showStoredPSpecClass
 
-/-  theorem Scalar.add_spec {ty} {x y : Scalar ty}
+  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 [*] -/
+    simp [*]
 
 /-
   @[pspec]
-- 
cgit v1.2.3