blob: 07c8126f18c7acf13c6069a8099e14b1c150532b (
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
|
(************************************************************************)
(* 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$ *)
open Printf
open Coqdep_lexer
open Coqdep_common
(** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
are now in [Coqdep_common]. The code that remains here concerns
the other options. Calling this complete coqdep with the [-boot]
option should be equivalent to calling [coqdep_boot].
*)
let option_D = ref false
let option_w = ref false
let option_sort = ref false
let sort () =
let seen = Hashtbl.create 97 in
let rec loop file =
let file = canonize file in
if not (Hashtbl.mem seen file) then begin
Hashtbl.add seen file ();
let cin = open_in (file ^ ".v") in
let lb = Lexing.from_channel cin in
try
while true do
match coq_action lb with
| Require sl ->
List.iter
(fun s ->
try loop (Hashtbl.find vKnown s)
with Not_found -> ())
sl
| RequireString s -> loop s
| _ -> ()
done
with Fin_fichier ->
close_in cin;
printf "%s%s " file !suffixe
end
in
List.iter (fun (name,_) -> loop name) !vAccu
let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151
let mL_dep_list b f =
try
Hashtbl.find dep_tab f
with Not_found ->
let deja_vu = ref ([] : string list) in
try
let chan = open_in f in
let buf = Lexing.from_channel chan in
try
while true do
let (Use_module str) = caml_action buf in
if str = b then begin
eprintf "*** Warning : in file %s the" f;
eprintf " notation %s. is useless !\n" b;
flush stderr
end else
if not (List.mem str !deja_vu) then addQueue deja_vu str
done; []
with Fin_fichier -> begin
close_in chan;
let rl = List.rev !deja_vu in
Hashtbl.add dep_tab f rl;
rl
end
with Sys_error _ -> []
let affiche_Declare f dcl =
printf "\n*** In file %s: \n" f;
printf "Declare ML Module";
List.iter (fun str -> printf " \"%s\"" str) dcl;
printf ".\n";
flush stdout
let warning_Declare f dcl =
eprintf "*** Warning : in file %s, the ML modules" f;
eprintf " declaration should be\n";
eprintf "*** Declare ML Module";
List.iter (fun str -> eprintf " \"%s\"" str) dcl;
eprintf ".\n";
flush stderr
let traite_Declare f =
let decl_list = ref ([] : string list) in
let rec treat = function
| s :: ll ->
let s' = basename_noext s in
(match search_ml_known s with
| Some mldir when not (List.mem s' !decl_list) ->
let fullname = file_name (String.uncapitalize s') mldir in
let depl = mL_dep_list s (fullname ^ ".ml") in
treat depl;
decl_list := s :: !decl_list
| _ -> ());
treat ll
| [] -> ()
in
try
let chan = open_in f in
let buf = Lexing.from_channel chan in
begin try
while true do
let tok = coq_action buf in
(match tok with
| Declare sl ->
decl_list := [];
treat sl;
decl_list := List.rev !decl_list;
if !option_D then
affiche_Declare f !decl_list
else if !decl_list <> sl then
warning_Declare f !decl_list
| _ -> ())
done
with Fin_fichier -> () end;
close_in chan
with Sys_error _ -> ()
let declare_dependencies () =
List.iter
(fun (name,_) ->
traite_Declare (name^".v");
flush stdout)
(List.rev !vAccu)
let usage () =
eprintf
"[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
flush stderr;
exit 1
let rec parse = function
| "-c" :: ll -> option_c := true; parse ll
| "-D" :: ll -> option_D := true; parse ll
| "-w" :: ll -> option_w := true; parse ll
| "-boot" :: ll -> Flags.boot := true; parse ll
| "-sort" :: ll -> option_sort := true; parse ll
| ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
| "-I" :: r :: ll -> add_dir add_known r []; parse ll
| "-I" :: [] -> usage ()
| "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
| "-R" :: ([] | [_]) -> usage ()
| "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
| "-coqlib" :: [] -> usage ()
| "-suffix" :: (s :: ll) -> suffixe := s ; parse ll
| "-suffix" :: [] -> usage ()
| "-slash" :: ll -> option_slash := true; parse ll
| ("-h"|"--help"|"-help") :: _ -> usage ()
| f :: ll -> treat_file None f; parse ll
| [] -> ()
let coqdep () =
if Array.length Sys.argv < 2 then usage ();
parse (List.tl (Array.to_list Sys.argv));
if not Coq_config.has_natdynlink then option_natdynlk := false;
if !Flags.boot then begin
add_rec_dir add_known "theories" ["Coq"];
add_rec_dir add_known "contrib" ["Coq"]
end else begin
let coqlib = Envars.coqlib () in
add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir add_coqlib_known (coqlib//"contrib") ["Coq"];
add_dir add_coqlib_known (coqlib//"user-contrib") []
end;
List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;
List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu;
warning_mult ".mli" iter_mli_known;
warning_mult ".ml" iter_ml_known;
if !option_sort then begin sort (); exit 0 end;
if !option_c && not !option_D then mL_dependencies ();
if not !option_D then coq_dependencies ();
if !option_w || !option_D then declare_dependencies ()
let _ = Printexc.catch coqdep ()
|
