summaryrefslogtreecommitdiff
path: root/tools/gallina_lexer.mll
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_lexer.mll
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'tools/gallina_lexer.mll')
-rw-r--r--tools/gallina_lexer.mll128
1 files changed, 128 insertions, 0 deletions
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
new file mode 100644
index 00000000..ce9fb950
--- /dev/null
+++ b/tools/gallina_lexer.mll
@@ -0,0 +1,128 @@
+(************************************************************************)
+(* 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_lexer.mll,v 1.5.6.1 2004/07/16 19:31:46 herbelin Exp $ *)
+
+{
+ open Lexing
+
+ let chan_out = ref stdout
+
+ let comment_depth = ref 0
+ let cRcpt = ref 0
+ let comments = ref true
+ let print s = output_string !chan_out s
+
+ exception Fin_fichier
+
+}
+
+let space = [' ' '\t' '\n' '\r']
+let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof)
+
+rule action = parse
+ | "Theorem" space { print "Theorem "; body lexbuf;
+ cRcpt := 1; action lexbuf }
+ | "Lemma" space { print "Lemma "; body lexbuf;
+ cRcpt := 1; action lexbuf }
+ | "Fact" space { print "Fact "; body lexbuf;
+ cRcpt := 1; action lexbuf }
+ | "Remark" space { print "Remark "; body lexbuf;
+ cRcpt := 1; action lexbuf }
+ | "Goal" space { print "Goal "; body lexbuf;
+ cRcpt := 1; action lexbuf }
+ | "Correctness" space { print "Correctness "; body_pgm lexbuf;
+ cRcpt := 1; action lexbuf }
+ | "Definition" space { print "Definition "; body_def lexbuf;
+ cRcpt := 1; action lexbuf }
+ | "Hint" space { skip_until_point lexbuf ; action lexbuf }
+ | "Hints" space { skip_until_point lexbuf ; action lexbuf }
+ | "Transparent" space { skip_until_point lexbuf ; action lexbuf }
+ | "Immediate" space { skip_until_point lexbuf ; action lexbuf }
+ | "Syntax" space { skip_until_point lexbuf ; action lexbuf }
+ | "(*" { (if !comments then print "(*");
+ comment_depth := 1;
+ comment lexbuf;
+ cRcpt := 0; action lexbuf }
+ | [' ' '\t']* '\n' { if !cRcpt < 2 then print "\n";
+ cRcpt := !cRcpt+1; action lexbuf}
+ | eof { raise Fin_fichier}
+ | _ { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf }
+
+and comment = parse
+ | "(*" { (if !comments then print "(*");
+ comment_depth := succ !comment_depth; comment lexbuf }
+ | "*)" { (if !comments then print "*)");
+ comment_depth := pred !comment_depth;
+ if !comment_depth > 0 then comment lexbuf }
+ | "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf));
+ comment_depth := pred !comment_depth;
+ if !comment_depth > 0 then comment lexbuf }
+ | eof { raise Fin_fichier }
+ | _ { (if !comments then print (Lexing.lexeme lexbuf));
+ comment lexbuf }
+
+and skip_comment = parse
+ | "(*" { comment_depth := succ !comment_depth; skip_comment lexbuf }
+ | "*)" { comment_depth := pred !comment_depth;
+ if !comment_depth > 0 then skip_comment lexbuf }
+ | eof { raise Fin_fichier }
+ | _ { skip_comment lexbuf }
+
+and body_def = parse
+ | [^'.']* ":=" { print (Lexing.lexeme lexbuf); () }
+ | _ { print (Lexing.lexeme lexbuf); body lexbuf }
+
+and body = parse
+ | enddot { print ".\n"; skip_proof lexbuf }
+ | ":=" { print ".\n"; skip_proof lexbuf }
+ | "(*" { print "(*"; comment_depth := 1;
+ comment lexbuf; body lexbuf }
+ | eof { raise Fin_fichier }
+ | _ { print (Lexing.lexeme lexbuf); body lexbuf }
+
+and body_pgm = parse
+ | enddot { print ".\n"; skip_proof lexbuf }
+ | "(*" { print "(*"; comment_depth := 1;
+ comment lexbuf; body_pgm lexbuf }
+ | eof { raise Fin_fichier }
+ | _ { print (Lexing.lexeme lexbuf); body_pgm lexbuf }
+
+and skip_until_point = parse
+ | '.' '\n' { () }
+ | enddot { end_of_line lexbuf }
+ | "(*" { comment_depth := 1;
+ skip_comment lexbuf; skip_until_point lexbuf }
+ | eof { raise Fin_fichier }
+ | _ { skip_until_point lexbuf }
+
+and end_of_line = parse
+ | [' ' '\t' ]* { end_of_line lexbuf }
+ | '\n' { () }
+ | eof { raise Fin_fichier }
+ | _ { print (Lexing.lexeme lexbuf) }
+
+and skip_proof = parse
+ | "Save." { end_of_line lexbuf }
+ | "Save" space
+ { skip_until_point lexbuf }
+ | "Qed." { end_of_line lexbuf }
+ | "Qed" space
+ { skip_until_point lexbuf }
+ | "Defined." { end_of_line lexbuf }
+ | "Defined" space
+ { skip_until_point lexbuf }
+ | "Abort." { end_of_line lexbuf }
+ | "Abort" space
+ { skip_until_point lexbuf }
+ | "Proof" space { skip_until_point lexbuf }
+ | "Proof" [' ' '\t']* '.' { skip_proof lexbuf }
+ | "(*" { comment_depth := 1;
+ skip_comment lexbuf; skip_proof lexbuf }
+ | eof { raise Fin_fichier }
+ | _ { skip_proof lexbuf }