Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 182 insertions, 0 deletions

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
new file mode 100644
index 00000000..7d1cc206
--- /dev/null
+++ b/scripts/coqc.ml
@@ -0,0 +1,182 @@
+(************************************************************************)
+(*  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: coqc.ml,v 1.25.2.1 2004/07/16 19:30:50 herbelin Exp $ *)
+
+(* Afin de rendre Coq plus portable, ce programme Caml remplace le script
+   coqc. 
+
+   Ici, on trie la ligne de commande pour en extraire les fichiers à compiler,
+   puis on les compile un par un en passant le reste de la ligne de commande
+   à un process "coqtop -batch -load-vernac-source <fichier>".
+
+   On essaye au maximum d'utiliser les modules Sys et Filename pour que la
+   portabilité soit maximale, mais il reste encore des appels à des fonctions
+   du module Unix. Ceux-ci sont préfixés par "Unix."
+*)
+
+(* environment *)
+
+let environment = Unix.environment ()
+
+let bindir = ref Coq_config.bindir
+let binary = ref ("coqtop." ^ Coq_config.best)
+let image = ref ""
+
+(* the $COQBIN environment variable has priority over the Coq_config value *)
+let _ = 
+  try 
+    let c = Sys.getenv "COQBIN" in
+    if c <> "" then bindir := c
+  with Not_found -> ()
+
+(* coqc options *)
+
+let specification = ref false
+let keep = ref false
+let verbose = ref false
+
+(* Verifies that a string starts by a letter and do not contain
+   others caracters than letters, digits, or `_` *)
+
+let check_module_name s =
+  let err c =
+    output_string stderr "Invalid module name: ";
+    output_string stderr s;
+    output_string stderr " character ";
+    if c = '\'' then
+      output_string stderr "\"'\""
+    else
+      (output_string stderr"'"; output_char stderr c; output_string stderr"'");
+    output_string stderr " is not allowed in module names\n";
+    exit 1 
+  in
+  match String.get s 0 with 
+    | 'a' .. 'z' | 'A' .. 'Z' -> 
+	for i = 1 to (String.length s)-1 do
+	  match String.get s i with 
+	    | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_'  -> ()
+	    | c -> err c
+	done
+    | c -> err c
+
+let rec make_compilation_args = function
+  | [] -> []
+  | file :: fl -> 
+      let dirname = Filename.dirname file in
+      let basename = Filename.basename file in
+      let modulename =
+        if Filename.check_suffix basename ".v" then
+          Filename.chop_suffix basename ".v"
+        else
+          basename
+      in
+      check_module_name modulename;
+      let file = Filename.concat dirname modulename in
+      (if !verbose then "-compile-verbose" else "-compile")
+      :: file :: (make_compilation_args fl)
+
+(* compilation of files [files] with command [command] and args [args] *)
+
+let compile command args files =
+  let args' = command :: args @ (make_compilation_args files) in
+  match Sys.os_type with
+  | "Win32" -> 
+     let pid = 
+        Unix.create_process_env command (Array.of_list args') environment
+        Unix.stdin Unix.stdout Unix.stderr 
+     in
+     ignore (Unix.waitpid [] pid)
+  | _ ->
+     Unix.execvpe command (Array.of_list args') environment 
+
+(* parsing of the command line
+ *
+ * special treatment for -bindir and -i.
+ * other options are passed to coqtop *)
+
+let usage () =
+  Usage.print_usage_coqc () ;
+  flush stderr ;
+  exit 1
+
+let parse_args () =
+  let rec parse (cfiles,args) = function
+    | [] -> 
+	List.rev cfiles, List.rev args
+    | "-i" :: rem -> 
+	specification := true ; parse (cfiles,args) rem
+    | "-t" :: rem -> 
+	keep := true ; parse (cfiles,args) rem
+    | ("-verbose" | "--verbose") :: rem -> 
+	verbose := true ; parse (cfiles,args) rem
+    | "-boot" :: rem ->
+	bindir:= Filename.concat Coq_config.coqtop "bin";
+	parse (cfiles, "-boot"::args) rem
+    | "-bindir" :: d :: rem ->
+	bindir := d ; parse (cfiles,args) rem
+    | "-bindir" :: []       ->
+	usage ()
+    | "-byte" :: rem ->
+	binary := "coqtop.byte"; parse (cfiles,args) rem
+    | "-opt" :: rem ->
+	binary := "coqtop.opt"; parse (cfiles,args) rem
+    | "-image" :: f :: rem ->
+	image := f; parse (cfiles,args) rem
+    | "-image" :: [] ->
+	usage ()
+    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
+    | ("-libdir"|"-I"|"-include"|"-outputstate"
+      |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
+      |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
+      |"-init-file"|"-dump-glob" as o) :: rem ->
+	begin
+	  match rem with
+	    | s :: rem' -> parse (cfiles,s::o::args) rem'
+	    | []        -> usage ()
+	end
+    | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
+    | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois"
+      |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
+      |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate"|"-strict-implicit"
+      |"-dont-load-proofs"|"-impredicative-set" as o) :: rem ->
+	parse (cfiles,o::args) rem
+    | ("-v"|"--version") :: _ ->
+        Usage.version ()
+    | "-where" :: _ -> 
+	print_endline Coq_config.coqlib; exit 0
+    | f :: rem -> 
+	if Sys.file_exists f then
+	  parse (f::cfiles,args) rem
+	else 
+	  let fv = f ^ ".v" in
+	  if Sys.file_exists fv then
+	    parse (fv::cfiles,args) rem
+	  else begin
+	    prerr_endline ("coqc: "^f^": no such file or directory") ;
+	    exit 1
+	  end
+  in
+  parse ([],[]) (List.tl (Array.to_list Sys.argv))
+
+(* main: we parse the command line, define the command to compile files
+ * and then call the compilation on each file *)
+
+let main () =
+  let cfiles, args = parse_args () in
+  if cfiles = [] then begin
+    prerr_endline "coqc: too few arguments" ;
+    usage ()
+  end;
+  let coqtopname = 
+    if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension)
+  in
+(*  List.iter (compile coqtopname args) cfiles*)
+  Unix.handle_unix_error (compile coqtopname args) cfiles
+    
+let _ = Printexc.print main (); exit 0