Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / lib / parsers / parser_lustre.mly @ 9b0432bc

History | View | Annotate | Download (22 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

    
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

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

    
59
%token <string> STRING
60
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME 
61
%token ASSERT OPEN INCLUDE QUOTE POINT FUNCTION
62
%token <string> IDENT
63
%token <string> UIDENT
64
%token TRUE FALSE
65
%token <Lustre_types.expr_annot> ANNOT
66
%token <Lustre_types.spec_types> NODESPEC
67
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
68
%token AMPERAMPER BARBAR NOT POWER
69
%token IF THEN ELSE
70
%token MERGE FBY WHEN WHENNOT EVERY
71
%token NODE LET TEL RETURNS VAR IMPORTED TYPE CONST
72
%token STRUCT ENUM
73
%token TINT TREAL TBOOL TCLOCK
74
%token EQ LT GT LTE GTE NEQ
75
%token AND OR XOR IMPL
76
%token MULT DIV MOD
77
%token MINUS PLUS UMINUS
78
%token PRE ARROW
79
%token REQUIRE ENSURE ASSUME GUARANTEES IMPORT CONTRACT
80
%token INVARIANT MODE CCODE MATLAB
81
%token EXISTS FORALL
82
%token PROTOTYPE LIB
83
%token EOF
84

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

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

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

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

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

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

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

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

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

    
132

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

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

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

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

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

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

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

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

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

    
170
type_ident:
171
  IDENT { $1 }
172

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

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

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

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

    
189

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

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

    
199

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

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

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

    
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
| 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 
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 $2 key
247
	) ann.annots
248
      ) annots;
249
      (* Building the node *)
250
      let inputs = List.rev $4 in
251
      let outputs = List.rev $9 in
252
     let nd = mktop_decl false (Node
253
				  {node_id = $2;
254
				   node_type = Types.new_var ();
255
				   node_clock = Clocks.new_var true;
256
				   node_inputs = inputs;
257
				   node_outputs = outputs;
258
				   node_locals = List.rev $14;
259
				   node_gencalls = [];
260
				   node_checks = [];
261
				   node_asserts = asserts; 
262
				   node_stmts = stmts;
263
				   node_dec_stateless = $1;
264
				   node_stateless = None;
265
				   node_spec = $13;
266
				   node_annot = annots;
267
				   node_iscontract = false;
268
			       })
269
     in
270
     pop_node ();
271
     (*add_node $3 nd;*) [nd] }
272

    
273

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
456

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
733
SCOL_opt:
734
    SCOL {} | {}
735

    
736

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

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

    
749

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

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

    
759