....

[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 f1840cf7c95c75cf37877712fdfa70fdb66caa34..6910613d29b3b2d2bf778b751e1ce0b268339277 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -209,8 +209,14 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
    opt_proof g (info st "Optimizer: remove 3") es c x
 
 and opt_mutcase_plain g st es c uri tyno outty arg cases =
-   let g st v ts = g st (C.MutCase (uri, tyno, outty, v, ts)) in
-   g st arg cases
+   let g st v =
+      let g (st, ts) = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+      let map h v (st, vs) =
+         let h st vv = h (st, vv :: vs) in opt_proof h st es c v
+      in
+      if es then H.list_fold_right_cps g map cases (st, []) else g (st, cases)
+   in
+   if es then opt_proof g st es c arg else g st arg
 
 and opt_mutcase g =
    if !critical then opt_mutcase_critical g else opt_mutcase_plain g 
@@ -247,6 +253,7 @@ let wrap g st c bo =
 
 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
       let bo, ty = H.cic_bc c bo, H.cic_bc c ty in 
       let g st bo =
@@ -256,14 +263,14 @@ let optimize_obj = function
            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" (I.count_nodes 0 bo) 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
       in
       L.time_stamp ("PO: OPTIMIZING " ^ name);
       if !debug then Printf.eprintf "BEGIN: %s\n" name;
-      let nodes = Printf.sprintf "Initial nodes: %u" (I.count_nodes 0 bo) in
+      let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in
       wrap g (info st nodes) c bo
    | obj                                         -> obj, ""