aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/index.ml
blob: 47acc7b4362fe7f24bc31a5cb142d0771c4f87c2 (plain)
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Printf
open Cdglobals

type loc = int

type entry_type =
  | Library
  | Module
  | Definition
  | Inductive
  | Constructor
  | Lemma
  | Record
  | Projection
  | Instance
  | Class
  | Method
  | Variable
  | Axiom
  | TacticDefinition
  | Abbreviation
  | Notation
  | Section

type index_entry =
  | Def of string * entry_type
  | Ref of coq_module * string * entry_type

let current_library = ref ""
  (** refers to the file being parsed *)

(** [deftable] stores only definitions and is used to build the index *)
let deftable = Hashtbl.create 97

(** [byidtable] is used to interpolate idents inside comments, which are not
    globalized otherwise. *)
let byidtable = Hashtbl.create 97

(** [reftable] stores references and definitions *)
let reftable = Hashtbl.create 97

let full_ident sp id =
  if sp <> "<>" then
    if id <> "<>" then
      sp ^ "." ^ id
    else sp
  else if id <> "<>"
  then id
  else ""

let add_def loc1 loc2 ty sp id =
  let fullid = full_ident sp id in
  let def = Def (fullid, ty) in
  for loc = loc1 to loc2 do
    Hashtbl.add reftable (!current_library, loc) def
  done;
  Hashtbl.add deftable !current_library (fullid, ty);
  Hashtbl.add byidtable id (!current_library, fullid, ty)

let add_ref m loc m' sp id ty =
  let fullid = full_ident sp id in
  if Hashtbl.mem reftable (m, loc) then ()
  else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty));
  let idx = if id = "<>" then m' else id in
    if Hashtbl.mem byidtable idx then ()
    else Hashtbl.add byidtable idx (m', fullid, ty)

let find m l = Hashtbl.find reftable (m, l)

let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)

(*s Manipulating path prefixes *)

type stack = string list

let rec string_of_stack st =
  match st with
    | [] -> ""
    | x::[] -> x
    | x::tl -> (string_of_stack tl) ^ "." ^ x

let empty_stack = []

let module_stack = ref empty_stack
let section_stack = ref empty_stack

let push st p = st := p::!st
let pop st =
  match !st with
    | [] -> ()
    | _::tl -> st := tl

let head st =
  match st with
    | [] -> ""
    | x::_ -> x

(* Coq modules *)

let split_sp s =
  try
    let i = String.rindex s '.' in
      String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
  with
      Not_found -> "", s

let modules = Hashtbl.create 97
let local_modules = Hashtbl.create 97

let add_module m =
  let _,id = split_sp m in
  Hashtbl.add modules id m;
  Hashtbl.add local_modules m ()

type module_kind = Local | External of string | Unknown

let external_libraries = ref []

let add_external_library logicalpath url =
  external_libraries := (logicalpath,url) :: !external_libraries

let find_external_library logicalpath =
  let rec aux = function
    | [] -> raise Not_found
    | (l,u)::rest ->
        if String.length logicalpath > String.length l &&
          String.sub logicalpath 0 (String.length l + 1) = l ^"."
        then u
        else aux rest
  in aux !external_libraries

let init_coqlib_library () = add_external_library "Coq" !coqlib

let find_module m =
  if Hashtbl.mem local_modules m then
    Local
  else
    try External (Filename.concat (find_external_library m) m)
    with Not_found -> Unknown


(* Building indexes *)

type 'a index = {
  idx_name : string;
  idx_entries : (char * (string * 'a) list) list;
  idx_size : int }

let map f i =
  { i with idx_entries =
      List.map
	(fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l))
	i.idx_entries }

let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2

