summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
authorSon Ho2023-12-07 16:29:18 +0100
committerSon Ho2023-12-07 16:29:18 +0100
commitf7493580421d31b1d3798521b4f9154e69755f89 (patch)
treebbd020f2d69a0c00e92083e040808f4048962765 /backends/lean/Base/Progress
parentb3b53e369233247d41770432396fbd1932633c0d (diff)
Reorganize a bit
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Base.lean65
1 files changed, 4 insertions, 61 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 76a92795..cf2a3b70 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -2,6 +2,7 @@ import Lean
import Std.Lean.HashSet
import Base.Utils
import Base.Primitives.Base
+import Base.Lookup.Base
namespace Progress
@@ -166,67 +167,9 @@ structure PSpecClassExprAttr where
ext : MapDeclarationExtension (HashMap Expr 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)
- }
-
--- Declare an extension of maps of maps (using [RBMap]).
--- The important point is that we need to merge the bound values (which are maps).
-def mkMapMapDeclarationExtension [Inhabited β] (ord : α → α → Ordering)
- (name : Name := by exact decl_name%) :
- IO (MapDeclarationExtension (RBMap α β ord)) :=
- registerSimplePersistentEnvExtension {
- name := name,
- addImportedFn := fun a =>
- a.foldl (fun s a => a.foldl (
- -- We need to merge the maps
- fun s (k0, k1_to_v) =>
- match s.find? k0 with
- | none =>
- -- No binding: insert one
- s.insert k0 k1_to_v
- | some m =>
- -- There is already a binding: merge
- let m := RBMap.fold (fun m k v => m.insert k v) m k1_to_v
- s.insert k0 m)
- 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)
- }
-
--- Declare an extension of maps of maps (using [HashMap]).
--- The important point is that we need to merge the bound values (which are maps).
-def mkMapHashMapDeclarationExtension [BEq α] [Hashable α] [Inhabited β]
- (name : Name := by exact decl_name%) :
- IO (MapDeclarationExtension (HashMap α β)) :=
- registerSimplePersistentEnvExtension {
- name := name,
- addImportedFn := fun a =>
- a.foldl (fun s a => a.foldl (
- -- We need to merge the maps
- fun s (k0, k1_to_v) =>
- match s.find? k0 with
- | none =>
- -- No binding: insert one
- s.insert k0 k1_to_v
- | some m =>
- -- There is already a binding: merge
- let m := HashMap.fold (fun m k v => m.insert k v) m k1_to_v
- s.insert k0 m)
- 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
+ let ext ← Lookup.mkMapDeclarationExtension `pspecMap
let attrImpl : AttributeImpl := {
name := `pspec
descr := "Marks theorems to use with the `progress` tactic"
@@ -250,7 +193,7 @@ initialize pspecAttr : PSpecAttr ← do
/- The persistent map from type classes to pspec theorems -/
initialize pspecClassAttr : PSpecClassAttr ← do
let ext : MapDeclarationExtension (NameMap Name) ←
- mkMapMapDeclarationExtension Name.quickCmp `pspecClassMap
+ Lookup.mkMapMapDeclarationExtension Name.quickCmp `pspecClassMap
let attrImpl : AttributeImpl := {
name := `cpspec
descr := "Marks theorems to use for type classes with the `progress` tactic"
@@ -282,7 +225,7 @@ initialize pspecClassAttr : PSpecClassAttr ← do
/- The 2nd persistent map from type classes to pspec theorems -/
initialize pspecClassExprAttr : PSpecClassExprAttr ← do
let ext : MapDeclarationExtension (HashMap Expr Name) ←
- mkMapHashMapDeclarationExtension `pspecClassExprMap
+ Lookup.mkMapHashMapDeclarationExtension `pspecClassExprMap
let attrImpl : AttributeImpl := {
name := `cepspec
descr := "Marks theorems to use for type classes with the `progress` tactic"