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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
|
(* $Id$ *)
open Pp
open Util
(* Identifiers *)
type identifier = {
atom : string ;
index : int }
type name = Name of identifier | Anonymous
let code_of_0 = Char.code '0'
let code_of_9 = Char.code '9'
let repr_ident { atom = sa; index = n } =
if n = -1 then (sa,None) else (sa,Some n)
let make_ident sa = function
| Some n ->
let c = Char.code (String.get sa (String.length sa -1)) in
if c < code_of_0 or c > code_of_9 then { atom = sa; index = n }
else { atom = sa^"_"; index = n }
| None -> { atom = sa; index = -1 }
let string_of_id id = match repr_ident id with
| (s,None) -> s
| (s,Some n) -> s ^ (string_of_int n)
let id_of_string s =
let slen = String.length s in
(* [n'] is the position of the first non nullary digit *)
let rec numpart n n' =
if n = 0 then
failwith
("The string " ^ s ^ " is not an identifier: it contains only digits")
else
let c = Char.code (String.get s (n-1)) in
if c = code_of_0 && n <> slen then
numpart (n-1) n'
else if code_of_0 <= c && c <= code_of_9 then
numpart (n-1) (n-1)
else
n'
in
let numstart = numpart slen slen in
if numstart = slen then
{ atom = s; index = -1 }
else
{ atom = String.sub s 0 numstart;
index = int_of_string (String.sub s numstart (slen - numstart)) }
let atompart_of_id id = id.atom
let index_of_id id = snd (repr_ident id)
let pr_id id =
match repr_ident id with
| ("",None) -> [< 'sTR"[]" >]
| ("",Some n) -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >]
| (s,None) -> [< 'sTR s >]
| (s,Some n) -> [< 'sTR s ; 'iNT n >]
let id_ord { atom = s1; index = n1 } { atom = s2; index = n2 } =
let s_bit = Pervasives.compare s1 s2 in
if s_bit = 0 then n1 - n2 else s_bit
let first_char id =
if id.atom = "" then
failwith "lowercase_first_char"
else
String.make 1 id.atom.[0]
module IdOrdered =
struct
type t = identifier
let compare = id_ord
end
module Idset = Set.Make(IdOrdered)
module Idmap = Map.Make(IdOrdered)
(* Fresh names *)
let lift_ident { atom = str; index = i } = { atom = str; index = i+1 }
let next_ident_away id avoid =
if List.mem id avoid then
let id0 = if id.index = -1 then id else
(* Ce serait sans doute mieux avec quelque chose inspiré de
*** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
{ id with index = 0 } in
let rec name_rec id =
if List.mem id avoid then name_rec (lift_ident id) else id in
name_rec id0
else id
let next_ident_away_from id avoid =
let rec name_rec id =
if List.mem id avoid then name_rec (lift_ident id) else id in
name_rec id
let next_name_away_with_default default name l =
match name with
| Name str -> next_ident_away str l
| Anonymous -> next_ident_away (id_of_string default) l
let next_name_away name l =
match name with
| Name str -> next_ident_away str l
| Anonymous -> id_of_string "_"
(* Kinds *)
type path_kind = CCI | FW | OBJ
let string_of_kind = function
| CCI -> "cci"
| FW -> "fw"
| OBJ -> "obj"
let kind_of_string = function
| "cci" -> CCI
| "fw" -> FW
| "obj" -> OBJ
| _ -> invalid_arg "kind_of_string"
(*s Section paths *)
type qualid = string list * string
let make_qualid p s = (p,s)
let repr_qualid q = q
let string_of_qualid (l,s) = String.concat "." (l@[s])
let pr_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
(*s Directory paths = section names paths *)
type dir_path = string list
(* The root of absolute names *)
let coq_root = ["Coq"]
(*s Section paths are absolute names *)
type section_path = {
dirpath : dir_path ;
basename : identifier ;
kind : path_kind }
let make_path pa id k = { dirpath = pa; basename = id; kind = k }
let repr_path { dirpath = pa; basename = id; kind = k} = (pa,id,k)
let kind_of_path sp = sp.kind
let basename sp = sp.basename
let dirpath sp = sp.dirpath
let qualid_of_sp sp =
make_qualid (coq_root @ dirpath sp) (string_of_id (basename sp))
(* parsing and printing of section paths *)
let string_of_dirpath sl = String.concat "." (coq_root@sl)
let string_of_path sp =
let (sl,id,k) = repr_path sp in
String.concat ""
(List.flatten (List.map (fun s -> [s;"."]) (coq_root@sl))
@ [ string_of_id id ])
let path_of_string s =
try
let (sl,s,k) = parse_section_path s in
make_path sl (id_of_string s) (kind_of_string k)
with
| Invalid_argument _ -> invalid_arg "path_of_string"
let pr_sp sp = [< 'sTR (string_of_path sp) >]
let sp_of_wd = function
| [] -> invalid_arg "Names.sp_of_wd"
| l -> let (bn,dp) = list_sep_last l in make_path dp (id_of_string bn) OBJ
let wd_of_sp sp =
let (sp,id,_) = repr_path sp in sp @ [string_of_id id]
let sp_ord sp1 sp2 =
let (p1,id1,k) = repr_path sp1
and (p2,id2,k') = repr_path sp2 in
let ck = compare k k' in
if ck = 0 then
let p_bit = compare p1 p2 in
if p_bit = 0 then id_ord id1 id2 else p_bit
else
ck
let dirpath_prefix_of = list_prefix_of
module SpOrdered =
struct
type t = section_path
let compare = sp_ord
end
module Spset = Set.Make(SpOrdered)
module Spmap = Map.Make(SpOrdered)
(* Special references for inductive objects *)
type constant_path = section_path
type inductive_path = section_path * int
type constructor_path = inductive_path * int
(* Hash-consing of name objects *)
module Hident = Hashcons.Make(
struct
type t = identifier
type u = string -> string
let hash_sub hstr id =
{ atom = hstr id.atom; index = id.index }
let equal id1 id2 = id1.atom == id2.atom && id1.index = id2.index
let hash = Hashtbl.hash
end)
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 Hsp = Hashcons.Make(
struct
type t = section_path
type u = (identifier -> identifier) * (string -> string)
let hash_sub (hident,hstr) sp =
{ dirpath = List.map hstr sp.dirpath;
basename = hident sp.basename;
kind = sp.kind }
let equal sp1 sp2 =
(sp1.basename == sp2.basename) && (sp1.kind = sp2.kind)
&& (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 hspcci = Hashcons.simple_hcons Hsp.f (hident,hstring) in
let hspfw = Hashcons.simple_hcons Hsp.f (hident,hstring) in
(hspcci,hspfw,hname,hident,hstring)
|