From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 2 Feb 2004 16:14:56 +0000 (+0000)
Subject: - removed unwind: every substitution is now _not_ unwinded
X-Git-Tag: V_0_2_3~114
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4ce27bd72e72474d4d6654898faaa5a583dd6365;p=helm.git

- removed unwind: every substitution is now _not_ unwinded
- removed extra metasenv argument from all kernel proxies
- added kernel proxy: subst (for CicSubstitution.subst)
- added pretty printer ppterm
---

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 6d8b03ddb..a28b853be 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -4,8 +4,6 @@ open Printf
 exception AssertFailure of string
 exception MetaSubstFailure of string
 
-exception RelToHiddenHypothesis (* TODO remove this exception *)
-
 let debug_print = prerr_endline
 
 type substitution = (int * Cic.term) list
@@ -41,29 +39,194 @@ 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) ->
+        (try
+          aux k (CicSubstitution.lift_meta l (List.assoc n subst))
+        with Not_found ->
+          let l' =
+            let i = ref 0 in
+            List.map
+              (function
+                | None -> None
+                | Some t ->
+                    incr i;
+                    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,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, 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 n subst context metasenv l t =
+ let l =
+  let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+  List.map2 (fun ct lt ->
+    match (ct, lt) with
+    | None, _ -> None
+    | Some _, _ -> lt)
+    canonical_context l
+ in
  let module S = CicSubstitution in
   let to_be_restricted = ref [] in
   let rec deliftaux k =
@@ -92,7 +255,7 @@ let delift n subst 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
@@ -116,8 +279,7 @@ let delift n subst context metasenv l t =
                   try
                    Some (deliftaux k t)::l1'
                   with
-                     RelToHiddenHypothesis
-                   | NotInTheList
+                     NotInTheList
                    | MetaSubstFailure _ ->
                       to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
             in
@@ -184,158 +346,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,_) = CicUtil.lookup_meta i metasenv in
-                delift i subst 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   *)
@@ -347,124 +430,78 @@ 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 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,_) ->
@@ -477,23 +514,27 @@ 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 metasenv subst n term =
-  (* TODO unwind's result is thrown away :-( *)
-  let (subst, _) = unwind_subst metasenv subst in
+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))
+    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 metasenv subst context term =
-  (* TODO unwind's result is thrown away :-( *)
-  let (subst, _) = unwind_subst metasenv subst in
+let whd subst context term =
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in
   try
@@ -502,16 +543,13 @@ let whd metasenv subst context term =
     raise (MetaSubstFailure ("Weak head reduction failure: " ^
       Printexc.to_string e))
 
-let are_convertible metasenv subst context t1 t2 =
-  (* TODO unwind's result is thrown away :-( *)
-  let (subst, _) = unwind_subst metasenv subst in
+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 =
-  (* TODO unwind's result is thrown away :-( *)
-  let (subst, _) = unwind_subst metasenv subst in
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in
   let metasenv =
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index a81f50c1d..fd770215a 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -31,13 +31,9 @@ exception MetaSubstFailure of string
 type substitution = (int * Cic.term) list
 
 val delift : 
-  int -> substitution -> Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term ->
-   Cic.term * Cic.metasenv
-
-(* unwind_subst metasenv subst                         *)
-(* unwinds [subst] w.r.t. itself.                      *)
-(* It can restrict some metavariable in the [metasenv] *)
-val unwind_subst : Cic.metasenv -> substitution -> substitution * Cic.metasenv
+  int -> substitution -> Cic.context -> Cic.metasenv ->
+  (Cic.term option) list -> Cic.term ->
+    Cic.term * Cic.metasenv * substitution
 
 (* apply_subst subst t                     *)
 (* applies the substitution [subst] to [t] *)
@@ -55,29 +51,26 @@ val apply_subst : substitution -> Cic.term -> Cic.term
 (*  during the unwinding the eta-expansions are undone.                 *)
 (* [subst] must be already unwinded                                     *)
 val apply_subst_reducing :
- substitution -> (int * int) option -> Cic.term -> Cic.term
+ (int * int) option -> substitution -> Cic.term -> Cic.term
 
 val apply_subst_context : substitution -> Cic.context -> Cic.context
 
 (** {2 Pretty printers} *)
 
 val ppcontext: ?sep: string -> substitution -> Cic.context -> string
-val ppmetasenv: ?sep: string -> substitution -> Cic.metasenv -> string
+val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string
 val ppsubst: substitution -> string
+val ppterm: substitution -> Cic.term -> string
 
 (* {2 Kernel wrappers}
  * From now on we recreate a kernel abstraction where substitutions are part of
  * the calculus *)
 
-val lift : Cic.metasenv -> substitution -> int -> Cic.term -> Cic.term
-
-val whd: Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
-
-val are_convertible:
-  Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term ->
-    bool
+val lift : substitution -> int -> Cic.term -> Cic.term
+val subst: substitution -> Cic.term -> Cic.term -> Cic.term
+val whd: substitution -> Cic.context -> Cic.term -> Cic.term
+val are_convertible: substitution -> Cic.context -> Cic.term -> Cic.term -> bool
 
 val type_of_aux':
-  Cic.metasenv -> substitution -> Cic.context -> Cic.term ->
-    Cic.term
+  Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term