Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ 6affc9f5

History | View | Annotate | Download (16 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
let add_symbol msg hashtbl name value =
46
 if Hashtbl.mem hashtbl name
47
 then raise (Corelang.Error (Corelang.Already_bound_symbol msg, Location.symbol_rloc ()))
48
 else Hashtbl.add hashtbl name value
49

    
50
let check_symbol msg hashtbl name =
51
 if not (Hashtbl.mem hashtbl name)
52
 then raise (Corelang.Error (Corelang.Unbound_symbol msg, Location.symbol_rloc ()))
53
 else ()
54

    
55
%}
56

    
57
%token <int> INT
58
%token <string> REAL
59
%token <float> FLOAT
60
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
61
%token STATELESS ASSERT OPEN QUOTE FUNCTION
62
%token <string> IDENT
63
%token <LustreSpec.expr_annot> ANNOT
64
%token <LustreSpec.node_annot> NODESPEC
65
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
66
%token AMPERAMPER BARBAR NOT POWER
67
%token IF THEN ELSE
68
%token UCLOCK DCLOCK PHCLOCK TAIL
69
%token MERGE FBY WHEN WHENNOT EVERY
70
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
71
%token STRUCT ENUM
72
%token TINT TFLOAT TREAL TBOOL TCLOCK
73
%token RATE DUE
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

    
80
%token EOF
81

    
82
%nonassoc COMMA
83
%left MERGE IF
84
%nonassoc ELSE
85
%right ARROW FBY
86
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
87
%right COLCOL
88
%right IMPL
89
%left OR XOR BARBAR
90
%left AND AMPERAMPER
91
%left NOT
92
%nonassoc INT
93
%nonassoc EQ LT GT LTE GTE NEQ
94
%left MINUS PLUS
95
%left MULT DIV MOD
96
%left UMINUS
97
%left POWER
98
%left PRE LAST
99
%nonassoc RBRACKET
100
%nonassoc LBRACKET
101

    
102
%start prog
103
%type <Corelang.top_decl list> prog
104
%start header
105
%type <Corelang.top_decl list> header
106

    
107
%%
108

    
109
prog:
110
 open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }
111

    
112
header:
113
 open_list typ_def_list top_decl_header_list EOF { $1 @ (List.rev $3) }
114

    
115
open_list:
116
  { [] }
117
| open_lusi open_list { $1 :: $2 }
118

    
119
open_lusi:
120
  OPEN QUOTE IDENT QUOTE { mktop_decl (Open $3) }
121

    
122
top_decl_list:
123
  top_decl {[$1]}
124
| top_decl_list top_decl {$2::$1}
125

    
126

    
127
top_decl_header_list:
128
  top_decl_header {[$1]}
129
| top_decl_header_list top_decl_header {$2::$1}
130

    
131

    
132
top_decl_header:
133
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL
134
    {let nd = mktop_decl (ImportedNode
135
                            {nodei_id = $2;
136
                             nodei_type = Types.new_var ();
137
                             nodei_clock = Clocks.new_var true;
138
                             nodei_inputs = List.rev $4;
139
                             nodei_outputs = List.rev $9;
140
			     nodei_stateless = $12;
141
			     nodei_spec = None})
142
    in
143
    add_symbol ("node " ^ $2) node_table $2 nd; nd}
144

    
145
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL
146
    {let nd = mktop_decl (ImportedNode
147
                            {nodei_id = $3;
148
                             nodei_type = Types.new_var ();
149
                             nodei_clock = Clocks.new_var true;
150
                             nodei_inputs = List.rev $5;
151
                             nodei_outputs = List.rev $10;
152
			     nodei_stateless = $13;
153
			     nodei_spec = Some $1})
154
    in
155
    add_symbol ("node " ^ $3) node_table $3 nd; nd}
156

    
157
| FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
158
    {let nd = mktop_decl (ImportedNode
159
                            {nodei_id = $2;
160
                             nodei_type = Types.new_var ();
161
			     nodei_clock = Clocks.new_var true;
162
                             nodei_inputs = List.rev $4;
163
                             nodei_outputs = List.rev $9;
164
			     nodei_stateless = true;
165
			     nodei_spec = None})
166
     in
167
     add_symbol ("function " ^ $2) node_table $2 nd; nd}
168

    
169
| nodespec_list FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
170
    {let nd = mktop_decl (ImportedNode
171
                            {nodei_id = $3;
172
                             nodei_type = Types.new_var ();
173
			     nodei_clock = Clocks.new_var true;
174
                             nodei_inputs = List.rev $5;
175
                             nodei_outputs = List.rev $10;
176
			     nodei_stateless = true;
177
			     nodei_spec = Some $1})
178
     in
179
    add_symbol ("function " ^ $3) node_table $3 nd; nd}
