Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 4f26dcf5

History | View | Annotate | Download (18.3 KB)

1 70e1006b xthirioux
/********************************************************************/
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 8446bf03 ploc
open Lustre_types
15 70e1006b xthirioux
open Corelang
16
open Dimension
17
open Parse
18
19
let get_loc () = Location.symbol_rloc ()
20
21 53206908 xthirioux
let mkident x = x, get_loc ()
22 70e1006b xthirioux
let mktyp x = mktyp (get_loc ()) x
23
let mkclock x = mkclock (get_loc ()) x
24 53206908 xthirioux
let mkvar_decl x loc = mkvar_decl loc ~orig:true x
25 70e1006b xthirioux
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 6394042a ploc
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 e0523910 ploc
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 70e1006b xthirioux
%}
54
55
%token <int> INT
56 53206908 xthirioux
%token <Num.num * int * string> REAL
57
58 70e1006b xthirioux
%token <string> STRING
59 4f26dcf5 ploc
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME 
60 17e1d0f4 ploc
%token ASSERT OPEN QUOTE FUNCTION
61 70e1006b xthirioux
%token <string> IDENT
62
%token <string> UIDENT
63
%token TRUE FALSE
64 8446bf03 ploc
%token <Lustre_types.expr_annot> ANNOT
65 4f26dcf5 ploc
%token <Lustre_types.contract_desc> NODESPEC
66 70e1006b xthirioux
%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 17e1d0f4 ploc
%token NODE LET TEL RETURNS VAR IMPORTED TYPE CONST
71 70e1006b xthirioux
%token STRUCT ENUM
72 53206908 xthirioux
%token TINT TREAL TBOOL TCLOCK
73 70e1006b xthirioux
%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 REQUIRES ENSURES OBSERVER
79 85da3a4b ploc
%token INVARIANT BEHAVIOR ASSUMES CCODE MATLAB
80 70e1006b xthirioux
%token EXISTS FORALL
81
%token PROTOTYPE LIB
82
%token EOF
83
84
%nonassoc prec_exists prec_forall
85
%nonassoc COMMA
86 01d48bb0 xthirioux
%nonassoc EVERY
87 70e1006b xthirioux
%left MERGE IF
88
%nonassoc ELSE
89
%right ARROW FBY
90 17e1d0f4 ploc
%left WHEN WHENNOT 
91 70e1006b xthirioux
%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 8446bf03 ploc
%type <Lustre_types.top_decl list> prog
108 70e1006b xthirioux
109
%start header
110 8446bf03 ploc
%type <Lustre_types.top_decl list> header
111 70e1006b xthirioux
112
%start lustre_annot
113 8446bf03 ploc
%type <Lustre_types.expr_annot> lustre_annot
114 70e1006b xthirioux
115
%start lustre_spec
116 4f26dcf5 ploc
%type <Lustre_types.contract_desc> lustre_spec
117 70e1006b xthirioux
118 53206908 xthirioux
%start signed_const
119 8446bf03 ploc
%type <Lustre_types.constant> signed_const
120 53206908 xthirioux
121 aa0cc4e8 ploc
%start expr
122 8446bf03 ploc
%type <Lustre_types.expr> expr
123 aa0cc4e8 ploc
124
%start stmt_list
125 8446bf03 ploc
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list
126 aa0cc4e8 ploc
127
%start vdecl_list
128 8446bf03 ploc
%type <Lustre_types.var_decl list> vdecl_list
129 70e1006b xthirioux
%%
130
131
module_ident:
132
  UIDENT { $1 }
133
| IDENT  { $1 }
134
135
tag_ident:
136
  UIDENT  { $1 }
137
| TRUE    { tag_true }
138
| FALSE   { tag_false }
139
140
node_ident:
141
  UIDENT { $1 }
142
| IDENT  { $1 }
143
144 6394042a ploc
node_ident_decl:
145
 node_ident { push_node $1; $1 }
146
147 70e1006b xthirioux
vdecl_ident:
148 53206908 xthirioux
  UIDENT { mkident $1 }
149
| IDENT  { mkident $1 }
150 70e1006b xthirioux
151
const_ident:
152
  UIDENT { $1 }
153
| IDENT  { $1 }
154
155
type_ident:
156
  IDENT { $1 }
157
158
prog:
159
 open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
160
161
typ_def_prog:
162
 typ_def_list { $1 false }
163
164
header:
165
 open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) }
166
167
typ_def_header:
168
 typ_def_list { $1 true }
