Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ b38ffff3

History | View | Annotate | Download (16.3 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 LustreSpec
14
open Corelang
15
open Dimension
16
open Utils
17

    
18
let get_loc () = Location.symbol_rloc ()
19
let mktyp x = mktyp (get_loc ()) x
20
let mkclock x = mkclock (get_loc ()) x
21
let mkvar_decl x = mkvar_decl (get_loc ()) x
22
let mkexpr x = mkexpr (get_loc ()) x
23
let mkeexpr x = mkeexpr (get_loc ()) x 
24
let mkeq x = mkeq (get_loc ()) x
25
let mkassert x = mkassert (get_loc ()) x
26
let mktop_decl x = mktop_decl (get_loc ()) x
27
let mkpredef_call x = mkpredef_call (get_loc ()) x
28
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
29

    
30
let mkdim_int i = mkdim_int (get_loc ()) i
31
let mkdim_bool b = mkdim_bool (get_loc ()) b
32
let mkdim_ident id = mkdim_ident (get_loc ()) id
33
let mkdim_appl f args = mkdim_appl (get_loc ()) f args
34
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
35

    
36
let mkannots annots = { annots = annots; annot_loc = get_loc () }
37

    
38
let add_node loc own msg hashtbl name value =
39
  try
40
    match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with
41
    | Node _        , ImportedNode _ when own   -> ()
42
    | ImportedNode _, _                         -> Hashtbl.add hashtbl name value
43
    | Node _        , _                         -> raise (Error (loc, Already_bound_symbol msg))
44
    | _                                         -> assert false
45
  with
46
    Not_found                                   -> Hashtbl.add hashtbl name value
47

    
48

    
49
let add_symbol loc msg hashtbl name value =
50
 if Hashtbl.mem hashtbl name
51
 then raise (Error (loc, Already_bound_symbol msg))
52
 else Hashtbl.add hashtbl name value
53

    
54
let check_symbol loc msg hashtbl name =
55
 if not (Hashtbl.mem hashtbl name)
56
 then raise (Error (loc, Unbound_symbol msg))
57
 else ()
58

    
59
let check_node_symbol msg name value =
60
 if Hashtbl.mem node_table name
61
 then () (* TODO: should we check the types here ? *)
62
 else Hashtbl.add node_table name value
63

    
64
%}
65

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

    
95
%nonassoc prec_exists prec_forall
96
%nonassoc COMMA
97
%left MERGE IF
98
%nonassoc ELSE
99
%right ARROW FBY
100
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
101
%right COLCOL
102
%right IMPL
103
%left OR XOR BARBAR
104
%left AND AMPERAMPER
105
%left NOT
106
%nonassoc INT
107
%nonassoc EQ LT GT LTE GTE NEQ
108
%left MINUS PLUS
109
%left MULT DIV MOD
110
%left UMINUS
111
%left POWER
112
%left PRE LAST
113
%nonassoc RBRACKET
114
%nonassoc LBRACKET
115

    
116
%start prog
117
%type <LustreSpec.top_decl list> prog
118

    
119
%start header
120
%type <bool -> LustreSpec.top_decl list> header
121

    
122
%start lustre_annot
123
%type <LustreSpec.expr_annot> lustre_annot
124

    
125
%start lustre_spec
126
%type <LustreSpec.node_annot> lustre_spec
127

    
128
%%
129

    
130
prog:
131
 open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }
132

    
133
header:
134
 open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ (List.rev ($3 own)))) }
135

    
136
open_list:
137
  { [] }
138
| open_lusi open_list { $1 :: $2 }
139

    
140
open_lusi:
141
| OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))}
142
| OPEN LT IDENT GT { mktop_decl (Open (false, $3)) }
143

    
144
top_decl_list:
145
  top_decl {[$1]}
146
| top_decl_list top_decl {$2::$1}
147

    
148

    
149
top_decl_header_list:
150
  top_decl_header {(fun own -> [$1 own]) }
151
| top_decl_header_list top_decl_header {(fun own -> ($2 own)::($1 own)) }
152

    
153
state_annot:
154
  FUNCTION { true }
155
| NODE { false }
156

    
157
top_decl_header:
158
| CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ -> top }
159
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_opt SCOL
160
    {let nd = mktop_decl (ImportedNode
161
                            {nodei_id = $3;
162
                             nodei_type = Types.new_var ();
163
                             nodei_clock = Clocks.new_var true;
164
                             nodei_inputs = List.rev $5;
165
                             nodei_outputs = List.rev $10;
166
			     nodei_stateless = $2;
167
			     nodei_spec = $1;
168
			     nodei_prototype = $13;
169
			     nodei_in_lib = $14;})
170
    in
171
     check_node_symbol ("node " ^ $3) $3 nd; 
172
     let loc = get_loc () in
173
     (fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) }
