← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to kernel/names.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
kernel/names.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: names.ml 11750 2009-01-05 20:47:34Z herbelin $ *)
 
10
 
 
11
open Pp
 
12
open Util
 
13
 
 
14
(*s Identifiers *)
 
15
 
 
16
type identifier = string
 
17
 
 
18
let id_ord = Pervasives.compare
 
19
 
 
20
let id_of_string s = check_ident_soft s; String.copy s
 
21
 
 
22
let string_of_id id = String.copy id
 
23
 
 
24
(* Hash-consing of identifier *)
 
25
module Hident = Hashcons.Make(
 
26
  struct 
 
27
    type t = string
 
28
    type u = string -> string
 
29
    let hash_sub hstr id = hstr id
 
30
    let equal id1 id2 = id1 == id2
 
31
    let hash = Hashtbl.hash
 
32
  end)
 
33
 
 
34
module IdOrdered = 
 
35
  struct
 
36
    type t = identifier
 
37
    let compare = id_ord
 
38
  end
 
39
 
 
40
module Idset = Set.Make(IdOrdered)
 
41
module Idmap = Map.Make(IdOrdered)
 
42
module Idpred = Predicate.Make(IdOrdered)
 
43
 
 
44
(* Names *)
 
45
 
 
46
type name = Name of identifier | Anonymous
 
47
 
 
48
(* Dirpaths are lists of module identifiers. The actual representation
 
49
   is reversed to optimise sharing: Coq.A.B is ["B";"A";"Coq"] *)
 
50
 
 
51
type module_ident = identifier
 
52
type dir_path = module_ident list
 
53
 
 
54
module ModIdOrdered = 
 
55
  struct
 
56
    type t = identifier
 
57
    let compare = Pervasives.compare
 
58
  end
 
59
 
 
60
module ModIdmap = Map.Make(ModIdOrdered)
 
61
 
 
62
let make_dirpath x = x
 
63
let repr_dirpath x = x
 
64
 
 
65
let empty_dirpath = []
 
66
 
 
67
let string_of_dirpath = function
 
68
  | [] -> "<>"
 
69
  | sl -> String.concat "." (List.map string_of_id (List.rev sl))
 
70
 
 
71
 
 
72
let u_number = ref 0 
 
73
type uniq_ident = int * string * dir_path
 
74
let make_uid dir s = incr u_number;(!u_number,String.copy s,dir)
 
75
 let debug_string_of_uid (i,s,p) =
 
76
 "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
 
77
let string_of_uid (i,s,p) = 
 
78
  string_of_dirpath p ^"."^s
 
79
 
 
80
module Umap = Map.Make(struct 
 
81
                         type t = uniq_ident 
 
82
                         let compare = Pervasives.compare
 
83
                       end)
 
84
 
 
85
type label = string
 
86
 
 
87
type mod_self_id = uniq_ident
 
88
let make_msid = make_uid
 
89
let repr_msid (n, id, dp) = (n, id, dp)
 
90
let debug_string_of_msid = debug_string_of_uid
 
91
let refresh_msid (_,s,dir) = make_uid dir s
 
92
let string_of_msid = string_of_uid
 
93
let id_of_msid (_,s,_) = s
 
94
let label_of_msid (_,s,_) = s
 
95
 
 
96
type mod_bound_id = uniq_ident
 
97
let make_mbid = make_uid
 
98
let repr_mbid (n, id, dp) = (n, id, dp)
 
99
let debug_string_of_mbid = debug_string_of_uid
 
100
let string_of_mbid = string_of_uid
 
101
let id_of_mbid (_,s,_) = s
 
102
let label_of_mbid (_,s,_) = s
 
103
 
 
104
 
 
105
let mk_label l = l
 
106
let string_of_label = string_of_id
 
107
 
 
108
let id_of_label l = l
 
109
let label_of_id id = id
 
110
 
 
111
module Labset = Idset
 
112
module Labmap = Idmap
 
113
 
 
114
type module_path =
 
115
  | MPfile of dir_path
 
116
  | MPbound of mod_bound_id
 
117
  | MPself of mod_self_id 
 
118
  | MPdot of module_path * label
 
119
 
 
120
 
 
121
let rec check_bound_mp = function
 
122
  | MPbound _ -> true
 
123
  | MPdot(mp,_) ->check_bound_mp mp
 
124
  | _ -> false
 
125
 
 
126
let rec string_of_mp = function
 
127
  | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")"
 
128
  | MPbound uid -> string_of_uid uid
 
129
  | MPself uid -> string_of_uid uid
 
130
  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
 
