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
type value =
| Integer
| Rational
| Real
| Binary
| Hexadecimal
| Bitvector
| String
type namespace =
| Var
| Sort
| Term
| Attr
| Decl
| Track
| Module of string
| Value of value
type t = {
ns : namespace;
name : string;
}
let hash = Hashtbl.hash
let compare = Stdlib.compare
let equal = Stdlib.(=)
let split { name; _ } =
Misc.split_on_char '\000' name
let to_string ({ name; _} as id) =
match split id with
| [s] -> s
| l ->
let b = Buffer.create (String.length name + List.length l + 3) in
Buffer.add_string b "(_";
List.iter (fun s -> Buffer.add_char b ' '; Buffer.add_string b s) l;
Buffer.add_char b ')';
Buffer.contents b
let pp b id =
Printf.bprintf b "%s" (to_string id)
let print fmt id =
Format.fprintf fmt "%s" (to_string id)
let full_name = function
| { ns = Module m; _ } as id ->
Printf.sprintf "%s.%s" m (to_string id)
| id ->
to_string id
let trackers = Hashtbl.create 13
let trackeds = Hashtbl.create 13
let var = Var
let sort = Sort
let term = Term
let attr = Attr
let decl = Decl
let track = Track
let mod_name s = Module s
let mk ns name = { ns; name; }
let tracked ~track ns name =
let id = mk ns name in
Hashtbl.add trackers track id;
Hashtbl.add trackeds id track;
id
let ac_symbol = mk Attr "ac"
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"