174

    
175
prototype_opt:
176
 { None }
177
| PROTOTYPE IDENT { Some $2}
178

    
179
in_lib_opt:
180
{ None }
181
| LIB IDENT {Some $2} 
182

    
183
top_decl:
184
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
185
| 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 
186
    {let eqs, asserts, annots = $16 in
187
     let nd = mktop_decl (Node
188
                            {node_id = $3;
189
                             node_type = Types.new_var ();
190
                             node_clock = Clocks.new_var true;
191
                             node_inputs = List.rev $5;
192
                             node_outputs = List.rev $10;
193
                             node_locals = List.rev $14;
194
			     node_gencalls = [];
195
			     node_checks = [];
196
			     node_asserts = asserts; 
197
                             node_eqs = eqs;
198
			     node_dec_stateless = $2;
199
			     node_stateless = None;
200
			     node_spec = $1;
201
			     node_annot = annots})
202
     in
203
     let loc = Location.symbol_rloc () in
204
     add_node loc true ("node " ^ $3) node_table $3 nd; nd}
205

    
206
nodespec_list:
207
 { None }
208
| NODESPEC nodespec_list { 
209
  (function 
210
  | None    -> (fun s1 -> Some s1) 
211
  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
212

    
213
typ_def_list:
214
    /* empty */ {}
215
| typ_def SCOL typ_def_list {$1;$3}
216

    
217
typ_def:
218
  TYPE IDENT EQ typeconst {
219
    try
220
      let loc = Location.symbol_rloc () in
221
      add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (get_repr_type $4)
222
    with Not_found-> assert false }
223
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
224
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) }
225

    
226
array_typ_decl:
227
                            { fun typ -> typ }
228
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
229

    
230
typeconst:
231
  TINT array_typ_decl  { $2 Tydec_int }
232
| TBOOL array_typ_decl { $2 Tydec_bool  }
233
| TREAL array_typ_decl { $2 Tydec_real  }
234
| TFLOAT array_typ_decl { $2 Tydec_float }
235
| IDENT array_typ_decl { 
236
        let loc = Location.symbol_rloc () in
237
	check_symbol loc ("type " ^ $1) type_table (Tydec_const $1); $2 (Tydec_const $1) }
238
| TBOOL TCLOCK  { Tydec_clock Tydec_bool }
239
| IDENT TCLOCK  { Tydec_clock (Tydec_const $1) }
240

    
241
tag_list:
242
  IDENT
243
  { let loc = Location.symbol_rloc () in 
244
    (fun t -> 
245
      add_symbol loc ("tag " ^ $1) tag_table $1 t; $1 :: []) }
246
| tag_list COMMA IDENT
247
      {       
248
	let loc = Location.symbol_rloc () in
249
	(fun t -> add_symbol loc ("tag " ^ $3)tag_table $3 t; $3 :: ($1 t)) 
250
      }
251
      
252
field_list:
253
  { (fun t -> []) }
254
| field_list IDENT COL typeconst SCOL
255
      {
256
	let loc = Location.symbol_rloc () in
257
	(fun t -> add_symbol loc ("field " ^ $2) field_table $2 t; ($1 t) @ [ ($2, $4) ]) }
258
      
259
eq_list:
260
  { [], [], [] }
261
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
262
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
263
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
264
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
265

    
266
automaton:
267
 AUTOMATON IDENT handler_list { failwith "not implemented" }
268

    
269
handler_list:
270
     { [] }
271
| handler handler_list { $1::$2 }
272

    
273
handler:
274
 STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
275

    
276
unless_list:
277
    { [] }
278
| unless unless_list { $1::$2 }
279

    
280
until_list:
281
    { [] }
282
| until until_list { $1::$2 }
283

    
284
unless:
285
  UNLESS expr RESTART IDENT { }
286
| UNLESS expr RESUME IDENT  { }
287

    
288
until:
289
  UNTIL expr RESTART IDENT { }
290
| UNTIL expr RESUME IDENT  { }
291

    
292
assert_:
293
| ASSERT expr SCOL {mkassert ($2)}
294

    
295
eq:
296
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
297
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
298

    
299
lustre_spec:
300
| contract EOF { $1 }
301

    
302
contract:
303
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
304
 
305
requires:
306
{ [] }
307
| REQUIRES qexpr SCOL requires { $2::$4 }
308

    
309
ensures:
310
{ [] }
311
| ENSURES qexpr SCOL ensures { $2 :: $4 }
312
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { 
313
  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
314
}
315

    
316
behaviors:
317
{ [] }
318
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
319

    
320
assumes:
321
{ [] }
322
| ASSUMES qexpr SCOL assumes { $2::$4 } 
323

    
324
/* WARNING: UNUSED RULES */
325
tuple_qexpr:
326
| qexpr COMMA qexpr {[$3;$1]}
327
| tuple_qexpr COMMA qexpr {$3::$1}
328

    
329
qexpr:
330
| expr { mkeexpr $1 }
331
  /* Quantifiers */
