Revision b4d9710b src/automata.ml
src/automata.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
12 |
open Utils |
|
13 |
open LustreSpec |
|
14 |
open Corelang |
|
15 |
|
|
16 |
let mkbool loc b = |
|
17 |
mkexpr loc (Expr_const (const_of_bool b)) |
|
18 |
|
|
19 |
let mkident loc id = |
|
20 |
mkexpr loc (Expr_ident id) |
|
21 |
|
|
22 |
let mkfby loc e1 e2 = |
|
23 |
mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2))) |
|
24 |
|
|
25 |
let mkidentpair loc restart state = |
|
26 |
mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state]) |
|
27 |
|
|
28 |
let add_branch (loc, expr, restart, st) cont = |
|
29 |
mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont)) |
|
30 |
|
|
31 |
let mkhandler loc st unless until locals (stmts, asserts, annots) = |
|
32 |
{hand_state = st; |
|
33 |
hand_unless = unless; |
|
34 |
hand_until = until; |
|
35 |
hand_locals = locals; |
|
36 |
hand_stmts = stmts; |
|
37 |
hand_asserts = asserts; |
|
38 |
hand_annots = annots; |
|
39 |
hand_loc = loc} |
|
40 |
|
|
41 |
let mkautomata loc id handlers = |
|
42 |
{aut_id = id; |
|
43 |
aut_handlers = handlers; |
|
44 |
aut_loc = loc} |
|
45 |
|
|
46 |
let rec handler_read reads handler = |
|
47 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
|
48 |
let allvars = |
|
49 |
List.fold_left (fun read stmt -> |
|
50 |
match stmt with |
|
51 |
| Eq eq -> get_expr_vars read eq.eq_rhs |
|
52 |
| Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts |
|
53 |
in ISet.diff allvars locals |
|
54 |
|
|
55 |
let rec handler_write writes handler = |
|
56 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
|
57 |
let allvars = |
|
58 |
List.fold_left (fun write stmt -> |
|
59 |
match stmt with |
|
60 |
| Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs |
|
61 |
| Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts |
|
62 |
in ISet.diff allvars locals |
|
63 |
|
|
64 |
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name) |
|
65 |
|
|
66 |
let rec rename_stmts_outputs frename stmts = |
|
67 |
match stmts with |
|
68 |
| [] -> [] |
|
69 |
| (Eq eq) :: q -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in |
|
70 |
eq' :: rename_stmts_outputs frename q |
|
71 |
| (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in |
|
72 |
let aut' = Aut { aut with aut_handlers = handlers' } in |
|
73 |
aut' :: rename_stmts_outputs frename q |
|
74 |
|
|
75 |
let mk_frename used outputs = |
|
76 |
let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in |
|
77 |
(fun name -> try IMap.find name table with Not_found -> name) |
|
78 |
|
|
79 |
let node_of_handler nused used node aut_id handler = |
|
80 |
let outputs = handler_write ISet.empty handler in |
|
81 |
let (new_locals, inputs) = ISet.partition (fun v -> ISet.mem v outputs) (handler_read ISet.empty handler) in |
|
82 |
let frename = mk_frename used outputs in |
|
83 |
let var_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs) in |
|
84 |
let new_var_locals = List.map (fun v -> get_node_var v node) (ISet.elements new_locals) in |
|
85 |
let var_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs) in |
|
86 |
let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in |
|
87 |
let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in |
|
88 |
var_outputs, |
|
89 |
{ |
|
90 |
node_id = mk_new_name nused (Format.sprintf "%s_%s_handler" aut_id handler.hand_state); |
|
91 |
node_type = Types.new_var (); |
|
92 |
node_clock = Clocks.new_var true; |
|
93 |
node_inputs = var_inputs; |
|
94 |
node_outputs = new_var_outputs; |
|
95 |
node_locals = new_var_locals @ handler.hand_locals; |
|
96 |
node_gencalls = []; |
|
97 |
node_checks = []; |
|
98 |
node_asserts = handler.hand_asserts; |
|
99 |
node_stmts = new_output_eqs @ handler.hand_stmts; |
|
100 |
node_dec_stateless = false; |
|
101 |
node_stateless = None; |
|
102 |
node_spec = None; |
|
103 |
node_annot = handler.hand_annots |
|
104 |
} |
|
105 |
|
|
106 |
let expr_of_exit loc restart state conds tag = |
|
107 |
mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag)) |
|
108 |
|
|
109 |
let expr_of_handler loc restart state node tag = |
|
110 |
let args = List.map (fun v -> mkexpr loc (Expr_when (mkident loc v.var_id, state, tag))) node.node_inputs in |
|
111 |
let arg = mkexpr loc (Expr_tuple args) in |
|
112 |
let reset = Some (mkident loc restart) in |
|
113 |
mkexpr loc (Expr_appl (node.node_id, arg, reset)) |
|
114 |
|
|
115 |
let assign_aut_handlers loc actual_r actual_s hnodes = |
|
116 |
let outputs = fst (snd (List.hd hnodes)) in |
|
117 |
let assign_handlers = List.map (fun (hs, (_, n)) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in |
|
118 |
let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in |
|
119 |
let assign_eq = mkeq loc (List.map (fun v -> v.var_id) outputs, assign_expr) in |
|
120 |
assign_eq |
|
121 |
|
|
122 |
let typedef_of_automata aut = |
|
123 |
let tname = Format.sprintf "%s_type" aut.aut_id in |
|
124 |
{ tydef_id = tname; |
|
125 |
tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers) |
|
126 |
} |
|
127 |
(* |
|
128 |
let expand_automata nused used owner typedef node aut = |
|
129 |
let initial = (List.hd aut.aut_handlers).hand_state in |
|
130 |
let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in |
|
131 |
let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in |
|
132 |
let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in |
|
133 |
let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in |
|
134 |
let next_incoming_r = mk_new_name used (aut.aut_id ^ "__next_restart_in") in |
|
135 |
let next_incoming_s = mk_new_name used (aut.aut_id ^ "__next_state_in") in |
|
136 |
(* merge on incoming_s gives actual_s by the unless equations *) |
|
137 |
let actual_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 |
|
138 |
let actual_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in |
|
139 |
let actual_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in |
|
140 |
(* next_incoming_s and initial conditions gives incoming_s *) |
|
141 |
let incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc next_incoming_r next_incoming_s) in |
|
142 |
let incoming_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], incoming_expr) in |
|
143 |
(* merge on actual_s gives handler assigned variables and next_incoming_s by the until equations *) |
|
144 |
let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in |
|
145 |
let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in |
|
146 |
let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in |
|
147 |
let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in |
|
148 |
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in |
|
149 |
let outputs = fst (snd (List.hd hnodes)) in |
|
150 |
let next_incoming_and_assigned_vars = next_incoming_r :: next_incoming_s :: List.map (fun v -> v.var_id) outputs in |
|
151 |
let next_incoming_and_assigned_handlers = |
|
152 |
List.map (fun h -> ) aut.aut_handlers in |
|
153 |
let next_incoming_and_assigned_expr = mkexpr loc (Expr_merge (actual_s, next_incoming_and_assigned_handlers) in |
|
154 |
let next_incoming_and_assigned_eq = mkeq aut.aut_loc (next_incoming_and_assigned_vars, next_incoming_and_assigned_expr) in |
|
155 |
(* declaration of new local variables, equations and handler nodes *) |
|
156 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in |
|
157 |
let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in |
|
158 |
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in |
|
159 |
let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false); |
|
160 |
mkvar_decl aut.aut_loc (actual_r , tydec_bool, ckdec_any, false); |
|
161 |
mkvar_decl aut.aut_loc (next_incoming_r , tydec_bool, ckdec_any, false); |
|
162 |
mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false); |
|
163 |
mkvar_decl aut.aut_loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false); |
|
164 |
mkvar_decl aut.aut_loc (next_incoming_s, tydec_state typedef.tydef_id, ckdec_any, false)] in |
|
165 |
let eqs' = [Eq actual_eq; Eq next_incoming_and_assigned_eq; Eq incoming_eq] in |
|
166 |
(List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes, |
|
167 |
locals', |
|
168 |
eqs') |
|
169 |
*) |
|
170 |
|
|
171 |
let expand_automata nused used owner typedef node aut = |
|
172 |
let initial = (List.hd aut.aut_handlers).hand_state in |
|
173 |
let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in |
|
174 |
let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in |
|
175 |
let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in |
|
176 |
let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in |
|
177 |
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 |
|
178 |
let unless_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in |
|
179 |
let unless_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in |
|
180 |
let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in |
|
181 |
let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in |
|
182 |
let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in |
|
183 |
let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in |
|
184 |
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in |
|
185 |
let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in |
|
186 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in |
|
187 |
let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in |
|
188 |
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in |
|
189 |
let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false); |
|
190 |
mkvar_decl aut.aut_loc (actual_r , tydec_bool, ckdec_any, false); |
|
191 |
mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false); |
|
192 |
mkvar_decl aut.aut_loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false)] in |
|
193 |
let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in |
|
194 |
(List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes, |
|
195 |
locals', |
|
196 |
eqs') |
|
197 |
|
|
198 |
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt = |
|
199 |
match stmt with |
|
200 |
| Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs) |
|
201 |
| Aut aut -> |
|
202 |
let typedef = typedef_of_automata aut in |
|
203 |
let used' name = used name || List.exists (fun v -> v.var_id = name) locals in |
|
204 |
let nused' name = |
|
205 |
nused name || |
|
206 |
List.exists (fun t -> match t.top_decl_desc with |
|
207 |
| ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name |
|
208 |
| _ -> false) top_nodes in |
|
209 |
let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in |
|
210 |
let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in |
|
211 |
(top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs) |
|
212 |
|
|
213 |
let expand_node_stmts nused used loc owner node = |
|
214 |
let (top_types', top_nodes', locals', eqs') = |
|
215 |
List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in |
|
216 |
let node' = |
|
217 |
{ node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in |
|
218 |
let top_node = mktop_decl loc owner false (Node node') in |
|
219 |
top_types', top_node, top_nodes' |
|
220 |
|
|
221 |
let rec expand_decls_rec nused top_decls = |
|
222 |
match top_decls with |
|
223 |
| [] -> [] |
|
224 |
| top_decl::q -> |
|
225 |
match top_decl.top_decl_desc with |
|
226 |
| Node nd -> |
|
227 |
let used name = |
|
228 |
List.exists (fun v -> v.var_id = name) nd.node_inputs |
|
229 |
|| List.exists (fun v -> v.var_id = name) nd.node_outputs |
|
230 |
|| List.exists (fun v -> v.var_id = name) nd.node_locals in |
|
231 |
let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in |
|
232 |
top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q)) |
|
233 |
| _ -> top_decl :: expand_decls_rec nused q |
|
234 |
|
|
235 |
let expand_decls top_decls = |
|
236 |
let top_names = List.fold_left (fun names t -> match t.top_decl_desc with |
|
237 |
| Node nd -> ISet.add nd.node_id names |
|
238 |
| ImportedNode nd -> ISet.add nd.nodei_id names |
|
239 |
| _ -> names) ISet.empty top_decls in |
|
240 |
let nused name = ISet.mem name top_names in |
|
241 |
expand_decls_rec nused top_decls |
|
242 |
|
|
243 |
(* Local Variables: *) |
|
244 |
(* compile-command:"make -C .." *) |
|
245 |
(* End: *) |
|
246 |
|
|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
12 |
open Utils |
|
13 |
open LustreSpec |
|
14 |
open Corelang |
|
15 |
|
|
16 |
|
|
17 |
type aut_state = |
|
18 |
{ |
|
19 |
incoming_r' : var_decl; |
|
20 |
incoming_s' : var_decl; |
|
21 |
incoming_r : var_decl; |
|
22 |
incoming_s : var_decl; |
|
23 |
actual_r : var_decl; |
|
24 |
actual_s : var_decl |
|
25 |
} |
|
26 |
|
|
27 |
let as_clock var_decl = |
|
28 |
let tydec = var_decl.var_dec_type in |
|
29 |
{ var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } } |
|
30 |
|
|
31 |
let mkbool loc b = |
|
32 |
mkexpr loc (Expr_const (const_of_bool b)) |
|
33 |
|
|
34 |
let mkident loc id = |
|
35 |
mkexpr loc (Expr_ident id) |
|
36 |
|
|
37 |
let mkfby loc e1 e2 = |
|
38 |
mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2))) |
|
39 |
|
|
40 |
let mkidentpair loc restart state = |
|
41 |
mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state]) |
|
42 |
|
|
43 |
let add_branch (loc, expr, restart, st) cont = |
|
44 |
mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont)) |
|
45 |
|
|
46 |
let mkhandler loc st unless until locals (stmts, asserts, annots) = |
|
47 |
{hand_state = st; |
|
48 |
hand_unless = unless; |
|
49 |
hand_until = until; |
|
50 |
hand_locals = locals; |
|
51 |
hand_stmts = stmts; |
|
52 |
hand_asserts = asserts; |
|
53 |
hand_annots = annots; |
|
54 |
hand_loc = loc} |
|
55 |
|
|
56 |
let mkautomata loc id handlers = |
|
57 |
{aut_id = id; |
|
58 |
aut_handlers = handlers; |
|
59 |
aut_loc = loc} |
|
60 |
|
|
61 |
let expr_of_exit loc restart state conds tag = |
|
62 |
mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag)) |
|
63 |
|
|
64 |
let rec unless_read reads handler = |
|
65 |
List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_unless |
|
66 |
|
|
67 |
let rec until_read reads handler = |
|
68 |
List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_until |
|
69 |
|
|
70 |
let rec handler_read reads handler = |
|
71 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
|
72 |
let allvars = |
|
73 |
List.fold_left (fun read stmt -> |
|
74 |
match stmt with |
|
75 |
| Eq eq -> get_expr_vars read eq.eq_rhs |
|
76 |
| Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts |
|
77 |
in ISet.diff allvars locals |
|
78 |
|
|
79 |
let rec handler_write writes handler = |
|
80 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
|
81 |
let allvars = |
|
82 |
List.fold_left (fun write stmt -> |
|
83 |
match stmt with |
|
84 |
| Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs |
|
85 |
| Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts |
|
86 |
in ISet.diff allvars locals |
|
87 |
|
|
88 |
let node_vars_of_idents node iset = |
|
89 |
List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) [] |
|
90 |
|
|
91 |
let mkautomata_state used typedef loc id = |
|
92 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in |
|
93 |
let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in |
|
94 |
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in |
|
95 |
let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in |
|
96 |
let incoming_s' = mk_new_name used (id ^ "__next_state_in") in |
|
97 |
let incoming_r = mk_new_name used (id ^ "__restart_in") in |
|
98 |
let incoming_s = mk_new_name used (id ^ "__state_in") in |
|
99 |
let actual_r = mk_new_name used (id ^ "__restart_act") in |
|
100 |
let actual_s = mk_new_name used (id ^ "__state_act") in |
|
101 |
{ |
|
102 |
incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false); |
|
103 |
incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false); |
|
104 |
incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false); |
|
105 |
incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false); |
|
106 |
actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false); |
|
107 |
actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false) |
|
108 |
} |
|
109 |
|
|
110 |
let vars_of_aut_state aut_state = |
|
111 |
[aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s] |
|
112 |
|
|
113 |
let node_of_unless nused used node aut_id aut_state handler = |
|
114 |
let inputs = unless_read ISet.empty handler in |
|
115 |
let var_inputs = aut_state.incoming_r :: aut_state.incoming_s :: (node_vars_of_idents node inputs) in |
|
116 |
let var_outputs = aut_state.actual_r :: aut_state.actual_s :: [] in |
|
117 |
let expr_outputs = List.fold_right add_branch handler.hand_unless (mkidentpair handler.hand_loc aut_state.incoming_r.var_id aut_state.incoming_s.var_id) in |
|
118 |
let eq_outputs = Eq (mkeq handler.hand_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], expr_outputs)) in |
|
119 |
let node_id = mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state) in |
|
120 |
let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.incoming_s.var_id, handler.hand_state))) var_inputs in |
|
121 |
let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in |
|
122 |
{ |
|
123 |
node_id = node_id; |
|
124 |
node_type = Types.new_var (); |
|
125 |
node_clock = Clocks.new_var true; |
|
126 |
node_inputs = var_inputs; |
|
127 |
node_outputs = var_outputs; |
|
128 |
node_locals = []; |
|
129 |
node_gencalls = []; |
|
130 |
node_checks = []; |
|
131 |
node_asserts = []; |
|
132 |
node_stmts = [ eq_outputs ]; |
|
133 |
node_dec_stateless = false; |
|
134 |
node_stateless = None; |
|
135 |
node_spec = None; |
|
136 |
node_annot = [] |
|
137 |
}, |
|
138 |
mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) |
|
139 |
|
|
140 |
|
|
141 |
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name) |
|
142 |
|
|
143 |
let rec rename_stmts_outputs frename stmts = |
|
144 |
match stmts with |
|
145 |
| [] -> [] |
|
146 |
| (Eq eq) :: q -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in |
|
147 |
eq' :: rename_stmts_outputs frename q |
|
148 |
| (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in |
|
149 |
let aut' = Aut { aut with aut_handlers = handlers' } in |
|
150 |
aut' :: rename_stmts_outputs frename q |
|
151 |
|
|
152 |
let mk_frename used outputs = |
|
153 |
let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in |
|
154 |
(fun name -> try IMap.find name table with Not_found -> name) |
|
155 |
|
|
156 |
let node_of_assign_until nused used node aut_id aut_state handler = |
|
157 |
let writes = handler_write ISet.empty handler in |
|
158 |
let inputs = ISet.diff (handler_read (until_read ISet.empty handler) handler) writes in |
|
159 |
let frename = mk_frename used writes in |
|
160 |
let var_inputs = node_vars_of_idents node inputs in |
|
161 |
let new_var_locals = node_vars_of_idents node writes in |
|
162 |
let var_outputs = node_vars_of_idents node writes in |
|
163 |
let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in |
|
164 |
let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in |
|
165 |
let until_expr = List.fold_right add_branch handler.hand_until (mkidentpair handler.hand_loc aut_state.actual_r.var_id aut_state.actual_s.var_id) in |
|
166 |
let until_eq = Eq (mkeq handler.hand_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], until_expr)) in |
|
167 |
let node_id = mk_new_name nused (Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state) in |
|
168 |
let var_inputs = aut_state.actual_r :: aut_state.actual_s :: var_inputs in |
|
169 |
let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.actual_s.var_id, handler.hand_state))) var_inputs in |
|
170 |
let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in |
|
171 |
List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs, |
|
172 |
{ |
|
173 |
node_id = node_id; |
|
174 |
node_type = Types.new_var (); |
|
175 |
node_clock = Clocks.new_var true; |
|
176 |
node_inputs = var_inputs; |
|
177 |
node_outputs = aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs; |
|
178 |
node_locals = new_var_locals @ handler.hand_locals; |
|
179 |
node_gencalls = []; |
|
180 |
node_checks = []; |
|
181 |
node_asserts = handler.hand_asserts; |
|
182 |
node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts; |
|
183 |
node_dec_stateless = false; |
|
184 |
node_stateless = None; |
|
185 |
node_spec = None; |
|
186 |
node_annot = handler.hand_annots |
|
187 |
}, |
|
188 |
mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) |
|
189 |
|
|
190 |
let typedef_of_automata aut = |
|
191 |
let tname = Format.sprintf "%s__type" aut.aut_id in |
|
192 |
{ tydef_id = tname; |
|
193 |
tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers) |
|
194 |
} |
|
195 |
|
|
196 |
let expand_automata nused used owner typedef node aut = |
|
197 |
let initial = (List.hd aut.aut_handlers).hand_state in |
|
198 |
let aut_state = mkautomata_state used typedef aut.aut_loc aut.aut_id in |
|
199 |
let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in |
|
200 |
let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in |
|
201 |
let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in |
|
202 |
let unless_handlers = List.map2 (fun h (n, c) -> (h.hand_state, c)) aut.aut_handlers unodes in |
|
203 |
let unless_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.incoming_s.var_id, unless_handlers)) in |
|
204 |
let unless_eq = mkeq aut.aut_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], unless_expr) in |
|
205 |
let assign_until_handlers = List.map2 (fun h (_, n, c) -> (h.hand_state, c)) aut.aut_handlers aunodes in |
|
206 |
let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in |
|
207 |
let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in |
|
208 |
let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in |
|
209 |
let fby_incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in |
|
210 |
let incoming_eq = mkeq aut.aut_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], fby_incoming_expr) in |
|
211 |
let locals' = vars_of_aut_state aut_state in |
|
212 |
let eqs' = [Eq unless_eq; Eq assign_until_eq; Eq incoming_eq] in |
|
213 |
( List.map2 (fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers unodes |
|
214 |
@ List.map2 (fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers aunodes, |
|
215 |
locals', |
|
216 |
eqs') |
|
217 |
|
|
218 |
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt = |
|
219 |
match stmt with |
|
220 |
| Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs) |
|
221 |
| Aut aut -> |
|
222 |
let typedef = typedef_of_automata aut in |
|
223 |
let used' name = used name || List.exists (fun v -> v.var_id = name) locals in |
|
224 |
let nused' name = |
|
225 |
nused name || |
|
226 |
List.exists (fun t -> match t.top_decl_desc with |
|
227 |
| ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name |
|
228 |
| _ -> false) top_nodes in |
|
229 |
let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in |
|
230 |
let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in |
|
231 |
(top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs) |
|
232 |
|
|
233 |
let expand_node_stmts nused used loc owner node = |
|
234 |
let (top_types', top_nodes', locals', eqs') = |
|
235 |
List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in |
|
236 |
let node' = |
|
237 |
{ node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in |
|
238 |
let top_node = mktop_decl loc owner false (Node node') in |
|
239 |
top_types', top_node, top_nodes' |
|
240 |
|
|
241 |
let rec expand_decls_rec nused top_decls = |
|
242 |
match top_decls with |
|
243 |
| [] -> [] |
|
244 |
| top_decl::q -> |
|
245 |
match top_decl.top_decl_desc with |
|
246 |
| Node nd -> |
|
247 |
let used name = |
|
248 |
List.exists (fun v -> v.var_id = name) nd.node_inputs |
|
249 |
|| List.exists (fun v -> v.var_id = name) nd.node_outputs |
|
250 |
|| List.exists (fun v -> v.var_id = name) nd.node_locals in |
|
251 |
let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in |
|
252 |
top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q)) |
|
253 |
| _ -> top_decl :: expand_decls_rec nused q |
|
254 |
|
|
255 |
let expand_decls top_decls = |
|
256 |
let top_names = List.fold_left (fun names t -> match t.top_decl_desc with |
|
257 |
| Node nd -> ISet.add nd.node_id names |
|
258 |
| ImportedNode nd -> ISet.add nd.nodei_id names |
|
259 |
| _ -> names) ISet.empty top_decls in |
|
260 |
let nused name = ISet.mem name top_names in |
|
261 |
expand_decls_rec nused top_decls |
|
262 |
|
|
263 |
(* Local Variables: *) |
|
264 |
(* compile-command:"make -C .." *) |
|
265 |
(* End: *) |
|
266 |
|
Also available in: Unified diff