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