summaryrefslogtreecommitdiff
path: root/tools/gallina_lexer.mll
blob: 0b769dbd34b2cbd7c69174b47212e429ad6baeab (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
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 5920 2004-07-16 20:01:26Z herbelin $ *)

{
 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 }