- Coq/preamble: missing alias added

[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 1b4cbd8e003ca3790f89f21c2f72ec465036bc35..a05bbd26d8df836d422b6fee82dd838b44840281 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -46,6 +46,8 @@ let debug = ref false
 
 (* term optimization ********************************************************)
 
+let critical = ref true
+
 type status = {
    dummy: unit;
    info: string
@@ -68,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
 
@@ -177,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
@@ -206,6 +208,19 @@ 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 =
+      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 
+
 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