Evil case fixed, the coulde should be more readable

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 6abe62e809de4803da53fdde26c71394e1292f5f..2c23af050239065351c854f9c43cfc1651d64990 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -368,21 +368,33 @@ let delift metasenv subst context n l t =
                   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*)
-                  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 (*max 1 (k+1-shift1)*) (k+1) (low_gap + 1) @
-                     HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1) 
+              | NCic.Irl len, NCic.Irl len1 ->
+                  let low_restrictions, new_shift = 
+                    if k <= shift1 && shift1 < shift then 
+                      HExtlib.list_seq 1 (shift - shift1 + 1), k
+                    else if shift1 < k (* <= shift *) then
+                      let save_below = k - shift1 in
+                      HExtlib.list_seq (save_below + 1) (shift - shift1 + 1),
+                      shift1
+                    else [], shift1 - shift + k
+                  in
+                  let high_restrictions = 
+                    let last = shift + len in
+                    let last1 = shift1 + len1 in
+                    if last1 > last then
+                      let high_gap = last1 - last in
+                      HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1)
+                    else []
                   in
+                  let restrictions = low_restrictions @ high_restrictions in
+                  if restrictions = [] then
+                    if shift = k then ms, orig
+                    else ms, NCic.Meta (i, (new_shift, lc1))
+                  else
                     let metasenv, subst, newmeta = 
-                       restrict metasenv subst i restrictions 
+                       restrict metasenv subst i restrictions
                     in
-(*
+(* {{{
                   prerr_endline ("RESTRICTIONS FOR: " ^ 
                     NCicPp.ppterm ~metasenv ~subst ~context:[] 
                     (NCic.Meta (i,l1))^" that was part of a term unified with "
@@ -391,22 +403,16 @@ let delift metasenv subst context n l t =
                     string_of_int restrictions) ^ "\nMENV:\n" ^
                     NCicPp.ppmetasenv ~subst metasenv ^ "\nSUBST:\n" ^
                     NCicPp.ppsubst subst ~metasenv);
-*)
-                  let newlc_len = 
-                    len1 - low_gap - high_gap + max 0 (k - shift1) in
-                  assert (if shift1 > k then 
-                    shift1 + low_gap - shift = 0 else true);
-                  let meta = 
-                     NCic.Meta(newmeta,(shift1 + low_gap - shift, 
-                       NCic.Irl newlc_len))
-                  in
-                  let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in
-                  assert (List.length cctx = newlc_len);
+}}} *)
+                    let newlc_len = len1 - List.length restrictions in 
+                    let meta = 
+                       NCic.Meta(newmeta,(new_shift, NCic.Irl newlc_len))
+                    in
+                    assert (
+                      let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in
+                      List.length cctx = newlc_len);
                     (metasenv, subst), meta
-                  
-              | NCic.Irl _, NCic.Irl _ when shift = k -> ms, orig
-              | NCic.Irl _, NCic.Irl _ ->
-                   ms, NCic.Meta (i, (max 0 (shift1 - shift + k), lc1))
+
               | _ ->
                   let lc1 = NCicUtils.expand_local_context lc1 in
                   let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in