332
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
333
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
334

    
335

    
336
tuple_expr:
337
    expr COMMA expr {[$3;$1]}
338
| tuple_expr COMMA expr {$3::$1}
339

    
340
// Same as tuple expr but accepting lists with single element
341
array_expr:
342
  expr {[$1]}
343
| expr COMMA array_expr {$1::$3}
344

    
345
dim_list:
346
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
347
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
348

    
349
expr:
350
/* constants */
351
  INT {mkexpr (Expr_const (Const_int $1))}
352
| REAL {mkexpr (Expr_const (Const_real $1))}
353
| FLOAT {mkexpr (Expr_const (Const_float $1))}
354
/* Idents or type enum tags */
355
| IDENT {
356
  if Hashtbl.mem tag_table $1
357
  then mkexpr (Expr_const (Const_tag $1))
358
  else mkexpr (Expr_ident $1)}
359
| LPAR ANNOT expr RPAR
360
    {update_expr_annot $3 $2}
361
| LPAR expr RPAR
362
    {$2}
363
| LPAR tuple_expr RPAR
364
    {mkexpr (Expr_tuple (List.rev $2))}
365

    
366
/* Array expressions */
367
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
368
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
369
| expr LBRACKET dim_list { $3 $1 }
370

    
371
/* Temporal operators */
372
| PRE expr 
373
    {mkexpr (Expr_pre $2)}
374
| expr ARROW expr 
375
    {mkexpr (Expr_arrow ($1,$3))}