169
170
open_list:
171
  { [] }
172
| open_lusi open_list { $1 :: $2 }
173
174
open_lusi:
175
| OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))}
176
| OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) }
177
178
top_decl_list:
179
   {[]}
180
| top_decl_list top_decl {$2@$1}
181
182
183
top_decl_header_list:
184
   { [] }
185
| top_decl_header_list top_decl_header { $2@$1 }
186
187
state_annot:
188
  FUNCTION { true }
189
| NODE { false }
190
191
top_decl_header:
192
| CONST cdecl_list { List.rev ($2 true) }
193 53206908 xthirioux
| 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
194 70e1006b xthirioux
    {let nd = mktop_decl true (ImportedNode
195
				 {nodei_id = $3;
196
				  nodei_type = Types.new_var ();
197
				  nodei_clock = Clocks.new_var true;
198
				  nodei_inputs = List.rev $5;
199
				  nodei_outputs = List.rev $10;
200
				  nodei_stateless = $2;
201
				  nodei_spec = $1;
202
				  nodei_prototype = $13;
203
				  nodei_in_lib = $14;})
204
     in
205
     (*add_imported_node $3 nd;*) [nd] }
206
207
prototype_opt:
208
 { None }
209
| PROTOTYPE node_ident { Some $2}
210
211 53206908 xthirioux
in_lib_list:
212
{ [] }
213
| LIB module_ident in_lib_list { $2::$3 } 
214 70e1006b xthirioux
215
top_decl:
216
| CONST cdecl_list { List.rev ($2 false) }
217 6394042a ploc
| 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 
218
    {
219 85da3a4b ploc
     let stmts, asserts, annots = $16 in
220 6394042a ploc
      (* Declaring eqs annots *)
221
      List.iter (fun ann -> 
222
	List.iter (fun (key, _) -> 
223
	  Annotations.add_node_ann $3 key
224
	) ann.annots
225
      ) annots;
226
     (* Building the node *)
227 85da3a4b ploc
     let nd = mktop_decl false (Node
228
				  {node_id = $3;
229
				   node_type = Types.new_var ();
230
				   node_clock = Clocks.new_var true;
231
				   node_inputs = List.rev $5;
232
				   node_outputs = List.rev $10;
233
				   node_locals = List.rev $14;
234
				   node_gencalls = [];
235
				   node_checks = [];
236
				   node_asserts = asserts; 
237
				   node_stmts = stmts;
238
				   node_dec_stateless = $2;
239
				   node_stateless = None;
240
				   node_spec = $1;
241
				   node_annot = annots})
242
     in
243
     pop_node ();
244 70e1006b xthirioux
     (*add_node $3 nd;*) [nd] }
245 53206908 xthirioux
246
nodespec_list:
247 70e1006b xthirioux
 { None }
248
| NODESPEC nodespec_list { 
249
  (function 
250
  | None    -> (fun s1 -> Some s1) 
251 4f26dcf5 ploc
  | Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 }
252 70e1006b xthirioux
253
typ_def_list:
254
    /* empty */             { (fun itf -> []) }
255
| typ_def SCOL typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($3 itf)) }
256
257
typ_def:
258
  TYPE type_ident EQ typ_def_rhs { (fun itf ->
259
			       let typ = mktop_decl itf (TypeDef { tydef_id = $2;
260
								   tydef_desc = $4
261
							})
262
			       in (*add_type itf $2 typ;*) typ) }
263
264
typ_def_rhs:
265
  typeconst                   { $1 }
266
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }
267
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
268
269
array_typ_decl:
270 79614a15 xthirioux
 %prec POWER                { fun typ -> typ }
271 70e1006b xthirioux
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
272
273
typeconst:
274
  TINT array_typ_decl   { $2 Tydec_int }
275
| TBOOL array_typ_decl  { $2 Tydec_bool  }
276
| TREAL array_typ_decl  { $2 Tydec_real  }
277 53206908 xthirioux
/* | TFLOAT array_typ_decl { $2 Tydec_float } */
278 70e1006b xthirioux
| type_ident array_typ_decl  { $2 (Tydec_const $1) }
279
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }
280
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }
281
282
tag_list:
283
  UIDENT                { $1 :: [] }
284
| tag_list COMMA UIDENT { $3 :: $1 }
285
      
286
field_list:                           { [] }
287
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
288
      
289 1eda3e78 xthirioux
stmt_list:
290 70e1006b xthirioux
  { [], [], [] }
