more bug fixed (or introduced)

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index bc22a21608c1042ea20cbe3cd4d6bf582097056e..5e68057bb21f6559e2424ed589a8f71cd1cfc129 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -275,6 +275,7 @@ let _ =
                prerr_endline msg;
                assert false
           in
+          prerr_endline "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX";
           let metasenv, subst = 
             try 
               NCicUnification.unify metasenv subst [] infty ty

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index cbcd8153cc2db8741da71c1715cd8e264244b9a8..aa49a84ee726db1edafa785df5b5cd686aa261f9 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -345,6 +345,7 @@ let delift metasenv subst context n l t =
                   aux k ms (NCicSubstitution.lift n bo))
           | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k)
         with Failure _ -> assert false) (*Unbound variable found in delift*)
+    | NCic.Meta (_,(_,(NCic.Irl 0| NCic.Ctx []))) as orig -> ms, orig
     | NCic.Meta (i,l1) as orig ->
         (try
            let _,_,t,_ = NCicUtils.lookup_subst i subst in
@@ -360,36 +361,56 @@ let delift metasenv subst context n l t =
            else
               let shift1,lc1 = l1 in
               let shift,lc = l in
+              let shift = shift + k in
+              let _ = prerr_endline ("XXX restringo " ^ string_of_int i) in
               match lc, lc1 with
               | NCic.Irl len, NCic.Irl len1 
-                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
+                when shift1 + len1 < shift || shift1 > shift + len ->
+                        prerr_endline "WWW 1";
+                  let restrictions = HExtlib.list_seq 1 (len1 + 1) in
+                  let metasenv, subst, newmeta = 
+                     restrict metasenv subst i restrictions 
+                  in
+                  (metasenv, subst), 
+                    NCic.Meta (newmeta, (0,NCic.Irl (max 0 (k-shift1))))
+              | NCic.Irl len, NCic.Irl len1 
+                when shift1 < shift || len1 + shift1 > len + shift ->
+                  (* C. Hoare. Premature optimization is the root of all evil*)
+                        prerr_endline ("WWW 2 : " ^ string_of_int i);
+                  let stop = shift + len in
+                  let stop1 = shift1 + len1 in
+                  let low_gap = max 0 (shift - shift1) in
+                  let high_gap = max 0 (stop1 - stop) in
                   let restrictions = 
-                     HExtlib.list_seq 1 (low_gap+1) @
-                     HExtlib.list_seq (len1-high_gap) len1
+                     HExtlib.list_seq (k+1-shift1) (low_gap + 1) @
+                     HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1)
                   in
-(*
+                    let metasenv, subst, newmeta = 
+                       restrict metasenv subst i restrictions 
+                    in
                   prerr_endline ("RESTRICTIONS FOR: " ^ 
-                    NCicPp.ppterm ~metasenv ~subst ~context:[] 
+                  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
+                    String.concat "," (List.map string_of_int restrictions)
+                    ^ "\nMENV:\n" ^ NCicPp.ppmetasenv ~subst metasenv
+                    ^ "\nSUBST:\n" ^ NCicPp.ppsubst subst ~metasenv
+                    );
+                  let newlc = 
+                    assert (if shift1 > k then shift1 + low_gap - shift = 0 else
+                    true);
+                    NCic.Irl (len1 - low_gap - high_gap + max 0 (k - shift1)) in
                   let meta = 
-                    NCic.Meta(newmeta,(k,NCic.Irl (len - low_gap - high_gap))) 
+                     NCic.Meta(newmeta,(shift1 + low_gap - shift, newlc))
                   in
-                  (metasenv, subst), meta
+                    (metasenv, subst), meta
                   
               | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
               | NCic.Irl _, NCic.Irl _ ->
-                   ms, NCic.Meta (i, (shift1 - shift, lc1))
-              | _ -> 
+                   ms, NCic.Meta (i, (max 0 (shift1 - shift), lc1))
+              | _ ->
                   let lc1 = NCicUtils.expand_local_context lc1 in
                   let rec deliftl tbr j ms = function
                     | [] -> ms, tbr, []