From 2e58d03db0222ac0d885abeaebceac07ac586761 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 21 May 2009 12:45:14 +0000 Subject: [PATCH] - cicUtil: is_sober now detects non-positive rels. - PropceduralOptimizer: bug fix in critical step detection now decidable_kit/streicher.ma is fully reconstructed :) --- .../components/acic_procedural/proceduralOptimizer.ml | 4 ++++ helm/software/components/cic/cicUtil.ml | 3 ++- helm/software/components/cic/cicUtil.mli | 4 ++-- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 8a7e5bea5..c5a27efc4 100644 --- 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 deb8f1e68..36f65391e 100644 --- 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 237aa19a4..c9dd896b9 100644 --- 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 -- 2.39.2