291 1eda3e78 xthirioux
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
292
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
293
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
294
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
295 70e1006b xthirioux
296
automaton:
297 bc7b6c62 xthirioux
 AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }
298 70e1006b xthirioux
299
handler_list:
300
     { [] }
301
| handler handler_list { $1::$2 }
302
303
handler:
304 6a1a01d2 xthirioux
 STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
305 70e1006b xthirioux
306
unless_list:
307 29ced7be xthirioux
    { [] }
308
| unless unless_list { $1::$2 }
309 70e1006b xthirioux
310
until_list:
311 29ced7be xthirioux
    { [] }
312
| until until_list { $1::$2 }
313 70e1006b xthirioux
314
unless:
315 29ced7be xthirioux
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
316
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
317 70e1006b xthirioux
318
until:
319 29ced7be xthirioux
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
320
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
321 70e1006b xthirioux
322
assert_:
323
| ASSERT expr SCOL {mkassert ($2)}
324
325
eq:
326 53206908 xthirioux
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
327
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
328 70e1006b xthirioux
329
lustre_spec:
330
| contract EOF { $1 }
331
332
contract:
333
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
334
 
335
requires:
336
{ [] }
337
| REQUIRES qexpr SCOL requires { $2::$4 }
338
339
ensures:
340
{ [] }
341
| ENSURES qexpr SCOL ensures { $2 :: $4 }
342
| OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { 
343
  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
344
}
345
346
behaviors:
347
{ [] }
348
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
349
350
assumes:
351
{ [] }
352
| ASSUMES qexpr SCOL assumes { $2::$4 } 
353
354
/* WARNING: UNUSED RULES */
355
tuple_qexpr:
356
| qexpr COMMA qexpr {[$3;$1]}
357
| tuple_qexpr COMMA qexpr {$3::$1}
358
359
qexpr:
360
| expr { mkeexpr $1 }
361
  /* Quantifiers */
362
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
363
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
364
365
366
tuple_expr:
367
    expr COMMA expr {[$3;$1]}
368
| tuple_expr COMMA expr {$3::$1}
369
370
// Same as tuple expr but accepting lists with single element
371
array_expr:
372
  expr {[$1]}
373
| expr COMMA array_expr {$1::$3}
374
375
dim_list:
376
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
377
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
378
379
expr:
380
/* constants */
381
  INT {mkexpr (Expr_const (Const_int $1))}
382 53206908 xthirioux
| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
383 66359a5e ploc
| STRING {mkexpr (Expr_const (Const_string $1))}
384
385 53206908 xthirioux
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
386 70e1006b xthirioux
/* Idents or type enum tags */
387
| IDENT { mkexpr (Expr_ident $1) }
388
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
389
| LPAR ANNOT expr RPAR
390 6394042a ploc
    {update_expr_annot (get_current_node ()) $3 $2}
391 70e1006b xthirioux
| LPAR expr RPAR
392
    {$2}
393
| LPAR tuple_expr RPAR
394
    {mkexpr (Expr_tuple (List.rev $2))}
395
396
/* Array expressions */
397
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
398
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
399
| expr LBRACKET dim_list { $3 $1 }
400
401
/* Temporal operators */
402
| PRE expr 
403
    {mkexpr (Expr_pre $2)}
404
| expr ARROW expr 
405
    {mkexpr (Expr_arrow ($1,$3))}
406
| expr FBY expr 
407
    {(*mkexpr (Expr_fby ($1,$3))*)
408
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
409
| expr WHEN vdecl_ident
410 53206908 xthirioux
    {mkexpr (Expr_when ($1,fst $3,tag_true))}
411 70e1006b xthirioux
| expr WHENNOT vdecl_ident
412 53206908 xthirioux
    {mkexpr (Expr_when ($1,fst $3,tag_false))}
413 70e1006b xthirioux
| expr WHEN tag_ident LPAR vdecl_ident RPAR
414 53206908 xthirioux
    {mkexpr (Expr_when ($1, fst $5, $3))}
415 70e1006b xthirioux
| MERGE vdecl_ident handler_expr_list
416 53206908 xthirioux
    {mkexpr (Expr_merge (fst $2,$3))}
417 70e1006b xthirioux
418
/* Applications */
419
| node_ident LPAR expr RPAR
420
    {mkexpr (Expr_appl ($1, $3, None))}
421 6a1a01d2 xthirioux
| node_ident LPAR expr RPAR EVERY expr
422
    {mkexpr (Expr_appl ($1, $3, Some $6))}
423 70e1006b xthirioux
| node_ident LPAR tuple_expr RPAR
424 85da3a4b ploc
    {
425
      let id=$1 in
426
      let args=List.rev $3 in
427
      match id, args with
428
      | "fbyn", [expr;n;init] ->
429
	let n = match n.expr_desc with
430
	  | Expr_const (Const_int n) -> n
431
	  | _ -> assert false
432
	in
433
	fby expr n init
434
      | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))
