X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=eaa094fdcf464147727fa61a139a6c95804044a1;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=db63ff5685ab23cfe2eec391a304d2caf87c651b;hpb=1592bfa20a80f2f58fe0593c019689cb32072db6;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index db63ff568..eaa094fdc 100644
--- 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
@@ -72,7 +72,7 @@ exception MetaSubstFailure of string
 exception Uncertain of string
 exception AssertFailure of string
 
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
 
 type substitution = (int * (Cic.context * Cic.term)) list
 
@@ -83,7 +83,7 @@ let rec deref subst =
       Cic.Meta(n,l) as t -> 
 	(try 
 	   deref subst
-	     (CicSubstitution.lift_meta 
+	     (CicSubstitution.subst_meta 
 		l (third (CicUtil.lookup_subst n subst))) 
 	 with 
 	   CicUtil.Subst_not_found _ -> t)
@@ -183,7 +183,7 @@ let apply_subst_gen ~appl_fun subst term =
     | C.Meta (i, l) -> 
         (try
           let (_, t,_) = lookup_subst i subst in
-          um_aux (S.lift_meta l t)
+          um_aux (S.subst_meta l t)
         with CicUtil.Subst_not_found _ -> 
 	  (* unconstrained variable, i.e. free in subst*)
           let l' =
@@ -594,10 +594,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 +613,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)))); 
 *)
 
@@ -655,32 +655,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 (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)
@@ -734,7 +738,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 "; "