diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 57 |
1 files changed, 54 insertions, 3 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 6f820a84..76a92795 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -167,7 +167,8 @@ structure PSpecClassExprAttr where 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 α) := +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, @@ -175,6 +176,54 @@ def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name% 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 @@ -200,7 +249,8 @@ initialize pspecAttr : PSpecAttr ← do /- The persistent map from type classes to pspec theorems -/ initialize pspecClassAttr : PSpecClassAttr ← do - let ext : MapDeclarationExtension (NameMap Name) ← mkMapDeclarationExtension `pspecClassMap + let ext : MapDeclarationExtension (NameMap Name) ← + mkMapMapDeclarationExtension Name.quickCmp `pspecClassMap let attrImpl : AttributeImpl := { name := `cpspec descr := "Marks theorems to use for type classes with the `progress` tactic" @@ -231,7 +281,8 @@ initialize pspecClassAttr : PSpecClassAttr ← do /- The 2nd persistent map from type classes to pspec theorems -/ initialize pspecClassExprAttr : PSpecClassExprAttr ← do - let ext : MapDeclarationExtension (HashMap Expr Name) ← mkMapDeclarationExtension `pspecClassExprMap + let ext : MapDeclarationExtension (HashMap Expr Name) ← + mkMapHashMapDeclarationExtension `pspecClassExprMap let attrImpl : AttributeImpl := { name := `cepspec descr := "Marks theorems to use for type classes with the `progress` tactic" |