lustrec / src / parser_lustre.mly @ 8446bf03
History  View  Annotate  Download (18.4 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 Utils 
14 
open Lustre_types 
15 
open Corelang 
16 
open Dimension 
17 
open Parse 
18  
19 
let get_loc () = Location.symbol_rloc () 
20  
21 
let mkident x = x, get_loc () 
22 
let mktyp x = mktyp (get_loc ()) x 
23 
let mkclock x = mkclock (get_loc ()) x 
24 
let mkvar_decl x loc = mkvar_decl loc ~orig:true x 
25 
let mkexpr x = mkexpr (get_loc ()) x 
26 
let mkeexpr x = mkeexpr (get_loc ()) x 
27 
let mkeq x = mkeq (get_loc ()) x 
28 
let mkassert x = mkassert (get_loc ()) x 
29 
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x 
30 
let mkpredef_call x = mkpredef_call (get_loc ()) x 
31 
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*) 
32  
33 
let mkdim_int i = mkdim_int (get_loc ()) i 
34 
let mkdim_bool b = mkdim_bool (get_loc ()) b 
35 
let mkdim_ident id = mkdim_ident (get_loc ()) id 
36 
let mkdim_appl f args = mkdim_appl (get_loc ()) f args 
37 
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e 
38  
39 
let mkannots annots = { annots = annots; annot_loc = get_loc () } 
40  
41 
let node_stack : ident list ref = ref [] 
42 
let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack 
43 
let push_node nd = node_stack:= nd :: !node_stack 
44 
let pop_node () = try node_stack := List.tl !node_stack with _ > assert false 
45 
let get_current_node () = try List.hd !node_stack with _ > assert false 
46  
47 
let rec fby expr n init = 
48 
if n<=1 then 
49 
mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr))) 
50 
else 
51 
mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n1) init)))) 
52 

53 
%} 
54  
55 
%token <int> INT 
56 
%token <Num.num * int * string> REAL 
57  
58 
%token <string> STRING 
59 
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST 
60 
%token STATELESS ASSERT OPEN QUOTE FUNCTION 
61 
%token <string> IDENT 
62 
%token <string> UIDENT 
63 
%token TRUE FALSE 
64 
%token <Lustre_types.expr_annot> ANNOT 
65 
%token <Lustre_types.node_annot> NODESPEC 
66 
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
67 
%token AMPERAMPER BARBAR NOT POWER 
68 
%token IF THEN ELSE 
69 
%token UCLOCK DCLOCK PHCLOCK TAIL 
70 
%token MERGE FBY WHEN WHENNOT EVERY 
71 
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST 
72 
%token STRUCT ENUM 
73 
%token TINT TREAL TBOOL TCLOCK 
74 
%token RATE DUE 
75 
%token EQ LT GT LTE GTE NEQ 
76 
%token AND OR XOR IMPL 
77 
%token MULT DIV MOD 
78 
%token MINUS PLUS UMINUS 
79 
%token PRE ARROW 
80 
%token REQUIRES ENSURES OBSERVER 
81 
%token INVARIANT BEHAVIOR ASSUMES CCODE MATLAB 
82 
%token EXISTS FORALL 
83 
%token PROTOTYPE LIB 
84 
%token EOF 
85  
86 
%nonassoc prec_exists prec_forall 
87 
%nonassoc COMMA 
88 
%nonassoc EVERY 
89 
%left MERGE IF 
90 
%nonassoc ELSE 
91 
%right ARROW FBY 
92 
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK 
93 
%right COLCOL 
94 
%right IMPL 
95 
%left OR XOR BARBAR 
96 
%left AND AMPERAMPER 
97 
%left NOT 
98 
%nonassoc INT 
99 
%nonassoc EQ LT GT LTE GTE NEQ 
100 
%left MINUS PLUS 
101 
%left MULT DIV MOD 
102 
%left UMINUS 
103 
%left POWER 
104 
%left PRE LAST 
105 
%nonassoc RBRACKET 
106 
%nonassoc LBRACKET 
107  
108 
%start prog 
109 
%type <Lustre_types.top_decl list> prog 
110  
111 
%start header 
112 
%type <Lustre_types.top_decl list> header 
113  
114 
%start lustre_annot 
115 
%type <Lustre_types.expr_annot> lustre_annot 
116  
117 
%start lustre_spec 
118 
%type <Lustre_types.node_annot> lustre_spec 
119  
120 
%start signed_const 
121 
%type <Lustre_types.constant> signed_const 
122  
123 
%start expr 
124 
%type <Lustre_types.expr> expr 
125  
126 
%start stmt_list 
127 
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list 
128  
129 
%start vdecl_list 
130 
%type <Lustre_types.var_decl list> vdecl_list 
131 
%% 
132  
133 
module_ident: 
134 
UIDENT { $1 } 
135 
 IDENT { $1 } 
