Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parser_lustre.mly @ b616fe7a

History | View | Annotate | Download (14.9 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

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

    
44
let add_node loc own msg hashtbl name value =
45
  try
46
    match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with
47
    | Node _        , ImportedNode _ when own   -> ()
48
    | ImportedNode _, _                         -> Hashtbl.add hashtbl name value
49
    | Node _        , _                         -> raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))
50
    | _                                         -> assert false
51
  with
52
    Not_found                                   -> Hashtbl.add hashtbl name value
53

    
54

    
55
let add_symbol loc msg hashtbl name value =
56
 if Hashtbl.mem hashtbl name
57
 then raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))
58
 else Hashtbl.add hashtbl name value
59

    
60
let check_symbol loc msg hashtbl name =
61
 if not (Hashtbl.mem hashtbl name)
62
 then raise (Corelang.Error (loc, Corelang.Unbound_symbol msg))
63
 else ()
64

    
65
%}
66

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

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

    
112
%start prog
113
%type <Corelang.top_decl list> prog
114
%start header
115
%type <bool -> Corelang.top_decl list> header
116

    
117
%%
118

    
119
prog:
120
 open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }
121

    
122
header:
123
 open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ (List.rev ($3 own)))) }
124

    
125
open_list:
126
  { [] }
127
| open_lusi open_list { $1 :: $2 }
128

    
129
open_lusi:
130
| OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))}
131
| OPEN LT IDENT GT { mktop_decl (Open (false, $3)) }
132

    
133
top_decl_list:
134
  top_decl {[$1]}
135
| top_decl_list top_decl {$2::$1}
136

    
137

    
138
top_decl_header_list:
139
  top_decl_header {(fun own -> [$1 own]) }
140
| top_decl_header_list top_decl_header {(fun own -> ($2 own)::($1 own)) }
141

    
142
state_annot:
143
  FUNCTION { true }
144
| NODE { false }
145

    
146
top_decl_header:
147
| CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ -> top }
148
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_opt SCOL
149
    {let nd = mktop_decl (ImportedNode
150
                            {nodei_id = $3;
151
                             nodei_type = Types.new_var ();
152
                             nodei_clock = Clocks.new_var true;
153
                             nodei_inputs = List.rev $5;
154
                             nodei_outputs = List.rev $10;
155
			     nodei_stateless = $2;
156
			     nodei_spec = $1;
157
			     nodei_prototype = $13;
158
			     nodei_in_lib = $14;})
159
    in
160
    (let loc = Location.symbol_rloc () in 
161
     fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) }
162

    
163
prototype_opt:
164
 { None }
165
| PROTOTYPE IDENT { Some $2}
166

    
167
in_lib_opt:
168
{ None }
169
| LIB IDENT {Some $2} 
170

    
171
top_decl:
172
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
173
| 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 
174
    {let eqs, asserts, annots = $16 in
175
     let nd = mktop_decl (Node
176
                            {node_id = $3;
177
                             node_type = Types.new_var ();
178
                             node_clock = Clocks.new_var true;
179
                             node_inputs = List.rev $5;
180
                             node_outputs = List.rev $10;
181
                             node_locals = List.rev $14;
182
			     node_gencalls = [];
183
			     node_checks = [];
184
			     node_asserts = asserts; 
185
                             node_eqs = eqs;
186
			     node_dec_stateless = $2;
187
			     node_stateless = None;
188
			     node_spec = $1;
189
			     node_annot = match annots with [] -> None | _ -> Some annots})
190
     in
191
     let loc = Location.symbol_rloc () in
192
     add_node loc true ("node " ^ $3) node_table $3 nd; nd}
193

    
194
nodespec_list:
195
 { None }
196
| NODESPEC nodespec_list { (function None -> (fun s1 -> Some s1) | Some s2 -> (fun s1 -> Some (LustreSpec.merge_node_annot s1 s2))) $2 $1 }
197

    
198
typ_def_list:
199
    /* empty */ {}
