made executable again

[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 0364803c73d82c8552aa4e01b9e3b7d6b1c1f165..c5a27efc44942bbd8e7b028a99791779e9be9a47 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -99,7 +99,9 @@ let rec opt_letin g st es c name v w t =
          | v when H.is_proof c v && H.is_atomic v          ->
            let x = S.subst v t in
            opt_proof g (info st "Optimizer: remove 5") true c x 
-        | v                                               ->
+(*      | v when t = C.Rel 1                              ->
+           g (info st "Optimizer: remove 6") v 
+*)      | v                                               ->
            g st (C.LetIn (name, v, w, t))
       in
       if es then opt_term g st es c v else g st v
@@ -190,6 +192,10 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
       opt_mutcase_plain g st es c uri tyno outty arg cases
    else
    let predicate = clear_absts rpsno (1 - sort_disp) outty in   
+   if H.occurs c ~what:(C.Rel 0) ~where:predicate then
+(* FG: the transformation is not possible, we fall back into the plain case *)
+      opt_mutcase_plain g st es c uri tyno outty arg cases
+   else
    let is_recursive t =
       I.S.mem tyno (I.get_mutinds_of_uri uri t) 
    in
@@ -209,8 +215,13 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
    in
    let lifted_cases = List.map2 map2 cases constructors in
    let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
-   let x = H.refine c (C.Appl args) in
-   opt_proof g (info st "Optimizer: remove 3") es c x
+   try 
+      let x = H.refine c (C.Appl args) in
+      opt_proof g (info st "Optimizer: remove 3") es c x        
+   with e ->
+(* FG: the transformation is not possible, we fall back into the plain case *)
+      let st = info st ("Optimizer: refine_error: " ^ Printexc.to_string e) in
+      opt_mutcase_plain g st es c uri tyno outty arg cases
 
 and opt_mutcase_plain g st es c uri tyno outty arg cases =
    let g st v =