376
| expr FBY expr 
377
    {(*mkexpr (Expr_fby ($1,$3))*)
378
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
379
| expr WHEN IDENT 
380
    {mkexpr (Expr_when ($1,$3,tag_true))}
381
| expr WHENNOT IDENT
382
    {mkexpr (Expr_when ($1,$3,tag_false))}
383
| expr WHEN IDENT LPAR IDENT RPAR
384
    {mkexpr (Expr_when ($1, $5, $3))}
385
| MERGE IDENT handler_expr_list
386
    {mkexpr (Expr_merge ($2,$3))}
387

    
388
/* Applications */
389
| IDENT LPAR expr RPAR
390
    {mkexpr (Expr_appl ($1, $3, None))}
391
| IDENT LPAR expr RPAR EVERY IDENT
392
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
393
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
394
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
395
| IDENT LPAR tuple_expr RPAR
396
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
397
| IDENT LPAR tuple_expr RPAR EVERY IDENT
398
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
399
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
400
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
401

    
402
/* Boolean expr */
403
| expr AND expr 
404
    {mkpredef_call "&&" [$1;$3]}
405
| expr AMPERAMPER expr 
406
    {mkpredef_call "&&" [$1;$3]}
407
| expr OR expr 
408
    {mkpredef_call "||" [$1;$3]}
409
| expr BARBAR expr 
410
    {mkpredef_call "||" [$1;$3]}
411
| expr XOR expr 
412
    {mkpredef_call "xor" [$1;$3]}
413
| NOT expr 
414
    {mkpredef_call "not" [$2]}
415
| expr IMPL expr 
416
    {mkpredef_call "impl" [$1;$3]}
417

    
418
/* Comparison expr */
419
| expr EQ expr 
420
    {mkpredef_call "=" [$1;$3]}
421
| expr LT expr 
422
    {mkpredef_call "<" [$1;$3]}
423
| expr LTE expr 
424
    {mkpredef_call "<=" [$1;$3]}
425
| expr GT expr 
426
    {mkpredef_call ">" [$1;$3]}
427
| expr GTE  expr 
428
    {mkpredef_call ">=" [$1;$3]}
429
| expr NEQ expr 
430
    {mkpredef_call "!=" [$1;$3]}
431

    
432
/* Arithmetic expr */
433
| expr PLUS expr 
434
    {mkpredef_call "+" [$1;$3]}
435
| expr MINUS expr 
436
    {mkpredef_call "-" [$1;$3]}
437
| expr MULT expr 
438
    {mkpredef_call "*" [$1;$3]}
439
| expr DIV expr 
440
    {mkpredef_call "/" [$1;$3]}
441
| MINUS expr %prec UMINUS
442
  {mkpredef_call "uminus" [$2]}
443
| expr MOD expr 
444
    {mkpredef_call "mod" [$1;$3]}
445

    
446
/* If */
447
| IF expr THEN expr ELSE expr
448
    {mkexpr (Expr_ite ($2, $4, $6))}
449

    
450
handler_expr_list:
451
   { [] }
452
| handler_expr handler_expr_list { $1 :: $2 }
453

    
454
handler_expr:
455
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
456

    
457
signed_const_array:
458
| signed_const { [$1] }
459
| signed_const COMMA signed_const_array { $1 :: $3 }
460

    
461
signed_const_struct:
462
| IDENT EQ signed_const { [ ($1, $3) ] }
463
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
464

    
465
signed_const:
466
  INT {Const_int $1}
467
| REAL {Const_real $1}
468
| FLOAT {Const_float $1}
469
| IDENT {Const_tag $1}
470
| MINUS INT {Const_int (-1 * $2)}
471
| MINUS REAL {Const_real ("-" ^ $2)}
472
| MINUS FLOAT {Const_float (-1. *. $2)}
473
| LCUR signed_const_struct RCUR { Const_struct $2 }
474
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
475

    
476
dim:
477
   INT { mkdim_int $1 }
478
| LPAR dim RPAR { $2 }
479
| IDENT { mkdim_ident $1 }
480
| dim AND dim 
481
    {mkdim_appl "&&" [$1;$3]}
482
| dim AMPERAMPER dim 
483
    {mkdim_appl "&&" [$1;$3]}
484
| dim OR dim 
485
    {mkdim_appl "||" [$1;$3]}
486
| dim BARBAR dim 
487
    {mkdim_appl "||" [$1;$3]}
488
| dim XOR dim 
489
    {mkdim_appl "xor" [$1;$3]}
490
| NOT dim 
491
    {mkdim_appl "not" [$2]}
492
| dim IMPL dim 
493
    {mkdim_appl "impl" [$1;$3]}
494

    
495
/* Comparison dim */
496
| dim EQ dim 
497
    {mkdim_appl "=" [$1;$3]}
498
| dim LT dim 
499
    {mkdim_appl "<" [$1;$3]}
500
| dim LTE dim 
501
    {mkdim_appl "<=" [$1;$3]}
502
| dim GT dim 
503
    {mkdim_appl ">" [$1;$3]}
504
| dim GTE  dim 
505
    {mkdim_appl ">=" [$1;$3]}
506
| dim NEQ dim 
507
    {mkdim_appl "!=" [$1;$3]}
508

    
509
/* Arithmetic dim */
510
| dim PLUS dim 
511
    {mkdim_appl "+" [$1;$3]}
512
| dim MINUS dim 
513
    {mkdim_appl "-" [$1;$3]}
514
| dim MULT dim 
515
    {mkdim_appl "*" [$1;$3]}
516
| dim DIV dim 
517
    {mkdim_appl "/" [$1;$3]}
518
| MINUS dim %prec UMINUS
519
  {mkdim_appl "uminus" [$2]}
520
| dim MOD dim 
521
    {mkdim_appl "mod" [$1;$3]}
522
/* If */
523
| IF dim THEN dim ELSE dim
524
    {mkdim_ite $2 $4 $6}
525

    
526
locals:
527
  {[]}
528
| VAR vdecl_list SCOL {$2}
529

    
530
vdecl_list:
531
    vdecl {$1}
532
| vdecl_list SCOL vdecl {$3 @ $1}
533

    
534
vdecl:
535
/* Useless no ?*/    ident_list
536
    {List.map mkvar_decl 
537
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
538

    
539
| ident_list COL typeconst clock 
540
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
541
| CONST ident_list COL typeconst /* static parameters don't have clocks */
542
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
543

    
544
cdecl_list:
545
  cdecl SCOL { [$1] }
546
| cdecl_list cdecl SCOL { $2::$1 }
547

    
548
cdecl:
549
    IDENT EQ signed_const {
550
      let c = {
551
	const_id = $1;
552
	const_loc = Location.symbol_rloc ();
553
        const_type = Types.new_var ();
554
	const_value = $3;
555
      } in
556
      Hashtbl.add consts_table $1 c; c
557
    }
558

    
559
clock:
560
    {mkclock Ckdec_any}
561
| when_list
562
    {mkclock (Ckdec_bool (List.rev $1))}
563

    
564
when_cond:
565
    WHEN IDENT {($2, tag_true)}
566
| WHENNOT IDENT {($2, tag_false)}
567
| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
568

    
569
when_list:
570
    when_cond {[$1]}
571
| when_list when_cond {$2::$1}
572

    
573
ident_list:
574
  IDENT {[$1]}
575
| ident_list COMMA IDENT {$3::$1}
576

    
577
SCOL_opt:
578
    SCOL {} | {}
579

    
580

    
581
lustre_annot:
582
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
583

    
584
lustre_annot_list:
585
  { [] } 
586
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
587
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
588
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
589
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
590

    
591
kwd:
592
DIV { [] }
593
| DIV IDENT kwd { $2::$3}
594

    
595
%%
596
(* Local Variables: *)
597
(* compile-command:"make -C .." *)
598
(* End: *)
599

    
600