|
1
|
(* This file is part of the Kind 2 model checker.
|
|
2
|
|
|
3
|
Copyright (c) 2014 by the Board of Trustees of the University of Iowa
|
|
4
|
|
|
5
|
Licensed under the Apache License, Version 2.0 (the "License"); you
|
|
6
|
may not use this file except in compliance with the License. You
|
|
7
|
may obtain a copy of the License at
|
|
8
|
|
|
9
|
http://www.apache.org/licenses/LICENSE-2.0
|
|
10
|
|
|
11
|
Unless required by applicable law or agreed to in writing, software
|
|
12
|
distributed under the License is distributed on an "AS IS" BASIS,
|
|
13
|
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
|
|
14
|
implied. See the License for the specific language governing
|
|
15
|
permissions and limitations under the License.
|
|
16
|
|
|
17
|
*)
|
|
18
|
|
|
19
|
open KindLib
|
|
20
|
|
|
21
|
|
|
22
|
(* TODO:
|
|
23
|
|
|
24
|
- Hashccons identifiers and use for StateVar, UfSymbol etc.
|
|
25
|
|
|
26
|
- Hide implementation and provide smart constructors that fail if
|
|
27
|
identifier was previously defined
|
|
28
|
|
|
29
|
- Allow several namespaces to avoid spurious name clashes
|
|
30
|
|
|
31
|
- List reserved identifiers per namespace and fail if reserved
|
|
32
|
identifier is created
|
|
33
|
|
|
34
|
- Use tag of identifier as short name instead of full string when
|
|
35
|
passing to SMT solver etc.
|
|
36
|
|
|
37
|
*)
|
|
38
|
|
|
39
|
(* Namespace to avoid clashes between reserved and user identifiers *)
|
|
40
|
type namespace =
|
|
41
|
|
|
42
|
(* Reserved identifier *)
|
|
43
|
| ReservedIdentifier
|
|
44
|
|
|
45
|
(* Identifier in user input *)
|
|
46
|
| UserIdentifier
|
|
47
|
|
|
48
|
module Ident = struct
|
|
49
|
|
|
50
|
(* Identifier with namespace *)
|
|
51
|
(* type t = namespace * string *)
|
|
52
|
type t = string
|
|
53
|
|
|
54
|
(* Equality on identifiers *)
|
|
55
|
let equal = String.equal
|
|
56
|
|
|
57
|
(* Total order on identifiers *)
|
|
58
|
let compare = String.compare
|
|
59
|
|
|
60
|
end
|
|
61
|
|
|
62
|
include Ident
|
|
63
|
|
|
64
|
module IdentSet = Set.Make (Ident)
|
|
65
|
|
|
66
|
module IdentMap = Map.Make (Ident)
|
|
67
|
|
|
68
|
|
|
69
|
let pp_print_ident ppf i = Format.fprintf ppf "%s" i
|
|
70
|
|
|
71
|
(* Construct an identifier from a string
|
|
72
|
|
|
73
|
Simply return the string for now, later do some smarter things. *)
|
|
74
|
let of_string s = s
|
|
75
|
|
|
76
|
let to_string = string_of_t pp_print_ident
|
|
77
|
|
|
78
|
(*
|
|
79
|
Local Variables:
|
|
80
|
compile-command: "make -C .. -k"
|
|
81
|
indent-tabs-mode: nil
|
|
82
|
End:
|
|
83
|
*)
|