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
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
|
(***********************************************************************)
(* 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 *)
(* Utilities *)
let code_of_0 = Char.code '0'
let code_of_9 = Char.code '9'
(* Identifiers *)
type identifier = string
let cut_ident 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
numpart slen slen
let repr_ident s =
let slen = String.length s in
let numstart = cut_ident s in
if numstart = slen then
(s, None)
else
(String.sub s 0 numstart,
Some (int_of_string (String.sub s numstart (slen - numstart))))
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 sa ^ (string_of_int n)
else sa ^ "_" ^ (string_of_int n)
| None -> String.copy sa
let first_char id =
assert (id <> "");
String.make 1 id.[0]
let id_ord = Pervasives.compare
(* Rem: semantics is a bit different, if an ident starts with toto00 then
after successive renamings it comes to toto09, then it goes on with toto10 *)
let lift_subscript id =
let len = String.length id in
let rec add carrypos =
let c = id.[carrypos] in
if is_digit c then
if c = '9' then begin
assert (carrypos>0);
add (carrypos-1)
end
else begin
let newid = String.copy id in
String.fill newid (carrypos+1) (len-1-carrypos) '0';
newid.[carrypos] <- Char.chr (Char.code c + 1);
newid
end
else begin
let newid = id^"0" in
if carrypos < len-1 then begin
String.fill newid (carrypos+1) (len-1-carrypos) '0';
newid.[carrypos+1] <- '1'
end;
newid
end
in add (len-1)
let has_subscript id = is_digit (id.[String.length id - 1])
let forget_subscript id =
let len = String.length id in
let numstart = cut_ident id in
let newid = String.make (numstart+1) '0' in
String.blit id 0 newid 0 numstart;
newid
(* This checks that a string is acceptable as an ident, i.e. starts
with a letter and contains only letters, digits or "'" *)
let check_ident_suffix i l s =
for i=1 to l-1 do
let c = String.get s i in
if not (is_letter c or is_digit c or c = '\'' or c = '_' or c = '@') then
error
("Character "^(String.sub s i 1)^" is not allowed in identifier "^s)
done
let check_ident s =
let l = String.length s in
if l = 0 then error "The empty string is not an identifier";
let c = String.get s 0 in
if (is_letter c) or c = '_' or c = '$' or c = '?'
then check_ident_suffix 1 l s
else error (s^": an identifier should start with a letter")
let is_ident s = try check_ident s; true with _ -> false
let check_suffix s = check_ident_suffix 0 (String.length s) s
let add_suffix id s = check_suffix s; id^s
let add_prefix s id = check_ident s; s^id
let string_of_id id = String.copy id
let id_of_string s = check_ident 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)
let atompart_of_id id = fst (repr_ident id)
let index_of_id id = snd (repr_ident id)
let pr_id id = [< 'sTR (string_of_id id) >]
let wildcard = id_of_string "_"
(* Fresh names *)
let lift_ident = lift_subscript
let next_ident_away id avoid =
if List.mem id avoid then
let id0 = if not (has_subscript id) then id else
(* Ce serait sans doute mieux avec quelque chose inspiré de
*** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
forget_subscript id 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
(* Names *)
type name = Name of identifier | Anonymous
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 "_"
let out_name = function
| Name id -> id
| Anonymous -> anomaly "out_name: expects a defined name"
(* 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 Directory paths = section names paths *)
let parse_fields s =
let len = String.length s in
let rec decoupe_dirs n =
try
let pos = String.index_from s n '.' in
let dir = String.sub s n (pos-n) in
let dirs,n' = decoupe_dirs (succ pos) in
(id_of_string dir)::dirs,n'
with
| Not_found -> [],n
in
if len = 0 then invalid_arg "parse_section_path";
let dirs,n = decoupe_dirs 0 in
let id = String.sub s n (len-n) in
dirs, (id_of_string id)
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)
(* These are the only functions which depend on how a dirpath is encoded *)
let make_dirpath x = List.rev x
let repr_dirpath x = List.rev x
let rev_repr_dirpath x = x
let dirpath_prefix = function
| [] -> anomaly "dirpath_prefix: empty dirpath"
| _::l -> l
let split_dirpath = function
| [] -> failwith "Empty"
| d::b -> (b,d)
let extend_dirpath d id = id::d
let add_dirpath_prefix id d = d@[id]
let is_dirpath_prefix_of d1 d2 = list_prefix_of (List.rev d1) (List.rev d2)
(**)
let is_empty_dirpath d = (d = [])
let dirpath_of_string s =
try
let sl,s = parse_fields s in
make_dirpath (sl @ [s])
with
| Invalid_argument _ -> invalid_arg "dirpath_of_string"
let string_of_dirpath = function
| [] -> "<empty>"
| sl -> String.concat "." (List.map string_of_id (repr_dirpath sl))
let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
let default_module_name = id_of_string "Top"
let default_module = make_dirpath [default_module_name]
(*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
(* parsing and printing of section paths *)
let string_of_path sp =
let (sl,id,k) = repr_path sp in
if sl = [] then string_of_id id
else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
let path_of_string s =
try
let sl,s = parse_fields s in
make_path (make_dirpath sl) s CCI
with
| Invalid_argument _ -> invalid_arg "path_of_string"
let pr_sp sp = [< 'sTR (string_of_path sp) >]
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
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 = section_path
type constant = section_path
type inductive = section_path * int
type constructor = inductive * int
type mutual_inductive = section_path
type global_reference =
| VarRef of section_path
| ConstRef of constant
| IndRef of inductive
| ConstructRef of constructor
(* 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;
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 hdir = Hashcons.simple_hcons Hdir.f hident in
let hspcci = Hashcons.simple_hcons Hsp.f hident in
(hspcci,hdir,hname,hident,hstring)
|