Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parsers / parser_lustre.mly @ 684d39e7

History | View | Annotate | Download (20.9 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 INCLUDE QUOTE POINT 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 COLCOL 
67
%token AMPERAMPER BARBAR NOT POWER
68
%token IF THEN ELSE
69
%token MERGE FBY WHEN WHENNOT EVERY
70
%token NODE LET TEL RETURNS VAR IMPORTED TYPE CONST
71
%token STRUCT ENUM
72
%token TINT TREAL TBOOL TCLOCK
73
%token EQ LT GT LTE GTE NEQ
74
%token AND OR XOR IMPL
75
%token MULT DIV MOD
76
%token MINUS PLUS UMINUS
77
%token PRE ARROW
78
%token REQUIRE ENSURE ASSUME GUARANTEES IMPORT CONTRACT
79
%token INVARIANT MODE CCODE MATLAB
80
%token EXISTS FORALL
81
%token PROTOTYPE LIB
82
%token EOF
83

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

    
106
%start prog
107
%type <Lustre_types.top_decl list> prog
108

    
109
%start header
110
%type <Lustre_types.top_decl list> header
111

    
112
%start lustre_annot
113
%type <Lustre_types.expr_annot> lustre_annot
114

    
115
%start lustre_spec
116
%type <Lustre_types.contract_desc> lustre_spec
117

    
118
%start signed_const
119
%type <Lustre_types.constant> signed_const
120

    
121
%start expr
122
%type <Lustre_types.expr> expr
123

    
124
%start stmt_list
125
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list
126

    
127
%start vdecl_list
128
%type <Lustre_types.var_decl list> vdecl_list
129
%%
130

    
131

    
132
module_ident:
133
  UIDENT { $1 }
134
| IDENT  { $1 }
135

    
136
file_ident:
137
module_ident { $1 } 
138
| module_ident POINT file_ident { $1 ^ "." ^ $3 } 
139

    
140
path_ident:
141
POINT DIV path_ident { "./" ^ $3 }
142
| file_ident DIV path_ident { $1 ^ "/" ^ $3 }
143
| DIV path_ident { "/" ^ $2 }
144
| file_ident { $1 }
145

    
146
tag_ident:
147
  UIDENT  { $1 }
148
| TRUE    { tag_true }
149
| FALSE   { tag_false }
150

    
151
node_ident:
152
  UIDENT { $1 }
153
| IDENT  { $1 }
154

    
155
node_ident_decl:
156
 node_ident { push_node $1; $1 }
157

    
158
vdecl_ident:
159
  UIDENT { mkident $1 }
160
| IDENT  { mkident $1 }
161

    
162
const_ident:
163
  UIDENT { $1 }
164
| IDENT  { $1 }
165

    
166
type_ident:
167
  IDENT { $1 }
168

    
169
prog:
170
 prefix_prog top_decl_list EOF { $1 @ (List.rev $2) }
171

    
172
prefix_prog:
173
    { [] }
174
  | open_lusi prefix_prog { $1 :: $2 }
175
  | typ_def prefix_prog   { ($1 false (* not a header *)) :: $2 }
176

    
177
prefix_header:
178
    { [] }
179
  | open_lusi prefix_header { $1 :: $2 }
180
  | typ_def prefix_header   { ($1 true (* is a header *)) :: $2 }
181

    
182
header:
183
 prefix_header top_decl_header_list EOF { $1 @ (List.rev $2) }
184

    
185

    
186
open_lusi:
187
  | OPEN QUOTE path_ident QUOTE { mktop_decl false (Open (true, $3)) }
188
  | INCLUDE QUOTE path_ident QUOTE { mktop_decl false (Include ($3)) }
189
  | OPEN LT path_ident GT { mktop_decl false (Open (false, $3))  }
190

    
191
top_decl_list:
192
   {[]}
193
| top_decl_list top_decl {$2@$1}
194

    
195

    
196
top_decl_header_list:
197
   { [] }
198
| top_decl_header_list top_decl_header { $2@$1 }
199

    
200
state_annot:
201
  FUNCTION { true }
202
| NODE { false }
203

    
204
top_decl_header:
205
| CONST cdecl_list { List.rev ($2 true) }
206
| 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
207
    {let nd = mktop_decl true (ImportedNode
208
				 {nodei_id = $3;
209
				  nodei_type = Types.new_var ();
210
				  nodei_clock = Clocks.new_var true;
211
				  nodei_inputs = List.rev $5;
212
				  nodei_outputs = List.rev $10;
213
				  nodei_stateless = $2;
214
				  nodei_spec = $1;
215
				  nodei_prototype = $13;
216
				  nodei_in_lib = $14;})
217
     in
218
     (*add_imported_node $3 nd;*) [nd] } 
219
| CONTRACT node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL 
220
    {let nd = mktop_decl true (ImportedNode
221
				 {nodei_id = $2;
222
				  nodei_type = Types.new_var ();
223
				  nodei_clock = Clocks.new_var true;
224
				  nodei_inputs = List.rev $4;
225
				  nodei_outputs = List.rev $9;
226
				  nodei_stateless = false (* By default we assume contracts as stateful *);
227
				  nodei_spec = Some $14;
228
				  nodei_prototype = None;
229
				  nodei_in_lib = [];})
230
     in
231
     (*add_imported_node $3 nd;*) [nd] }
232

    
233
prototype_opt:
234
 { None }
235
| PROTOTYPE node_ident { Some $2}
236

    
237
in_lib_list:
238
{ [] }
239
| LIB module_ident in_lib_list { $2::$3 } 
240

    
241
top_decl:
242
| CONST cdecl_list { List.rev ($2 false) }
243
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespec_list locals LET stmt_list TEL 
244
    {
245
     let stmts, asserts, annots = $16 in
246
      (* Declaring eqs annots *)
247
      List.iter (fun ann -> 
248
	List.iter (fun (key, _) -> 
249
	  Annotations.add_node_ann $2 key
250
	) ann.annots
251
      ) annots;
252
     (* Building the node *)
253
     let nd = mktop_decl false (Node
254
				  {node_id = $2;
255
				   node_type = Types.new_var ();
256
				   node_clock = Clocks.new_var true;
257
				   node_inputs = List.rev $4;
258
				   node_outputs = List.rev $9;
259
				   node_locals = List.rev $14;
260
				   node_gencalls = [];
261
				   node_checks = [];
262
				   node_asserts = asserts; 
263
				   node_stmts = stmts;
264
				   node_dec_stateless = $1;
265
				   node_stateless = None;
266
				   node_spec = $13;
267
				   node_annot = annots})
268
     in
269
     pop_node ();
270
     (*add_node $3 nd;*) [nd] }
271

    
272
| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL
273
    {let nd = mktop_decl true (ImportedNode
274
				 {nodei_id = $3;
275
				  nodei_type = Types.new_var ();
276
				  nodei_clock = Clocks.new_var true;
277
				  nodei_inputs = List.rev $5;
278
				  nodei_outputs = List.rev $10;
279
				  nodei_stateless = $1;
280
				  nodei_spec = Some $15;
281
				  nodei_prototype = None;
282
				  nodei_in_lib = [];})
283
     in
284
     pop_node ();
285
     (*add_imported_node $3 nd;*) [nd] } 
286
| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
287
    {let nd = mktop_decl true (ImportedNode
288
				 {nodei_id = $3;
289
				  nodei_type = Types.new_var ();
290
				  nodei_clock = Clocks.new_var true;
291
				  nodei_inputs = List.rev $5;
292
				  nodei_outputs = List.rev $10;
293
				  nodei_stateless = $1;
294
				  nodei_spec = None;
295
				  nodei_prototype = None;
296
				  nodei_in_lib = [];})
297
     in
298
     pop_node ();
299
     (*add_imported_node $3 nd;*) [nd] } 
300

    
301
nodespec_list:
302
 { None }
303
| NODESPEC nodespec_list { 
304
  (function 
305
  | None    -> (fun s1 -> Some s1) 
306
  | Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 }
307

    
308
typ_def_list:
309
    /* empty */             { (fun itf -> []) }
310
| typ_def typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($2 itf)) }
311

    
312
typ_def:
313
  TYPE type_ident EQ typ_def_rhs SCOL { (fun itf ->
314
			       let typ = mktop_decl itf (TypeDef { tydef_id = $2;
315
								   tydef_desc = $4
316
							})
317
			       in (*add_type itf $2 typ;*) typ) }
