Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ a0b18d45

History | View | Annotate | Download (19 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 Lustre_types
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
60
%token ASSERT OPEN QUOTE FUNCTION
61
%token <string> IDENT
62
%token <string> UIDENT
63
%token TRUE FALSE
64
%token <Lustre_types.expr_annot> ANNOT
65
%token <Lustre_types.contract_desc> NODESPEC
66
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA
67
/* unused token? */
68
%token COLCOL
69
%token AMPERAMPER BARBAR NOT POWER
70
%token IF THEN ELSE
71
%token MERGE FBY WHEN WHENNOT EVERY
72
%token NODE LET TEL RETURNS VAR TYPE CONST
73
/* unused token? */
74
%token IMPORTED
75
%token STRUCT ENUM
76
%token TINT TREAL TBOOL TCLOCK
77
%token EQ LT GT LTE GTE NEQ
78
%token AND OR XOR IMPL
79
%token MULT DIV MOD
80
%token MINUS PLUS UMINUS
81
%token PRE ARROW
82
%token REQUIRES ENSURES OBSERVER
83
%token INVARIANT BEHAVIOR ASSUMES CCODE MATLAB
84
%token EXISTS FORALL
85
%token PROTOTYPE LIB
86
%token EOF
87
%token END
88

    
89
%nonassoc prec_exists prec_forall
90
/* unused precedence rules*/
91
/*
92
%nonassoc COMMA
93
*/
94
%nonassoc EVERY
95
/* unused precedence rules
96
%left MERGE IF
97
*/
98
%nonassoc ELSE
99
%right ARROW FBY
100
%left WHEN WHENNOT
101
/* unused token
102
%right COLCOL
103
*/
104
%right IMPL
105
%left OR XOR BARBAR
106
%left AND AMPERAMPER
107
%left NOT
108
/* unused precedence rule
109
%nonassoc INT
110
*/
111
%nonassoc EQ LT GT LTE GTE NEQ
112
%left MINUS PLUS
113
%left MULT DIV MOD
114
%left UMINUS
115
%left POWER
116
%left PRE
117
%nonassoc RBRACKET
118
%nonassoc LBRACKET
119

    
120
/* these XXX_main rules are used to avoid end-of-stream conflicts with
121
   menhir. See http://gallium.inria.fr/~fpottier/menhir/manual.html#sec43
122
*/
123
%start prog_main %type <Lustre_types.top_decl list>
124
prog_main
125

    
126
%start header_main
127
%type <Lustre_types.top_decl list> header_main
128

    
129
%start lustre_annot_main
130
%type <Lustre_types.expr_annot> lustre_annot_main
131

    
132
%start lustre_spec_main
133
%type <Lustre_types.contract_desc> lustre_spec_main
134

    
135
%start signed_const_main
136
%type <Lustre_types.constant> signed_const_main
137

    
138
%start expr_main
139
%type <Lustre_types.expr> expr_main
140

    
141
%start stmt_list_main
142
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list_main
143

    
144
%start vdecl_list_main
145
%type <Lustre_types.var_decl list> vdecl_list_main
146
%%
147

    
148
module_ident:
149
  UIDENT { $1 }
150
| IDENT  { $1 }
151

    
152
tag_ident:
153
  UIDENT  { $1 }
154
| TRUE    { tag_true }
155
| FALSE   { tag_false }
156

    
157
node_ident:
158
  UIDENT { $1 }
159
| IDENT  { $1 }
160

    
161
node_ident_decl:
162
 node_ident { push_node $1; $1 }
163

    
164
vdecl_ident:
165
  UIDENT { mkident $1 }
166
| IDENT  { mkident $1 }
167

    
168
const_ident:
169
  UIDENT { $1 }
170
| IDENT  { $1 }
171

    
172
type_ident:
173
  IDENT { $1 }
174

    
175
prog_main:
176
  | e = prog END { e }
177

    
178
prog:
179
 open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
180

    
181
typ_def_prog:
182
 typ_def_list { $1 false }
183

    
184
header_main:
185
  | e = header END { e }
186

    
187
header:
188
 open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) }
