Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 01d48bb0

History | View | Annotate | Download (17 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 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 ()) ~orig:true 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
let node_stack : ident list ref = ref []
41
let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack
42
let push_node nd =  node_stack:= nd :: !node_stack
43
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
44
let get_current_node () = try List.hd !node_stack with _ -> assert false
45

    
46
%}
47

    
48
%token <int> INT
49
%token <string> REAL
50
%token <float> FLOAT
51
%token <string> STRING
52
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
53
%token STATELESS ASSERT OPEN QUOTE FUNCTION
54
%token <string> IDENT
55
%token <string> UIDENT
56
%token TRUE FALSE
57
%token <LustreSpec.expr_annot> ANNOT
58
%token <LustreSpec.node_annot> NODESPEC
59
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
60
%token AMPERAMPER BARBAR NOT POWER
61
%token IF THEN ELSE
62
%token UCLOCK DCLOCK PHCLOCK TAIL
63
%token MERGE FBY WHEN WHENNOT EVERY
64
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
65
%token STRUCT ENUM
66
%token TINT TFLOAT TREAL TBOOL TCLOCK
67
%token RATE DUE
68
%token EQ LT GT LTE GTE NEQ
69
%token AND OR XOR IMPL
70
%token MULT DIV MOD
71
%token MINUS PLUS UMINUS
72
%token PRE ARROW
73
%token REQUIRES ENSURES OBSERVER
74
%token INVARIANT BEHAVIOR ASSUMES
75
%token EXISTS FORALL
76
%token PROTOTYPE LIB
77
%token EOF
78

    
79
%nonassoc prec_exists prec_forall
80
%nonassoc COMMA
81
%nonassoc EVERY
82
%left MERGE IF
83
%nonassoc ELSE
84
%right ARROW FBY
85
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
86
%right COLCOL
87
%right IMPL
88
%left OR XOR BARBAR
89
%left AND AMPERAMPER
90
%left NOT
91
%nonassoc INT
92
%nonassoc EQ LT GT LTE GTE NEQ
93
%left MINUS PLUS
94
%left MULT DIV MOD
95
%left UMINUS
96
%left POWER
97
%left PRE LAST
98
%nonassoc RBRACKET
99
%nonassoc LBRACKET
100

    
101
%start prog
102
%type <LustreSpec.top_decl list> prog
103

    
104
%start header
105
%type <LustreSpec.top_decl list> header
106

    
107
%start lustre_annot
108
%type <LustreSpec.expr_annot> lustre_annot
109

    
110
%start lustre_spec
111
%type <LustreSpec.node_annot> lustre_spec
112

    
113
%%
114

    
115
module_ident:
116
  UIDENT { $1 }
117
| IDENT  { $1 }
118

    
119
tag_ident:
120
  UIDENT  { $1 }
121
| TRUE    { tag_true }
122
| FALSE   { tag_false }
123

    
124
node_ident:
125
  UIDENT { $1 }
126
| IDENT  { $1 }
127

    
128
node_ident_decl:
129
 node_ident { push_node $1; $1 }
130

    
131
vdecl_ident:
132
  UIDENT { $1 }
133
| IDENT  { $1 }
134

    
135
const_ident:
136
  UIDENT { $1 }
137
| IDENT  { $1 }
138

    
139
type_ident:
140
  IDENT { $1 }
141

    
142
prog:
143
 open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
144

    
145
typ_def_prog:
146
 typ_def_list { $1 false }
147

    
148
header:
149
 open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) }
150

    
151
typ_def_header:
152
 typ_def_list { $1 true }
153

    
154
open_list:
155
  { [] }
156
| open_lusi open_list { $1 :: $2 }
157

    
158
open_lusi:
159
| OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))}
160
| OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) }
161

    
162
top_decl_list:
163
   {[]}
164
| top_decl_list top_decl {$2@$1}
165

    
166

    
167
top_decl_header_list:
168
   { [] }
169
| top_decl_header_list top_decl_header { $2@$1 }
170

    
171
state_annot:
172
  FUNCTION { true }
173
| NODE { false }
174

    
175
top_decl_header:
176
| CONST cdecl_list { List.rev ($2 true) }
177
| 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
178
    {let nd = mktop_decl true (ImportedNode
179
				 {nodei_id = $3;
180
				  nodei_type = Types.new_var ();
181
				  nodei_clock = Clocks.new_var true;
182
				  nodei_inputs = List.rev $5;
183
				  nodei_outputs = List.rev $10;
184
				  nodei_stateless = $2;
185
				  nodei_spec = $1;
186
				  nodei_prototype = $13;
187
				  nodei_in_lib = $14;})
188
     in
189
     (*add_imported_node $3 nd;*) [nd] }
190

    
191
prototype_opt:
192
 { None }
