← Back to branch summary

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

« back to all changes in this revision

Viewing changes to library/nametab.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:
library/nametab.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: nametab.ml 10664 2008-03-14 11:27:37Z soubiran $ *)
 
10
 
 
11
open Util
 
12
open Pp
 
13
open Names
 
14
open Libnames
 
15
open Nameops
 
16
open Declarations
 
17
 
 
18
 
 
19
exception GlobalizationError of qualid
 
20
exception GlobalizationConstantError of qualid
 
21
 
 
22
let error_global_not_found_loc loc q =
 
23
  Stdpp.raise_with_loc loc (GlobalizationError q)
 
24
 
 
25
let error_global_constant_not_found_loc loc q =
 
26
  Stdpp.raise_with_loc loc (GlobalizationConstantError q)
 
27
 
 
28
let error_global_not_found q = raise (GlobalizationError q)
 
29
 
 
30
 
 
31
 
 
32
(* The visibility can be registered either 
 
33
   - for all suffixes not shorter then a given int - when the object
 
34
     is loaded inside a module
 
35
   or
 
36
   - for a precise suffix, when the module containing (the module
 
37
     containing ...) the object is open (imported) 
 
38
*)
 
39
type visibility = Until of int | Exactly of int
 
40
 
 
41
 
 
42
(* Data structure for nametabs *******************************************)
 
43
 
 
44
 
 
45
(* This module type will be instantiated by [section_path] of [dir_path] *)
 
46
(* The [repr] function is assumed to return the reversed list of idents. *)
 
47
module type UserName = sig 
 
48
  type t
 
49
  val to_string : t -> string
 
50
  val repr : t -> identifier * module_ident list
 
51
end
 
