Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 53206908

History | View | Annotate | Download (17.5 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 mkident x = x, get_loc ()
22
let mktyp x = mktyp (get_loc ()) x
23
let mkclock x = mkclock (get_loc ()) x
24
let mkvar_decl x loc = mkvar_decl loc ~orig:true x
25
let mkexpr x = mkexpr (get_loc ()) x
26
let mkeexpr x = mkeexpr (get_loc ()) x 
27
let mkeq x = mkeq (get_loc ()) x
28
let mkassert x = mkassert (get_loc ()) x
29
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x
30
let mkpredef_call x = mkpredef_call (get_loc ()) x
31
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
32

    
33
let mkdim_int i = mkdim_int (get_loc ()) i
34
let mkdim_bool b = mkdim_bool (get_loc ()) b
35
let mkdim_ident id = mkdim_ident (get_loc ()) id
36
let mkdim_appl f args = mkdim_appl (get_loc ()) f args
37
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
38

    
39
let mkannots annots = { annots = annots; annot_loc = get_loc () }
40

    
41
let node_stack : ident list ref = ref []
42
let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack
43
let push_node nd =  node_stack:= nd :: !node_stack
44
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
45
let get_current_node () = try List.hd !node_stack with _ -> assert false
46

    
47
let rec fby expr n init =
48
  if n<=1 then
49
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))
50
  else
51
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))
52
  
53
%}
54

    
55
%token <int> INT
56
%token <Num.num * int * string> REAL
57

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

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

    
108
%start prog
109
%type <LustreSpec.top_decl list> prog
110

    
111
%start header
112
%type <LustreSpec.top_decl list> header
113

    
114
%start lustre_annot
115
%type <LustreSpec.expr_annot> lustre_annot
116

    
117
%start lustre_spec
118
%type <LustreSpec.node_annot> lustre_spec
119

    
120
%start signed_const
121
%type <LustreSpec.constant> signed_const
122

    
123
%%
124

    
125
module_ident:
126
  UIDENT { $1 }
127
| IDENT  { $1 }
128

    
129
tag_ident:
130
  UIDENT  { $1 }
131
| TRUE    { tag_true }
132
| FALSE   { tag_false }
133

    
134
node_ident:
135
  UIDENT { $1 }
136
| IDENT  { $1 }
137

    
138
node_ident_decl:
139
 node_ident { push_node $1; $1 }
140

    
141
vdecl_ident:
142
  UIDENT { mkident $1 }
143
| IDENT  { mkident $1 }
144

    
145
const_ident:
146
  UIDENT { $1 }
147
| IDENT  { $1 }
148

    
149
type_ident:
150
  IDENT { $1 }
151

    
152
prog:
153
 open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
154

    
155
typ_def_prog:
156
 typ_def_list { $1 false }
157

    
158
header:
159
 open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) }
160

    
161
typ_def_header:
162
 typ_def_list { $1 true }
163

    
164
open_list:
165
  { [] }
166
| open_lusi open_list { $1 :: $2 }
167

    
168
open_lusi:
169
| OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))}
170
| OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) }
171

    
172
top_decl_list:
173
   {[]}
174
| top_decl_list top_decl {$2@$1}
175

    
176

    
177
top_decl_header_list:
178
   { [] }
179
| top_decl_header_list top_decl_header { $2@$1 }
180

    
181
state_annot:
182
  FUNCTION { true }
183
| NODE { false }
184

    
185
top_decl_header:
186
| CONST cdecl_list { List.rev ($2 true) }
187
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_list SCOL
188
    {let nd = mktop_decl true (ImportedNode
189
				 {nodei_id = $3;
190
				  nodei_type = Types.new_var ();
191
				  nodei_clock = Clocks.new_var true;
192
				  nodei_inputs = List.rev $5;
193
				  nodei_outputs = List.rev $10;
194
				  nodei_stateless = $2;
195
				  nodei_spec = $1;
196
				  nodei_prototype = $13;
197
				  nodei_in_lib = $14;})
198
     in
199
     (*add_imported_node $3 nd;*) [nd] }
200

    
201
prototype_opt:
202
 { None }
203
| PROTOTYPE node_ident { Some $2}
204

    
205
in_lib_list:
206
{ [] }
207
| LIB module_ident in_lib_list { $2::$3 } 
208

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

    
240
nodespec_list:
241
 { None }