189

    
190
typ_def_header:
191
 typ_def_list { $1 true }
192

    
193
open_list:
194
  { [] }
195
| open_lusi open_list { $1 :: $2 }
196

    
197
open_lusi:
198
| OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))}
199
| OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) }
200

    
201
top_decl_list:
202
   {[]}
203
| top_decl_list top_decl {$2@$1}
204

    
205

    
206
top_decl_header_list:
207
   { [] }
208
| top_decl_header_list top_decl_header { $2@$1 }
209

    
210
state_annot:
211
  FUNCTION { true }
212
| NODE { false }
213

    
214
top_decl_header:
215
| CONST cdecl_list { List.rev ($2 true) }
216
| 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
217
    {let nd = mktop_decl true (ImportedNode
218
				 {nodei_id = $3;
219
				  nodei_type = Types.new_var ();
220
				  nodei_clock = Clocks.new_var true;
221
				  nodei_inputs = List.rev $5;
222
				  nodei_outputs = List.rev $10;
223
				  nodei_stateless = $2;
224
				  nodei_spec = $1;
225
				  nodei_prototype = $13;
226
				  nodei_in_lib = $14;})
227
     in
228
     (*add_imported_node $3 nd;*) [nd] }
229

    
230
prototype_opt:
231
 { None }
232
| PROTOTYPE node_ident { Some $2}
233

    
234
in_lib_list:
235
{ [] }
236
| LIB module_ident in_lib_list { $2::$3 }
237

    
238
top_decl:
239
| CONST cdecl_list { List.rev ($2 false) }
240
| 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
241
    {
242
     let stmts, asserts, annots = $16 in
243
      (* Declaring eqs annots *)
244
      List.iter (fun ann ->
245
	List.iter (fun (key, _) ->
246
	  Annotations.add_node_ann $3 key
247
	) ann.annots
248
      ) annots;
249
     (* Building the node *)
250
     let nd = mktop_decl false (Node
251
				  {node_id = $3;
252
				   node_type = Types.new_var ();
253
				   node_clock = Clocks.new_var true;
254
				   node_inputs = List.rev $5;
255
				   node_outputs = List.rev $10;
256
				   node_locals = List.rev $14;
257
				   node_gencalls = [];
258
				   node_checks = [];
259
				   node_asserts = asserts;
260
				   node_stmts = stmts;
261
				   node_dec_stateless = $2;
262
				   node_stateless = None;
263
				   node_spec = $1;
264
				   node_annot = annots})
265
     in
266
     pop_node ();
267
     (*add_node $3 nd;*) [nd] }
268

    
269
nodespec_list:
270
 { None }
271
| NODESPEC nodespec_list {
272
  (function
273
  | None    -> (fun s1 -> Some s1)
274
  | Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 }
275

    
276
typ_def_list:
277
    /* empty */             { (fun itf -> []) }
278
| typ_def SCOL typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($3 itf)) }
279

    
280
typ_def:
281
  TYPE type_ident EQ typ_def_rhs { (fun itf ->
282
			       let typ = mktop_decl itf (TypeDef { tydef_id = $2;
283
								   tydef_desc = $4
284
							})
285
			       in (*add_type itf $2 typ;*) typ) }
286

    
287
typ_def_rhs:
288
  typeconst                   { $1 }
289
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }
290
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
291

    
292
array_typ_decl:
293
 %prec POWER                { fun typ -> typ }
294
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
295

    
296
typeconst:
297
  TINT array_typ_decl   { $2 Tydec_int }
298
| TBOOL array_typ_decl  { $2 Tydec_bool  }
299
| TREAL array_typ_decl  { $2 Tydec_real  }
300
/* | TFLOAT array_typ_decl { $2 Tydec_float } */
301
| type_ident array_typ_decl  { $2 (Tydec_const $1) }
302
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }
303
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }
304

    
305
tag_list:
306
  UIDENT                { $1 :: [] }
