Revision 3b2bd83d src/inliner.ml
src/inliner.ml  

39  39 
eq_lhs = List.map rename eq.eq_lhs; 
40  40 
eq_rhs = rename_expr rename eq.eq_rhs 
41  41 
} 
42  
43 
let rec add_expr_reset_cond cond expr = 

44 
let aux = add_expr_reset_cond cond in 

45 
let new_desc = 

46 
match expr.expr_desc with 

47 
 Expr_const _ 

48 
 Expr_ident _ > expr.expr_desc 

49 
 Expr_tuple el > Expr_tuple (List.map aux el) 

50 
 Expr_ite (c, t, e) > Expr_ite (aux c, aux t, aux e) 

51 


52 
 Expr_arrow (e1, e2) > 

53 
(* we replace the expression e1 > e2 by e1 > (if cond then e1 else e2) *) 

54 
let e1 = aux e1 and e2 = aux e2 in 

55 
(* inlining is performed before typing. we can leave the fields free *) 

56 
let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in 

57 
Expr_arrow (e1, new_e2) 

58  
59 
 Expr_fby _ > assert false (* TODO: deal with fby. This hasn't been much handled yet *) 

60  
61 
 Expr_array el > Expr_array (List.map aux el) 

62 
 Expr_access (e, dim) > Expr_access (aux e, dim) 

63 
 Expr_power (e, dim) > Expr_power (aux e, dim) 

64 
 Expr_pre e > Expr_pre (aux e) 

65 
 Expr_when (e, id, l) > Expr_when (aux e, id, l) 

66 
 Expr_merge (id, cases) > Expr_merge (id, List.map (fun (l,e) > l, aux e) cases) 

67  
68 
 Expr_appl (id, args, reset_opt) > 

69 
(* we "add" cond to the reset field. *) 

70 
let new_reset = match reset_opt with 

71 
None > cond 

72 
 Some cond' > mkpredef_call cond'.expr_loc "" [cond; cond'] 

73 
in 

74 
Expr_appl (id, args, Some new_reset) 

75 


76  
77 
in 

78 
{ expr with expr_desc = new_desc } 

79  
80 
let add_eq_reset_cond cond eq = 

81 
{ eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs } 

42  82 
(* 
43  83 
let get_static_inputs input_arg_list = 
44  84 
List.fold_right (fun (vdecl, arg) res > 
...  ...  
54  94 
else res) 
55  95 
input_arg_list [] 
56  96 
*) 
97  
98  
57  99 
(* 
58  100 
expr, locals', eqs = inline_call id args' reset locals node nodes 
59  101  
...  ...  
64  106 
the resulting expression is tuple_of_renamed_outputs 
65  107 

66  108 
TODO: convert the specification/annotation/assert and inject them 
67 
TODO: deal with reset 

68  109 
*) 
69 
let inline_call node orig_expr args reset locals caller = 

70 
let loc = orig_expr.expr_loc in 

71 
let uid = orig_expr.expr_tag in 

110 
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr, 

111 
locals, eqs, asserts) 

112 
*) 

113 
let inline_call node loc uid args reset locals caller = 

72  114 
let rename v = 
73  115 
if v = tag_true  v = tag_false  not (is_node_var node v) then v else 
74  116 
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) 
...  ...  
96  138 
v.var_dec_const, 
97  139 
Utils.option_map (rename_expr rename) v.var_dec_value) in 
98  140 
begin 
99 
(* 

100 
(try


101 
Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);


102 
Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))


103 
with Not_found > ());


104 
(try


105 
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) 

106 
with Not_found > ());


107 
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*) 

108 
*) 

141 
(*


142 
(try


143 
Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs); 

144 
Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ())) 

145 
with Not_found > ());


146 
(try


147 
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))


148 
with Not_found > ());


149 
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)


150 
*)


109  151 
vdecl 
110  152 
end 
111 
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)


153 
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*) 

112  154 
in 
113  155 
let inputs' = List.map (fun (vdecl, _) > rename_var vdecl) dynamic_inputs in 
114  156 
let outputs' = List.map rename_var node.node_outputs in 
115  157 
let locals' = 
116 
(List.map (fun (vdecl, arg) > let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)


158 
(List.map (fun (vdecl, arg) > let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs) 

117  159 
@ (List.map rename_var node.node_locals) 
118 
in 

160 
in


119  161 
(* checking we are at the appropriate (early) step: node_checks and 
120  162 
node_gencalls should be empty (not yet assigned) *) 
121  163 
assert (node.node_checks = []); 
122  164 
assert (node.node_gencalls = []); 
123  165  
124 
(* Bug included: todo deal with reset *) 

125 
assert (reset = None); 

126  
127 
let assign_inputs = mkeq loc (List.map (fun v > v.var_id) inputs', expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in 

166 
(* Expressing reset locally in equations *) 

167 
let eqs_r' = 

168 
match reset with 

169 
None > eqs' 

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

171 
in 

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

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

128  174 
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') 
129  175 
in 
130  176 
let asserts' = (* We rename variables in assert expressions *) 
...  ...  
133  179 
{a with assert_expr = 
134  180 
let expr = a.assert_expr in 
135  181 
rename_expr rename expr 
136 
})


182 
})


137  183 
node.node_asserts 
138  184 
in 
185 
let annots' = 

186 
Plugins.inline_annots rename node.node_annot 

187 
in 

139  188 
expr, 
140  189 
inputs'@outputs'@locals'@locals, 
141 
assign_inputs::eqs', 

142 
asserts' 

