summaryrefslogtreecommitdiff
path: root/tools/gallina.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /tools/gallina.ml
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'tools/gallina.ml')
-rw-r--r--tools/gallina.ml66
1 files changed, 66 insertions, 0 deletions
diff --git a/tools/gallina.ml b/tools/gallina.ml
new file mode 100644
index 00000000..c997820c
--- /dev/null
+++ b/tools/gallina.ml
@@ -0,0 +1,66 @@
+(************************************************************************)
+(* 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: gallina.ml,v 1.2.16.1 2004/07/16 19:31:46 herbelin Exp $ *)
+
+open Gallina_lexer
+
+let vfiles = ref ([] : string list)
+
+let option_moins = ref false
+
+let option_stdout = ref false
+
+let traite_fichier f =
+ try
+ let chan_in = open_in (f^".v") in
+ let buf = Lexing.from_channel chan_in in
+ if not !option_stdout then chan_out := open_out (f ^ ".g");
+ try
+ while true do Gallina_lexer.action buf done
+ with Fin_fichier -> begin
+ flush !chan_out;
+ close_in chan_in;
+ if not !option_stdout then close_out !chan_out
+ end
+ with Sys_error _ ->
+ ()
+
+let traite_stdin () =
+ try
+ let buf = Lexing.from_channel stdin in
+ try
+ while true do Gallina_lexer.action buf done
+ with Fin_fichier ->
+ flush !chan_out
+ with Sys_error _ ->
+ ()
+
+let gallina () =
+ let lg_command = Array.length Sys.argv in
+ if lg_command < 2 then begin
+ output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
+ flush stderr;
+ exit 1
+ end;
+ let treat = function
+ | "-" -> option_moins := true
+ | "-stdout" -> option_stdout := true
+ | "-nocomments" -> comments := false
+ | f ->
+ if Filename.check_suffix f ".v" then
+ vfiles := (Filename.chop_suffix f ".v") :: !vfiles
+ in
+ Array.iter treat Sys.argv;
+ if !option_moins then
+ traite_stdin ()
+ else
+ List.iter traite_fichier !vfiles
+
+let _ = Printexc.catch gallina ()
+