X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=19d96a91aa7ef042f7113656a43cb8a4ce99f4fa;hb=2921483dad22e14c2e697cbe5597a0b32af04090;hp=fe06207d38b9c99dfdb3e2a7424c63b79e2dae35;hpb=93afc8e27cf27754ff73b426e0b1d4df97224dee;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index fe06207d3..19d96a91a 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -82,10 +82,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 =
@@ -126,11 +123,11 @@ and opt1_appl g es c t vs =
 	          | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv ->
 		     let x = C.Appl (t :: List.rev rvs @ [define rv]) in
 		     HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x
-	          | Some _, _                                              ->
+	          | _ (* Some _, _ *)                                             ->
 		     g (C.Appl (t :: vs))
-		  | None, _                                                ->
+(*		  | None, _                                                ->
 	             aux false [] (vs, classes)
-	    in
+*)	    in
 	    let rec aux h prev = function
 	       | C.LetIn (name, vv, tt) :: vs ->
 	          let t = S.lift 1 t in
@@ -264,11 +261,13 @@ and opt2_term g c t =
 let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
       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