Revision 1ac315e3 src/parser_lustre.mly
src/parser_lustre.mly  

23  23 
let mkclock x = mkclock (get_loc ()) x 
24  24 
let mkvar_decl x loc = mkvar_decl loc ~orig:true x 
25  25 
let mkexpr x = mkexpr (get_loc ()) x 
26 
let mkeexpr x = mkeexpr (get_loc ()) x


26 
let mkeexpr x = mkeexpr (get_loc ()) x 

27  27 
let mkeq x = mkeq (get_loc ()) x 
28  28 
let mkassert x = mkassert (get_loc ()) x 
29  29 
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x 
...  ...  
49  49 
mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr))) 
50  50 
else 
51  51 
mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n1) init)))) 
52 


52  
53  53 
%} 
54  54  
55  55 
%token <int> INT 
56  56 
%token <Num.num * int * string> REAL 
57  57  
58  58 
%token <string> STRING 
59 
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME


59 
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME 

60  60 
%token ASSERT OPEN QUOTE FUNCTION 
61  61 
%token <string> IDENT 
62  62 
%token <string> UIDENT 
63  63 
%token TRUE FALSE 
64  64 
%token <Lustre_types.expr_annot> ANNOT 
65  65 
%token <Lustre_types.contract_desc> NODESPEC 
66 
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 

66 
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA 

67 
/* unused token? */ 

68 
%token COLCOL 

67  69 
%token AMPERAMPER BARBAR NOT POWER 
68  70 
%token IF THEN ELSE 
69  71 
%token MERGE FBY WHEN WHENNOT EVERY 
70 
%token NODE LET TEL RETURNS VAR IMPORTED TYPE CONST 

72 
%token NODE LET TEL RETURNS VAR TYPE CONST 

73 
/* unused token? */ 

74 
%token IMPORTED 

71  75 
%token STRUCT ENUM 
72  76 
%token TINT TREAL TBOOL TCLOCK 
73  77 
%token EQ LT GT LTE GTE NEQ 
...  ...  
82  86 
%token EOF 
83  87  
84  88 
%nonassoc prec_exists prec_forall 
89 
/* unused precedence rules*/ 

90 
/* 

85  91 
%nonassoc COMMA 
92 
*/ 

86  93 
%nonassoc EVERY 
94 
/* unused precedence rules 

87  95 
%left MERGE IF 
96 
*/ 

88  97 
%nonassoc ELSE 
89  98 
%right ARROW FBY 
90 
%left WHEN WHENNOT 

99 
%left WHEN WHENNOT 

100 
/* unused token 

91  101 
%right COLCOL 
102 
*/ 

92  103 
%right IMPL 
93  104 
%left OR XOR BARBAR 
94  105 
%left AND AMPERAMPER 
95  106 
%left NOT 
107 
/* unused precedence rule 

96  108 
%nonassoc INT 
109 
*/ 

97  110 
%nonassoc EQ LT GT LTE GTE NEQ 
98  111 
%left MINUS PLUS 
99  112 
%left MULT DIV MOD 
100  113 
%left UMINUS 
101  114 
%left POWER 
102 
%left PRE LAST


115 
%left PRE 

103  116 
%nonassoc RBRACKET 
104  117 
%nonassoc LBRACKET 
105  118  
...  ...  
210  223  
211  224 
in_lib_list: 
212  225 
{ [] } 
213 
 LIB module_ident in_lib_list { $2::$3 }


226 
 LIB module_ident in_lib_list { $2::$3 } 

214  227  
215  228 
top_decl: 
216  229 
 CONST cdecl_list { List.rev ($2 false) } 
217 
 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


230 
 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 