136  
137 
tag_ident: 
138 
UIDENT { $1 } 
139 
 TRUE { tag_true } 
140 
 FALSE { tag_false } 
141  
142 
node_ident: 
143 
UIDENT { $1 } 
144 
 IDENT { $1 } 
145  
146 
node_ident_decl: 
147 
node_ident { push_node $1; $1 } 
148  
149 
vdecl_ident: 
150 
UIDENT { mkident $1 } 
151 
 IDENT { mkident $1 } 
152  
153 
const_ident: 
154 
UIDENT { $1 } 
155 
 IDENT { $1 } 
156  
157 
type_ident: 
158 
IDENT { $1 } 
159  
160 
prog: 
161 
open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) } 
162  
163 
typ_def_prog: 
164 
typ_def_list { $1 false } 
165  
166 
header: 
167 
open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) } 
168  
169 
typ_def_header: 
170 
typ_def_list { $1 true } 
171  
172 
open_list: 
173 
{ [] } 
174 
 open_lusi open_list { $1 :: $2 } 
175  
176 
open_lusi: 
177 
 OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))} 
178 
 OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) } 
179  
180 
top_decl_list: 
181 
{[]} 
182 
 top_decl_list top_decl {$2@$1} 
183  
184  
185 
top_decl_header_list: 
186 
{ [] } 
187 
 top_decl_header_list top_decl_header { $2@$1 } 
188  
189 
state_annot: 
190 
FUNCTION { true } 
191 
 NODE { false } 
192  
193 
top_decl_header: 
194 
 CONST cdecl_list { List.rev ($2 true) } 
195 
 nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_list SCOL 
196 
{let nd = mktop_decl true (ImportedNode 
197 
{nodei_id = $3; 
198 
nodei_type = Types.new_var (); 
199 
nodei_clock = Clocks.new_var true; 
200 
nodei_inputs = List.rev $5; 
201 
nodei_outputs = List.rev $10; 
202 
nodei_stateless = $2; 
203 
nodei_spec = $1; 
204 
nodei_prototype = $13; 
205 
nodei_in_lib = $14;}) 
206 
in 
207 
(*add_imported_node $3 nd;*) [nd] } 
208  
209 
prototype_opt: 
210 
{ None } 
211 
 PROTOTYPE node_ident { Some $2} 
212  
213 
in_lib_list: 
214 
{ [] } 
215 
 LIB module_ident in_lib_list { $2::$3 } 
216  
217 
top_decl: 
218 
 CONST cdecl_list { List.rev ($2 false) } 
219 
 nodespec_list state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL 
220 
{ 
221 
let stmts, asserts, annots = $16 in 
222 
(* Declaring eqs annots *) 
223 
List.iter (fun ann > 
224 
List.iter (fun (key, _) > 
225 
Annotations.add_node_ann $3 key 
226 
) ann.annots 
227 
) annots; 
228 
(* Building the node *) 
229 
let nd = mktop_decl false (Node 
230 
{node_id = $3; 
231 
node_type = Types.new_var (); 
232 
node_clock = Clocks.new_var true; 
233 
node_inputs = List.rev $5; 
234 
node_outputs = List.rev $10; 
235 
node_locals = List.rev $14; 
236 
node_gencalls = []; 
237 
node_checks = []; 
238 
node_asserts = asserts; 
239 
node_stmts = stmts; 
240 
node_dec_stateless = $2; 
241 
node_stateless = None; 
242 
node_spec = $1; 
243 
node_annot = annots}) 
244 
in 
245 
pop_node (); 
246 
(*add_node $3 nd;*) [nd] } 
247  
248 
nodespec_list: 
249 
{ None } 
250 
 NODESPEC nodespec_list { 
251 
(function 
252 
 None > (fun s1 > Some s1) 
253 
 Some s2 > (fun s1 > Some (merge_node_annot s1 s2))) $2 $1 } 
