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
type namespace =
| Var
| Sort
| Term
| Attr
| Decl
| Module of string
type t = {
ns : namespace;
name : string;
}
let hash = Hashtbl.hash
let compare = Pervasives.compare
let equal = Pervasives.(=)
let pp b { name ; _ } =
Printf.bprintf b "%s" name
let print fmt { name ; _ } =
Format.fprintf fmt "%s" name
let sort = Sort
let term = Term
let attr = Attr
let decl = Decl
let mod_name s = Module s
let mk ns name = { ns; name; }
let full_name =function
| { name; ns = Module m; } ->
Printf.sprintf "%s.%s" m name
| { name; _ } ->
name
let rwrt_rule = mk Decl "rewrite_rule"
let tptp_role = mk Decl "tptp_role"