242
| NODESPEC nodespec_list { 
243
  (function 
244
  | None    -> (fun s1 -> Some s1) 
245
  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
246

    
247
typ_def_list:
248
    /* empty */             { (fun itf -> []) }
249
| typ_def SCOL typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($3 itf)) }
250

    
251
typ_def:
252
  TYPE type_ident EQ typ_def_rhs { (fun itf ->
253
			       let typ = mktop_decl itf (TypeDef { tydef_id = $2;
254
								   tydef_desc = $4
255
							})
256
			       in (*add_type itf $2 typ;*) typ) }
257

    
258
typ_def_rhs:
259
  typeconst                   { $1 }
260
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }
261
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
262

    
263
array_typ_decl:
264
 %prec POWER                { fun typ -> typ }
265
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
266

    
267
typeconst:
268
  TINT array_typ_decl   { $2 Tydec_int }
269
| TBOOL array_typ_decl  { $2 Tydec_bool  }
270
| TREAL array_typ_decl  { $2 Tydec_real  }
271
/* | TFLOAT array_typ_decl { $2 Tydec_float } */
272
| type_ident array_typ_decl  { $2 (Tydec_const $1) }
273
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }
274
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }
275

    
276
tag_list:
277
  UIDENT                { $1 :: [] }
278
| tag_list COMMA UIDENT { $3 :: $1 }
279
      
280
field_list:                           { [] }
281
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
282
      
283
stmt_list:
284
  { [], [], [] }
285
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
286
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
287
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
288
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
289

    
290
automaton:
291
 AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }
292

    
293
handler_list:
294
     { [] }
295
| handler handler_list { $1::$2 }
296

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

    
300
unless_list:
301
    { [] }
302
| unless unless_list { $1::$2 }
303

    
304
until_list:
305
    { [] }
306
| until until_list { $1::$2 }
307

    
308
unless:
309
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
310
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
311

    
312
until:
313
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
314
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
315

    
316
assert_:
317
| ASSERT expr SCOL {mkassert ($2)}
318

    
319
eq:
320
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
321
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
322

    
323
lustre_spec:
324
| contract EOF { $1 }
325

    
326
contract:
327
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
328
 
329
requires:
330
{ [] }
331
| REQUIRES qexpr SCOL requires { $2::$4 }
332

    
333
ensures:
334
{ [] }
335
| ENSURES qexpr SCOL ensures { $2 :: $4 }
336
| OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { 
337
  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
338
}
339

    
340
behaviors:
341
{ [] }
342
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
343

    
344
assumes:
345
{ [] }
346
| ASSUMES qexpr SCOL assumes { $2::$4 } 
347

    
348
/* WARNING: UNUSED RULES */
349
tuple_qexpr:
350
| qexpr COMMA qexpr {[$3;$1]}
351
| tuple_qexpr COMMA qexpr {$3::$1}
352

    
353
qexpr:
354
| expr { mkeexpr $1 }
355
  /* Quantifiers */
356
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
357
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
358

    
359

    
360
tuple_expr:
361
    expr COMMA expr {[$3;$1]}
362
| tuple_expr COMMA expr {$3::$1}
363

    
364
// Same as tuple expr but accepting lists with single element
365
array_expr:
366
  expr {[$1]}
367
| expr COMMA array_expr {$1::$3}
368

    
369
dim_list:
370
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
371
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
372

    
373
expr:
374
/* constants */
375
  INT {mkexpr (Expr_const (Const_int $1))}
376
| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
377
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
378
/* Idents or type enum tags */
379
| IDENT { mkexpr (Expr_ident $1) }
380
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
381
| LPAR ANNOT expr RPAR
382
    {update_expr_annot (get_current_node ()) $3 $2}
383
| LPAR expr RPAR
384
    {$2}
385
| LPAR tuple_expr RPAR
386
    {mkexpr (Expr_tuple (List.rev $2))}
387

    
388
/* Array expressions */
389
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
390
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
391
| expr LBRACKET dim_list { $3 $1 }
392

    
393
/* Temporal operators */
394
| PRE expr 
395
    {mkexpr (Expr_pre $2)}
396
| expr ARROW expr 
397
    {mkexpr (Expr_arrow ($1,$3))}
