Revision 1eda3e78
Added by Xavier Thirioux almost 8 years ago
src/inliner.ml  

46  46 
node.node_id uid v; 
47  47 
Format.flush_str_formatter ()) 
48  48 
in 
49 
let eqs' = List.map (rename_eq rename) node.node_eqs


49 
let eqs' = List.map (rename_eq rename) (get_node_eqs node)


50  50 
in 
51  51 
let rename_var v = { v with var_id = rename v.var_id } in 
52  52 
let inputs' = List.map rename_var node.node_inputs in 
...  ...  
171  171 
inline_expr eq.eq_rhs locals nodes 
172  172 
in 
173  173 
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts 
174 
) (nd.node_locals, [], nd.node_asserts) nd.node_eqs


174 
) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)


175  175 
in 
176  176 
{ nd with 
177  177 
node_locals = new_locals; 
178 
node_eqs = eqs;


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


179  179 
node_asserts = asserts; 
180  180 
} 
181  181  
...  ...  
241  241  
242  242 
(* Building main node *) 
243  243  
244 
let ok_i_eq = 

245 
{ eq_loc = loc; 

246 
eq_lhs = List.map (fun v > v.var_id) ok_i; 

247 
eq_rhs = 

248 
let inputs = expr_of_expr_list loc (List.map (fun v > mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in 

249 
let call_orig = 

250 
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in 

251 
let call_inlined = 

252 
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in 

253 
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 

254 
mkexpr loc (Expr_appl ("=", args, None)) 

255 
} in 

256 
let ok_eq = 

257 
{ eq_loc = loc; 

258 
eq_lhs = [ok_ident]; 

259 
eq_rhs = main_ok_expr; 

260 
} in 

244  261 
let main_node = { 
245  262 
node_id = "check"; 
246  263 
node_type = Types.new_var (); 
...  ...  
251  268 
node_gencalls = []; 
252  269 
node_checks = []; 
253  270 
node_asserts = []; 
254 
node_eqs = [ 

255 
{ eq_loc = loc; 

256 
eq_lhs = List.map (fun v > v.var_id) ok_i; 

257 
eq_rhs = 

258 
let inputs = expr_of_expr_list loc (List.map (fun v > mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in 

259 
let call_orig = 

260 
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in 

261 
let call_inlined = 

262 
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in 

263 
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 

264 
mkexpr loc (Expr_appl ("=", args, None)) 

265 
}; 

266 
{ eq_loc = loc; 

267 
eq_lhs = [ok_ident]; 

268 
eq_rhs = main_ok_expr; 

269 
} 

270 
]; 

271 
node_stmts = [Eq ok_i_eq; Eq ok_eq]; 

271  272 
node_dec_stateless = false; 
272  273 
node_stateless = None; 
273  274 
node_spec = Some 
Also available in: Unified diff
 work in progress for automata...