From c87ca87169e38a22e7bf7a347238597500964285 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Apr 2008 17:02:00 +0000 Subject: [PATCH] fixed wrong Rel, still to do: Fix(i,j) applied to dangerous rel, check all bodies in parallel, not just the i-th --- .../components/ng_kernel/nCicTypeChecker.ml | 32 +++++++++++-------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 63b7765a5..55a3a6d7f 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -71,9 +71,12 @@ let string_of_recfuns ~subst ~metasenv ~context l = let fixed_args bo j n nn = let rec aux k acc = function | NCic.Appl (NCic.Rel i::args) when i+k > n && i+k <= nn -> - let lefts, _ = HExtlib.split_nth j args in - List.map (fun ((b,x),i) -> b && x = NCic.Rel (k+(j-i))) - (HExtlib.list_mapi (fun x i -> x,i) (List.combine acc lefts)) + (try + let lefts, _ = HExtlib.split_nth j args in + List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) + (HExtlib.list_mapi (fun x i -> x,i) (List.combine acc lefts)) + with Failure "HExtlib.split_nth" -> assert false) + (* se sono meno di j, fino a j deduco, dopo false *) | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t in aux 0 (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bo @@ -990,12 +993,8 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = match t with | C.Rel m as t when is_dangerous m recfuns -> raise (NotGuarded (lazy - (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around"))) - | C.Rel m -> - (match List.nth context (m-1) with - | _,C.Decl _ -> () - | _,C.Def (bo,_) -> aux k (S.lift m bo)) - | C.Meta _ -> () + (NCicPp.ppterm ~subst ~metasenv ~context t ^ + " is a partial application of a fix"))) | C.Appl ((C.Rel m)::tl) as t when is_dangerous m recfuns -> let rec_no = get_recno m recfuns in if not (List.length tl > rec_no) then @@ -1013,8 +1012,14 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = | C.Appl ((C.Rel m)::tl) when is_unfolded m recfuns -> let fixed_args = get_fixed_args m recfuns in list_iter_default2 (fun x b -> if not b then aux k x) tl false fixed_args - | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,j))) as r)::args) - when List.exists (fun t->try aux k t;false with NotGuarded _->true) args -> + | C.Rel m -> + (match List.nth context (m-1) with + | _,C.Decl _ -> () + | _,C.Def (bo,_) -> aux k (S.lift m bo)) + | C.Meta _ -> () + | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,j))) as r)::args) -> + if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args + then let fl,_,_ = E.get_checked_fixes r in let ctx_tys, bos = List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl) @@ -1023,13 +1028,14 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = let fl_len = List.length fl in let bo = debruijn uri fl_len context bo in let ctx_len = List.length context in - (* cerco i parametri fissi solo fino a j, un po aleatorio *) + (* we may look for fixed params not only up to j ... *) let fa = fixed_args bo j ctx_len (ctx_len + fl_len) in list_iter_default2 (fun x b -> if not b then aux k x) args false fa; let context = context@ctx_tys in let k = context, recfuns, x in let bo, k = - (* potrebbe anche aggiungere un arg di cui fa push alle safe *) + (* we should enrich k with infos regarding args that are safe but not + * fixed *) eat_or_subst_lambdas ~subst ~metasenv j bo fa args k in let k = context, (List.length context - i,UnfFix fa) :: recfuns, x in -- 2.39.2