- procedural: bugfix in "Barendregt convention" test

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

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index c27966a4a0e05192a1ac880175a50c7e759e7072..0364803c73d82c8552aa4e01b9e3b7d6b1c1f165 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -81,7 +81,7 @@ let rec add_abst k = function
    | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
 
 let rec opt_letin g st es c name v w t =
-   let name = H.mk_fresh_name c name in
+   let name = H.mk_fresh_name true c name in
    let entry = Some (name, C.Def (v, w)) in
    let g st t =
       if DTI.does_not_occur 1 t then
@@ -107,7 +107,7 @@ let rec opt_letin g st es c name v w t =
    if es then opt_proof g st es (entry :: c) t else g st t
 
 and opt_lambda g st es c name w t =
-   let name = H.mk_fresh_name c name in
+   let name = H.mk_fresh_name true c name in
    let entry = Some (name, C.Decl w) in
    let g st t = g st (C.Lambda (name, w, t)) in
    if es then opt_proof g st es (entry :: c) t else g st t
@@ -259,6 +259,14 @@ let optimize_obj = function
    | 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 
@@ -272,9 +280,6 @@ let optimize_obj = function
         L.time_stamp ("PO: DONE       " ^ name);
         C.Constant (name, Some bo, ty, pars, attrs), st.info
       in
-      L.time_stamp ("PO: OPTIMIZING " ^ name);
-      if !debug then Printf.eprintf "BEGIN: %s\n" name;
-      let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in
       wrap g (info st nodes) c bo
    | obj                                         -> obj, ""