Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 8b3afe43

History | View | Annotate | Download (15.5 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 OPEN 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
%start header
95
%type <Corelang.top_decl list> header
96

    
97
%%
98

    
99
prog:
100
 open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }
101

    
102
header:
103
 open_list typ_def_list top_decl_header_list EOF { $1 @ (List.rev $3) }
104

    
105
open_list:
106
  { [] }
107
| open_lusi open_list { $1 :: $2 }
108

    
109
open_lusi:
110
  OPEN QUOTE IDENT QUOTE { mktop_decl (Open $3) }
111

    
112
top_decl_list:
113
  top_decl {[$1]}
114
| top_decl_list top_decl {$2::$1}
115

    
116

    
117
top_decl_header_list:
118
  top_decl_header {[$1]}
119
| top_decl_header_list top_decl_header {$2::$1}
120

    
121

    
122
top_decl_header:
123
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL
124
    {let nd = mktop_decl (ImportedNode
125
                            {nodei_id = $2;
126
                             nodei_type = Types.new_var ();
127
                             nodei_clock = Clocks.new_var true;
128
                             nodei_inputs = List.rev $4;
129
                             nodei_outputs = List.rev $9;
130
			     nodei_stateless = $12;
131
			     nodei_spec = None})
132
    in
133
    Hashtbl.add node_table $2 nd; nd}
134

    
135
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL
136
    {let nd = mktop_decl (ImportedNode
137
                            {nodei_id = $3;
138
                             nodei_type = Types.new_var ();
139
                             nodei_clock = Clocks.new_var true;
140
                             nodei_inputs = List.rev $5;
141
                             nodei_outputs = List.rev $10;
142
			     nodei_stateless = $13;
143
			     nodei_spec = Some $1})
144
    in
145
    Hashtbl.add node_table $3 nd; nd}
146

    
147
| FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
148
    {let nd = mktop_decl (ImportedNode
149
                            {nodei_id = $2;
150
                             nodei_type = Types.new_var ();
151
			     nodei_clock = Clocks.new_var true;
152
                             nodei_inputs = List.rev $4;
153
                             nodei_outputs = List.rev $9;
154
			     nodei_stateless = true;
155
			     nodei_spec = None})
156
     in
157
     Hashtbl.add node_table $2 nd; nd}
158

    
159
| nodespec_list FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
160
    {let nd = mktop_decl (ImportedNode
161
                            {nodei_id = $3;
162
                             nodei_type = Types.new_var ();
163
			     nodei_clock = Clocks.new_var true;
164
                             nodei_inputs = List.rev $5;
165
                             nodei_outputs = List.rev $10;
166
			     nodei_stateless = true;
167
			     nodei_spec = Some $1})
168
     in
169
    Hashtbl.add node_table $3 nd; nd}
170

    
171
top_decl:
172
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
173

    
174
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
175
    {let eqs, asserts, annots = $15 in
176
     let nd = mktop_decl (Node
177
                            {node_id = $2;
178
                             node_type = Types.new_var ();
179
                             node_clock = Clocks.new_var true;
180
                             node_inputs = List.rev $4;
181
                             node_outputs = List.rev $9;
182
                             node_locals = List.rev $13;
183
			     node_gencalls = [];
184
			     node_checks = [];
185
			     node_asserts = asserts; 
186
                             node_eqs = eqs;
187
			     node_spec = None;
188
			     node_annot = match annots with [] -> None | _ -> Some annots})
189
    in
190
    Hashtbl.add node_table $2 nd; nd}
191

    
192
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
193
    {let eqs, asserts, annots = $16 in
194
     let nd = mktop_decl (Node
195
                            {node_id = $3;
196
                             node_type = Types.new_var ();
197
                             node_clock = Clocks.new_var true;
198
                             node_inputs = List.rev $5;
199
                             node_outputs = List.rev $10;
200
                             node_locals = List.rev $14;
201
			     node_gencalls = [];
202
			     node_checks = [];
203
			     node_asserts = asserts; 
204
                             node_eqs = eqs;
205
			     node_spec = Some $1;
206
			     node_annot = match annots with [] -> None | _ -> Some annots})
207
    in
208
    Hashtbl.add node_table $3 nd; nd}