254  
255 
typ_def_list: 
256 
/* empty */ { (fun itf > []) } 
257 
 typ_def SCOL typ_def_list { (fun itf > let ty1 = ($1 itf) in ty1 :: ($3 itf)) } 
258  
259 
typ_def: 
260 
TYPE type_ident EQ typ_def_rhs { (fun itf > 
261 
let typ = mktop_decl itf (TypeDef { tydef_id = $2; 
262 
tydef_desc = $4 
263 
}) 
264 
in (*add_type itf $2 typ;*) typ) } 
265  
266 
typ_def_rhs: 
267 
typeconst { $1 } 
268 
 ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) } 
269 
 STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) } 
270  
271 
array_typ_decl: 
272 
%prec POWER { fun typ > typ } 
273 
 POWER dim array_typ_decl { fun typ > $3 (Tydec_array ($2, typ)) } 
274  
275 
typeconst: 
276 
TINT array_typ_decl { $2 Tydec_int } 
277 
 TBOOL array_typ_decl { $2 Tydec_bool } 
278 
 TREAL array_typ_decl { $2 Tydec_real } 
279 
/*  TFLOAT array_typ_decl { $2 Tydec_float } */ 
280 
 type_ident array_typ_decl { $2 (Tydec_const $1) } 
281 
 TBOOL TCLOCK { Tydec_clock Tydec_bool } 
282 
 IDENT TCLOCK { Tydec_clock (Tydec_const $1) } 
283  
284 
tag_list: 
285 
UIDENT { $1 :: [] } 
286 
 tag_list COMMA UIDENT { $3 :: $1 } 
287 

288 
field_list: { [] } 
289 
 field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 } 
290 

291 
stmt_list: 
292 
{ [], [], [] } 
293 
 eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl} 
294 
 assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl} 
295 
 ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl} 
296 
 automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl} 
297  
298 
automaton: 
299 
AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 } 
300  
301 
handler_list: 
302 
{ [] } 
303 
 handler handler_list { $1::$2 } 
304  
305 
handler: 
306 
STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 } 
307  
308 
unless_list: 
309 
{ [] } 
310 
 unless unless_list { $1::$2 } 
311  
312 
until_list: 
313 
{ [] } 
314 
 until until_list { $1::$2 } 
315  
316 
unless: 
317 
UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4) } 
318 
 UNLESS expr RESUME UIDENT { (get_loc (), $2, false, $4) } 
319  
320 
until: 
321 
UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4) } 
322 
 UNTIL expr RESUME UIDENT { (get_loc (), $2, false, $4) } 
323  
324 
assert_: 
325 
 ASSERT expr SCOL {mkassert ($2)} 
326  
327 
eq: 
328 
ident_list EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)} 
329 
 LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)} 
330  
331 
lustre_spec: 
332 
 contract EOF { $1 } 
333  
334 
contract: 
335 
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } } 
336 

337 
requires: 
338 
{ [] } 
339 
 REQUIRES qexpr SCOL requires { $2::$4 } 
340  
341 
ensures: 
342 
{ [] } 
343 
 ENSURES qexpr SCOL ensures { $2 :: $4 } 
344 
 OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { 
345 
mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7 
346 
} 
347  
348 
behaviors: 
349 
{ [] } 
350 
 BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 } 
351  
352 
assumes: 
353 
{ [] } 
354 
 ASSUMES qexpr SCOL assumes { $2::$4 } 
355  
356 
/* WARNING: UNUSED RULES */ 
357 
tuple_qexpr: 
358 
 qexpr COMMA qexpr {[$3;$1]} 
