Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 6aeb3388

History | View | Annotate | Download (14.9 KB)

1 b38ffff3 ploc
/********************************************************************/
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 0cbf0839 ploc
12
%{
13 6aeb3388 xthirioux
open Utils
14 0cbf0839 ploc
open LustreSpec
15
open Corelang
16
open Dimension
17 6aeb3388 xthirioux
open Parse
18 0cbf0839 ploc
19 0038002e ploc
let get_loc () = Location.symbol_rloc ()
20
let mktyp x = mktyp (get_loc ()) x
21
let mkclock x = mkclock (get_loc ()) x
22
let mkvar_decl x = mkvar_decl (get_loc ()) x
23
let mkexpr x = mkexpr (get_loc ()) x
24
let mkeexpr x = mkeexpr (get_loc ()) x 
25
let mkeq x = mkeq (get_loc ()) x
26
let mkassert x = mkassert (get_loc ()) x
27
let mktop_decl x = mktop_decl (get_loc ()) x
28
let mkpredef_call x = mkpredef_call (get_loc ()) x
29
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
30
31
let mkdim_int i = mkdim_int (get_loc ()) i
32
let mkdim_bool b = mkdim_bool (get_loc ()) b
33
let mkdim_ident id = mkdim_ident (get_loc ()) id
34
let mkdim_appl f args = mkdim_appl (get_loc ()) f args
35
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
36
37
let mkannots annots = { annots = annots; annot_loc = get_loc () }
38 0cbf0839 ploc
39
%}
40
41
%token <int> INT
42
%token <string> REAL
43
%token <float> FLOAT
44 0038002e ploc
%token <string> STRING
45 0cbf0839 ploc
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
46 f22632aa ploc
%token STATELESS ASSERT OPEN QUOTE FUNCTION
47 0cbf0839 ploc
%token <string> IDENT
48
%token <LustreSpec.expr_annot> ANNOT
49
%token <LustreSpec.node_annot> NODESPEC
50
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
51
%token AMPERAMPER BARBAR NOT POWER
52
%token IF THEN ELSE
53
%token UCLOCK DCLOCK PHCLOCK TAIL
54
%token MERGE FBY WHEN WHENNOT EVERY
55
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
56
%token STRUCT ENUM
57
%token TINT TFLOAT TREAL TBOOL TCLOCK
58
%token RATE DUE
59
%token EQ LT GT LTE GTE NEQ
60
%token AND OR XOR IMPL
61
%token MULT DIV MOD
62
%token MINUS PLUS UMINUS
63
%token PRE ARROW
64 0038002e ploc
%token REQUIRES ENSURES OBSERVER
65
%token INVARIANT BEHAVIOR ASSUMES
66
%token EXISTS FORALL
67 45c0d258 ploc
%token PROTOTYPE LIB
68 0cbf0839 ploc
%token EOF
69
70 0038002e ploc
%nonassoc prec_exists prec_forall
71 0cbf0839 ploc
%nonassoc COMMA
72
%left MERGE IF
73
%nonassoc ELSE
74
%right ARROW FBY
75
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
76
%right COLCOL
77
%right IMPL
78
%left OR XOR BARBAR
79
%left AND AMPERAMPER
80
%left NOT
81
%nonassoc INT
82
%nonassoc EQ LT GT LTE GTE NEQ
83
%left MINUS PLUS
84
%left MULT DIV MOD
85
%left UMINUS
86
%left POWER
87
%left PRE LAST
88
%nonassoc RBRACKET
89
%nonassoc LBRACKET
90
91
%start prog
92 0038002e ploc
%type <LustreSpec.top_decl list> prog
93
94 f22632aa ploc
%start header
95 0038002e ploc
%type <bool -> LustreSpec.top_decl list> header
96
97
%start lustre_annot
98
%type <LustreSpec.expr_annot> lustre_annot
99
100
%start lustre_spec
101
%type <LustreSpec.node_annot> lustre_spec
102 0cbf0839 ploc
103
%%
104
105
prog:
106 6aeb3388 xthirioux
 open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
107
108
typ_def_prog:
109
 typ_def_list { $1 true }
