- let g bo =
- Printf.eprintf "Optimized : %s\nPost Nodes: %u\n"
- (Pp.ppterm bo) (I.count_nodes 0 bo);
- let _ = H.get_type [] (C.Cast (bo, ty)) in
- C.Constant (name, Some bo, ty, pars, attrs)
+ let count_nodes = I.count_nodes ~meta:false 0 in
+ let st, c = {info = ""; dummy = ()}, [] in
+ L.time_stamp ("PO: OPTIMIZING " ^ name);
+ let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in
+ if !debug then begin
+ Printf.eprintf "BEGIN: %s\n" name;
+ Printf.eprintf "Initial : %s\n" (Pp.ppterm bo);
+ prerr_string "Ut.pp_term : ";
+ Ut.pp_term prerr_string [] c bo; prerr_newline ()
+ end;
+ let bo, ty = H.cic_bc c bo, H.cic_bc c ty in
+ let g st bo =
+ if !debug then begin
+ Printf.eprintf "Optimized : %s\n" (Pp.ppterm bo);
+ prerr_string "Ut.pp_term : ";
+ Ut.pp_term prerr_string [] c bo; prerr_newline ()
+ end;
+(* let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *)
+ let nodes = Printf.sprintf "Optimized nodes: %u" (count_nodes bo) in
+ let st = info st nodes in
+ L.time_stamp ("PO: DONE " ^ name);
+ C.Constant (name, Some bo, ty, pars, attrs), st.info