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
(************************************************************************)
9
(* coqwc - counts the lines of spec, proof and comments in Coq sources
10
* Copyright (C) 2003 Jean-Christophe Filli�tre *)
12
(*i $Id: coqwc.mll 9691 2007-03-08 15:29:27Z msozeau $ i*)
14
(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
15
It assumes the files to be lexically well-formed. *)
23
(*s Command-line options. *)
25
let spec_only = ref false
26
let proof_only = ref false
27
let percentage = ref false
28
let skip_header = ref true
30
(*s Counters. [clines] counts the number of code lines of the current
31
file, and [dlines] the number of comment lines. [tclines] and [tdlines]
32
are the corresponding totals. *)
42
let update_totals () =
43
tslines := !tslines + !slines;
44
tplines := !tplines + !plines;
45
tdlines := !tdlines + !dlines
47
(*s The following booleans indicate whether we have seen spec, proof or
48
comment so far on the current line; when a newline is reached, [newline]
49
is called and updates the counters accordingly. *)
51
let seen_spec = ref false
52
let seen_proof = ref false
53
let seen_comment = ref false
56
if !seen_spec then incr slines;
57
if !seen_proof then incr plines;
58
if !seen_comment then incr dlines;
59
seen_spec := false; seen_proof := false; seen_comment := false
61
let reset_counters () =
62
seen_spec := false; seen_proof := false; seen_comment := false;
63
slines := 0; plines := 0; dlines := 0
67
let print_line sl pl dl fo =
68
if not !proof_only then printf " %8d" sl;
69
if not !spec_only then printf " %8d" pl;
70
if not (!proof_only || !spec_only) then printf " %8d" dl;
71
(match fo with Some f -> printf " %s" f | _ -> ());
72
if !percentage then begin
73
let s = sl + pl + dl in
74
let p = if s > 0 then 100 * dl / s else 0 in
79
let print_file fo = print_line !slines !plines !dlines fo
81
let print_totals () = print_line !tslines !tplines !tdlines (Some "total")
85
(*s Shortcuts for regular expressions. The [rcs] regular expression
86
is used to skip the CVS infos possibly contained in some comments,
87
in order not to consider it as documentation. *)
89
let space = [' ' '\t' '\r']
92
'\\' (['\\' '\'' 'n' 't' 'b' 'r'] | ['0'-'9'] ['0'-'9'] ['0'-'9'])) "'"
94
"Author" | "Date" | "Header" | "Id" | "Name" | "Locker" | "Log" |
95
"RCSfile" | "Revision" | "Source" | "State"
96
let rcs = "\036" rcs_keyword [^ '$']* "\036"
97
let stars = "(*" '*'* "*)"
98
let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
100
"Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
102
("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.'
104
(*s [spec] scans the specification. *)
107
| "(*" { comment lexbuf; spec lexbuf }
108
| '"' { let n = string lexbuf in slines := !slines + n;
109
seen_spec := true; spec lexbuf }
110
| '\n' { newline (); spec lexbuf }
114
{ seen_spec := true; spec_to_dot lexbuf; proof lexbuf }
116
{ seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf }
117
| "Program"? "Definition" space
118
{ seen_spec := true; definition lexbuf }
119
| "Program"? "Fixpoint" space
120
{ seen_spec := true; definition lexbuf }
122
{ seen_spec := true; spec lexbuf }
125
(*s [spec_to_dot] scans a spec until a dot is reached and returns. *)
127
and spec_to_dot = parse
128
| "(*" { comment lexbuf; spec_to_dot lexbuf }
129
| '"' { let n = string lexbuf in slines := !slines + n;
130
seen_spec := true; spec_to_dot lexbuf }
131
| '\n' { newline (); spec_to_dot lexbuf }
134
{ spec_to_dot lexbuf }
136
{ seen_spec := true; spec_to_dot lexbuf }
139
(*s [definition] scans a definition; passes to [proof] is the body is
140
absent, and to [spec] otherwise *)
142
and definition = parse
143
| "(*" { comment lexbuf; definition lexbuf }
144
| '"' { let n = string lexbuf in slines := !slines + n;
145
seen_spec := true; definition lexbuf }
146
| '\n' { newline (); definition lexbuf }
147
| ":=" { seen_spec := true; spec lexbuf }
148
| dot { proof lexbuf }
150
{ definition lexbuf }
152
{ seen_spec := true; definition lexbuf }
155
(*s Scans a proof, then returns to [spec]. *)
158
| "(*" { comment lexbuf; proof lexbuf }
159
| '"' { let n = string lexbuf in plines := !plines + n;
160
seen_proof := true; proof lexbuf }
163
| '\n' { newline (); proof lexbuf }
165
{ seen_proof := true; proof lexbuf }
167
{ proof_term lexbuf }
169
{ seen_proof := true; spec lexbuf }
171
{ seen_proof := true; proof lexbuf }
174
and proof_term = parse
175
| "(*" { comment lexbuf; proof_term lexbuf }
176
| '"' { let n = string lexbuf in plines := !plines + n;
177
seen_proof := true; proof_term lexbuf }
179
{ proof_term lexbuf }
180
| '\n' { newline (); proof_term lexbuf }
181
| dot { spec lexbuf }
183
{ seen_proof := true; proof_term lexbuf }
186
(*s Scans a comment. *)
189
| "(*" { comment lexbuf; comment lexbuf }
191
| '"' { let n = string lexbuf in dlines := !dlines + n;
192
seen_comment := true; comment lexbuf }
193
| '\n' { newline (); comment lexbuf }
197
{ seen_comment := true; comment lexbuf }
200
(*s The entry [string] reads a string until its end and returns the number
201
of newlines it contains. *)
205
| '\\' ('\\' | 'n' | '"') { string lexbuf }
206
| '\n' { succ (string lexbuf) }
207
| _ { string lexbuf }
210
(*s The following entry [read_header] is used to skip the possible header at
211
the beggining of files (unless option \texttt{-e} is specified).
212
It stops whenever it encounters an empty line or any character outside
213
a comment. In this last case, it correctly resets the lexer position
214
on that character (decreasing [lex_curr_pos] by 1). *)
216
and read_header = parse
217
| "(*" { skip_comment lexbuf; skip_until_nl lexbuf;
220
| space+ { read_header lexbuf }
221
| _ { lexbuf.lex_curr_pos <- lexbuf.lex_curr_pos - 1 }
224
and skip_comment = parse
226
| "(*" { skip_comment lexbuf; skip_comment lexbuf }
227
| _ { skip_comment lexbuf }
230
and skip_until_nl = parse
232
| _ { skip_until_nl lexbuf }
237
(*s Processing files and channels. *)
239
let process_channel ch =
240
let lb = Lexing.from_channel ch in
242
if !skip_header then read_header lb;
247
let ch = open_in f in
253
| Sys_error "Is a directory" ->
254
flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
256
flush stdout; eprintf "coqwc: %s\n" s; flush stderr
258
(*s Parsing of the command line. *)
261
prerr_endline "usage: coqwc [options] [files]";
262
prerr_endline "Options are:";
263
prerr_endline " -p print percentage of comments";
264
prerr_endline " -s print only the spec size";
265
prerr_endline " -r print only the proof size";
266
prerr_endline " -e (everything) do not skip headers";
269
let rec parse = function
271
| ("-h" | "-?" | "-help" | "--help") :: _ -> usage ()
272
| ("-s" | "--spec-only") :: args ->
273
proof_only := false; spec_only := true; parse args
274
| ("-r" | "--proof-only") :: args ->
275
spec_only := false; proof_only := true; parse args
276
| ("-p" | "--percentage") :: args -> percentage := true; parse args
277
| ("-e" | "--header") :: args -> skip_header := false; parse args
278
| f :: args -> f :: (parse args)
283
let files = parse (List.tl (Array.to_list Sys.argv)) in
284
if not (!spec_only || !proof_only) then
285
printf " spec proof comments\n";
287
| [] -> process_channel stdin; print_file None
288
| [f] -> process_file f
289
| _ -> List.iter process_file files; print_totals ()
291
let _ = Printexc.catch main ()
added
removed
tools/coqwc.mll