52
 
 
53
 
 
54
(* A ['a t] is a map from [user_name] to ['a], with possible lookup by
 
55
   partially qualified names of type [qualid]. The mapping of
 
56
   partially qualified names to ['a] is determined by the [visibility]
 
57
   parameter of [push].
 
58
   
 
59
   The [shortest_qualid] function given a user_name Coq.A.B.x, tries
 
60
   to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes
 
61
   the same object. 
 
62
*)
 
63
module type NAMETREE = sig
 
64
  type 'a t
 
65
  type user_name
 
66
  
 
67
  val empty : 'a t
 
68
  val push : visibility -> user_name -> 'a -> 'a t -> 'a t
 
69
  val locate : qualid -> 'a t -> 'a
 
70
  val find : user_name -> 'a t -> 'a
 
71
  val exists : user_name -> 'a t -> bool
 
72
  val user_name : qualid -> 'a t -> user_name
 
73
  val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid
 
74
  val find_prefixes : qualid -> 'a t -> 'a list
 
75
end
 
76
 
 
77
module Make(U:UserName) : NAMETREE with type user_name = U.t 
 
78
                                     = 
 
79
struct
 
80
 
 
81
  type user_name = U.t
 
82
 
 
83
  type 'a path_status = 
 
84
      Nothing 
 
85
    | Relative of user_name * 'a 
 
86
    | Absolute of user_name * 'a
 
87
 
 
88
  (* Dictionaries of short names *)
 
89
  type 'a nametree = ('a path_status * 'a nametree ModIdmap.t)
 
90
 
 
91
  type 'a t = 'a nametree Idmap.t
 
92
 
 
93
  let empty = Idmap.empty
 
94
                
 
95
  (* [push_until] is used to register [Until vis] visibility and 
 
96
     [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
 
97
 
 
98
  let rec push_until uname o level (current,dirmap) = function
 
99
    | modid :: path ->
 
100
        let mc = 
 
101
          try ModIdmap.find modid dirmap
 
102
          with Not_found -> (Nothing, ModIdmap.empty)
 
103
        in
 
104
        let this =
 
105
          if level <= 0 then
 
106
            match current with
 
107
              | Absolute (n,_) -> 
 
108
                  (* This is an absolute name, we must keep it 
 
109
                     otherwise it may become unaccessible forever *)
 
110
                  Flags.if_verbose
 
111
                    warning ("Trying to mask the absolute name \"" 
 
112
                             ^ U.to_string n ^ "\"!"); 
 
113
                  current
 
114
              | Nothing
 
115
              | Relative _ -> Relative (uname,o)
 
116
          else current 
 
117
        in
 
118
        let ptab' = push_until uname o (level-1) mc path in
 
119
          (this, ModIdmap.add modid ptab' dirmap)
 
120
    | [] -> 
 
121
        match current with
 
122
          | Absolute (uname',o') -> 
 
123
              if o'=o then begin
 
124
                assert (uname=uname');
 
125
                current, dirmap 
 
126
                  (* we are putting the same thing for the second time :) *)
 
127
              end
 
128
              else
 
129
                (* This is an absolute name, we must keep it otherwise it may
 
130
                   become unaccessible forever *)
 
131
                (* But ours is also absolute! This is an error! *)
 
132
                error ("Cannot mask the absolute name \""
 
133
                       ^ U.to_string uname' ^ "\"!")
 
134
          | Nothing
 
135
          | Relative _ -> Absolute (uname,o), dirmap
 
136
 
 
137
 
 
138
let rec push_exactly uname o level (current,dirmap) = function
 
139
  | modid :: path ->
 
140
      let mc = 
 
141
        try ModIdmap.find modid dirmap
 
142
        with Not_found -> (Nothing, ModIdmap.empty)
 
143
      in
 
144
        if level = 0 then
 
145
          let this =
 
146
            match current with
 
147
              | Absolute (n,_) -> 
 
148
                  (* This is an absolute name, we must keep it 
 
149
                     otherwise it may become unaccessible forever *)
 
150
                  Flags.if_verbose
 
151
                    warning ("Trying to mask the absolute name \""
 
152
                             ^ U.to_string n ^ "\"!");
 
153
                  current
 
154
              | Nothing
 
155
              | Relative _ -> Relative (uname,o)
 
156
          in
 
157
            (this, dirmap)
 
158
        else (* not right level *)
 
159
          let ptab' = push_exactly uname o (level-1) mc path in
 
160
            (current, ModIdmap.add modid ptab' dirmap)
 
161
  | [] -> 
 
162
      anomaly "Prefix longer than path! Impossible!"
 
163
 
 
164
 
 
165
let push visibility uname o tab =
 
166
  let id,dir = U.repr uname in
 
167
  let ptab =
 
168
    try Idmap.find id tab
 
169
    with Not_found -> (Nothing, ModIdmap.empty) 
 
170
  in
 
171
  let ptab' = match visibility with
 
172
    | Until i -> push_until uname o (i-1) ptab dir
 
173
    | Exactly i -> push_exactly uname o (i-1) ptab dir
 
174
  in
 
175
    Idmap.add id ptab' tab
 
176
 
 
177
 
 
178
let rec search (current,modidtab) = function
 
179
  | modid :: path -> search (ModIdmap.find modid modidtab) path
 
180
  | [] -> current
 
181
      
 
182
let find_node qid tab =
 
183
  let (dir,id) = repr_qualid qid in
 
184
    search (Idmap.find id tab) (repr_dirpath dir)
 
185
 
 
186
let locate qid tab = 
 
187
  let o = match find_node qid tab with
 
188
    | Absolute (uname,o) | Relative (uname,o) -> o
 
189
    | Nothing -> raise Not_found                                            
 
190
  in
 
191
    o
 
192
 
 
193
let user_name qid tab =
 
194
  let uname = match find_node qid tab with
 
195
    | Absolute (uname,o) | Relative (uname,o) -> uname
 
196
    | Nothing -> raise Not_found                                            
 
197
  in
 
198
    uname
 
199
  
 
200
let find uname tab = 
 
201
  let id,l = U.repr uname in
 
202
    match search (Idmap.find id tab) l with
 
203
        Absolute (_,o) -> o
 
204
      | _ -> raise Not_found
 
205
 
 
206
let exists uname tab =
 
207
  try 
 
208
    let _ = find uname tab in
 
209
      true
 
210
  with
 
211
      Not_found -> false
 
212
 
 
213
let shortest_qualid ctx uname tab = 
 
214
  let id,dir = U.repr uname in
 
215
  let hidden = Idset.mem id ctx in
 
216
  let rec find_uname pos dir (path,tab) = match path with
 
217
    | Absolute (u,_) | Relative (u,_)
 
218
          when u=uname && not(pos=[] && hidden) -> List.rev pos
 
219
    | _ -> 
 
220
        match dir with 
 
221
            [] -> raise Not_found
 
222
          | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tab)
 
223
  in
 
224
  let ptab = Idmap.find id tab in
 
225
  let found_dir = find_uname [] dir ptab in
 
226
    make_qualid (make_dirpath found_dir) id
 
227
 
 
228
let push_node node l =
 
229
  match node with
 
230
  | Absolute (_,o) | Relative (_,o) when not (List.mem o l) -> o::l
 
231
  | _ -> l
 
232
 
 
233
let rec flatten_idmap tab l =
 
234
  ModIdmap.fold (fun _ (current,idtab) l ->
 
235
    flatten_idmap idtab (push_node current l)) tab l
 
236
 
 
237
let rec search_prefixes (current,modidtab) = function
 
238
  | modid :: path -> search_prefixes (ModIdmap.find modid modidtab) path
 
239
  | [] -> List.rev (flatten_idmap  modidtab (push_node current []))
 
240
      
 
241
let find_prefixes qid tab =
 
242
  try
 
243
    let (dir,id) = repr_qualid qid in
 
244
    search_prefixes (Idmap.find id tab) (repr_dirpath dir)
 
245
  with Not_found -> []
 
246
 
 
247
end
 
248
 
 
249
 
 
250
 
 
251
(* Global name tables *************************************************)
 
252
 
 
253
module SpTab = Make (struct 
 
254
                       type t = section_path
 
255
                       let to_string = string_of_path
 
256
                       let repr sp = 
 
257
                         let dir,id = repr_path sp in
 
258
                           id, (repr_dirpath dir)
 
259
                     end)
 
260
 
 
261
 
 
262
type ccitab = extended_global_reference SpTab.t
 
263
let the_ccitab = ref (SpTab.empty : ccitab)
 
264
 
 
265
type kntab = kernel_name SpTab.t
 
266
let the_tactictab = ref (SpTab.empty : kntab)
 
267
 
 
268
type mptab = module_path SpTab.t
 
269
let the_modtypetab = ref (SpTab.empty : mptab)
 
270
 
 
271
type objtab = unit SpTab.t
 
272
let the_objtab = ref (SpTab.empty : objtab)
 
273
 
 
274
 
 
275
module DirTab = Make(struct 
 
276
                       type t = dir_path
 
277
                       let to_string = string_of_dirpath
 
278
                       let repr dir = match repr_dirpath dir with
 
279
                         | [] -> anomaly "Empty dirpath"
 
280
                         | id::l -> (id,l)
 
281
                     end)
 
282
 
 
283
(* If we have a (closed) module M having a submodule N, than N does not
 
284
   have the entry in [the_dirtab]. *)
 
285
type dirtab = global_dir_reference DirTab.t
 
286
let the_dirtab = ref (DirTab.empty : dirtab)
 
287
 
 
288
 
 
289
(* Reversed name tables ***************************************************)
 
290
 
 
291
(* This table translates extended_global_references back to section paths *)
 
292
module Globrevtab = Map.Make(struct 
 
293
                               type t=extended_global_reference 
 
294
                               let compare = compare 
 
295
                             end)
 
296
 
 
297
type globrevtab = section_path Globrevtab.t
 
298
let the_globrevtab = ref (Globrevtab.empty : globrevtab)
 
299
 
 
300
 
 
301
type mprevtab = dir_path MPmap.t
 
302
let the_modrevtab = ref (MPmap.empty : mprevtab)
 
303
 
 
304
type mptrevtab = section_path MPmap.t
 
305
let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
 
306
 
 
307
type knrevtab = section_path KNmap.t
 
308
let the_tacticrevtab = ref (KNmap.empty : knrevtab)
 
309
 
 
310
 
 
311
(* Push functions *********************************************************)
 
312
 
 
313
(* This is for permanent constructions (never discharged -- but with
 
314
   possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
 
315
   Parameter but also Remark and Fact) *)
 
316
 
 
317
let push_xref visibility sp xref =
 
318
  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
 
319
  match visibility with
 
320
    | Until _ -> 
 
321
        if Globrevtab.mem xref !the_globrevtab then
 
322
          ()
 
323
        else
 
324
          the_globrevtab := Globrevtab.add xref sp !the_globrevtab
 
325
    | _ -> ()
 
326
 
 
327
let push_cci visibility sp ref =
 
328
  push_xref visibility sp (TrueGlobal ref)
 
329
 
 
330
(* This is for Syntactic Definitions *)
 
331
let push_syntactic_definition visibility sp kn =
 
332
  push_xref visibility sp (SyntacticDef kn)
 
333
 
 
334
let push = push_cci
 
335
 
 
336
let push_modtype vis sp kn = 
 
337
  the_modtypetab := SpTab.push vis sp kn !the_modtypetab;
 
338
  the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab
 
339
 
 
340
(* This is for tactic definition names *)
 
341
 
 
342
let push_tactic vis sp kn = 
 
343
  the_tactictab := SpTab.push vis sp kn !the_tactictab;
 
344
  the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab
 
345
 
 
346
 
 
347
(* This is for dischargeable non-cci objects (removed at the end of the
 
348
   section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
 
349
 
 
350
let push_object visibility sp =
 
351
  the_objtab := SpTab.push visibility sp () !the_objtab
 
352
 
 
353
(* This is to remember absolute Section/Module names and to avoid redundancy *)
 
354
let push_dir vis dir dir_ref = 
 
355
  the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
 
356
  match dir_ref with
 
357
      DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab
 
358
    | _ -> ()
 
359
 
 
360
 
 
361
(* Locate functions *******************************************************)
 
362
 
 
363
 
 
364
(* This should be used when syntactic definitions are allowed *)
 
365
let extended_locate qid = SpTab.locate qid !the_ccitab
 
366
 
 
367
(* This should be used when no syntactic definitions is expected *)
 
368
let locate qid = match extended_locate qid with
 
369
  | TrueGlobal ref -> ref
 
370
  | SyntacticDef _ -> raise Not_found
 
371
let full_name_cci qid = SpTab.user_name qid !the_ccitab
 
372
 
 
373
let locate_syntactic_definition qid = match extended_locate qid with
 
374
  | TrueGlobal _ -> raise Not_found
 
375
  | SyntacticDef kn -> kn
 
376
 
 
377
let locate_modtype qid = SpTab.locate qid !the_modtypetab
 
378
let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
 
379
 
 
380
let locate_obj qid = SpTab.user_name qid !the_objtab
 
381
 
 
382
type ltac_constant = kernel_name
 
383
let locate_tactic qid = SpTab.locate qid !the_tactictab
 
384
let full_name_tactic qid = SpTab.user_name qid !the_tactictab
 
385
 
 
386
let locate_dir qid = DirTab.locate qid !the_dirtab
 
387
 
 
388
let locate_module qid = 
 
389
  match locate_dir qid with
 
390
    | DirModule (_,(mp,_)) -> mp
 
391
    | _ -> raise Not_found
 
392
 
 
393
let full_name_module qid = 
 
394
  match locate_dir qid with
 
395
    | DirModule (dir,_) -> dir
 
396
    | _ -> raise Not_found
 
397
 
 
398
let locate_section qid =
 
399
  match locate_dir qid with
 
400
    | DirOpenSection (dir, _) 
 
401
    | DirClosedSection dir -> dir
 
402
    | _ -> raise Not_found
 
403
 
 
404
let locate_all qid = 
 
405
  List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l)
 
406
    (SpTab.find_prefixes qid !the_ccitab) []
 
407
 
 
408
let extended_locate_all qid = SpTab.find_prefixes qid !the_ccitab
 
409
 
 
410
(* Derived functions *)
 
411
 
 
412
let locate_constant qid =
 
413
  match extended_locate qid with
 
414
    | TrueGlobal (ConstRef kn) -> kn
 
415
    | _ -> raise Not_found
 
416
 
 
417
let locate_mind qid = 
 
418
  match extended_locate qid with
 
419
    | TrueGlobal (IndRef (kn,0)) -> kn
 
420
    | _ -> raise Not_found
 
421
 
 
422
 
 
423
let absolute_reference sp =
 
424
  match SpTab.find sp !the_ccitab with
 
425
    | TrueGlobal ref -> ref
 
426
    | _ -> raise Not_found
 
427
 
 
428
let locate_in_absolute_module dir id =
 
429
  absolute_reference (make_path dir id)
 
430
 
 
431
let global r =
 
432
  let (loc,qid) = qualid_of_reference r in
 
433
  try match extended_locate qid with
 
434
    | TrueGlobal ref -> ref
 
435
    | SyntacticDef _ -> 
 
436
        user_err_loc (loc,"global",
 
437
          str "Unexpected reference to a notation: " ++
 
438
          pr_qualid qid)
 
439
  with Not_found ->
 
440
    error_global_not_found_loc loc qid
 
441
 
 
442
(* Exists functions ********************************************************)
 
443
 
 
444
let exists_cci sp = SpTab.exists sp !the_ccitab
 
445
      
 
446
let exists_dir dir = DirTab.exists dir !the_dirtab
 
447
 
 
448
let exists_section = exists_dir
 
449
 
 
450
let exists_module = exists_dir
 
451
 
 
452
let exists_modtype sp = SpTab.exists sp !the_modtypetab
 
453
 
 
454
let exists_tactic sp = SpTab.exists sp !the_tactictab
 
455
 
 
456
(* Reverse locate functions ***********************************************)
 
457
 
 
458
let sp_of_global ref = 
 
459
  match ref with
 
460
    | VarRef id -> make_path empty_dirpath id
 
461
    | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
 
462
 
 
463
 
 
464
let id_of_global ref = 
 
465
  let (_,id) = repr_path (sp_of_global ref) in 
 
466
  id
 
467
 
 
468
let sp_of_syntactic_definition kn = 
 
469
  Globrevtab.find (SyntacticDef kn) !the_globrevtab
 
470
 
 
471
let dir_of_mp mp =
 
472
  MPmap.find mp !the_modrevtab
 
473
 
 
474
 
 
475
(* Shortest qualid functions **********************************************)
 
476
 
 
477
let shortest_qualid_of_global ctx ref = 
 
478
  match ref with
 
479
    | VarRef id -> make_qualid empty_dirpath id
 
480
    | _ ->
 
481
        let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
 
482
        SpTab.shortest_qualid ctx sp !the_ccitab
 
483
 
 
484
let shortest_qualid_of_syndef ctx kn = 
 
485
  let sp = sp_of_syntactic_definition kn in
 
486
    SpTab.shortest_qualid ctx sp !the_ccitab
 
487
 
 
488
let shortest_qualid_of_module mp = 
 
489
  let dir = MPmap.find mp !the_modrevtab in
 
490
    DirTab.shortest_qualid Idset.empty dir !the_dirtab
 
491
 
 
492
let shortest_qualid_of_modtype kn =
 
493
  let sp = MPmap.find kn !the_modtyperevtab in
 
494
    SpTab.shortest_qualid Idset.empty sp !the_modtypetab
 
495
 
 
496
let shortest_qualid_of_tactic kn =
 
497
  let sp = KNmap.find kn !the_tacticrevtab in
 
498
    SpTab.shortest_qualid Idset.empty sp !the_tactictab
 
499
 
 
500
let pr_global_env env ref =
 
501
  (* Il est important de laisser le let-in, car les streams s'�valuent
 
502
  paresseusement : il faut forcer l'�valuation pour capturer
 
503
  l'�ventuelle lev�e d'une exception (le cas �choit dans le debugger) *)
 
504
  let s = string_of_qualid (shortest_qualid_of_global env ref) in
 
505
  (str s)
 
506
 
 
507
let inductive_of_reference r =
 
508
  match global r with
 
509
  | IndRef ind -> ind
 
510
  | ref ->
 
511
      user_err_loc (loc_of_reference r,"global_inductive",
 
512
        pr_reference r ++ spc () ++ str "is not an inductive type")
 
513
 
 
514
 
 
515
(********************************************************************)
 
516
 
 
517
(********************************************************************)
 
518
(* Registration of tables as a global table and rollback            *)
 
519
 
 
520
type frozen = ccitab * dirtab * objtab * kntab * kntab
 
521
    * globrevtab * mprevtab * knrevtab * knrevtab
 
522
 
 
523
let init () = 
 
524
  the_ccitab := SpTab.empty; 
 
525
  the_dirtab := DirTab.empty;
 
526
  the_objtab := SpTab.empty;
 
527
  the_modtypetab := SpTab.empty;
 
528
  the_tactictab := SpTab.empty;
 
529
  the_globrevtab := Globrevtab.empty;
 
530
  the_modrevtab := MPmap.empty;
 
531
  the_modtyperevtab := MPmap.empty;
 
532
  the_tacticrevtab := KNmap.empty
 
533
 
 
534
 
 
535
 
 
536
let freeze () =
 
537
  !the_ccitab, 
 
538
  !the_dirtab,
 
539
  !the_objtab,
 
540
  !the_modtypetab,
 
541
  !the_tactictab,
 
542
  !the_globrevtab,
 
543
  !the_modrevtab,
 
544
  !the_modtyperevtab,
 
545
  !the_tacticrevtab
 
546
 
 
547
let unfreeze (ccit,dirt,objt,mtyt,tact,globr,modr,mtyr,tacr) =
 
548
  the_ccitab := ccit;
 
549
  the_dirtab := dirt;
 
550
  the_objtab := objt;
 
551
  the_modtypetab := mtyt;
 
552
  the_tactictab := tact;
 
553
  the_globrevtab := globr;
 
554
  the_modrevtab := modr;
 
555
  the_modtyperevtab := mtyr;
 
556
  the_tacticrevtab := tacr
 
557
 
 
558
let _ = 
 
559
  Summary.declare_summary "names"
 
560
    { Summary.freeze_function = freeze;
 
561
      Summary.unfreeze_function = unfreeze;
 
562
      Summary.init_function = init;
 
563
      Summary.survive_module = false;
 
564
      Summary.survive_section = false }