X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=acb942ec5f37b9c4000a7b72c57e79a424b457eb;hb=0568c864d39f55fd2a32382bf5bc163edc0284b0;hp=f8a73f2f53b0fd4e00cfb3e73f4d832def6a2fd3;hpb=6696898978f86977863429cc3a8690d2546a918b;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index f8a73f2f5..acb942ec5 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -3,7 +3,6 @@ open Printf
 
 exception AssertFailure of string
 exception MetaSubstFailure of string
-exception RelToHiddenHypothesis
 
 let debug_print = prerr_endline
 
@@ -16,17 +15,19 @@ let ppsubst subst =
       subst)
 
 (**** DELIFT ****)
-
-(* the delift function takes in input an ordered list of optional terms       *)
-(* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with   *)
-(* rel(k). Typically, the list of optional terms is the explicit substitution *)
-(* that is applied to a metavariable occurrence and the result of the delift  *)
-(* function is a term the implicit variable can be substituted with to make   *)
-(* the term [t] unifiable with the metavariable occurrence.                   *)
-(* In general, the problem is undecidable if we consider equivalence in place *)
-(* of alpha convertibility. Our implementation, though, is even weaker than   *)
-(* alpha convertibility, since it replace the term [tk] if and only if [tk]   *)
-(* is a Rel (missing all the other cases). Does this matter in practice?      *)
+(* the delift function takes in input a metavariable index, an ordered list of
+ * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
+ * (rel(nk)) with rel(k).  Typically, the list of optional terms is the explicit
+ * substitution that is applied to a metavariable occurrence and the result of
+ * the delift function is a term the implicit variable can be substituted with
+ * to make the term [t] unifiable with the metavariable occurrence.  In general,
+ * the problem is undecidable if we consider equivalence in place of alpha
+ * convertibility. Our implementation, though, is even weaker than alpha
+ * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
+ * (missing all the other cases). Does this matter in practice?
+ * The metavariable index is the index of the metavariable that must not occur
+ * in the term (for occur check).
+ *)
 
 exception NotInTheList;;
 
@@ -38,29 +39,187 @@ let position n =
      | _::tl -> aux (k+1) tl in
   aux 1
 ;;
+
+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 ->
+prerr_endline (Printf.sprintf "RESTRINGO (%d,%d)" n !i) ;
+                   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,dest) -> C.LetIn (name, aux k so, 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)
  
