Revision 53206908 src/inliner.ml
src/inliner.ml  

64  64 
the resulting expression is tuple_of_renamed_outputs 
65  65 

66  66 
TODO: convert the specification/annotation/assert and inject them 
67 
DONE: annotations 

67  68 
TODO: deal with reset 
68  69 
*) 
69  70 
let inline_call node orig_expr args reset locals caller = 
...  ...  
136  137 
}) 
137  138 
node.node_asserts 
138  139 
in 
140 
let annots' = 

141 
Plugins.inline_annots rename node.node_annot 

142 
in 

139  143 
expr, 
140  144 
inputs'@outputs'@locals'@locals, 
141  145 
assign_inputs::eqs', 
142 
asserts' 

146 
asserts', 

147 
annots' 

143  148  
144  149  
145  150  
...  ...  
156  161 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 
157  162 
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in 
158  163 
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, [], []) 

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


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


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


167 
) el ([], locals, [], [], [])


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

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


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

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


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

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


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

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


174  179 
 _ > assert false 
175  180 
in 
176 


181 


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

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


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

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


192  197 
inline_call called' expr args' reset locals' node in 
193 
expr, locals', eqs'@eqs'', asserts'@asserts'' 

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


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

204 
asserts', 

205 
annots' 

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

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


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

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

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


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


207  213 
 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' 

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


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


210  216 
 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' 

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


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


213  219 
 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' 

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


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


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

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

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


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


219  225 
 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' 

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


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


222  228 
 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' 

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


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


225  231 
 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' 

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


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


228  234 
 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' 

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


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


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

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


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

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


235  241  
236  242 
and inline_node ?(selection_on_annotation=false) node nodes = 
237  243 
try copy_node (Hashtbl.find inline_table node.node_id) 
238  244 
with Not_found > 
239  245 
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' = 

246 
let new_locals, eqs, asserts, annots =


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


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


243  249 
inline_expr eq.eq_rhs locals node nodes 
244  250 
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) 

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


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


247  253 
in 
248  254 
let inlined = 
249  255 
{ node with 
250  256 
node_locals = new_locals; 
251  257 
node_stmts = List.map (fun eq > Eq eq) eqs; 
252  258 
node_asserts = asserts; 
259 
node_annot = annots; 

253  260 
} 
254  261 
in 
255  262 
begin 
...  ...  
363  370 
in 
364  371 
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in 
365  372 
let new_prog = others@nodes_origs@nodes_inlined@main in 
373 
(* 

374 
let _ = Typing.type_prog type_env new_prog in 

375 
let _ = Clock_calculus.clock_prog clock_env new_prog in 

376 
*) 

377 


366  378 
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in 
367  379 
let witness_out = open_out witness_file in 
368  380 
let witness_fmt = Format.formatter_of_out_channel witness_out in 
...  ...  
387  399 
 _ > main_opt, nodes, top::others) 
388  400 
prog (None, [], []) 
389  401 
in 
390  
391  402 
(* Recursively each call of a node in the top node is replaced *) 
392  403 
let main_node = Utils.desome main_node in 
393  404 
let main_node' = inline_all_calls main_node other_nodes in 
394 
let res = List.map (fun top > if check_node_name !Options.main_node top then main_node' else top) prog in 

405 
let res = main_node'::other_tops in 

406 
if !Options.witnesses then ( 

407 
witness 

408 
basename 

409 
(match main_node.top_decl_desc with Node nd > nd.node_id  _ > assert false) 

410 
prog res type_env clock_env 

411 
); 

395  412 
res 
396  413  
397  414 
let local_inline basename prog type_env clock_env = 
Also available in: Unified diff