From f1ce4df54ccdeba41d69a6366b4ad2b970a02773 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jul 2008 17:01:49 +0000 Subject: [PATCH] - too strict check on left parameters of constructors in guarded by constructors removed - the cases Fixpont and CoFixpoint in guarded by constructors are useless code in the new kernel since: o recursive/corecursive objects are now closed terms o we do not allow (yet?) to pass co-recursive functions around o we do check that the arguments of the application of a fix/cofix do not contain the function we are checking for GBC --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 173803367..56119fce7 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -947,7 +947,6 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = (List.map (fun x-> PP.ppterm ~subst ~metasenv ~context x) args)))) in let left, args = HExtlib.split_nth paramsno tl in - List.for_all (does_not_occur ~subst context n nn) left && analyse_instantiated_type rec_params args | C.Appl ((C.Match (_,out,te,pl))::_) | C.Match (_,out,te,pl) as t -> @@ -956,6 +955,9 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te && List.for_all (aux context n nn h) pl +(* IMPOSSIBLE unsless we allow to pass cofix to other fix/cofix as we do for + higher order fix in g_b_destructors. + | C.Const (Ref.Ref (u,(Ref.Fix _| Ref.CoFix _)) as ref) | C.Appl(C.Const (Ref.Ref(u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t -> let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in @@ -967,6 +969,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = (fun (_,_,_,_,bo) -> aux (context@tys) n nn h (debruijn u len context bo)) fl +*) | C.Const _ | C.Appl _ as t -> does_not_occur ~subst context n nn t in -- 2.39.2