summaryrefslogtreecommitdiff
path: root/interp/dumpglob.ml
blob: 702c509dc73449a8f5484b5a25729a19d34709ad (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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)


(* Dump of globalization (to be used by coqdoc) *)

let glob_file = ref Pervasives.stdout

let open_glob_file f =
  glob_file := Pervasives.open_out f

let close_glob_file () =
  Pervasives.close_out !glob_file

type glob_output_t =
    | NoGlob
    | StdOut
    | MultFiles
    | File of string

let glob_output = ref NoGlob

let dump () = !glob_output != NoGlob

let noglob () = glob_output := NoGlob

let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout

let multi_dump () = !glob_output = MultFiles

let dump_to_dotglob f = glob_output := MultFiles

let dump_into_file f = glob_output := File f; open_glob_file f

let dump_string s =
  if dump () then Pervasives.output_string !glob_file s


let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
let continue () = glob_output := !previous_state

type coqdoc_state = Lexer.location_table

let coqdoc_freeze = Lexer.location_table
let coqdoc_unfreeze = Lexer.restore_location_table

open Decl_kinds

let type_of_logical_kind = function
  | IsDefinition def ->
      (match def with
      | Definition -> "def"
      | Coercion -> "coe"
      | SubClass -> "subclass"
      | CanonicalStructure -> "canonstruc"
      | Example -> "ex"
      | Fixpoint -> "def"
      | CoFixpoint -> "def"
      | Scheme -> "scheme"
      | StructureComponent -> "proj"
      | IdentityCoercion -> "coe"
      | Instance -> "inst"
      | Method -> "meth")
  | IsAssumption a ->
      (match a with
      | Definitional -> "defax"
      | Logical -> "prfax"
      | Conjectural -> "prfax")
  | IsProof th ->
      (match th with
      | Theorem
      | Lemma
      | Fact
      | Remark
      | Property
      | Proposition
      | Corollary -> "thm")

let type_of_global_ref gr =
  if Typeclasses.is_class gr then
    "class"
  else
    match gr with
    | Libnames.ConstRef cst ->
	type_of_logical_kind (Decls.constant_kind cst)
    | Libnames.VarRef v ->
	"var" ^ type_of_logical_kind (Decls.variable_kind v)
    | Libnames.IndRef ind ->
	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
	  if mib.Declarations.mind_record then
	    if mib.Declarations.mind_finite then "rec"
	    else "corec"
	  else if mib.Declarations.mind_finite then "ind"
	  else "coind"
    | Libnames.ConstructRef _ -> "constr"

let remove_sections dir =
  if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
    (* Not yet (fully) discharged *)
    Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
  else
    (* Theorem/Lemma outside its outer section of definition *)
    dir

let dump_ref loc filepath modpath ident ty =
  dump_string (Printf.sprintf "R%d %s %s %s %s\n"
		  (fst (Util.unloc loc)) filepath modpath ident ty)

let add_glob_gen loc sp lib_dp ty =
  if dump () then
    let mod_dp,id = Libnames.repr_path sp in
    let mod_dp = remove_sections mod_dp in
    let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
    let filepath = Names.string_of_dirpath lib_dp in
    let modpath = Names.string_of_dirpath mod_dp_trunc in
    let ident = Names.string_of_id id in
      dump_ref loc filepath modpath ident ty

let add_glob loc ref =
  if dump () && loc <> Util.dummy_loc then
    let sp = Nametab.path_of_global ref in
    let lib_dp = Lib.library_part ref in
    let ty = type_of_global_ref ref in
      add_glob_gen loc sp lib_dp ty

let mp_of_kn kn =
  let mp,sec,l = Names.repr_kn kn in
    Names.MPdot (mp,l)

let add_glob_kn loc kn =
  if dump () && loc <> Util.dummy_loc then
    let sp = Nametab.path_of_syndef kn in
    let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
      add_glob_gen loc sp lib_dp "syndef"

let dump_binding loc id = ()

let dump_definition (loc, id) sec s =
  dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))

let dump_reference loc modpath ident ty =
  dump_string (Printf.sprintf "R%d %s %s %s %s\n"
		  (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)

let dump_constraint ((loc, n), _, _) sec ty =
  match n with
    | Names.Name id -> dump_definition (loc, id) sec ty
    | Names.Anonymous -> ()

let dump_name (loc, n) sec ty =
  match n with
    | Names.Name id -> dump_definition (loc, id) sec ty
    | Names.Anonymous -> ()

let dump_local_binder b sec ty =
  if dump () then
    match b with
      | Topconstr.LocalRawAssum (nl, _, _) ->
	  List.iter (fun x -> dump_name x sec ty) nl
      | Topconstr.LocalRawDef _ -> ()

let dump_modref loc mp ty =
  if dump () then
    let (dp, l) = Lib.split_modpath mp in
    let l = if l = [] then l else Util.list_drop_last l in
    let fp = Names.string_of_dirpath dp in
    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
      dump_string (Printf.sprintf "R%d %s %s %s %s\n"
		      (fst (Util.unloc loc)) fp mp "<>" ty)

let dump_moddef loc mp ty =
  if dump () then
    let (dp, l) = Lib.split_modpath mp in
    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)

let dump_libref loc dp ty =
  dump_string (Printf.sprintf "R%d %s <> <> %s\n"
		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)

let cook_notation df sc =
  let ntn = String.make (String.length df * 3) '_' in
  let j = ref 0 in
  let quoted = ref false in
  for i = 0 to String.length df - 1 do
    if df.[i] = '\'' then quoted := not !quoted;
    if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else
    if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else
    if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else
    (ntn.[!j] <- df.[i]; incr j)
  done;
  let df = String.sub ntn 0 !j in
  match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df

let dump_notation (loc,(df,_)) sc sec =
  (* We dump the location of the opening '"' *)
  dump_string (Printf.sprintf "not %d %s %s\n" (fst (Util.unloc loc))
    (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))

let dump_notation_location posl df (((path,secpath),_),sc) =
  if dump () then
    let path = Names.string_of_dirpath path in
    let secpath = Names.string_of_dirpath secpath in
    let df = cook_notation df sc in
    List.iter (fun (bl,el) ->
      dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df))
      posl