200
| typ_def SCOL typ_def_list {$1;$3}
201

    
202
typ_def:
203
  TYPE IDENT EQ typeconst {
204
    try
205
      let loc = Location.symbol_rloc () in
206
      add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (Corelang.get_repr_type $4)
207
    with Not_found-> assert false }
208
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
209
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) }
210

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

    
215
typeconst:
216
  TINT array_typ_decl  { $2 Tydec_int }
217
| TBOOL array_typ_decl { $2 Tydec_bool  }
218
| TREAL array_typ_decl { $2 Tydec_real  }
219
| TFLOAT array_typ_decl { $2 Tydec_float }
220
| IDENT array_typ_decl { 
221
        let loc = Location.symbol_rloc () in
222
	check_symbol loc ("type " ^ $1) type_table (Tydec_const $1); $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
  { let loc = Location.symbol_rloc () in 
229
    (fun t -> 
230
      add_symbol loc ("tag " ^ $1) tag_table $1 t; $1 :: []) }
231
| tag_list COMMA IDENT
232
      {       
233
	let loc = Location.symbol_rloc () in
234
	(fun t -> add_symbol loc ("tag " ^ $3)tag_table $3 t; $3 :: ($1 t)) 
235
      }
236
      
237
field_list:
238
  { (fun t -> []) }
239
| field_list IDENT COL typeconst SCOL
240
      {
241
	let loc = Location.symbol_rloc () in
242
	(fun t -> add_symbol loc ("field " ^ $2) field_table $2 t; ($1 t) @ [ ($2, $4) ]) }
243
      
244
eq_list:
245
  { [], [], [] }
246
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
247
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
248
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}
249
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
250

    
251
automaton:
252
 AUTOMATON IDENT handler_list { failwith "not implemented" }
253

    
254
handler_list:
255
     { [] }
256
| handler handler_list { $1::$2 }
257

    
258
handler:
259
 STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
260

    
261
unless_list:
262
    { [] }
263
| unless unless_list { $1::$2 }
264

    
265
until_list:
266
    { [] }
267
| until until_list { $1::$2 }
268

    
269
unless:
270
  UNLESS expr RESTART IDENT { }
271
| UNLESS expr RESUME IDENT  { }
272

    
273
until:
274
  UNTIL expr RESTART IDENT { }
275
| UNTIL expr RESUME IDENT  { }
276

    
277
assert_:
278
| ASSERT expr SCOL {mkassert ($2)}
279

    
280
eq:
281
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
282
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
283

    
284
tuple_expr:
285
    expr COMMA expr {[$3;$1]}
286
| tuple_expr COMMA expr {$3::$1}
287

    
288
// Same as tuple expr but accepting lists with single element
289
array_expr:
290
  expr {[$1]}
291
| expr COMMA array_expr {$1::$3}
292

    
293
dim_list:
294
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
295
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
296

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

    
314
/* Array expressions */
315
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
316
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
317
| expr LBRACKET dim_list { $3 $1 }
318

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

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

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

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

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

    
394
/* If */
395
| IF expr THEN expr ELSE expr
396
    {mkexpr (Expr_ite ($2, $4, $6))}
397

    
398
handler_expr_list:
399
   { [] }
400
| handler_expr handler_expr_list { $1 :: $2 }
401

    
402
handler_expr:
403
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
404

    
405
signed_const_array:
406
| signed_const { [$1] }
407
| signed_const COMMA signed_const_array { $1 :: $3 }
408

    
409
signed_const_struct:
410
| IDENT EQ signed_const { [ ($1, $3) ] }
411
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
412

    
413
signed_const:
414
  INT {Const_int $1}