307
| tag_list COMMA UIDENT { $3 :: $1 }
308

    
309
field_list:                           { [] }
310
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
311

    
312
stmt_list_main:
313
| e = stmt_list END { e }
314

    
315
stmt_list:
316
  { [], [], [] }
317
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
318
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
319
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
320
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
321

    
322
automaton:
323
 AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }
324

    
325
handler_list:
326
     { [] }
327
| handler handler_list { $1::$2 }
328

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

    
332
unless_list:
333
    { [] }
334
| unless unless_list { $1::$2 }
335

    
336
until_list:
337
    { [] }
338
| until until_list { $1::$2 }
339

    
340
unless:
341
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
342
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
343

    
344
until:
345
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
346
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
347

    
348
assert_:
349
| ASSERT expr SCOL {mkassert ($2)}
350

    
351
eq:
352
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
353
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
354

    
355
lustre_spec_main:
356
  | e = lustre_spec END { e }
357

    
358
lustre_spec:
359
  | contract EOF { $1 }
360

    
361
contract:
362
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
363

    
364
requires:
365
{ [] }
366
| REQUIRES qexpr SCOL requires { $2::$4 }
367

    
368
ensures:
369
{ [] }
370
| ENSURES qexpr SCOL ensures { $2 :: $4 }
371
| OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures {
372
  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
373
}
374

    
375
behaviors:
376
{ [] }
377
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
378

    
379
assumes:
380
{ [] }
381
| ASSUMES qexpr SCOL assumes { $2::$4 }
382

    
383
/* WARNING: UNREACHABLE RULE */
384
/*
385
tuple_qexpr:
386
| qexpr COMMA qexpr {[$3;$1]}
387
| tuple_qexpr COMMA qexpr {$3::$1}
388
*/
389
/* END OF UNREACHABLE RULE */
390

    
391
qexpr:
392
| expr { mkeexpr $1 }
393
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 }
394
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
395

    
396
tuple_expr:
397
  expr COMMA expr {[$3;$1]}
398
| tuple_expr COMMA expr {$3::$1}
399

    
400
// Same as tuple expr but accepting lists with single element
401
array_expr:
402
  expr {[$1]}
403
| expr COMMA array_expr {$1::$3}
404

    
405
dim_list:
406
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
407
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
408

    
409
expr_main:
410
  | e = expr END { e }
411

    
412
expr:
413
/* constants */
414
  INT {mkexpr (Expr_const (Const_int $1))}
415
| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
416
| STRING {mkexpr (Expr_const (Const_string $1))}
417

    
418
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
419
/* Idents or type enum tags */
420
| IDENT { mkexpr (Expr_ident $1) }
421
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
422
| LPAR ANNOT expr RPAR
423
    {update_expr_annot (get_current_node ()) $3 $2}
424
| LPAR expr RPAR
425
    {$2}
426
| LPAR tuple_expr RPAR
427
    {mkexpr (Expr_tuple (List.rev $2))}
428

    
429
/* Array expressions */
430
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
431
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
432
| expr LBRACKET dim_list { $3 $1 }
433

    
434
/* Temporal operators */
435
| PRE expr
436
    {mkexpr (Expr_pre $2)}
437
| expr ARROW expr
438
    {mkexpr (Expr_arrow ($1,$3))}
