...

[helm.git] / components / acic_procedural / proceduralOptimizer.ml

diff --git a/components/acic_procedural/proceduralOptimizer.ml b/components/acic_procedural/proceduralOptimizer.ml
index 67b3af94091650d924b0269fe2af8d1f04c077c7..1953ae7f1b6a5c385fcdbb6aad65b76740a15a28 100644 (file)
--- a/components/acic_procedural/proceduralOptimizer.ml
+++ b/components/acic_procedural/proceduralOptimizer.ml
@@ -72,7 +72,10 @@ let rec opt1_letin g es c name v t =
          | 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
@@ -82,10 +85,7 @@ let rec opt1_letin g es c name v t =
 and opt1_lambda g es c name w t =
    let name = H.mk_fresh_name c name in
    let entry = Some (name, C.Decl w) in
-   let g t = 
-      let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
-      g (C.Lambda (name, w, t))
-   in
+   let g t = g (C.Lambda (name, w, t)) in
    if es then opt1_proof g es (entry :: c) t else g t
 
 and opt1_appl g es c t vs =
@@ -263,12 +263,15 @@ and opt2_term g c t =
 
 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\n" (Pp.ppterm 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)
       in
-      Printf.eprintf "BEGIN: %s\n" name;
-      begin try opt1_term (opt2_term g []) true [] bo
+      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