415
| REAL {Const_real $1}
416
| FLOAT {Const_float $1}
417
| IDENT {Const_tag $1}
418
| MINUS INT {Const_int (-1 * $2)}
419
| MINUS REAL {Const_real ("-" ^ $2)}
420
| MINUS FLOAT {Const_float (-1. *. $2)}
421
| LCUR signed_const_struct RCUR { Const_struct $2 }
422
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
423

    
424
dim:
425
   INT { mkdim_int $1 }
426
| LPAR dim RPAR { $2 }
427
| IDENT { mkdim_ident $1 }
428
| dim AND dim 
429
    {mkdim_appl "&&" [$1;$3]}
430
| dim AMPERAMPER dim 
431
    {mkdim_appl "&&" [$1;$3]}
432
| dim OR dim 
433
    {mkdim_appl "||" [$1;$3]}
434
| dim BARBAR dim 
435
    {mkdim_appl "||" [$1;$3]}
436
| dim XOR dim 
437
    {mkdim_appl "xor" [$1;$3]}
438
| NOT dim 
439
    {mkdim_appl "not" [$2]}
440
| dim IMPL dim 
441
    {mkdim_appl "impl" [$1;$3]}
442

    
443
/* Comparison dim */
444
| dim EQ dim 
445
    {mkdim_appl "=" [$1;$3]}
446
| dim LT dim 
447
    {mkdim_appl "<" [$1;$3]}
448
| dim LTE dim 
449
    {mkdim_appl "<=" [$1;$3]}
450
| dim GT dim 
451
    {mkdim_appl ">" [$1;$3]}
452
| dim GTE  dim 
453
    {mkdim_appl ">=" [$1;$3]}
454
| dim NEQ dim 
455
    {mkdim_appl "!=" [$1;$3]}
456

    
457
/* Arithmetic dim */
458
| dim PLUS dim 
459
    {mkdim_appl "+" [$1;$3]}
460
| dim MINUS dim 
461
    {mkdim_appl "-" [$1;$3]}
462
| dim MULT dim 
463
    {mkdim_appl "*" [$1;$3]}
464
| dim DIV dim 
465
    {mkdim_appl "/" [$1;$3]}
466
| MINUS dim %prec UMINUS
467
  {mkdim_appl "uminus" [$2]}
468
| dim MOD dim 
469
    {mkdim_appl "mod" [$1;$3]}
470
/* If */
471
| IF dim THEN dim ELSE dim
472
    {mkdim_ite $2 $4 $6}
473

    
474
locals:
475
  {[]}
476
| VAR vdecl_list SCOL {$2}
477

    
478
vdecl_list:
479
    vdecl {$1}
480
| vdecl_list SCOL vdecl {$3 @ $1}
481

    
482
vdecl:
483
/* Useless no ?*/    ident_list
484
    {List.map mkvar_decl 
485
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
486

    
487
| ident_list COL typeconst clock 
488
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
489
| CONST ident_list COL typeconst /* static parameters don't have clocks */
490
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
491

    
492
cdecl_list:
493
  cdecl SCOL { [$1] }
494
| cdecl_list cdecl SCOL { $2::$1 }
495

    
496
cdecl:
497
    IDENT EQ signed_const {
498
      let c = {
499
	const_id = $1;
500
	const_loc = Location.symbol_rloc ();
501
        const_type = Types.new_var ();
502
	const_value = $3;
503
      } in
504
      Hashtbl.add consts_table $1 c; c
505
    }
506

    
507
clock:
508
    {mkclock Ckdec_any}
509
| when_list
510
    {mkclock (Ckdec_bool (List.rev $1))}
511

    
512
when_cond:
513
    WHEN IDENT {($2, tag_true)}
514
| WHENNOT IDENT {($2, tag_false)}
515
| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
516

    
517
when_list:
518
    when_cond {[$1]}
519
| when_list when_cond {$2::$1}
520

    
521
ident_list:
522
  IDENT {[$1]}
523
| ident_list COMMA IDENT {$3::$1}
524

    
525
SCOL_opt:
526
    SCOL {} | {}