439
| expr FBY expr
440
    {(*mkexpr (Expr_fby ($1,$3))*)
441
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
442
| expr WHEN vdecl_ident
443
    {mkexpr (Expr_when ($1,fst $3,tag_true))}
444
| expr WHENNOT vdecl_ident
445
    {mkexpr (Expr_when ($1,fst $3,tag_false))}
446
| expr WHEN tag_ident LPAR vdecl_ident RPAR
447
    {mkexpr (Expr_when ($1, fst $5, $3))}
448
| MERGE vdecl_ident handler_expr_list
449
    {mkexpr (Expr_merge (fst $2,$3))}
450

    
451
/* Applications */
452
| node_ident LPAR expr RPAR
453
    {mkexpr (Expr_appl ($1, $3, None))}
454
| node_ident LPAR expr RPAR EVERY expr
455
    {mkexpr (Expr_appl ($1, $3, Some $6))}
456
| node_ident LPAR tuple_expr RPAR
457
    {
458
      let id=$1 in
459
      let args=List.rev $3 in
460
      match id, args with
461
      | "fbyn", [expr;n;init] ->
462
	let n = match n.expr_desc with
463
	  | Expr_const (Const_int n) -> n
464
	  | _ -> assert false
465
	in
466
	fby expr n init
467
      | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))
468
    }
469
| node_ident LPAR tuple_expr RPAR EVERY expr
470
    {
471
      let id=$1 in
472
      let args=List.rev $3 in
473
      let clock=$6 in
474
      if id="fby" then
475
	assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
476
      else
477
	mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock))
478
    }
479

    
480
/* Boolean expr */
481
| expr AND expr
482
    {mkpredef_call "&&" [$1;$3]}
483
| expr AMPERAMPER expr
484
    {mkpredef_call "&&" [$1;$3]}
485
| expr OR expr
486
    {mkpredef_call "||" [$1;$3]}
487
| expr BARBAR expr
488
    {mkpredef_call "||" [$1;$3]}
489
| expr XOR expr
490
    {mkpredef_call "xor" [$1;$3]}
491
| NOT expr
492
    {mkpredef_call "not" [$2]}
493
| expr IMPL expr
494
    {mkpredef_call "impl" [$1;$3]}
495

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

    
510
/* Arithmetic expr */
511
| expr PLUS expr
512
    {mkpredef_call "+" [$1;$3]}
513
| expr MINUS expr
514
    {mkpredef_call "-" [$1;$3]}
515
| expr MULT expr
516
    {mkpredef_call "*" [$1;$3]}
517
| expr DIV expr
518
    {mkpredef_call "/" [$1;$3]}
519
| MINUS expr %prec UMINUS
520
  {mkpredef_call "uminus" [$2]}
521
| expr MOD expr
522
    {mkpredef_call "mod" [$1;$3]}
523

    
524
/* If */
525
| IF expr THEN expr ELSE expr
526
    {mkexpr (Expr_ite ($2, $4, $6))}
527

    
528
handler_expr_list:
529
   { [] }
530
| handler_expr handler_expr_list { $1 :: $2 }
531

    
532
handler_expr:
533
 LPAR tag_ident ARROW expr RPAR { ($2, $4) }
534

    
535
signed_const_array:
536
| signed_const { [$1] }
537
| signed_const COMMA signed_const_array { $1 :: $3 }
538

    
539
signed_const_struct:
540
| IDENT EQ signed_const { [ ($1, $3) ] }
541
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
542

    
543
signed_const_main:
544
  | e = signed_const END { e }
545

    
546
signed_const:
547
  INT {Const_int $1}
548
| REAL {let c,e,s =$1 in Const_real (c,e,s)}
549
/* | FLOAT {Const_float $1} */
550
| tag_ident {Const_tag $1}
551
| MINUS INT {Const_int (-1 * $2)}
552
| MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)}
553
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
554
| LCUR signed_const_struct RCUR { Const_struct $2 }
555
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
556

    
557
dim:
558
   INT { mkdim_int $1 }
559
| LPAR dim RPAR { $2 }
560
| UIDENT { mkdim_ident $1 }
561
| IDENT { mkdim_ident $1 }
562
| dim AND dim
563
    {mkdim_appl "&&" [$1;$3]}
564
| dim AMPERAMPER dim
565
    {mkdim_appl "&&" [$1;$3]}
566
| dim OR dim
567
    {mkdim_appl "||" [$1;$3]}
568
| dim BARBAR dim
569
    {mkdim_appl "||" [$1;$3]}
570
| dim XOR dim
571
    {mkdim_appl "xor" [$1;$3]}
