Revision 333e3a25
Added by PierreLoïc Garoche over 5 years ago
src/inliner.ml  

32  32 
ignore (Corelang.get_node_var v node); true 
33  33 
with Not_found > false 
34  34  
35 
let rename_expr rename expr = expr_replace_var rename expr


36  
35 
(* let rename_expr rename expr = expr_replace_var rename expr *)


36 
(* 

37  37 
let rename_eq rename eq = 
38  38 
{ eq with 
39  39 
eq_lhs = List.map rename eq.eq_lhs; 
40  40 
eq_rhs = rename_expr rename eq.eq_rhs 
41  41 
} 
42  
42 
*) 

43 


43  44 
let rec add_expr_reset_cond cond expr = 
44  45 
let aux = add_expr_reset_cond cond in 
45  46 
let new_desc = 
...  ...  
113  114 
if v = tag_true  v = tag_false  not (is_node_var node v) then v else 
114  115 
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) 
115  116 
in 
116 
let eqs' = List.map (rename_eq rename) (get_node_eqs node) in 

117 
let eqs, auts = get_node_eqs node in 

118 
let eqs' = List.map (rename_eq (fun x > x) rename) eqs in 

119 
let auts' = List.map (rename_aut (fun x > x) rename) auts in 

117  120 
let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in 
118  121 
let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) > vdecl.var_dec_const) input_arg_list in 
119  122 
let static_inputs = List.map (fun (vdecl, arg) > vdecl, Corelang.dimension_of_expr arg) static_inputs in 
...  ...  
134  137 
{ v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc }, 
135  138 
{ v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc }, 
136  139 
v.var_dec_const, 
137 
Utils.option_map (rename_expr rename) v.var_dec_value) in 

140 
Utils.option_map (rename_expr (fun x > x) rename) v.var_dec_value) in


