X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=718951c68a579756e4c4bd1d0994c835d28e2bac;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b594e009ecd08be7e3a627900ea206094acd1855;hpb=cf5d6fab96c47ccb7d623d72742717d9b08bae7b;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index b594e009e..718951c68 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -25,8 +25,9 @@
 
 open Printf
 
-(*  (* PROFILING *)
-let apply_subst_counter = ref 0
+(* PROFILING *)
+(*
+let deref_counter = ref 0
 let apply_subst_context_counter = ref 0
 let apply_subst_metasenv_counter = ref 0
 let lift_counter = ref 0
@@ -46,7 +47,7 @@ let reset_counters () =
  metasenv_length := 0;
  context_length := 0
 let print_counters () =
-  prerr_endline (Printf.sprintf
+  debug_print (lazy (Printf.sprintf
 "apply_subst: %d
 apply_subst_context: %d
 apply_subst_metasenv: %d
@@ -63,26 +64,42 @@ context length: %d (avg = %.2f)
   ((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
   !context_length
   ((float !context_length) /. (float !apply_subst_context_counter))
-  )
-*)
+  ))*)
+
+
 
-exception MetaSubstFailure of string
-exception Uncertain of string
-exception AssertFailure of string
-exception SubstNotFound of int
+exception MetaSubstFailure of string Lazy.t
+exception Uncertain of string Lazy.t
+exception AssertFailure of string Lazy.t
+exception DeliftingARelWouldCaptureAFreeVariable;;
 
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
 
 type substitution = (int * (Cic.context * Cic.term)) list
 
-let lookup_subst n subst =
-  try
-    List.assoc n subst
-  with Not_found -> raise (SubstNotFound n)
+(* 
+let rec deref subst =
+  let third _,_,a = a in
+  function
+      Cic.Meta(n,l) as t -> 
+	(try 
+	   deref subst
+	     (CicSubstitution.subst_meta 
+		l (third (CicUtil.lookup_subst n subst))) 
+	 with 
+	   CicUtil.Subst_not_found _ -> t)
+    | t -> t
+;;
+*)
+
+let lookup_subst = CicUtil.lookup_subst
+;;
+
 
 (* clean_up_meta take a metasenv and a term and make every local context
 of each occurrence of a metavariable consistent with its canonical context, 
 with respect to the hidden hipothesis *)
+
 (*
 let clean_up_meta subst metasenv t =
   let module C = Cic in
@@ -95,7 +112,7 @@ let clean_up_meta subst metasenv t =
         let cc =
 	  (try
 	     let (cc,_) = lookup_subst n subst in cc
-	   with SubstNotFound _ ->
+	   with CicUtil.Subst_not_found _ ->
 	     try
 	       let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc
              with CicUtil.Meta_not_found _ -> assert false) in
@@ -166,15 +183,16 @@ let apply_subst_gen ~appl_fun subst term =
        C.Var (uri, exp_named_subst')
     | C.Meta (i, l) -> 
         (try
-          let (context, t) = lookup_subst i subst in
-          um_aux (S.lift_meta l t)
-        with SubstNotFound _ -> (* unconstrained variable, i.e. free in subst*)
+          let (_, t,_) = lookup_subst i subst in
+          um_aux (S.subst_meta l t)
+        with CicUtil.Subst_not_found _ -> 
+	  (* unconstrained 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.Sort _
+    | 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)
@@ -214,17 +232,6 @@ let apply_subst_gen ~appl_fun subst term =
 ;;
 
 let apply_subst =
-(* CSC: old code that never performs beta reduction
-  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 appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
     let t' =
@@ -234,18 +241,7 @@ let apply_subst =
     in
      begin
       match he with
-         Cic.Meta (m,_) ->
-          let rec beta_reduce =
-           function
-              (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-                let he'' = CicSubstitution.subst he' t in
-                 if tl' = [] then
-                  he''
-                 else
-                  beta_reduce (Cic.Appl(he''::tl'))
-            | t -> t
-          in
-           beta_reduce t'
+         Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
        | _ -> t'
      end
   in
@@ -292,9 +288,15 @@ let apply_subst_metasenv subst metasenv =
 
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
-let ppterm_in_context subst term name_context =
+let ppterm_in_name_context subst term name_context =
  CicPp.pp (apply_subst subst term) name_context
 
+let ppterm_in_context subst term context =
+ let name_context =
+  List.map (function None -> None | Some (n,_) -> Some n) context
+ in
+  ppterm_in_name_context subst term name_context
+
 let ppcontext' ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
@@ -302,13 +304,13 @@ let ppcontext' ?(sep = "\n") subst context =
      match context_entry with
         Some (n,Cic.Decl t) ->
          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_context subst t name_context), (Some n)::name_context
+          (ppterm_in_name_context subst t name_context), (Some n)::name_context
       | Some (n,Cic.Def (bo,ty)) ->
          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
           (match ty with
               None -> "_"
-            | Some ty -> ppterm_in_context subst ty name_context)
-          (ppterm_in_context subst bo name_context), (Some n)::name_context
+            | Some ty -> ppterm_in_name_context subst ty name_context)
+          (ppterm_in_name_context subst bo name_context), (Some n)::name_context
        | None ->
           sprintf "%s_ :? _" (separate i), None::name_context
     ) context ("",[])
@@ -316,10 +318,10 @@ let ppcontext' ?(sep = "\n") subst context =
 let ppsubst_unfolded subst =
   String.concat "\n"
     (List.map
-      (fun (idx, (c, t)) ->
+      (fun (idx, (c, t,_)) ->
         let context,name_context = ppcontext' ~sep:"; " subst c in
          sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_context subst t name_context))
+          (ppterm_in_name_context subst t name_context))
        subst)
 (* 
         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
@@ -329,87 +331,30 @@ let ppsubst_unfolded subst =
 let ppsubst subst =
   String.concat "\n"
     (List.map
-      (fun (idx, (c, t)) ->
+      (fun (idx, (c, t, _)) ->
         let context,name_context = ppcontext' ~sep:"; " [] c in
          sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_context [] t name_context))
+          (ppterm_in_name_context [] t name_context))
        subst)
 ;;
 
 let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
 
-let ppmetasenv ?(sep = "\n") metasenv subst =
+let ppmetasenv ?(sep = "\n") subst metasenv =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
         let context,name_context = ppcontext' ~sep:"; " subst c in
          sprintf "%s |- ?%d: %s" context i
-          (ppterm_in_context subst t name_context))
+          (ppterm_in_name_context subst t name_context))
       (List.filter
         (fun (i, _, _) -> not (List.mem_assoc i subst))
         metasenv))
 
-(* From now on we recreate a kernel abstraction where substitutions are part of
- * the calculus *)
-
-let lift subst n term =
-(*   incr subst_counter; *)
-  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 =
-(*   incr subst_counter; *)
-  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 =
-(*   incr whd_counter; *)
-  let term = apply_subst subst term in
-  let context = apply_subst_context subst context in
-  try
-    CicReduction.whd context term
-  with e ->
-    raise (MetaSubstFailure ("Weak head reduction failure: " ^
-      Printexc.to_string e))
-
-let are_convertible subst context t1 t2 =
-(*   incr are_convertible_counter; *)
-  let context = apply_subst_context subst context in
-  let t1 = apply_subst subst t1 in
-  let t2 = apply_subst subst t2 in
-  CicReduction.are_convertible context t1 t2
-
 let tempi_type_of_aux_subst = ref 0.0;;
 let tempi_subst = ref 0.0;;
 let tempi_type_of_aux = ref 0.0;;
 
-  (* assumption: metasenv is already instantiated wrt subst *)
-let type_of_aux' metasenv subst context term =
-  let time1 = Unix.gettimeofday () in
-(* let term = clean_up_meta subst metasenv term in *)
-  let term = apply_subst subst term in
-  let context = apply_subst_context subst context in
-(*   let metasenv = apply_subst_metasenv subst metasenv in *)
-  let time2 = Unix.gettimeofday () in
-  let res =
-    try
-      CicTypeChecker.type_of_aux' metasenv context term
-    with CicTypeChecker.TypeCheckerFailure msg ->
-      raise (MetaSubstFailure ("Type checker failure: " ^ msg))
-  in
-  let time3 = Unix.gettimeofday () in
-   tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; 
-   tempi_subst := !tempi_subst +. time2 -. time1 ; 
-   tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ; 
-   res
-
 (**** DELIFT ****)
 (* 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
@@ -552,11 +497,11 @@ let rec restrict subst to_be_restricted metasenv =
     | [] -> [], to_be_restricted, []
     | hd::tl ->
         let more_to_be_restricted,restricted,tl' =
-         erase (i+1) to_be_restricted n 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'
+          more_to_be_restricted, restricted, None:: tl'
         else
           (try
             let more_to_be_restricted', hd' =
@@ -597,14 +542,15 @@ let rec restrict subst to_be_restricted metasenv =
           (more @ more_to_be_restricted @ more_to_be_restricted',
           metasenv')
         with Occur ->
-          raise (MetaSubstFailure (sprintf
+          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)))) 
+	    n (names_of_context_indexes context to_be_restricted)))))
       metasenv ([], [])
   in
   let (more_to_be_restricted', subst) = (* restrict subst *)
     List.fold_right
-      (fun (n, (context, term)) (more, subst') ->
+      (* 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
@@ -619,22 +565,26 @@ let rec restrict subst to_be_restricted metasenv =
           let more_to_be_restricted', term' =
             force_does_not_occur subst restricted term
           in
-          let subst' = (n, (context', term')) :: subst' in
-          let more = more @ more_to_be_restricted @ more_to_be_restricted' 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 = sprintf
+          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 subst term)
-	  in
+            (ppterm subst term))
+	  in 
           (* DEBUG
-          prerr_endline error_msg;
-          prerr_endline ("metasenv = \n" ^ (ppmetasenv metasenv subst));
-          prerr_endline ("subst = \n" ^ (ppsubst subst)); 
-          prerr_endline ("context = \n" ^ (ppcontext subst context)); *)
+          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 ([], [])
+      subst ([], []) 
   in
   match more_to_be_restricted @ more_to_be_restricted' with
   | [] -> (metasenv, subst)
@@ -646,9 +596,10 @@ let rec restrict subst to_be_restricted metasenv =
 let delift n subst context metasenv l t =
 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
    otherwise the occur check does not make sense *)
+
 (*
- prerr_endline ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
- al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))); 
+ debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))));
 *)
 
  let module S = CicSubstitution in