572
| NOT dim
573
    {mkdim_appl "not" [$2]}
574
| dim IMPL dim
575
    {mkdim_appl "impl" [$1;$3]}
576

    
577
/* Comparison dim */
578
| dim EQ dim
579
    {mkdim_appl "=" [$1;$3]}
580
| dim LT dim
581
    {mkdim_appl "<" [$1;$3]}
582
| dim LTE dim
583
    {mkdim_appl "<=" [$1;$3]}
584
| dim GT dim
585
    {mkdim_appl ">" [$1;$3]}
586
| dim GTE  dim
587
    {mkdim_appl ">=" [$1;$3]}
588
| dim NEQ dim
589
    {mkdim_appl "!=" [$1;$3]}
590

    
591
/* Arithmetic dim */
592
| dim PLUS dim
593
    {mkdim_appl "+" [$1;$3]}
594
| dim MINUS dim
595
    {mkdim_appl "-" [$1;$3]}
596
| dim MULT dim
597
    {mkdim_appl "*" [$1;$3]}
598
| dim DIV dim
599
    {mkdim_appl "/" [$1;$3]}
600
| MINUS dim %prec UMINUS
601
  {mkdim_appl "uminus" [$2]}
602
| dim MOD dim
603
    {mkdim_appl "mod" [$1;$3]}
604
/* If */
605
| IF dim THEN dim ELSE dim
606
    {mkdim_ite $2 $4 $6}
607

    
608
locals:
609
  {[]}
610
| VAR local_vdecl_list SCOL {$2}
611

    
612
vdecl_list_main:
613
  | e = vdecl_list END { e }
614

    
615
vdecl_list:
616
  vdecl {$1}
617
| vdecl_list SCOL vdecl {$3 @ $1}
618

    
619
vdecl:
620
  ident_list COL typeconst clock
621
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
622
| CONST ident_list /* static parameters don't have clocks */
623
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 }
624
| CONST ident_list COL typeconst /* static parameters don't have clocks */
625
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 }
626

    
627
local_vdecl_list:
628
  local_vdecl {$1}
629
| local_vdecl_list SCOL local_vdecl {$3 @ $1}
630

    
631
local_vdecl:
632
/* Useless no ?*/    ident_list
633
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 }
634
| ident_list COL typeconst clock
635
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
636
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
637
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] }
638
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
639
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] }
640

    
641
cdecl_list:
642
  cdecl SCOL { (fun itf -> [$1 itf]) }
643
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
644

    
645
cdecl:
646
    const_ident EQ signed_const {
647
      (fun itf ->
648
       let c = mktop_decl itf (Const {
649
				   const_id = $1;
650
				   const_loc = Location.symbol_rloc ();
651
				   const_type = Types.new_var ();
652
				   const_value = $3})
653
       in
654
       (*add_const itf $1 c;*) c)
655
    }
656

    
657
clock:
658
    {mkclock Ckdec_any}
659
| when_list
660
    {mkclock (Ckdec_bool (List.rev $1))}
661

    
662
when_cond:
663
  WHEN IDENT {($2, tag_true)}
664
| WHENNOT IDENT {($2, tag_false)}
665
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
666

    
667
when_list:
668
    when_cond {[$1]}
669
| when_list when_cond {$2::$1}
670

    
671
ident_list:
672
  vdecl_ident {[$1]}
673
| ident_list COMMA vdecl_ident {$3::$1}
674

    
675
SCOL_opt:
676
    SCOL {} | {}
677

    
678
lustre_annot_main:
679
  | e = lustre_annot END { e }
680

    
681
lustre_annot:
682
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
683

    
684
lustre_annot_list:
685
  { [] }
686
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
687
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
688
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
689
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
690
| CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 }
691
| MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 }
692

    
693

    
694
kwd:
695
DIV { [] }
696
| DIV IDENT kwd { $2::$3}
697

    
698
%%
699
(* Local Variables: *)
700
(* compile-command:"make -C .." *)
701
(* End: *)