Revision 1eda3e78 src/inliner.ml
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