← Back to branch summary

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

« back to all changes in this revision

Viewing changes to interp/dumpglob.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:
interp/dumpglob.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: dumpglob.ml 11582 2008-11-12 19:49:57Z notin $ *)
 
10
 
 
11
 
 
12
(* Dump of globalization (to be used by coqdoc) *)
 
13
 
 
14
let glob_file = ref Pervasives.stdout
 
15
 
 
16
let open_glob_file f =
 
17
  glob_file := Pervasives.open_out f
 
18
  
 
19
let close_glob_file () =
 
20
  Pervasives.close_out !glob_file
 
21
 
 
22
type glob_output_t = 
 
23
    | NoGlob
 
24
    | StdOut
 
25
    | MultFiles
 
26
    | File of string
 
27
 
 
28
let glob_output = ref NoGlob
 
29
 
 
30
let dump () = !glob_output != NoGlob
 
31
 
 
32
let noglob () = glob_output := NoGlob
 
33
 
 
34
let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
 
35
 
 
36
let multi_dump () = !glob_output = MultFiles
 
37
 
 
38
let dump_to_dotglob f = glob_output := MultFiles
 
39
 
 
40
let dump_into_file f = glob_output := File f; open_glob_file f
 
41
 
 
42
let dump_string s = 
 
43
  if dump () then Pervasives.output_string !glob_file s
 
44
 
 
45
 
 
46
let previous_state = ref MultFiles
 
47
let pause () = previous_state := !glob_output; glob_output := NoGlob
 
48
let continue () = glob_output := !previous_state
 
49
 
 
50
 
 
51
let token_number = ref 0
 
52
let last_pos = ref 0
 
53
 
 
54
type coqdoc_state = Lexer.location_table * int * int
 
55
 
 
56
let coqdoc_freeze () =
 
57
  let lt = Lexer.location_table() in
 
58
  let state = (lt,!token_number,!last_pos) in
 
59
    token_number := 0;
 
60
    last_pos := 0;
 
61
    state
 
62
 
 
63
let coqdoc_unfreeze (lt,tn,lp) =
 
64
  Lexer.restore_location_table lt;
 
65
  token_number := tn;
 
66
  last_pos := lp
 
67
 
 
68
open Decl_kinds
 
69
 
 
70
let type_of_logical_kind = function
 
71
  | IsDefinition def -> 
 
72
      (match def with
 
73
      | Definition -> "def"
 
74
      | Coercion -> "coe"
 
75
      | SubClass -> "subclass"
 
76
      | CanonicalStructure -> "canonstruc"
 
77
      | Example -> "ex"
 
78
      | Fixpoint -> "def"
 
79
      | CoFixpoint -> "def"
 
80
      | Scheme -> "scheme"
 
81
      | StructureComponent -> "proj"
 
82
      | IdentityCoercion -> "coe"
 
83
      | Instance -> "inst"
 
84
      | Method -> "meth")
 
85
  | IsAssumption a ->
 
86
      (match a with
 
87
      | Definitional -> "defax"
 
88
      | Logical -> "prfax"
 
89
      | Conjectural -> "prfax")
 
90
  | IsProof th ->
 
91
      (match th with
 
92
      | Theorem
 
93
      | Lemma
 
94
      | Fact
 
95
      | Remark
 
96
      | Property
 
97
      | Proposition
 
98
      | Corollary -> "thm")
 
99
 
 
100
let type_of_global_ref gr =
 
101
  if Typeclasses.is_class gr then
 
102
    "class"
 
103
  else
 
104
    match gr with
 
105
    | Libnames.ConstRef cst -> 
 
106
        type_of_logical_kind (Decls.constant_kind cst)
 
107
    | Libnames.VarRef v ->
 
108
        "var" ^ type_of_logical_kind (Decls.variable_kind v)
 
109
    | Libnames.IndRef ind ->
 
110
        let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
 
111
          if mib.Declarations.mind_record then
 
112
            if mib.Declarations.mind_finite then "rec"
 
113
            else "corec"
 
114
          else if mib.Declarations.mind_finite then "ind"
 
115
          else "coind"
 
116
    | Libnames.ConstructRef _ -> "constr"
 
117
 
 
118
let remove_sections dir =
 
119
  if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
 
120
    (* Not yet (fully) discharged *)
 
121
    Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
 
122
  else
 
123
    (* Theorem/Lemma outside its outer section of definition *)
 
124
    dir
 
125
 
 
126
let dump_ref loc filepath modpath ident ty =
 
127
  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
 
