From 0771f484b17fbe61f17c03288cfdc1124698f161 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 28 Sep 2009 14:38:54 +0000
Subject: [PATCH] 2 lift related bugs fixed!

---
 .../components/ng_refiner/nCicMetaSubst.ml    | 24 +++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 60abe85c3..52d2e4594 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -227,7 +227,10 @@ let rec flexible_arg context subst = function
                  (NCicSubstitution.lift i bo)
          | _ -> false
       with 
-      | Failure _ -> assert false
+      | Failure _ -> 
+          prerr_endline (Printf.sprintf "Rel %d inside context:\n%s" i  
+            (NCicPp.ppcontext ~subst ~metasenv:[] context));
+          assert false
       | Invalid_argument _ -> assert false)
   | _ -> false
 ;;
@@ -276,11 +279,15 @@ let delift ~unify metasenv subst context n l t =
     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
        if flexible_arg context subst t || contains_in_scope subst t then None else
-         let lb = List.map (fun t -> t, flexible_arg context subst t) l in
+         let lb = 
+           List.map (fun t -> 
+            let t = NCicSubstitution.lift (k+shift) t in
+            t, flexible_arg context subst t) 
+           l 
+         in
          HExtlib.list_findopt
           (fun (li,flexible) i ->
             if flexible || i < in_scope then None else
-             let li = NCicSubstitution.lift (k+shift) li in
              match unify metasenv subst context li t with
              | Some (metasenv,subst) -> 
                  Some ((metasenv, subst), NCic.Rel (i+1+k))
@@ -295,7 +302,7 @@ let delift ~unify metasenv subst context n l t =
     | NCic.Rel n as t when n <= k -> ms, t
     | NCic.Rel n -> 
         (try
-          match List.nth context (n-k-1) with
+          match List.nth context (n-1) with
           | _,NCic.Def (bo,_) -> 
                 (try ms, NCic.Rel ((position in_scope (n-k) l) + k)
                  with NotInTheList ->
@@ -422,6 +429,15 @@ let delift ~unify metasenv subst context n l t =
         NCicUntrusted.map_term_fold_a 
           (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
   in
+(*
+  prerr_endline (
+    "DELIFTO " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^
+    String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) ( 
+      let shift, lc = l in
+      (List.map (NCicSubstitution.lift shift) 
+        (NCicUtils.expand_local_context lc))
+  )));
+*)
    try aux (context,0,0) (metasenv,subst) t
    with NotInTheList ->
       (* This is the case where we fail even first order unification. *)
-- 
2.39.2