From 641ab7e5aa7dbfa352028d7bba95def7234cc3f1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Oct 2009 13:36:32 +0000
Subject: [PATCH] relocate is hopefully fixed once and for-all!

---
 .../components/ng_tactics/nTacStatus.ml       | 77 +++++++++++--------
 1 file changed, 43 insertions(+), 34 deletions(-)

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 70ddfeaa9..8d47439c0 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -73,51 +73,60 @@ let relocate status destination (source,t as orig) =
  pp(lazy("relocate in:\n" ^ ppcontext status destination));
  let rc = 
    if source == destination then status, orig else
-    let u, d, metasenv, subst, o = status#obj in
-    let cons x (a,b) = a, x::b in
-    let rec lcp ctx j i = function
-      | (n1, NCic.Decl t1 as e)::cl1, (n2, NCic.Decl t2)::cl2 ->
+    let _, _, metasenv, subst, _ = status#obj in
+    let rec compute_ops ctx = function (* destination, source *)
+      | (n1, NCic.Decl t1 as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
           if n1 = n2 && 
              NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
-            cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2))
+            compute_ops (e::ctx) (cl1,cl2)
           else
-            j, []
-      | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 ->
+            [ `Delift ctx; `Lift (List.rev ex) ]
+      | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Def (b2,t2))::cl2 ->
           if n1 = n2 && 
              NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 &&
              NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then
-            cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2))
+            compute_ops (e::ctx) (cl1,cl2)
           else
-            j, []
-      | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Decl t2)::cl2 ->
+            [ `Delift ctx; `Lift (List.rev ex) ]
+      | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
           if n1 = n2 && 
              NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
-            cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2))
+            compute_ops (e::ctx) (cl1,cl2)
           else
-            j, []
-      | (n1, NCic.Decl _)::cl1, (n2, NCic.Def _)::cl2 -> assert false
-      | _::_, [] -> j, []
-      | _ -> 0, []
+            [ `Delift ctx; `Lift (List.rev ex) ]
+      | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 -> 
+            [ `Delift ctx; `Lift (List.rev ex) ]
+      | _::_ as ex, [] -> [ `Lift (List.rev ex) ]
+      | [], _::_ -> [ `Delift ctx ]
+      | [],[] -> []
     in
-    let shift, lc = 
-      lcp [] (List.length destination) (List.length source) 
-        (List.rev destination, List.rev source)
-    in
-    let lc = (shift,NCic.Ctx (List.rev lc)) in
-    pp(lazy("delifting as " ^ 
-      NCicPp.ppterm ~metasenv ~subst ~context:source 
-       (NCic.Meta (0,lc))));
-    let (metasenv, subst), t =
-      NCicMetaSubst.delift 
-         ~unify:(fun m s c t1 t2 -> 
-           try Some (NCicUnification.unify status m s c t1 t2)
-           with 
-            | NCicUnification.UnificationFailure _ 
-            | NCicUnification.Uncertain _ -> None) 
-       metasenv subst source 0 lc t
-    in
-    let status = status#set_obj (u, d, metasenv, subst, o) in
-    status, (destination, t)
+    let ops = compute_ops [] (List.rev destination, List.rev source) in
+    let rec mk_irl i j = if i > j then [] else NCic.Rel i :: mk_irl (i+1) j in
+    List.fold_left 
+     (fun (status, (source,t)) -> function 
+      | `Lift extra_ctx -> 
+           let len = List.length extra_ctx in
+           status, (extra_ctx@source, NCicSubstitution.lift len t)
+      | `Delift ctx -> 
+            let len_ctx = List.length ctx in
+            let irl = mk_irl 1 (List.length ctx) in
+            let lc = List.length source - len_ctx, NCic.Ctx irl in
+            let u, d, metasenv, subst, o = status#obj in
+            pp(lazy("delifting as " ^ 
+              NCicPp.ppterm ~metasenv ~subst ~context:source 
+               (NCic.Meta (0,lc))));
+            let (metasenv, subst), t =
+              NCicMetaSubst.delift 
+                 ~unify:(fun m s c t1 t2 -> 
+                   try Some (NCicUnification.unify status m s c t1 t2)
+                   with 
+                    | NCicUnification.UnificationFailure _ 
+                    | NCicUnification.Uncertain _ -> None) 
+               metasenv subst source 0 lc t
+            in
+            let status = status#set_obj (u, d, metasenv, subst, o) in
+            status, (ctx,t))
+       (status,orig) ops
  in
  pp(lazy("relocated: " ^ ppterm (fst rc) (snd rc)));
  rc
-- 
2.39.2