Revision d3e4c22f src/corelang.ml
| 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; |
|
| 108 |
mutable node_stateless: bool option; |
|
| 107 | 109 |
node_spec: LustreSpec.node_annot option; |
| 108 | 110 |
node_annot: LustreSpec.expr_annot option; |
| 109 | 111 |
} |
| ... | ... | |
| 118 | 120 |
nodei_spec: LustreSpec.node_annot option; |
| 119 | 121 |
} |
| 120 | 122 |
|
| 121 |
type imported_fun_desc = |
|
| 122 |
{fun_id: ident;
|
|
| 123 |
mutable fun_type: Types.type_expr; |
|
| 124 |
fun_inputs: var_decl list; |
|
| 125 |
fun_outputs: var_decl list; |
|
| 126 |
fun_spec: LustreSpec.node_annot option;} |
|
| 127 |
|
|
| 128 | 123 |
type const_desc = |
| 129 | 124 |
{const_id: ident;
|
| 130 | 125 |
const_loc: Location.t; |
| ... | ... | |
| 136 | 131 |
| Node of node_desc |
| 137 | 132 |
| Consts of const_desc list |
| 138 | 133 |
| ImportedNode of imported_node_desc |
| 139 |
| ImportedFun of imported_fun_desc |
|
| 140 | 134 |
| Open of string |
| 141 | 135 |
|
| 142 | 136 |
type top_decl = |
| ... | ... | |
| 151 | 145 |
| No_main_specified |
| 152 | 146 |
| Unbound_symbol of ident |
| 153 | 147 |
| Already_bound_symbol of ident |
| 148 |
| Stateful of ident |
|
| 154 | 149 |
|
| 155 |
exception Error of error * Location.t
|
|
| 150 |
exception Error of Location.t * error
|
|
| 156 | 151 |
|
| 157 | 152 |
module VDeclModule = |
| 158 | 153 |
struct (* Node module *) |
| ... | ... | |
| 267 | 262 |
| ImportedNode nd -> true |
| 268 | 263 |
| _ -> assert false |
| 269 | 264 |
|
| 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 |
|
|
| 270 | 303 |
(* alias and type definition table *) |
| 271 | 304 |
let type_table = |
| 272 | 305 |
Utils.create_hashtable 20 [ |
| ... | ... | |
| 505 | 538 |
fun consts decl -> |
| 506 | 539 |
match decl.top_decl_desc with |
| 507 | 540 |
| Consts clist -> clist@consts |
| 508 |
| Node _ | ImportedNode _ | ImportedFun _ | Open _ -> consts
|
|
| 541 |
| Node _ | ImportedNode _ | Open _ -> consts |
|
| 509 | 542 |
) [] prog |
| 510 | 543 |
|
| 511 | 544 |
|
| ... | ... | |
| 514 | 547 |
fun nodes decl -> |
| 515 | 548 |
match decl.top_decl_desc with |
| 516 | 549 |
| Node nd -> nd::nodes |
| 517 |
| Consts _ | ImportedNode _ | ImportedFun _ | Open _ -> nodes
|
|
| 550 |
| Consts _ | ImportedNode _ | Open _ -> nodes |
|
| 518 | 551 |
) [] prog |
| 519 | 552 |
|
| 520 | 553 |
let prog_unfold_consts prog = |
| ... | ... | |
| 658 | 691 |
node_checks = node_checks; |
| 659 | 692 |
node_asserts = node_asserts; |
| 660 | 693 |
node_eqs = eqs; |
| 694 |
node_dec_stateless = nd.node_dec_stateless; |
|
| 695 |
node_stateless = nd.node_stateless; |
|
| 661 | 696 |
node_spec = spec; |
| 662 | 697 |
node_annot = annot; |
| 663 | 698 |
} |
| ... | ... | |
| 675 | 710 |
| Consts c -> |
| 676 | 711 |
{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
|
| 677 | 712 |
| ImportedNode _ |
| 678 |
| ImportedFun _ |
|
| 679 | 713 |
| Open _ -> top) |
| 680 | 714 |
::accu |
| 681 | 715 |
) [] prog |
| ... | ... | |
| 694 | 728 |
fprintf fmt "%s: " ind.nodei_id; |
| 695 | 729 |
Utils.reset_names (); |
| 696 | 730 |
fprintf fmt "%a@ " Types.print_ty ind.nodei_type |
| 697 |
| ImportedFun ind -> |
|
| 698 |
fprintf fmt "%s: " ind.fun_id; |
|
| 699 |
Utils.reset_names (); |
|
| 700 |
fprintf fmt "%a@ " Types.print_ty ind.fun_type |
|
| 701 | 731 |
| Consts _ | Open _ -> () |
| 702 | 732 |
|
| 703 | 733 |
let pp_prog_type fmt tdecl_list = |
| ... | ... | |
| 713 | 743 |
fprintf fmt "%s: " ind.nodei_id; |
| 714 | 744 |
Utils.reset_names (); |
| 715 | 745 |
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock |
| 716 |
| ImportedFun _ | Consts _ | Open _ -> ()
|
|
| 746 |
| Consts _ | Open _ -> () |
|
| 717 | 747 |
|
| 718 | 748 |
let pp_prog_clock fmt prog = |
| 719 | 749 |
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog |
| ... | ... | |
| 736 | 766 |
fprintf fmt |
| 737 | 767 |
"%s is already defined.@." |
| 738 | 768 |
sym |
| 769 |
| Stateful nd -> |
|
| 770 |
fprintf fmt |
|
| 771 |
"node %s is declared stateless, but it is stateful.@." |
|
| 772 |
nd |
|
| 739 | 773 |
|
| 740 | 774 |
(* filling node table with internal functions *) |
| 741 | 775 |
let vdecls_of_typ_ck cpt ty = |
Also available in: Unified diff