Revision ef34b4ae src/parser_lustre.mly
src/parser_lustre.mly | ||
---|---|---|
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 Utils |
|
14 |
open LustreSpec |
|
15 |
open Corelang |
|
16 |
open Dimension |
|
17 |
open Parse |
|
18 |
|
|
19 |
let get_loc () = Location.symbol_rloc () |
|
20 |
let mktyp x = mktyp (get_loc ()) x |
|
21 |
let mkclock x = mkclock (get_loc ()) x |
|
22 |
let mkvar_decl x = mkvar_decl (get_loc ()) x |
|
23 |
let mkexpr x = mkexpr (get_loc ()) x |
|
24 |
let mkeexpr x = mkeexpr (get_loc ()) x |
|
25 |
let mkeq x = mkeq (get_loc ()) x |
|
26 |
let mkassert x = mkassert (get_loc ()) x |
|
27 |
let mktop_decl x = mktop_decl (get_loc ()) x |
|
28 |
let mkpredef_call x = mkpredef_call (get_loc ()) x |
|
29 |
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*) |
|
30 |
|
|
31 |
let mkdim_int i = mkdim_int (get_loc ()) i |
|
32 |
let mkdim_bool b = mkdim_bool (get_loc ()) b |
|
33 |
let mkdim_ident id = mkdim_ident (get_loc ()) id |
|
34 |
let mkdim_appl f args = mkdim_appl (get_loc ()) f args |
|
35 |
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e |
|
36 |
|
|
37 |
let mkannots annots = { annots = annots; annot_loc = get_loc () } |
|
38 |
|
|
39 |
%} |
|
40 |
|
|
41 |
%token <int> INT |
|
42 |
%token <string> REAL |
|
43 |
%token <float> FLOAT |
|
44 |
%token <string> STRING |
|
45 |
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST |
|
46 |
%token STATELESS ASSERT OPEN QUOTE FUNCTION |
|
47 |
%token <string> IDENT |
|
48 |
%token <LustreSpec.expr_annot> ANNOT |
|
49 |
%token <LustreSpec.node_annot> NODESPEC |
|
50 |
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL |
|
51 |
%token AMPERAMPER BARBAR NOT POWER |
|
52 |
%token IF THEN ELSE |
|
53 |
%token UCLOCK DCLOCK PHCLOCK TAIL |
|
54 |
%token MERGE FBY WHEN WHENNOT EVERY |
|
55 |
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST |
|
56 |
%token STRUCT ENUM |
|
57 |
%token TINT TFLOAT TREAL TBOOL TCLOCK |
|
58 |
%token RATE DUE |
|
59 |
%token EQ LT GT LTE GTE NEQ |
|
60 |
%token AND OR XOR IMPL |
|
61 |
%token MULT DIV MOD |
|
62 |
%token MINUS PLUS UMINUS |
|
63 |
%token PRE ARROW |
|
64 |
%token REQUIRES ENSURES OBSERVER |
|
65 |
%token INVARIANT BEHAVIOR ASSUMES |
|
66 |
%token EXISTS FORALL |
|
67 |
%token PROTOTYPE LIB |
|
68 |
%token EOF |
|
69 |
|
|
70 |
%nonassoc prec_exists prec_forall |
|
71 |
%nonassoc COMMA |
|
72 |
%left MERGE IF |
|
73 |
%nonassoc ELSE |
|
74 |
%right ARROW FBY |
|
75 |
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK |
|
76 |
%right COLCOL |
|
77 |
%right IMPL |
|
78 |
%left OR XOR BARBAR |
|
79 |
%left AND AMPERAMPER |
|
80 |
%left NOT |
|
81 |
%nonassoc INT |
|
82 |
%nonassoc EQ LT GT LTE GTE NEQ |
|
83 |
%left MINUS PLUS |
|
84 |
%left MULT DIV MOD |
|
85 |
%left UMINUS |
|
86 |
%left POWER |
|
87 |
%left PRE LAST |
|
88 |
%nonassoc RBRACKET |
|
89 |
%nonassoc LBRACKET |
|
90 |
|
|
91 |
%start prog |
|
92 |
%type <LustreSpec.top_decl list> prog |
|
93 |
|
|
94 |
%start header |
|
95 |
%type <bool -> LustreSpec.top_decl list> header |
|
96 |
|
|
97 |
%start lustre_annot |
|
98 |
%type <LustreSpec.expr_annot> lustre_annot |
|
99 |
|
|
100 |
%start lustre_spec |
|
101 |
%type <LustreSpec.node_annot> lustre_spec |
|
102 |
|
|
103 |
%% |
|
104 |
|
|
105 |
prog: |
|
106 |
open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) } |
|
107 |
|
|
108 |
typ_def_prog: |
|
109 |
typ_def_list { $1 true } |
|
110 |
|
|
111 |
header: |
|
112 |
open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ let typs = $2 own in typs @ (List.rev ($3 own)))) } |
|
113 |
|
|
114 |
open_list: |
|
115 |
{ [] } |
|
116 |
| open_lusi open_list { $1 :: $2 } |
|
117 |
|
|
118 |
open_lusi: |
|
119 |
| OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))} |
|
120 |
| OPEN LT IDENT GT { mktop_decl (Open (false, $3)) } |
|
121 |
|
|
122 |
top_decl_list: |
|
123 |
{[]} |
|
124 |
| top_decl_list top_decl {$2::$1} |
|
125 |
|
|
126 |
|
|
127 |
top_decl_header_list: |
|
128 |
{(fun own -> []) } |
|
129 |
| top_decl_header_list top_decl_header {(fun own -> let h1 = $1 own in ($2 own)::h1) } |
|
130 |
|
|
131 |
state_annot: |
|
132 |
FUNCTION { true } |
|
133 |
| NODE { false } |
|
134 |
|
|
135 |
top_decl_header: |
|
136 |
| CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ -> top } |
|
137 |
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL |
|
138 |
{let nd = mktop_decl (ImportedNode |
|
139 |
{nodei_id = $3; |
|
140 |
nodei_type = Types.new_var (); |
|
141 |
nodei_clock = Clocks.new_var true; |
|
142 |
nodei_inputs = List.rev $5; |
|
143 |
nodei_outputs = List.rev $10; |
|
144 |
nodei_stateless = $2; |
|
145 |
nodei_spec = $1; |
|
146 |
nodei_prototype = $13; |
|
147 |
nodei_in_lib = $14;}) |
|
148 |
in |
|
149 |
(fun own -> add_node own $3 nd; nd) } |
|
150 |
|
|
151 |
prototype_opt: |
|
152 |
{ None } |
|
153 |
| PROTOTYPE IDENT { Some $2} |
|
154 |
|
|
155 |
in_lib_opt: |
|
156 |
{ None } |
|
157 |
| LIB IDENT {Some $2} |
|
158 |
|
|
159 |
top_decl: |
|
160 |
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) } |
|
161 |
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
162 |
{let eqs, asserts, annots = $16 in |
|
163 |
let nd = mktop_decl (Node |
|
164 |
{node_id = $3; |
|
165 |
node_type = Types.new_var (); |
|
166 |
node_clock = Clocks.new_var true; |
|
167 |
node_inputs = List.rev $5; |
|
168 |
node_outputs = List.rev $10; |
|
169 |
node_locals = List.rev $14; |
|
170 |
node_gencalls = []; |
|
171 |
node_checks = []; |
|
172 |
node_asserts = asserts; |
|
173 |
node_eqs = eqs; |
|
174 |
node_dec_stateless = $2; |
|
175 |
node_stateless = None; |
|
176 |
node_spec = $1; |
|
177 |
node_annot = annots}) |
|
178 |
in |
|
179 |
add_node true $3 nd; nd} |
|
180 |
|
|
181 |
nodespec_list: |
|
182 |
{ None } |
|
183 |
| NODESPEC nodespec_list { |
|
184 |
(function |
|
185 |
| None -> (fun s1 -> Some s1) |
|
186 |
| Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 } |
|
187 |
|
|
188 |
typ_def_list: |
|
189 |
/* empty */ { (fun own -> []) } |
|
190 |
| typ_def SCOL typ_def_list { (fun own -> let ty1 = ($1 own) in ty1 :: ($3 own)) } |
|
191 |
|
|
192 |
typ_def: |
|
193 |
TYPE IDENT EQ typ_def_rhs { let typ = mktop_decl (Type { ty_def_id = $2; |
|
194 |
ty_def_desc = $4 |
|
195 |
}) |
|
196 |
in (fun own -> add_type own $2 typ; typ) } |
|
197 |
|
|
198 |
typ_def_rhs: |
|
199 |
typeconst { $1 } |
|
200 |
| ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) } |
|
201 |
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) } |
|
202 |
|
|
203 |
array_typ_decl: |
|
204 |
{ fun typ -> typ } |
|
205 |
| POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) } |
|
206 |
|
|
207 |
typeconst: |
|
208 |
TINT array_typ_decl { $2 Tydec_int } |
|
209 |
| TBOOL array_typ_decl { $2 Tydec_bool } |
|
210 |
| TREAL array_typ_decl { $2 Tydec_real } |
|
211 |
| TFLOAT array_typ_decl { $2 Tydec_float } |
|
212 |
| IDENT array_typ_decl { $2 (Tydec_const $1) } |
|
213 |
| TBOOL TCLOCK { Tydec_clock Tydec_bool } |
|
214 |
| IDENT TCLOCK { Tydec_clock (Tydec_const $1) } |
|
215 |
|
|
216 |
tag_list: |
|
217 |
IDENT { $1 :: [] } |
|
218 |
| tag_list COMMA IDENT { $3 :: $1 } |
|
219 |
|
|
220 |
field_list: { [] } |
|
221 |
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 } |
|
222 |
|
|
223 |
eq_list: |
|
224 |
{ [], [], [] } |
|
225 |
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl} |
|
226 |
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl} |
|
227 |
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl} |
|
228 |
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl} |
|
229 |
|
|
230 |
automaton: |
|
231 |
AUTOMATON IDENT handler_list { failwith "not implemented" } |
|
232 |
|
|
233 |
handler_list: |
|
234 |
{ [] } |
|
235 |
| handler handler_list { $1::$2 } |
|
236 |
|
|
237 |
handler: |
|
238 |
STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () } |
|
239 |
|
|
240 |
unless_list: |
|
241 |
{ [] } |
|
242 |
| unless unless_list { $1::$2 } |
|
243 |
|
|
244 |
until_list: |
|
245 |
{ [] } |
|
246 |
| until until_list { $1::$2 } |
|
247 |
|
|
248 |
unless: |
|
249 |
UNLESS expr RESTART IDENT { } |
|
250 |
| UNLESS expr RESUME IDENT { } |
|
251 |
|
|
252 |
until: |
|
253 |
UNTIL expr RESTART IDENT { } |
|
254 |
| UNTIL expr RESUME IDENT { } |
|
255 |
|
|
256 |
assert_: |
|
257 |
| ASSERT expr SCOL {mkassert ($2)} |
|
258 |
|
|
259 |
eq: |
|
260 |
ident_list EQ expr SCOL {mkeq (List.rev $1,$3)} |
|
261 |
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)} |
|
262 |
|
|
263 |
lustre_spec: |
|
264 |
| contract EOF { $1 } |
|
265 |
|
|
266 |
contract: |
|
267 |
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } } |
|
268 |
|
|
269 |
requires: |
|
270 |
{ [] } |
|
271 |
| REQUIRES qexpr SCOL requires { $2::$4 } |
|
272 |
|
|
273 |
ensures: |
|
274 |
{ [] } |
|
275 |
| ENSURES qexpr SCOL ensures { $2 :: $4 } |
|
276 |
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { |
|
277 |
mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7 |
|
278 |
} |
|
279 |
|
|
280 |
behaviors: |
|
281 |
{ [] } |
|
282 |
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 } |
|
283 |
|
|
284 |
assumes: |
|
285 |
{ [] } |
|
286 |
| ASSUMES qexpr SCOL assumes { $2::$4 } |
|
287 |
|
|
288 |
/* WARNING: UNUSED RULES */ |
|
289 |
tuple_qexpr: |
|
290 |
| qexpr COMMA qexpr {[$3;$1]} |
|
291 |
| tuple_qexpr COMMA qexpr {$3::$1} |
|
292 |
|
|
293 |
qexpr: |
|
294 |
| expr { mkeexpr $1 } |
|
295 |
/* Quantifiers */ |
|
296 |
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } |
|
297 |
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 } |
|
298 |
|
|
299 |
|
|
300 |
tuple_expr: |
|
301 |
expr COMMA expr {[$3;$1]} |
|
302 |
| tuple_expr COMMA expr {$3::$1} |
|
303 |
|
|
304 |
// Same as tuple expr but accepting lists with single element |
|
305 |
array_expr: |
|
306 |
expr {[$1]} |
|
307 |
| expr COMMA array_expr {$1::$3} |
|
308 |
|
|
309 |
dim_list: |
|
310 |
dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) } |
|
311 |
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) } |
|
312 |
|
|
313 |
expr: |
|
314 |
/* constants */ |
|
315 |
INT {mkexpr (Expr_const (Const_int $1))} |
|
316 |
| REAL {mkexpr (Expr_const (Const_real $1))} |
|
317 |
| FLOAT {mkexpr (Expr_const (Const_float $1))} |
|
318 |
/* Idents or type enum tags */ |
|
319 |
| IDENT { |
|
320 |
if Hashtbl.mem tag_table $1 |
|
321 |
then mkexpr (Expr_const (Const_tag $1)) |
|
322 |
else mkexpr (Expr_ident $1)} |
|
323 |
| LPAR ANNOT expr RPAR |
|
324 |
{update_expr_annot $3 $2} |
|
325 |
| LPAR expr RPAR |
|
326 |
{$2} |
|
327 |
| LPAR tuple_expr RPAR |
|
328 |
{mkexpr (Expr_tuple (List.rev $2))} |
|
329 |
|
|
330 |
/* Array expressions */ |
|
331 |
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } |
|
332 |
| expr POWER dim { mkexpr (Expr_power ($1, $3)) } |
|
333 |
| expr LBRACKET dim_list { $3 $1 } |
|
334 |
|
|
335 |
/* Temporal operators */ |
|
336 |
| PRE expr |
|
337 |
{mkexpr (Expr_pre $2)} |
|
338 |
| expr ARROW expr |
|
339 |
{mkexpr (Expr_arrow ($1,$3))} |
|
340 |
| expr FBY expr |
|
341 |
{(*mkexpr (Expr_fby ($1,$3))*) |
|
342 |
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
|
343 |
| expr WHEN IDENT |
|
344 |
{mkexpr (Expr_when ($1,$3,tag_true))} |
|
345 |
| expr WHENNOT IDENT |
|
346 |
{mkexpr (Expr_when ($1,$3,tag_false))} |
|
347 |
| expr WHEN IDENT LPAR IDENT RPAR |
|
348 |
{mkexpr (Expr_when ($1, $5, $3))} |
|
349 |
| MERGE IDENT handler_expr_list |
|
350 |
{mkexpr (Expr_merge ($2,$3))} |
|
351 |
|
|
352 |
/* Applications */ |
|
353 |
| IDENT LPAR expr RPAR |
|
354 |
{mkexpr (Expr_appl ($1, $3, None))} |
|
355 |
| IDENT LPAR expr RPAR EVERY IDENT |
|
356 |
{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))} |
|
357 |
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR |
|
358 |
{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) } |
|
359 |
| IDENT LPAR tuple_expr RPAR |
|
360 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))} |
|
361 |
| IDENT LPAR tuple_expr RPAR EVERY IDENT |
|
362 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) } |
|
363 |
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR |
|
364 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) } |
|
365 |
|
|
366 |
/* Boolean expr */ |
|
367 |
| expr AND expr |
|
368 |
{mkpredef_call "&&" [$1;$3]} |
|
369 |
| expr AMPERAMPER expr |
|
370 |
{mkpredef_call "&&" [$1;$3]} |
|
371 |
| expr OR expr |
|
372 |
{mkpredef_call "||" [$1;$3]} |
|
373 |
| expr BARBAR expr |
|
374 |
{mkpredef_call "||" [$1;$3]} |
|
375 |
| expr XOR expr |
|
376 |
{mkpredef_call "xor" [$1;$3]} |
|
377 |
| NOT expr |
|
378 |
{mkpredef_call "not" [$2]} |
|
379 |
| expr IMPL expr |
|
380 |
{mkpredef_call "impl" [$1;$3]} |
|
381 |
|
|
382 |
/* Comparison expr */ |
|
383 |
| expr EQ expr |
|
384 |
{mkpredef_call "=" [$1;$3]} |
|
385 |
| expr LT expr |
|
386 |
{mkpredef_call "<" [$1;$3]} |
|
387 |
| expr LTE expr |
|
388 |
{mkpredef_call "<=" [$1;$3]} |
|
389 |
| expr GT expr |
|
390 |
{mkpredef_call ">" [$1;$3]} |
|
391 |
| expr GTE expr |
|
392 |
{mkpredef_call ">=" [$1;$3]} |
|
393 |
| expr NEQ expr |
|
394 |
{mkpredef_call "!=" [$1;$3]} |
|
395 |
|
|
396 |
/* Arithmetic expr */ |
|
397 |
| expr PLUS expr |
|
398 |
{mkpredef_call "+" [$1;$3]} |
|
399 |
| expr MINUS expr |
|
400 |
{mkpredef_call "-" [$1;$3]} |
|
401 |
| expr MULT expr |
|
402 |
{mkpredef_call "*" [$1;$3]} |
|
403 |
| expr DIV expr |
|
404 |
{mkpredef_call "/" [$1;$3]} |
|
405 |
| MINUS expr %prec UMINUS |
|
406 |
{mkpredef_call "uminus" [$2]} |
|
407 |
| expr MOD expr |
|
408 |
{mkpredef_call "mod" [$1;$3]} |
|
409 |
|
|
410 |
/* If */ |
|
411 |
| IF expr THEN expr ELSE expr |
|
412 |
{mkexpr (Expr_ite ($2, $4, $6))} |
|
413 |
|
|
414 |
handler_expr_list: |
|
415 |
{ [] } |
|
416 |
| handler_expr handler_expr_list { $1 :: $2 } |
|
417 |
|
|
418 |
handler_expr: |
|
419 |
LPAR IDENT ARROW expr RPAR { ($2, $4) } |
|
420 |
|
|
421 |
signed_const_array: |
|
422 |
| signed_const { [$1] } |
|
423 |
| signed_const COMMA signed_const_array { $1 :: $3 } |
|
424 |
|
|
425 |
signed_const_struct: |
|
426 |
| IDENT EQ signed_const { [ ($1, $3) ] } |
|
427 |
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 } |
|
428 |
|
|
429 |
signed_const: |
|
430 |
INT {Const_int $1} |
|
431 |
| REAL {Const_real $1} |
|
432 |
| FLOAT {Const_float $1} |
|
433 |
| IDENT {Const_tag $1} |
|
434 |
| MINUS INT {Const_int (-1 * $2)} |
|
435 |
| MINUS REAL {Const_real ("-" ^ $2)} |
|
436 |
| MINUS FLOAT {Const_float (-1. *. $2)} |
|
437 |
| LCUR signed_const_struct RCUR { Const_struct $2 } |
|
438 |
| LBRACKET signed_const_array RBRACKET { Const_array $2 } |
|
439 |
|
|
440 |
dim: |
|
441 |
INT { mkdim_int $1 } |
|
442 |
| LPAR dim RPAR { $2 } |
|
443 |
| IDENT { mkdim_ident $1 } |
|
444 |
| dim AND dim |
|
445 |
{mkdim_appl "&&" [$1;$3]} |
|
446 |
| dim AMPERAMPER dim |
|
447 |
{mkdim_appl "&&" [$1;$3]} |
|
448 |
| dim OR dim |
|
449 |
{mkdim_appl "||" [$1;$3]} |
|
450 |
| dim BARBAR dim |
|
451 |
{mkdim_appl "||" [$1;$3]} |
|
452 |
| dim XOR dim |
|
453 |
{mkdim_appl "xor" [$1;$3]} |
|
454 |
| NOT dim |
|
455 |
{mkdim_appl "not" [$2]} |
|
456 |
| dim IMPL dim |
|
457 |
{mkdim_appl "impl" [$1;$3]} |
|
458 |
|
|
459 |
/* Comparison dim */ |
|
460 |
| dim EQ dim |
|
461 |
{mkdim_appl "=" [$1;$3]} |
|
462 |
| dim LT dim |
|
463 |
{mkdim_appl "<" [$1;$3]} |
|
464 |
| dim LTE dim |
|
465 |
{mkdim_appl "<=" [$1;$3]} |
|
466 |
| dim GT dim |
|
467 |
{mkdim_appl ">" [$1;$3]} |
|
468 |
| dim GTE dim |
|
469 |
{mkdim_appl ">=" [$1;$3]} |
|
470 |
| dim NEQ dim |
|
471 |
{mkdim_appl "!=" [$1;$3]} |
|
472 |
|
|
473 |
/* Arithmetic dim */ |
|
474 |
| dim PLUS dim |
|
475 |
{mkdim_appl "+" [$1;$3]} |
|
476 |
| dim MINUS dim |
|
477 |
{mkdim_appl "-" [$1;$3]} |
|
478 |
| dim MULT dim |
|
479 |
{mkdim_appl "*" [$1;$3]} |
|
480 |
| dim DIV dim |
|
481 |
{mkdim_appl "/" [$1;$3]} |
|
482 |
| MINUS dim %prec UMINUS |
|
483 |
{mkdim_appl "uminus" [$2]} |
|
484 |
| dim MOD dim |
|
485 |
{mkdim_appl "mod" [$1;$3]} |
|
486 |
/* If */ |
|
487 |
| IF dim THEN dim ELSE dim |
|
488 |
{mkdim_ite $2 $4 $6} |
|
489 |
|
|
490 |
locals: |
|
491 |
{[]} |
|
492 |
| VAR vdecl_list SCOL {$2} |
|
493 |
|
|
494 |
vdecl_list: |
|
495 |
vdecl {$1} |
|
496 |
| vdecl_list SCOL vdecl {$3 @ $1} |
|
497 |
|
|
498 |
vdecl: |
|
499 |
/* Useless no ?*/ ident_list |
|
500 |
{List.map mkvar_decl |
|
501 |
(List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)} |
|
502 |
|
|
503 |
| ident_list COL typeconst clock |
|
504 |
{List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)} |
|
505 |
| CONST ident_list COL typeconst /* static parameters don't have clocks */ |
|
506 |
{List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)} |
|
507 |
|
|
508 |
cdecl_list: |
|
509 |
cdecl SCOL { [$1] } |
|
510 |
| cdecl_list cdecl SCOL { $2::$1 } |
|
511 |
|
|
512 |
cdecl: |
|
513 |
IDENT EQ signed_const { |
|
514 |
let c = { |
|
515 |
const_id = $1; |
|
516 |
const_loc = Location.symbol_rloc (); |
|
517 |
const_type = Types.new_var (); |
|
518 |
const_value = $3; |
|
519 |
} in |
|
520 |
Hashtbl.add consts_table $1 c; c |
|
521 |
} |
|
522 |
|
|
523 |
clock: |
|
524 |
{mkclock Ckdec_any} |
|
525 |
| when_list |
|
526 |
{mkclock (Ckdec_bool (List.rev $1))} |
|
527 |
|
|
528 |
when_cond: |
|
529 |
WHEN IDENT {($2, tag_true)} |
|
530 |
| WHENNOT IDENT {($2, tag_false)} |
|
531 |
| WHEN IDENT LPAR IDENT RPAR {($4, $2)} |
|
532 |
|
|
533 |
when_list: |
|
534 |
when_cond {[$1]} |
|
535 |
| when_list when_cond {$2::$1} |
|
536 |
|
|
537 |
ident_list: |
|
538 |
IDENT {[$1]} |
|
539 |
| ident_list COMMA IDENT {$3::$1} |
|
540 |
|
|
541 |
SCOL_opt: |
|
542 |
SCOL {} | {} |
|
543 |
|
|
544 |
|
|
545 |
lustre_annot: |
|
546 |
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } } |
|
547 |
|
|
548 |
lustre_annot_list: |
|
549 |
{ [] } |
|
550 |
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 } |
|
551 |
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 } |
|
552 |
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } |
|
553 |
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } |
|
554 |
|
|
555 |
kwd: |
|
556 |
DIV { [] } |
|
557 |
| DIV IDENT kwd { $2::$3} |
|
558 |
|
|
559 |
%% |
|
560 |
(* Local Variables: *) |
|
561 |
(* compile-command:"make -C .." *) |
|
562 |
(* End: *) |
|
563 |
|
|
564 |
|
|
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 Utils |
|
14 |
open LustreSpec |
|
15 |
open Corelang |
|
16 |
open Dimension |
|
17 |
open Parse |
|
18 |
|
|
19 |
let get_loc () = Location.symbol_rloc () |
|
20 |
|
|
21 |
let mktyp x = mktyp (get_loc ()) x |
|
22 |
let mkclock x = mkclock (get_loc ()) x |
|
23 |
let mkvar_decl x = mkvar_decl (get_loc ()) x |
|
24 |
let mkexpr x = mkexpr (get_loc ()) x |
|
25 |
let mkeexpr x = mkeexpr (get_loc ()) x |
|
26 |
let mkeq x = mkeq (get_loc ()) x |
|
27 |
let mkassert x = mkassert (get_loc ()) x |
|
28 |
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x |
|
29 |
let mkpredef_call x = mkpredef_call (get_loc ()) x |
|
30 |
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*) |
|
31 |
|
|
32 |
let mkdim_int i = mkdim_int (get_loc ()) i |
|
33 |
let mkdim_bool b = mkdim_bool (get_loc ()) b |
|
34 |
let mkdim_ident id = mkdim_ident (get_loc ()) id |
|
35 |
let mkdim_appl f args = mkdim_appl (get_loc ()) f args |
|
36 |
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e |
|
37 |
|
|
38 |
let mkannots annots = { annots = annots; annot_loc = get_loc () } |
|
39 |
|
|
40 |
%} |
|
41 |
|
|
42 |
%token <int> INT |
|
43 |
%token <string> REAL |
|
44 |
%token <float> FLOAT |
|
45 |
%token <string> STRING |
|
46 |
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST |
|
47 |
%token STATELESS ASSERT OPEN QUOTE FUNCTION |
|
48 |
%token <string> IDENT |
|
49 |
%token <string> UIDENT |
|
50 |
%token TRUE FALSE |
|
51 |
%token <LustreSpec.expr_annot> ANNOT |
|
52 |
%token <LustreSpec.node_annot> NODESPEC |
|
53 |
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL |
|
54 |
%token AMPERAMPER BARBAR NOT POWER |
|
55 |
%token IF THEN ELSE |
|
56 |
%token UCLOCK DCLOCK PHCLOCK TAIL |
|
57 |
%token MERGE FBY WHEN WHENNOT EVERY |
|
58 |
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST |
|
59 |
%token STRUCT ENUM |
|
60 |
%token TINT TFLOAT TREAL TBOOL TCLOCK |
|
61 |
%token RATE DUE |
|
62 |
%token EQ LT GT LTE GTE NEQ |
|
63 |
%token AND OR XOR IMPL |
|
64 |
%token MULT DIV MOD |
|
65 |
%token MINUS PLUS UMINUS |
|
66 |
%token PRE ARROW |
|
67 |
%token REQUIRES ENSURES OBSERVER |
|
68 |
%token INVARIANT BEHAVIOR ASSUMES |
|
69 |
%token EXISTS FORALL |
|
70 |
%token PROTOTYPE LIB |
|
71 |
%token EOF |
|
72 |
|
|
73 |
%nonassoc prec_exists prec_forall |
|
74 |
%nonassoc COMMA |
|
75 |
%left MERGE IF |
|
76 |
%nonassoc ELSE |
|
77 |
%right ARROW FBY |
|
78 |
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK |
|
79 |
%right COLCOL |
|
80 |
%right IMPL |
|
81 |
%left OR XOR BARBAR |
|
82 |
%left AND AMPERAMPER |
|
83 |
%left NOT |
|
84 |
%nonassoc INT |
|
85 |
%nonassoc EQ LT GT LTE GTE NEQ |
|
86 |
%left MINUS PLUS |
|
87 |
%left MULT DIV MOD |
|
88 |
%left UMINUS |
|
89 |
%left POWER |
|
90 |
%left PRE LAST |
|
91 |
%nonassoc RBRACKET |
|
92 |
%nonassoc LBRACKET |
|
93 |
|
|
94 |
%start prog |
|
95 |
%type <LustreSpec.top_decl list> prog |
|
96 |
|
|
97 |
%start header |
|
98 |
%type <LustreSpec.top_decl list> header |
|
99 |
|
|
100 |
%start lustre_annot |
|
101 |
%type <LustreSpec.expr_annot> lustre_annot |
|
102 |
|
|
103 |
%start lustre_spec |
|
104 |
%type <LustreSpec.node_annot> lustre_spec |
|
105 |
|
|
106 |
%% |
|
107 |
|
|
108 |
module_ident: |
|
109 |
UIDENT { $1 } |
|
110 |
| IDENT { $1 } |
|
111 |
|
|
112 |
tag_ident: |
|
113 |
UIDENT { $1 } |
|
114 |
| TRUE { tag_true } |
|
115 |
| FALSE { tag_false } |
|
116 |
|
|
117 |
node_ident: |
|
118 |
UIDENT { $1 } |
|
119 |
| IDENT { $1 } |
|
120 |
|
|
121 |
vdecl_ident: |
|
122 |
UIDENT { $1 } |
|
123 |
| IDENT { $1 } |
|
124 |
|
|
125 |
const_ident: |
|
126 |
UIDENT { $1 } |
|
127 |
| IDENT { $1 } |
|
128 |
|
|
129 |
type_ident: |
|
130 |
IDENT { $1 } |
|
131 |
|
|
132 |
prog: |
|
133 |
open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) } |
|
134 |
|
|
135 |
typ_def_prog: |
|
136 |
typ_def_list { $1 false } |
|
137 |
|
|
138 |
header: |
|
139 |
open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) } |
|
140 |
|
|
141 |
typ_def_header: |
|
142 |
typ_def_list { $1 true } |
|
143 |
|
|
144 |
open_list: |
|
145 |
{ [] } |
|
146 |
| open_lusi open_list { $1 :: $2 } |
|
147 |
|
|
148 |
open_lusi: |
|
149 |
| OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))} |
|
150 |
| OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) } |
|
151 |
|
|
152 |
top_decl_list: |
|
153 |
{[]} |
|
154 |
| top_decl_list top_decl {$2@$1} |
|
155 |
|
|
156 |
|
|
157 |
top_decl_header_list: |
|
158 |
{ [] } |
|
159 |
| top_decl_header_list top_decl_header { $2@$1 } |
|
160 |
|
|
161 |
state_annot: |
|
162 |
FUNCTION { true } |
|
163 |
| NODE { false } |
|
164 |
|
|
165 |
top_decl_header: |
|
166 |
| CONST cdecl_list { List.rev ($2 true) } |
|
167 |
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL |
|
168 |
{let nd = mktop_decl true (ImportedNode |
|
169 |
{nodei_id = $3; |
|
170 |
nodei_type = Types.new_var (); |
|
171 |
nodei_clock = Clocks.new_var true; |
|
172 |
nodei_inputs = List.rev $5; |
|
173 |
nodei_outputs = List.rev $10; |
|
174 |
nodei_stateless = $2; |
|
175 |
nodei_spec = $1; |
|
176 |
nodei_prototype = $13; |
|
177 |
nodei_in_lib = $14;}) |
|
178 |
in |
|
179 |
(*add_imported_node $3 nd;*) [nd] } |
|
180 |
|
|
181 |
prototype_opt: |
|
182 |
{ None } |
|
183 |
| PROTOTYPE node_ident { Some $2} |
|
184 |
|
|
185 |
in_lib_opt: |
|
186 |
{ None } |
|
187 |
| LIB module_ident {Some $2} |
|
188 |
|
|
189 |
top_decl: |
|
190 |
| CONST cdecl_list { List.rev ($2 false) } |
|
191 |
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
192 |
{let eqs, asserts, annots = $16 in |
|
193 |
let nd = mktop_decl false (Node |
|
194 |
{node_id = $3; |
|
195 |
node_type = Types.new_var (); |
|
196 |
node_clock = Clocks.new_var true; |
|
197 |
node_inputs = List.rev $5; |
|
198 |
node_outputs = List.rev $10; |
|
199 |
node_locals = List.rev $14; |
|
200 |
node_gencalls = []; |
|
201 |
node_checks = []; |
|
202 |
node_asserts = asserts; |
|
203 |
node_eqs = eqs; |
|
204 |
node_dec_stateless = $2; |
|
205 |
node_stateless = None; |
|
206 |
node_spec = $1; |
|
207 |
node_annot = annots}) |
|
208 |
in |
|
209 |
(*add_node $3 nd;*) [nd] } |
|
210 |
|
|
211 |
nodespec_list: |
|
212 |
{ None } |
|
213 |
| NODESPEC nodespec_list { |
|
214 |
(function |
|
215 |
| None -> (fun s1 -> Some s1) |
|
216 |
| Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 } |
|
217 |
|
|
218 |
typ_def_list: |
|
219 |
/* empty */ { (fun itf -> []) } |
|
220 |
| typ_def SCOL typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($3 itf)) } |
|
221 |
|
|
222 |
typ_def: |
|
223 |
TYPE type_ident EQ typ_def_rhs { (fun itf -> |
|
224 |
let typ = mktop_decl itf (TypeDef { tydef_id = $2; |
|
225 |
tydef_desc = $4 |
|
226 |
}) |
|
227 |
in (*add_type itf $2 typ;*) typ) } |
|
228 |
|
|
229 |
typ_def_rhs: |
|
230 |
typeconst { $1 } |
|
231 |
| ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) } |
|
232 |
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) } |
|
233 |
|
|
234 |
array_typ_decl: |
|
235 |
{ fun typ -> typ } |
|
236 |
| POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) } |
|
237 |
|
|
238 |
typeconst: |
|
239 |
TINT array_typ_decl { $2 Tydec_int } |
|
240 |
| TBOOL array_typ_decl { $2 Tydec_bool } |
|
241 |
| TREAL array_typ_decl { $2 Tydec_real } |
|
242 |
| TFLOAT array_typ_decl { $2 Tydec_float } |
|
243 |
| type_ident array_typ_decl { $2 (Tydec_const $1) } |
|
244 |
| TBOOL TCLOCK { Tydec_clock Tydec_bool } |
|
245 |
| IDENT TCLOCK { Tydec_clock (Tydec_const $1) } |
|
246 |
|
|
247 |
tag_list: |
|
248 |
UIDENT { $1 :: [] } |
|
249 |
| tag_list COMMA UIDENT { $3 :: $1 } |
|
250 |
|
|
251 |
field_list: { [] } |
|
252 |
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 } |
|
253 |
|
|
254 |
eq_list: |
|
255 |
{ [], [], [] } |
|
256 |
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl} |
|
257 |
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl} |
|
258 |
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl} |
|
259 |
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl} |
|
260 |
|
|
261 |
automaton: |
|
262 |
AUTOMATON type_ident handler_list { failwith "not implemented" } |
|
263 |
|
|
264 |
handler_list: |
|
265 |
{ [] } |
|
266 |
| handler handler_list { $1::$2 } |
|
267 |
|
|
268 |
handler: |
|
269 |
STATE UIDENT ARROW unless_list locals LET eq_list TEL until_list { () } |
|
270 |
|
|
271 |
unless_list: |
|
272 |
{ Automata.init } |
|
273 |
| unless unless_list { let (expr1, case1) = $1 in (fun case -> Automata.add_branch expr1 case1 ($2 case)) } |
|
274 |
|
|
275 |
until_list: |
|
276 |
{ Automata.init } |
|
277 |
| until until_list { let (expr1, case1) = $1 in (fun case -> Automata.add_branch expr1 case1 ($2 case)) } |
|
278 |
|
|
279 |
unless: |
|
280 |
UNLESS expr RESTART UIDENT { ($2, (get_loc (), true, $4)) } |
|
281 |
| UNLESS expr RESUME UIDENT { ($2, (get_loc (), false, $4)) } |
|
282 |
|
|
283 |
until: |
|
284 |
UNTIL expr RESTART UIDENT { ($2, (get_loc (), true, $4)) } |
|
285 |
| UNTIL expr RESUME UIDENT { ($2, (get_loc (), false, $4)) } |
|
286 |
|
|
287 |
assert_: |
|
288 |
| ASSERT expr SCOL {mkassert ($2)} |
|
289 |
|
|
290 |
eq: |
|
291 |
ident_list EQ expr SCOL {mkeq (List.rev $1,$3)} |
|
292 |
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)} |
|
293 |
|
|
294 |
lustre_spec: |
|
295 |
| contract EOF { $1 } |
|
296 |
|
|
297 |
contract: |
|
298 |
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } } |
|
299 |
|
|
300 |
requires: |
|
301 |
{ [] } |
|
302 |
| REQUIRES qexpr SCOL requires { $2::$4 } |
|
303 |
|
|
304 |
ensures: |
|
305 |
{ [] } |
|
306 |
| ENSURES qexpr SCOL ensures { $2 :: $4 } |
|
307 |
| OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { |
|
308 |
mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7 |
|
309 |
} |
|
310 |
|
|
311 |
behaviors: |
|
312 |
{ [] } |
|
313 |
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 } |
|
314 |
|
|
315 |
assumes: |
|
316 |
{ [] } |
|
317 |
| ASSUMES qexpr SCOL assumes { $2::$4 } |
|
318 |
|
|
319 |
/* WARNING: UNUSED RULES */ |
|
320 |
tuple_qexpr: |
|
321 |
| qexpr COMMA qexpr {[$3;$1]} |
|
322 |
| tuple_qexpr COMMA qexpr {$3::$1} |
|
323 |
|
|
324 |
qexpr: |
|
325 |
| expr { mkeexpr $1 } |
|
326 |
/* Quantifiers */ |
|
327 |
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } |
|
328 |
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 } |
|
329 |
|
|
330 |
|
|
331 |
tuple_expr: |
|
332 |
expr COMMA expr {[$3;$1]} |
|
333 |
| tuple_expr COMMA expr {$3::$1} |
|
334 |
|
|
335 |
// Same as tuple expr but accepting lists with single element |
|
336 |
array_expr: |
|
337 |
expr {[$1]} |
|
338 |
| expr COMMA array_expr {$1::$3} |
|
339 |
|
|
340 |
dim_list: |
|
341 |
dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) } |
|
342 |
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) } |
|
343 |
|
|
344 |
expr: |
|
345 |
/* constants */ |
|
346 |
INT {mkexpr (Expr_const (Const_int $1))} |
|
347 |
| REAL {mkexpr (Expr_const (Const_real $1))} |
|
348 |
| FLOAT {mkexpr (Expr_const (Const_float $1))} |
|
349 |
/* Idents or type enum tags */ |
|
350 |
| IDENT { mkexpr (Expr_ident $1) } |
|
351 |
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) } |
|
352 |
| LPAR ANNOT expr RPAR |
|
353 |
{update_expr_annot $3 $2} |
|
354 |
| LPAR expr RPAR |
|
355 |
{$2} |
|
356 |
| LPAR tuple_expr RPAR |
|
357 |
{mkexpr (Expr_tuple (List.rev $2))} |
|
358 |
|
|
359 |
/* Array expressions */ |
|
360 |
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } |
|
361 |
| expr POWER dim { mkexpr (Expr_power ($1, $3)) } |
|
362 |
| expr LBRACKET dim_list { $3 $1 } |
|
363 |
|
|
364 |
/* Temporal operators */ |
|
365 |
| PRE expr |
|
366 |
{mkexpr (Expr_pre $2)} |
|
367 |
| expr ARROW expr |
|
368 |
{mkexpr (Expr_arrow ($1,$3))} |
|
369 |
| expr FBY expr |
|
370 |
{(*mkexpr (Expr_fby ($1,$3))*) |
|
371 |
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
|
372 |
| expr WHEN vdecl_ident |
|
373 |
{mkexpr (Expr_when ($1,$3,tag_true))} |
|
374 |
| expr WHENNOT vdecl_ident |
|
375 |
{mkexpr (Expr_when ($1,$3,tag_false))} |
|
376 |
| expr WHEN tag_ident LPAR vdecl_ident RPAR |
|
377 |
{mkexpr (Expr_when ($1, $5, $3))} |
|
378 |
| MERGE vdecl_ident handler_expr_list |
|
379 |
{mkexpr (Expr_merge ($2,$3))} |
|
380 |
|
|
381 |
/* Applications */ |
|
382 |
| node_ident LPAR expr RPAR |
|
383 |
{mkexpr (Expr_appl ($1, $3, None))} |
|
384 |
| node_ident LPAR expr RPAR EVERY vdecl_ident |
|
385 |
{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))} |
|
386 |
| node_ident LPAR expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR |
|
387 |
{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) } |
|
388 |
| node_ident LPAR tuple_expr RPAR |
|
389 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))} |
|
390 |
| node_ident LPAR tuple_expr RPAR EVERY vdecl_ident |
|
391 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) } |
|
392 |
| node_ident LPAR tuple_expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR |
|
393 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) } |
|
394 |
|
|
395 |
/* Boolean expr */ |
|
396 |
| expr AND expr |
|
397 |
{mkpredef_call "&&" [$1;$3]} |
|
398 |
| expr AMPERAMPER expr |
|
399 |
{mkpredef_call "&&" [$1;$3]} |
|
400 |
| expr OR expr |
|
401 |
{mkpredef_call "||" [$1;$3]} |
|
402 |
| expr BARBAR expr |
|
403 |
{mkpredef_call "||" [$1;$3]} |
|
404 |
| expr XOR expr |
|
405 |
{mkpredef_call "xor" [$1;$3]} |
|
406 |
| NOT expr |
|
407 |
{mkpredef_call "not" [$2]} |
|
408 |
| expr IMPL expr |
|
409 |
{mkpredef_call "impl" [$1;$3]} |
|
410 |
|
|
411 |
/* Comparison expr */ |
|
412 |
| expr EQ expr |
|
413 |
{mkpredef_call "=" [$1;$3]} |
|
414 |
| expr LT expr |
|
415 |
{mkpredef_call "<" [$1;$3]} |
|
416 |
| expr LTE expr |
|
417 |
{mkpredef_call "<=" [$1;$3]} |
|
418 |
| expr GT expr |
|
419 |
{mkpredef_call ">" [$1;$3]} |
|
420 |
| expr GTE expr |
|
421 |
{mkpredef_call ">=" [$1;$3]} |
|
422 |
| expr NEQ expr |
|
423 |
{mkpredef_call "!=" [$1;$3]} |
|
424 |
|
|
425 |
/* Arithmetic expr */ |
|
426 |
| expr PLUS expr |
|
427 |
{mkpredef_call "+" [$1;$3]} |
|
428 |
| expr MINUS expr |
|
429 |
{mkpredef_call "-" [$1;$3]} |
|
430 |
| expr MULT expr |
|
431 |
{mkpredef_call "*" [$1;$3]} |
|
432 |
| expr DIV expr |
|
433 |
{mkpredef_call "/" [$1;$3]} |
|
434 |
| MINUS expr %prec UMINUS |
|
435 |
{mkpredef_call "uminus" [$2]} |
|
436 |
| expr MOD expr |
|
437 |
{mkpredef_call "mod" [$1;$3]} |
|
438 |
|
|
439 |
/* If */ |
|
440 |
| IF expr THEN expr ELSE expr |
|
441 |
{mkexpr (Expr_ite ($2, $4, $6))} |
|
442 |
|
|
443 |
handler_expr_list: |
|
444 |
{ [] } |
|
445 |
| handler_expr handler_expr_list { $1 :: $2 } |
|
446 |
|
|
447 |
handler_expr: |
|
448 |
LPAR tag_ident ARROW expr RPAR { ($2, $4) } |
|
449 |
|
|
450 |
signed_const_array: |
|
451 |
| signed_const { [$1] } |
|
452 |
| signed_const COMMA signed_const_array { $1 :: $3 } |
|
453 |
|
|
454 |
signed_const_struct: |
|
455 |
| IDENT EQ signed_const { [ ($1, $3) ] } |
|
456 |
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 } |
|
457 |
|
|
458 |
signed_const: |
|
459 |
INT {Const_int $1} |
|
460 |
| REAL {Const_real $1} |
|
461 |
| FLOAT {Const_float $1} |
|
462 |
| tag_ident {Const_tag $1} |
|
463 |
| MINUS INT {Const_int (-1 * $2)} |
|
464 |
| MINUS REAL {Const_real ("-" ^ $2)} |
|
465 |
| MINUS FLOAT {Const_float (-1. *. $2)} |
|
466 |
| LCUR signed_const_struct RCUR { Const_struct $2 } |
|
467 |
| LBRACKET signed_const_array RBRACKET { Const_array $2 } |
|
468 |
|
|
469 |
dim: |
|
470 |
INT { mkdim_int $1 } |
|
471 |
| LPAR dim RPAR { $2 } |
|
472 |
| UIDENT { mkdim_ident $1 } |
|
473 |
| IDENT { mkdim_ident $1 } |
|
474 |
| dim AND dim |
|
475 |
{mkdim_appl "&&" [$1;$3]} |
|
476 |
| dim AMPERAMPER dim |
|
477 |
{mkdim_appl "&&" [$1;$3]} |
|
478 |
| dim OR dim |
|
479 |
{mkdim_appl "||" [$1;$3]} |
|
480 |
| dim BARBAR dim |
|
481 |
{mkdim_appl "||" [$1;$3]} |
|
482 |
| dim XOR dim |
|
483 |
{mkdim_appl "xor" [$1;$3]} |
|
484 |
| NOT dim |
|
485 |
{mkdim_appl "not" [$2]} |
|
486 |
| dim IMPL dim |
|
487 |
{mkdim_appl "impl" [$1;$3]} |
|
488 |
|
|
489 |
/* Comparison dim */ |
|
490 |
| dim EQ dim |
|
491 |
{mkdim_appl "=" [$1;$3]} |
|
492 |
| dim LT dim |
|
493 |
{mkdim_appl "<" [$1;$3]} |
|
494 |
| dim LTE dim |
|
495 |
{mkdim_appl "<=" [$1;$3]} |
|
496 |
| dim GT dim |
|
497 |
{mkdim_appl ">" [$1;$3]} |
|
498 |
| dim GTE dim |
|
499 |
{mkdim_appl ">=" [$1;$3]} |
|
500 |
| dim NEQ dim |
|
501 |
{mkdim_appl "!=" [$1;$3]} |
|
502 |
|
|
503 |
/* Arithmetic dim */ |
|
504 |
| dim PLUS dim |
|
505 |
{mkdim_appl "+" [$1;$3]} |
|
506 |
| dim MINUS dim |
|
507 |
{mkdim_appl "-" [$1;$3]} |
|
508 |
| dim MULT dim |
|
509 |
{mkdim_appl "*" [$1;$3]} |
|
510 |
| dim DIV dim |
|
511 |
{mkdim_appl "/" [$1;$3]} |
|
512 |
| MINUS dim %prec UMINUS |
|
513 |
{mkdim_appl "uminus" [$2]} |
|
514 |
| dim MOD dim |
|
515 |
{mkdim_appl "mod" [$1;$3]} |
|
516 |
/* If */ |
|
517 |
| IF dim THEN dim ELSE dim |
|
518 |
{mkdim_ite $2 $4 $6} |
|
519 |
|
|
520 |
locals: |
|
521 |
{[]} |
|
522 |
| VAR vdecl_list SCOL {$2} |
|
523 |
|
|
524 |
vdecl_list: |
|
525 |
vdecl {$1} |
|
526 |
| vdecl_list SCOL vdecl {$3 @ $1} |
|
527 |
|
|
528 |
vdecl: |
|
529 |
/* Useless no ?*/ ident_list |
|
530 |
{List.map mkvar_decl |
|
531 |
(List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)} |
|
532 |
|
|
533 |
| ident_list COL typeconst clock |
|
534 |
{List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)} |
|
535 |
| CONST ident_list COL typeconst /* static parameters don't have clocks */ |
|
536 |
{List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)} |
|
537 |
|
|
538 |
cdecl_list: |
|
539 |
cdecl SCOL { (fun itf -> [$1 itf]) } |
|
540 |
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) } |
|
541 |
|
|
542 |
cdecl: |
|
543 |
const_ident EQ signed_const { |
|
544 |
(fun itf -> |
|
545 |
let c = mktop_decl itf (Const { |
|
546 |
const_id = $1; |
|
547 |
const_loc = Location.symbol_rloc (); |
|
548 |
const_type = Types.new_var (); |
|
549 |
const_value = $3}) |
|
550 |
in |
|
551 |
(*add_const itf $1 c;*) c) |
|
552 |
} |
|
553 |
|
|
554 |
clock: |
|
555 |
{mkclock Ckdec_any} |
|
556 |
| when_list |
|
557 |
{mkclock (Ckdec_bool (List.rev $1))} |
|
558 |
|
|
559 |
when_cond: |
|
560 |
WHEN IDENT {($2, tag_true)} |
|
561 |
| WHENNOT IDENT {($2, tag_false)} |
|
562 |
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)} |
|
563 |
|
|
564 |
when_list: |
|
565 |
when_cond {[$1]} |
|
566 |
| when_list when_cond {$2::$1} |
|
567 |
|
|
568 |
ident_list: |
|
569 |
vdecl_ident {[$1]} |
|
570 |
| ident_list COMMA vdecl_ident {$3::$1} |
|
571 |
|
|
572 |
SCOL_opt: |
|
573 |
SCOL {} | {} |
|
574 |
|
|
575 |
|
|
576 |
lustre_annot: |
|
577 |
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } } |
|
578 |
|
|
579 |
lustre_annot_list: |
|
580 |
{ [] } |
|
581 |
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 } |
|
582 |
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 } |
|
583 |
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } |
|
584 |
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } |
|
585 |
|
|
586 |
kwd: |
|
587 |
DIV { [] } |
|
588 |
| DIV IDENT kwd { $2::$3} |
|
589 |
|
|
590 |
%% |
|
591 |
(* Local Variables: *) |
|
592 |
(* compile-command:"make -C .." *) |
|
593 |
(* End: *) |
|
594 |
|
|
595 |
|
Also available in: Unified diff