Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ e135421f

History | View | Annotate | Download (14.3 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_node own msg hashtbl name value =
46
  try
47
    match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with
48
    | Node _        , ImportedNode _ when own
49
                        -> ()
50
    | ImportedNode _, _ ->
51
       Hashtbl.add hashtbl name value
52
    | Node _        , _ -> 
53
       raise (Corelang.Error (Location.symbol_rloc (), Corelang.Already_bound_symbol msg))
54
    | _                 -> assert false
55
  with
56
    Not_found ->
57
       Hashtbl.add hashtbl name value
58

    
59
let add_symbol msg hashtbl name value =
60
 if Hashtbl.mem hashtbl name
61
 then raise (Corelang.Error (Location.symbol_rloc (), Corelang.Already_bound_symbol msg))
62
 else Hashtbl.add hashtbl name value
63

    
64
let check_symbol msg hashtbl name =
65
 if not (Hashtbl.mem hashtbl name)
66
 then raise (Corelang.Error (Location.symbol_rloc (), Corelang.Unbound_symbol msg))
67
 else ()
68

    
69
%}
70

    
71
%token <int> INT
72
%token <string> REAL
73
%token <float> FLOAT
74
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
75
%token STATELESS ASSERT OPEN QUOTE FUNCTION
76
%token <string> IDENT
77
%token <LustreSpec.expr_annot> ANNOT
78
%token <LustreSpec.node_annot> NODESPEC
79
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
80
%token AMPERAMPER BARBAR NOT POWER
81
%token IF THEN ELSE
82
%token UCLOCK DCLOCK PHCLOCK TAIL
83
%token MERGE FBY WHEN WHENNOT EVERY
84
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
85
%token STRUCT ENUM
86
%token TINT TFLOAT TREAL TBOOL TCLOCK
87
%token RATE DUE
88
%token EQ LT GT LTE GTE NEQ
89
%token AND OR XOR IMPL
90
%token MULT DIV MOD
91
%token MINUS PLUS UMINUS
92
%token PRE ARROW
93

    
94
%token EOF
95

    
96
%nonassoc COMMA
97
%left MERGE IF
98
%nonassoc ELSE
99
%right ARROW FBY
100
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
101
%right COLCOL
102
%right IMPL
103
%left OR XOR BARBAR
104
%left AND AMPERAMPER
105
%left NOT
106
%nonassoc INT
107
%nonassoc EQ LT GT LTE GTE NEQ
108
%left MINUS PLUS
109
%left MULT DIV MOD
110
%left UMINUS
111
%left POWER
112
%left PRE LAST
113
%nonassoc RBRACKET
114
%nonassoc LBRACKET
115

    
116
%start prog
117
%type <Corelang.top_decl list> prog
118
%start header
119
%type <bool -> Corelang.top_decl list> header
120

    
121
%%
122

    
123
prog:
124
 open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }
125

    
126
header:
127
 open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ (List.rev ($3 own)))) }
128

    
129
open_list:
130
  { [] }
131
| open_lusi open_list { $1 :: $2 }
132

    
133
open_lusi:
134
  OPEN QUOTE IDENT QUOTE { mktop_decl (Open $3) }
135

    
136
top_decl_list:
137
  top_decl {[$1]}
138
| top_decl_list top_decl {$2::$1}
139

    
140

    
141
top_decl_header_list:
142
  top_decl_header {(fun own -> [$1 own]) }
143
| top_decl_header_list top_decl_header {(fun own -> ($2 own)::($1 own)) }
144

    
145
state_annot:
146
  FUNCTION { true }
147
| NODE { false }
148

    
149
top_decl_header:
150
  nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
151
    {let nd = mktop_decl (ImportedNode
152
                            {nodei_id = $3;
153
                             nodei_type = Types.new_var ();
154
                             nodei_clock = Clocks.new_var true;
155
                             nodei_inputs = List.rev $5;
156
                             nodei_outputs = List.rev $10;
157
			     nodei_stateless = $2;
158
			     nodei_spec = $1})
159
    in
160
    (fun own -> add_node own ("node " ^ $3) node_table $3 nd; nd) }
