- cicUtil: is_sober now detects non-positive rels.

- PropceduralOptimizer: bug fix in critical step detection

now decidable_kit/streicher.ma is fully reconstructed :)

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 8a7e5bea5047cd0e3bcdddc9b9d50e130834751d..c5a27efc44942bbd8e7b028a99791779e9be9a47 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -192,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

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index deb8f1e68bc3fdf69a84b4f3e5fc77d50d5f4515..36f65391eeac23d27c565b65d8e09ea52cd22f0c 100644 (file)
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -550,7 +550,8 @@ let alpha_equivalence =
 
 let is_sober c t =
    let rec sober_term c g = function
-      | C.Rel _ 
+      | C.Rel i                         ->
+         if i <= 0 then fun b -> false else g
       | C.Sort _  
       | C.Implicit _                    -> g      
       | C.Const (_, xnss) 

diff --git a/helm/software/components/cic/cicUtil.mli b/helm/software/components/cic/cicUtil.mli
index 237aa19a436fb6f0bdfb51dd9571e967d367569b..c9dd896b9c3902f199976bbd5259e1c80fc329d2 100644 (file)
--- a/helm/software/components/cic/cicUtil.mli
+++ b/helm/software/components/cic/cicUtil.mli
@@ -66,8 +66,8 @@ val rehash_obj: Cic.obj -> Cic.obj
 
 val alpha_equivalence: Cic.term -> Cic.term -> bool
 
-(* FG: Consistency Check 
- * detects applications without arguments and folded applications
+(* FG: Consistency Check. Detects:
+ * applications without arguments, folded applications, non-positive rels
  *)
 val is_sober: Cic.context -> Cic.term -> bool