Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 44bea83a

History | View | Annotate | Download (16.7 KB)

1
/* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- */
22

    
23
%{
24
open LustreSpec
25
open Corelang
26
open Dimension
27
open Utils
28

    
29
let get_loc () = Location.symbol_rloc ()
30
let mktyp x = mktyp (get_loc ()) x
31
let mkclock x = mkclock (get_loc ()) x
32
let mkvar_decl x = mkvar_decl (get_loc ()) x
33
let mkexpr x = mkexpr (get_loc ()) x
34
let mkeexpr x = mkeexpr (get_loc ()) x 
35
let mkeq x = mkeq (get_loc ()) x
36
let mkassert x = mkassert (get_loc ()) x
37
let mktop_decl x = mktop_decl (get_loc ()) x
38
let mkpredef_call x = mkpredef_call (get_loc ()) x
39
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
40

    
41
let mkdim_int i = mkdim_int (get_loc ()) i
42
let mkdim_bool b = mkdim_bool (get_loc ()) b
43
let mkdim_ident id = mkdim_ident (get_loc ()) id
44
let mkdim_appl f args = mkdim_appl (get_loc ()) f args
45
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
46

    
47
let mkannots annots = { annots = annots; annot_loc = get_loc () }
48

    
49
let add_node loc own msg hashtbl name value =
50
  try
51
    match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with
52
    | Node _        , ImportedNode _ when own   -> ()
53
    | ImportedNode _, _                         -> Hashtbl.add hashtbl name value
54
    | Node _        , _                         -> raise (Error (loc, Already_bound_symbol msg))
55
    | _                                         -> assert false
56
  with
57
    Not_found                                   -> Hashtbl.add hashtbl name value
58

    
59

    
60
let add_symbol loc msg hashtbl name value =
61
 if Hashtbl.mem hashtbl name
62
 then raise (Error (loc, Already_bound_symbol msg))
63
 else Hashtbl.add hashtbl name value
64

    
65
let check_symbol loc msg hashtbl name =
66
 if not (Hashtbl.mem hashtbl name)
67
 then raise (Error (loc, Unbound_symbol msg))
68
 else ()
69

    
70
let check_node_symbol msg name value =
71
 if Hashtbl.mem node_table name
72
 then () (* TODO: should we check the types here ? *)
73
 else Hashtbl.add node_table name value
74

    
75
%}
76

    
77
%token <int> INT
78
%token <string> REAL
79
%token <float> FLOAT
80
%token <string> STRING
81
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
82
%token STATELESS ASSERT OPEN QUOTE FUNCTION
83
%token <string> IDENT
84
%token <LustreSpec.expr_annot> ANNOT
85
%token <LustreSpec.node_annot> NODESPEC
86
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
87
%token AMPERAMPER BARBAR NOT POWER
88
%token IF THEN ELSE
89
%token UCLOCK DCLOCK PHCLOCK TAIL
90
%token MERGE FBY WHEN WHENNOT EVERY
91
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
92
%token STRUCT ENUM
93
%token TINT TFLOAT TREAL TBOOL TCLOCK
94
%token RATE DUE
95
%token EQ LT GT LTE GTE NEQ
96
%token AND OR XOR IMPL
97
%token MULT DIV MOD
98
%token MINUS PLUS UMINUS
99
%token PRE ARROW
100
%token REQUIRES ENSURES OBSERVER
101
%token INVARIANT BEHAVIOR ASSUMES
102
%token EXISTS FORALL
103
%token PROTOTYPE LIB
104
%token EOF
105

    
106
%nonassoc prec_exists prec_forall
107
%nonassoc COMMA
108
%left MERGE IF
109
%nonassoc ELSE
110
%right ARROW FBY
111
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
112
%right COLCOL
113
%right IMPL
114
%left OR XOR BARBAR
115
%left AND AMPERAMPER
116
%left NOT
117
%nonassoc INT
118
%nonassoc EQ LT GT LTE GTE NEQ
119
%left MINUS PLUS
120
%left MULT DIV MOD
121
%left UMINUS
122
%left POWER
123
%left PRE LAST
124
%nonassoc RBRACKET
125
%nonassoc LBRACKET
126

    
127
%start prog
128
%type <LustreSpec.top_decl list> prog
129

    
130
%start header
131
%type <bool -> LustreSpec.top_decl list> header
132

    
133
%start lustre_annot
134
%type <LustreSpec.expr_annot> lustre_annot
135

    
136
%start lustre_spec
137
%type <LustreSpec.node_annot> lustre_spec
138

    
139
%%
140

    
141
prog:
142
 open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }
143

    
144
header:
145
 open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ (List.rev ($3 own)))) }
146

    
147
open_list:
148
  { [] }
149
| open_lusi open_list { $1 :: $2 }
150

    
151
open_lusi:
152
| OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))}
153
| OPEN LT IDENT GT { mktop_decl (Open (false, $3)) }
154

    
155
top_decl_list:
156
  top_decl {[$1]}
157
| top_decl_list top_decl {$2::$1}
158

    
159

    
160
top_decl_header_list:
161
  top_decl_header {(fun own -> [$1 own]) }
162
| top_decl_header_list top_decl_header {(fun own -> ($2 own)::($1 own)) }
163

    
164
state_annot:
165
  FUNCTION { true }
166
| NODE { false }
167

    
168
top_decl_header:
169
| CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ -> top }
170
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_opt SCOL
171
    {let nd = mktop_decl (ImportedNode
172
                            {nodei_id = $3;
173
                             nodei_type = Types.new_var ();
174
                             nodei_clock = Clocks.new_var true;
175
                             nodei_inputs = List.rev $5;
176
                             nodei_outputs = List.rev $10;
177
			     nodei_stateless = $2;
178
			     nodei_spec = $1;
179
			     nodei_prototype = $13;
180
			     nodei_in_lib = $14;})
181
    in
182
     check_node_symbol ("node " ^ $3) $3 nd; 
183
     let loc = get_loc () in
184
     (fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) }
185

    
186
prototype_opt:
187
 { None }
188
| PROTOTYPE IDENT { Some $2}
189

    
190
in_lib_opt:
191
{ None }
192
| LIB IDENT {Some $2} 
193

    
194
top_decl:
195
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
196
| 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 
197
    {let eqs, asserts, annots = $16 in
198
     let nd = mktop_decl (Node
199
                            {node_id = $3;
200
                             node_type = Types.new_var ();
201
                             node_clock = Clocks.new_var true;
202
                             node_inputs = List.rev $5;
203
                             node_outputs = List.rev $10;
204
                             node_locals = List.rev $14;
205
			     node_gencalls = [];
206
			     node_checks = [];
207
			     node_asserts = asserts; 
208
                             node_eqs = eqs;
209
			     node_dec_stateless = $2;
210
			     node_stateless = None;
211
			     node_spec = $1;
212
			     node_annot = annots})
213
     in
214
     let loc = Location.symbol_rloc () in
215
     add_node loc true ("node " ^ $3) node_table $3 nd; nd}
216

    
217
nodespec_list:
218
 { None }
219
| NODESPEC nodespec_list { 
220
  (function 
221
  | None    -> (fun s1 -> Some s1) 
222
  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
223

    
224
typ_def_list:
225
    /* empty */ {}
226
| typ_def SCOL typ_def_list {$1;$3}
227

    
228
typ_def:
229
  TYPE IDENT EQ typeconst {
230
    try
231
      let loc = Location.symbol_rloc () in
232
      add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (get_repr_type $4)
233
    with Not_found-> assert false }
234
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
235
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) }
236

    
237
array_typ_decl:
238
                            { fun typ -> typ }
239
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
240

    
241
typeconst:
242
  TINT array_typ_decl  { $2 Tydec_int }
243
| TBOOL array_typ_decl { $2 Tydec_bool  }
244
| TREAL array_typ_decl { $2 Tydec_real  }
245
| TFLOAT array_typ_decl { $2 Tydec_float }
246
| IDENT array_typ_decl { 
247
        let loc = Location.symbol_rloc () in
248
	check_symbol loc ("type " ^ $1) type_table (Tydec_const $1); $2 (Tydec_const $1) }
249
| TBOOL TCLOCK  { Tydec_clock Tydec_bool }
250
| IDENT TCLOCK  { Tydec_clock (Tydec_const $1) }
251

    
252
tag_list:
253
  IDENT
254
  { let loc = Location.symbol_rloc () in 
255
    (fun t -> 
256
      add_symbol loc ("tag " ^ $1) tag_table $1 t; $1 :: []) }
257
| tag_list COMMA IDENT
258
      {       
259
	let loc = Location.symbol_rloc () in
260
	(fun t -> add_symbol loc ("tag " ^ $3)tag_table $3 t; $3 :: ($1 t)) 
261
      }
262
      
263
field_list:
264
  { (fun t -> []) }