193
| PROTOTYPE node_ident { Some $2}
194

    
195
in_lib_opt:
196
{ None }
197
| LIB module_ident {Some $2} 
198

    
199
top_decl:
200
| CONST cdecl_list { List.rev ($2 false) }
201
| 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 
202
    {
203
      let stmts, asserts, annots = $16 in
204
      (* Declaring eqs annots *)
205
      List.iter (fun ann -> 
206
	List.iter (fun (key, _) -> 
207
	  Annotations.add_node_ann $3 key
208
	) ann.annots
209
      ) annots;
210
     (* Building the node *)
211
      let nd = mktop_decl false (Node
212
				   {node_id = $3;
213
				    node_type = Types.new_var ();
214
				    node_clock = Clocks.new_var true;
215
				    node_inputs = List.rev $5;
216
				    node_outputs = List.rev $10;
217
				    node_locals = List.rev $14;
218
				    node_gencalls = [];
219
				    node_checks = [];
220
				    node_asserts = asserts; 
221
				    node_stmts = stmts;
222
				    node_dec_stateless = $2;
223
				    node_stateless = None;
224
				    node_spec = $1;
225
				    node_annot = annots})
226
      in
227
      pop_node ();
228
     (*add_node $3 nd;*) [nd] }
229
    
230
 nodespec_list:
231
 { None }
232
| NODESPEC nodespec_list { 
233
  (function 
234
  | None    -> (fun s1 -> Some s1) 
235
  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
236

    
237
typ_def_list:
238
    /* empty */             { (fun itf -> []) }
239
| typ_def SCOL typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($3 itf)) }
240

    
241
typ_def:
242
  TYPE type_ident EQ typ_def_rhs { (fun itf ->
243
			       let typ = mktop_decl itf (TypeDef { tydef_id = $2;
244
								   tydef_desc = $4
245
							})
246
			       in (*add_type itf $2 typ;*) typ) }
247

    
248
typ_def_rhs:
249
  typeconst                   { $1 }
250
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }
251
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
252

    
253
array_typ_decl:
254
                            { fun typ -> typ }
255
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
256

    
257
typeconst:
258
  TINT array_typ_decl   { $2 Tydec_int }
259
| TBOOL array_typ_decl  { $2 Tydec_bool  }
260
| TREAL array_typ_decl  { $2 Tydec_real  }
261
| TFLOAT array_typ_decl { $2 Tydec_float }
262
| type_ident array_typ_decl  { $2 (Tydec_const $1) }
263
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }
264
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }
265

    
266
tag_list:
267
  UIDENT                { $1 :: [] }
268
| tag_list COMMA UIDENT { $3 :: $1 }
269
      
270
field_list:                           { [] }
271
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
272
      
273
stmt_list:
274
  { [], [], [] }
275
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
276
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
277
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
278
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
279

    
280
automaton:
281
 AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }
282

    
283
handler_list:
284
     { [] }
285
| handler handler_list { $1::$2 }
286

    
287
handler:
288
 STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
289

    
290
unless_list:
291
    { [] }
292
| unless unless_list { $1::$2 }
293

    
294
until_list:
295
    { [] }
296
| until until_list { $1::$2 }
297

    
298
unless:
299
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
300
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
301

    
302
until:
303
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
304
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
305

    
306
assert_:
307
| ASSERT expr SCOL {mkassert ($2)}
308

    
309
eq:
310
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
311
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
312

    
313
lustre_spec:
314
| contract EOF { $1 }
315

    
316
contract:
317
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
318
 
319
requires:
320
{ [] }
321
| REQUIRES qexpr SCOL requires { $2::$4 }
322

    
323
ensures:
324
{ [] }
325
| ENSURES qexpr SCOL ensures { $2 :: $4 }
326
| OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { 
327
  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
328
}
329

    
330
behaviors:
331
{ [] }
332
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
333

    
334
assumes:
335
{ [] }
336
| ASSUMES qexpr SCOL assumes { $2::$4 } 
337

    
338
/* WARNING: UNUSED RULES */
339
tuple_qexpr:
340
| qexpr COMMA qexpr {[$3;$1]}
341
| tuple_qexpr COMMA qexpr {$3::$1}
342

    
343
qexpr:
344
| expr { mkeexpr $1 }
345
  /* Quantifiers */
346
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
347
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
348

    
349

    
350
tuple_expr:
351
    expr COMMA expr {[$3;$1]}
352
| tuple_expr COMMA expr {$3::$1}
353

    
354
// Same as tuple expr but accepting lists with single element
355
array_expr:
356
  expr {[$1]}
357
| expr COMMA array_expr {$1::$3}
358

    
359
dim_list:
360
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
361
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
362

    
363
expr:
364
/* constants */
365
  INT {mkexpr (Expr_const (Const_int $1))}
