Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 293 insertions, 0 deletions

diff --git a/tools/coqwc.mll b/tools/coqwc.mll
new file mode 100644
index 00000000..08bf2bcc
--- /dev/null
+++ b/tools/coqwc.mll
@@ -0,0 +1,293 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* coqwc - counts the lines of spec, proof and comments in Coq sources
+ * Copyright (C) 2003 Jean-Christophe Filliātre *)
+
+(*i $Id: coqwc.mll,v 1.2.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source. 
+    It assumes the files to be lexically well-formed. *)
+
+(*i*){ 
+open Printf
+open Lexing
+open Filename
+(*i*)
+
+(*s Command-line options. *)
+
+let spec_only = ref false
+let proof_only = ref false
+let percentage = ref false
+let skip_header = ref true
+
+(*s Counters. [clines] counts the number of code lines of the current
+    file, and [dlines] the number of comment lines. [tclines] and [tdlines]
+    are the corresponding totals. *)
+
+let slines = ref 0
+let plines = ref 0
+let dlines = ref 0
+
+let tslines = ref 0
+let tplines = ref 0
+let tdlines = ref 0
+
+let update_totals () =
+  tslines := !tslines + !slines; 
+  tplines := !tplines + !plines; 
+  tdlines := !tdlines + !dlines
+
+(*s The following booleans indicate whether we have seen spec, proof or
+    comment so far on the current line; when a newline is reached, [newline]
+    is called and updates the counters accordingly. *)
+
+let seen_spec = ref false
+let seen_proof = ref false
+let seen_comment = ref false
+
+let newline () =
+  if !seen_spec then incr slines; 
+  if !seen_proof then incr plines; 
+  if !seen_comment then incr dlines; 
+  seen_spec := false; seen_proof := false; seen_comment := false
+
+let reset_counters () = 
+  seen_spec := false; seen_proof := false; seen_comment := false;
+  slines := 0; plines := 0; dlines := 0
+
+(*s Print results. *)
+
+let print_line sl pl dl fo =
+  if not !proof_only then printf " %8d" sl;
+  if not !spec_only then printf " %8d" pl;
+  if not (!proof_only || !spec_only) then printf " %8d" dl;
+  (match fo with Some f -> printf " %s" f | _ -> ());
+  if !percentage then begin
+    let s = sl + pl + dl in
+    let p = if s > 0 then 100 * dl / s else 0 in
+    printf " (%d%%)" p
+  end;
+  print_newline ()
+
+let print_file fo = print_line !slines !plines !dlines fo
+
+let print_totals () = print_line !tslines !tplines !tdlines (Some "total")
+
+(*i*)}(*i*)
+
+(*s Shortcuts for regular expressions. The [rcs] regular expression
+    is used to skip the CVS infos possibly contained in some comments, 
+    in order not to consider it as documentation. *)
+
+let space = [' ' '\t' '\r']
+let character =
+  "'" ([^ '\\' '\''] |
+       '\\' (['\\' '\'' 'n' 't' 'b' 'r'] | ['0'-'9'] ['0'-'9'] ['0'-'9'])) "'"
+let rcs_keyword =
+  "Author" | "Date" | "Header" | "Id" | "Name" | "Locker" | "Log" |
+  "RCSfile" | "Revision" | "Source" | "State"
+let rcs = "\036" rcs_keyword [^ '$']* "\036"
+let stars = "(*" '*'* "*)"
+let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
+let proof_start =   
+  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness"
+let proof_end =
+  ("Save" | "Qed" | "Defined" | "Abort") [^'.']* '.'
+
+(*s [spec] scans the specification. *)
+
+rule spec = parse
+  | "(*"   { comment lexbuf; spec lexbuf }
+  | '"'    { let n = string lexbuf in slines := !slines + n; 
+	     seen_spec := true; spec lexbuf }
+  | '\n'   { newline (); spec lexbuf }
+  | space+ | stars 
+           { spec lexbuf }
+  | proof_start space
+           { seen_spec := true; spec_to_dot lexbuf; proof lexbuf }
+  | proof_start '\n'
+           { seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf }
+  | "Definition" space
+           { seen_spec := true; definition lexbuf }
+  | character | _ 
+	   { seen_spec := true; spec lexbuf }
+  | eof    { () }
+
+(*s [spec_to_dot] scans a spec until a dot is reached and returns. *)
+
+and spec_to_dot = parse
+  | "(*"   { comment lexbuf; spec_to_dot lexbuf }
+  | '"'    { let n = string lexbuf in slines := !slines + n; 
+	     seen_spec := true; spec_to_dot lexbuf }
+  | '\n'   { newline (); spec_to_dot lexbuf }
+  | dot    { () }
+  | space+ | stars 
+           { spec_to_dot lexbuf }
+  | character | _ 
+	   { seen_spec := true; spec_to_dot lexbuf }
+  | eof    { () }
+
+(*s [definition] scans a definition; passes to [proof] is the body is 
+    absent, and to [spec] otherwise *)
+
+and definition = parse
+  | "(*"   { comment lexbuf; definition lexbuf }
+  | '"'    { let n = string lexbuf in slines := !slines + n; 
+	     seen_spec := true; definition lexbuf }
+  | '\n'   { newline (); definition lexbuf }
+  | ":="   { seen_spec := true; spec lexbuf }
+  | dot    { proof lexbuf }
+  | space+ | stars 
+           { definition lexbuf }
+  | character | _ 
+	   { seen_spec := true; definition lexbuf }
+  | eof    { () }
+
+(*s Scans a proof, then returns to [spec]. *)
+
+and proof = parse
+  | "(*"   { comment lexbuf; proof lexbuf }
+  | '"'    { let n = string lexbuf in plines := !plines + n; 
+	     seen_proof := true; proof lexbuf }
+  | space+ | stars 
+           { proof lexbuf }
+  | '\n'   { newline (); proof lexbuf }
+  | "Proof" space* '.' 
+           { seen_proof := true; proof lexbuf }
+  | "Proof" space
+           { proof_term lexbuf }
+  | proof_end
+           { seen_proof := true; spec lexbuf }
+  | character | _ 
+	   { seen_proof := true; proof lexbuf }
+  | eof    { () }
+
+and proof_term = parse
+  | "(*"   { comment lexbuf; proof_term lexbuf }
+  | '"'    { let n = string lexbuf in plines := !plines + n; 
+	     seen_proof := true; proof_term lexbuf }
+  | space+ | stars 
+           { proof_term lexbuf }
+  | '\n'   { newline (); proof_term lexbuf }
+  | dot    { spec lexbuf }
+  | character | _ 
+	   { seen_proof := true; proof_term lexbuf }
+  | eof    { () }
+
+(*s Scans a comment. *)
+
+and comment = parse
+  | "(*"   { comment lexbuf; comment lexbuf }
+  | "*)"   { () }
+  | '"'    { let n = string lexbuf in dlines := !dlines + n; 
+	     seen_comment := true; comment lexbuf }
+  | '\n'   { newline (); comment lexbuf }
+  | space+ | stars
+	   { comment lexbuf }
+  | character | _ 
+	   { seen_comment := true; comment lexbuf }
+  | eof    { () }
+
+(*s The entry [string] reads a string until its end and returns the number
+    of newlines it contains. *)
+
+and string = parse
+  | '"'  { 0 }
+  | '\\' ('\\' | 'n' | '"') { string lexbuf }
+  | '\n' { succ (string lexbuf) }
+  | _    { string lexbuf }
+  | eof  { 0 }
+
+(*s The following entry [read_header] is used to skip the possible header at
+    the beggining of files (unless option \texttt{-e} is specified).
+    It stops whenever it encounters an empty line or any character outside
+    a comment. In this last case, it correctly resets the lexer position
+    on that character (decreasing [lex_curr_pos] by 1). *)
+ 
+and read_header = parse
+  | "(*"   { skip_comment lexbuf; skip_until_nl lexbuf; 
+	     read_header lexbuf }
+  | "\n"   { () }
+  | space+ { read_header lexbuf }
+  | _      { lexbuf.lex_curr_pos <- lexbuf.lex_curr_pos - 1 }
+  | eof    { () }
+
+and skip_comment = parse
+  | "*)" { () }
+  | "(*" { skip_comment lexbuf; skip_comment lexbuf }
+  | _    { skip_comment lexbuf }
+  | eof  { () }
+
+and skip_until_nl = parse
+  | '\n' { () }
+  | _    { skip_until_nl lexbuf }
+  | eof  { () }
+
+(*i*){(*i*)
+
+(*s Processing files and channels. *)
+
+let process_channel ch =
+  let lb = Lexing.from_channel ch in
+  reset_counters ();
+  if !skip_header then read_header lb;
+  spec lb
+
+let process_file f =
+  try
+    let ch = open_in f in
+    process_channel ch;
+    close_in ch;
+    print_file (Some f);
+    update_totals ()
+  with
+    | Sys_error "Is a directory" -> 
+	flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
+    | Sys_error s -> 
+	flush stdout; eprintf "coqwc: %s\n" s; flush stderr
+
+(*s Parsing of the command line. *)
+
+let usage () =
+  prerr_endline "usage: coqwc [options] [files]";
+  prerr_endline "Options are:";
+  prerr_endline "  -p   print percentage of comments";
+  prerr_endline "  -s   print only the spec size";
+  prerr_endline "  -r   print only the proof size";
+  prerr_endline "  -e   (everything) do not skip headers";
+  exit 1
+
+let rec parse = function
+  | [] -> []
+  | ("-h" | "-?" | "-help" | "--help") :: _ -> usage ()
+  | ("-s" | "--spec-only") :: args -> 
+      proof_only := false; spec_only := true; parse args
+  | ("-r" | "--proof-only") :: args -> 
+      spec_only := false; proof_only := true; parse args
+  | ("-p" | "--percentage") :: args -> percentage := true; parse args
+  | ("-e" | "--header") :: args -> skip_header := false; parse args
+  | f :: args -> f :: (parse args)
+
+(*s Main program. *)
+
+let main () =
+  let files = parse (List.tl (Array.to_list Sys.argv)) in
+  if not (!spec_only || !proof_only) then 
+    printf "     spec    proof comments\n";
+  match files with
+    | [] -> process_channel stdin; print_file None
+    | [f] -> process_file f
+    | _ -> List.iter process_file files; print_totals ()
+
+let _ = Printexc.catch main ()
+
+(*i*)}(*i*)
+
+