218  231 
{ 
219  232 
let stmts, asserts, annots = $16 in 
220  233 
(* Declaring eqs annots *) 
221 
List.iter (fun ann >


222 
List.iter (fun (key, _) >


234 
List.iter (fun ann > 

235 
List.iter (fun (key, _) > 

223  236 
Annotations.add_node_ann $3 key 
224  237 
) ann.annots 
225  238 
) annots; 
...  ...  
233  246 
node_locals = List.rev $14; 
234  247 
node_gencalls = []; 
235  248 
node_checks = []; 
236 
node_asserts = asserts;


249 
node_asserts = asserts; 

237  250 
node_stmts = stmts; 
238  251 
node_dec_stateless = $2; 
239  252 
node_stateless = None; 
...  ...  
245  258  
246  259 
nodespec_list: 
247  260 
{ None } 
248 
 NODESPEC nodespec_list {


249 
(function


250 
 None > (fun s1 > Some s1)


261 
 NODESPEC nodespec_list { 

262 
(function 

263 
 None > (fun s1 > Some s1) 

251  264 
 Some s2 > (fun s1 > Some (merge_contracts s1 s2))) $2 $1 } 
252  265  
253  266 
typ_def_list: 
...  ...  
282  295 
tag_list: 
283  296 
UIDENT { $1 :: [] } 
284  297 
 tag_list COMMA UIDENT { $3 :: $1 } 
285 


298  
286  299 
field_list: { [] } 
287  300 
 field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 } 
288 


301  
289  302 
stmt_list: 
290  303 
{ [], [], [] } 
291  304 
 eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl} 
...  ...  
331  344  
332  345 
contract: 
333  346 
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } } 
334 


347  
335  348 
requires: 
336  349 
{ [] } 
337  350 
 REQUIRES qexpr SCOL requires { $2::$4 } 
...  ...  
339  352 
ensures: 
340  353 
{ [] } 
341  354 
 ENSURES qexpr SCOL ensures { $2 :: $4 } 
342 
 OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures {


355 
 OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { 

343  356 
mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7 
344  357 
} 
345  358  
...  ...  
349  362  
350  363 
assumes: 
351  364 
{ [] } 
352 
 ASSUMES qexpr SCOL assumes { $2::$4 }


365 
 ASSUMES qexpr SCOL assumes { $2::$4 } 

353  366  
354 
/* WARNING: UNUSED RULES */ 

367 
/* WARNING: UNREACHABLE RULE */ 

368 
/* 

355  369 
tuple_qexpr: 
356  370 
 qexpr COMMA qexpr {[$3;$1]} 
357  371 
 tuple_qexpr COMMA qexpr {$3::$1} 
372 
*/ 

373 
/* END OF UNREACHABLE RULE */ 

358  374  
359  375 
qexpr: 
360  376 
 expr { mkeexpr $1 } 
361 
/* Quantifiers */ 

362 
 EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 

377 
 EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 

363  378 
 FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 } 
364  379  
365  
366  380 
tuple_expr: 
367 
expr COMMA expr {[$3;$1]}


381 
expr COMMA expr {[$3;$1]} 

368  382 
 tuple_expr COMMA expr {$3::$1} 
369  383  
370  384 
// Same as tuple expr but accepting lists with single element 
...  ...  
399  413 
 expr LBRACKET dim_list { $3 $1 } 
400  414  
401  415 
/* Temporal operators */ 
402 
 PRE expr


416 
 PRE expr 

403  417 
{mkexpr (Expr_pre $2)} 
404 
 expr ARROW expr


418 
 expr ARROW expr 

405  419 
{mkexpr (Expr_arrow ($1,$3))} 
406 
 expr FBY expr


420 
 expr FBY expr 

407  421 
{(*mkexpr (Expr_fby ($1,$3))*) 
408  422 
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} 
409  423 
 expr WHEN vdecl_ident 
...  ...  
441  455 
if id="fby" then 
442  456 
assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *) 
443  457 
else 
444 
mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock))


458 
mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 

445  459 
} 
446  460  
447  461 
/* Boolean expr */ 
448 
 expr AND expr


462 
 expr AND expr 

449  463 
{mkpredef_call "&&" [$1;$3]} 
450 
 expr AMPERAMPER expr


464 
 expr AMPERAMPER expr 

451  465 
{mkpredef_call "&&" [$1;$3]} 
452 
 expr OR expr


466 
 expr OR expr 

453  467 
{mkpredef_call "" [$1;$3]} 
454 
 expr BARBAR expr


468 
 expr BARBAR expr 

455  469 
{mkpredef_call "" [$1;$3]} 
456 
 expr XOR expr


470 
 expr XOR expr 

457  471 
{mkpredef_call "xor" [$1;$3]} 
458 
 NOT expr


472 
 NOT expr 

459  473 
{mkpredef_call "not" [$2]} 
460 
 expr IMPL expr


474 
 expr IMPL expr 

461  475 
{mkpredef_call "impl" [$1;$3]} 
462  476  
463  477 
/* Comparison expr */ 
464 
 expr EQ expr


478 
 expr EQ expr 

465  479 
{mkpredef_call "=" [$1;$3]} 
466 
 expr LT expr


480 
 expr LT expr 

467  481 
{mkpredef_call "<" [$1;$3]} 
468 
 expr LTE expr


482 
 expr LTE expr 

469  483 
{mkpredef_call "<=" [$1;$3]} 
470 
 expr GT expr


484 
 expr GT expr 

471  485 
{mkpredef_call ">" [$1;$3]} 
472 
 expr GTE expr


486 
 expr GTE expr 

473  487 
{mkpredef_call ">=" [$1;$3]} 
474 
 expr NEQ expr


488 
 expr NEQ expr 

475  489 
{mkpredef_call "!=" [$1;$3]} 
476  490  
477  491 
/* Arithmetic expr */ 
478 
 expr PLUS expr


492 
 expr PLUS expr 

479  493 
{mkpredef_call "+" [$1;$3]} 
480 
 expr MINUS expr


494 
 expr MINUS expr 

481  495 
{mkpredef_call "" [$1;$3]} 
482 
 expr MULT expr


