Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 22fe1c93

History | View | Annotate | Download (15.1 KB)

1
/* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- */
22

    
23
%{
24
open LustreSpec
25
open Corelang
26
open Dimension
27
open Utils
28

    
29
let mktyp x = mktyp (Location.symbol_rloc ()) x
30
let mkclock x = mkclock (Location.symbol_rloc ()) x
31
let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x
32
let mkexpr x = mkexpr (Location.symbol_rloc ()) x
33
let mkeq x = mkeq (Location.symbol_rloc ()) x
34
let mkassert x = mkassert (Location.symbol_rloc ()) x
35
let mktop_decl x = mktop_decl (Location.symbol_rloc ()) x
36
let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x
37
let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x
38

    
39
let mkdim_int i = mkdim_int (Location.symbol_rloc ()) i
40
let mkdim_bool b = mkdim_bool (Location.symbol_rloc ()) b
41
let mkdim_ident id = mkdim_ident (Location.symbol_rloc ()) id
42
let mkdim_appl f args = mkdim_appl (Location.symbol_rloc ()) f args
43
let mkdim_ite i t e = mkdim_ite (Location.symbol_rloc ()) i t e
44

    
45
%}
46

    
47
%token <int> INT
48
%token <string> REAL
49
%token <float> FLOAT
50
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
51
%token STATELESS ASSERT INCLUDE QUOTE FUNCTION
52
%token <string> IDENT
53
%token <LustreSpec.expr_annot> ANNOT
54
%token <LustreSpec.node_annot> NODESPEC
55
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
56
%token AMPERAMPER BARBAR NOT POWER
57
%token IF THEN ELSE
58
%token UCLOCK DCLOCK PHCLOCK TAIL
59
%token MERGE FBY WHEN WHENNOT EVERY
60
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
61
%token STRUCT ENUM
62
%token TINT TFLOAT TREAL TBOOL TCLOCK
63
%token RATE DUE
64
%token EQ LT GT LTE GTE NEQ
65
%token AND OR XOR IMPL
66
%token MULT DIV MOD
67
%token MINUS PLUS UMINUS
68
%token PRE ARROW
69

    
70
%token EOF
71

    
72
%nonassoc COMMA
73
%left MERGE IF
74
%nonassoc ELSE
75
%right ARROW FBY
76
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
77
%right COLCOL
78
%right IMPL
79
%left OR XOR BARBAR
80
%left AND AMPERAMPER
81
%left NOT
82
%nonassoc INT
83
%nonassoc EQ LT GT LTE GTE NEQ
84
%left MINUS PLUS
85
%left MULT DIV MOD
86
%left UMINUS
87
%left POWER
88
%left PRE LAST
89
%nonassoc RBRACKET
90
%nonassoc LBRACKET
91

    
92
%start prog
93
%type <Corelang.top_decl list> prog
94

    
95
%%
96

    
97
prog:
98
    typ_def_list top_decl_list EOF {$1;(List.rev $2)}
99

    
100
top_decl_list:
101
  top_decl {[$1]}
102
| top_decl_list top_decl {$2::$1}
103

    
104
top_decl:
105
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
106

    
107
| NODE IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
108
    {let eqs, asserts, annots = $14 in
109
     let nd = mktop_decl (Node
110
                            {node_id = $2;
111
                             node_type = Types.new_var ();
112
                             node_clock = Clocks.new_var true;
113
                             node_inputs = List.rev $4;
114
                             node_outputs = List.rev $8;
115
                             node_locals = List.rev $12;
116
			     node_gencalls = [];
117
			     node_checks = [];
118
			     node_asserts = asserts; 
119
                             node_eqs = eqs;
120
			     node_spec = None;
121
			     node_annot = match annots with [] -> None | _ -> Some annots})
122
    in
123
    Hashtbl.add node_table $2 nd; nd}
124

    
125
| nodespec_list NODE IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
126
    {let eqs, asserts, annots = $15 in
127
     let nd = mktop_decl (Node
128
                            {node_id = $3;
129
                             node_type = Types.new_var ();
130
                             node_clock = Clocks.new_var true;
131
                             node_inputs = List.rev $5;
132
                             node_outputs = List.rev $9;
133
                             node_locals = List.rev $13;
134
			     node_gencalls = [];
135
			     node_checks = [];
136
			     node_asserts = asserts; 
137
                             node_eqs = eqs;
138
			     node_spec = Some $1;
139
			     node_annot = match annots with [] -> None | _ -> Some annots})
140
    in
141
    Hashtbl.add node_table $3 nd; nd}