318

    
319
typ_def_rhs:
320
  typeconst                   { $1 }
321
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }
322
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
323

    
324
array_typ_decl:
325
 %prec POWER                { fun typ -> typ }
326
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
327

    
328
typeconst:
329
  TINT array_typ_decl   { $2 Tydec_int }
330
| TBOOL array_typ_decl  { $2 Tydec_bool  }
331
| TREAL array_typ_decl  { $2 Tydec_real  }
332
/* | TFLOAT array_typ_decl { $2 Tydec_float } */
333
| type_ident array_typ_decl  { $2 (Tydec_const $1) }
334
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }
335
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }
336

    
337
tag_list:
338
  UIDENT                { $1 :: [] }
339
| tag_list COMMA UIDENT { $3 :: $1 }
340
      
341
field_list:                           { [] }
342
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
343
      
344
stmt_list:
345
  { [], [], [] }
346
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
347
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
348
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
349
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
350

    
351
automaton:
352
 AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }
353

    
354
handler_list:
355
     { [] }
356
| handler handler_list { $1::$2 }
357

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

    
361
unless_list:
362
    { [] }
363
| unless unless_list { $1::$2 }
364

    
365
until_list:
366
    { [] }
367
| until until_list { $1::$2 }
368

    
369
unless:
370
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
371
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
372

    
373
until:
374
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
375
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
376

    
377
assert_:
378
| ASSERT expr SCOL {mkassert ($2)}
379

    
380
eq:
381
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
382
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
383

    
384
lustre_spec:
385
| contract EOF { $1 }
386

    
387
contract:
388
{ empty_contract }
389
| CONTRACT contract { $2 }
390
| CONST IDENT EQ expr SCOL contract
391
    { merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
392
| CONST IDENT COL typeconst EQ expr SCOL contract
393
    { merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
394
| VAR IDENT COL typeconst EQ expr SCOL contract
395
    { merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
396
| ASSUME qexpr SCOL contract
397
    { merge_contracts (mk_contract_assume $2) $4 }
398
| GUARANTEES qexpr SCOL contract	
399
    { merge_contracts (mk_contract_guarantees $2) $4 }
400
| MODE IDENT LPAR mode_content RPAR SCOL contract
401
	{ merge_contracts (
402
	  let r, e = $4 in 
403
	  mk_contract_mode $2 r e (get_loc())) $7 }	
404
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract
405
    { merge_contracts (mk_contract_import $2  $4  $8 (get_loc())) $11 }
406

    
407
mode_content:
408
{ [], [] }
409
| REQUIRE qexpr SCOL mode_content { let (r,e) = $4 in $2::r, e }
410
| ENSURE qexpr SCOL mode_content { let (r,e) = $4 in r, $2::e }
411

    
412
/* WARNING: UNUSED RULES */
413
tuple_qexpr:
414
| qexpr COMMA qexpr {[$3;$1]}
415
| tuple_qexpr COMMA qexpr {$3::$1}
416

    
417
qexpr:
418
| expr { mkeexpr $1 }
419
  /* Quantifiers */
420
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
421
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
422

    
423

    
424
tuple_expr:
425
    expr COMMA expr {[$3;$1]}
426
| tuple_expr COMMA expr {$3::$1}
427

    
428
// Same as tuple expr but accepting lists with single element
429
array_expr:
430
  expr {[$1]}
431
| expr COMMA array_expr {$1::$3}
432

    
433
dim_list:
434
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
435
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
436

    
437
expr:
438
/* constants */
439
  INT {mkexpr (Expr_const (Const_int $1))}
440
| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
441
| STRING {mkexpr (Expr_const (Const_string $1))}
442
| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))} 
443
    
