lustrec / src / parsers / lexer_lustre.mll @ f9f06e7d
History | View | Annotate | Download (5.87 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
{ |
13 |
open Parser_lustre |
14 |
open Utils |
15 |
|
16 |
(* As advised by Caml documentation. This way a single lexer rule is |
17 |
used to handle all the possible keywords. *) |
18 |
let keyword_table = |
19 |
create_hashtable 20 [ |
20 |
"function", FUNCTION; |
21 |
"struct", STRUCT; |
22 |
"enum", ENUM; |
23 |
"automaton", AUTOMATON; |
24 |
"state", STATE; |
25 |
"until", UNTIL; |
26 |
"unless", UNLESS; |
27 |
"resume", RESUME; |
28 |
"restart", RESTART; |
29 |
"if", IF; |
30 |
"then", THEN; |
31 |
"else", ELSE; |
32 |
"merge", MERGE; |
33 |
"arrow", ARROW; |
34 |
"fby", FBY; |
35 |
"when", WHEN; |
36 |
"whenot", WHENNOT; |
37 |
"every", EVERY; |
38 |
"node", NODE; |
39 |
"let", LET; |
40 |
"tel", TEL; |
41 |
"returns", RETURNS; |
42 |
"var", VAR; |
43 |
"imported", IMPORTED; |
44 |
"type", TYPE; |
45 |
"int", TINT; |
46 |
"bool", TBOOL; |
47 |
(* "float", TFLOAT; *) |
48 |
"real", TREAL; |
49 |
"clock", TCLOCK; |
50 |
"not", NOT; |
51 |
"true", TRUE; |
52 |
"false", FALSE; |
53 |
"and", AND; |
54 |
"or", OR; |
55 |
"xor", XOR; |
56 |
"mod", MOD; |
57 |
"pre", PRE; |
58 |
"div", DIV; |
59 |
"const", CONST; |
60 |
"assert", ASSERT; |
61 |
"contract", CONTRACT; |
62 |
"lib", LIB; |
63 |
"prototype", PROTOTYPE; |
64 |
"ensure", ENSURE; |
65 |
"require", REQUIRE; |
66 |
(* "observer", OBSERVER; *) |
67 |
"invariant", INVARIANT; |
68 |
"mode", MODE; |
69 |
"assume", ASSUME; |
70 |
"contract", CONTRACT; |
71 |
"guarantees", GUARANTEES; |
72 |
"exists", EXISTS; |
73 |
"forall", FORALL; |
74 |
|
75 |
"c_code", CCODE; (* not sure how it is used *) |
76 |
"matlab", MATLAB; (* same as above *) |
77 |
] |
78 |
|
79 |
|
80 |
(* Buffer for parsing specification/annotation *) |
81 |
let buf = Buffer.create 1024 |
82 |
|
83 |
let make_annot lexbuf s = |
84 |
try |
85 |
let ann = LexerLustreSpec.annot s in |
86 |
ANNOT ann |
87 |
with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift (Location.curr lexbuf) loc, Parse.Annot_error s)) |
88 |
|
89 |
let make_spec lexbuf s = |
90 |
try |
91 |
let ns = LexerLustreSpec.spec s in |
92 |
NODESPEC ns |
93 |
with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift (Location.curr lexbuf) loc, Parse.Node_spec_error s)) |
94 |
|
95 |
} |
96 |
|
97 |
let newline = ('\010' | '\013' | "\013\010") |
98 |
let notnewline = [^ '\010' '\013'] |
99 |
let blank = [' ' '\009' '\012'] |
100 |
|
101 |
rule token = parse |
102 |
| "--@" { Buffer.clear buf; |
103 |
spec_singleline lexbuf } |
104 |
| "(*@" { Buffer.clear buf; |
105 |
spec_multiline 0 lexbuf } |
106 |
| "--!" { Buffer.clear buf; |
107 |
annot_singleline lexbuf } |
108 |
| "(*!" { Buffer.clear buf; |
109 |
annot_multiline 0 lexbuf } |
110 |
| "(*" |
111 |
{ comment 0 lexbuf } |
112 |
| "--" [^ '!' '@'] notnewline* (newline|eof) |
113 |
{ incr_line lexbuf; |
114 |
token lexbuf } |
115 |
| newline |
116 |
{ incr_line lexbuf; |
117 |
token lexbuf } |
118 |
| blank + |
119 |
{token lexbuf} |
120 |
| ((['0'-'9']+ as l) '.' (['0'-'9']* as r) ('E'|'e') (('+'|'-')? ['0'-'9']+ as exp)) as s |
121 |
{REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp , s)} |
122 |
| ((['0'-'9']+ as l) '.' (['0'-'9']* as r)) as s |
123 |
{REAL (Num.num_of_string (l^r), String.length r, s)} |
124 |
| ['0'-'9']+ |
125 |
{INT (int_of_string (Lexing.lexeme lexbuf)) } |
126 |
| "tel." {TEL} |
127 |
| "tel;" {TEL} |
128 |
| "#open" { OPEN } |
129 |
| ['_' 'a'-'z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']* |
130 |
{let s = Lexing.lexeme lexbuf in |
131 |
try |
132 |
Hashtbl.find keyword_table s |
133 |
with Not_found -> |
134 |
IDENT s} |
135 |
| ['A'-'Z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']* |
136 |
{let s = Lexing.lexeme lexbuf in |
137 |
try |
138 |
Hashtbl.find keyword_table s |
139 |
with Not_found -> |
140 |
UIDENT s} |
141 |
| "->" {ARROW} |
142 |
| "=>" {IMPL} |
143 |
| "<=" {LTE} |
144 |
| ">=" {GTE} |
145 |
| "<>" {NEQ} |
146 |
| '<' {LT} |
147 |
| '>' {GT} |
148 |
| "!=" {NEQ} |
149 |
| '-' {MINUS} |
150 |
| '+' {PLUS} |
151 |
| '/' {DIV} |
152 |
| '*' {MULT} |
153 |
| '=' {EQ} |
154 |
| '(' {LPAR} |
155 |
| ')' {RPAR} |
156 |
| '[' {LBRACKET} |
157 |
| ']' {RBRACKET} |
158 |
| '{' {LCUR} |
159 |
| '}' {RCUR} |
160 |
| ';' {SCOL} |
161 |
| ':' {COL} |
162 |
| ',' {COMMA} |
163 |
| '=' {EQ} |
164 |
| '/' {DIV} |
165 |
| "&&" {AMPERAMPER} |
166 |
| "||" {BARBAR} |
167 |
| "::" {COLCOL} |
168 |
| "^" {POWER} |
169 |
| '"' {QUOTE} |
170 |
| eof { EOF } |
171 |
| _ { raise (Parse.Error (Location.curr lexbuf, Parse.Undefined_token (Lexing.lexeme lexbuf))) } |
172 |
|
173 |
and comment n = parse |
174 |
| eof |
175 |
{ raise (Parse.Error (Location.curr lexbuf, Parse.Unfinished_comment)) } |
176 |
| "(*" |
177 |
{ comment (n+1) lexbuf } |
178 |
| "*)" |
179 |
{ if n > 0 then comment (n-1) lexbuf else token lexbuf } |
180 |
| newline |
181 |
{ incr_line lexbuf; |
182 |
comment n lexbuf } |
183 |
| _ { comment n lexbuf } |
184 |
|
185 |
and annot_singleline = parse |
186 |
| eof { make_annot lexbuf (Buffer.contents buf) } |
187 |
| newline { incr_line lexbuf; make_annot lexbuf (Buffer.contents buf) } |
188 |
| _ as c { Buffer.add_char buf c; annot_singleline lexbuf } |
189 |
|
190 |
and annot_multiline n = parse |
191 |
| eof { raise (Parse.Error (Location.curr lexbuf, Parse.Unfinished_annot)) } |
192 |
| "*)" as s { |
193 |
if n > 0 then |
194 |
(Buffer.add_string buf s; annot_multiline (n-1) lexbuf) |
195 |
else |
196 |
make_annot lexbuf (Buffer.contents buf) } |
197 |
| "(*" as s { Buffer.add_string buf s; annot_multiline (n+1) lexbuf } |
198 |
| newline as s { incr_line lexbuf; Buffer.add_string buf s; annot_multiline n lexbuf } |
199 |
| _ as c { Buffer.add_char buf c; annot_multiline n lexbuf } |
200 |
|
201 |
and spec_singleline = parse |
202 |
| eof { make_spec lexbuf (Buffer.contents buf) } |
203 |
| newline { incr_line lexbuf; make_spec lexbuf (Buffer.contents buf) } |
204 |
| _ as c { Buffer.add_char buf c; spec_singleline lexbuf } |
205 |
|
206 |
and spec_multiline n = parse |
207 |
| eof { raise (Parse.Error (Location.curr lexbuf, Parse.Unfinished_node_spec)) } |
208 |
| "*)" as s { if n > 0 then |
209 |
(Buffer.add_string buf s; spec_multiline (n-1) lexbuf) |
210 |
else |
211 |
make_spec lexbuf (Buffer.contents buf) } |
212 |
| "(*" as s { Buffer.add_string buf s; spec_multiline (n+1) lexbuf } |
213 |
| newline as s { incr_line lexbuf; Buffer.add_string buf s; spec_multiline n lexbuf } |
214 |
| _ as c { Buffer.add_char buf c; spec_multiline n lexbuf } |
215 |
|