435
    }
436 6a1a01d2 xthirioux
| node_ident LPAR tuple_expr RPAR EVERY expr
437 85da3a4b ploc
    {
438
      let id=$1 in
439
      let args=List.rev $3 in
440
      let clock=$6 in
441
      if id="fby" then
442
	assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
443
      else
444
	mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 
445
    }
446 70e1006b xthirioux
447
/* Boolean expr */
448
| expr AND expr 
449
    {mkpredef_call "&&" [$1;$3]}
450
| expr AMPERAMPER expr 
451
    {mkpredef_call "&&" [$1;$3]}
452
| expr OR expr 
453
    {mkpredef_call "||" [$1;$3]}
454
| expr BARBAR expr 
455
    {mkpredef_call "||" [$1;$3]}
456
| expr XOR expr 
457
    {mkpredef_call "xor" [$1;$3]}
458
| NOT expr 
459
    {mkpredef_call "not" [$2]}
460
| expr IMPL expr 
461
    {mkpredef_call "impl" [$1;$3]}
462
463
/* Comparison expr */
464
| expr EQ expr 
465
    {mkpredef_call "=" [$1;$3]}
466
| expr LT expr 
467
    {mkpredef_call "<" [$1;$3]}
468
| expr LTE expr 
469
    {mkpredef_call "<=" [$1;$3]}
470
| expr GT expr 
471
    {mkpredef_call ">" [$1;$3]}
472
| expr GTE  expr 
473
    {mkpredef_call ">=" [$1;$3]}
474
| expr NEQ expr 
475
    {mkpredef_call "!=" [$1;$3]}
476
477
/* Arithmetic expr */
478
| expr PLUS expr 
479
    {mkpredef_call "+" [$1;$3]}
480
| expr MINUS expr 
481
    {mkpredef_call "-" [$1;$3]}
482
| expr MULT expr 
483
    {mkpredef_call "*" [$1;$3]}
484
| expr DIV expr 
485
    {mkpredef_call "/" [$1;$3]}
486
| MINUS expr %prec UMINUS
487
  {mkpredef_call "uminus" [$2]}
488
| expr MOD expr 
489
    {mkpredef_call "mod" [$1;$3]}
490
491
/* If */
492
| IF expr THEN expr ELSE expr
493
    {mkexpr (Expr_ite ($2, $4, $6))}
494
495
handler_expr_list:
496
   { [] }
497
| handler_expr handler_expr_list { $1 :: $2 }
498
499
handler_expr:
500
 LPAR tag_ident ARROW expr RPAR { ($2, $4) }
501
502
signed_const_array:
503
| signed_const { [$1] }
504
| signed_const COMMA signed_const_array { $1 :: $3 }
505
506
signed_const_struct:
507
| IDENT EQ signed_const { [ ($1, $3) ] }
508
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
509
510
signed_const:
511
  INT {Const_int $1}
512 53206908 xthirioux
| REAL {let c,e,s =$1 in Const_real (c,e,s)}
513
/* | FLOAT {Const_float $1} */
514 70e1006b xthirioux
| tag_ident {Const_tag $1}
515
| MINUS INT {Const_int (-1 * $2)}
516 53206908 xthirioux
| MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)}
517
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
518 70e1006b xthirioux
| LCUR signed_const_struct RCUR { Const_struct $2 }
519
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
520
521
dim:
522
   INT { mkdim_int $1 }
523
| LPAR dim RPAR { $2 }
524
| UIDENT { mkdim_ident $1 }
525
| IDENT { mkdim_ident $1 }
526
| dim AND dim 
527
    {mkdim_appl "&&" [$1;$3]}
528
| dim AMPERAMPER dim 
529
    {mkdim_appl "&&" [$1;$3]}
530
| dim OR dim 
531
    {mkdim_appl "||" [$1;$3]}
532
| dim BARBAR dim 
533
    {mkdim_appl "||" [$1;$3]}