496 
 expr MULT expr 

483  497 
{mkpredef_call "*" [$1;$3]} 
484 
 expr DIV expr


498 
 expr DIV expr 

485  499 
{mkpredef_call "/" [$1;$3]} 
486  500 
 MINUS expr %prec UMINUS 
487  501 
{mkpredef_call "uminus" [$2]} 
488 
 expr MOD expr


502 
 expr MOD expr 

489  503 
{mkpredef_call "mod" [$1;$3]} 
490  504  
491  505 
/* If */ 
...  ...  
523  537 
 LPAR dim RPAR { $2 } 
524  538 
 UIDENT { mkdim_ident $1 } 
525  539 
 IDENT { mkdim_ident $1 } 
526 
 dim AND dim


540 
 dim AND dim 

527  541 
{mkdim_appl "&&" [$1;$3]} 
528 
 dim AMPERAMPER dim


542 
 dim AMPERAMPER dim 

529  543 
{mkdim_appl "&&" [$1;$3]} 
530 
 dim OR dim


544 
 dim OR dim 

531  545 
{mkdim_appl "" [$1;$3]} 
532 
 dim BARBAR dim


546 
 dim BARBAR dim 

533  547 
{mkdim_appl "" [$1;$3]} 
534 
 dim XOR dim


548 
 dim XOR dim 

535  549 
{mkdim_appl "xor" [$1;$3]} 
536 
 NOT dim


550 
 NOT dim 

537  551 
{mkdim_appl "not" [$2]} 
538 
 dim IMPL dim


552 
 dim IMPL dim 

539  553 
{mkdim_appl "impl" [$1;$3]} 
540  554  
541  555 
/* Comparison dim */ 
542 
 dim EQ dim


556 
 dim EQ dim 

543  557 
{mkdim_appl "=" [$1;$3]} 
544 
 dim LT dim


558 
 dim LT dim 

545  559 
{mkdim_appl "<" [$1;$3]} 
546 
 dim LTE dim


560 
 dim LTE dim 

547  561 
{mkdim_appl "<=" [$1;$3]} 
548 
 dim GT dim


562 
 dim GT dim 

549  563 
{mkdim_appl ">" [$1;$3]} 
550 
 dim GTE dim


564 
 dim GTE dim 

551  565 
{mkdim_appl ">=" [$1;$3]} 
552 
 dim NEQ dim


566 
 dim NEQ dim 

553  567 
{mkdim_appl "!=" [$1;$3]} 
554  568  
555  569 
/* Arithmetic dim */ 
556 
 dim PLUS dim


570 
 dim PLUS dim 

557  571 
{mkdim_appl "+" [$1;$3]} 
558 
 dim MINUS dim


572 
 dim MINUS dim 

559  573 
{mkdim_appl "" [$1;$3]} 
560 
 dim MULT dim


574 
 dim MULT dim 

561  575 
{mkdim_appl "*" [$1;$3]} 
562 
 dim DIV dim


576 
 dim DIV dim 

563  577 
{mkdim_appl "/" [$1;$3]} 
564  578 
 MINUS dim %prec UMINUS 
565  579 
{mkdim_appl "uminus" [$2]} 
566 
 dim MOD dim


580 
 dim MOD dim 

567  581 
{mkdim_appl "mod" [$1;$3]} 
568  582 
/* If */ 
569  583 
 IF dim THEN dim ELSE dim 
...  ...  
578  592 
 vdecl_list SCOL vdecl {$3 @ $1} 
579  593  
580  594 
vdecl: 
581 
ident_list COL typeconst clock


595 
ident_list COL typeconst clock 

582  596 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 } 
583  597 
 CONST ident_list /* static parameters don't have clocks */ 
584  598 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 } 
...  ...  
592  606 
local_vdecl: 
593  607 
/* Useless no ?*/ ident_list 
594  608 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 } 
595 
 ident_list COL typeconst clock


609 
 ident_list COL typeconst clock 

596  610 
{ List.map (fun (id, loc) > mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 } 
597  611 
 CONST vdecl_ident EQ expr /* static parameters don't have clocks */ 
598  612 
{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] } 
...  ...  
605  619  
606  620 
cdecl: 
607  621 
const_ident EQ signed_const { 
608 
(fun itf >


622 
(fun itf > 

609  623 
let c = mktop_decl itf (Const { 
610  624 
const_id = $1; 
611  625 
const_loc = Location.symbol_rloc (); 
...  ...  
641  655 
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } } 
642  656  
643  657 
lustre_annot_list: 
644 
{ [] }


658 
{ [] } 

645  659 
 kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 } 
646  660 
 IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 } 
647  661 
 INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } 
...  ...  
658  672 
(* Local Variables: *) 
659  673 
(* compilecommand:"make C .." *) 
660  674 
(* End: *) 
661  
662 
Also available in: Unified diff