110 0cbf0839 ploc
111 f22632aa ploc
header:
112 6aeb3388 xthirioux
 open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ let typs = $2 own in typs @ (List.rev ($3 own)))) }
113 8b3afe43 xthirioux
114
open_list:
115
  { [] }
116
| open_lusi open_list { $1 :: $2 }
117
118
open_lusi:
119 c00d0b42 ploc
| OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))}
120
| OPEN LT IDENT GT { mktop_decl (Open (false, $3)) }
121 f22632aa ploc
122 0cbf0839 ploc
top_decl_list:
123 6aeb3388 xthirioux
   {[]}
124 0cbf0839 ploc
| top_decl_list top_decl {$2::$1}
125
126
127 f22632aa ploc
top_decl_header_list:
128 6aeb3388 xthirioux
   {(fun own -> []) }
129
| top_decl_header_list top_decl_header {(fun own -> let h1 = $1 own in ($2 own)::h1) }
130 0cbf0839 ploc
131 d3e4c22f xthirioux
state_annot:
132
  FUNCTION { true }
133
| NODE { false }
134 0cbf0839 ploc
135 f22632aa ploc
top_decl_header:
136 45c0d258 ploc
| CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ -> top }
137 c00d0b42 ploc
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_opt SCOL
138 0cbf0839 ploc
    {let nd = mktop_decl (ImportedNode
139 f22632aa ploc
                            {nodei_id = $3;
140 0cbf0839 ploc
                             nodei_type = Types.new_var ();
141
                             nodei_clock = Clocks.new_var true;
142 f22632aa ploc
                             nodei_inputs = List.rev $5;
143 0cbf0839 ploc
                             nodei_outputs = List.rev $10;
144 d3e4c22f xthirioux
			     nodei_stateless = $2;
145 c00d0b42 ploc
			     nodei_spec = $1;
146
			     nodei_prototype = $13;
147
			     nodei_in_lib = $14;})
148 0cbf0839 ploc
    in
149 6aeb3388 xthirioux
     (fun own -> add_node own $3 nd; nd) }
150 0cbf0839 ploc
151 c00d0b42 ploc
prototype_opt:
152
 { None }
153
| PROTOTYPE IDENT { Some $2}
154
155
in_lib_opt:
156
{ None }
157 45c0d258 ploc
| LIB IDENT {Some $2} 
158 c00d0b42 ploc
159 f22632aa ploc
top_decl:
160
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
161 d3e4c22f xthirioux
| 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 
162 f22632aa ploc
    {let eqs, asserts, annots = $16 in
163
     let nd = mktop_decl (Node
164
                            {node_id = $3;
165
                             node_type = Types.new_var ();
166
                             node_clock = Clocks.new_var true;
167
                             node_inputs = List.rev $5;
168
                             node_outputs = List.rev $10;
169
                             node_locals = List.rev $14;
170
			     node_gencalls = [];
171
			     node_checks = [];
172
			     node_asserts = asserts; 
173
                             node_eqs = eqs;
174 d3e4c22f xthirioux
			     node_dec_stateless = $2;
175
			     node_stateless = None;
176
			     node_spec = $1;
177 0038002e ploc
			     node_annot = annots})
178 45c0d258 ploc
     in
179 6aeb3388 xthirioux
     add_node true $3 nd; nd}
180 f22632aa ploc
181 0cbf0839 ploc
nodespec_list:
182 d3e4c22f xthirioux
 { None }
