Revision c02d255e
Added by Pierre-Loïc Garoche almost 9 years ago
| src/lustreSpec.ml | ||
|---|---|---|
| 68 | 68 |
| EExpr_tuple of eexpr list |
| 69 | 69 |
| EExpr_arrow of eexpr * eexpr |
| 70 | 70 |
| EExpr_fby of eexpr * eexpr |
| 71 |
| EExpr_concat of eexpr * eexpr
|
|
| 72 |
| EExpr_tail of eexpr
|
|
| 71 |
(* | EExpr_concat of eexpr * eexpr *)
|
|
| 72 |
(* | EExpr_tail of eexpr *)
|
|
| 73 | 73 |
| EExpr_pre of eexpr |
| 74 | 74 |
| EExpr_when of eexpr * ident |
| 75 |
| EExpr_whennot of eexpr * ident
|
|
| 75 |
(* | EExpr_whennot of eexpr * ident *)
|
|
| 76 | 76 |
| EExpr_merge of ident * eexpr * eexpr |
| 77 | 77 |
| EExpr_appl of ident * eexpr * ident option |
| 78 |
| EExpr_uclock of eexpr * int
|
|
| 79 |
| EExpr_dclock of eexpr * int
|
|
| 80 |
| EExpr_phclock of eexpr * rat
|
|
| 78 |
(* | EExpr_uclock of eexpr * int *)
|
|
| 79 |
(* | EExpr_dclock of eexpr * int *)
|
|
| 80 |
(* | EExpr_phclock of eexpr * rat *)
|
|
| 81 | 81 |
| EExpr_exists of var_decl list * eexpr |
| 82 | 82 |
| EExpr_forall of var_decl list * eexpr |
| 83 | 83 |
|
Also available in: Unified diff
Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process