366
| REAL {mkexpr (Expr_const (Const_real $1))}
367
| FLOAT {mkexpr (Expr_const (Const_float $1))}
368
/* Idents or type enum tags */
369
| IDENT { mkexpr (Expr_ident $1) }
370
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
371
| LPAR ANNOT expr RPAR
372
    {update_expr_annot (get_current_node ()) $3 $2}
373
| LPAR expr RPAR
374
    {$2}
375
| LPAR tuple_expr RPAR
376
    {mkexpr (Expr_tuple (List.rev $2))}
377

    
378
/* Array expressions */
379
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
380
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
381
| expr LBRACKET dim_list { $3 $1 }
382

    
383
/* Temporal operators */
384
| PRE expr 
385
    {mkexpr (Expr_pre $2)}
386
| expr ARROW expr 
387
    {mkexpr (Expr_arrow ($1,$3))}
388
| expr FBY expr 
389
    {(*mkexpr (Expr_fby ($1,$3))*)
390
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
391
| expr WHEN vdecl_ident
392
    {mkexpr (Expr_when ($1,$3,tag_true))}
393
| expr WHENNOT vdecl_ident
394
    {mkexpr (Expr_when ($1,$3,tag_false))}
395
| expr WHEN tag_ident LPAR vdecl_ident RPAR
396
    {mkexpr (Expr_when ($1, $5, $3))}
397
| MERGE vdecl_ident handler_expr_list
398
    {mkexpr (Expr_merge ($2,$3))}
399

    
400
/* Applications */
401
| node_ident LPAR expr RPAR
402
    {mkexpr (Expr_appl ($1, $3, None))}
403
| node_ident LPAR expr RPAR EVERY expr
404
    {mkexpr (Expr_appl ($1, $3, Some $6))}
405
| node_ident LPAR tuple_expr RPAR
406
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
407
| node_ident LPAR tuple_expr RPAR EVERY expr
408
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some $6)) }
409

    
410
/* Boolean expr */
411
| expr AND expr 
412
    {mkpredef_call "&&" [$1;$3]}
413
| expr AMPERAMPER expr 
414
    {mkpredef_call "&&" [$1;$3]}
415
| expr OR expr 
416
    {mkpredef_call "||" [$1;$3]}
417
| expr BARBAR expr 
418
    {mkpredef_call "||" [$1;$3]}
419
| expr XOR expr 
420
    {mkpredef_call "xor" [$1;$3]}
421
| NOT expr 
422
    {mkpredef_call "not" [$2]}
423
| expr IMPL expr 
424
    {mkpredef_call "impl" [$1;$3]}
425

    
426
/* Comparison expr */
427
| expr EQ expr 
428
    {mkpredef_call "=" [$1;$3]}
429
| expr LT expr 
430
    {mkpredef_call "<" [$1;$3]}
431
| expr LTE expr 
432
    {mkpredef_call "<=" [$1;$3]}
433
| expr GT expr 
434
    {mkpredef_call ">" [$1;$3]}
435
| expr GTE  expr 
436
    {mkpredef_call ">=" [$1;$3]}
437
| expr NEQ expr 
438
    {mkpredef_call "!=" [$1;$3]}
439

    
440
/* Arithmetic expr */
441
| expr PLUS expr 
442
    {mkpredef_call "+" [$1;$3]}
443
| expr MINUS expr 
444
    {mkpredef_call "-" [$1;$3]}
445
| expr MULT expr 
446
    {mkpredef_call "*" [$1;$3]}
447
| expr DIV expr 
448
    {mkpredef_call "/" [$1;$3]}
449
| MINUS expr %prec UMINUS
450
  {mkpredef_call "uminus" [$2]}
451
| expr MOD expr 
452
    {mkpredef_call "mod" [$1;$3]}
453

    
454
/* If */
455
| IF expr THEN expr ELSE expr
456
    {mkexpr (Expr_ite ($2, $4, $6))}
457

    
458
handler_expr_list:
459
   { [] }
460
| handler_expr handler_expr_list { $1 :: $2 }
461

    
462
handler_expr:
463
 LPAR tag_ident ARROW expr RPAR { ($2, $4) }
464

    
465
signed_const_array:
466
| signed_const { [$1] }
467
| signed_const COMMA signed_const_array { $1 :: $3 }
468

    
469
signed_const_struct:
470
| IDENT EQ signed_const { [ ($1, $3) ] }
471
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
472

    
473
signed_const:
474
  INT {Const_int $1}
475
| REAL {Const_real $1}
476
| FLOAT {Const_float $1}
477
| tag_ident {Const_tag $1}
478
| MINUS INT {Const_int (-1 * $2)}
479
| MINUS REAL {Const_real ("-" ^ $2)}
480
| MINUS FLOAT {Const_float (-1. *. $2)}
481
| LCUR signed_const_struct RCUR { Const_struct $2 }
482
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
483

    
484
dim:
485
   INT { mkdim_int $1 }