359 
 tuple_qexpr COMMA qexpr {$3::$1} 
360  
361 
qexpr: 
362 
 expr { mkeexpr $1 } 
363 
/* Quantifiers */ 
364 
 EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
365 
 FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 } 
366  
367  
368 
tuple_expr: 
369 
expr COMMA expr {[$3;$1]} 
370 
 tuple_expr COMMA expr {$3::$1} 
371  
372 
// Same as tuple expr but accepting lists with single element 
373 
array_expr: 
374 
expr {[$1]} 
375 
 expr COMMA array_expr {$1::$3} 
376  
377 
dim_list: 
378 
dim RBRACKET { fun base > mkexpr (Expr_access (base, $1)) } 
379 
 dim RBRACKET LBRACKET dim_list { fun base > $4 (mkexpr (Expr_access (base, $1))) } 
380  
381 
expr: 
382 
/* constants */ 
383 
INT {mkexpr (Expr_const (Const_int $1))} 
384 
 REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))} 
385 
 STRING {mkexpr (Expr_const (Const_string $1))} 
386  
387 
/*  FLOAT {mkexpr (Expr_const (Const_float $1))}*/ 
388 
/* Idents or type enum tags */ 
389 
 IDENT { mkexpr (Expr_ident $1) } 
390 
 tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) } 
391 
 LPAR ANNOT expr RPAR 
392 
{update_expr_annot (get_current_node ()) $3 $2} 
393 
 LPAR expr RPAR 
394 
{$2} 
395 
 LPAR tuple_expr RPAR 
396 
{mkexpr (Expr_tuple (List.rev $2))} 
397  
398 
/* Array expressions */ 
399 
 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } 
400 
 expr POWER dim { mkexpr (Expr_power ($1, $3)) } 
401 
 expr LBRACKET dim_list { $3 $1 } 
402  
403 
/* Temporal operators */ 
404 
 PRE expr 
405 
{mkexpr (Expr_pre $2)} 
406 
 expr ARROW expr 
407 
{mkexpr (Expr_arrow ($1,$3))} 
408 
 expr FBY expr 
409 
{(*mkexpr (Expr_fby ($1,$3))*) 
410 
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} 
411 
 expr WHEN vdecl_ident 
412 
{mkexpr (Expr_when ($1,fst $3,tag_true))} 
413 
 expr WHENNOT vdecl_ident 
414 
{mkexpr (Expr_when ($1,fst $3,tag_false))} 
415 
 expr WHEN tag_ident LPAR vdecl_ident RPAR 
416 
{mkexpr (Expr_when ($1, fst $5, $3))} 
417 
 MERGE vdecl_ident handler_expr_list 
418 
{mkexpr (Expr_merge (fst $2,$3))} 
419  
420 
/* Applications */ 
421 
 node_ident LPAR expr RPAR 
422 
{mkexpr (Expr_appl ($1, $3, None))} 
423 
 node_ident LPAR expr RPAR EVERY expr 
424 
{mkexpr (Expr_appl ($1, $3, Some $6))} 
425 
 node_ident LPAR tuple_expr RPAR 
426 
{ 
427 
let id=$1 in 
428 
let args=List.rev $3 in 
429 
match id, args with 
430 
 "fbyn", [expr;n;init] > 
431 
let n = match n.expr_desc with 
432 
 Expr_const (Const_int n) > n 
433 
 _ > assert false 
434 
in 
435 
fby expr n init 
436 
 _ > mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None)) 
437 
} 
438 
 node_ident LPAR tuple_expr RPAR EVERY expr 
439 
{ 
440 
let id=$1 in 
441 
let args=List.rev $3 in 
442 
let clock=$6 in 
443 
if id="fby" then 
444 
assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *) 
445 
else 
446 
mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 
447 
} 
448  
449 
/* Boolean expr */ 
450 
 expr AND expr 
451 
{mkpredef_call "&&" [$1;$3]} 
452 
 expr AMPERAMPER expr 
453 
{mkpredef_call "&&" [$1;$3]} 
454 
 expr OR expr 
