Project

General

Profile

Download (22 KB) Statistics
| Branch: | Tag: | Revision:
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
   
20
let get_loc () = Location.symbol_rloc ()
21

    
22
let mkident x = x, get_loc ()
23
let mktyp x = mktyp (get_loc ()) x
24
let mkclock x = mkclock (get_loc ()) x
25
let mkvar_decl x loc = mkvar_decl loc ~orig:true x
26
let mkexpr x = mkexpr (get_loc ()) x
27
let mkeexpr x = mkeexpr (get_loc ()) x 
28
let mkeq x = mkeq (get_loc ()) x
29
let mkassert x = mkassert (get_loc ()) x
30
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x
31
let mkpredef_call x = mkpredef_call (get_loc ()) x
32
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
33

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

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

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

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

    
54
 
55
%}
56

    
57
%token <int> INT
58
%token <Real.t> REAL
59

    
60
%token <string> STRING
61
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME 
62
%token ASSERT OPEN INCLUDE QUOTE POINT FUNCTION
63
%token <string> IDENT
64
%token <string> UIDENT
65
%token TRUE FALSE
66
%token <Lustre_types.expr_annot> ANNOT
67
%token <Lustre_types.spec_types> NODESPEC
68
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA 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 IMPORTED TYPE CONST
73
%token STRUCT ENUM
74
%token TINT TREAL TBOOL TCLOCK
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 REQUIRE ENSURE ASSUME GUARANTEES IMPORT CONTRACT
81
%token INVARIANT MODE CCODE MATLAB
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 
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 <Lustre_types.top_decl list> prog
110

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

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

    
117
%start lustre_spec
118
%type <Lustre_types.spec_types> lustre_spec
119

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

    
123
%start expr
124
%type <Lustre_types.expr> expr
125

    
126
%start stmt_list
127
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list
128

    
129
%start vdecl_list
130
%type <Lustre_types.var_decl list> vdecl_list
131
%%
132

    
133

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

    
138
file_ident:
139
module_ident { $1 } 
140
| module_ident POINT file_ident { $1 ^ "." ^ $3 } 
141

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

    
148
tag_bool:
149
  | TRUE    { tag_true }
150
  | FALSE   { tag_false }
151

    
152
tag_ident:
153
  UIDENT  { $1 }
154
  | tag_bool { $1 }
155

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

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

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

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

    
171
type_ident:
172
  IDENT { $1 }
173

    
174
prog:
175
 prefix_prog top_decl_list EOF { $1 @ (List.rev $2) }
176

    
177
prefix_prog:
178
    { [] }
179
  | open_lusi prefix_prog { $1 :: $2 }
180
  | typ_def prefix_prog   { ($1 false (* not a header *)) :: $2 }
181

    
182
prefix_header:
183
    { [] }
184
  | open_lusi prefix_header { $1 :: $2 }
185
  | typ_def prefix_header   { ($1 true (* is a header *)) :: $2 }
186

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

    
190

    
191
open_lusi:
192
  | OPEN QUOTE path_ident QUOTE { mktop_decl false (Open (true, $3)) }
193
  | INCLUDE QUOTE path_ident QUOTE { mktop_decl false (Include ($3)) }
194
  | OPEN LT path_ident GT { mktop_decl false (Open (false, $3))  }
195

    
196
top_decl_list:
197
   {[]}
198
| top_decl_list top_decl {$2@$1}
199

    
200

    
201
top_decl_header_list:
202
   { [] }
203
| top_decl_header_list top_decl_header { $2@$1 }
204

    
205
state_annot:
206
  FUNCTION { true }
207
| NODE { false }
208

    
209
top_decl_header:
210
| CONST cdecl_list { List.rev ($2 true) }
211
| nodespecs state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_list SCOL
212
    {
213
      let inputs = List.rev $5 in
214
      let outputs = List.rev $10 in
215
      let nd = mktop_decl true (ImportedNode
216
				 {nodei_id = $3;
217
				  nodei_type = Types.new_var ();
218
				  nodei_clock = Clocks.new_var true;
219
				  nodei_inputs = inputs;
220
				  nodei_outputs = outputs;
221
				  nodei_stateless = $2;
222
				  nodei_spec = $1;
223
				  nodei_prototype = $13;
224
				  nodei_in_lib = $14;})
225
     in
226
     pop_node ();
227
     [nd] } 
