X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=f1840cf7c95c75cf37877712fdfa70fdb66caa34;hb=8c0ccf03dbefd83818bc3b6849634f422f8ec727;hp=52192f723de1f0181a3f0cb1474307de068dc025;hpb=04c05cf08605156ba8c6fa7225b4a90496c03698;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 52192f723..f1840cf7c 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -35,6 +35,7 @@ module PEH  = ProofEngineHelpers
 module TC   = CicTypeChecker 
 module Un   = CicUniv
 module L    = Librarian
+module Ut   = CicUtil
 
 module H    = ProceduralHelpers
 module Cl   = ProceduralClassify
@@ -45,6 +46,8 @@ let debug = ref false
 
 (* term optimization ********************************************************)
 
+let critical = ref true
+
 type status = {
    dummy: unit;
    info: string
@@ -67,8 +70,8 @@ let clear_absts m =
          aux 0 (pred n) (S.lift (-1) t)
       | t                  when n > 0 ->
          Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t);
-	 assert false 
-      | t                                 -> t
+         assert false
+      | t                             -> t
    in 
    aux m
 
@@ -176,7 +179,7 @@ and opt_appl g st es c t vs =
    in
    if es then H.list_fold_right_cps g map vs (st, []) else g (st, vs)
 
-and opt_mutcase g st es c uri tyno outty arg cases =
+and opt_mutcase_critical g st es c uri tyno outty arg cases =   
    let eliminator = H.get_default_eliminator c uri tyno outty in
    let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
    let ps, sort_disp = H.get_ind_parameters c arg in
@@ -205,6 +208,13 @@ and opt_mutcase g st es c uri tyno outty arg cases =
    let x = H.refine c (C.Appl args) in
    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
+
+and opt_mutcase g =
+   if !critical then opt_mutcase_critical g else opt_mutcase_plain g 
+
 and opt_cast g st es c t w =
    let g st t = g (info st "Optimizer: remove 4") t in
    if es then opt_proof g st es c t else g st t
@@ -242,8 +252,8 @@ let optimize_obj = function
       let g st bo =
 	 if !debug then begin 
 	    Printf.eprintf "Optimized : %s\n" (Pp.ppterm bo); 
-	    prerr_string "H.pp_term : ";
-	    H.pp_term prerr_string [] c bo; prerr_newline ()
+	    prerr_string "Ut.pp_term : ";
+	    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