Revision 95944ba1
Added by PierreLoïc Garoche almost 5 years ago
src/plugins/mpfr/mpfr.ml  

262  262 
let inject_node node = 
263  263 
cpt_fresh := 0; 
264  264 
let inputs_outputs = node.node_inputs@node.node_outputs in 
265 
let norm_ctx = (node.node_id, get_node_vars node) in 

265  266 
let is_local v = 
266  267 
List.for_all ((!=) v) inputs_outputs in 
267  268 
let orig_vars = inputs_outputs@node.node_locals in 
268  269 
let defs, vars = 
269  270 
let eqs, auts = get_node_eqs node in 
270  271 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
271 
List.fold_left (inject_eq node) ([], orig_vars) eqs in


272 
List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in


272  273 
(* Normalize the asserts *) 
273  274 
let vars, assert_defs, asserts = 
274  275 
List.fold_left ( 
...  ...  
277  278 
let (defs, vars'), expr = 
278  279 
inject_expr 
279  280 
~alias:false 
280 
node


281 
norm_ctx


281  282 
([], vars) (* defvar only contains vars *) 
282  283 
assert_expr 
283  284 
in 
Also available in: Unified diff
Cleaning up stuff in normalization. Mainly replace arguments with only required elements
node_Table hashtbl is now only available through functions of the corelang.mli