228
| top_contract { [$1] }
229

    
230

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

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

    
239
top_decl:
240
| CONST cdecl_list { List.rev ($2 false) }
241
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespecs locals LET stmt_list TEL 
242
    {
243
     let stmts, asserts, annots = $16 in
244
      (* Declaring eqs annots *)
245
      List.iter (fun ann -> 
246
	List.iter (fun (key, _) -> 
247
	  Annotations.add_node_ann $2 key
248
	) ann.annots
249
      ) annots;
250
      (* Building the node *)
251
      let inputs = List.rev $4 in
252
      let outputs = List.rev $9 in
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 = inputs;
258
				   node_outputs = outputs;
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
				   node_iscontract = false;
269
			       })
270
     in
271
     pop_node ();
272
     (*add_node $3 nd;*) [nd] }
273

    
274

    
275
| NODESPEC
276
    { match $1 with
277
      | LocalContract c -> assert false
278
      | TopContract c   -> c
279
			 
280
    }
281

    
282
nodespecs:
283
nodespec_list {
284
  match $1 with
285
  | None -> None 
286
  | Some c -> Some (Contract c)
287
}
288

    
289
nodespec_list:
290
 { None }
291
  | NODESPEC nodespec_list {
292
	       let extract x = match x with LocalContract c -> c | _ -> assert false in
293
	       let s1 = extract $1 in
294
	       match $2 with
295
	       | None -> Some s1
296
	       | Some s2 -> Some (merge_contracts s1 s2) }
297

    
298
typ_def_list:
299
    /* empty */             { (fun itf -> []) }
300
| typ_def typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($2 itf)) }
301

    
302
typ_def:
303
  TYPE type_ident EQ typ_def_rhs SCOL { (fun itf ->
304
			       let typ = mktop_decl itf (TypeDef { tydef_id = $2;
305
								   tydef_desc = $4
306
							})
307
			       in (*add_type itf $2 typ;*) typ) }
308

    
309
typ_def_rhs:
310
  typeconst                   { $1 }
311
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }
312
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
313

    
314
array_typ_decl:
315
 %prec POWER                { fun typ -> typ }
316
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
317

    
318
typeconst:
319
  TINT array_typ_decl   { $2 Tydec_int }
320
| TBOOL array_typ_decl  { $2 Tydec_bool  }
321
| TREAL array_typ_decl  { $2 Tydec_real  }
322
/* | TFLOAT array_typ_decl { $2 Tydec_float } */
323
| type_ident array_typ_decl  { $2 (Tydec_const $1) }
324
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }
325
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }
326

    
327
tag_list:
328
  UIDENT                { $1 :: [] }
329
| tag_list COMMA UIDENT { $3 :: $1 }
330
      
331
field_list:                           { [] }
332
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
333
      
334
stmt_list:
335
  { [], [], [] }
336
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
337
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
338
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
339
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
340

    
341
automaton:
342
 AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }
343

    
344
handler_list:
345
     { [] }
346
| handler handler_list { $1::$2 }
347

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

    
351
unless_list:
352
    { [] }
353
| unless unless_list { $1::$2 }
354

    
355
until_list:
356
    { [] }
357
| until until_list { $1::$2 }
358

    
359
unless:
360
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
361
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
362

    
363
until:
364
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
365
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
366

    
367
assert_:
368
| ASSERT expr SCOL {mkassert ($2)}
369

    
370
eq:
371
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
372
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
373

    
374
lustre_spec:
375
| top_contracts EOF     { TopContract $1 }
376
| contract_content EOF { LocalContract $1}
377

    
378
top_contracts:
379
| top_contract { [$1] }
380
| top_contract top_contracts { $1::$2 }
381

    
382
top_contract:
383
| CONTRACT node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract_content TEL 
384
    {
385
      let nd = mktop_decl true (Node
386
				 {node_id = $2;
387
				  node_type = Types.new_var ();
388
				  node_clock = Clocks.new_var true;
389
				  node_inputs = List.rev $4;
390
				  node_outputs = List.rev $9;
391
				  node_locals = []; (* will be filled later *)
392
				  node_gencalls = [];
393
				  node_checks = [];
394
				  node_asserts = [];
395
				  node_stmts = []; (* will be filled later *)
396
				  node_dec_stateless = false;
397
				  (* By default we assume contracts as stateful *)
398
				  node_stateless = None;
399
				  node_spec = Some (Contract $14);
400
				  node_annot = [];
401
				  node_iscontract = true;
402
				 }
403
			       )
404
     in
405
     pop_node ();
406
     (*add_imported_node $3 nd;*)
407
     nd }
