blob: 54d242ea3285f0042996f9ba39abe33bef16941d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
/- Utilities to have databases of theorems -/
import Lean
import Std.Lean.HashSet
import Base.Utils
import Base.Primitives.Base
namespace Lookup
open Lean Elab Term Meta
open Utils
-- 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)
}
end Lookup
|