161

    
162
top_decl:
163
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
164
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
165
    {let eqs, asserts, annots = $16 in
166
     let nd = mktop_decl (Node
167
                            {node_id = $3;
168
                             node_type = Types.new_var ();
169
                             node_clock = Clocks.new_var true;
170
                             node_inputs = List.rev $5;
171
                             node_outputs = List.rev $10;
172
                             node_locals = List.rev $14;
173
			     node_gencalls = [];
174
			     node_checks = [];
175
			     node_asserts = asserts; 
176
                             node_eqs = eqs;
177
			     node_dec_stateless = $2;
178
			     node_stateless = None;
179
			     node_spec = $1;
180
			     node_annot = match annots with [] -> None | _ -> Some annots})
181
    in
182
    add_node true ("node " ^ $3) node_table $3 nd; nd}
183

    
184
nodespec_list:
185
 { None }
186
| NODESPEC nodespec_list { (function None -> (fun s1 -> Some s1) | Some s2 -> (fun s1 -> Some (LustreSpec.merge_node_annot s1 s2))) $2 $1 }
187

    
188
typ_def_list:
189
    /* empty */ {}
190
| typ_def SCOL typ_def_list {$1;$3}
191

    
192
typ_def:
193
  TYPE IDENT EQ typeconst {
194
    try
195
      add_symbol ("type " ^ $2) type_table (Tydec_const $2) (Corelang.get_repr_type $4)
196
    with Not_found-> assert false }
197
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
198
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) }
199

    
200
array_typ_decl:
201
                            { fun typ -> typ }
202
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
203

    
204
typeconst:
205
  TINT array_typ_decl  { $2 Tydec_int }
206
| TBOOL array_typ_decl { $2 Tydec_bool  }
207
| TREAL array_typ_decl { $2 Tydec_real  }
208
| TFLOAT array_typ_decl { $2 Tydec_float }
209
| IDENT array_typ_decl { check_symbol ("type " ^ $1) type_table (Tydec_const $1); $2 (Tydec_const $1) }
210
| TBOOL TCLOCK  { Tydec_clock Tydec_bool }
211
| IDENT TCLOCK  { Tydec_clock (Tydec_const $1) }
212

    
213
tag_list:
214
  IDENT
215
  { (fun t -> add_symbol ("tag " ^ $1) tag_table $1 t; $1 :: []) }
216
| tag_list COMMA IDENT
217
  { (fun t -> add_symbol ("tag " ^ $3)tag_table $3 t; $3 :: ($1 t)) }
218

    
219
field_list:
220
  { (fun t -> []) }
221
| field_list IDENT COL typeconst SCOL
222
  { (fun t -> add_symbol ("field " ^ $2) field_table $2 t; ($1 t) @ [ ($2, $4) ]) }
223

    
224
eq_list:
225
  { [], [], [] }
226
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
227
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
228
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}
229
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
230

    
231
automaton:
232
 AUTOMATON IDENT handler_list { failwith "not implemented" }
233

    
234
handler_list:
235
     { [] }
236
| handler handler_list { $1::$2 }
237

    
238
handler:
239
 STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
240

    
241
unless_list:
242
    { [] }
243
| unless unless_list { $1::$2 }
244

    
245
until_list:
246
    { [] }
247
| until until_list { $1::$2 }
248

    
249
unless:
250
  UNLESS expr RESTART IDENT { }
251
| UNLESS expr RESUME IDENT  { }
252

    
253
until:
254
  UNTIL expr RESTART IDENT { }
255
| UNTIL expr RESUME IDENT  { }
256

    
257
assert_:
258
| ASSERT expr SCOL {mkassert ($2)}
259

    
260
eq:
261
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
262
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
263

    
264
tuple_expr:
265
    expr COMMA expr {[$3;$1]}
266
| tuple_expr COMMA expr {$3::$1}
267

    
268
// Same as tuple expr but accepting lists with single element
269
array_expr:
270
  expr {[$1]}
271
| expr COMMA array_expr {$1::$3}
272

    
273
dim_list:
274
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
275
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
276

    
277
expr:
278
/* constants */
279
  INT {mkexpr (Expr_const (Const_int $1))}
