61 |
61 |
| Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
|
62 |
62 |
in ISet.diff allvars locals
|
63 |
63 |
|
64 |
|
let node_of_handler node aut_id handler =
|
|
64 |
let node_of_handler nused node aut_id handler =
|
65 |
65 |
let inputs = handler_read ISet.empty handler in
|
66 |
66 |
let outputs = handler_write ISet.empty handler in
|
67 |
67 |
{
|
68 |
|
node_id = Format.sprintf "%s_%s_handler" aut_id handler.hand_state;
|
|
68 |
node_id = mk_new_name nused (Format.sprintf "%s_%s_handler" aut_id handler.hand_state);
|
69 |
69 |
node_type = Types.new_var ();
|
70 |
70 |
node_clock = Clocks.new_var true;
|
71 |
71 |
node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs);
|
... | ... | |
95 |
95 |
let assign_eq = mkeq loc (List.map (fun v -> v.var_id) outputs, assign_expr) in
|
96 |
96 |
assign_eq
|
97 |
97 |
|
98 |
|
let typedef_of_automata node aut =
|
|
98 |
let typedef_of_automata aut =
|
99 |
99 |
let tname = Format.sprintf "%s_type" aut.aut_id in
|
100 |
100 |
{ tydef_id = tname;
|
101 |
101 |
tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
|
102 |
102 |
}
|
103 |
|
(*
|
104 |
|
let expand_automata_stmt (top_decls, locals, eqs) stmt =
|
105 |
|
match stmt with
|
106 |
|
| Eq eq -> (top_decls, locals, eq::eqs)
|
107 |
|
| Aut aut ->
|
108 |
103 |
|
109 |
|
|
110 |
|
let expand_automata top_node aut =
|
111 |
|
let node = node_of_top top_node in
|
112 |
|
let owner = top_node.top_decl_owner in
|
113 |
|
let typedef = typedef_of_automata node aut in
|
|
104 |
let expand_automata nused used owner typedef node aut =
|
114 |
105 |
let initial = (List.hd aut.aut_handlers).hand_state in
|
115 |
|
let incoming_r = mk_new_name (get_node_vars node) (aut.aut_id ^ "__restart_in") in
|
116 |
|
let incoming_s = mk_new_name (get_node_vars node) (aut.aut_id ^ "__state_in") in
|
117 |
|
let actual_r = mk_new_name (get_node_vars node) (aut.aut_id ^ "__restart_act") in
|
118 |
|
let actual_s = mk_new_name (get_node_vars node) (aut.aut_id ^ "__state_act") in
|
|
106 |
let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in
|
|
107 |
let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in
|
|
108 |
let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in
|
|
109 |
let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in
|
119 |
110 |
let unless_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc incoming_r incoming_s h.hand_unless h.hand_state)) aut.aut_handlers in
|
120 |
111 |
let unless_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in
|
121 |
112 |
let unless_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in
|
... | ... | |
123 |
114 |
let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in
|
124 |
115 |
let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in
|
125 |
116 |
let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
|
126 |
|
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler node aut.aut_id h)) aut.aut_handlers in
|
|
117 |
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused node aut.aut_id h)) aut.aut_handlers in
|
127 |
118 |
let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in
|
128 |
119 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
|
129 |
120 |
let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in
|
... | ... | |
133 |
124 |
mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);
|
134 |
125 |
mkvar_decl aut.aut_loc (actual_s , tydec_const typedef.tydef_id, ckdec_any, false)] in
|
135 |
126 |
let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in
|
136 |
|
let node' = { node with node_locals = locals'@node.node_locals; node_stmts = eqs'@node.node_stmts } in
|
137 |
|
(mktop_decl aut.aut_loc owner false (TypeDef typedef)) ::
|
138 |
|
{ top_node with top_decl_desc = Node node' } ::
|
139 |
|
(List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes)
|
140 |
|
*)
|
141 |
|
let rec node_extract_automata top_decl =
|
142 |
|
match top_decl.top_decl_desc with
|
143 |
|
| Node nd -> []
|
144 |
|
| _ -> [top_decl]
|
145 |
|
(*
|
146 |
|
let extract_automata top_decls =
|
147 |
|
List.fold_left (fun top_decls top_decl -> ) top_decls
|
148 |
|
*)
|
|
127 |
(List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
|
|
128 |
locals',
|
|
129 |
eqs')
|
|
130 |
|
|
131 |
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt =
|
|
132 |
match stmt with
|
|
133 |
| Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs)
|
|
134 |
| Aut aut ->
|
|
135 |
let typedef = typedef_of_automata aut in
|
|
136 |
let used' name = used name || List.exists (fun v -> v.var_id = name) locals in
|
|
137 |
let nused' name =
|
|
138 |
nused name ||
|
|
139 |
List.exists (fun t -> match t.top_decl_desc with
|
|
140 |
| ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name
|
|
141 |
| _ -> false) top_nodes in
|
|
142 |
let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in
|
|
143 |
let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
|
|
144 |
(top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs)
|
|
145 |
|
|
146 |
let expand_node_stmts nused used loc owner node =
|
|
147 |
let (top_types', top_nodes', locals', eqs') =
|
|
148 |
List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in
|
|
149 |
let node' =
|
|
150 |
{ node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in
|
|
151 |
let top_node = mktop_decl loc owner false (Node node') in
|
|
152 |
top_types', top_node, top_nodes'
|
|
153 |
|
|
154 |
let rec expand_decls_rec nused top_decls =
|
|
155 |
match top_decls with
|
|
156 |
| [] -> []
|
|
157 |
| top_decl::q ->
|
|
158 |
match top_decl.top_decl_desc with
|
|
159 |
| Node nd ->
|
|
160 |
let used name =
|
|
161 |
List.exists (fun v -> v.var_id = name) nd.node_inputs
|
|
162 |
|| List.exists (fun v -> v.var_id = name) nd.node_outputs
|
|
163 |
|| List.exists (fun v -> v.var_id = name) nd.node_locals in
|
|
164 |
let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
|
|
165 |
top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q))
|
|
166 |
| _ -> top_decl :: expand_decls_rec nused q
|
|
167 |
|
|
168 |
let expand_decls top_decls =
|
|
169 |
let top_names = List.fold_left (fun names t -> match t.top_decl_desc with
|
|
170 |
| Node nd -> ISet.add nd.node_id names
|
|
171 |
| ImportedNode nd -> ISet.add nd.nodei_id names
|
|
172 |
| _ -> names) ISet.empty top_decls in
|
|
173 |
let nused name = ISet.mem name top_names in
|
|
174 |
expand_decls_rec nused top_decls
|
|
175 |
|
149 |
176 |
(* Local Variables: *)
|
150 |
177 |
(* compile-command:"make -C .." *)
|
151 |
178 |
(* End: *)
|
|
179 |
|