444
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
445
/* Idents or type enum tags */
446
| IDENT { mkexpr (Expr_ident $1) }
447
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
448
| LPAR ANNOT expr RPAR
449
    {update_expr_annot (get_current_node ()) $3 $2}
450
| LPAR expr RPAR
451
    {$2}
452
| LPAR tuple_expr RPAR
453
    {mkexpr (Expr_tuple (List.rev $2))}
454

    
455
/* Array expressions */
456
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
457
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
458
| expr LBRACKET dim_list { $3 $1 }
459

    
460
/* Temporal operators */
461
| PRE expr 
462
    {mkexpr (Expr_pre $2)}
463
| expr ARROW expr 
464
    {mkexpr (Expr_arrow ($1,$3))}
465
| expr FBY expr 
466
    {(*mkexpr (Expr_fby ($1,$3))*)
467
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
468
| expr WHEN vdecl_ident
469
    {mkexpr (Expr_when ($1,fst $3,tag_true))}
470
| expr WHENNOT vdecl_ident
471
    {mkexpr (Expr_when ($1,fst $3,tag_false))}
472
| expr WHEN tag_ident LPAR vdecl_ident RPAR
473
    {mkexpr (Expr_when ($1, fst $5, $3))}
474
| MERGE vdecl_ident handler_expr_list
475
    {mkexpr (Expr_merge (fst $2,$3))}
476

    
477
/* Applications */
478
| node_ident LPAR expr RPAR
479
    {mkexpr (Expr_appl ($1, $3, None))}
480
| node_ident LPAR expr RPAR EVERY expr
481
    {mkexpr (Expr_appl ($1, $3, Some $6))}
482
| node_ident LPAR tuple_expr RPAR
483
    {
484
      let id=$1 in
485
      let args=List.rev $3 in
486
      match id, args with
487
      | "fbyn", [expr;n;init] ->
488
	let n = match n.expr_desc with
489
	  | Expr_const (Const_int n) -> n
490
	  | _ -> assert false
491
	in
492
	fby expr n init
493
      | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))