131
 
 
132
(* we compare labels first if both are MPdots *)
 
133
let rec mp_ord mp1 mp2 = match (mp1,mp2) with
 
134
    MPdot(mp1,l1), MPdot(mp2,l2) -> 
 
135
      let c = Pervasives.compare l1 l2 in
 
136
        if c<>0 then
 
137
          c
 
138
        else
 
139
          mp_ord mp1 mp2
 
140
  |  _,_ -> Pervasives.compare mp1 mp2
 
141
 
 
142
module MPord = struct
 
143
  type t = module_path
 
144
  let compare = mp_ord
 
145
end
 
146
 
 
147
module MPset = Set.Make(MPord)
 
148
module MPmap = Map.Make(MPord)
 
149
 
 
150
(* Kernel names *)
 
151
 
 
152
type kernel_name = module_path * dir_path * label
 
153
 
 
154
let make_kn mp dir l = (mp,dir,l)
 
155
let repr_kn kn = kn
 
156
 
 
157
let modpath kn = 
 
158
  let mp,_,_ = repr_kn kn in mp
 
159
 
 
160
let label kn = 
 
161
  let _,_,l = repr_kn kn in l
 
162
 
 
163
let string_of_kn (mp,dir,l) = 
 
164
  string_of_mp mp ^ "#" ^ string_of_dirpath dir ^ "#" ^ string_of_label l
 
165
 
 
166
let pr_kn kn = str (string_of_kn kn)
 
167
 
 
168
 
 
169
let kn_ord kn1 kn2 = 
 
170
    let mp1,dir1,l1 = kn1 in
 
171
    let mp2,dir2,l2 = kn2 in
 
172
    let c = Pervasives.compare l1 l2 in
 
173
      if c <> 0 then
 
174
        c
 
175
      else 
 
176
        let c = Pervasives.compare dir1 dir2 in
 
177
          if c<>0 then
 
178
            c 
 
179
          else
 
180
            MPord.compare mp1 mp2
 
181
 
 
182
 
 
183
module KNord = struct
 
184
  type t = kernel_name
 
185
  let compare =kn_ord
 
186
end
 
187
 
 
188
module KNmap = Map.Make(KNord)
 
189
module KNpred = Predicate.Make(KNord)
 
190
module KNset = Set.Make(KNord)
 
191
module Cmap = KNmap
 
192
module Cpred = KNpred
 
193
module Cset = KNset
 
194
 
 
195
let default_module_name = "If you see this, it's a bug"
 
196
 
 
197
let initial_dir = make_dirpath [default_module_name]
 
198
 
 
199
let initial_msid = (make_msid initial_dir "If you see this, it's a bug")
 
200
let initial_path = MPself initial_msid
 
201
 
 
202
type variable = identifier
 
203
type constant = kernel_name
 
204
type mutual_inductive = kernel_name
 
205
type inductive = mutual_inductive * int
 
206
type constructor = inductive * int
 
207
 
 
208
let constant_of_kn kn = kn
 
209
let make_con mp dir l = (mp,dir,l)
 
210
let repr_con con = con
 
211
let string_of_con = string_of_kn
 
212
let con_label = label
 
213
let pr_con = pr_kn
 
214
let con_modpath = modpath
 
215
 
 
216
let mind_modpath = modpath
 
217
let ind_modpath ind = mind_modpath (fst ind)
 
218
let constr_modpath c = ind_modpath (fst c)
 
219
 
 
220
let ith_mutual_inductive (kn,_) i = (kn,i)
 
221
let ith_constructor_of_inductive ind i = (ind,i)
 
222
let inductive_of_constructor (ind,i) = ind
 
223
let index_of_constructor (ind,i) = i
 
224
 
 
225
module InductiveOrdered = struct
 
226
  type t = inductive
 
227
  let compare (spx,ix) (spy,iy) = 
 
228
    let c = ix - iy in if c = 0 then KNord.compare spx spy else c
 
229
end
 
230
 
 
231
module Indmap = Map.Make(InductiveOrdered)
 
232
 
 
233
module ConstructorOrdered = struct
 
234
  type t = constructor
 
235
  let compare (indx,ix) (indy,iy) = 
 
236
    let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c
 
237
end
 
238
 
 
239
module Constrmap = Map.Make(ConstructorOrdered)
 
240
 
 
241
(* Better to have it here that in closure, since used in grammar.cma *)
 
242
type evaluable_global_reference =
 
243
  | EvalVarRef of identifier
 
244
  | EvalConstRef of constant
 
245
 
 
246
(* Hash-consing of name objects *)
 
