| C.LetIn (nname, vv, tt) when H.is_proof c v ->
let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
HLog.warn "Optimizer: swap 1"; opt1_proof g true c x
- | v ->
+ | v when H.is_proof c v && H.is_atomic v ->
+ let x = S.subst v t in
+ HLog.warn "Optimizer: remove 5"; opt1_proof g true c x
+ | v ->
g (C.LetIn (name, v, t))
in
if es then opt1_term g es c v else g v
let optimize_obj = function
| C.Constant (name, Some bo, ty, pars, attrs) ->
+ let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in
let g bo =
- Printf.eprintf "Optimized: %s\nNodes : %u"
+ 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)
in
- Printf.eprintf "BEGIN: %s\n" name;
+ Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n"
+ name (I.count_nodes 0 bo);
begin try opt1_term g (* (opt2_term g []) *) true [] bo
with e -> failwith ("PPP: " ^ Printexc.to_string e) end
| obj -> obj