From 94224469bd2c6a410e9cadecd4f2c5e87be082e8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Apr 2008 19:42:34 +0000 Subject: [PATCH] added check on all bodies, only the one we actually encountered is applied to all arguments, other boedies are applied only up to j --- .../components/ng_kernel/nCicTypeChecker.ml | 41 +++++++++++-------- 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 55a3a6d7f..99829c4a7 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -68,7 +68,7 @@ let string_of_recfuns ~subst ~metasenv ~context l = | _ -> assert false) dang) ;; -let fixed_args bo j n nn = +let fixed_args bos j n nn = let rec aux k acc = function | NCic.Appl (NCic.Rel i::args) when i+k > n && i+k <= nn -> (try @@ -79,7 +79,8 @@ let fixed_args bo j n nn = (* 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 + List.fold_left (aux 0) + (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos ;; let rec list_iter_default2 f l1 def l2 = @@ -965,19 +966,20 @@ and eat_lambdas ~subst ~metasenv context n te = (NCicPp.ppterm ~subst ~metasenv ~context te)))) and eat_or_subst_lambdas - ~subst ~metasenv n te to_be_subst args (context, recfuns, x as k) + ~subst ~metasenv app_all_args n te to_be_subst args (context, recfuns, x as k) = match n, R.whd ~subst context te, to_be_subst, args with - | (0, _,_,[]) -> te, k + | (0, _,_,_) when args = [] || not app_all_args -> te, k | (0, _,_,_::_) -> C.Appl (te::args), k | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 -> - eat_or_subst_lambdas ~subst ~metasenv + eat_or_subst_lambdas ~subst ~metasenv app_all_args (n - 1) (S.subst arg ta) to_be_subst args k | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 -> - eat_or_subst_lambdas ~subst ~metasenv + eat_or_subst_lambdas ~subst ~metasenv app_all_args (n - 1) ta to_be_subst args (shift_k (name,(C.Decl so)) k) - | (n, te, _, []) -> te, k + | (n, te, _, _) when args = [] || not app_all_args -> te, k | (n, te, _, _::_) -> C.Appl (te::args), k + | (_,_,_,[]) -> assert false (* caml thinks is missing *) and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in @@ -1017,29 +1019,32 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = | _,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) -> + | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,_))) 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) in - let bo = List.nth bos i in let fl_len = List.length fl in - let bo = debruijn uri fl_len context bo in + let bos = List.map (debruijn uri fl_len context) bos in + let j = List.fold_left min max_int (List.map (fun (_,_,i,_,_)->i) fl) in let ctx_len = List.length context in (* we may look for fixed params not only up to j ... *) - let fa = fixed_args bo j ctx_len (ctx_len + fl_len) in + let fa = fixed_args bos 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 = - (* 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 + let ctx_len = List.length context in + let extra_recfuns = + HExtlib.list_mapi (fun _ i -> ctx_len - i, UnfFix fa) ctx_tys + in + let k = context, extra_recfuns@recfuns, x in + let bos_and_ks = + HExtlib.list_mapi (fun bo fno -> + (* potrebbe anche aggiungere un arg di cui fa push alle safe *) + eat_or_subst_lambdas ~subst ~metasenv (fno=i) j bo fa args k) bos in - let k = context, (List.length context - i,UnfFix fa) :: recfuns, x in - aux k bo + List.iter (fun (bo,k) -> aux k bo) bos_and_ks | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t -> (match R.whd ~subst context term with | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x -> -- 2.39.2