From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 1 Aug 2008 07:29:58 +0000 (+0000)
Subject: fixed recursiveness check
X-Git-Tag: make_still_working~4868
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cbb7f68d7d012f385e74d466f0bce7881d9eb71c;p=helm.git

fixed recursiveness check
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 7fed3ddf3..00e40dfa6 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1135,6 +1135,21 @@ and guarded_by_constructors ~logger ~subst ~metasenv indURI =
  in
    aux 
 
+and is_non_recursive ctx paramsno t uri =
+  let t = debrujin_constructor uri 1 [] t in
+(*   let ctx, t =  split_prods ~subst:[] ctx paramsno t in *)
+  let len = List.length ctx in
+  let rec aux ctx n nn t =
+    match CicReduction.whd ctx t with
+    | Cic.Prod (name,src,tgt) -> 
+        does_not_occur ctx n nn src &&
+         aux (Some (name,Cic.Decl src) :: ctx) (n+1) (nn+1) tgt
+    | (Cic.Rel k) 
+    | Cic.Appl (Cic.Rel k :: _) when k = nn -> true
+    | t -> assert false
+  in
+    aux ctx (len-1) len t
+
 and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   need_dummy ind arity1 arity2 ugraph =
  let module C = Cic in
@@ -1179,8 +1194,8 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
                  paramsno (snd (List.nth cl 0)) ugraph
                in
                 b && 
-               does_not_occur [Some (C.Name name,C.Decl ty)] 0 1
-                (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ug
+                is_non_recursive [Some (C.Name name,C.Decl ty)]
+                  paramsno  (snd (List.nth cl 0)) uri, ug
              in
               (* is it a singleton or empty non recursive and non informative
                  definition? *)