455 
{mkpredef_call "" [$1;$3]} 
456 
 expr BARBAR expr 
457 
{mkpredef_call "" [$1;$3]} 
458 
 expr XOR expr 
459 
{mkpredef_call "xor" [$1;$3]} 
460 
 NOT expr 
461 
{mkpredef_call "not" [$2]} 
462 
 expr IMPL expr 
463 
{mkpredef_call "impl" [$1;$3]} 
464  
465 
/* Comparison expr */ 
466 
 expr EQ expr 
467 
{mkpredef_call "=" [$1;$3]} 
468 
 expr LT expr 
469 
{mkpredef_call "<" [$1;$3]} 
470 
 expr LTE expr 
471 
{mkpredef_call "<=" [$1;$3]} 
472 
 expr GT expr 
473 
{mkpredef_call ">" [$1;$3]} 
474 
 expr GTE expr 
475 
{mkpredef_call ">=" [$1;$3]} 
476 
 expr NEQ expr 
477 
{mkpredef_call "!=" [$1;$3]} 
478  
479 
/* Arithmetic expr */ 
480 
 expr PLUS expr 
481 
{mkpredef_call "+" [$1;$3]} 
482 
 expr MINUS expr 
483 
{mkpredef_call "" [$1;$3]} 
484 
 expr MULT expr 
485 
{mkpredef_call "*" [$1;$3]} 
486 
 expr DIV expr 
487 
{mkpredef_call "/" [$1;$3]} 
488 
 MINUS expr %prec UMINUS 
489 
{mkpredef_call "uminus" [$2]} 
490 
 expr MOD expr 
491 
{mkpredef_call "mod" [$1;$3]} 
492  
493 
/* If */ 
494 
 IF expr THEN expr ELSE expr 
495 
{mkexpr (Expr_ite ($2, $4, $6))} 
496  
497 
handler_expr_list: 
498 
{ [] } 
499 
 handler_expr handler_expr_list { $1 :: $2 } 
500  
501 
handler_expr: 
502 
LPAR tag_ident ARROW expr RPAR { ($2, $4) } 
503  
504 
signed_const_array: 
505 
 signed_const { [$1] } 
506 
 signed_const COMMA signed_const_array { $1 :: $3 } 
507  
508 
signed_const_struct: 
509 
 IDENT EQ signed_const { [ ($1, $3) ] } 
510 
 IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 } 
511  
512 
signed_const: 
513 
INT {Const_int $1} 
514 
 REAL {let c,e,s =$1 in Const_real (c,e,s)} 
515 
/*  FLOAT {Const_float $1} */ 
516 
 tag_ident {Const_tag $1} 
517 
 MINUS INT {Const_int (1 * $2)} 
518 
 MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "" ^ s)} 
519 
/*  MINUS FLOAT {Const_float (1. *. $2)} */ 
520 
 LCUR signed_const_struct RCUR { Const_struct $2 } 
521 
 LBRACKET signed_const_array RBRACKET { Const_array $2 } 
522  
523 
dim: 
524 
INT { mkdim_int $1 } 
525 
 LPAR dim RPAR { $2 } 
526 
 UIDENT { mkdim_ident $1 } 
527 
 IDENT { mkdim_ident $1 } 
528 
 dim AND dim 
529 
{mkdim_appl "&&" [$1;$3]} 
530 
 dim AMPERAMPER dim 
531 
{mkdim_appl "&&" [$1;$3]} 
532 
 dim OR dim 
533 
{mkdim_appl "" [$1;$3]} 
534 
 dim BARBAR dim 
535 
{mkdim_appl "" [$1;$3]} 
536 
 dim XOR dim 
537 
{mkdim_appl "xor" [$1;$3]} 
538 
 NOT dim 
539 
{mkdim_appl "not" [$2]} 
540 
 dim IMPL dim 
541 
{mkdim_appl "impl" [$1;$3]} 
542  
543 
/* Comparison dim */ 
544 
 dim EQ dim 
545 
{mkdim_appl "=" [$1;$3]} 
546 
 dim LT dim 
547 
{mkdim_appl "<" [$1;$3]} 
548 
 dim LTE dim 
