delifting a Meta with an IRL w.r.t. another IRL completely changed.

the explanation is on my whiteboard, hope someone copies it

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 72151deb802e4e1ca6f9c3c2f3349195a00a3090..cbcd8153cc2db8741da71c1715cd8e264244b9a8 100644 (file)
--- 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),