let sort_entries el =
  let t = Hashtbl.create 97 in
  List.iter
    (fun c -> Hashtbl.add t c [])
    ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N';
     'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'; '*'];
  List.iter
    (fun ((s,_) as e) ->
      let c = Alpha.norm_char s.[0] in
      let c,l =
	try c,Hashtbl.find t c with Not_found -> '*',Hashtbl.find t '*' in
      Hashtbl.replace t c (e :: l))
    el;
  let res = ref [] in
  Hashtbl.iter (fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
  List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res

let display_letter c = if c = '*' then "other" else String.make 1 c

let type_name = function
  | Library ->
      let ln = !lib_name in
        if ln <> "" then String.lowercase ln else "library"
  | Module -> "module"
  | Definition -> "definition"
  | Inductive -> "inductive"
  | Constructor -> "constructor"
  | Lemma -> "lemma"
  | Record -> "record"
  | Projection -> "projection"
  | Instance -> "instance"
  | Class -> "class"
  | Method -> "method"
  | Variable -> "variable"
  | Axiom -> "axiom"
  | TacticDefinition -> "tactic"
  | Abbreviation -> "abbreviation"
  | Notation -> "notation"
  | Section -> "section"

let prepare_entry s = function
  | Notation ->
      (* We decode the encoding done in Dumpglob.cook_notation of coqtop *)
      (* Encoded notations have the form section:sc:x_'++'_x where:      *)
      (* - the section, if any, ends with a "."                          *)
      (* - the scope can be empty                                        *)
      (* - tokens are separated with "_"                                 *)
      (* - non-terminal symbols are conventionally represented by "x"    *)
      (* - terminals are enclosed within simple quotes                   *)
      (* - existing simple quotes (that necessarily are parts of         *)
      (*   terminals) are doubled                                        *)
      (*   (as a consequence, when a terminal contains "_" or "x", these *)
      (*   necessarily appear enclosed within non-doubled simple quotes) *)
      (* - non-printable characters < 32 are left encoded so that they   *)
      (*   are human-readable in index files                             *)
      (* Example: "x ' %x _% y %'x %'_' z" is encoded as                 *)
      (*   "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x"                        *)
      let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in
      let h = try String.index_from s 0 ':' with _ -> err () in
      let i = try String.index_from s (h+1) ':' with _ -> err () in
      let sc = String.sub s (h+1) (i-h-1) in
      let ntn = String.make (String.length s - i) ' ' in
      let k = ref 0 in
      let j = ref (i+1) in
      let quoted = ref false in
      let l = String.length s - 1 in
      while !j <= l do
	if not !quoted then begin
	  (match s.[!j] with
	  | '_' -> ntn.[!k] <- ' '; incr k
	  | 'x' -> ntn.[!k] <- '_'; incr k
	  | '\'' -> quoted := true
	  | _ -> assert false)
	end
	else
	  if s.[!j] = '\'' then
	    if (!j = l || s.[!j+1] = '_') then quoted := false
	    else (incr j; ntn.[!k] <- s.[!j]; incr k)
	  else begin
	    ntn.[!k] <- s.[!j];
	    incr k
	  end;
	incr j
      done;
      let ntn = String.sub ntn 0 !k in
      if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
  | _ ->
      s

let all_entries () =
  let gl = ref [] in
  let add_g s m t = gl := (s,(m,t)) :: !gl in
  let bt = Hashtbl.create 11 in
  let add_bt t s m =
    let l = try Hashtbl.find bt t with Not_found -> [] in
      Hashtbl.replace bt t ((s,m) :: l)
  in
  let classify m (s,t) = (add_g s m t; add_bt t s m) in
    Hashtbl.iter classify deftable;
    Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
    { idx_name = "global";
      idx_entries = sort_entries !gl;
      idx_size = List.length !gl },
    Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t;
			             idx_entries = sort_entries e;
			             idx_size = List.length e }) :: l) bt []

let type_of_string = function
  | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
  | "ex" | "scheme" -> Definition
  | "prf" | "thm" -> Lemma
  | "ind" | "variant" | "coind" -> Inductive
  | "constr" -> Constructor
  | "indrec" | "rec" | "corec" -> Record
  | "proj" -> Projection
  | "class" -> Class
  | "meth" -> Method
  | "inst" -> Instance
  | "var" -> Variable
  | "defax" | "prfax" | "ax" -> Axiom
  | "syndef" -> Abbreviation
  | "not" -> Notation
  | "lib" -> Library
  | "mod" | "modtype" -> Module
  | "tac" -> TacticDefinition
  | "sec" -> Section
  | s -> invalid_arg ("type_of_string:" ^ s)

let ill_formed_glob_file f =
  eprintf "Warning: ill-formed file %s (links will not be available)\n" f
let outdated_glob_file f =
  eprintf "Warning: %s not consistent with corresponding .v file (links will not be available)\n" f

let correct_file vfile f c =
  let s = input_line c in
  if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then
    (ill_formed_glob_file f; false)
  else
    let s = String.sub s 7 (String.length s - 7) in
    match vfile, s with
    | None, "NO" -> true
    | Some _, "NO" -> ill_formed_glob_file f; false
    | None, _ -> ill_formed_glob_file f; false
    | Some vfile, s ->
        s = Digest.to_hex (Digest.file vfile) || (outdated_glob_file f; false)

let read_glob vfile f =
  let c = open_in f in
  if correct_file vfile f c then
  let cur_mod = ref "" in
  try
    while true do
      let s = input_line c in
      let n = String.length s in
      if n > 0 then begin
	match s.[0] with
	  | 'F' ->
	      cur_mod := String.sub s 1 (n - 1);
	      current_library := !cur_mod
	  | 'R' ->
	      (try
		Scanf.sscanf s "R%d:%d %s %s %s %s"
		  (fun loc1 loc2 lib_dp sp id ty ->
		    for loc=loc1 to loc2 do
		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty);

                      (* Also add an entry for each module mentioned in [lib_dp],
                       * to use in interpolation. *)
                      ignore (List.fold_right (fun thisPiece priorPieces ->
                                                let newPieces = match priorPieces with
                                                                | "" -> thisPiece
                                                                | _ -> thisPiece ^ "." ^ priorPieces in
                                                add_ref !cur_mod loc "" "" newPieces Library;
                                                newPieces) (Str.split (Str.regexp_string ".") lib_dp) "")
		    done)
	       with _ -> ())
	  | _ ->
	      try Scanf.sscanf s "%s %d:%d %s %s"
		(fun ty loc1 loc2 sp id ->
                  add_def loc1 loc2 (type_of_string ty) sp id)
	      with Scanf.Scan_failure _ -> ()

      end
    done; assert false
  with End_of_file ->
    close_in c