209

    
210
nodespec_list:
211
NODESPEC { $1 }
212
| NODESPEC nodespec_list { LustreSpec.merge_node_annot $1 $2 }
213

    
214
stateless_opt:
215
   { false }
216
| STATELESS {true}
217

    
218
typ_def_list:
219
    /* empty */ {}
220
| typ_def SCOL typ_def_list {$1;$3}
221

    
222
typ_def:
223
  TYPE IDENT EQ typeconst {
224
    try
225
      Hashtbl.add type_table (Tydec_const $2) (Corelang.get_repr_type $4)
226
    with Not_found-> raise (Corelang.Unbound_type ($4, Location.symbol_rloc())) }
227
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
228
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) Tydec_any }
229

    
230
array_typ_decl:
231
                            { fun typ -> typ }
232
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
233

    
234
typeconst:
235
  TINT array_typ_decl  { $2 Tydec_int }
236
| TBOOL array_typ_decl { $2 Tydec_bool  }
237
| TREAL array_typ_decl { $2 Tydec_real  }
238
| TFLOAT array_typ_decl { $2 Tydec_float }
239
| IDENT array_typ_decl { $2 (Tydec_const $1) }
240
| TBOOL TCLOCK  { Tydec_clock Tydec_bool }
241
| IDENT TCLOCK  { Tydec_clock (Tydec_const $1) }
242

    
243
tag_list:
244
  IDENT
245
  { (fun t -> if Hashtbl.mem tag_table $1
246
             then raise (Corelang.Already_bound_label ($1, t, Location.symbol_rloc ()))
247
             else (Hashtbl.add tag_table $1 t; $1 :: [])) }
248
| tag_list COMMA IDENT
249
  { (fun t -> if Hashtbl.mem tag_table $3
250
             then raise (Corelang.Already_bound_label ($3, t, Location.symbol_rloc ()))
251
             else (Hashtbl.add tag_table $3 t; $3 :: ($1 t))) }
252

    
253
field_list:
254
   { [] }
255
| IDENT COL typeconst SCOL field_list { ($1, $3) :: $5 }
256

    
257
eq_list:
258
  { [], [], [] }
259
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
260
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
261
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}
262
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
263

    
264
automaton:
265
 AUTOMATON IDENT handler_list { failwith "not implemented" }
266

    
267
handler_list:
268
     { [] }
269
| handler handler_list { $1::$2 }
270

    
271
handler:
272
 STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
273

    
274
unless_list:
275
    { [] }
276
| unless unless_list { $1::$2 }
277

    
278
until_list:
279
    { [] }
280
| until until_list { $1::$2 }
281

    
282
unless:
283
  UNLESS expr RESTART IDENT { }
284
| UNLESS expr RESUME IDENT  { }
285

    
286
until:
287
  UNTIL expr RESTART IDENT { }
288
| UNTIL expr RESUME IDENT  { }
289

    
290
assert_:
291
| ASSERT expr SCOL {mkassert ($2)}
292

    
293
eq:
294
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
295
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
296

    
297
tuple_expr:
298
    expr COMMA expr {[$3;$1]}
299
| tuple_expr COMMA expr {$3::$1}
300

    
301
// Same as tuple expr but accepting lists with single element
302
array_expr:
303
  expr {[$1]}
304
| expr COMMA array_expr {$1::$3}
305

    
306
dim_list:
307
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
308
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
309

    
310
expr:
311
/* constants */
312
  INT {mkexpr (Expr_const (Const_int $1))}
313
| REAL {mkexpr (Expr_const (Const_real $1))}
314
| FLOAT {mkexpr (Expr_const (Const_float $1))}
315
/* Idents or type enum tags */
316
| IDENT {
317
  if Hashtbl.mem tag_table $1
318
  then mkexpr (Expr_const (Const_tag $1))
319
  else mkexpr (Expr_ident $1)}