-(*CSC: this restriction function is utterly wrong, since it does not check  *)
-(*CSC: that the variable that is going to be restricted does not occur free *)
-(*CSC: in a part of the sequent that is not going to be restricted.         *)
-(*CSC: In particular, the whole approach is wrong; if restriction can fail  *)
-(*CSC: (as indeed it is the case), we can not collect all the restrictions  *)
-(*CSC: and restrict everything at the end ;-(                               *)
-let restrict to_be_restricted =
-  let rec erase i n = 
-    function
-        [] -> []
-      |        _::tl when List.mem (n,i) to_be_restricted ->
-          None::(erase (i+1) n tl) 
-      | he::tl -> he::(erase (i+1) n tl) in
-  let rec aux =
-    function 
-        [] -> []
-      |        (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
-  aux
+let rec restrict subst to_be_restricted metasenv =
+  let names_of_context_indexes context indexes =
+    String.concat ", "
+      (List.map
+        (fun i ->
+          match List.nth context i with
+          | None -> assert false
+          | Some (n, _) -> CicPp.ppname n)
+        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' =
+          match ty with
+          | None ->  more_to_be_restricted, None
+          | Some 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',
+              Some 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 restrict_me = List.mem i to_be_restricted in
+        if restrict_me then
+          let more_to_be_restricted, restricted, new_tl =
+            erase (i+1) (i :: to_be_restricted) n tl
+          in
+          more_to_be_restricted, restricted, None :: new_tl
+        else
+          (try
+            let more_to_be_restricted, hd' =
+              force_does_not_occur_in_context to_be_restricted hd
+            in
+            let more_to_be_restricted', restricted, tl' =
+              erase (i+1) to_be_restricted n tl
+            in
+            more_to_be_restricted @ more_to_be_restricted',
+            restricted, hd' :: tl'
+          with Occur ->
+            let more_to_be_restricted, restricted, tl' =
+              erase (i+1) (i :: to_be_restricted) n tl
+            in
+            more_to_be_restricted, restricted, None :: tl')
+  in
+  let (more_to_be_restricted, metasenv, subst) =
+    List.fold_right
+      (fun (n, context, t) (more, metasenv, subst) ->
+        let to_be_restricted =
+          List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
+        in
+        let (more_to_be_restricted, restricted, context') =
+          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
+          (try
+            let s = List.assoc n subst in
+            try
+              let more_to_be_restricted'', s' =
+                force_does_not_occur subst restricted s
+              in
+              let subst' = (n, s') :: (List.remove_assoc n subst) in
+              let more =
+                more @ more_to_be_restricted @ more_to_be_restricted' @
+                  more_to_be_restricted''
+              in
+              (more, metasenv', subst')
+            with Occur ->
+              raise (MetaSubstFailure (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
+                (CicPp.ppterm s)))
+           with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
+        with Occur ->
+          raise (MetaSubstFailure (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 ([], [], subst)
+  in
+  match more_to_be_restricted with
+  | [] -> (metasenv, subst)
+  | _ -> restrict subst more_to_be_restricted metasenv
 ;;
 
 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
-let delift context metasenv l t =
+let delift n subst context metasenv l t =
  let module S = CicSubstitution in
   let to_be_restricted = ref [] in
   let rec deliftaux k =
@@ -89,28 +248,35 @@ let delift context metasenv l t =
                ignore (deliftaux k (S.lift m t)) ;*)
              (*CSC: end of bug commented out                           *)
              C.Rel ((position (m-k) l) + k)
-          | None -> raise RelToHiddenHypothesis)
+          | None -> raise (MetaSubstFailure "RelToHiddenHypothesis"))
      | 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 -> 
-        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
-                 RelToHiddenHypothesis
-               | NotInTheList ->
-                  to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
-        in
-         let l' = deliftl 1 l1 in
-          C.Meta(i,l')
+        if i = n then
+          raise (MetaSubstFailure (sprintf
+            "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
+            i (CicPp.ppterm t)))
+        else
+         (* I do not consider the term associated to ?i in subst since *)
+         (* in this way I can restrict if something goes wrong.        *)
+          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')
      | C.Sort _ as t -> t
      | C.Implicit as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
@@ -172,161 +338,79 @@ debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have
             (function Some t -> CicPp.ppterm t | None -> "_")
             l))))
    in
-    res, restrict !to_be_restricted metasenv
+   let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
+    res, metasenv, subst
 ;;
 
 (**** END OF DELIFT ****)
 
-let rec unwind metasenv subst unwinded t =
- let unwinded = ref unwinded in
- let frozen = ref [] in
- let rec um_aux metasenv =
+let apply_subst_gen ~appl_fun subst term =
+ let rec um_aux =
   let module C = Cic in
   let module S = CicSubstitution in 
    function
-      C.Rel _ as t -> t,metasenv
-    | C.Var _  as t -> t,metasenv
-    | C.Meta (i,l) -> 
+      C.Rel _ as t -> t
+    | C.Var _  as t -> t
+    | C.Meta (i, l) -> 
         (try
-          S.lift_meta l (List.assoc i !unwinded), metasenv
-         with Not_found ->
-           if List.mem i !frozen then
-             raise (MetaSubstFailure
-              "Failed to unify due to cyclic constraints (occur check)")
-           else
-            let saved_frozen = !frozen in 
-            frozen := i::!frozen ;
-            let res =
-             try
-              let t = List.assoc i subst in
-              let t',metasenv' = um_aux metasenv t in
-              let _,metasenv'' =
-               let (_,canonical_context,_) = 
-                List.find (function (m,_,_) -> m=i) metasenv
-               in
-                delift canonical_context metasenv' l t'
-              in
-               unwinded := (i,t')::!unwinded ;
-               S.lift_meta l t', metasenv'
-             with
-              Not_found ->
-               (* not constrained variable, i.e. free in subst*)
-               let l',metasenv' =
-                List.fold_right
-                 (fun t (tl,metasenv) ->
-                   match t with
-                      None -> None::tl,metasenv
-                    | Some t -> 
-                       let t',metasenv' = um_aux metasenv t in
-                        (Some t')::tl, metasenv'
-                 ) l ([],metasenv)
-               in
-                C.Meta (i,l'), metasenv'
-            in
-            frozen := saved_frozen ;
-            res
-        ) 
-    | C.Sort _
-    | C.Implicit as t -> t,metasenv
-    | C.Cast (te,ty) ->
-       let te',metasenv' = um_aux metasenv te in
-       let ty',metasenv'' = um_aux metasenv' ty in
-       C.Cast (te',ty'),metasenv''
-    | C.Prod (n,s,t) ->
-       let s',metasenv' = um_aux metasenv s in
-       let t',metasenv'' = um_aux metasenv' t in
-       C.Prod (n, s', t'), metasenv''
-    | C.Lambda (n,s,t) ->
-       let s',metasenv' = um_aux metasenv s in
-       let t',metasenv'' = um_aux metasenv' t in
-       C.Lambda (n, s', t'), metasenv''
-    | C.LetIn (n,s,t) ->
-       let s',metasenv' = um_aux metasenv s in
-       let t',metasenv'' = um_aux metasenv' t in
-       C.LetIn (n, s', t'), metasenv''
-    | C.Appl (he::tl) ->
-       let tl',metasenv' =
-        List.fold_right
-         (fun t (tl,metasenv) ->
-           let t',metasenv' = um_aux metasenv t in
-            t'::tl, metasenv'
-         ) tl ([],metasenv)
-       in
-        begin
-         match um_aux metasenv' he with
-            (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
-          | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
-        end
+          let t = List.assoc i subst in
+          um_aux (S.lift_meta l t)
+        with Not_found -> (* not constrained variable, i.e. free in subst*)
+          let l' =
+            List.map (function None -> None | Some t -> Some (um_aux t)) l
+          in
+           C.Meta (i,l'))
+    | C.Sort _ as t -> t
+    | C.Implicit -> assert false
+    | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
+    | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
+    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
+    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+    | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst', metasenv' =
-        List.fold_right
-         (fun (uri,t) (tl,metasenv) ->
-           let t',metasenv' = um_aux metasenv t in
-            (uri,t')::tl, metasenv'
-         ) exp_named_subst ([],metasenv)
+       let exp_named_subst' =
+         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
        in
-        C.Const (uri,exp_named_subst'),metasenv'
+       C.Const (uri, exp_named_subst')
     | C.MutInd (uri,typeno,exp_named_subst) ->
-       let exp_named_subst', metasenv' =
-        List.fold_right
-         (fun (uri,t) (tl,metasenv) ->
-           let t',metasenv' = um_aux metasenv t in
-            (uri,t')::tl, metasenv'
-         ) exp_named_subst ([],metasenv)
+       let exp_named_subst' =
+         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
        in
-        C.MutInd (uri,typeno,exp_named_subst'),metasenv'
+       C.MutInd (uri,typeno,exp_named_subst')
     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-       let exp_named_subst', metasenv' =
-        List.fold_right
-         (fun (uri,t) (tl,metasenv) ->
-           let t',metasenv' = um_aux metasenv t in
-            (uri,t')::tl, metasenv'
-         ) exp_named_subst ([],metasenv)
+       let exp_named_subst' =
+         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
        in
-        C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
+       C.MutConstruct (uri,typeno,consno,exp_named_subst')
     | C.MutCase (sp,i,outty,t,pl) ->
-       let outty',metasenv' = um_aux metasenv outty in
-       let t',metasenv'' = um_aux metasenv' t in
-       let pl',metasenv''' =
-        List.fold_right
-         (fun p (pl,metasenv) ->
-           let p',metasenv' = um_aux metasenv p in
-            p'::pl, metasenv'
-         ) pl ([],metasenv'')
-       in
-        C.MutCase (sp, i, outty', t', pl'),metasenv'''
+       let pl' = List.map um_aux pl in
+       C.MutCase (sp, i, um_aux outty, um_aux t, pl')
     | C.Fix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl,metasenv' =
-        List.fold_right
-         (fun (name, i, ty, bo) (fl,metasenv) ->
-           let ty',metasenv' = um_aux metasenv ty in
-           let bo',metasenv'' = um_aux metasenv' bo in
-            (name, i, ty', bo')::fl,metasenv''
-         ) fl ([],metasenv)
+       let fl' =
+         List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
        in
-        C.Fix (i, liftedfl),metasenv'
+       C.Fix (i, fl')
     | C.CoFix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl,metasenv' =
-        List.fold_right
-         (fun (name, ty, bo) (fl,metasenv) ->
-           let ty',metasenv' = um_aux metasenv ty in
-           let bo',metasenv'' = um_aux metasenv' bo in
-            (name, ty', bo')::fl,metasenv''
-         ) fl ([],metasenv)
+       let fl' =
+         List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
        in
-        C.CoFix (i, liftedfl),metasenv'
+       C.CoFix (i, fl')
  in
-  let t',metasenv' = um_aux metasenv t in
-   t',metasenv',!unwinded 
+ um_aux term
 
-let apply_subst subst t = 
- (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
- let metasenv = [] in
-  let (t',_,_) = unwind metasenv [] subst t in
-   t'
+let apply_subst =
+  let appl_fun um_aux he tl =
+    let tl' = List.map um_aux tl in
+      begin
+       match um_aux he with
+          Cic.Appl l -> Cic.Appl (l@tl')
+        | he' -> Cic.Appl (he'::tl')
+      end
+  in
+  apply_subst_gen ~appl_fun
+
+let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
 (* performs as (apply_subst subst t) until it finds an application of   *)
@@ -338,130 +422,90 @@ let apply_subst subst t =
 (*  application has been unified with (META [meta_to_reduce]):          *)
 (*  during the unwinding the eta-expansions are undone.                 *)
 
-let rec apply_subst_context subst =
-    List.map (function
-      | Some (n, Cic.Decl t) -> Some (n, Cic.Decl (apply_subst subst t))
+let apply_subst_reducing meta_to_reduce =
+  let appl_fun um_aux he tl =
+    let tl' = List.map um_aux tl in
+    let t' =
+     match um_aux he with
+        Cic.Appl l -> Cic.Appl (l@tl')
+      | he' -> Cic.Appl (he'::tl')
+    in
+     begin
+      match meta_to_reduce, he with
+         Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr ->
+          let rec beta_reduce =
+           function
+              (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
+                let he'' = CicSubstitution.subst he' t in
+                 if tl' = [] then
+                  he''
+                 else
+                  beta_reduce (n-1,Cic.Appl(he''::tl'))
+            | (_,t) -> t
+          in
+           beta_reduce (reductions_no,t')
+       | _,_ -> t'
+     end
+  in
+  apply_subst_gen ~appl_fun
+
+let rec apply_subst_context subst context =
+  List.fold_right
+    (fun item context ->
+      match item with
+      | Some (n, Cic.Decl t) ->
+          let t' = apply_subst subst t in
+          Some (n, Cic.Decl t') :: context
       | Some (n, Cic.Def (t, ty)) ->
           let ty' =
             match ty with
             | None -> None
             | Some ty -> Some (apply_subst subst ty)
           in
-          Some (n, Cic.Def (apply_subst subst t, ty'))
-      | None -> None)
+          let t' = apply_subst subst t in
+          Some (n, Cic.Def (t', ty')) :: context
+      | None -> None :: context)
+    context []
 
-let rec apply_subst_reducing subst meta_to_reduce t =
- let rec um_aux =
-  let module C = Cic in
-  let module S = CicSubstitution in 
-   function
-      C.Rel _
-    | C.Var _  as t -> t
-    | C.Meta (i,l) as t ->
-       (try
-         S.lift_meta l (List.assoc i subst)
-        with Not_found ->
-          C.Meta (i,l))
-    | C.Sort _ as t -> t
-    | C.Implicit as t -> t
-    | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
-    | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
-    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
-    | C.Appl (he::tl) ->
-       let tl' = List.map um_aux tl in
-        let t' =
-         match um_aux he with
-            C.Appl l -> C.Appl (l@tl')
-          | _ as he' -> C.Appl (he'::tl')
-        in
-         begin
-          match meta_to_reduce,he with
-             Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
-              let rec beta_reduce =
-               function
-                  (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
-                    let he'' = CicSubstitution.subst he' t in
-                     if tl' = [] then
-                      he''
-                     else
-                      beta_reduce (n-1,C.Appl(he''::tl'))
-                | (_,t) -> t
-              in
-               beta_reduce (reductions_no,t')
-           | _,_ -> t'
-         end
-    | C.Appl _ -> assert false
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> (uri,um_aux 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,um_aux 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,um_aux t)) exp_named_subst
-       in
-        C.MutConstruct (uri,typeno,consno,exp_named_subst')
-    | C.MutCase (sp,i,outty,t,pl) ->
-       C.MutCase (sp, i, um_aux outty, um_aux t,
-        List.map um_aux pl)
-    | C.Fix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl =
-        List.map
-         (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux 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, um_aux ty, um_aux bo))
-          fl
-       in
-        C.CoFix (i, liftedfl)
- in
-   um_aux t
+let apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, apply_subst_context subst context, apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+      metasenv)
+
+let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
 let ppcontext ?(sep = "\n") subst context =
   String.concat sep
     (List.rev_map (function
       | Some (n, Cic.Decl t) ->
-          sprintf "%s : %s"
-            (CicPp.ppname n) (CicPp.ppterm (apply_subst subst t))
+          sprintf "%s : %s" (CicPp.ppname n) (ppterm subst t)
       | Some (n, Cic.Def (t, ty)) ->
           sprintf "%s : %s := %s"
             (CicPp.ppname n)
-            (match ty with
-            | None -> "_"
-            | Some ty -> CicPp.ppterm (apply_subst subst ty))
-            (CicPp.ppterm (apply_subst subst t))
+            (match ty with None -> "_" | Some ty -> ppterm subst ty)
+            (ppterm subst t)
       | None -> "_")
       context)
 
-let ppmetasenv ?(sep = "\n") subst metasenv =
+let ppmetasenv ?(sep = "\n") metasenv subst =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
         sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
-          (CicPp.ppterm (apply_subst subst t)))
+          (ppterm subst t))
       (List.filter
         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
         metasenv))
 
 (* UNWIND THE MGU INSIDE THE MGU *)
+(*
 let unwind_subst metasenv subst =
   List.fold_left
    (fun (unwinded,metasenv) (i,_) ->
-     let (_,canonical_context,_) =
-       List.find (function (m,_,_) -> m=i) metasenv
-     in
+     let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
      let identity_relocation_list =
       CicMkImplicit.identity_relocation_list_for_metavariable canonical_context
      in
@@ -470,10 +514,26 @@ let unwind_subst metasenv subst =
       in
        subst',metasenv'
    ) ([],metasenv) subst
+*)
 
 (* From now on we recreate a kernel abstraction where substitutions are part of
  * the calculus *)
 
+let lift subst n term =
+  let term = apply_subst subst term in
+  try
+    CicSubstitution.lift n term
+  with e ->
+    raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
+
+let subst subst t1 t2 =
+  let t1 = apply_subst subst t1 in
+  let t2 = apply_subst subst t2 in
+  try
+    CicSubstitution.subst t1 t2
+  with e ->
+    raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
+
 let whd subst context term =
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in
@@ -485,7 +545,8 @@ let whd subst context term =
 
 let are_convertible subst context t1 t2 =
   let context = apply_subst_context subst context in
-  let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in
+  let t1 = apply_subst subst t1 in
+  let t2 = apply_subst subst t2 in
   CicReduction.are_convertible context t1 t2
 
 let type_of_aux' metasenv subst context term =