180

    
181
top_decl:
182
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
183

    
184
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
185
    {let eqs, asserts, annots = $15 in
186
     let nd = mktop_decl (Node
187
                            {node_id = $2;
188
                             node_type = Types.new_var ();
189
                             node_clock = Clocks.new_var true;
190
                             node_inputs = List.rev $4;
191
                             node_outputs = List.rev $9;
192
                             node_locals = List.rev $13;
193
			     node_gencalls = [];
194
			     node_checks = [];
195
			     node_asserts = asserts; 
196
                             node_eqs = eqs;
197
			     node_spec = None;
198
			     node_annot = match annots with [] -> None | _ -> Some annots})
199
    in
200
    add_symbol ("node " ^ $2) node_table $2 nd; nd}
201

    
202
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
203
    {let eqs, asserts, annots = $16 in
204
     let nd = mktop_decl (Node
205
                            {node_id = $3;
206
                             node_type = Types.new_var ();
207
                             node_clock = Clocks.new_var true;
208
                             node_inputs = List.rev $5;
209
                             node_outputs = List.rev $10;
210
                             node_locals = List.rev $14;
211
			     node_gencalls = [];
212
			     node_checks = [];
213
			     node_asserts = asserts; 
214
                             node_eqs = eqs;
215
			     node_spec = Some $1;
216
			     node_annot = match annots with [] -> None | _ -> Some annots})
217
    in
218
    add_symbol ("node " ^ $3) node_table $3 nd; nd}
219

    
220
nodespec_list:
221
NODESPEC { $1 }
222
| NODESPEC nodespec_list { LustreSpec.merge_node_annot $1 $2 }
223

    
224
stateless_opt:
225
   { false }
226
| STATELESS {true}
227

    
228
typ_def_list:
229
    /* empty */ {}
230
| typ_def SCOL typ_def_list {$1;$3}
231

    
232
typ_def:
233
  TYPE IDENT EQ typeconst {
234
    try
235
      add_symbol ("type " ^ $2) type_table (Tydec_const $2) (Corelang.get_repr_type $4)
236
    with Not_found-> assert false }
237
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
238
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) }
239

    
240
array_typ_decl:
241
                            { fun typ -> typ }
242
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
243

    
244
typeconst:
245
  TINT array_typ_decl  { $2 Tydec_int }
246
| TBOOL array_typ_decl { $2 Tydec_bool  }
247
| TREAL array_typ_decl { $2 Tydec_real  }
248
| TFLOAT array_typ_decl { $2 Tydec_float }
249
| IDENT array_typ_decl { check_symbol ("type " ^ $1) type_table (Tydec_const $1); $2 (Tydec_const $1) }
250
| TBOOL TCLOCK  { Tydec_clock Tydec_bool }
251
| IDENT TCLOCK  { Tydec_clock (Tydec_const $1) }
252

    
253
tag_list:
254
  IDENT
255
  { (fun t -> add_symbol ("tag " ^ $1) tag_table $1 t; $1 :: []) }
256
| tag_list COMMA IDENT
257
  { (fun t -> add_symbol ("tag " ^ $3)tag_table $3 t; $3 :: ($1 t)) }
258

    
259
field_list:
260
  { (fun t -> []) }
261
| field_list IDENT COL typeconst SCOL
262
  { (fun t -> add_symbol ("field " ^ $2) field_table $2 t; ($1 t) @ [ ($2, $4) ]) }
263

    
264
eq_list:
265
  { [], [], [] }
266
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
267
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
268
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}
269
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
270

    
271
automaton:
272
 AUTOMATON IDENT handler_list { failwith "not implemented" }
273

    
274
handler_list:
275
     { [] }
276
| handler handler_list { $1::$2 }
277

    
278
handler:
279
 STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
280

    
281
unless_list:
282
    { [] }
283
| unless unless_list { $1::$2 }
284

    
285
until_list:
286
    { [] }
287
| until until_list { $1::$2 }
288

    
289
unless:
290
  UNLESS expr RESTART IDENT { }
291
| UNLESS expr RESUME IDENT  { }
292

    
293
until:
294
  UNTIL expr RESTART IDENT { }