398
| expr FBY expr 
399
    {(*mkexpr (Expr_fby ($1,$3))*)
400
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
401
| expr WHEN vdecl_ident
402
    {mkexpr (Expr_when ($1,fst $3,tag_true))}
403
| expr WHENNOT vdecl_ident
404
    {mkexpr (Expr_when ($1,fst $3,tag_false))}
405
| expr WHEN tag_ident LPAR vdecl_ident RPAR
406
    {mkexpr (Expr_when ($1, fst $5, $3))}
407
| MERGE vdecl_ident handler_expr_list
408
    {mkexpr (Expr_merge (fst $2,$3))}
409

    
410
/* Applications */
411
| node_ident LPAR expr RPAR
412
    {mkexpr (Expr_appl ($1, $3, None))}
413
| node_ident LPAR expr RPAR EVERY expr
414
    {mkexpr (Expr_appl ($1, $3, Some $6))}
415
| node_ident LPAR tuple_expr RPAR
416
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
417
| node_ident LPAR tuple_expr RPAR EVERY expr
418
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some $6)) }
419

    
420
/* Boolean expr */
421
| expr AND expr 
422
    {mkpredef_call "&&" [$1;$3]}
423
| expr AMPERAMPER expr 
424
    {mkpredef_call "&&" [$1;$3]}
425
| expr OR expr 
426
    {mkpredef_call "||" [$1;$3]}
427
| expr BARBAR expr 
428
    {mkpredef_call "||" [$1;$3]}
429
| expr XOR expr 
430
    {mkpredef_call "xor" [$1;$3]}
431
| NOT expr 
432
    {mkpredef_call "not" [$2]}
433
| expr IMPL expr 
434
    {mkpredef_call "impl" [$1;$3]}
435

    
436
/* Comparison expr */
437
| expr EQ expr 
438
    {mkpredef_call "=" [$1;$3]}
439
| expr LT expr 
440
    {mkpredef_call "<" [$1;$3]}
441
| expr LTE expr 
442
    {mkpredef_call "<=" [$1;$3]}
443
| expr GT expr 
444
    {mkpredef_call ">" [$1;$3]}
445
| expr GTE  expr 
446
    {mkpredef_call ">=" [$1;$3]}
447
| expr NEQ expr 
448
    {mkpredef_call "!=" [$1;$3]}
449

    
450
/* Arithmetic expr */
451
| expr PLUS expr 
452
    {mkpredef_call "+" [$1;$3]}
453
| expr MINUS expr 
454
    {mkpredef_call "-" [$1;$3]}
455
| expr MULT expr 
456
    {mkpredef_call "*" [$1;$3]}
457
| expr DIV expr 
458
    {mkpredef_call "/" [$1;$3]}
459
| MINUS expr %prec UMINUS
460
  {mkpredef_call "uminus" [$2]}
461
| expr MOD expr 
462
    {mkpredef_call "mod" [$1;$3]}
463

    
464
/* If */
465
| IF expr THEN expr ELSE expr
466
    {mkexpr (Expr_ite ($2, $4, $6))}
467

    
468
handler_expr_list:
469
   { [] }
470
| handler_expr handler_expr_list { $1 :: $2 }
471

    
472
handler_expr:
473
 LPAR tag_ident ARROW expr RPAR { ($2, $4) }
474

    
475
signed_const_array:
476
| signed_const { [$1] }
477
| signed_const COMMA signed_const_array { $1 :: $3 }
478

    
479
signed_const_struct:
480
| IDENT EQ signed_const { [ ($1, $3) ] }
481
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
482

    
483
signed_const:
484
  INT {Const_int $1}
485
| REAL {let c,e,s =$1 in Const_real (c,e,s)}
486
/* | FLOAT {Const_float $1} */
487
| tag_ident {Const_tag $1}
488
| MINUS INT {Const_int (-1 * $2)}
489
| MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)}
490
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
491
| LCUR signed_const_struct RCUR { Const_struct $2 }
492
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
493

    
494
dim:
495
   INT { mkdim_int $1 }
496
| LPAR dim RPAR { $2 }
497
| UIDENT { mkdim_ident $1 }
498
| IDENT { mkdim_ident $1 }
499
| dim AND dim 
500
    {mkdim_appl "&&" [$1;$3]}
