From cbb7f68d7d012f385e74d466f0bce7881d9eb71c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 1 Aug 2008 07:29:58 +0000 Subject: [PATCH] fixed recursiveness check --- .../cic_proof_checking/cicTypeChecker.ml | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) 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? *) -- 2.39.2