Revision 5538b7ac
Added by Xavier Thirioux about 11 years ago
| src/corelang.ml | ||
|---|---|---|
| 104 | 104 |
mutable node_checks: Dimension.dim_expr list; |
| 105 | 105 |
node_asserts: assert_t list; |
| 106 | 106 |
node_eqs: eq list; |
| 107 |
node_dec_stateless: bool; |
|
| 107 |
mutable node_dec_stateless: bool;
|
|
| 108 | 108 |
mutable node_stateless: bool option; |
| 109 | 109 |
node_spec: LustreSpec.node_annot option; |
| 110 | 110 |
node_annot: LustreSpec.expr_annot option; |
| ... | ... | |
| 145 | 145 |
| No_main_specified |
| 146 | 146 |
| Unbound_symbol of ident |
| 147 | 147 |
| Already_bound_symbol of ident |
| 148 |
| Stateful of ident |
|
| 149 | 148 |
|
| 150 | 149 |
exception Error of Location.t * error |
| 151 | 150 |
|
| ... | ... | |
| 262 | 261 |
| ImportedNode nd -> true |
| 263 | 262 |
| _ -> assert false |
| 264 | 263 |
|
| 265 |
let rec is_stateless_expr expr = |
|
| 266 |
match expr.expr_desc with |
|
| 267 |
| Expr_const _ |
|
| 268 |
| Expr_ident _ -> true |
|
| 269 |
| Expr_tuple el |
|
| 270 |
| Expr_array el -> List.for_all is_stateless_expr el |
|
| 271 |
| Expr_access (e1, _) |
|
| 272 |
| Expr_power (e1, _) -> is_stateless_expr e1 |
|
| 273 |
| Expr_ite (c, t, e) -> is_stateless_expr c && is_stateless_expr t && is_stateless_expr e |
|
| 274 |
| Expr_arrow (e1, e2) |
|
| 275 |
| Expr_fby (e1, e2) -> is_stateless_expr e1 && is_stateless_expr e2 |
|
| 276 |
| Expr_pre e' -> is_stateless_expr e' |
|
| 277 |
| Expr_when (e', i, l)-> is_stateless_expr e' |
|
| 278 |
| Expr_merge (i, hl) -> List.for_all (fun (t, h) -> is_stateless_expr h) hl |
|
| 279 |
| Expr_appl (i, e', i') -> |
|
| 280 |
is_stateless_expr e' && |
|
| 281 |
(Basic_library.is_internal_fun i || check_stateless_node (node_from_name i)) |
|
| 282 |
| Expr_uclock _ |
|
| 283 |
| Expr_dclock _ |
|
| 284 |
| Expr_phclock _ -> assert false |
|
| 285 |
and compute_stateless_node nd = |
|
| 286 |
List.for_all (fun eq -> is_stateless_expr eq.eq_rhs) nd.node_eqs |
|
| 287 |
and check_stateless_node td = |
|
| 288 |
match td.top_decl_desc with |
|
| 289 |
| Node nd -> ( |
|
| 290 |
match nd.node_stateless with |
|
| 291 |
| None -> |
|
| 292 |
begin |
|
| 293 |
let stateless = compute_stateless_node nd in |
|
| 294 |
nd.node_stateless <- Some (false && stateless); |
|
| 295 |
if nd.node_dec_stateless && (not stateless) |
|
| 296 |
then raise (Error (td.top_decl_loc, Stateful nd.node_id)) |
|
| 297 |
else stateless |
|
| 298 |
end |
|
| 299 |
| Some stl -> stl) |
|
| 300 |
| ImportedNode nd -> nd.nodei_stateless |
|
| 301 |
| _ -> true |
|
| 302 | 264 |
|
| 303 | 265 |
(* alias and type definition table *) |
| 304 | 266 |
let type_table = |
| ... | ... | |
| 766 | 728 |
fprintf fmt |
| 767 | 729 |
"%s is already defined.@." |
| 768 | 730 |
sym |
| 769 |
| Stateful nd -> |
|
| 770 |
fprintf fmt |
|
| 771 |
"node %s is declared stateless, but it is stateful.@." |
|
| 772 |
nd |
|
| 773 | 731 |
|
| 774 | 732 |
(* filling node table with internal functions *) |
| 775 | 733 |
let vdecls_of_typ_ck cpt ty = |
Also available in: Unified diff
Added declaration/definition of stateless/stateful nodes.
The 'function' keyword is for stateless nodes only,
the 'node' keyword is any kind of node.
Improves compilation and paves the way for more optimizations.