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 11301 2008-08-04 19:41:18Z 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 : unit)}
| _ { 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 }
|
