X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=188d4dc207ff4bf8e4f47d4bf28d8407b12be214;hb=b0b6b600e029435bfce53f41cd267c669a1f8dc2;hp=57a1b7be7a8557cdd25e6cc1873597980f6ce322;hpb=27bce1d83422883b6415862ec92e75baf4f87186;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 57a1b7be7..188d4dc20 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -145,380 +145,194 @@ let tempi_subst = ref 0.0;;
 let tempi_type_of_aux = ref 0.0;;
 *)
 
+let newmeta = 
+  let maxmeta = ref 0 in
+  fun () -> incr maxmeta; !maxmeta
+;;
 
 exception NotInTheList;;
 
 let position n (shift, lc) =
   match lc with
   | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
-  | NCic.Itl len -> n - shift
+  | NCic.Irl _ -> n - shift
   | NCic.Ctx tl ->
       let rec aux k = function 
          | [] -> raise NotInTheList
-         | (Cic.Rel m)::_ when m + shift = n -> k
+         | (NCic.Rel m)::_ when m + shift = n -> k
          | _::tl -> aux (k+1) tl 
       in
        aux 1 tl
 ;;
-(*
-exception Occur;;
 
-let rec force_does_not_occur subst to_be_restricted t =
- let module C = Cic in
- let more_to_be_restricted = ref [] in
- let rec aux k = function
-      C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
-    | C.Rel _
-    | C.Sort _ as t -> t
-    | C.Implicit _ -> assert false
-    | C.Meta (n, l) ->
-       (* we do not retrieve the term associated to ?n in subst since *)
-       (* in this way we can restrict if something goes wrong         *)
-       let l' =
-         let i = ref 0 in
-         List.map
-           (function t ->
-             incr i ;
-             match t with
-                None -> None
-              | Some t ->
-                 try
-                   Some (aux k t)
-                 with Occur ->
-                   more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
-                   None)
-           l
-       in
-        C.Meta (n, l')
-    | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
-    | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
-    | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
-    | C.LetIn (name,so,ty,dest) ->
-       C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
-    | C.Appl l -> C.Appl (List.map (aux k) l)
-    | C.Var (uri,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
-        in
-        C.Var (uri, exp_named_subst')
-    | C.Const (uri, exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
-        in
-        C.Const (uri, exp_named_subst')
-    | C.MutInd (uri,tyno,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
-        in
-        C.MutInd (uri, tyno, exp_named_subst')
-    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
-        in
-        C.MutConstruct (uri, tyno, consno, exp_named_subst')
-    | C.MutCase (uri,tyno,out,te,pl) ->
-        C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl)
-    | C.Fix (i,fl) ->
-       let len = List.length fl in
-       let k_plus_len = k + len in
-       let fl' =
-         List.map
-          (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl
-       in
-       C.Fix (i, fl')
-    | C.CoFix (i,fl) ->
-       let len = List.length fl in
-       let k_plus_len = k + len in
-       let fl' =
-         List.map
-          (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl
-       in
-       C.CoFix (i, fl')
- in
- let res = aux 0 t in
- (!more_to_be_restricted, res)
- 
-let rec restrict subst to_be_restricted metasenv =
- match to_be_restricted with
- | [] -> metasenv, subst
- | _ ->
-  let names_of_context_indexes context indexes =
-    String.concat ", "
-      (List.map
-        (fun i ->
-          try
-           match List.nth context (i-1) with
-           | None -> assert false
-           | Some (n, _) -> CicPp.ppname n
-          with
-           Failure _ -> assert false
-        ) indexes)
-  in
-  let force_does_not_occur_in_context to_be_restricted = function
-    | None -> [], None
-    | Some (name, Cic.Decl t) ->
-        let (more_to_be_restricted, t') =
-          force_does_not_occur subst to_be_restricted t
-        in
-        more_to_be_restricted, Some (name, Cic.Decl t')
-    | Some (name, Cic.Def (bo, ty)) ->
-        let (more_to_be_restricted, bo') =
-          force_does_not_occur subst to_be_restricted bo
-        in
-        let more_to_be_restricted, ty' =
-         let more_to_be_restricted', ty' =
-           force_does_not_occur subst to_be_restricted ty
-         in
-         more_to_be_restricted @ more_to_be_restricted',
-         ty'
-        in
-        more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
-  in
-  let rec erase i to_be_restricted n = function
-    | [] -> [], to_be_restricted, []
-    | hd::tl ->
-        let more_to_be_restricted,restricted,tl' =
-          erase (i+1) to_be_restricted n tl
-        in
-        let restrict_me = List.mem i restricted in
-        if restrict_me then
-          more_to_be_restricted, restricted, None:: tl'
-        else
-          (try
-            let more_to_be_restricted', hd' =
-              let delifted_restricted =
-               let rec aux =
-                function
-                   [] -> []
-                 | j::tl when j > i -> (j - i)::aux tl
-                 | _::tl -> aux tl
-               in
-                aux restricted
-              in
-               force_does_not_occur_in_context delifted_restricted hd
-            in
-             more_to_be_restricted @ more_to_be_restricted',
-             restricted, hd' :: tl'
-          with Occur ->
-            more_to_be_restricted, (i :: restricted), None :: tl')
-  in
-  let (more_to_be_restricted, metasenv) =  (* restrict metasenv *)
-    List.fold_right
-      (fun (n, context, t) (more, metasenv) ->
-        let to_be_restricted =
-          List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
-        in
-        let (more_to_be_restricted, restricted, context') =
-         (* just an optimization *)
-         if to_be_restricted = [] then
-          [],[],context
-         else
-          erase 1 to_be_restricted n context
-        in
-        try
-          let more_to_be_restricted', t' =
-            force_does_not_occur subst restricted t
-          in
-          let metasenv' = (n, context', t') :: metasenv in
-          (more @ more_to_be_restricted @ more_to_be_restricted',
-          metasenv')
-        with Occur ->
-          raise (MetaSubstFailure (lazy (sprintf
-            "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
-	    n (names_of_context_indexes context to_be_restricted)))))
-      metasenv ([], [])
+let pack_lc orig = 
+  let rec are_contiguous k = function
+    | [] -> true
+    | (NCic.Rel j) :: tl when j = k+1 -> are_contiguous j tl
+    | _ -> false
   in
-  let (more_to_be_restricted', subst) = (* restrict subst *)
-    List.fold_right
-      (* TODO: cambiare dopo l'aggiunta del ty *)
-      (fun (n, (context, term,ty)) (more, subst') ->
-        let to_be_restricted =
-          List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
-        in
-        (try
-          let (more_to_be_restricted, restricted, context') =
-           (* just an optimization *)
-            if to_be_restricted = [] then
-              [], [], context
-            else
-              erase 1 to_be_restricted n context
-          in
-          let more_to_be_restricted', term' =
-            force_does_not_occur subst restricted term
-          in
-          let more_to_be_restricted'', ty' =
-            force_does_not_occur subst restricted ty in
-          let subst' = (n, (context', term',ty')) :: subst' in
-          let more = 
-	    more @ more_to_be_restricted 
-	    @ more_to_be_restricted'@more_to_be_restricted'' in
-          (more, subst')
-        with Occur ->
-          let error_msg = lazy (sprintf
-            "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
-            n (names_of_context_indexes context to_be_restricted) n
-            (ppterm ~metasenv subst term))
-	  in 
-          (* DEBUG
-          debug_print (lazy error_msg);
-          debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
-          debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
-          debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
-          raise (MetaSubstFailure error_msg))) 
-      subst ([], []) 
-  in
-   restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
+  match orig with
+  | _, NCic.Ctx [] -> 0, NCic.Irl 0
+  | shift, NCic.Ctx (NCic.Rel k::tl as l) when are_contiguous k tl ->
+      shift+k-1, NCic.Irl (List.length l)
+  | _ -> orig
 ;;
-*)
 
-let newmeta = 
-  let maxmeta = ref 0 in
-  fun () -> incr maxmeta; !maxmeta
+let mk_restricted_irl shift len restrictions =
+  let rec aux n =
+    if n = 0 then [] else
+      if List.mem (n+shift) restrictions then aux (n-1)
+      else (NCic.Rel n)::aux (n-1)
+  in
+    pack_lc (shift, NCic.Ctx (List.rev (aux len)))
 ;;
 
-let restrict metasenv subst i to_be_restricted =
-  let force_does_not_occur_in_context to_be_restricted = function
-    | None -> [], None
-    | Some (name, Cic.Decl t) ->
-        let (more_to_be_restricted, t') =
-          force_does_not_occur subst to_be_restricted t
-        in
-        more_to_be_restricted, Some (name, Cic.Decl t')
-    | Some (name, Cic.Def (bo, ty)) ->
-        let (more_to_be_restricted, bo') =
-          force_does_not_occur subst to_be_restricted bo
-        in
-        let more_to_be_restricted, ty' =
-         let more_to_be_restricted', ty' =
-           force_does_not_occur subst to_be_restricted ty
-         in
-         more_to_be_restricted @ more_to_be_restricted',
-         ty'
-        in
-        more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
-  in
-  let rec erase i to_be_restricted n = function
-    | [] -> [], to_be_restricted, []
-    | hd::tl ->
-        let more_to_be_restricted,restricted,tl' =
-          erase (i+1) to_be_restricted n tl
-        in
-        let restrict_me = List.mem i restricted in
-        if restrict_me then
-          more_to_be_restricted, restricted, None:: tl'
-        else
-          (try
-            let more_to_be_restricted', hd' =
-              let delifted_restricted =
-               let rec aux =
-                function
-                   [] -> []
-                 | j::tl when j > i -> (j - i)::aux tl
-                 | _::tl -> aux tl
-               in
-                aux restricted
-              in
-               force_does_not_occur_in_context delifted_restricted hd
+exception Occur;;
+
+let rec force_does_not_occur metasenv subst restrictions t =
+ let rec aux k ms = function
+    | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur
+    | NCic.Meta (n, l) as orig ->
+       (* we ignore the subst since restrict will take care of already
+        * instantiated/restricted metavariabels *)
+       let (metasenv,subst as ms), restrictions_for_n, l' =
+         match l with
+         | shift, NCic.Irl len -> 
+             let restrictions = 
+               List.filter 
+                (fun i -> i > shift && i <= shift + len) restrictions in
+             ms, restrictions, mk_restricted_irl shift len restrictions
+         | shift, NCic.Ctx l ->
+            let ms, _, restrictions_for_n, l =
+             List.fold_right
+               (fun t (ms, i, restrictions_for_n, l) ->
+                 try 
+                   let ms, t = aux (k-shift) ms t in
+                   ms, i-1, restrictions_for_n, t::l
+                 with Occur ->
+                   ms, i-1, i::restrictions_for_n, l)
+               l (ms, List.length l, [], [])
             in
-             more_to_be_restricted @ more_to_be_restricted',
-             restricted, hd' :: tl'
-          with Occur ->
-            more_to_be_restricted, (i :: restricted), None :: tl')
-  in
-  let (more_to_be_restricted, metasenv) =  (* restrict metasenv *)
-    List.fold_right
-      (fun (n, context, t) (more, metasenv) ->
-        let to_be_restricted =
-          List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
-        in
-        let (more_to_be_restricted, restricted, context') =
-         (* just an optimization *)
-         if to_be_restricted = [] then
-          [],[],context
-         else
-          erase 1 to_be_restricted n context
-        in
+             ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
+       in
+       if restrictions_for_n = [] then
+         ms, if l = l' then orig else NCic.Meta (n, l')
+       else
+         let metasenv, subst, newmeta = 
+           restrict metasenv subst n restrictions_for_n 
+         in
+           (metasenv, subst), NCic.Meta (newmeta, l')
+    | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
+ in
+   aux 0 (metasenv,subst) t 
+
+and force_does_not_occur_in_context metasenv subst restrictions = function
+  | name, NCic.Decl t as orig ->
+      let (metasenv, subst), t' =
+        force_does_not_occur metasenv subst restrictions t in
+      metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
+  | name, NCic.Def (bo, ty) as orig ->
+      let (metasenv, subst), bo' =
+        force_does_not_occur metasenv subst restrictions bo in
+      let (metasenv, subst), ty' =
+        force_does_not_occur metasenv subst restrictions ty in
+      metasenv, subst, 
+       (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty')))
+
+and erase_in_context metasenv subst pos restrictions = function
+  | [] -> metasenv, subst, restrictions, []
+  | hd::tl as orig ->
+      let metasenv, subst, restricted, tl' = 
+        erase_in_context metasenv subst (pos+1) restrictions tl in
+      if List.mem pos restricted then
+        metasenv, subst, restricted, tl'
+      else
         try
-          let more_to_be_restricted', t' =
-            force_does_not_occur subst restricted t
+          let metasenv, subst, hd' =
+            let delifted_restricted = 
+              List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in
+            force_does_not_occur_in_context 
+              metasenv subst delifted_restricted hd
           in
-          let metasenv' = (n, context', t') :: metasenv in
-          (more @ more_to_be_restricted @ more_to_be_restricted',
-          metasenv')
+           metasenv, subst, restricted, 
+            (if hd' == hd && tl' == tl then orig else (hd' :: tl'))
         with Occur ->
-          raise (MetaSubstFailure (lazy (sprintf
-            "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
-	    n (names_of_context_indexes context to_be_restricted)))))
-      metasenv ([], [])
-  in
-  let (more_to_be_restricted', subst) = (* restrict subst *)
-    List.fold_right
-      (* TODO: cambiare dopo l'aggiunta del ty *)
-      (fun (n, (context, term,ty)) (more, subst') ->
-        let to_be_restricted =
-          List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
-        in
-        (try
-          let (more_to_be_restricted, restricted, context') =
-           (* just an optimization *)
-            if to_be_restricted = [] then
-              [], [], context
-            else
-              erase 1 to_be_restricted n context
-          in
-          let more_to_be_restricted', term' =
-            force_does_not_occur subst restricted term
-          in
-          let more_to_be_restricted'', ty' =
-            force_does_not_occur subst restricted ty in
-          let subst' = (n, (context', term',ty')) :: subst' in
-          let more = 
-	    more @ more_to_be_restricted 
-	    @ more_to_be_restricted'@more_to_be_restricted'' in
-          (more, subst')
-        with Occur ->
-          let error_msg = lazy (sprintf
-            "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
-            n (names_of_context_indexes context to_be_restricted) n
-            (ppterm ~metasenv subst term))
-	  in 
-          (* DEBUG
-          debug_print (lazy error_msg);
-          debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
-          debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
-          debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
-          raise (MetaSubstFailure error_msg))) 
-      subst ([], []) 
-  in
-   restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
+            metasenv, subst, (pos :: restricted), tl'
+
+and restrict metasenv subst i restrictions =
+  assert (restrictions <> []);
+  try 
+    let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
+      try 
+        let metasenv, subst, restrictions, newctx = 
+          erase_in_context metasenv subst 1 restrictions ctx in
+        let (metasenv, subst), newty =  
+          force_does_not_occur metasenv subst restrictions ty in
+        let (metasenv, subst), newbo =  
+          force_does_not_occur metasenv subst restrictions bo in
+        let j = newmeta () in
+        let subst_entry_j = j, (name, newctx, newty, newbo) in
+        let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in
+        let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
+        metasenv,
+        subst_entry_j :: List.map 
+          (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst,
+        j
+      with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
+            ("Cannot restrict the context of the metavariable ?%d over "^^
+            "the hypotheses %s since ?%d is already instantiated "^^
+            "with %s and at least one of the hypotheses occurs in "^^
+            "the substituted term") i  (String.concat ", " 
+            (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
+            (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo))))
+  with NCicUtils.Subst_not_found _ -> 
+    try 
+      let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
+      try
+        let metasenv, subst, restrictions, newctx = 
+          erase_in_context metasenv subst 1 restrictions ctx in
+        let (metasenv, subst), newty =  
+          force_does_not_occur metasenv subst restrictions ty in
+        let j = newmeta () in
+        let metasenv_entry = j, (name, newctx, newty) in
+        let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in
+        let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
+        List.map 
+          (fun (n,_) as orig -> if i = n then metasenv_entry else orig) 
+          metasenv,
+        subst_entry :: subst, j
+      with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
+          ("Cannot restrict the context of the metavariable ?%d "^^
+          "over the hypotheses %s since metavariable's type depends "^^
+          "on at least one of them") i (String.concat ", " 
+          (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)))))
+    with 
+    | NCicUtils.Meta_not_found _ -> assert false
 ;;
-*)
-;; 
 
 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
    otherwise the occur check does not make sense in case of unification
    of ?n with ?n *)
 let delift metasenv subst context n l t =
-  let to_be_restricted = ref [] in
-  let rec aux k = function
-    | NCic.Rel n as t when n <= k -> t
+  let rec aux k (metasenv, subst as ms) = function
+    | NCic.Rel n as t when n <= k -> ms, t
     | NCic.Rel n -> 
         (try
           match List.nth context (n-k-1) with
           | _,NCic.Def (bo,_) -> 
-                (try C.Rel ((position (n-k) l) + k)
+                (try ms, NCic.Rel ((position (n-k) l) + k)
                  with NotInTheList ->
                 (* CSC: This bit of reduction hurts performances since it is
                  * possible to  have an exponential explosion of the size of the
                  * proof. required for nat/nth_prime.ma *)
-                  aux k (NCicSubstitution.lift n bo))
-          | _,NCic.Decl _ -> NCic.Rel ((position (n-k) l) + k)
+                  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 (i,l1) as orig ->
         (try
-           let _,_,t,_ = NCicUtil.lookup_subst i subst in
-           aux k (NCicSubstitution.subst_meta l1 t)
-         with NCicUtil.Subst_not_found _ ->
+           let _,_,t,_ = NCicUtils.lookup_subst i subst in
+           aux k ms (NCicSubstitution.subst_meta l1 t)
+         with NCicUtils.Subst_not_found _ ->
            (* see the top level invariant *)
            if (i = n) then 
             raise (MetaSubstFailure (lazy (Printf.sprintf (
@@ -532,183 +346,68 @@ let delift metasenv subst context n l t =
               match lc, lc1 with
               | NCic.Irl len, NCic.Irl len1 
                 when shift1 < shift || len1 + shift1 > len + shift ->
-                  (* new meta with shortened l1
-                    (1 -> shift - shift1 /\ shift + len + 1 -> shift1+len1)
-                  subst += (i,new meta)
-                  restrict checks (deleted entry cannot occur in the type...)
-                  return that meta *)
-                  assert false
-              | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig
-              | NCic.Irl len, NCic.Irl len1 ->
-                   NCic.Meta (i, (shift1 - shift, lc1))
+                  let restrictions = 
+                     HExtlib.list_seq 1 (shift - shift1) @
+                     HExtlib.list_seq (shift+len+1) (shift1+len1)
+                  in
+                  let metasenv, subst, newmeta = 
+                     restrict metasenv subst i restrictions 
+                  in
+                  (metasenv, subst), 
+                  NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions)
+              | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
+              | NCic.Irl _, NCic.Irl _ ->
+                   ms, NCic.Meta (i, (shift1 - shift, lc1))
               | _ -> 
                   let lc1 = NCicUtils.expand_local_context lc1 in
-                  let rec deliftl j = function
-                    | [] -> []
+                  let rec deliftl tbr j ms = function
+                    | [] -> ms, tbr, []
                     | t::tl ->
-                        let tl = deliftl (j+1) tl in
-                        try (aux (k+shift1) t)::tl
+                        let ms, tbr, tl = deliftl tbr (j+1) ms tl in
+                        try 
+                          let ms, t = aux (k-shift1) ms t in 
+                          ms, tbr, t::tl
                         with
-                        | NotInTheList | MetaSubstFailure _ ->
-                            to_be_restricted := (i,j)::!to_be_restricted; 
-                            tl
+                        | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
                   in
-                  let l1 = deliftl 1 l1 in
-                  C.Meta(i,l1)) (* or another ?k and possibly compress l1 *)
-    | t -> NCicUtils.map (fun _ k -> k+1) k aux t
-  in
-  let t = aux 0 t in
-  let metasenv, subst = restrict subst !to_be_restricted metasenv in
-  metasenv, subst, t
-;;
-
-
-  let to_be_restricted = ref [] in
-  let rec deliftaux k =
-   let module C = Cic in
-    function
-     | C.Rel m as t-> 
-         if m <=k then
-          t
-         else
-           (try
-            match List.nth context (m-k-1) with
-               Some (_,C.Def (t,_)) ->
-                (try
-                  C.Rel ((position (m-k) l) + k)
-                 with
-                  NotInTheList ->
-                (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
-                (*CSC: first order unification. Does it help or does it harm? *)
-                (*CSC: ANSWER: it hurts performances since it is possible to  *)
-                (*CSC: have an exponential explosion of the size of the proof.*)
-                (*CSC: However, without this bit of reduction some "apply" in *)
-                (*CSC: the library fail (e.g. nat/nth_prime.ma).              *)
-                  deliftaux k (S.lift m t))
-             | Some (_,C.Decl t) ->
-                C.Rel ((position (m-k) l) + k)
-             | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
-           with
-            Failure _ -> 
-             raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
-          )
-     | C.Var (uri,exp_named_subst) ->
-        let exp_named_subst' =
-         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
-        in
-         C.Var (uri,exp_named_subst')
-     | C.Meta (i, l1) as t -> 
-         (try
-           let (_,t,_) = CicUtil.lookup_subst i subst in
-             deliftaux k (CicSubstitution.subst_meta l1 t)
-         with CicUtil.Subst_not_found _ ->
-           (* see the top level invariant *)
-           if (i = n) then 
-            raise (MetaSubstFailure (lazy (sprintf
-              "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
-              i (ppterm ~metasenv subst t))))
-          else
-            begin
-              let rec deliftl j =
-                function
-                    [] -> []
-                  | None::tl -> None::(deliftl (j+1) tl)
-                  | (Some t)::tl ->
-                      let l1' = (deliftl (j+1) tl) in
-                        try
-                          Some (deliftaux k t)::l1'
-                        with
-                            NotInTheList
-                          | MetaSubstFailure _ ->
-                              to_be_restricted := 
-                              (i,j)::!to_be_restricted ; None::l1'
-              in
-              let l' = deliftl 1 l1 in
-                C.Meta(i,l')
-            end)
-     | C.Sort _ as t -> t
-     | C.Implicit _ as t -> t
-     | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
-     | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
-     | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
-     | C.LetIn (n,s,ty,t) ->
-        C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
-     | C.Appl l -> C.Appl (List.map (deliftaux k) l)
-     | C.Const (uri,exp_named_subst) ->
-        let exp_named_subst' =
-         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
-        in
-         C.Const (uri,exp_named_subst')
-     | C.MutInd (uri,typeno,exp_named_subst) ->
-        let exp_named_subst' =
-         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
-        in
-         C.MutInd (uri,typeno,exp_named_subst')
-     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-        let exp_named_subst' =
-         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
-        in
-         C.MutConstruct (uri,typeno,consno,exp_named_subst')
-     | C.MutCase (sp,i,outty,t,pl) ->
-        C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
-         List.map (deliftaux k) pl)
-     | C.Fix (i, fl) ->
-        let len = List.length fl in
-        let liftedfl =
-         List.map
-          (fun (name, i, ty, bo) ->
-           (name, i, deliftaux k ty, deliftaux (k+len) bo))
-           fl
-        in
-         C.Fix (i, liftedfl)
-     | C.CoFix (i, fl) ->
-        let len = List.length fl in
-        let liftedfl =
-         List.map
-          (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
-           fl
-        in
-         C.CoFix (i, liftedfl)
+                  let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in
+                  let l1 = pack_lc (shift, NCic.Ctx lc1') in
+                  if to_be_r = [] then
+                    (metasenv, subst), 
+                    (if lc1' = lc1 then orig else NCic.Meta (i,l1))
+                  else
+                    let metasenv, subst, newmeta = 
+                      restrict metasenv subst i to_be_r in
+                    (metasenv, subst), NCic.Meta(newmeta,l1))
+    | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
   in
-   let res =
-    try
-     deliftaux 0 t
-    with
-     NotInTheList ->
+   try aux 0 (metasenv,subst) t
+   with NotInTheList ->
       (* This is the case where we fail even first order unification. *)
       (* The reason is that our delift function is weaker than first  *)
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
-(* debug_print (lazy "First Order UnificationFailure during delift") ;
-debug_print(lazy (sprintf
-        "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
-        (ppterm subst t)
-        (String.concat "; "
-          (List.map
-            (function Some t -> ppterm subst t | None -> "_") l
-          )))); *)
-      let msg = (lazy (sprintf
-        "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
-        (ppterm ~metasenv subst t)
-        (String.concat "; "
-          (List.map
-            (function Some t -> ppterm ~metasenv subst t | None -> "_")
-            l))))
+      let msg = (lazy (Printf.sprintf
+        ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^
+        "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst
+        ~context 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))))))
       in
+      let shift, lc = l in
+      let lc = NCicUtils.expand_local_context lc in
+      let l = List.map (NCicSubstitution.lift shift) lc in
        if
          List.exists
-          (function
-              Some t -> CicUtil.is_meta_closed (apply_subst subst t)
-            | None -> true) l
+          (fun t -> NCicUntrusted.metas_of_term subst context t = [])
+            l
        then
         raise (Uncertain msg)
        else
         raise (MetaSubstFailure msg)
-   in
-   let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
-    res, metasenv, subst
 ;;
 
+(*
 (* delifts a term t of n levels strating from k, that is changes (Rel m)
  * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
  *)
@@ -846,5 +545,32 @@ let delift_rels_from subst metasenv k n =
 
 let delift_rels subst metasenv n t =
   delift_rels_from subst metasenv 1 n t
- 
+*) 
+
+let mk_meta ?name metasenv context ty = 
+  let n = newmeta () in
+  let len = List.length context in
+  let menv_entry = (n, (name, context, ty)) in
+  menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len))
+;;
 
+let saturate ?(delta=0) metasenv context ty goal_arity =
+ assert (goal_arity >= 0);
+  let rec aux metasenv = function
+   | NCic.Prod (name,s,t) ->
+       let metasenv1, arg = mk_meta ~name:name metasenv context s in            
+       let t, metasenv1, args, pno = 
+           aux metasenv1 (NCicSubstitution.subst arg t) 
+       in
+       if pno + 1 = goal_arity then
+         ty, metasenv, [], goal_arity+1
+       else
+         t, metasenv1, arg::args, pno+1
+   | ty ->
+        match NCicReduction.whd context ty ~delta with
+        | NCic.Prod _ as ty -> aux metasenv ty
+        | ty -> ty, metasenv, [], 0
+  in
+  let res, newmetasenv, arguments, _ = aux metasenv ty in
+  res, newmetasenv, arguments
+;;