Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/parsers/parser_lustre.mly | ||
---|---|---|
81 | 81 |
%token INVARIANT MODE CCODE MATLAB |
82 | 82 |
%token EXISTS FORALL |
83 | 83 |
%token PROTOTYPE LIB |
84 |
%token BY |
|
85 |
%token <int> KINDUCTION |
|
84 | 86 |
%token EOF |
85 | 87 |
|
86 | 88 |
%nonassoc p_string |
... | ... | |
370 | 372 |
nd |
371 | 373 |
} |
372 | 374 |
|
375 |
proof_annotation: |
|
376 |
| BY k=KINDUCTION { Kinduction k } |
|
377 |
|
|
373 | 378 |
contract_content: |
374 | 379 |
| { empty_contract } |
375 | 380 |
/* | CONTRACT cc=contract_content */ |
... | ... | |
380 | 385 |
{ merge_contracts (mk_contract_var x false (Some (mktyp $sloc t)) e $sloc) cc } |
381 | 386 |
| ASSUME x=ioption(STRING) e=qexpr SCOL cc=contract_content |
382 | 387 |
{ merge_contracts (mk_contract_assume x e) cc } |
383 |
| GUARANTEES x=ioption(STRING) e=qexpr SCOL cc=contract_content |
|
384 |
{ merge_contracts (mk_contract_guarantees x e) cc } |
|
388 |
| GUARANTEES x=ioption(STRING) e=qexpr p=proof_annotation? SCOL cc=contract_content
|
|
389 |
{ merge_contracts (mk_contract_guarantees x e p) cc }
|
|
385 | 390 |
| MODE x=IDENT LPAR mc=mode_content RPAR SCOL cc=contract_content |
386 | 391 |
{ merge_contracts ( |
387 | 392 |
let r, e = mc in |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example