lustrec / src / parsers / parser_lustre.mly @ 684d39e7
History | View | Annotate | Download (20.9 KB)
1 |
/********************************************************************/ |
---|---|
2 |
/* */ |
3 |
/* The LustreC compiler toolset / The LustreC Development Team */ |
4 |
/* Copyright 2012 - -- ONERA - CNRS - INPT */ |
5 |
/* */ |
6 |
/* LustreC is free software, distributed WITHOUT ANY WARRANTY */ |
7 |
/* under the terms of the GNU Lesser General Public License */ |
8 |
/* version 2.1. */ |
9 |
/* */ |
10 |
/********************************************************************/ |
11 |
|
12 |
%{ |
13 |
open Utils |
14 |
open Lustre_types |
15 |
open Corelang |
16 |
open Dimension |
17 |
open Parse |
18 |
|
19 |
let get_loc () = Location.symbol_rloc () |
20 |
|
21 |
let mkident x = x, get_loc () |
22 |
let mktyp x = mktyp (get_loc ()) x |
23 |
let mkclock x = mkclock (get_loc ()) x |
24 |
let mkvar_decl x loc = mkvar_decl loc ~orig:true x |
25 |
let mkexpr x = mkexpr (get_loc ()) x |
26 |
let mkeexpr x = mkeexpr (get_loc ()) x |
27 |
let mkeq x = mkeq (get_loc ()) x |
28 |
let mkassert x = mkassert (get_loc ()) x |
29 |
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x |
30 |
let mkpredef_call x = mkpredef_call (get_loc ()) x |
31 |
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*) |
32 |
|
33 |
let mkdim_int i = mkdim_int (get_loc ()) i |
34 |
let mkdim_bool b = mkdim_bool (get_loc ()) b |
35 |
let mkdim_ident id = mkdim_ident (get_loc ()) id |
36 |
let mkdim_appl f args = mkdim_appl (get_loc ()) f args |
37 |
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e |
38 |
|
39 |
let mkannots annots = { annots = annots; annot_loc = get_loc () } |
40 |
|
41 |
let node_stack : ident list ref = ref [] |
42 |
let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack |
43 |
let push_node nd = node_stack:= nd :: !node_stack |
44 |
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false |
45 |
let get_current_node () = try List.hd !node_stack with _ -> assert false |
46 |
|
47 |
let rec fby expr n init = |
48 |
if n<=1 then |
49 |
mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr))) |
50 |
else |
51 |
mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init)))) |
52 |
|
53 |
%} |
54 |
|
55 |
%token <int> INT |
56 |
%token <Num.num * int * string> REAL |
57 |
|
58 |
%token <string> STRING |
59 |
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME |
60 |
%token ASSERT OPEN INCLUDE QUOTE POINT FUNCTION |
61 |
%token <string> IDENT |
62 |
%token <string> UIDENT |
63 |
%token TRUE FALSE |
64 |
%token <Lustre_types.expr_annot> ANNOT |
65 |
%token <Lustre_types.contract_desc> NODESPEC |
66 |
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL |
67 |
%token AMPERAMPER BARBAR NOT POWER |
68 |
%token IF THEN ELSE |
69 |
%token MERGE FBY WHEN WHENNOT EVERY |
70 |
%token NODE LET TEL RETURNS VAR IMPORTED TYPE CONST |
71 |
%token STRUCT ENUM |
72 |
%token TINT TREAL TBOOL TCLOCK |
73 |
%token EQ LT GT LTE GTE NEQ |
74 |
%token AND OR XOR IMPL |
75 |
%token MULT DIV MOD |
76 |
%token MINUS PLUS UMINUS |
77 |
%token PRE ARROW |
78 |
%token REQUIRE ENSURE ASSUME GUARANTEES IMPORT CONTRACT |
79 |
%token INVARIANT MODE CCODE MATLAB |
80 |
%token EXISTS FORALL |
81 |
%token PROTOTYPE LIB |
82 |
%token EOF |
83 |
|
84 |
%nonassoc prec_exists prec_forall |
85 |
%nonassoc COMMA |
86 |
%nonassoc EVERY |
87 |
%left MERGE IF |
88 |
%nonassoc ELSE |
89 |
%right ARROW FBY |
90 |
%left WHEN WHENNOT |
91 |
%right COLCOL |
92 |
%right IMPL |
93 |
%left OR XOR BARBAR |
94 |
%left AND AMPERAMPER |
95 |
%left NOT |
96 |
%nonassoc INT |
97 |
%nonassoc EQ LT GT LTE GTE NEQ |
98 |
%left MINUS PLUS |
99 |
%left MULT DIV MOD |
100 |
%left UMINUS |
101 |
%left POWER |
102 |
%left PRE LAST |
103 |
%nonassoc RBRACKET |
104 |
%nonassoc LBRACKET |
105 |
|
106 |
%start prog |
107 |
%type <Lustre_types.top_decl list> prog |
108 |
|
109 |
%start header |
110 |
%type <Lustre_types.top_decl list> header |
111 |
|
112 |
%start lustre_annot |
113 |
%type <Lustre_types.expr_annot> lustre_annot |
114 |
|
115 |
%start lustre_spec |
116 |
%type <Lustre_types.contract_desc> lustre_spec |
117 |
|
118 |
%start signed_const |
119 |
%type <Lustre_types.constant> signed_const |
120 |
|
121 |
%start expr |
122 |
%type <Lustre_types.expr> expr |
123 |
|
124 |
%start stmt_list |
125 |
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list |
126 |
|
127 |
%start vdecl_list |
128 |
%type <Lustre_types.var_decl list> vdecl_list |
129 |
%% |
130 |
|
131 |
|
132 |
module_ident: |
133 |
UIDENT { $1 } |
134 |
| IDENT { $1 } |
135 |
|
136 |
file_ident: |
137 |
module_ident { $1 } |
138 |
| module_ident POINT file_ident { $1 ^ "." ^ $3 } |
139 |
|
140 |
path_ident: |
141 |
POINT DIV path_ident { "./" ^ $3 } |
142 |
| file_ident DIV path_ident { $1 ^ "/" ^ $3 } |
143 |
| DIV path_ident { "/" ^ $2 } |
144 |
| file_ident { $1 } |
145 |
|
146 |
tag_ident: |
147 |
UIDENT { $1 } |
148 |
| TRUE { tag_true } |
149 |
| FALSE { tag_false } |
150 |
|
151 |
node_ident: |
152 |
UIDENT { $1 } |
153 |
| IDENT { $1 } |
154 |
|
155 |
node_ident_decl: |
156 |
node_ident { push_node $1; $1 } |
157 |
|
158 |
vdecl_ident: |
159 |
UIDENT { mkident $1 } |
160 |
| IDENT { mkident $1 } |
161 |
|
162 |
const_ident: |
163 |
UIDENT { $1 } |
164 |
| IDENT { $1 } |
165 |
|
166 |
type_ident: |
167 |
IDENT { $1 } |
168 |
|
169 |
prog: |
170 |
prefix_prog top_decl_list EOF { $1 @ (List.rev $2) } |
171 |
|
172 |
prefix_prog: |
173 |
{ [] } |
174 |
| open_lusi prefix_prog { $1 :: $2 } |
175 |
| typ_def prefix_prog { ($1 false (* not a header *)) :: $2 } |
176 |
|
177 |
prefix_header: |
178 |
{ [] } |
179 |
| open_lusi prefix_header { $1 :: $2 } |
180 |
| typ_def prefix_header { ($1 true (* is a header *)) :: $2 } |
181 |
|
182 |
header: |
183 |
prefix_header top_decl_header_list EOF { $1 @ (List.rev $2) } |
184 |
|
185 |
|
186 |
open_lusi: |
187 |
| OPEN QUOTE path_ident QUOTE { mktop_decl false (Open (true, $3)) } |
188 |
| INCLUDE QUOTE path_ident QUOTE { mktop_decl false (Include ($3)) } |
189 |
| OPEN LT path_ident GT { mktop_decl false (Open (false, $3)) } |
190 |
|
191 |
top_decl_list: |
192 |
{[]} |
193 |
| top_decl_list top_decl {$2@$1} |
194 |
|
195 |
|
196 |
top_decl_header_list: |
197 |
{ [] } |
198 |
| top_decl_header_list top_decl_header { $2@$1 } |
199 |
|
200 |
state_annot: |
201 |
FUNCTION { true } |
202 |
| NODE { false } |
203 |
|
204 |
top_decl_header: |
205 |
| CONST cdecl_list { List.rev ($2 true) } |
206 |
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_list SCOL |
207 |
{let nd = mktop_decl true (ImportedNode |
208 |
{nodei_id = $3; |
209 |
nodei_type = Types.new_var (); |
210 |
nodei_clock = Clocks.new_var true; |
211 |
nodei_inputs = List.rev $5; |
212 |
nodei_outputs = List.rev $10; |
213 |
nodei_stateless = $2; |
214 |
nodei_spec = $1; |
215 |
nodei_prototype = $13; |
216 |
nodei_in_lib = $14;}) |
217 |
in |
218 |
(*add_imported_node $3 nd;*) [nd] } |
219 |
| CONTRACT node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL |
220 |
{let nd = mktop_decl true (ImportedNode |
221 |
{nodei_id = $2; |
222 |
nodei_type = Types.new_var (); |
223 |
nodei_clock = Clocks.new_var true; |
224 |
nodei_inputs = List.rev $4; |
225 |
nodei_outputs = List.rev $9; |
226 |
nodei_stateless = false (* By default we assume contracts as stateful *); |
227 |
nodei_spec = Some $14; |
228 |
nodei_prototype = None; |
229 |
nodei_in_lib = [];}) |
230 |
in |
231 |
(*add_imported_node $3 nd;*) [nd] } |
232 |
|
233 |
prototype_opt: |
234 |
{ None } |
235 |
| PROTOTYPE node_ident { Some $2} |
236 |
|
237 |
in_lib_list: |
238 |
{ [] } |
239 |
| LIB module_ident in_lib_list { $2::$3 } |
240 |
|
241 |
top_decl: |
242 |
| CONST cdecl_list { List.rev ($2 false) } |
243 |
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespec_list locals LET stmt_list TEL |
244 |
{ |
245 |
let stmts, asserts, annots = $16 in |
246 |
(* Declaring eqs annots *) |
247 |
List.iter (fun ann -> |
248 |
List.iter (fun (key, _) -> |
249 |
Annotations.add_node_ann $2 key |
250 |
) ann.annots |
251 |
) annots; |
252 |
(* Building the node *) |
253 |
let nd = mktop_decl false (Node |
254 |
{node_id = $2; |
255 |
node_type = Types.new_var (); |
256 |
node_clock = Clocks.new_var true; |
257 |
node_inputs = List.rev $4; |
258 |
node_outputs = List.rev $9; |
259 |
node_locals = List.rev $14; |
260 |
node_gencalls = []; |
261 |
node_checks = []; |
262 |
node_asserts = asserts; |
263 |
node_stmts = stmts; |
264 |
node_dec_stateless = $1; |
265 |
node_stateless = None; |
266 |
node_spec = $13; |
267 |
node_annot = annots}) |
268 |
in |
269 |
pop_node (); |
270 |
(*add_node $3 nd;*) [nd] } |
271 |
|
272 |
| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL |
273 |
{let nd = mktop_decl true (ImportedNode |
274 |
{nodei_id = $3; |
275 |
nodei_type = Types.new_var (); |
276 |
nodei_clock = Clocks.new_var true; |
277 |
nodei_inputs = List.rev $5; |
278 |
nodei_outputs = List.rev $10; |
279 |
nodei_stateless = $1; |
280 |
nodei_spec = Some $15; |
281 |
nodei_prototype = None; |
282 |
nodei_in_lib = [];}) |
283 |
in |
284 |
pop_node (); |
285 |
(*add_imported_node $3 nd;*) [nd] } |
286 |
| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL |
287 |
{let nd = mktop_decl true (ImportedNode |
288 |
{nodei_id = $3; |
289 |
nodei_type = Types.new_var (); |
290 |
nodei_clock = Clocks.new_var true; |
291 |
nodei_inputs = List.rev $5; |
292 |
nodei_outputs = List.rev $10; |
293 |
nodei_stateless = $1; |
294 |
nodei_spec = None; |
295 |
nodei_prototype = None; |
296 |
nodei_in_lib = [];}) |
297 |
in |
298 |
pop_node (); |
299 |
(*add_imported_node $3 nd;*) [nd] } |
300 |
|
301 |
nodespec_list: |
302 |
{ None } |
303 |
| NODESPEC nodespec_list { |
304 |
(function |
305 |
| None -> (fun s1 -> Some s1) |
306 |
| Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 } |
307 |
|
308 |
typ_def_list: |
309 |
/* empty */ { (fun itf -> []) } |
310 |
| typ_def typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($2 itf)) } |
311 |
|
312 |
typ_def: |
313 |
TYPE type_ident EQ typ_def_rhs SCOL { (fun itf -> |
314 |
let typ = mktop_decl itf (TypeDef { tydef_id = $2; |
315 |
tydef_desc = $4 |
316 |
}) |
317 |
in (*add_type itf $2 typ;*) typ) } |
318 |
|
319 |
typ_def_rhs: |
320 |
typeconst { $1 } |
321 |
| ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) } |
322 |
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) } |
323 |
|
324 |
array_typ_decl: |
325 |
%prec POWER { fun typ -> typ } |
326 |
| POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) } |
327 |
|
328 |
typeconst: |
329 |
TINT array_typ_decl { $2 Tydec_int } |
330 |
| TBOOL array_typ_decl { $2 Tydec_bool } |
331 |
| TREAL array_typ_decl { $2 Tydec_real } |
332 |
/* | TFLOAT array_typ_decl { $2 Tydec_float } */ |
333 |
| type_ident array_typ_decl { $2 (Tydec_const $1) } |
334 |
| TBOOL TCLOCK { Tydec_clock Tydec_bool } |
335 |
| IDENT TCLOCK { Tydec_clock (Tydec_const $1) } |
336 |
|
337 |
tag_list: |
338 |
UIDENT { $1 :: [] } |
339 |
| tag_list COMMA UIDENT { $3 :: $1 } |
340 |
|
341 |
field_list: { [] } |
342 |
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 } |
343 |
|
344 |
stmt_list: |
345 |
{ [], [], [] } |
346 |
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl} |
347 |
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl} |
348 |
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl} |
349 |
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl} |
350 |
|
351 |
automaton: |
352 |
AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 } |
353 |
|
354 |
handler_list: |
355 |
{ [] } |
356 |
| handler handler_list { $1::$2 } |
357 |
|
358 |
handler: |
359 |
STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 } |
360 |
|
361 |
unless_list: |
362 |
{ [] } |
363 |
| unless unless_list { $1::$2 } |
364 |
|
365 |
until_list: |
366 |
{ [] } |
367 |
| until until_list { $1::$2 } |
368 |
|
369 |
unless: |
370 |
UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4) } |
371 |
| UNLESS expr RESUME UIDENT { (get_loc (), $2, false, $4) } |
372 |
|
373 |
until: |
374 |
UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4) } |
375 |
| UNTIL expr RESUME UIDENT { (get_loc (), $2, false, $4) } |
376 |
|
377 |
assert_: |
378 |
| ASSERT expr SCOL {mkassert ($2)} |
379 |
|
380 |
eq: |
381 |
ident_list EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)} |
382 |
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)} |
383 |
|
384 |
lustre_spec: |
385 |
| contract EOF { $1 } |
386 |
|
387 |
contract: |
388 |
{ empty_contract } |
389 |
| CONTRACT contract { $2 } |
390 |
| CONST IDENT EQ expr SCOL contract |
391 |
{ merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 } |
392 |
| CONST IDENT COL typeconst EQ expr SCOL contract |
393 |
{ merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 } |
394 |
| VAR IDENT COL typeconst EQ expr SCOL contract |
395 |
{ merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 } |
396 |
| ASSUME qexpr SCOL contract |
397 |
{ merge_contracts (mk_contract_assume $2) $4 } |
398 |
| GUARANTEES qexpr SCOL contract |
399 |
{ merge_contracts (mk_contract_guarantees $2) $4 } |
400 |
| MODE IDENT LPAR mode_content RPAR SCOL contract |
401 |
{ merge_contracts ( |
402 |
let r, e = $4 in |
403 |
mk_contract_mode $2 r e (get_loc())) $7 } |
404 |
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract |
405 |
{ merge_contracts (mk_contract_import $2 $4 $8 (get_loc())) $11 } |
406 |
|
407 |
mode_content: |
408 |
{ [], [] } |
409 |
| REQUIRE qexpr SCOL mode_content { let (r,e) = $4 in $2::r, e } |
410 |
| ENSURE qexpr SCOL mode_content { let (r,e) = $4 in r, $2::e } |
411 |
|
412 |
/* WARNING: UNUSED RULES */ |
413 |
tuple_qexpr: |
414 |
| qexpr COMMA qexpr {[$3;$1]} |
415 |
| tuple_qexpr COMMA qexpr {$3::$1} |
416 |
|
417 |
qexpr: |
418 |
| expr { mkeexpr $1 } |
419 |
/* Quantifiers */ |
420 |
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } |
421 |
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 } |
422 |
|
423 |
|
424 |
tuple_expr: |
425 |
expr COMMA expr {[$3;$1]} |
426 |
| tuple_expr COMMA expr {$3::$1} |
427 |
|
428 |
// Same as tuple expr but accepting lists with single element |
429 |
array_expr: |
430 |
expr {[$1]} |
431 |
| expr COMMA array_expr {$1::$3} |
432 |
|
433 |
dim_list: |
434 |
dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) } |
435 |
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) } |
436 |
|
437 |
expr: |
438 |
/* constants */ |
439 |
INT {mkexpr (Expr_const (Const_int $1))} |
440 |
| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))} |
441 |
| STRING {mkexpr (Expr_const (Const_string $1))} |
442 |
| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))} |
443 |
|
444 |
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/ |
445 |
/* Idents or type enum tags */ |
446 |
| IDENT { mkexpr (Expr_ident $1) } |
447 |
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) } |
448 |
| LPAR ANNOT expr RPAR |
449 |
{update_expr_annot (get_current_node ()) $3 $2} |
450 |
| LPAR expr RPAR |
451 |
{$2} |
452 |
| LPAR tuple_expr RPAR |
453 |
{mkexpr (Expr_tuple (List.rev $2))} |
454 |
|
455 |
/* Array expressions */ |
456 |
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } |
457 |
| expr POWER dim { mkexpr (Expr_power ($1, $3)) } |
458 |
| expr LBRACKET dim_list { $3 $1 } |
459 |
|
460 |
/* Temporal operators */ |
461 |
| PRE expr |
462 |
{mkexpr (Expr_pre $2)} |
463 |
| expr ARROW expr |
464 |
{mkexpr (Expr_arrow ($1,$3))} |
465 |
| expr FBY expr |
466 |
{(*mkexpr (Expr_fby ($1,$3))*) |
467 |
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
468 |
| expr WHEN vdecl_ident |
469 |
{mkexpr (Expr_when ($1,fst $3,tag_true))} |
470 |
| expr WHENNOT vdecl_ident |
471 |
{mkexpr (Expr_when ($1,fst $3,tag_false))} |
472 |
| expr WHEN tag_ident LPAR vdecl_ident RPAR |
473 |
{mkexpr (Expr_when ($1, fst $5, $3))} |
474 |
| MERGE vdecl_ident handler_expr_list |
475 |
{mkexpr (Expr_merge (fst $2,$3))} |
476 |
|
477 |
/* Applications */ |
478 |
| node_ident LPAR expr RPAR |
479 |
{mkexpr (Expr_appl ($1, $3, None))} |
480 |
| node_ident LPAR expr RPAR EVERY expr |
481 |
{mkexpr (Expr_appl ($1, $3, Some $6))} |
482 |
| node_ident LPAR tuple_expr RPAR |
483 |
{ |
484 |
let id=$1 in |
485 |
let args=List.rev $3 in |
486 |
match id, args with |
487 |
| "fbyn", [expr;n;init] -> |
488 |
let n = match n.expr_desc with |
489 |
| Expr_const (Const_int n) -> n |
490 |
| _ -> assert false |
491 |
in |
492 |
fby expr n init |
493 |
| _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None)) |
494 |
} |
495 |
| node_ident LPAR tuple_expr RPAR EVERY expr |
496 |
{ |
497 |
let id=$1 in |
498 |
let args=List.rev $3 in |
499 |
let clock=$6 in |
500 |
if id="fby" then |
501 |
assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *) |
502 |
else |
503 |
mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) |
504 |
} |
505 |
|
506 |
/* Boolean expr */ |
507 |
| expr AND expr |
508 |
{mkpredef_call "&&" [$1;$3]} |
509 |
| expr AMPERAMPER expr |
510 |
{mkpredef_call "&&" [$1;$3]} |
511 |
| expr OR expr |
512 |
{mkpredef_call "||" [$1;$3]} |
513 |
| expr BARBAR expr |
514 |
{mkpredef_call "||" [$1;$3]} |
515 |
| expr XOR expr |
516 |
{mkpredef_call "xor" [$1;$3]} |
517 |
| NOT expr |
518 |
{mkpredef_call "not" [$2]} |
519 |
| expr IMPL expr |
520 |
{mkpredef_call "impl" [$1;$3]} |
521 |
|
522 |
/* Comparison expr */ |
523 |
| expr EQ expr |
524 |
{mkpredef_call "=" [$1;$3]} |
525 |
| expr LT expr |
526 |
{mkpredef_call "<" [$1;$3]} |
527 |
| expr LTE expr |
528 |
{mkpredef_call "<=" [$1;$3]} |
529 |
| expr GT expr |
530 |
{mkpredef_call ">" [$1;$3]} |
531 |
| expr GTE expr |
532 |
{mkpredef_call ">=" [$1;$3]} |
533 |
| expr NEQ expr |
534 |
{mkpredef_call "!=" [$1;$3]} |
535 |
|
536 |
/* Arithmetic expr */ |
537 |
| expr PLUS expr |
538 |
{mkpredef_call "+" [$1;$3]} |
539 |
| expr MINUS expr |
540 |
{mkpredef_call "-" [$1;$3]} |
541 |
| expr MULT expr |
542 |
{mkpredef_call "*" [$1;$3]} |
543 |
| expr DIV expr |
544 |
{mkpredef_call "/" [$1;$3]} |
545 |
| MINUS expr %prec UMINUS |
546 |
{mkpredef_call "uminus" [$2]} |
547 |
| expr MOD expr |
548 |
{mkpredef_call "mod" [$1;$3]} |
549 |
|
550 |
/* If */ |
551 |
| IF expr THEN expr ELSE expr |
552 |
{mkexpr (Expr_ite ($2, $4, $6))} |
553 |
|
554 |
handler_expr_list: |
555 |
{ [] } |
556 |
| handler_expr handler_expr_list { $1 :: $2 } |
557 |
|
558 |
handler_expr: |
559 |
LPAR tag_ident ARROW expr RPAR { ($2, $4) } |
560 |
|
561 |
signed_const_array: |
562 |
| signed_const { [$1] } |
563 |
| signed_const COMMA signed_const_array { $1 :: $3 } |
564 |
|
565 |
signed_const_struct: |
566 |
| IDENT EQ signed_const { [ ($1, $3) ] } |
567 |
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 } |
568 |
|
569 |
signed_const: |
570 |
INT {Const_int $1} |
571 |
| REAL {let c,e,s =$1 in Const_real (c,e,s)} |
572 |
/* | FLOAT {Const_float $1} */ |
573 |
| tag_ident {Const_tag $1} |
574 |
| MINUS INT {Const_int (-1 * $2)} |
575 |
| MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)} |
576 |
/* | MINUS FLOAT {Const_float (-1. *. $2)} */ |
577 |
| LCUR signed_const_struct RCUR { Const_struct $2 } |
578 |
| LBRACKET signed_const_array RBRACKET { Const_array $2 } |
579 |
|
580 |
dim: |
581 |
INT { mkdim_int $1 } |
582 |
| LPAR dim RPAR { $2 } |
583 |
| UIDENT { mkdim_ident $1 } |
584 |
| IDENT { mkdim_ident $1 } |
585 |
| dim AND dim |
586 |
{mkdim_appl "&&" [$1;$3]} |
587 |
| dim AMPERAMPER dim |
588 |
{mkdim_appl "&&" [$1;$3]} |
589 |
| dim OR dim |
590 |
{mkdim_appl "||" [$1;$3]} |
591 |
| dim BARBAR dim |
592 |
{mkdim_appl "||" [$1;$3]} |
593 |
| dim XOR dim |
594 |
{mkdim_appl "xor" [$1;$3]} |
595 |
| NOT dim |
596 |
{mkdim_appl "not" [$2]} |
597 |
| dim IMPL dim |
598 |
{mkdim_appl "impl" [$1;$3]} |
599 |
|
600 |
/* Comparison dim */ |
601 |
| dim EQ dim |
602 |
{mkdim_appl "=" [$1;$3]} |
603 |
| dim LT dim |
604 |
{mkdim_appl "<" [$1;$3]} |
605 |
| dim LTE dim |
606 |
{mkdim_appl "<=" [$1;$3]} |
607 |
| dim GT dim |
608 |
{mkdim_appl ">" [$1;$3]} |
609 |
| dim GTE dim |
610 |
{mkdim_appl ">=" [$1;$3]} |
611 |
| dim NEQ dim |
612 |
{mkdim_appl "!=" [$1;$3]} |
613 |
|
614 |
/* Arithmetic dim */ |
615 |
| dim PLUS dim |
616 |
{mkdim_appl "+" [$1;$3]} |
617 |
| dim MINUS dim |
618 |
{mkdim_appl "-" [$1;$3]} |
619 |
| dim MULT dim |
620 |
{mkdim_appl "*" [$1;$3]} |
621 |
| dim DIV dim |
622 |
{mkdim_appl "/" [$1;$3]} |
623 |
| MINUS dim %prec UMINUS |
624 |
{mkdim_appl "uminus" [$2]} |
625 |
| dim MOD dim |
626 |
{mkdim_appl "mod" [$1;$3]} |
627 |
/* If */ |
628 |
| IF dim THEN dim ELSE dim |
629 |
{mkdim_ite $2 $4 $6} |
630 |
|
631 |
locals: |
632 |
{[]} |
633 |
| VAR local_vdecl_list SCOL {$2} |
634 |
|
635 |
vdecl_list: |
636 |
vdecl {$1} |
637 |
| vdecl_list SCOL vdecl {$3 @ $1} |
638 |
|
639 |
vdecl: |
640 |
ident_list COL typeconst clock |
641 |
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 } |
642 |
| CONST ident_list /* static parameters don't have clocks */ |
643 |
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 } |
644 |
| CONST ident_list COL typeconst /* static parameters don't have clocks */ |
645 |
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 } |
646 |
|
647 |
local_vdecl_list: |
648 |
local_vdecl {$1} |
649 |
| local_vdecl_list SCOL local_vdecl {$3 @ $1} |
650 |
|
651 |
local_vdecl: |
652 |
/* Useless no ?*/ ident_list |
653 |
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 } |
654 |
| ident_list COL typeconst clock |
655 |
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 } |
656 |
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */ |
657 |
{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] } |
658 |
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */ |
659 |
{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] } |
660 |
|
661 |
cdecl_list: |
662 |
cdecl SCOL { (fun itf -> [$1 itf]) } |
663 |
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) } |
664 |
|
665 |
cdecl: |
666 |
const_ident EQ signed_const { |
667 |
(fun itf -> |
668 |
let c = mktop_decl itf (Const { |
669 |
const_id = $1; |
670 |
const_loc = Location.symbol_rloc (); |
671 |
const_type = Types.new_var (); |
672 |
const_value = $3}) |
673 |
in |
674 |
(*add_const itf $1 c;*) c) |
675 |
} |
676 |
|
677 |
clock: |
678 |
{mkclock Ckdec_any} |
679 |
| when_list |
680 |
{mkclock (Ckdec_bool (List.rev $1))} |
681 |
|
682 |
when_cond: |
683 |
WHEN IDENT {($2, tag_true)} |
684 |
| WHENNOT IDENT {($2, tag_false)} |
685 |
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)} |
686 |
|
687 |
when_list: |
688 |
when_cond {[$1]} |
689 |
| when_list when_cond {$2::$1} |
690 |
|
691 |
ident_list: |
692 |
vdecl_ident {[$1]} |
693 |
| ident_list COMMA vdecl_ident {$3::$1} |
694 |
|
695 |
SCOL_opt: |
696 |
SCOL {} | {} |
697 |
|
698 |
|
699 |
lustre_annot: |
700 |
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } } |
701 |
|
702 |
lustre_annot_list: |
703 |
{ [] } |
704 |
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 } |
705 |
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 } |
706 |
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } |
707 |
// (* | OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } *) |
708 |
| CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 } |
709 |
| MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 } |
710 |
|
711 |
|
712 |
kwd: |
713 |
DIV { [] } |
714 |
| DIV IDENT kwd { $2::$3} |
715 |
|
716 |
%% |
717 |
(* Local Variables: *) |
718 |
(* compile-command:"make -C .." *) |
719 |
(* End: *) |
720 |
|
721 |
|