295
| UNTIL expr RESUME IDENT  { }
296

    
297
assert_:
298
| ASSERT expr SCOL {mkassert ($2)}
299

    
300
eq:
301
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
302
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
303

    
304
tuple_expr:
305
    expr COMMA expr {[$3;$1]}
306
| tuple_expr COMMA expr {$3::$1}
307

    
308
// Same as tuple expr but accepting lists with single element
309
array_expr:
310
  expr {[$1]}
311
| expr COMMA array_expr {$1::$3}
312

    
313
dim_list:
314
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
315
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
316

    
317
expr:
318
/* constants */
319
  INT {mkexpr (Expr_const (Const_int $1))}
320
| REAL {mkexpr (Expr_const (Const_real $1))}
321
| FLOAT {mkexpr (Expr_const (Const_float $1))}
322
/* Idents or type enum tags */
323
| IDENT {
324
  if Hashtbl.mem tag_table $1
325
  then mkexpr (Expr_const (Const_tag $1))
326
  else mkexpr (Expr_ident $1)}
327
| LPAR ANNOT expr RPAR
328
    {update_expr_annot $3 $2}
329
| LPAR expr RPAR
330
    {$2}
331
| LPAR tuple_expr RPAR
332
    {mkexpr (Expr_tuple (List.rev $2))}
333

    
334
/* Array expressions */
335
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
336
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
337
| expr LBRACKET dim_list { $3 $1 }
338

    
339
/* Temporal operators */
340
| PRE expr 
341
    {mkexpr (Expr_pre $2)}
342
| expr ARROW expr 
343
    {mkexpr (Expr_arrow ($1,$3))}