280
| REAL {mkexpr (Expr_const (Const_real $1))}
281
| FLOAT {mkexpr (Expr_const (Const_float $1))}
282
/* Idents or type enum tags */
283
| IDENT {
284
  if Hashtbl.mem tag_table $1
285
  then mkexpr (Expr_const (Const_tag $1))
286
  else mkexpr (Expr_ident $1)}
287
| LPAR ANNOT expr RPAR
288
    {update_expr_annot $3 $2}
289
| LPAR expr RPAR
290
    {$2}
291
| LPAR tuple_expr RPAR
292
    {mkexpr (Expr_tuple (List.rev $2))}
293

    
294
/* Array expressions */
295
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
296
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
297
| expr LBRACKET dim_list { $3 $1 }
298

    
299
/* Temporal operators */
300
| PRE expr 
301
    {mkexpr (Expr_pre $2)}
302
| expr ARROW expr 
303
    {mkexpr (Expr_arrow ($1,$3))}
304
| expr FBY expr 
305
    {(*mkexpr (Expr_fby ($1,$3))*)
306
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
307
| expr WHEN IDENT 
308
    {mkexpr (Expr_when ($1,$3,tag_true))}
309
| expr WHENNOT IDENT
310
    {mkexpr (Expr_when ($1,$3,tag_false))}
311
| expr WHEN IDENT LPAR IDENT RPAR
312
    {mkexpr (Expr_when ($1, $5, $3))}
313
| MERGE IDENT handler_expr_list
314
    {mkexpr (Expr_merge ($2,$3))}
315

    
316
/* Applications */
317
| IDENT LPAR expr RPAR
318
    {mkexpr (Expr_appl ($1, $3, None))}
319
| IDENT LPAR expr RPAR EVERY IDENT
320
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
321
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
322
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
323
| IDENT LPAR tuple_expr RPAR
324
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
325
| IDENT LPAR tuple_expr RPAR EVERY IDENT
326
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
327
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
328
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
329

    
330
/* Boolean expr */
331
| expr AND expr 
332
    {mkpredef_call "&&" [$1;$3]}
333
| expr AMPERAMPER expr 
334
    {mkpredef_call "&&" [$1;$3]}
335
| expr OR expr 
336
    {mkpredef_call "||" [$1;$3]}
337
| expr BARBAR expr 
338
    {mkpredef_call "||" [$1;$3]}
339
| expr XOR expr 
340
    {mkpredef_call "xor" [$1;$3]}
341
| NOT expr 
342
    {mkpredef_unary_call "not" $2}
343
| expr IMPL expr 
344
    {mkpredef_call "impl" [$1;$3]}
345

    
346
/* Comparison expr */
347
| expr EQ expr 
348
    {mkpredef_call "=" [$1;$3]}
349
| expr LT expr 
350
    {mkpredef_call "<" [$1;$3]}
351
| expr LTE expr 
352
    {mkpredef_call "<=" [$1;$3]}
353
| expr GT expr 
354
    {mkpredef_call ">" [$1;$3]}
355
| expr GTE  expr 
356
    {mkpredef_call ">=" [$1;$3]}
357
| expr NEQ expr 
358
    {mkpredef_call "!=" [$1;$3]}
359

    
360
/* Arithmetic expr */
361
| expr PLUS expr 
362
    {mkpredef_call "+" [$1;$3]}
363
| expr MINUS expr 
364
    {mkpredef_call "-" [$1;$3]}
365
| expr MULT expr 
366
    {mkpredef_call "*" [$1;$3]}
367
| expr DIV expr 
368
    {mkpredef_call "/" [$1;$3]}
369
| MINUS expr %prec UMINUS
370
  {mkpredef_unary_call "uminus" $2}
371
| expr MOD expr 
372
    {mkpredef_call "mod" [$1;$3]}
373

    
374
/* If */
375
| IF expr THEN expr ELSE expr
376
    {mkexpr (Expr_ite ($2, $4, $6))}
377

    
378
handler_expr_list:
379
   { [] }
380
| handler_expr handler_expr_list { $1 :: $2 }
381

    
382
handler_expr:
383
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
384

    
385
signed_const_array:
386
| signed_const { [$1] }
387
| signed_const COMMA signed_const_array { $1 :: $3 }
388

    
389
signed_const_struct:
390
| IDENT EQ signed_const { [ ($1, $3) ] }
391
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
392

    
393
signed_const:
394
  INT {Const_int $1}
395
| REAL {Const_real $1}
396
| FLOAT {Const_float $1}
397
| IDENT {Const_tag $1}
398
| MINUS INT {Const_int (-1 * $2)}
399
| MINUS REAL {Const_real ("-" ^ $2)}
400
| MINUS FLOAT {Const_float (-1. *. $2)}
401
| LCUR signed_const_struct RCUR { Const_struct $2 }
402
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
403

    
404
dim:
405
   INT { mkdim_int $1 }
406
| LPAR dim RPAR { $2 }
407
| IDENT { mkdim_ident $1 }
408
| dim AND dim 
409
    {mkdim_appl "&&" [$1;$3]}
410
| dim AMPERAMPER dim 
411
    {mkdim_appl "&&" [$1;$3]}
412
| dim OR dim 
413
    {mkdim_appl "||" [$1;$3]}
414
| dim BARBAR dim 
415
    {mkdim_appl "||" [$1;$3]}
416
| dim XOR dim 
417
    {mkdim_appl "xor" [$1;$3]}
418
| NOT dim 
419
    {mkdim_appl "not" [$2]}
420
| dim IMPL dim 
421
    {mkdim_appl "impl" [$1;$3]}
422

    
423
/* Comparison dim */
424
| dim EQ dim 
425
    {mkdim_appl "=" [$1;$3]}
426
| dim LT dim 
427
    {mkdim_appl "<" [$1;$3]}
428
| dim LTE dim 
429
    {mkdim_appl "<=" [$1;$3]}
430
| dim GT dim 
431
    {mkdim_appl ">" [$1;$3]}
432
| dim GTE  dim 
433
    {mkdim_appl ">=" [$1;$3]}
434
| dim NEQ dim 
435
    {mkdim_appl "!=" [$1;$3]}
436

    
437
/* Arithmetic dim */
438
| dim PLUS dim 
439
    {mkdim_appl "+" [$1;$3]}
440
| dim MINUS dim 
441
    {mkdim_appl "-" [$1;$3]}
442
| dim MULT dim 
443
    {mkdim_appl "*" [$1;$3]}
444
| dim DIV dim 
445
    {mkdim_appl "/" [$1;$3]}
446
| MINUS dim %prec UMINUS
447
  {mkdim_appl "uminus" [$2]}
448
| dim MOD dim 
449
    {mkdim_appl "mod" [$1;$3]}
450
/* If */
451
| IF dim THEN dim ELSE dim
452
    {mkdim_ite $2 $4 $6}
453

    
454
locals:
455
  {[]}
456
| VAR vdecl_list SCOL {$2}
457

    
458
vdecl_list:
459
    vdecl {$1}
460
| vdecl_list SCOL vdecl {$3 @ $1}
461

    
462
vdecl:
463
/* Useless no ?*/    ident_list
464
    {List.map mkvar_decl 
465
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
466

    
467
| ident_list COL typeconst clock 
468
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
469
| CONST ident_list COL typeconst /* static parameters don't have clocks */
470
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
471

    
472
cdecl_list:
473
  cdecl SCOL { [$1] }
474
| cdecl_list cdecl SCOL { $2::$1 }
475

    
476
cdecl:
477
    IDENT EQ signed_const {
478
      let c = {
479
	const_id = $1;
480
	const_loc = Location.symbol_rloc ();
481
        const_type = Types.new_var ();
482
	const_value = $3;
483
      } in
484
      Hashtbl.add consts_table $1 c; c
485
    }
486

    
487
clock:
488
    {mkclock Ckdec_any}
489
| when_list
490
    {mkclock (Ckdec_bool (List.rev $1))}
491

    
492
when_cond:
493
    WHEN IDENT {($2, tag_true)}
494
| WHENNOT IDENT {($2, tag_false)}
495
| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
496

    
497
when_list:
498
    when_cond {[$1]}
499
| when_list when_cond {$2::$1}
500

    
501
ident_list:
502
  IDENT {[$1]}
503
| ident_list COMMA IDENT {$3::$1}
504

    
505
SCOL_opt:
506
    SCOL {} | {}