408

    
409
contract_content:
410
{ empty_contract }
411
| CONTRACT contract_content { $2 }
412
| CONST IDENT EQ expr SCOL contract_content
413
    { merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
414
| CONST IDENT COL typeconst EQ expr SCOL contract_content
415
    { merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
416
| VAR IDENT COL typeconst EQ expr SCOL contract_content
417
    { merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
418
| ASSUME qexpr SCOL contract_content
419
    { merge_contracts (mk_contract_assume $2) $4 }
420
| ASSUME STRING qexpr SCOL contract_content
421
    { merge_contracts (mk_contract_assume ~name:$2 $3) $5 }
422
| GUARANTEES qexpr SCOL contract_content	
423
    { merge_contracts (mk_contract_guarantees $2) $4 }
424
| GUARANTEES STRING qexpr SCOL contract_content	
425
    { merge_contracts (mk_contract_guarantees ~name:$2 $3) $5 }
426
| MODE IDENT LPAR mode_content RPAR SCOL contract_content
427
	{ merge_contracts (
428
	  let r, e = $4 in 
429
	  mk_contract_mode $2 r e (get_loc())) $7 }	
430
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content
431
    { merge_contracts (mk_contract_import $2  (mkexpr (Expr_tuple (List.rev $4)))  (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }
432
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content
433
    { merge_contracts (mk_contract_import $2  $4  (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }
434
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
435
    { merge_contracts (mk_contract_import $2  (mkexpr (Expr_tuple (List.rev $4)))  $8 (get_loc())) $11 }
436
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
437
    { merge_contracts (mk_contract_import $2  $4  $8 (get_loc())) $11 }
438

    
439
mode_content:
440
{ [], [] }
441
| REQUIRE qexpr SCOL mode_content { let (r,e) = $4 in $2::r, e }
442
| REQUIRE STRING qexpr SCOL mode_content { let (r,e) = $5 in {$3 with eexpr_name = Some $2}::r, e }
443
| ENSURE qexpr SCOL mode_content { let (r,e) = $4 in r, $2::e }
444
| ENSURE STRING qexpr SCOL mode_content { let (r,e) = $5 in r, {$3 with eexpr_name = Some $2}::e }
445

    
446
/* WARNING: UNUSED RULES */
447
tuple_qexpr:
448
| qexpr COMMA qexpr {[$3;$1]}
449
| tuple_qexpr COMMA qexpr {$3::$1}
450

    
451
qexpr:
452
| expr { mkeexpr $1 }
453
  /* Quantifiers */
454
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
455
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
456

    
457

    
458
tuple_expr:
459
    expr COMMA expr {[$3;$1]}
460
| tuple_expr COMMA expr {$3::$1}
461

    
462
// Same as tuple expr but accepting lists with single element
463
array_expr:
464
  expr {[$1]}
465
| expr COMMA array_expr {$1::$3}
466

    
467
dim_list:
468
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
469
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
470

    
471
expr:
472
/* constants */
473
  INT {mkexpr (Expr_const (Const_int $1))}
474
| REAL {mkexpr (Expr_const (Const_real $1))}
475
| STRING {mkexpr (Expr_const (Const_string $1))}
476
| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))} 
477
    
478
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
479
/* Idents or type enum tags */
480
| IDENT { mkexpr (Expr_ident $1) }
481
| UIDENT { mkexpr (Expr_ident $1) (* TODO we will differenciate enum constants from variables later *) }
482
| tag_bool {
483
	(* on sept 2014, X chenged the Const to 
484
	mkexpr (Expr_ident $1)
485
	reverted back to const on july 2019 *)
486
	mkexpr (Expr_const (Const_tag $1)) }
487
| LPAR ANNOT expr RPAR
488
    {update_expr_annot (get_current_node ()) $3 $2}
489
| LPAR expr RPAR
490
    {$2}
491
| LPAR tuple_expr RPAR
492
    {mkexpr (Expr_tuple (List.rev $2))}
493

    
494
/* Array expressions */
495
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
496
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
497
| expr LBRACKET dim_list { $3 $1 }
498

    
499
/* Temporal operators */
500
| PRE expr 
501
    {mkexpr (Expr_pre $2)}
502
| expr ARROW expr 
503
    {mkexpr (Expr_arrow ($1,$3))}
504
| expr FBY expr 
505
    {(*mkexpr (Expr_fby ($1,$3))*)
506
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
507
| expr WHEN vdecl_ident
508
    {mkexpr (Expr_when ($1,fst $3,tag_true))}
509
| expr WHENNOT vdecl_ident
510
    {mkexpr (Expr_when ($1,fst $3,tag_false))}
511
| expr WHEN tag_ident LPAR vdecl_ident RPAR
512
    {mkexpr (Expr_when ($1, fst $5, $3))}
513
| MERGE vdecl_ident handler_expr_list
514
    {mkexpr (Expr_merge (fst $2,$3))}
515

    
516
/* Applications */
517
| node_ident LPAR expr RPAR
518
    {mkexpr (Expr_appl ($1, $3, None))}
519
| node_ident LPAR expr RPAR EVERY expr
520
    {mkexpr (Expr_appl ($1, $3, Some $6))}
521
| node_ident LPAR tuple_expr RPAR
522
    {
523
      let id=$1 in
524
      let args=List.rev $3 in
525
      match id, args with
526
      | "fbyn", [expr;n;init] ->
527
	let n = match n.expr_desc with
528
	  | Expr_const (Const_int n) -> n
529
	  | _ -> assert false
530
	in
531
	fby expr n init
532
      | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))
533
    }
534
| node_ident LPAR tuple_expr RPAR EVERY expr
535
    {
536
      let id=$1 in
537
      let args=List.rev $3 in
538
      let clock=$6 in
539
      if id="fby" then
540
	assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
541
      else
542
	mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 
543
    }
544

    
545
/* Boolean expr */
546
| expr AND expr 
547
    {mkpredef_call "&&" [$1;$3]}
548
| expr AMPERAMPER expr 
549
    {mkpredef_call "&&" [$1;$3]}
550
| expr OR expr 
551
    {mkpredef_call "||" [$1;$3]}
552
| expr BARBAR expr 
553
    {mkpredef_call "||" [$1;$3]}
554
| expr XOR expr 
555
    {mkpredef_call "xor" [$1;$3]}
556
| NOT expr 
557
    {mkpredef_call "not" [$2]}
558
| expr IMPL expr 
559
    {mkpredef_call "impl" [$1;$3]}
560

    
561
/* Comparison expr */
562
| expr EQ expr 
563
    {mkpredef_call "=" [$1;$3]}
564
| expr LT expr 
565
    {mkpredef_call "<" [$1;$3]}
566
| expr LTE expr 
567
    {mkpredef_call "<=" [$1;$3]}
568
| expr GT expr 
569
    {mkpredef_call ">" [$1;$3]}
570
| expr GTE  expr 
571
    {mkpredef_call ">=" [$1;$3]}
572
| expr NEQ expr 
573
    {mkpredef_call "!=" [$1;$3]}
574

    
575
/* Arithmetic expr */
576
| expr PLUS expr 
577
    {mkpredef_call "+" [$1;$3]}
578
| expr MINUS expr 
579
    {mkpredef_call "-" [$1;$3]}
580
| expr MULT expr 
581
    {mkpredef_call "*" [$1;$3]}
582
| expr DIV expr 
583
    {mkpredef_call "/" [$1;$3]}
584
| MINUS expr %prec UMINUS
585
  {mkpredef_call "uminus" [$2]}
586
| expr MOD expr 
587
    {mkpredef_call "mod" [$1;$3]}
588

    
589
/* If */
590
| IF expr THEN expr ELSE expr
591
    {mkexpr (Expr_ite ($2, $4, $6))}
592

    
593
handler_expr_list:
594
   { [] }
595
| handler_expr handler_expr_list { $1 :: $2 }
596

    
597
handler_expr:
598
 LPAR tag_ident ARROW expr RPAR { ($2, $4) }
599

    
600
signed_const_array:
601
| signed_const { [$1] }
602
| signed_const COMMA signed_const_array { $1 :: $3 }
603

    
604
signed_const_struct:
605
| IDENT EQ signed_const { [ ($1, $3) ] }
606
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
607

    
608
signed_const:
609
  INT {Const_int $1}
610
| REAL {Const_real $1}
611
/* | FLOAT {Const_float $1} */
612
| tag_ident {Const_tag $1}
613
| MINUS INT {Const_int (-1 * $2)}
614
| MINUS REAL {Const_real (Real.uminus $2)}
615
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
616
| LCUR signed_const_struct RCUR { Const_struct $2 }
617
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
618

    
619
dim:
620
   INT { mkdim_int $1 }
621
| LPAR dim RPAR { $2 }
622
| UIDENT { mkdim_ident $1 }
623
| IDENT { mkdim_ident $1 }
624
| dim AND dim 
625
    {mkdim_appl "&&" [$1;$3]}
626
| dim AMPERAMPER dim 
627
    {mkdim_appl "&&" [$1;$3]}
628
| dim OR dim 
629
    {mkdim_appl "||" [$1;$3]}
630
| dim BARBAR dim 
631
    {mkdim_appl "||" [$1;$3]}
632
| dim XOR dim 
633
    {mkdim_appl "xor" [$1;$3]}
634
| NOT dim 
635
    {mkdim_appl "not" [$2]}
636
| dim IMPL dim 
637
    {mkdim_appl "impl" [$1;$3]}
638

    
639
/* Comparison dim */
640
| dim EQ dim 
641
    {mkdim_appl "=" [$1;$3]}
642
| dim LT dim 
643
    {mkdim_appl "<" [$1;$3]}
644
| dim LTE dim 
645
    {mkdim_appl "<=" [$1;$3]}
646
| dim GT dim 
647
    {mkdim_appl ">" [$1;$3]}
648
| dim GTE  dim 
649
    {mkdim_appl ">=" [$1;$3]}
650
| dim NEQ dim 
651
    {mkdim_appl "!=" [$1;$3]}
652

    
653
/* Arithmetic dim */
654
| dim PLUS dim 
655
    {mkdim_appl "+" [$1;$3]}
656
| dim MINUS dim 
657
    {mkdim_appl "-" [$1;$3]}
658
| dim MULT dim 
659
    {mkdim_appl "*" [$1;$3]}
660
| dim DIV dim 
661
    {mkdim_appl "/" [$1;$3]}
662
| MINUS dim %prec UMINUS
663
  {mkdim_appl "uminus" [$2]}
664
| dim MOD dim 
665
    {mkdim_appl "mod" [$1;$3]}
666
/* If */
667
| IF dim THEN dim ELSE dim
668
    {mkdim_ite $2 $4 $6}
669

    
670
locals:
671
  {[]}
672
| VAR local_vdecl_list SCOL {$2}
673

    
674
vdecl_list:
675
  vdecl {$1}
676
| vdecl_list SCOL vdecl {$3 @ $1}
677

    
678
vdecl:
679
  ident_list COL typeconst clock 
680
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
681
| CONST ident_list /* static parameters don't have clocks */
682
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 }
683
| CONST ident_list COL typeconst /* static parameters don't have clocks */
684
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 }
685

    
686
local_vdecl_list:
687
  local_vdecl {$1}
688
| local_vdecl_list SCOL local_vdecl {$3 @ $1}
689

    
690
local_vdecl:
691
/* Useless no ?*/    ident_list
692
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 }
693
| ident_list COL typeconst clock 
694
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
695
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
696
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] }
697
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
698
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] }
699

    
700
cdecl_list:
701
  cdecl SCOL { (fun itf -> [$1 itf]) }
