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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
type namespace = Namespace.t
type t = {
name : Name.t;
ns : namespace;
}
let hash { ns; name; } =
Misc.hash2 (Namespace.hash ns) (Name.hash name)
let compare { ns; name; } { ns = ns'; name = name'; } =
let (<?>) = Misc.(<?>) in
Namespace.compare ns ns'
<?> (Name.compare, name, name')
let equal id id' =
id == id' || compare id id' = 0
let print fmt { name; ns = _; } =
Name.print fmt name
let var = Namespace.var
let sort = Namespace.sort
let term = Namespace.term
let attr = Namespace.attr
let decl = Namespace.decl
let track = Namespace.track
let ns { ns; _ } = ns
let name { name; _ } = name
let create ns name = { ns; name; }
let mk ns s =
let name = Name.simple s in
create ns name
let indexed ns basename indexes =
let name = Name.indexed basename indexes in
create ns name
let qualified ns path name =
let name = Name.qualified path name in
create ns name
let trackers = Hashtbl.create 13
let trackeds = Hashtbl.create 13
let tracked ~track ns path =
let id = mk ns path in
Hashtbl.add trackers track id;
Hashtbl.add trackeds id track;
id
let stmt = mk Attr "stmt"
let ac_symbol = mk Attr "ac"
let predicate_def = mk Attr "predicate"
let case_split = mk Decl "case_split"
let theory_decl = mk Decl "theory"
let rwrt_rule = mk Decl "rewrite_rule"
let tptp_role = mk Decl "tptp_role"
let tptp_kind = mk Decl "tptp_kind"
module Map = struct
type 'a t = 'a Name.Map.t Namespace.Map.t
let empty = Namespace.Map.empty
let find_exn k t =
Name.Map.find_exn k.name (Namespace.Map.find_exn k.ns t)
let find_opt k t =
match Namespace.Map.find_opt k.ns t with
| None -> None
| Some map -> Name.Map.find_opt k.name map
let add k v t =
Namespace.Map.find_add k.ns (function
| None -> Name.Map.add k.name v Name.Map.empty
| Some map -> Name.Map.add k.name v map
) t
let find_add k f t =
Namespace.Map.find_add k.ns (function
| None -> Name.Map.find_add k.name f Name.Map.empty
| Some map -> Name.Map.find_add k.name f map
) t
let iter f t =
Namespace.Map.iter (fun ns map ->
Name.Map.iter (fun name v ->
f { ns; name; } v
) map
) t
let fold f t acc =
Namespace.Map.fold (fun ns map acc ->
Name.Map.fold (fun name v acc ->
f { ns; name; } v acc
) map acc
) t acc
end