501
| dim AMPERAMPER dim 
502
    {mkdim_appl "&&" [$1;$3]}
503
| dim OR dim 
504
    {mkdim_appl "||" [$1;$3]}
505
| dim BARBAR dim 
506
    {mkdim_appl "||" [$1;$3]}
507
| dim XOR dim 
508
    {mkdim_appl "xor" [$1;$3]}
509
| NOT dim 
510
    {mkdim_appl "not" [$2]}
511
| dim IMPL dim 
512
    {mkdim_appl "impl" [$1;$3]}
513

    
514
/* Comparison dim */
515
| dim EQ dim 
516
    {mkdim_appl "=" [$1;$3]}
517
| dim LT dim 
518
    {mkdim_appl "<" [$1;$3]}
519
| dim LTE dim 
520
    {mkdim_appl "<=" [$1;$3]}
521
| dim GT dim 
522
    {mkdim_appl ">" [$1;$3]}
523
| dim GTE  dim 
524
    {mkdim_appl ">=" [$1;$3]}
525
| dim NEQ dim 
526
    {mkdim_appl "!=" [$1;$3]}
527

    
528
/* Arithmetic dim */
529
| dim PLUS dim 
530
    {mkdim_appl "+" [$1;$3]}
531
| dim MINUS dim 
532
    {mkdim_appl "-" [$1;$3]}
533
| dim MULT dim 
534
    {mkdim_appl "*" [$1;$3]}
535
| dim DIV dim 
536
    {mkdim_appl "/" [$1;$3]}
537
| MINUS dim %prec UMINUS
538
  {mkdim_appl "uminus" [$2]}
539
| dim MOD dim 
540
    {mkdim_appl "mod" [$1;$3]}
541
/* If */
542
| IF dim THEN dim ELSE dim
543
    {mkdim_ite $2 $4 $6}
544

    
545
locals:
546
  {[]}
547
| VAR local_vdecl_list SCOL {$2}
548

    
549
vdecl_list:
550
  vdecl {$1}
551
| vdecl_list SCOL vdecl {$3 @ $1}
552

    
553
vdecl:
554
  ident_list COL typeconst clock 
555
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None) loc) $1 }
556
| CONST ident_list /* static parameters don't have clocks */
557
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None) loc) $2 }
558
| CONST ident_list COL typeconst /* static parameters don't have clocks */
559
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None) loc) $2 }
560

    
561
local_vdecl_list:
562
  local_vdecl {$1}
563
| local_vdecl_list SCOL local_vdecl {$3 @ $1}
564

    
565
local_vdecl:
566
/* Useless no ?*/    ident_list
567
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None) loc) $1 }
568
| ident_list COL typeconst clock 
569
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None) loc) $1 }
570
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
571
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) loc ] }
572
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
573
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6) loc ] }
574

    
575
cdecl_list:
576
  cdecl SCOL { (fun itf -> [$1 itf]) }
577
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
578

    
579
cdecl:
580
    const_ident EQ signed_const {
581
      (fun itf -> 
582
       let c = mktop_decl itf (Const {
583
				   const_id = $1;
584
				   const_loc = Location.symbol_rloc ();
585
				   const_type = Types.new_var ();
586
				   const_value = $3})
587
       in
588
       (*add_const itf $1 c;*) c)
589
    }
590

    
591
clock:
592
    {mkclock Ckdec_any}
593
| when_list
594
    {mkclock (Ckdec_bool (List.rev $1))}
595

    
596
when_cond:
597
  WHEN IDENT {($2, tag_true)}
598
| WHENNOT IDENT {($2, tag_false)}
599
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
600

    
601
when_list:
602
    when_cond {[$1]}
603
| when_list when_cond {$2::$1}
604

    
605
ident_list:
606
  vdecl_ident {[$1]}
607
| ident_list COMMA vdecl_ident {$3::$1}
608

    
609
SCOL_opt:
610
    SCOL {} | {}
611

    
612

    
613
lustre_annot:
614
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
615

    
616
lustre_annot_list:
617
  { [] } 
618
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
619
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
620
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
621
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
622

    
623
kwd:
624
DIV { [] }
625
| DIV IDENT kwd { $2::$3}
626

    
627
%%
628
(* Local Variables: *)
629
(* compile-command:"make -C .." *)
630
(* End: *)
631

    
632