142

    
143
| IMPORTED NODE IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list RPAR stateless_opt SCOL
144
    {let nd = mktop_decl (ImportedNode
145
                            {nodei_id = $3;
146
                             nodei_type = Types.new_var ();
147
                             nodei_clock = Clocks.new_var true;
148
                             nodei_inputs = List.rev $5;
149
                             nodei_outputs = List.rev $9;
150
			     nodei_stateless = $11;
151
			     nodei_spec = None})
152
    in
153
    Hashtbl.add node_table $3 nd; nd}
154

    
155
| nodespec_list IMPORTED NODE IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list RPAR stateless_opt SCOL
156
    {let nd = mktop_decl (ImportedNode
157
                            {nodei_id = $4;
158
                             nodei_type = Types.new_var ();
159
                             nodei_clock = Clocks.new_var true;
160
                             nodei_inputs = List.rev $6;
161
                             nodei_outputs = List.rev $10;
162
			     nodei_stateless = $12;
163
			     nodei_spec = Some $1})
164
    in
165
    Hashtbl.add node_table $4 nd; nd}
166

    
167
| FUNCTION IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list RPAR SCOL
168
    {let nd = mktop_decl (ImportedNode
169
                            {nodei_id = $2;
170
                             nodei_type = Types.new_var ();
171
			     nodei_clock = Clocks.new_var true;
172
                             nodei_inputs = List.rev $4;
173
                             nodei_outputs = List.rev $8;
174
			     nodei_stateless = true;
175
			     nodei_spec = None})
176
     in
177
     Hashtbl.add node_table $2 nd; nd}
178

    
179
| nodespec_list FUNCTION IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list RPAR SCOL
180
    {let nd = mktop_decl (ImportedNode
181
                            {nodei_id = $3;
182
                             nodei_type = Types.new_var ();
183
			     nodei_clock = Clocks.new_var true;
184
                             nodei_inputs = List.rev $5;
185
                             nodei_outputs = List.rev $9;
186
			     nodei_stateless = true;
187
			     nodei_spec = Some $1})
188
     in
189
    Hashtbl.add node_table $3 nd; nd}
190

    
191
| INCLUDE QUOTE IDENT QUOTE { mktop_decl (Include $3) }
192

    
193
nodespec_list:
194
NODESPEC { $1 }
195
| NODESPEC nodespec_list { LustreSpec.merge_node_annot $1 $2 }
196

    
197
stateless_opt:
198
   { false }
199
| STATELESS {true}
200

    
201
typ_def_list:
202
    /* empty */ {}
203
| typ_def SCOL typ_def_list {$1;$3}
204

    
205
typ_def:
206
  TYPE IDENT EQ typeconst {
207
    try
208
      Hashtbl.add type_table (Tydec_const $2) (Corelang.get_repr_type $4)
209
    with Not_found-> raise (Corelang.Unbound_type ($4, Location.symbol_rloc())) }
210
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
211
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) Tydec_any }
212

    
213
array_typ_decl:
214
                            { fun typ -> typ }
215
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
216

    
217
typeconst:
218
  TINT array_typ_decl  { $2 Tydec_int }
219
| TBOOL array_typ_decl { $2 Tydec_bool  }
220
| TREAL array_typ_decl { $2 Tydec_real  }
221
| TFLOAT array_typ_decl { $2 Tydec_float }
222
| IDENT array_typ_decl { $2 (Tydec_const $1) }
223
| TBOOL TCLOCK  { Tydec_clock Tydec_bool }
224
| IDENT TCLOCK  { Tydec_clock (Tydec_const $1) }
225

    
226
tag_list:
227
  IDENT
228
  { (fun t -> if Hashtbl.mem tag_table $1
229
             then raise (Corelang.Already_bound_label ($1, t, Location.symbol_rloc ()))
230
             else (Hashtbl.add tag_table $1 t; $1 :: [])) }
231
| tag_list COMMA IDENT
232
  { (fun t -> if Hashtbl.mem tag_table $3
233
             then raise (Corelang.Already_bound_label ($3, t, Location.symbol_rloc ()))
234
             else (Hashtbl.add tag_table $3 t; $3 :: ($1 t))) }
235

    
236
field_list:
237
   { [] }
238
| IDENT COL typeconst SCOL field_list { ($1, $3) :: $5 }
239

    
240
eq_list:
241
  { [], [], [] }
242
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
243
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
244
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}
245
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
246

    
247
automaton:
248
 AUTOMATON IDENT handler_list { failwith "not implemented" }
249

    
250
handler_list:
251
     { [] }
252
| handler handler_list { $1::$2 }
253

    
254
handler:
255
 STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
256

    
257
unless_list:
258
    { [] }