247
module Hname = Hashcons.Make(
 
248
  struct 
 
249
    type t = name
 
250
    type u = identifier -> identifier
 
251
    let hash_sub hident = function
 
252
      | Name id -> Name (hident id)
 
253
      | n -> n
 
254
    let equal n1 n2 =
 
255
      match (n1,n2) with
 
256
        | (Name id1, Name id2) -> id1 == id2
 
257
        | (Anonymous,Anonymous) -> true
 
258
        | _ -> false
 
259
    let hash = Hashtbl.hash
 
260
  end)
 
261
 
 
262
module Hdir = Hashcons.Make(
 
263
  struct 
 
264
    type t = dir_path
 
265
    type u = identifier -> identifier
 
266
    let hash_sub hident d = List.map hident d
 
267
    let rec equal d1 d2 = match (d1,d2) with
 
268
      | [],[] -> true
 
269
      | id1::d1,id2::d2 -> id1 == id2 & equal d1 d2
 
270
      | _ -> false
 
271
    let hash = Hashtbl.hash
 
272
  end)
 
273
 
 
274
module Huniqid = Hashcons.Make(
 
275
  struct 
 
276
    type t = uniq_ident
 
277
    type u = (string -> string) * (dir_path -> dir_path)
 
278
    let hash_sub (hstr,hdir) (n,s,dir) = (n,hstr s,hdir dir)
 
279
    let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 & s1 = s2 & dir1 == dir2
 
280
    let hash = Hashtbl.hash
 
281
  end)
 
282
 
 
283
module Hmod = Hashcons.Make(
 
284
  struct 
 
285
    type t = module_path
 
286
    type u = (dir_path -> dir_path) * (uniq_ident -> uniq_ident) *
 
287
        (string -> string)
 
288
    let rec hash_sub (hdir,huniqid,hstr as hfuns) = function
 
289
      | MPfile dir -> MPfile (hdir dir)
 
290
      | MPbound m -> MPbound (huniqid m)
 
291
      | MPself m -> MPself (huniqid m)
 
292
      | MPdot (md,l) -> MPdot (hash_sub hfuns md, hstr l)
 
293
    let rec equal d1 d2 = match (d1,d2) with
 
294
      | MPfile dir1, MPfile dir2 -> dir1 == dir2
 
295
      | MPbound m1, MPbound m2 -> m1 == m2
 
296
      | MPself m1, MPself m2 -> m1 == m2
 
297
      | MPdot (mod1,l1), MPdot (mod2,l2) -> equal mod1 mod2 & l1 = l2
 
298
      | _ -> false
 
299
    let hash = Hashtbl.hash
 
300
  end)
 
301
 
 
302
module Hkn = Hashcons.Make(
 
303
  struct 
 
304
    type t = kernel_name
 
305
    type u = (module_path -> module_path)
 
306
        * (dir_path -> dir_path) * (string -> string)
 
307
    let hash_sub (hmod,hdir,hstr) (md,dir,l) = (hmod md, hdir dir, hstr l)
 
308
    let equal (mod1,dir1,l1) (mod2,dir2,l2) =
 
309
      mod1 == mod2 && dir1 == dir2 && l1 == l2
 
310
    let hash = Hashtbl.hash
 
311
  end)
 
312
 
 
313
let hcons_names () =
 
314
  let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
 
315
  let hident = Hashcons.simple_hcons Hident.f hstring in
 
316
  let hname = Hashcons.simple_hcons Hname.f hident in
 
317
  let hdir = Hashcons.simple_hcons Hdir.f hident in
 
318
  let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in
 
319
  let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in
 
320
  let hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in
 
321
  (hkn,hkn,hdir,hname,hident,hstring)
 
322
 
 
323
 
 
324
(*******)
 
325
 
 
326
type transparent_state = Idpred.t * Cpred.t
 
327
 
 
328
let empty_transparent_state = (Idpred.empty, Cpred.empty)
 
329
let full_transparent_state = (Idpred.full, Cpred.full)
 
330
let var_full_transparent_state = (Idpred.full, Cpred.empty)
 
331
let cst_full_transparent_state = (Idpred.empty, Cpred.full)
 
332
 
 
333
type 'a tableKey =
 
334
  | ConstKey of constant
 
335
  | VarKey of identifier
 
336
  | RelKey of 'a 
 
337
 
 
338
 
 
339
type inv_rel_key = int (* index in the [rel_context] part of environment
 
340
                          starting by the end, {\em inverse} 
 
341
                          of de Bruijn indice *)
 
342
 
 
343
type id_key = inv_rel_key tableKey
 
344