183 0038002e ploc
| NODESPEC nodespec_list { 
184
  (function 
185
  | None    -> (fun s1 -> Some s1) 
186
  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
187 0cbf0839 ploc
188
typ_def_list:
189 6aeb3388 xthirioux
    /* empty */             { (fun own -> []) }
190
| typ_def SCOL typ_def_list { (fun own -> let ty1 = ($1 own) in ty1 :: ($3 own)) }
191 0cbf0839 ploc
192
typ_def:
193 6aeb3388 xthirioux
  TYPE IDENT EQ typ_def_rhs { let typ = mktop_decl (Type { ty_def_id = $2;
194
							   ty_def_desc = $4
195
							 })
196
			      in (fun own -> add_type own $2 typ; typ) }
197
198
typ_def_rhs:
199
  typeconst                   { $1 }
200
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }
201
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
202 0cbf0839 ploc
203
array_typ_decl:
204
                            { fun typ -> typ }
205
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
206
207
typeconst:
208 6aeb3388 xthirioux
  TINT array_typ_decl   { $2 Tydec_int }
209
| TBOOL array_typ_decl  { $2 Tydec_bool  }
210
| TREAL array_typ_decl  { $2 Tydec_real  }
211 0cbf0839 ploc
| TFLOAT array_typ_decl { $2 Tydec_float }
212 6aeb3388 xthirioux
| IDENT array_typ_decl  { $2 (Tydec_const $1) }
213
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }
214
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }
215 0cbf0839 ploc
216
tag_list:
217 6aeb3388 xthirioux
  IDENT                { $1 :: [] }
218
| tag_list COMMA IDENT { $3 :: $1 }
219 45c0d258 ploc
      
220 6aeb3388 xthirioux
field_list:                           { [] }
221
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
222 45c0d258 ploc
      
223 0cbf0839 ploc
eq_list:
224
  { [], [], [] }
225
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
226
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
227 0038002e ploc
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
228 0cbf0839 ploc
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
229
230
automaton:
231
 AUTOMATON IDENT handler_list { failwith "not implemented" }
232
233
handler_list:
234
     { [] }
235
| handler handler_list { $1::$2 }
236
237
handler:
238
 STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
239
240
unless_list:
241
    { [] }
242
| unless unless_list { $1::$2 }
243
244
until_list:
245
    { [] }
246
| until until_list { $1::$2 }
247
248
unless:
249
  UNLESS expr RESTART IDENT { }
250
| UNLESS expr RESUME IDENT  { }
251
252
until:
253
  UNTIL expr RESTART IDENT { }
254
| UNTIL expr RESUME IDENT  { }
255
256
assert_:
257
| ASSERT expr SCOL {mkassert ($2)}
258
259
eq:
260
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
261
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
262
263 0038002e ploc
lustre_spec:
264
| contract EOF { $1 }
265
266
contract:
267
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
268
 
269
requires:
270
{ [] }
271
| REQUIRES qexpr SCOL requires { $2::$4 }
272
273
ensures:
274
{ [] }
275
| ENSURES qexpr SCOL ensures { $2 :: $4 }
276
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { 
277
  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
278
}
279
280
behaviors:
281
{ [] }
282
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
283
284
assumes:
285
{ [] }
286
| ASSUMES qexpr SCOL assumes { $2::$4 } 
287
288 7cd31331 xthirioux
/* WARNING: UNUSED RULES */
289 0038002e ploc
tuple_qexpr:
290
| qexpr COMMA qexpr {[$3;$1]}
291
| tuple_qexpr COMMA qexpr {$3::$1}
292
293
qexpr:
294
| expr { mkeexpr $1 }
295
  /* Quantifiers */
296
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
297
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
298
299
300 0cbf0839 ploc
tuple_expr:
301
    expr COMMA expr {[$3;$1]}
302
| tuple_expr COMMA expr {$3::$1}
303
304
// Same as tuple expr but accepting lists with single element
305
array_expr:
306
  expr {[$1]}
307
| expr COMMA array_expr {$1::$3}
308
309
dim_list:
310
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
311
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
312
313
expr:
314
/* constants */
315
  INT {mkexpr (Expr_const (Const_int $1))}
316
| REAL {mkexpr (Expr_const (Const_real $1))}
317
| FLOAT {mkexpr (Expr_const (Const_float $1))}
318
/* Idents or type enum tags */
319
| IDENT {
320
  if Hashtbl.mem tag_table $1
321
  then mkexpr (Expr_const (Const_tag $1))
322
  else mkexpr (Expr_ident $1)}
323
| LPAR ANNOT expr RPAR
324
    {update_expr_annot $3 $2}
325
| LPAR expr RPAR
326
    {$2}
327
| LPAR tuple_expr RPAR
328
    {mkexpr (Expr_tuple (List.rev $2))}
