Revision 0697ff5b
Added by Pierre-Loïc Garoche about 5 years ago
| src/parsers/parser_lustre.mly | ||
|---|---|---|
| 144 | 144 |
| DIV path_ident { "/" ^ $2 }
|
| 145 | 145 |
| file_ident { $1 }
|
| 146 | 146 |
|
| 147 |
tag_bool: |
|
| 148 |
| TRUE { tag_true }
|
|
| 149 |
| FALSE { tag_false }
|
|
| 150 |
|
|
| 147 | 151 |
tag_ident: |
| 148 | 152 |
UIDENT { $1 }
|
| 149 |
| TRUE { tag_true }
|
|
| 150 |
| FALSE { tag_false }
|
|
| 153 |
| tag_bool { $1 }
|
|
| 151 | 154 |
|
| 152 | 155 |
node_ident: |
| 153 | 156 |
UIDENT { $1 }
|
| ... | ... | |
| 474 | 477 |
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
|
| 475 | 478 |
/* Idents or type enum tags */ |
| 476 | 479 |
| IDENT { mkexpr (Expr_ident $1) }
|
| 477 |
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
|
|
| 480 |
| UIDENT { mkexpr (Expr_ident $1) (* TODO we will differenciate enum constants from variables later *) }
|
|
| 481 |
| tag_bool {
|
|
| 482 |
(* on sept 2014, X chenged the Const to |
|
| 483 |
mkexpr (Expr_ident $1) |
|
| 484 |
reverted back to const on july 2019 *) |
|
| 485 |
mkexpr (Expr_const (Const_tag $1)) } |
|
| 478 | 486 |
| LPAR ANNOT expr RPAR |
| 479 | 487 |
{update_expr_annot (get_current_node ()) $3 $2}
|
| 480 | 488 |
| LPAR expr RPAR |
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 785 | 785 |
in |
| 786 | 786 |
(* Special cases to avoid useless computations: true, false conditions *) |
| 787 | 787 |
match elem.expr_desc with |
| 788 |
| Expr_ident "true" -> build_switch_sys pos prefix
|
|
| 788 |
(*| Expr_ident "true" -> build_switch_sys pos prefix *)
|
|
| 789 | 789 |
| Expr_const (Const_tag tag) when tag = Corelang.tag_true |
| 790 | 790 |
-> build_switch_sys pos prefix |
| 791 |
| Expr_ident "false" -> build_switch_sys neg prefix
|
|
| 791 |
(*| Expr_ident "false" -> build_switch_sys neg prefix *)
|
|
| 792 | 792 |
| Expr_const (Const_tag tag) when tag = Corelang.tag_false |
| 793 | 793 |
-> build_switch_sys neg prefix |
| 794 | 794 |
| _ -> (* Regular case *) |
Also available in: Unified diff
Produce true/false statements as constants