494
    }
495
| node_ident LPAR tuple_expr RPAR EVERY expr
496
    {
497
      let id=$1 in
498
      let args=List.rev $3 in
499
      let clock=$6 in
500
      if id="fby" then
501
	assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
502
      else
503
	mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 
504
    }
505

    
506
/* Boolean expr */
507
| expr AND expr 
508
    {mkpredef_call "&&" [$1;$3]}
509
| expr AMPERAMPER expr 
510
    {mkpredef_call "&&" [$1;$3]}
511
| expr OR expr 
512
    {mkpredef_call "||" [$1;$3]}
513
| expr BARBAR expr 
514
    {mkpredef_call "||" [$1;$3]}
515
| expr XOR expr 
516
    {mkpredef_call "xor" [$1;$3]}
517
| NOT expr 
518
    {mkpredef_call "not" [$2]}
519
| expr IMPL expr 
520
    {mkpredef_call "impl" [$1;$3]}
521

    
522
/* Comparison expr */
523
| expr EQ expr 
524
    {mkpredef_call "=" [$1;$3]}
525
| expr LT expr 
526
    {mkpredef_call "<" [$1;$3]}
527
| expr LTE expr 
528
    {mkpredef_call "<=" [$1;$3]}
529
| expr GT expr 
530
    {mkpredef_call ">" [$1;$3]}
531
| expr GTE  expr 
532
    {mkpredef_call ">=" [$1;$3]}
533
| expr NEQ expr 
534
    {mkpredef_call "!=" [$1;$3]}
535

    
536
/* Arithmetic expr */
537
| expr PLUS expr 
538
    {mkpredef_call "+" [$1;$3]}
539
| expr MINUS expr 
540
    {mkpredef_call "-" [$1;$3]}
541
| expr MULT expr 
542
    {mkpredef_call "*" [$1;$3]}
543
| expr DIV expr 
544
    {mkpredef_call "/" [$1;$3]}
545
| MINUS expr %prec UMINUS
546
  {mkpredef_call "uminus" [$2]}
547
| expr MOD expr 
548
    {mkpredef_call "mod" [$1;$3]}
549

    
550
/* If */
551
| IF expr THEN expr ELSE expr
552
    {mkexpr (Expr_ite ($2, $4, $6))}
553

    
554
handler_expr_list:
555
   { [] }
556
| handler_expr handler_expr_list { $1 :: $2 }
557

    
558
handler_expr:
559
 LPAR tag_ident ARROW expr RPAR { ($2, $4) }
560

    
561
signed_const_array:
562
| signed_const { [$1] }
563
| signed_const COMMA signed_const_array { $1 :: $3 }
564

    
565
signed_const_struct:
566
| IDENT EQ signed_const { [ ($1, $3) ] }
567
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
568

    
569
signed_const:
570
  INT {Const_int $1}
571
| REAL {let c,e,s =$1 in Const_real (c,e,s)}
572
/* | FLOAT {Const_float $1} */
573
| tag_ident {Const_tag $1}
574
| MINUS INT {Const_int (-1 * $2)}
575
| MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)}
576
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
577
| LCUR signed_const_struct RCUR { Const_struct $2 }
578
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
579

    
580
dim:
581
   INT { mkdim_int $1 }