486
| LPAR dim RPAR { $2 }
487
| UIDENT { mkdim_ident $1 }
488
| IDENT { mkdim_ident $1 }
489
| dim AND dim 
490
    {mkdim_appl "&&" [$1;$3]}
491
| dim AMPERAMPER dim 
492
    {mkdim_appl "&&" [$1;$3]}
493
| dim OR dim 
494
    {mkdim_appl "||" [$1;$3]}
495
| dim BARBAR dim 
496
    {mkdim_appl "||" [$1;$3]}
497
| dim XOR dim 
498
    {mkdim_appl "xor" [$1;$3]}
499
| NOT dim 
500
    {mkdim_appl "not" [$2]}
501
| dim IMPL dim 
502
    {mkdim_appl "impl" [$1;$3]}
503

    
504
/* Comparison dim */
505
| dim EQ dim 
506
    {mkdim_appl "=" [$1;$3]}
507
| dim LT dim 
508
    {mkdim_appl "<" [$1;$3]}
509
| dim LTE dim 
510
    {mkdim_appl "<=" [$1;$3]}
511
| dim GT dim 
512
    {mkdim_appl ">" [$1;$3]}
513
| dim GTE  dim 
514
    {mkdim_appl ">=" [$1;$3]}
515
| dim NEQ dim 
516
    {mkdim_appl "!=" [$1;$3]}
517

    
518
/* Arithmetic dim */
519
| dim PLUS dim 
520
    {mkdim_appl "+" [$1;$3]}
521
| dim MINUS dim 
522
    {mkdim_appl "-" [$1;$3]}
523
| dim MULT dim 
524
    {mkdim_appl "*" [$1;$3]}
525
| dim DIV dim 
526
    {mkdim_appl "/" [$1;$3]}
527
| MINUS dim %prec UMINUS
528
  {mkdim_appl "uminus" [$2]}
529
| dim MOD dim 
530
    {mkdim_appl "mod" [$1;$3]}
531
/* If */
532
| IF dim THEN dim ELSE dim
533
    {mkdim_ite $2 $4 $6}
534

    
535
locals:
536
  {[]}
537
| VAR local_vdecl_list SCOL {$2}
538

    
539
vdecl_list:
540
  vdecl {$1}
541
| vdecl_list SCOL vdecl {$3 @ $1}
542

    
543
vdecl:
544
  ident_list COL typeconst clock 
545
    { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false, None)) $1 }
546
| CONST ident_list /* static parameters don't have clocks */
547
    { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None)) $2 }
548
| CONST ident_list COL typeconst /* static parameters don't have clocks */
549
    { List.map (fun id -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None)) $2 }
550

    
551
local_vdecl_list:
552
  local_vdecl {$1}
553
| local_vdecl_list SCOL local_vdecl {$3 @ $1}
554

    
555
local_vdecl:
556
/* Useless no ?*/    ident_list
557
    { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None)) $1 }
558
| ident_list COL typeconst clock 
559
    { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false, None)) $1 }
560
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
561
    { [ mkvar_decl ($2, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) ] }
562
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
563
    { [ mkvar_decl ($2, mktyp $4, mkclock Ckdec_any, true, Some $6) ] }
564

    
565
cdecl_list:
566
  cdecl SCOL { (fun itf -> [$1 itf]) }
567
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
568

    
569
cdecl:
570
    const_ident EQ signed_const {
571
      (fun itf -> 
572
       let c = mktop_decl itf (Const {
573
				   const_id = $1;
574
				   const_loc = Location.symbol_rloc ();
575
				   const_type = Types.new_var ();
576
				   const_value = $3})
577
       in
578
       (*add_const itf $1 c;*) c)
579
    }
580

    
581
clock:
582
    {mkclock Ckdec_any}
583
| when_list
584
    {mkclock (Ckdec_bool (List.rev $1))}
585

    
586
when_cond:
587
  WHEN IDENT {($2, tag_true)}
588
| WHENNOT IDENT {($2, tag_false)}
589
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
590

    
591
when_list:
592
    when_cond {[$1]}
593
| when_list when_cond {$2::$1}
594

    
595
ident_list:
596
  vdecl_ident {[$1]}
597
| ident_list COMMA vdecl_ident {$3::$1}
598

    
599
SCOL_opt:
600
    SCOL {} | {}
601

    
602

    
603
lustre_annot:
604
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
605

    
606
lustre_annot_list:
607
  { [] } 
608
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
609
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
610
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
611
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
612

    
613
kwd:
614
DIV { [] }
615
| DIV IDENT kwd { $2::$3}
616

    
617
%%
618
(* Local Variables: *)
619
(* compile-command:"make -C .." *)
620
(* End: *)
621

    
622