320
| LPAR ANNOT expr RPAR
321
    {update_expr_annot $3 $2}
322
| LPAR expr RPAR
323
    {$2}
324
| LPAR tuple_expr RPAR
325
    {mkexpr (Expr_tuple (List.rev $2))}
326

    
327
/* Array expressions */
328
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
329
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
330
| expr LBRACKET dim_list { $3 $1 }
331

    
332
/* Temporal operators */
333
| PRE expr 
334
    {mkexpr (Expr_pre $2)}
335
| expr ARROW expr 
336
    {mkexpr (Expr_arrow ($1,$3))}
337
| expr FBY expr 
338
    {(*mkexpr (Expr_fby ($1,$3))*)
339
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
340
| expr WHEN IDENT 
341
    {mkexpr (Expr_when ($1,$3,tag_true))}
342
| expr WHENNOT IDENT
343
    {mkexpr (Expr_when ($1,$3,tag_false))}
344
| expr WHEN IDENT LPAR IDENT RPAR
345
    {mkexpr (Expr_when ($1, $5, $3))}
346
| MERGE IDENT handler_expr_list
347
    {mkexpr (Expr_merge ($2,$3))}
348

    
349
/* Applications */
350
| IDENT LPAR expr RPAR
351
    {mkexpr (Expr_appl ($1, $3, None))}
352
| IDENT LPAR expr RPAR EVERY IDENT
353
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
354
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
355
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
356
| IDENT LPAR tuple_expr RPAR
357
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
358
| IDENT LPAR tuple_expr RPAR EVERY IDENT
359
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
360
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
361
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
362

    
363
/* Boolean expr */
364
| expr AND expr 
365
    {mkpredef_call "&&" [$1;$3]}
366
| expr AMPERAMPER expr 
367
    {mkpredef_call "&&" [$1;$3]}
368
| expr OR expr 
369
    {mkpredef_call "||" [$1;$3]}
370
| expr BARBAR expr 
371
    {mkpredef_call "||" [$1;$3]}
372
| expr XOR expr 
373
    {mkpredef_call "xor" [$1;$3]}
374
| NOT expr 
375
    {mkpredef_unary_call "not" $2}
376
| expr IMPL expr 
377
    {mkpredef_call "impl" [$1;$3]}
378

    
379
/* Comparison expr */
380
| expr EQ expr 
381
    {mkpredef_call "=" [$1;$3]}
382
| expr LT expr 
383
    {mkpredef_call "<" [$1;$3]}
384
| expr LTE expr 
385
    {mkpredef_call "<=" [$1;$3]}
386
| expr GT expr 
387
    {mkpredef_call ">" [$1;$3]}
388
| expr GTE  expr 
389
    {mkpredef_call ">=" [$1;$3]}
390
| expr NEQ expr 
391
    {mkpredef_call "!=" [$1;$3]}
392

    
393
/* Arithmetic expr */
394
| expr PLUS expr 
395
    {mkpredef_call "+" [$1;$3]}
396
| expr MINUS expr 
397
    {mkpredef_call "-" [$1;$3]}
398
| expr MULT expr 
399
    {mkpredef_call "*" [$1;$3]}
400
| expr DIV expr 
401
    {mkpredef_call "/" [$1;$3]}
402
| MINUS expr %prec UMINUS
403
  {mkpredef_unary_call "uminus" $2}
404
| expr MOD expr 
405
    {mkpredef_call "mod" [$1;$3]}
406

    
407
/* If */
408
| IF expr THEN expr ELSE expr
409
    {mkexpr (Expr_ite ($2, $4, $6))}
410

    
411
handler_expr_list:
412
   { [] }
413
| handler_expr handler_expr_list { $1 :: $2 }
414

    
415
handler_expr:
416
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
417

    
418
signed_const_array:
419
| signed_const { [$1] }
420
| signed_const COMMA signed_const_array { $1 :: $3 }
421

    
422
signed_const:
423
  INT {Const_int $1}
424
| REAL {Const_real $1}
425
| FLOAT {Const_float $1}
426
| IDENT {Const_tag $1}
427
| MINUS INT {Const_int (-1 * $2)}
428
| MINUS REAL {Const_real ("-" ^ $2)}
429
| MINUS FLOAT {Const_float (-1. *. $2)}
430
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
431

    
432
dim:
433
   INT { mkdim_int $1 }
434
| LPAR dim RPAR { $2 }
435
| IDENT { mkdim_ident $1 }
436
| dim AND dim 
437
    {mkdim_appl "&&" [$1;$3]}
438
| dim AMPERAMPER dim 
439
    {mkdim_appl "&&" [$1;$3]}
440
| dim OR dim 
441
    {mkdim_appl "||" [$1;$3]}
442
| dim BARBAR dim 
443
    {mkdim_appl "||" [$1;$3]}
444
| dim XOR dim 
445
    {mkdim_appl "xor" [$1;$3]}
446
| NOT dim 
447
    {mkdim_appl "not" [$2]}
448
| dim IMPL dim 
449
    {mkdim_appl "impl" [$1;$3]}
450

    
451
/* Comparison dim */
452
| dim EQ dim 
453
    {mkdim_appl "=" [$1;$3]}
454
| dim LT dim 
455
    {mkdim_appl "<" [$1;$3]}
456
| dim LTE dim 
457
    {mkdim_appl "<=" [$1;$3]}
458
| dim GT dim 
459
    {mkdim_appl ">" [$1;$3]}
460
| dim GTE  dim 
461
    {mkdim_appl ">=" [$1;$3]}
462
| dim NEQ dim 
463
    {mkdim_appl "!=" [$1;$3]}
464

    
465
/* Arithmetic dim */
466
| dim PLUS dim 
467
    {mkdim_appl "+" [$1;$3]}
468
| dim MINUS dim 
469
    {mkdim_appl "-" [$1;$3]}
470
| dim MULT dim 
471
    {mkdim_appl "*" [$1;$3]}
472
| dim DIV dim 
473
    {mkdim_appl "/" [$1;$3]}
474
| MINUS dim %prec UMINUS
475
  {mkdim_appl "uminus" [$2]}
476
| dim MOD dim 
477
    {mkdim_appl "mod" [$1;$3]}
478
/* If */
479
| IF dim THEN dim ELSE dim
480
    {mkdim_ite $2 $4 $6}
481

    
482
locals:
483
  {[]}
484
| VAR vdecl_list SCOL {$2}
485

    
486
vdecl_list:
487
    vdecl {$1}
488
| vdecl_list SCOL vdecl {$3 @ $1}
489

    
490
vdecl:
491
/* Useless no ?*/    ident_list
492
    {List.map mkvar_decl 
493
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
494

    
495
| ident_list COL typeconst clock 
496
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
497
| CONST ident_list COL typeconst /* static parameters don't have clocks */
498
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
499

    
500
cdecl_list:
501
  cdecl SCOL { [$1] }
502
| cdecl_list cdecl SCOL { $2::$1 }
503

    
504
cdecl:
505
    IDENT EQ signed_const {
506
      let c = {
507
	const_id = $1;
508
	const_loc = Location.symbol_rloc ();
509
        const_type = Types.new_var ();
510
	const_value = $3;
511
      } in
512
      Hashtbl.add consts_table $1 c; c
513
    }
514

    
515
clock:
516
    {mkclock Ckdec_any}
517
| when_list
518
    {mkclock (Ckdec_bool (List.rev $1))}
519

    
520
when_cond:
521
    WHEN IDENT {($2, tag_true)}
522
| WHENNOT IDENT {($2, tag_false)}
523
| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
524

    
525
when_list:
526
    when_cond {[$1]}
527
| when_list when_cond {$2::$1}
528

    
529
ident_list:
530
  IDENT {[$1]}
531
| ident_list COMMA IDENT {$3::$1}
532

    
533
SCOL_opt:
534
    SCOL {} | {}