329
330
/* Array expressions */
331
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
332
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
333
| expr LBRACKET dim_list { $3 $1 }
334
335
/* Temporal operators */
336
| PRE expr 
337
    {mkexpr (Expr_pre $2)}
338
| expr ARROW expr 
339
    {mkexpr (Expr_arrow ($1,$3))}
340
| expr FBY expr 
341
    {(*mkexpr (Expr_fby ($1,$3))*)
342
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
343
| expr WHEN IDENT 
344
    {mkexpr (Expr_when ($1,$3,tag_true))}
345
| expr WHENNOT IDENT
346
    {mkexpr (Expr_when ($1,$3,tag_false))}
347
| expr WHEN IDENT LPAR IDENT RPAR
348
    {mkexpr (Expr_when ($1, $5, $3))}
349
| MERGE IDENT handler_expr_list
350
    {mkexpr (Expr_merge ($2,$3))}
351
352
/* Applications */
353
| IDENT LPAR expr RPAR
354
    {mkexpr (Expr_appl ($1, $3, None))}
355
| IDENT LPAR expr RPAR EVERY IDENT
356
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
357
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
358
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
359
| IDENT LPAR tuple_expr RPAR
360
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
361
| IDENT LPAR tuple_expr RPAR EVERY IDENT
362
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
363
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
364
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
365
366
/* Boolean expr */
367
| expr AND expr 
368
    {mkpredef_call "&&" [$1;$3]}
369
| expr AMPERAMPER expr 
370
    {mkpredef_call "&&" [$1;$3]}
371
| expr OR expr 
372
    {mkpredef_call "||" [$1;$3]}
373
| expr BARBAR expr 
374
    {mkpredef_call "||" [$1;$3]}
375
| expr XOR expr 
376
    {mkpredef_call "xor" [$1;$3]}
377
| NOT expr 
378 14d694c7 xthirioux
    {mkpredef_call "not" [$2]}
379 0cbf0839 ploc
| expr IMPL expr 
380
    {mkpredef_call "impl" [$1;$3]}
381
382
/* Comparison expr */
383
| expr EQ expr 
384
    {mkpredef_call "=" [$1;$3]}
385
| expr LT expr 
386
    {mkpredef_call "<" [$1;$3]}
387
| expr LTE expr 
388
    {mkpredef_call "<=" [$1;$3]}
389
| expr GT expr 
390
    {mkpredef_call ">" [$1;$3]}
391
| expr GTE  expr 
392
    {mkpredef_call ">=" [$1;$3]}
393
| expr NEQ expr 
394
    {mkpredef_call "!=" [$1;$3]}
395
396
/* Arithmetic expr */
397
| expr PLUS expr 
398
    {mkpredef_call "+" [$1;$3]}
399
| expr MINUS expr 
400
    {mkpredef_call "-" [$1;$3]}
401
| expr MULT expr 
402
    {mkpredef_call "*" [$1;$3]}
403
| expr DIV expr 
404
    {mkpredef_call "/" [$1;$3]}
405
| MINUS expr %prec UMINUS
406 14d694c7 xthirioux
  {mkpredef_call "uminus" [$2]}
407 0cbf0839 ploc
| expr MOD expr 
408
    {mkpredef_call "mod" [$1;$3]}
409
410
/* If */
411
| IF expr THEN expr ELSE expr
412
    {mkexpr (Expr_ite ($2, $4, $6))}
413
414
handler_expr_list:
415
   { [] }
416
| handler_expr handler_expr_list { $1 :: $2 }
417
418
handler_expr:
419
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
420
421
signed_const_array:
422
| signed_const { [$1] }
423
| signed_const COMMA signed_const_array { $1 :: $3 }
424
425 aa223e69 xthirioux
signed_const_struct:
426
| IDENT EQ signed_const { [ ($1, $3) ] }
427
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
428
429 0cbf0839 ploc
signed_const:
430
  INT {Const_int $1}
431
| REAL {Const_real $1}
432
| FLOAT {Const_float $1}
433
| IDENT {Const_tag $1}
434
| MINUS INT {Const_int (-1 * $2)}
435
| MINUS REAL {Const_real ("-" ^ $2)}
436
| MINUS FLOAT {Const_float (-1. *. $2)}
437 aa223e69 xthirioux
| LCUR signed_const_struct RCUR { Const_struct $2 }
438 0cbf0839 ploc
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
439
440
dim:
441
   INT { mkdim_int $1 }
442
| LPAR dim RPAR { $2 }
443
| IDENT { mkdim_ident $1 }
444
| dim AND dim 
445
    {mkdim_appl "&&" [$1;$3]}
446
| dim AMPERAMPER dim 
447
    {mkdim_appl "&&" [$1;$3]}
448
| dim OR dim 
449
    {mkdim_appl "||" [$1;$3]}
450
| dim BARBAR dim 
451
    {mkdim_appl "||" [$1;$3]}
452
| dim XOR dim 
453
    {mkdim_appl "xor" [$1;$3]}
454
| NOT dim 
455
    {mkdim_appl "not" [$2]}
456
| dim IMPL dim 
457
    {mkdim_appl "impl" [$1;$3]}
458
459
/* Comparison dim */
460
| dim EQ dim 
461
    {mkdim_appl "=" [$1;$3]}
462
| dim LT dim 
463
    {mkdim_appl "<" [$1;$3]}
464
| dim LTE dim 
465
    {mkdim_appl "<=" [$1;$3]}
466
| dim GT dim 
467
    {mkdim_appl ">" [$1;$3]}
468
| dim GTE  dim 
469
    {mkdim_appl ">=" [$1;$3]}
470
| dim NEQ dim 
471
    {mkdim_appl "!=" [$1;$3]}
472
473
/* Arithmetic dim */
474
| dim PLUS dim 
475
    {mkdim_appl "+" [$1;$3]}
476
| dim MINUS dim 
477
    {mkdim_appl "-" [$1;$3]}
478
| dim MULT dim 
479
    {mkdim_appl "*" [$1;$3]}
480
| dim DIV dim 
481
    {mkdim_appl "/" [$1;$3]}
482
| MINUS dim %prec UMINUS
483
  {mkdim_appl "uminus" [$2]}
484
| dim MOD dim 
485
    {mkdim_appl "mod" [$1;$3]}
486
/* If */
487
| IF dim THEN dim ELSE dim
488
    {mkdim_ite $2 $4 $6}
489
490
locals:
491
  {[]}
492
| VAR vdecl_list SCOL {$2}
493
494
vdecl_list:
495
    vdecl {$1}
496
| vdecl_list SCOL vdecl {$3 @ $1}
497
498
vdecl:
499
/* Useless no ?*/    ident_list
500
    {List.map mkvar_decl 
501
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
502
503
| ident_list COL typeconst clock 
504
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
505
| CONST ident_list COL typeconst /* static parameters don't have clocks */
506
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
507
508
cdecl_list:
509
  cdecl SCOL { [$1] }
510
| cdecl_list cdecl SCOL { $2::$1 }
511
512
cdecl:
513
    IDENT EQ signed_const {
514
      let c = {
515
	const_id = $1;
516
	const_loc = Location.symbol_rloc ();
517
        const_type = Types.new_var ();
518
	const_value = $3;
519
      } in
520
      Hashtbl.add consts_table $1 c; c
521
    }
522
523
clock:
524
    {mkclock Ckdec_any}
525
| when_list
526
    {mkclock (Ckdec_bool (List.rev $1))}
527
528
when_cond:
529
    WHEN IDENT {($2, tag_true)}
530
| WHENNOT IDENT {($2, tag_false)}
531
| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
532
533
when_list:
534
    when_cond {[$1]}
535
| when_list when_cond {$2::$1}
536
537
ident_list:
538
  IDENT {[$1]}
539
| ident_list COMMA IDENT {$3::$1}
540
541
SCOL_opt:
542
    SCOL {} | {}
543 0038002e ploc
544
545
lustre_annot:
546
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
547
548
lustre_annot_list:
549
  { [] } 
550
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
551
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
552
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
553
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
554
555
kwd:
556
DIV { [] }
557
| DIV IDENT kwd { $2::$3}
558
559
%%
560
(* Local Variables: *)
561
(* compile-command:"make -C .." *)
562
(* End: *)
563