265
| field_list IDENT COL typeconst SCOL
266
      {
267
	let loc = Location.symbol_rloc () in
268
	(fun t -> add_symbol loc ("field " ^ $2) field_table $2 t; ($1 t) @ [ ($2, $4) ]) }
269
      
270
eq_list:
271
  { [], [], [] }
272
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
273
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
274
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
275
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
276

    
277
automaton:
278
 AUTOMATON IDENT handler_list { failwith "not implemented" }
279

    
280
handler_list:
281
     { [] }
282
| handler handler_list { $1::$2 }
283

    
284
handler:
285
 STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
286

    
287
unless_list:
288
    { [] }
289
| unless unless_list { $1::$2 }
290

    
291
until_list:
292
    { [] }
293
| until until_list { $1::$2 }
294

    
295
unless:
296
  UNLESS expr RESTART IDENT { }
297
| UNLESS expr RESUME IDENT  { }
298

    
299
until:
300
  UNTIL expr RESTART IDENT { }
301
| UNTIL expr RESUME IDENT  { }
302

    
303
assert_:
304
| ASSERT expr SCOL {mkassert ($2)}
305

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

    
310
lustre_spec:
311
| contract EOF { $1 }
312

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

    
320
ensures:
321
{ [] }
322
| ENSURES qexpr SCOL ensures { $2 :: $4 }
323
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { 
324
  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
325
}
326

    
327
behaviors:
328
{ [] }
329
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
330

    
331
assumes:
332
{ [] }
333
| ASSUMES qexpr SCOL assumes { $2::$4 } 
334

    
335
/* WARNING: UNUSED RULES */
336
tuple_qexpr:
337
| qexpr COMMA qexpr {[$3;$1]}
338
| tuple_qexpr COMMA qexpr {$3::$1}
339

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

    
346

    
347
tuple_expr:
348
    expr COMMA expr {[$3;$1]}
349
| tuple_expr COMMA expr {$3::$1}
350

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

    
356
dim_list:
357
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
358
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
359

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

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

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

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

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

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

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

    
457
/* If */
458
| IF expr THEN expr ELSE expr
459
    {mkexpr (Expr_ite ($2, $4, $6))}
460

    
461
handler_expr_list:
462
   { [] }
463
| handler_expr handler_expr_list { $1 :: $2 }
464

    
465
handler_expr:
466
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
467

    
468
signed_const_array:
469
| signed_const { [$1] }
470
| signed_const COMMA signed_const_array { $1 :: $3 }
471

    
472
signed_const_struct:
473
| IDENT EQ signed_const { [ ($1, $3) ] }
474
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
475

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

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

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

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

    
537
locals:
538
  {[]}
539
| VAR vdecl_list SCOL {$2}
540

    
541
vdecl_list:
542
    vdecl {$1}
543
| vdecl_list SCOL vdecl {$3 @ $1}
544

    
545
vdecl:
546
/* Useless no ?*/    ident_list
547
    {List.map mkvar_decl 
548
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
549

    
550
| ident_list COL typeconst clock 
551
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
552
| CONST ident_list COL typeconst /* static parameters don't have clocks */
553
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
554

    
555
cdecl_list:
556
  cdecl SCOL { [$1] }
557
| cdecl_list cdecl SCOL { $2::$1 }
558

    
559
cdecl:
560
    IDENT EQ signed_const {
561
      let c = {
562
	const_id = $1;
563
	const_loc = Location.symbol_rloc ();
564
        const_type = Types.new_var ();
565
	const_value = $3;
566
      } in
567
      Hashtbl.add consts_table $1 c; c
568
    }
569

    
570
clock:
571
    {mkclock Ckdec_any}
572
| when_list
573
    {mkclock (Ckdec_bool (List.rev $1))}
574

    
575
when_cond:
576
    WHEN IDENT {($2, tag_true)}
577
| WHENNOT IDENT {($2, tag_false)}
578
| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
579

    
580
when_list:
581
    when_cond {[$1]}
582
| when_list when_cond {$2::$1}
583

    
584
ident_list:
585
  IDENT {[$1]}
586
| ident_list COMMA IDENT {$3::$1}
587

    
588
SCOL_opt:
589
    SCOL {} | {}
590

    
591

    
592
lustre_annot:
593
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
594

    
595
lustre_annot_list:
596
  { [] } 
597
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
598
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
599
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
600
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
601

    
602
kwd:
603
DIV { [] }
604
| DIV IDENT kwd { $2::$3}
605

    
606
%%
607
(* Local Variables: *)
608
(* compile-command:"make -C .." *)
609
(* End: *)
610

    
611