534
| dim XOR dim 
535
    {mkdim_appl "xor" [$1;$3]}
536
| NOT dim 
537
    {mkdim_appl "not" [$2]}
538
| dim IMPL dim 
539
    {mkdim_appl "impl" [$1;$3]}
540
541
/* Comparison dim */
542
| dim EQ dim 
543
    {mkdim_appl "=" [$1;$3]}
544
| dim LT dim 
545
    {mkdim_appl "<" [$1;$3]}
546
| dim LTE dim 
547
    {mkdim_appl "<=" [$1;$3]}
548
| dim GT dim 
549
    {mkdim_appl ">" [$1;$3]}
550
| dim GTE  dim 
551
    {mkdim_appl ">=" [$1;$3]}
552
| dim NEQ dim 
553
    {mkdim_appl "!=" [$1;$3]}
554
555
/* Arithmetic dim */
556
| dim PLUS dim 
557
    {mkdim_appl "+" [$1;$3]}
558
| dim MINUS dim 
559
    {mkdim_appl "-" [$1;$3]}
560
| dim MULT dim 
561
    {mkdim_appl "*" [$1;$3]}
562
| dim DIV dim 
563
    {mkdim_appl "/" [$1;$3]}
564
| MINUS dim %prec UMINUS
565
  {mkdim_appl "uminus" [$2]}
566
| dim MOD dim 
567
    {mkdim_appl "mod" [$1;$3]}
568
/* If */
569
| IF dim THEN dim ELSE dim
570
    {mkdim_ite $2 $4 $6}
571
572
locals:
573
  {[]}
574 01d48bb0 xthirioux
| VAR local_vdecl_list SCOL {$2}
575 70e1006b xthirioux
576
vdecl_list:
577 01d48bb0 xthirioux
  vdecl {$1}
578 70e1006b xthirioux
| vdecl_list SCOL vdecl {$3 @ $1}
579
580
vdecl:
581 01d48bb0 xthirioux
  ident_list COL typeconst clock 
582 66359a5e ploc
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
583 01d48bb0 xthirioux
| CONST ident_list /* static parameters don't have clocks */
584 66359a5e ploc
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 }
585 01d48bb0 xthirioux
| CONST ident_list COL typeconst /* static parameters don't have clocks */
586 66359a5e ploc
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 }
587 01d48bb0 xthirioux
588
local_vdecl_list:
589
  local_vdecl {$1}
590
| local_vdecl_list SCOL local_vdecl {$3 @ $1}
591 70e1006b xthirioux
592 01d48bb0 xthirioux
local_vdecl:
593
/* Useless no ?*/    ident_list
594 66359a5e ploc
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 }
595 70e1006b xthirioux
| ident_list COL typeconst clock 
596 66359a5e ploc
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
597 01d48bb0 xthirioux
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
598 66359a5e ploc
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] }
599 01d48bb0 xthirioux
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
600 66359a5e ploc
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] }
601 70e1006b xthirioux
602
cdecl_list:
603
  cdecl SCOL { (fun itf -> [$1 itf]) }
604
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
605
606
cdecl:
607
    const_ident EQ signed_const {
608
      (fun itf -> 
609
       let c = mktop_decl itf (Const {
610
				   const_id = $1;
611
				   const_loc = Location.symbol_rloc ();
612
				   const_type = Types.new_var ();
613
				   const_value = $3})
614
       in
615
       (*add_const itf $1 c;*) c)
616
    }
617
618
clock:
619
    {mkclock Ckdec_any}
620
| when_list
621
    {mkclock (Ckdec_bool (List.rev $1))}
622
623
when_cond:
624
  WHEN IDENT {($2, tag_true)}
625
| WHENNOT IDENT {($2, tag_false)}
626
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
627
628
when_list:
629
    when_cond {[$1]}
630
| when_list when_cond {$2::$1}
631
632
ident_list:
633
  vdecl_ident {[$1]}
634
| ident_list COMMA vdecl_ident {$3::$1}
635
636
SCOL_opt:
637
    SCOL {} | {}
638
639
640
lustre_annot:
641
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
642
643
lustre_annot_list:
644
  { [] } 
645
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
646
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
647
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
648
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
649 85da3a4b ploc
| CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 }
650
| MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 }
651
652 70e1006b xthirioux
653
kwd:
654
DIV { [] }
655
| DIV IDENT kwd { $2::$3}
656
657
%%
658
(* Local Variables: *)
659
(* compile-command:"make -C .." *)
660
(* End: *)
661
662