344
| expr FBY expr 
345
    {(*mkexpr (Expr_fby ($1,$3))*)
346
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
347
| expr WHEN IDENT 
348
    {mkexpr (Expr_when ($1,$3,tag_true))}
349
| expr WHENNOT IDENT
350
    {mkexpr (Expr_when ($1,$3,tag_false))}
351
| expr WHEN IDENT LPAR IDENT RPAR
352
    {mkexpr (Expr_when ($1, $5, $3))}
353
| MERGE IDENT handler_expr_list
354
    {mkexpr (Expr_merge ($2,$3))}
355

    
356
/* Applications */
357
| IDENT LPAR expr RPAR
358
    {mkexpr (Expr_appl ($1, $3, None))}
359
| IDENT LPAR expr RPAR EVERY IDENT
360
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
361
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
362
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
363
| IDENT LPAR tuple_expr RPAR
364
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
365
| IDENT LPAR tuple_expr RPAR EVERY IDENT
366
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
367
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
368
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
369

    
370
/* Boolean expr */
371
| expr AND expr 
372
    {mkpredef_call "&&" [$1;$3]}
373
| expr AMPERAMPER expr 
374
    {mkpredef_call "&&" [$1;$3]}
375
| expr OR expr 
376
    {mkpredef_call "||" [$1;$3]}
377
| expr BARBAR expr 
378
    {mkpredef_call "||" [$1;$3]}
379
| expr XOR expr 
380
    {mkpredef_call "xor" [$1;$3]}
381
| NOT expr 
382
    {mkpredef_unary_call "not" $2}
383
| expr IMPL expr 
384
    {mkpredef_call "impl" [$1;$3]}
385

    
386
/* Comparison expr */
387
| expr EQ expr 
388
    {mkpredef_call "=" [$1;$3]}
389
| expr LT expr 
390
    {mkpredef_call "<" [$1;$3]}
391
| expr LTE expr 
392
    {mkpredef_call "<=" [$1;$3]}
393
| expr GT expr 
394
    {mkpredef_call ">" [$1;$3]}
395
| expr GTE  expr 
396
    {mkpredef_call ">=" [$1;$3]}
397
| expr NEQ expr 
398
    {mkpredef_call "!=" [$1;$3]}
399

    
400
/* Arithmetic expr */
401
| expr PLUS expr 
402
    {mkpredef_call "+" [$1;$3]}
403
| expr MINUS expr 
404
    {mkpredef_call "-" [$1;$3]}
405
| expr MULT expr 
406
    {mkpredef_call "*" [$1;$3]}
407
| expr DIV expr 
408
    {mkpredef_call "/" [$1;$3]}
409
| MINUS expr %prec UMINUS
410
  {mkpredef_unary_call "uminus" $2}
411
| expr MOD expr 
412
    {mkpredef_call "mod" [$1;$3]}
413

    
414
/* If */
415
| IF expr THEN expr ELSE expr
416
    {mkexpr (Expr_ite ($2, $4, $6))}
417

    
418
handler_expr_list:
419
   { [] }
420
| handler_expr handler_expr_list { $1 :: $2 }
421

    
422
handler_expr:
423
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
424

    
425
signed_const_array:
426
| signed_const { [$1] }
427
| signed_const COMMA signed_const_array { $1 :: $3 }
428

    
429
signed_const_struct:
430
| IDENT EQ signed_const { [ ($1, $3) ] }
431
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
432

    
433
signed_const:
434
  INT {Const_int $1}
435
| REAL {Const_real $1}
436
| FLOAT {Const_float $1}
437
| IDENT {Const_tag $1}
438
| MINUS INT {Const_int (-1 * $2)}
439
| MINUS REAL {Const_real ("-" ^ $2)}
440
| MINUS FLOAT {Const_float (-1. *. $2)}
441
| LCUR signed_const_struct RCUR { Const_struct $2 }
442
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
443

    
444
dim:
445
   INT { mkdim_int $1 }
446
| LPAR dim RPAR { $2 }
447
| IDENT { mkdim_ident $1 }
448
| dim AND dim 
449
    {mkdim_appl "&&" [$1;$3]}
450
| dim AMPERAMPER dim 
451
    {mkdim_appl "&&" [$1;$3]}
452
| dim OR dim 
453
    {mkdim_appl "||" [$1;$3]}
454
| dim BARBAR dim 
455
    {mkdim_appl "||" [$1;$3]}
456
| dim XOR dim 
457
    {mkdim_appl "xor" [$1;$3]}
458
| NOT dim 
459
    {mkdim_appl "not" [$2]}
460
| dim IMPL dim 
461
    {mkdim_appl "impl" [$1;$3]}
462

    
463
/* Comparison dim */
464
| dim EQ dim 
465
    {mkdim_appl "=" [$1;$3]}
466
| dim LT dim 
467
    {mkdim_appl "<" [$1;$3]}
468
| dim LTE dim 
469
    {mkdim_appl "<=" [$1;$3]}
470
| dim GT dim 
471
    {mkdim_appl ">" [$1;$3]}
472
| dim GTE  dim 
473
    {mkdim_appl ">=" [$1;$3]}
474
| dim NEQ dim 
475
    {mkdim_appl "!=" [$1;$3]}
476

    
477
/* Arithmetic dim */
478
| dim PLUS dim 
479
    {mkdim_appl "+" [$1;$3]}
480
| dim MINUS dim 
481
    {mkdim_appl "-" [$1;$3]}
482
| dim MULT dim 
483
    {mkdim_appl "*" [$1;$3]}
484
| dim DIV dim 
485
    {mkdim_appl "/" [$1;$3]}
486
| MINUS dim %prec UMINUS
487
  {mkdim_appl "uminus" [$2]}
488
| dim MOD dim 
489
    {mkdim_appl "mod" [$1;$3]}
490
/* If */
491
| IF dim THEN dim ELSE dim
492
    {mkdim_ite $2 $4 $6}
493

    
494
locals:
495
  {[]}
496
| VAR vdecl_list SCOL {$2}
497

    
498
vdecl_list:
499
    vdecl {$1}
500
| vdecl_list SCOL vdecl {$3 @ $1}
501

    
502
vdecl:
503
/* Useless no ?*/    ident_list
504
    {List.map mkvar_decl 
505
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
506

    
507
| ident_list COL typeconst clock 
508
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
509
| CONST ident_list COL typeconst /* static parameters don't have clocks */
510
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
511

    
512
cdecl_list:
513
  cdecl SCOL { [$1] }
514
| cdecl_list cdecl SCOL { $2::$1 }
515

    
516
cdecl:
517
    IDENT EQ signed_const {
518
      let c = {
519
	const_id = $1;
520
	const_loc = Location.symbol_rloc ();
521
        const_type = Types.new_var ();
522
	const_value = $3;
523
      } in
524
      Hashtbl.add consts_table $1 c; c
525
    }
526

    
527
clock:
528
    {mkclock Ckdec_any}
529
| when_list
530
    {mkclock (Ckdec_bool (List.rev $1))}
531

    
532
when_cond:
533
    WHEN IDENT {($2, tag_true)}
534
| WHENNOT IDENT {($2, tag_false)}
535
| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
536

    
537
when_list:
538
    when_cond {[$1]}
539
| when_list when_cond {$2::$1}
540

    
541
ident_list:
542
  IDENT {[$1]}
543
| ident_list COMMA IDENT {$3::$1}
544

    
545
SCOL_opt:
546
    SCOL {} | {}