Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 0038002e

History | View | Annotate | Download (16.6 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
tuple_qexpr:
336
| qexpr COMMA qexpr {[$3;$1]}
337
| tuple_qexpr COMMA qexpr {$3::$1}
338

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

    
345

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
587
SCOL_opt:
588
    SCOL {} | {}
589

    
590

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

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

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

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

    
610