Source file `id.ml`

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

(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)

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

(* Namespaces *)
(* let var = Var *)
let sort = Sort
let term = Term
let attr = Attr
let decl = Decl
let mod_name s = Module s

(* Identifiers *)
let mk ns name = { ns; name; }

let full_name =function
  | { name; ns = Module m; } ->
    Printf.sprintf "%s.%s" m name
  | { name; _ } ->
    name

(* Standard attributes *)
let rwrt_rule = mk Decl "rewrite_rule"
let tptp_role = mk Decl "tptp_role"