128
                  (fst (Util.unloc loc)) filepath modpath ident ty)
 
129
 
 
130
let add_glob_gen loc sp lib_dp ty =
 
131
  if dump () then
 
132
    let mod_dp,id = Libnames.repr_path sp in
 
133
    let mod_dp = remove_sections mod_dp in
 
134
    let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
 
135
    let filepath = Names.string_of_dirpath lib_dp in
 
136
    let modpath = Names.string_of_dirpath mod_dp_trunc in
 
137
    let ident = Names.string_of_id id in
 
138
      dump_ref loc filepath modpath ident ty
 
139
 
 
140
let add_glob loc ref = 
 
141
  if dump () && loc <> Util.dummy_loc then
 
142
    let sp = Nametab.sp_of_global ref in
 
143
    let lib_dp = Lib.library_part ref in
 
144
    let ty = type_of_global_ref ref in
 
145
      add_glob_gen loc sp lib_dp ty
 
146
      
 
147
let mp_of_kn kn = 
 
148
  let mp,sec,l = Names.repr_kn kn in 
 
149
    Names.MPdot (mp,l) 
 
150
 
 
151
let add_glob_kn loc kn =
 
152
  if dump () && loc <> Util.dummy_loc then
 
153
    let sp = Nametab.sp_of_syntactic_definition kn in
 
154
    let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
 
155
      add_glob_gen loc sp lib_dp "syndef"
 
156
 
 
157
let add_local loc id = ()
 
158
(*   let mod_dp,id = repr_path sp in *)
 
159
(*   let mod_dp = remove_sections mod_dp in *)
 
160
(*   let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
 
161
(*   let filepath = string_of_dirpath lib_dp in *)
 
162
(*   let modpath = string_of_dirpath mod_dp_trunc in *)
 
163
(*   let ident = string_of_id id in *)
 
164
(*     dump_string (Printf.sprintf "R%d %s %s %s %s\n"  *)
 
165
(*                  (fst (unloc loc)) filepath modpath ident ty) *)
 
166
 
 
167
let dump_binding loc id = ()
 
168
      
 
169
let dump_definition (loc, id) sec s =
 
170
  dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc)) 
 
171
                        (Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
 
172
    
 
173
let dump_reference loc modpath ident ty =
 
174
  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
 
175
                  (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
 
176
 
 
177
let dump_constraint ((loc, n), _, _) sec ty =
 
178
  match n with
 
179
    | Names.Name id -> dump_definition (loc, id) sec ty
 
180
    | Names.Anonymous -> ()
 
181
 
 
182
let dump_name (loc, n) sec ty =
 
183
  match n with
 
184
    | Names.Name id -> dump_definition (loc, id) sec ty
 
185
    | Names.Anonymous -> ()
 
186
 
 
187
let dump_local_binder b sec ty =
 
188
  if dump () then
 
189
    match b with
 
190
      | Topconstr.LocalRawAssum (nl, _, _) -> 
 
191
          List.iter (fun x -> dump_name x sec ty) nl
 
192
      | Topconstr.LocalRawDef _ -> ()
 
193
 
 
194
let dump_modref loc mp ty =
 
195
  if dump () then
 
196
    let (dp, l) = Lib.split_modpath mp in
 
197
    let l = if l = [] then l else Util.list_drop_last l in
 
198
    let fp = Names.string_of_dirpath dp in
 
199
    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
 
200
      dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
 
201
                      (fst (Util.unloc loc)) fp mp "<>" ty)
 
202
 
 
203
let dump_moddef loc mp ty =
 
204
  if dump () then
 
205
    let (dp, l) = Lib.split_modpath mp in
 
206
    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
 
207
      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
 
208
 
 
209
let dump_libref loc dp ty =
 
210
  dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
 
211
                  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
212
 
 
213
let dump_notation_location pos ((path,df),sc) =
 
214
  if dump () then
 
215
    let rec next growing =
 
216
      let loc = Lexer.location_function !token_number in
 
217
      let (bp,_) = Util.unloc loc in
 
218
        if growing then if bp >= pos then loc else (incr token_number; next true)
 
219
        else if bp = pos then loc
 
220
        else if bp > pos then (decr token_number;next false)
 
221
        else (incr token_number;next true) in
 
222
    let loc = next (pos >= !last_pos) in
 
223
      last_pos := pos;
 
224
      let path = Names.string_of_dirpath path in
 
225
      let _sc = match sc with Some sc -> " "^sc | _ -> "" in
 
226
        dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
 
227
 
 
228