From f31566c556d6c47e283995f50d29f98d509a1fef Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Oct 2008 22:31:41 +0000 Subject: [PATCH] delifting a Meta with an IRL w.r.t. another IRL completely changed. the explanation is on my whiteboard, hope someone copies it --- .../components/ng_refiner/nCicMetaSubst.ml | 30 +++++++++++++------ 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 72151deb8..cbcd8153c 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -311,10 +311,6 @@ and restrict metasenv subst i restrictions = force_does_not_occur metasenv subst restrictions ty in let j = newmeta () in let metasenv_entry = j, (name, newctx, newty) in - prerr_endline ("restricting ?" ^ string_of_int i ^ " to ?" ^ - string_of_int j ^ " : " ^ NCicPp.ppterm ~metasenv ~context:newctx - ~subst newty ^" in a shorter context:\n" ^ - NCicPp.ppcontext ~metasenv ~subst newctx); let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in @@ -366,16 +362,30 @@ let delift metasenv subst context n l t = let shift,lc = l in match lc, lc1 with | NCic.Irl len, NCic.Irl len1 - when shift1 < shift || len1 + shift1 > len + shift -> + when shift1 - k < shift || len1 + shift1 - k > len + shift -> + let low_gap = max 0 (shift - (shift1 - k)) in + let high_gap = max 0 (shift1 + len1 - k - (shift + len)) in let restrictions = - HExtlib.list_seq 1 (shift - shift1) @ - HExtlib.list_seq (shift+len+1) (shift1+len1) + HExtlib.list_seq 1 (low_gap+1) @ + HExtlib.list_seq (len1-high_gap) len1 in +(* + prerr_endline ("RESTRICTIONS FOR: " ^ + NCicPp.ppterm ~metasenv ~subst ~context:[] + (NCic.Meta (i,l1)) ^ + " that was part of a term unified with " ^ + NCicPp.ppterm ~metasenv ~subst ~context:[] + (NCic.Meta (n,l)) ^ " ====> " ^ + String.concat "," (List.map string_of_int restrictions)); +*) let metasenv, subst, newmeta = restrict metasenv subst i restrictions in - (metasenv, subst), - NCic.Meta(newmeta, mk_perforated_irl shift1 len1 restrictions) + let meta = + NCic.Meta(newmeta,(k,NCic.Irl (len - low_gap - high_gap))) + in + (metasenv, subst), meta + | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig | NCic.Irl _, NCic.Irl _ -> ms, NCic.Meta (i, (shift1 - shift, lc1)) @@ -392,8 +402,10 @@ let delift metasenv subst context n l t = | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl in let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in +(* prerr_endline ("TO BE RESTRICTED: " ^ (String.concat "," (List.map string_of_int to_be_r))); +*) let l1 = pack_lc (shift, NCic.Ctx lc1') in if to_be_r = [] then (metasenv, subst), -- 2.39.2