702
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
703

    
704
cdecl:
705
    const_ident EQ signed_const {
706
      (fun itf -> 
707
       let c = mktop_decl itf (Const {
708
				   const_id = $1;
709
				   const_loc = get_loc ();
710
				   const_type = Types.new_var ();
711
				   const_value = $3})
712
       in
713
       (*add_const itf $1 c;*) c)
714
    }
715

    
716
clock:
717
    {mkclock Ckdec_any}
718
| when_list
719
    {mkclock (Ckdec_bool (List.rev $1))}
720

    
721
when_cond:
722
  WHEN IDENT {($2, tag_true)}
723
| WHENNOT IDENT {($2, tag_false)}
724
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
725

    
726
when_list:
727
    when_cond {[$1]}
728
| when_list when_cond {$2::$1}
729

    
730
ident_list:
731
  vdecl_ident {[$1]}
732
| ident_list COMMA vdecl_ident {$3::$1}
733

    
734
SCOL_opt:
735
    SCOL {} | {}
736

    
737

    
738
lustre_annot:
739
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
740

    
741
lustre_annot_list:
742
  { [] } 
743
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
744
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
745
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
746
// (* | OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } *)
747
| CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 }
748
| MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 }
749

    
750

    
751
kwd:
752
DIV { [] }
753
| DIV IDENT kwd { $2::$3}
754

    
755
%%
756
(* Local Variables: *)
757
(* compile-command:"make -C .." *)
758
(* End: *)
759

    
760

    
(8-8/8)