138  141 
begin 
139  142 
(* 
140  143 
(try 
...  ...  
162  165 
assert (node.node_gencalls = []); 
163  166  
164  167 
(* Expressing reset locally in equations *) 
165 
let eqs_r' = 

168 
let eqs_r' = 

169 
let all_eqs = (List.map (fun eq > Eq eq) eqs') @ (List.map (fun aut > Aut aut) auts') in 

166  170 
match reset with 
167 
None > eqs' 

168 
 Some cond > List.map (add_eq_reset_cond cond) eqs' 

171 
None > all_eqs 

172 
 Some cond > ( 

173 
assert (auts' = []); (* TODO: we do not handle properly automaton in case of reset call *) 

174 
List.map (fun eq > Eq (add_eq_reset_cond cond eq)) eqs' 

175 
) 

169  176 
in 
170 
let assign_inputs = mkeq loc (List.map (fun v > v.var_id) inputs', 

171 
expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in 

177 
let assign_inputs = Eq (mkeq loc (List.map (fun v > v.var_id) inputs',


178 
expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs))) in


172  179 
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') 
173  180 
in 
174  181 
let asserts' = (* We rename variables in assert expressions *) 
...  ...  
176  183 
(fun a > 
177  184 
{a with assert_expr = 
178  185 
let expr = a.assert_expr in 
179 
rename_expr rename expr 

186 
rename_expr (fun x > x) rename expr


180  187 
}) 
181  188 
node.node_asserts 
182  189 
in 
...  ...  
224  231 

225  232 
match expr.expr_desc with 
226  233 
 Expr_appl (id, args, reset) > 
227 
let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 

228 
if List.exists (check_node_name id) nodes && (* the current node call is provided 

229 
as arguments nodes *) 

230 
(not selection_on_annotation  is_inline_expr expr) (* and if selection on annotation is activated, 

231 
it is explicitely inlined here *) 

232 
then ( 

233 
(* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *) 

234 
(* The node should be inlined *) 

235 
(* let _ = Format.eprintf "Inlining call to %s@." id in *) 

236 
let called = try List.find (check_node_name id) nodes 

237 
with Not_found > (assert false) in 

238 
let called = node_of_top called in 

239 
let called' = inline_node called nodes in 

240 
let expr, locals', eqs'', asserts'', annots'' = 

241 
inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in 

242 
expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots'' 

243 
) 

244 
else 

245 
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) 

246 
{ expr with expr_desc = Expr_appl(id, args', reset)}, 

247 
locals', 

248 
eqs', 

249 
asserts', 

250 
annots' 

234 
let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in


235 
if List.exists (check_node_name id) nodes && (* the current node call is provided


236 
as arguments nodes *)


237 
(not selection_on_annotation  is_inline_expr expr) (* and if selection on annotation is activated,


238 
it is explicitely inlined here *)


239 
then (


240 
(* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)


241 
(* The node should be inlined *)


242 
(* let _ = Format.eprintf "Inlining call to %s@." id in *)


243 
let called = try List.find (check_node_name id) nodes


244 
with Not_found > (assert false) in


245 
let called = node_of_top called in


246 
let called' = inline_node called nodes in


247 
let expr, locals', eqs'', asserts'', annots'' =


248 
inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in


249 
expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''


250 
)


251 
else


252 
(* let _ = Format.eprintf "Not inlining call to %s@." id in *)


253 
{ expr with expr_desc = Expr_appl(id, args', reset)},


254 
locals',


255 
eqs',


256 
asserts',


257 
annots'


251  258  
252  259 
(* For other cases, we just keep the structure, but convert subexpressions *) 
253  260 
 Expr_const _ 
254  261 
 Expr_ident _ > expr, locals, [], [], [] 
255  262 
 Expr_tuple el > 
256 
let el', l', eqs', asserts', annots' = inline_tuple el in 

257 
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots' 

263 
let el', l', eqs', asserts', annots' = inline_tuple el in


264 
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'


258  265 
 Expr_ite (g, t, e) > 
259 
let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in 

260 
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots' 

266 
let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in


267 
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'


261  268 
 Expr_arrow (e1, e2) > 
262 
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in 

263 
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots' 

269 
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in


270 
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'


264  271 
 Expr_fby (e1, e2) > 
265 
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in 

266 
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots' 

272 
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in


273 
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'


267  274 
 Expr_array el > 
268 
let el', l', eqs', asserts', annots' = inline_tuple el in 

269 
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots' 

275 
let el', l', eqs', asserts', annots' = inline_tuple el in


276 
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'


270  277 
 Expr_access (e, dim) > 
271 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 

272 
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots' 

278 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in


279 
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'


273  280 
 Expr_power (e, dim) > 
274 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 

275 
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots' 

281 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in


282 
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'


276  283 
 Expr_pre e > 
277 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 

278 
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots' 

284 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in


285 
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'


279  286 
 Expr_when (e, id, label) > 
280 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 

281 
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots' 

287 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in


288 
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'


282  289 
 Expr_merge (id, branches) > 
283 
let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in 

284 
let branches' = List.map2 (fun (label, _) v > label, v) branches el in 

285 
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots' 

290 
let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in


291 
let branches' = List.map2 (fun (label, _) v > label, v) branches el in


292 
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'


286  293  
287  294 
and inline_node ?(selection_on_annotation=false) node nodes = 
288  295 
try copy_node (Hashtbl.find inline_table node.node_id) 
289  296 
with Not_found > 
290 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 

291 
let new_locals, eqs, asserts, annots = 

292 
List.fold_left (fun (locals, eqs, asserts, annots) eq > 

293 
let eq_rhs', locals', new_eqs', asserts', annots' = 

294 
inline_expr eq.eq_rhs locals node nodes 

295 
in 

296 
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts, annots'@annots 

297 
) (node.node_locals, [], node.node_asserts, node.node_annot) (get_node_eqs node) 

298 
in 

299 
let inlined = 

300 
{ node with 

301 
node_locals = new_locals; 

302 
node_stmts = List.map (fun eq > Eq eq) eqs; 

303 
node_asserts = asserts; 

304 
node_annot = annots; 

305 
} 

306 
in 

307 
begin 

308 
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*) 

309 
Hashtbl.add inline_table node.node_id inlined; 

310 
inlined 

311 
end 

297 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 

298 
let eqs, auts = get_node_eqs node in 

299 
assert (auts = []); (* No inlining of automaton yet. One should visit each 

300 
handler eqs and perform similar computation *) 

301 
let new_locals, stmts, asserts, annots = 

302 
List.fold_left (fun (locals, stmts, asserts, annots) eq > 

303 
let eq_rhs', locals', new_stmts', asserts', annots' = 

304 
inline_expr eq.eq_rhs locals node nodes 

305 
in 

306 
locals', Eq { eq with eq_rhs = eq_rhs' }::new_stmts'@stmts, asserts'@asserts, annots'@annots 

307 
) (node.node_locals, [], node.node_asserts, node.node_annot) eqs 

308 
in 

309 
let inlined = 

310 
{ node with 

311 
node_locals = new_locals; 

312 
node_stmts = stmts; 

313 
node_asserts = asserts; 

314 
node_annot = annots; 

315 
} 

316 
in 

317 
begin 

318 
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*) 

319 
Hashtbl.add inline_table node.node_id inlined; 

320 
inlined 

321 
end 

312  322  
313  323 
let inline_all_calls node nodes = 
314  324 
let nd = match node.top_decl_desc with Node nd > nd  _ > assert false in 
...  ...  
333  343 
let inlined_rename = rename_local_node inlined "inlined_" in 
334  344 
let identity = (fun x > x) in 
335  345 
let is_node top = match top.top_decl_desc with Node _ > true  _ > false in 
336 
let orig = rename_prog orig_rename identity identity orig in


346 
let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in


337  347 
let inlined = rename_prog inlined_rename identity identity inlined in 
338  348 
let nodes_origs, others = List.partition is_node orig in 
339  349 
let nodes_inlined, _ = List.partition is_node inlined in 
Also available in: Unified diff
[general] Refactor get_node_eqs to produce (eqs, auts) with automatons