549 
{mkdim_appl "<=" [$1;$3]} 
550 
 dim GT dim 
551 
{mkdim_appl ">" [$1;$3]} 
552 
 dim GTE dim 
553 
{mkdim_appl ">=" [$1;$3]} 
554 
 dim NEQ dim 
555 
{mkdim_appl "!=" [$1;$3]} 
556  
557 
/* Arithmetic dim */ 
558 
 dim PLUS dim 
559 
{mkdim_appl "+" [$1;$3]} 
560 
 dim MINUS dim 
561 
{mkdim_appl "" [$1;$3]} 
562 
 dim MULT dim 
563 
{mkdim_appl "*" [$1;$3]} 
564 
 dim DIV dim 
565 
{mkdim_appl "/" [$1;$3]} 
566 
 MINUS dim %prec UMINUS 
567 
{mkdim_appl "uminus" [$2]} 
568 
 dim MOD dim 
569 
{mkdim_appl "mod" [$1;$3]} 
570 
/* If */ 
571 
 IF dim THEN dim ELSE dim 
572 
{mkdim_ite $2 $4 $6} 
573  
574 
locals: 
575 
{[]} 
576 
 VAR local_vdecl_list SCOL {$2} 
577  
578 
vdecl_list: 
579 
vdecl {$1} 
580 
 vdecl_list SCOL vdecl {$3 @ $1} 
581  
582 
vdecl: 
583 
ident_list COL typeconst clock 
584 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 } 
585 
 CONST ident_list /* static parameters don't have clocks */ 
586 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 } 
587 
 CONST ident_list COL typeconst /* static parameters don't have clocks */ 
588 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 } 
589  
590 
local_vdecl_list: 
591 
local_vdecl {$1} 
592 
 local_vdecl_list SCOL local_vdecl {$3 @ $1} 
593  
594 
local_vdecl: 
595 
/* Useless no ?*/ ident_list 
596 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 } 
597 
 ident_list COL typeconst clock 
598 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 } 
599 
 CONST vdecl_ident EQ expr /* static parameters don't have clocks */ 
600 
{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] } 
601 
 CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */ 
602 
{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] } 
603  
604 
cdecl_list: 
605 
cdecl SCOL { (fun itf > [$1 itf]) } 
606 
 cdecl cdecl_list SCOL { (fun itf > let c1 = ($1 itf) in c1::($2 itf)) } 
607  
608 
cdecl: 
609 
const_ident EQ signed_const { 
610 
(fun itf > 
611 
let c = mktop_decl itf (Const { 
612 
const_id = $1; 
613 
const_loc = Location.symbol_rloc (); 
614 
const_type = Types.new_var (); 
615 
const_value = $3}) 
616 
in 
617 
(*add_const itf $1 c;*) c) 
618 
} 
619  
620 
clock: 
621 
{mkclock Ckdec_any} 
622 
 when_list 
623 
{mkclock (Ckdec_bool (List.rev $1))} 
624  
625 
when_cond: 
626 
WHEN IDENT {($2, tag_true)} 
627 
 WHENNOT IDENT {($2, tag_false)} 
628 
 WHEN tag_ident LPAR IDENT RPAR {($4, $2)} 
629  
630 
when_list: 
631 
when_cond {[$1]} 
632 
 when_list when_cond {$2::$1} 
633  
634 
ident_list: 
635 
vdecl_ident {[$1]} 
636 
 ident_list COMMA vdecl_ident {$3::$1} 
637  
638 
SCOL_opt: 
639 
SCOL {}  {} 
640  
641  
642 
lustre_annot: 
643 
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } } 
644  
645 
lustre_annot_list: 
646 
{ [] } 
647 
 kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 } 
648 
 IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 } 
649 
 INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } 
650 
 OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } 
651 
 CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 } 
652 
 MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 } 
653  
654  
655 
kwd: 
656 
DIV { [] } 
657 
 DIV IDENT kwd { $2::$3} 
658  
659 
%% 
660 
(* Local Variables: *) 
661 
(* compilecommand:"make C .." *) 
662 
(* End: *) 
663  
664 