259
| unless unless_list { $1::$2 }
260

    
261
until_list:
262
    { [] }
263
| until until_list { $1::$2 }
264

    
265
unless:
266
  UNLESS expr RESTART IDENT { }
267
| UNLESS expr RESUME IDENT  { }
268

    
269
until:
270
  UNTIL expr RESTART IDENT { }
271
| UNTIL expr RESUME IDENT  { }
272

    
273
assert_:
274
| ASSERT expr SCOL {mkassert ($2)}
275

    
276
eq:
277
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
278
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
279

    
280
tuple_expr:
281
    expr COMMA expr {[$3;$1]}
282
| tuple_expr COMMA expr {$3::$1}
283

    
284
// Same as tuple expr but accepting lists with single element
285
array_expr:
286
  expr {[$1]}
287
| expr COMMA array_expr {$1::$3}
288

    
289
dim_list:
290
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
291
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
292

    
293
expr:
294
/* constants */
295
  INT {mkexpr (Expr_const (Const_int $1))}
296
| REAL {mkexpr (Expr_const (Const_real $1))}
297
| FLOAT {mkexpr (Expr_const (Const_float $1))}
298
/* Idents or type enum tags */
299
| IDENT {
300
  if Hashtbl.mem tag_table $1
301
  then mkexpr (Expr_const (Const_tag $1))
302
  else mkexpr (Expr_ident $1)}
303
| LPAR ANNOT expr RPAR
304
    {update_expr_annot $3 $2}
305
| LPAR expr RPAR
306
    {$2}
307
| LPAR tuple_expr RPAR
308
    {mkexpr (Expr_tuple (List.rev $2))}
309

    
310
/* Array expressions */
311
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
312
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
313
| expr LBRACKET dim_list { $3 $1 }
314

    
315
/* Temporal operators */
316
| PRE expr 
317
    {mkexpr (Expr_pre $2)}
318
| expr ARROW expr 
319
    {mkexpr (Expr_arrow ($1,$3))}