@@ -678,10 +629,10 @@ let delift n subst context metasenv l t =
                 deliftaux k (S.lift m t)
              | Some (_,C.Decl t) ->
                 C.Rel ((position (m-k) l) + k)
-             | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
+             | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
            with
             Failure _ ->
-             raise (MetaSubstFailure "Unbound variable found in deliftaux")
+             raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
           )
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
@@ -689,31 +640,36 @@ let delift n subst context metasenv l t =
         in
          C.Var (uri,exp_named_subst')
      | C.Meta (i, l1) as t -> 
-         (* see the top level invariant *)
-	 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 (ppterm subst t))) 
-        else
-         begin
-         (* 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')
-	 end
+         (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 subst t))))
+          else
+            begin
+           (* 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')
+            end)
      | C.Sort _ as t -> t
      | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
@@ -766,26 +722,164 @@ let delift n subst context metasenv l t =
       (* 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 "First Order UnificationFailure during delift" ;
-prerr_endline(sprintf
+(* 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
-          ))); *)
-      raise (Uncertain (sprintf
+          )))); *)
+      raise (Uncertain (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))))
+            l)))))
    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
+ *)
+let delift_rels_from subst metasenv k n =
+ let rec liftaux subst metasenv k =
+  let module C = Cic in
+   function
+      C.Rel m ->
+       if m < k then
+        C.Rel m, subst, metasenv
+       else if m < k + n then
+         raise DeliftingARelWouldCaptureAFreeVariable
+       else
+        C.Rel (m - n), subst, metasenv
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst',subst,metasenv = 
+        List.fold_right
+         (fun (uri,t) (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+       in
+        C.Var (uri,exp_named_subst'),subst,metasenv
+    | C.Meta (i,l) ->
+        (try
+          let (_, t,_) = lookup_subst i subst in
+           liftaux subst metasenv k (CicSubstitution.subst_meta l t)
+         with CicUtil.Subst_not_found _ -> 
+          let l',to_be_restricted,subst,metasenv =
+           let rec aux con l subst metasenv =
+            match l with
+               [] -> [],[],subst,metasenv
+             | he::tl ->
+                let tl',to_be_restricted,subst,metasenv =
+                 aux (con + 1) tl subst metasenv in
+                let he',more_to_be_restricted,subst,metasenv =
+                 match he with
+                    None -> None,[],subst,metasenv
+                  | Some t ->
+                     try
+                      let t',subst,metasenv = liftaux subst metasenv k t in
+                       Some t',[],subst,metasenv
+                     with
+                      DeliftingARelWouldCaptureAFreeVariable ->
+                       None,[i,con],subst,metasenv
+                in
+                 he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
+           in
+            aux 1 l subst metasenv in
+          let metasenv,subst = restrict subst to_be_restricted metasenv in
+           C.Meta(i,l'),subst,metasenv)
+    | C.Sort _ as t -> t,subst,metasenv
+    | C.Implicit _ as t -> t,subst,metasenv
+    | C.Cast (te,ty) ->
+       let te',subst,metasenv = liftaux subst metasenv k te in
+       let ty',subst,metasenv = liftaux subst metasenv k ty in
+        C.Cast (te',ty'),subst,metasenv
+    | C.Prod (n,s,t) ->
+       let s',subst,metasenv = liftaux subst metasenv k s in
+       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+        C.Prod (n,s',t'),subst,metasenv
+    | C.Lambda (n,s,t) ->
+       let s',subst,metasenv = liftaux subst metasenv k s in
+       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+        C.Lambda (n,s',t'),subst,metasenv
+    | C.LetIn (n,s,t) ->
+       let s',subst,metasenv = liftaux subst metasenv k s in
+       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+        C.LetIn (n,s',t'),subst,metasenv
+    | C.Appl l ->
+       let l',subst,metasenv =
+        List.fold_right
+         (fun t (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            t'::l,subst,metasenv) l ([],subst,metasenv) in
+       C.Appl l',subst,metasenv
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst',subst,metasenv = 
+        List.fold_right
+         (fun (uri,t) (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+       in
+        C.Const (uri,exp_named_subst'),subst,metasenv
+    | C.MutInd (uri,tyno,exp_named_subst) ->
+       let exp_named_subst',subst,metasenv = 
+        List.fold_right
+         (fun (uri,t) (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+       in
+        C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
+    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+       let exp_named_subst',subst,metasenv = 
+        List.fold_right
+         (fun (uri,t) (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+       in
+        C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
+    | C.MutCase (sp,i,outty,t,pl) ->
+       let outty',subst,metasenv = liftaux subst metasenv k outty in
+       let t',subst,metasenv = liftaux subst metasenv k t in
+       let pl',subst,metasenv =
+        List.fold_right
+         (fun t (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            t'::l,subst,metasenv) pl ([],subst,metasenv)
+       in
+        C.MutCase (sp,i,outty',t',pl'),subst,metasenv
+    | C.Fix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl,subst,metasenv =
+        List.fold_right
+         (fun (name, i, ty, bo) (l,subst,metasenv) ->
+           let ty',subst,metasenv = liftaux subst metasenv k ty in
+           let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+            (name,i,ty',bo')::l,subst,metasenv
+         ) fl ([],subst,metasenv)
+       in
+        C.Fix (i, liftedfl),subst,metasenv
+    | C.CoFix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl,subst,metasenv =
+        List.fold_right
+         (fun (name, ty, bo) (l,subst,metasenv) ->
+           let ty',subst,metasenv = liftaux subst metasenv k ty in
+           let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+            (name,ty',bo')::l,subst,metasenv
+         ) fl ([],subst,metasenv)
+       in
+        C.CoFix (i, liftedfl),subst,metasenv
+ in
+  liftaux subst metasenv k
+
+let delift_rels subst metasenv n t =
+  delift_rels_from subst metasenv 1 n t
+ 
+
 (**** END OF DELIFT ****)
 
 
@@ -798,5 +892,5 @@ let fpp_gen ppf s =
 
 let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
 let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
-let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])
+let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)