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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Pp
open Util
(*s Identifiers *)
type identifier = string
let id_ord = Pervasives.compare
let string_of_id id = String.copy id
let id_of_string s = String.copy s
(* Hash-consing of identifier *)
module Hident = Hashcons.Make(
struct
type t = string
type u = string -> string
let hash_sub hstr id = hstr id
let equal id1 id2 = id1 == id2
let hash = Hashtbl.hash
end)
module IdOrdered =
struct
type t = identifier
let compare = id_ord
end
module Idset = Set.Make(IdOrdered)
module Idmap = Map.Make(IdOrdered)
module Idpred = Predicate.Make(IdOrdered)
(* Names *)
type name = Name of identifier | Anonymous
(* Dirpaths are lists of module identifiers. The actual representation
is reversed to optimise sharing: Coq.A.B is ["B";"A";"Coq"] *)
type module_ident = identifier
type dir_path = module_ident list
module ModIdOrdered =
struct
type t = identifier
let compare = Pervasives.compare
end
module ModIdmap = Map.Make(ModIdOrdered)
let make_dirpath x = x
let repr_dirpath x = x
let string_of_dirpath = function
| [] -> "<empty>"
| sl ->
String.concat "." (List.map string_of_id (List.rev sl))
(*s Section paths are absolute names *)
type section_path = {
dirpath : dir_path ;
basename : identifier }
let make_path pa id = { dirpath = pa; basename = id }
let repr_path { dirpath = pa; basename = id } = (pa,id)
(* parsing and printing of section paths *)
let string_of_path sp =
let (sl,id) = repr_path sp in
if sl = [] then string_of_id id
else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
let sp_ord sp1 sp2 =
let (p1,id1) = repr_path sp1
and (p2,id2) = repr_path sp2 in
let p_bit = compare p1 p2 in
if p_bit = 0 then id_ord id1 id2 else p_bit
module SpOrdered =
struct
type t = section_path
let compare = sp_ord
end
module Spset = Set.Make(SpOrdered)
module Sppred = Predicate.Make(SpOrdered)
module Spmap = Map.Make(SpOrdered)
(*s********************************************************************)
(* type of global reference *)
type variable = identifier
type constant = section_path
type inductive = section_path * int
type constructor = inductive * int
type mutual_inductive = section_path
let ith_mutual_inductive (sp,_) i = (sp,i)
let ith_constructor_of_inductive ind_sp i = (ind_sp,i)
let inductive_of_constructor (ind_sp,i) = ind_sp
let index_of_constructor (ind_sp,i) = i
(* Hash-consing of name objects *)
module Hname = Hashcons.Make(
struct
type t = name
type u = identifier -> identifier
let hash_sub hident = function
| Name id -> Name (hident id)
| n -> n
let equal n1 n2 =
match (n1,n2) with
| (Name id1, Name id2) -> id1 == id2
| (Anonymous,Anonymous) -> true
| _ -> false
let hash = Hashtbl.hash
end)
module Hdir = Hashcons.Make(
struct
type t = dir_path
type u = identifier -> identifier
let hash_sub hident d = List.map hident d
let equal d1 d2 = List.for_all2 (==) d1 d2
let hash = Hashtbl.hash
end)
module Hsp = Hashcons.Make(
struct
type t = section_path
type u = identifier -> identifier
let hash_sub hident sp =
{ dirpath = List.map hident sp.dirpath;
basename = hident sp.basename }
let equal sp1 sp2 =
(List.length sp1.dirpath = List.length sp2.dirpath) &&
(List.for_all2 (==) sp1.dirpath sp2.dirpath)
let hash = Hashtbl.hash
end)
let hcons_names () =
let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
let hident = Hashcons.simple_hcons Hident.f hstring in
let hname = Hashcons.simple_hcons Hname.f hident in
let hdir = Hashcons.simple_hcons Hdir.f hident in
let hspcci = Hashcons.simple_hcons Hsp.f hident in
(hspcci,hdir,hname,hident,hstring)
|
