Revision f4cba4b8 src/parsers/parser_lustre.mly
src/parsers/parser_lustre.mly | ||
---|---|---|
49 | 49 |
mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr))) |
50 | 50 |
else |
51 | 51 |
mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init)))) |
52 |
|
|
52 |
|
|
53 |
|
|
53 | 54 |
%} |
54 | 55 |
|
55 | 56 |
%token <int> INT |
... | ... | |
62 | 63 |
%token <string> UIDENT |
63 | 64 |
%token TRUE FALSE |
64 | 65 |
%token <Lustre_types.expr_annot> ANNOT |
65 |
%token <Lustre_types.contract_desc> NODESPEC
|
|
66 |
%token <Lustre_types.spec_types> NODESPEC
|
|
66 | 67 |
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL |
67 | 68 |
%token AMPERAMPER BARBAR NOT POWER |
68 | 69 |
%token IF THEN ELSE |
... | ... | |
113 | 114 |
%type <Lustre_types.expr_annot> lustre_annot |
114 | 115 |
|
115 | 116 |
%start lustre_spec |
116 |
%type <Lustre_types.contract_desc> lustre_spec
|
|
117 |
%type <Lustre_types.spec_types> lustre_spec
|
|
117 | 118 |
|
118 | 119 |
%start signed_const |
119 | 120 |
%type <Lustre_types.constant> signed_const |
... | ... | |
203 | 204 |
|
204 | 205 |
top_decl_header: |
205 | 206 |
| 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 |
|
207 |
| nodespecs state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_list SCOL |
|
208 |
{ |
|
209 |
let inputs = List.rev $5 in |
|
210 |
let outputs = List.rev $10 in |
|
211 |
let nd = mktop_decl true (ImportedNode |
|
208 | 212 |
{nodei_id = $3; |
209 | 213 |
nodei_type = Types.new_var (); |
210 | 214 |
nodei_clock = Clocks.new_var true; |
211 |
nodei_inputs = List.rev $5;
|
|
212 |
nodei_outputs = List.rev $10;
|
|
215 |
nodei_inputs = inputs;
|
|
216 |
nodei_outputs = outputs;
|
|
213 | 217 |
nodei_stateless = $2; |
214 | 218 |
nodei_spec = $1; |
215 | 219 |
nodei_prototype = $13; |
216 | 220 |
nodei_in_lib = $14;}) |
217 | 221 |
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] } |
|
222 |
pop_node (); |
|
223 |
[nd] } |
|
224 |
| top_contract { [$1] } |
|
225 |
|
|
232 | 226 |
|
233 | 227 |
prototype_opt: |
234 | 228 |
{ None } |
... | ... | |
240 | 234 |
|
241 | 235 |
top_decl: |
242 | 236 |
| 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
|
|
237 |
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespecs locals LET stmt_list TEL
|
|
244 | 238 |
{ |
245 | 239 |
let stmts, asserts, annots = $16 in |
246 | 240 |
(* Declaring eqs annots *) |
... | ... | |
249 | 243 |
Annotations.add_node_ann $2 key |
250 | 244 |
) ann.annots |
251 | 245 |
) annots; |
252 |
(* Building the node *) |
|
246 |
(* Building the node *) |
|
247 |
let inputs = List.rev $4 in |
|
248 |
let outputs = List.rev $9 in |
|
253 | 249 |
let nd = mktop_decl false (Node |
254 | 250 |
{node_id = $2; |
255 | 251 |
node_type = Types.new_var (); |
256 | 252 |
node_clock = Clocks.new_var true; |
257 |
node_inputs = List.rev $4;
|
|
258 |
node_outputs = List.rev $9;
|
|
253 |
node_inputs = inputs;
|
|
254 |
node_outputs = outputs;
|
|
259 | 255 |
node_locals = List.rev $14; |
260 | 256 |
node_gencalls = []; |
261 | 257 |
node_checks = []; |
... | ... | |
264 | 260 |
node_dec_stateless = $1; |
265 | 261 |
node_stateless = None; |
266 | 262 |
node_spec = $13; |
267 |
node_annot = annots}) |
|
263 |
node_annot = annots; |
|
264 |
node_iscontract = false; |
|
265 |
}) |
|
268 | 266 |
in |
269 | 267 |
pop_node (); |
270 | 268 |
(*add_node $3 nd;*) [nd] } |
271 | 269 |
|
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] } |
|
270 |
|
|
271 |
| NODESPEC |
|
272 |
{ match $1 with |
|
273 |
| LocalContract c -> assert false |
|
274 |
| TopContract c -> c |
|
275 |
|
|
276 |
} |
|
277 |
|
|
278 |
nodespecs: |
|
279 |
nodespec_list { |
|
280 |
match $1 with |
|
281 |
| None -> None |
|
282 |
| Some c -> Some (Contract c) |
|
283 |
} |
|
300 | 284 |
|
301 | 285 |
nodespec_list: |
302 | 286 |
{ 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 } |
|
287 |
| NODESPEC nodespec_list { |
|
288 |
let extract x = match x with LocalContract c -> c | _ -> assert false in |
|
289 |
let s1 = extract $1 in |
|
290 |
match $2 with |
|
291 |
| None -> Some s1 |
|
292 |
| Some s2 -> Some (merge_contracts s1 s2) } |
|
307 | 293 |
|
308 | 294 |
typ_def_list: |
309 | 295 |
/* empty */ { (fun itf -> []) } |
... | ... | |
382 | 368 |
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)} |
383 | 369 |
|
384 | 370 |
lustre_spec: |
385 |
| contract EOF { $1 } |
|
371 |
| top_contracts EOF { TopContract $1 } |
|
372 |
| contract_content EOF { LocalContract $1} |
|
373 |
|
|
374 |
top_contracts: |
|
375 |
| top_contract { [$1] } |
|
376 |
| top_contract top_contracts { $1::$2 } |
|
377 |
|
|
378 |
top_contract: |
|
379 |
| CONTRACT node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract_content TEL |
|
380 |
{ |
|
381 |
let nd = mktop_decl true (Node |
|
382 |
{node_id = $2; |
|
383 |
node_type = Types.new_var (); |
|
384 |
node_clock = Clocks.new_var true; |
|
385 |
node_inputs = List.rev $4; |
|
386 |
node_outputs = List.rev $9; |
|
387 |
node_locals = []; (* will be filled later *) |
|
388 |
node_gencalls = []; |
|
389 |
node_checks = []; |
|
390 |
node_asserts = []; |
|
391 |
node_stmts = []; (* will be filled later *) |
|
392 |
node_dec_stateless = false; |
|
393 |
(* By default we assume contracts as stateful *) |
|
394 |
node_stateless = None; |
|
395 |
node_spec = Some (Contract $14); |
|
396 |
node_annot = []; |
|
397 |
node_iscontract = true; |
|
398 |
} |
|
399 |
) |
|
400 |
in |
|
401 |
pop_node (); |
|
402 |
(*add_imported_node $3 nd;*) |
|
403 |
nd } |
|
386 | 404 |
|
387 |
contract: |
|
405 |
contract_content:
|
|
388 | 406 |
{ empty_contract } |
389 |
| CONTRACT contract { $2 } |
|
390 |
| CONST IDENT EQ expr SCOL contract |
|
407 |
| CONTRACT contract_content { $2 }
|
|
408 |
| CONST IDENT EQ expr SCOL contract_content
|
|
391 | 409 |
{ merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 } |
392 |
| CONST IDENT COL typeconst EQ expr SCOL contract |
|
410 |
| CONST IDENT COL typeconst EQ expr SCOL contract_content
|
|
393 | 411 |
{ merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 } |
394 |
| VAR IDENT COL typeconst EQ expr SCOL contract |
|
412 |
| VAR IDENT COL typeconst EQ expr SCOL contract_content
|
|
395 | 413 |
{ merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 } |
396 |
| ASSUME qexpr SCOL contract |
|
414 |
| ASSUME qexpr SCOL contract_content
|
|
397 | 415 |
{ merge_contracts (mk_contract_assume $2) $4 } |
398 |
| GUARANTEES qexpr SCOL contract |
|
416 |
| GUARANTEES qexpr SCOL contract_content
|
|
399 | 417 |
{ merge_contracts (mk_contract_guarantees $2) $4 } |
400 |
| MODE IDENT LPAR mode_content RPAR SCOL contract |
|
418 |
| MODE IDENT LPAR mode_content RPAR SCOL contract_content
|
|
401 | 419 |
{ merge_contracts ( |
402 | 420 |
let r, e = $4 in |
403 | 421 |
mk_contract_mode $2 r e (get_loc())) $7 } |
404 |
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract
|
|
422 |
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
|
|
405 | 423 |
{ merge_contracts (mk_contract_import $2 $4 $8 (get_loc())) $11 } |
406 | 424 |
|
407 | 425 |
mode_content: |
Also available in: Unified diff