CicSubstitution.delift ==> CicMetaSubst.delift_rels

[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index b8784d7172df6c95f1f8b170a62d7ac5dbcdfd31..021e87ea5c6a6c1221566fcf42b3b0dfe6bca738 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -47,7 +47,7 @@ let reset_counters () =
  metasenv_length := 0;
  context_length := 0
 let print_counters () =
-  prerr_endline (Printf.sprintf
+  debug_print (Printf.sprintf
 "apply_subst: %d
 apply_subst_context: %d
 apply_subst_metasenv: %d
@@ -71,8 +71,9 @@ context length: %d (avg = %.2f)
 exception MetaSubstFailure of string
 exception Uncertain of string
 exception AssertFailure of string
+exception DeliftingARelWouldCaptureAFreeVariable;;
 
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
 
 type substitution = (int * (Cic.context * Cic.term)) list
 
@@ -594,10 +595,10 @@ let rec restrict subst to_be_restricted metasenv =
             (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 error_msg;
+          debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst));
+          debug_print ("subst = \n" ^ (ppsubst subst)); 
+          debug_print ("context = \n" ^ (ppcontext subst context)); *)
           raise (MetaSubstFailure error_msg))) 
       subst ([], []) 
   in
@@ -613,7 +614,7 @@ let delift n subst context metasenv l t =
    otherwise the occur check does not make sense *)
 
 (*
- prerr_endline ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
  al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))); 
 *)
 
@@ -738,7 +739,7 @@ let delift n subst context metasenv l t =
       (* 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(sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
         (String.concat "; "
@@ -757,6 +758,82 @@ prerr_endline(sprintf
     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 k n =
+ let rec liftaux k =
+  let module C = Cic in
+   function
+      C.Rel m ->
+       if m < k then
+        C.Rel m
+       else if m < k + n then
+         raise DeliftingARelWouldCaptureAFreeVariable
+       else
+        C.Rel (m - n)
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+       in
+        C.Var (uri,exp_named_subst')
+    | C.Meta (i,l) ->
+       let l' =
+        List.map
+         (function
+             None -> None
+           | Some t -> Some (liftaux k t)
+         ) l
+       in
+        C.Meta(i,l')
+    | C.Sort _ as t -> t
+    | C.Implicit _ as t -> t
+    | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
+    | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
+    | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
+    | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
+    | C.Appl l -> C.Appl (List.map (liftaux k) l)
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,liftaux 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 (function (uri,t) -> (uri,liftaux 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 (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+       in
+        C.MutConstruct (uri,tyno,consno,exp_named_subst')
+    | C.MutCase (sp,i,outty,t,pl) ->
+       C.MutCase (sp, i, liftaux k outty, liftaux k t,
+        List.map (liftaux k) pl)
+    | C.Fix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl =
+        List.map
+         (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (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, liftaux k ty, liftaux (k+len) bo))
+          fl
+       in
+        C.CoFix (i, liftedfl)
+ in
+ liftaux k
+
+let delift_rels n t =
+  delift_rels_from 1 n t
+ 
+
 (**** END OF DELIFT ****)