Project

General

Profile

Revision 1ac315e3

View differences:

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 (n-1) 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
(* compile-command:"make -C .." *)
660 674
(* End: *)
661

  
662

  

Also available in: Unified diff