320
| expr FBY expr 
321
    {(*mkexpr (Expr_fby ($1,$3))*)
322
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
323
| expr WHEN IDENT 
324
    {mkexpr (Expr_when ($1,$3,tag_true))}
325
| expr WHENNOT IDENT
326
    {mkexpr (Expr_when ($1,$3,tag_false))}
327
| expr WHEN IDENT LPAR IDENT RPAR
328
    {mkexpr (Expr_when ($1, $5, $3))}
329
| MERGE IDENT handler_expr_list
330
    {mkexpr (Expr_merge ($2,$3))}
331

    
332
/* Applications */
333
| IDENT LPAR expr RPAR
334
    {mkexpr (Expr_appl ($1, $3, None))}
335
| IDENT LPAR expr RPAR EVERY IDENT
336
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
337
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
338
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
339
| IDENT LPAR tuple_expr RPAR
340
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
341
| IDENT LPAR tuple_expr RPAR EVERY IDENT
342
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
343
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
344
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
345

    
346
/* Boolean expr */
347
| expr AND expr 
348
    {mkpredef_call "&&" [$1;$3]}
349
| expr AMPERAMPER expr 
350
    {mkpredef_call "&&" [$1;$3]}
351
| expr OR expr 
352
    {mkpredef_call "||" [$1;$3]}
353
| expr BARBAR expr 
354
    {mkpredef_call "||" [$1;$3]}
355
| expr XOR expr 
356
    {mkpredef_call "xor" [$1;$3]}
357
| NOT expr 
358
    {mkpredef_unary_call "not" $2}
359
| expr IMPL expr 
360
    {mkpredef_call "impl" [$1;$3]}
361

    
362
/* Comparison expr */
363
| expr EQ expr 
364
    {mkpredef_call "=" [$1;$3]}
365
| expr LT expr 
366
    {mkpredef_call "<" [$1;$3]}
367
| expr LTE expr 
368
    {mkpredef_call "<=" [$1;$3]}
369
| expr GT expr 
370
    {mkpredef_call ">" [$1;$3]}
371
| expr GTE  expr 
372
    {mkpredef_call ">=" [$1;$3]}
373
| expr NEQ expr 
374
    {mkpredef_call "!=" [$1;$3]}
375

    
376
/* Arithmetic expr */
377
| expr PLUS expr 
378
    {mkpredef_call "+" [$1;$3]}
379
| expr MINUS expr 
380
    {mkpredef_call "-" [$1;$3]}
381
| expr MULT expr 
382
    {mkpredef_call "*" [$1;$3]}
383
| expr DIV expr 
384
    {mkpredef_call "/" [$1;$3]}
385
| MINUS expr %prec UMINUS
386
  {mkpredef_unary_call "uminus" $2}
387
| expr MOD expr 
388
    {mkpredef_call "mod" [$1;$3]}
389

    
390
/* If */
391
| IF expr THEN expr ELSE expr
392
    {mkexpr (Expr_ite ($2, $4, $6))}
393

    
394
handler_expr_list:
395
   { [] }
396
| handler_expr handler_expr_list { $1 :: $2 }
397

    
398
handler_expr:
399
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
400

    
401
signed_const_array:
402
| signed_const { [$1] }
403
| signed_const COMMA signed_const_array { $1 :: $3 }
404

    
405
signed_const:
406
  INT {Const_int $1}
407
| REAL {Const_real $1}
408
| FLOAT {Const_float $1}
409
| IDENT {Const_tag $1}
410
| MINUS INT {Const_int (-1 * $2)}
411
| MINUS REAL {Const_real ("-" ^ $2)}
412
| MINUS FLOAT {Const_float (-1. *. $2)}
413
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
414

    
415
dim:
416
   INT { mkdim_int $1 }
417
| LPAR dim RPAR { $2 }
418
| IDENT { mkdim_ident $1 }
419
| dim AND dim 
420
    {mkdim_appl "&&" [$1;$3]}
421
| dim AMPERAMPER dim 
422
    {mkdim_appl "&&" [$1;$3]}
423
| dim OR dim 
424
    {mkdim_appl "||" [$1;$3]}
425
| dim BARBAR dim 
426
    {mkdim_appl "||" [$1;$3]}
427
| dim XOR dim 
428
    {mkdim_appl "xor" [$1;$3]}
429
| NOT dim 
430
    {mkdim_appl "not" [$2]}
431
| dim IMPL dim 
432
    {mkdim_appl "impl" [$1;$3]}
433

    
434
/* Comparison dim */
435
| dim EQ dim 
436
    {mkdim_appl "=" [$1;$3]}
437
| dim LT dim 
438
    {mkdim_appl "<" [$1;$3]}
439
| dim LTE dim 
440
    {mkdim_appl "<=" [$1;$3]}
441
| dim GT dim 
442
    {mkdim_appl ">" [$1;$3]}
443
| dim GTE  dim 
444
    {mkdim_appl ">=" [$1;$3]}
445
| dim NEQ dim 
446
    {mkdim_appl "!=" [$1;$3]}
447

    
448
/* Arithmetic dim */
449
| dim PLUS dim 
450
    {mkdim_appl "+" [$1;$3]}
451
| dim MINUS dim 
452
    {mkdim_appl "-" [$1;$3]}
453
| dim MULT dim 
454
    {mkdim_appl "*" [$1;$3]}
455
| dim DIV dim 
456
    {mkdim_appl "/" [$1;$3]}
457
| MINUS dim %prec UMINUS
458
  {mkdim_appl "uminus" [$2]}
459
| dim MOD dim 
460
    {mkdim_appl "mod" [$1;$3]}
461
/* If */
462
| IF dim THEN dim ELSE dim
463
    {mkdim_ite $2 $4 $6}
464

    
465
locals:
466
  {[]}
467
| VAR vdecl_list SCOL {$2}
468

    
469
vdecl_list:
470
    vdecl {$1}
471
| vdecl_list SCOL vdecl {$3 @ $1}
472

    
473
vdecl:
474
/* Useless no ?*/    ident_list
475
    {List.map mkvar_decl 
476
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
477

    
478
| ident_list COL typeconst clock 
479
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
480
| CONST ident_list COL typeconst /* static parameters don't have clocks */
481
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
482

    
483
cdecl_list:
484
  cdecl SCOL { [$1] }
485
| cdecl_list cdecl SCOL { $2::$1 }
486

    
487
cdecl:
488
    IDENT EQ signed_const {
489
      let c = {
490
	const_id = $1;
491
	const_loc = Location.symbol_rloc ();
492
        const_type = Types.new_var ();
493
	const_value = $3;
494
      } in
495
      Hashtbl.add consts_table $1 c; c
496
    }
497

    
498
clock:
499
    {mkclock Ckdec_any}
500
| when_list
501
    {mkclock (Ckdec_bool (List.rev $1))}
502

    
503
when_cond:
504
    WHEN IDENT {($2, tag_true)}
505
| WHENNOT IDENT {($2, tag_false)}
506
| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
507

    
508
when_list:
509
    when_cond {[$1]}
510
| when_list when_cond {$2::$1}
511

    
512
ident_list:
513
  IDENT {[$1]}
514
| ident_list COMMA IDENT {$3::$1}
515

    
516
SCOL_opt:
517
    SCOL {} | {}