190 
assign_inputs::eqs_r', 

191 
asserts', 

192 
annots' 

143  193  
144  194  
145  195  
...  ...  
156  206 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 
157  207 
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in 
158  208 
let inline_tuple el = 
159 
List.fold_right (fun e (el_tail, locals, eqs, asserts) > 

160 
let e', locals', eqs', asserts' = inline_expr e locals node nodes in 

161 
e'::el_tail, locals', eqs'@eqs, asserts@asserts' 

162 
) el ([], locals, [], []) 

209 
List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) >


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


211 
e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots'


212 
) el ([], locals, [], [], [])


163  213 
in 
164  214 
let inline_pair e1 e2 = 
165 
let el', l', eqs', asserts' = inline_tuple [e1;e2] in 

215 
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in


166  216 
match el' with 
167 
 [e1'; e2'] > e1', e2', l', eqs', asserts' 

217 
 [e1'; e2'] > e1', e2', l', eqs', asserts', annots'


168  218 
 _ > assert false 
169  219 
in 
170  220 
let inline_triple e1 e2 e3 = 
171 
let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in 

221 
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in


172  222 
match el' with 
173 
 [e1'; e2'; e3'] > e1', e2', e3', l', eqs', asserts' 

223 
 [e1'; e2'; e3'] > e1', e2', e3', l', eqs', asserts', annots'


174  224 
 _ > assert false 
175  225 
in 
176  226 

177  227 
match expr.expr_desc with 
178  228 
 Expr_appl (id, args, reset) > 
179 
let args', locals', eqs', asserts' = inline_expr args locals node nodes in 

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


180  230 
if List.exists (check_node_name id) nodes && (* the current node call is provided 
181  231 
as arguments nodes *) 
182  232 
(not selection_on_annotation  is_inline_expr expr) (* and if selection on annotation is activated, 
...  ...  
188  238 
with Not_found > (assert false) in 
189  239 
let called = node_of_top called in 
190  240 
let called' = inline_node called nodes in 
191 
let expr, locals', eqs'', asserts'' = 

192 
inline_call called' expr args' reset locals' node in 

193 
expr, locals', eqs'@eqs'', asserts'@asserts'' 

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


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


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


194  244 
else 
195  245 
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) 
196  246 
{ expr with expr_desc = Expr_appl(id, args', reset)}, 
197  247 
locals', 
198  248 
eqs', 
199 
asserts' 

249 
asserts', 

250 
annots' 

200  251  
201  252 
(* For other cases, we just keep the structure, but convert subexpressions *) 
202  253 
 Expr_const _ 
203 
 Expr_ident _ > expr, locals, [], [] 

254 
 Expr_ident _ > expr, locals, [], [], []


204  255 
 Expr_tuple el > 
205 
let el', l', eqs', asserts' = inline_tuple el in 

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

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


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


207  258 
 Expr_ite (g, t, e) > 
208 
let g', t', e', l', eqs', asserts' = inline_triple g t e in 

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

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'


210  261 
 Expr_arrow (e1, e2) > 
211 
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in 

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

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'


213  264 
 Expr_fby (e1, e2) > 
214 
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in 

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

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'


216  267 
 Expr_array el > 
217 
let el', l', eqs', asserts' = inline_tuple el in 

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

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


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


219  270 
 Expr_access (e, dim) > 
220 
let e', l', eqs', asserts' = inline_expr e locals node nodes in 

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

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'


222  273 
 Expr_power (e, dim) > 
223 
let e', l', eqs', asserts' = inline_expr e locals node nodes in 

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

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'


225  276 
 Expr_pre e > 
226 
let e', l', eqs', asserts' = inline_expr e locals node nodes in 

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

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'


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

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

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'


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

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


233  284 
let branches' = List.map2 (fun (label, _) v > label, v) branches el in 
234 
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts' 

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


235  286  
236  287 
and inline_node ?(selection_on_annotation=false) node nodes = 
237  288 
try copy_node (Hashtbl.find inline_table node.node_id) 
238  289 
with Not_found > 
239  290 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 
240 
let new_locals, eqs, asserts = 

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

242 
let eq_rhs', locals', new_eqs', asserts' = 

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' =


243  294 
inline_expr eq.eq_rhs locals node nodes 
244  295 
in 
245 
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts 

246 
) (node.node_locals, [], node.node_asserts) (get_node_eqs node) 

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)


247  298 
in 
248  299 
let inlined = 
249  300 
{ node with 
250  301 
node_locals = new_locals; 
251  302 
node_stmts = List.map (fun eq > Eq eq) eqs; 
252  303 
node_asserts = asserts; 
304 
node_annot = annots; 

253  305 
} 
254  306 
in 
255  307 
begin 
...  ...  
363  415 
in 
364  416 
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in 
365  417 
let new_prog = others@nodes_origs@nodes_inlined@main in 
418 
(* 

419 
let _ = Typing.type_prog type_env new_prog in 

420 
let _ = Clock_calculus.clock_prog clock_env new_prog in 

421 
*) 

422 


366  423 
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in 
367  424 
let witness_out = open_out witness_file in 
368  425 
let witness_fmt = Format.formatter_of_out_channel witness_out in 
...  ...  
387  444 
 _ > main_opt, nodes, top::others) 
388  445 
prog (None, [], []) 
389  446 
in 
390  
391  447 
(* Recursively each call of a node in the top node is replaced *) 
392  448 
let main_node = Utils.desome main_node in 
393  449 
let main_node' = inline_all_calls main_node other_nodes in 
Also available in: Unified diff