582
| LPAR dim RPAR { $2 }
583
| UIDENT { mkdim_ident $1 }
584
| IDENT { mkdim_ident $1 }
585
| dim AND dim 
586
    {mkdim_appl "&&" [$1;$3]}
587
| dim AMPERAMPER dim 
588
    {mkdim_appl "&&" [$1;$3]}
589
| dim OR dim 
590
    {mkdim_appl "||" [$1;$3]}
591
| dim BARBAR dim 
592
    {mkdim_appl "||" [$1;$3]}
593
| dim XOR dim 
594
    {mkdim_appl "xor" [$1;$3]}
595
| NOT dim 
596
    {mkdim_appl "not" [$2]}
597
| dim IMPL dim 
598
    {mkdim_appl "impl" [$1;$3]}
599

    
600
/* Comparison dim */
601
| dim EQ dim 
602
    {mkdim_appl "=" [$1;$3]}
603
| dim LT dim 
604
    {mkdim_appl "<" [$1;$3]}
605
| dim LTE dim 
606
    {mkdim_appl "<=" [$1;$3]}
607
| dim GT dim 
608
    {mkdim_appl ">" [$1;$3]}
609
| dim GTE  dim 
610
    {mkdim_appl ">=" [$1;$3]}
611
| dim NEQ dim 
612
    {mkdim_appl "!=" [$1;$3]}
613

    
614
/* Arithmetic dim */
615
| dim PLUS dim 
616
    {mkdim_appl "+" [$1;$3]}
617
| dim MINUS dim 
618
    {mkdim_appl "-" [$1;$3]}
619
| dim MULT dim 
620
    {mkdim_appl "*" [$1;$3]}
621
| dim DIV dim 
622
    {mkdim_appl "/" [$1;$3]}
623
| MINUS dim %prec UMINUS
624
  {mkdim_appl "uminus" [$2]}
625
| dim MOD dim 
626
    {mkdim_appl "mod" [$1;$3]}
627
/* If */
628
| IF dim THEN dim ELSE dim
629
    {mkdim_ite $2 $4 $6}
630

    
631
locals:
632
  {[]}
633
| VAR local_vdecl_list SCOL {$2}
634

    
635
vdecl_list:
636
  vdecl {$1}
637
| vdecl_list SCOL vdecl {$3 @ $1}
638

    
639
vdecl:
640
  ident_list COL typeconst clock 
641
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
642
| CONST ident_list /* static parameters don't have clocks */
643
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 }
644
| CONST ident_list COL typeconst /* static parameters don't have clocks */
645
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 }
646

    
647
local_vdecl_list:
648
  local_vdecl {$1}
649
| local_vdecl_list SCOL local_vdecl {$3 @ $1}
650

    
651
local_vdecl:
652
/* Useless no ?*/    ident_list
653
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 }
654
| ident_list COL typeconst clock 
655
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
656
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
657
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] }
658
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
659
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] }
660

    
661
cdecl_list:
662
  cdecl SCOL { (fun itf -> [$1 itf]) }
663
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
664

    
665
cdecl:
666
    const_ident EQ signed_const {
667
      (fun itf -> 
668
       let c = mktop_decl itf (Const {
669
				   const_id = $1;
670
				   const_loc = Location.symbol_rloc ();
671
				   const_type = Types.new_var ();
672
				   const_value = $3})
673
       in
674
       (*add_const itf $1 c;*) c)
675
    }
676

    
677
clock:
678
    {mkclock Ckdec_any}
679
| when_list
680
    {mkclock (Ckdec_bool (List.rev $1))}
681

    
682
when_cond:
683
  WHEN IDENT {($2, tag_true)}
684
| WHENNOT IDENT {($2, tag_false)}
685
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
686

    
687
when_list:
688
    when_cond {[$1]}
689
| when_list when_cond {$2::$1}
690

    
691
ident_list:
692
  vdecl_ident {[$1]}
693
| ident_list COMMA vdecl_ident {$3::$1}
694

    
695
SCOL_opt:
696
    SCOL {} | {}
697

    
698

    
699
lustre_annot:
700
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
701

    
702
lustre_annot_list:
703
  { [] } 
704
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
705
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
706
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
707
// (* | OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } *)
708
| CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 }
709
| MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 }
710

    
711

    
712
kwd:
713
DIV { [] }
714
| DIV IDENT kwd { $2::$3}
715

    
716
%%
717
(* Local Variables: *)
718
(* compile-command:"make -C .." *)
719
(* End: *)
720

    
721