X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=d95415d99d64d42c6e5565eb0b33bdd996fafb3a;hb=667640d70feb01f2a800b548fa019c92b103d75a;hp=09b1f3d2e77d923b3345eba41da1aa76a6897062;hpb=2007402c996678701798d71124a1a255529061ee;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 09b1f3d2e..d95415d99 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -14,20 +14,14 @@
 exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
+exception KeepReducing of string Lazy.t;;
 
 let (===) x y = Pervasives.compare x y = 0 ;;
 
-let uncert_exc metasenv subst context t1 t2 = 
-  Uncertain (lazy (
+let mk_msg metasenv subst context t1 t2 =
+ (lazy (
   "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
-;;
-
-let fail_exc metasenv subst context t1 t2 = 
-  UnificationFailure (lazy (
-  "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
-  " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2));
-;;
 
 let mk_appl ~upto hd tl =
   NCicReduction.head_beta_reduce ~upto
@@ -78,20 +72,20 @@ let eta_reduce subst t =
 module C = NCic;;
 module Ref = NReference;;
 
-let debug = false;;
+let debug = ref false;;
 let indent = ref "";;
-let pp =
- if debug then
-  fun s -> prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+let pp s =
+ if !debug then
+  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
  else 
-  fun _ -> ()
+  ()
 ;;
 let inside c =
  indent := !indent ^ String.make 1 c;
- if debug then prerr_endline ("{{{" ^ !indent ^ " ")
+ if !debug then prerr_endline ("{{{" ^ !indent ^ " ")
 ;;
 let outside ok =
- if debug then prerr_endline "}}}";
+ if !debug then prerr_endline "}}}";
  if not ok then pp (lazy "exception raised!");
  try
   indent := String.sub !indent 0 (String.length !indent -1)
@@ -135,10 +129,9 @@ let is_locked n subst =
    with NCicUtils.Subst_not_found _ -> false
 ;;
 
-let rec mk_irl =
- function
-    0 -> []
-  | n -> NCic.Rel n :: mk_irl (n-1)
+let rec mk_irl stop base =
+  if base > stop then []
+  else (NCic.Rel base) :: mk_irl stop (base+1) 
 ;;
 
 (* the argument must be a term in whd *)
@@ -168,15 +161,16 @@ let rec lambda_intros rdb metasenv subst context t args =
        metasenv, subst, bo
    | (arg,ty)::tail ->
        pp(lazy("arg{ " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  ":" ^
+         NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  " : " ^
          NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty));
        let metasenv, subst, telescopic_ty = 
          if processed_args = [] then metasenv, subst, ty else
          let _ = pp(lazy("delift")) in
-         delift_type_wrt_terms rdb metasenv subst context_of_args ty 
-           (List.rev processed_args)
+         delift_type_wrt_terms rdb metasenv subst context 
+           (NCicSubstitution.lift n ty)
+           (List.map (NCicSubstitution.lift n) (List.rev processed_args))
        in
-       pp(lazy("arg}"));
+       pp(lazy("arg} "^NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty));
        let name = "HBeta"^string_of_int n in
        let metasenv, subst, bo =
         mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
@@ -200,98 +194,107 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
     if swap then unify rdb test_eq_only m s c t2 t1 
     else unify rdb test_eq_only m s c t1 t2
   in
-  let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
+  let has_tag = List.exists in
+  let tags, _, ty = NCicUtils.lookup_meta n metasenv in
+  (* on the types *)
   let metasenv, subst, t = 
     match ty with 
-    | NCic.Implicit (`Typeof _) ->
-       (match NCicReduction.whd ~subst context t with
-          NCic.Sort _ -> metasenv,subst,t
-        | NCic.Meta (i,_) when
-           let _,_,ty = NCicUtils.lookup_meta i metasenv in
-            (match ty with
-                NCic.Implicit (`Typeof _) -> true
-              | _ -> false)
-           -> metasenv,subst,t
-        | NCic.Meta (i,_) ->
-           let rec remove_and_hope i =
-            let _,ctx,ty = NCicUtils.lookup_meta i metasenv in
-            match ty with
-               NCic.Implicit _ -> List.filter (fun i',_ -> i <> i') metasenv
-             | _ ->
-               match NCicReduction.whd ~subst ctx ty with
-                  NCic.Meta (j,_) ->
-                   let metasenv = remove_and_hope j in
-                    List.filter (fun i',_ -> i <> i') metasenv
-                | _ -> assert false (* NON POSSO RESTRINGERE *)
-           in
-           let metasenv = remove_and_hope i in
-           let metasenv =
-            (i,([],[],NCic.Implicit (`Typeof i)))::
-             List.filter (fun i',_ -> i <> i') metasenv
-           in
-            metasenv,subst,t
-        | NCic.Appl (NCic.Meta _::_) ->
-           raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
-        | t when could_reduce t -> 
-           raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
-        | _ ->
-           raise (UnificationFailure (lazy "Trying to instantiate a metavariable that represents a sort with a term")))
+    | NCic.Implicit (`Typeof _) -> 
+         pp(lazy("meta with no type"));
+         assert(has_tag ((=)`IsSort) tags); 
+         metasenv, subst, t
     | _ ->
-       pp (lazy (
-               "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
-          ppcontext ~metasenv ~subst context ^ 
-          ppmetasenv ~subst metasenv));
-       let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
+       let exc_to_be =
+        UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t)
+       in
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
          with 
-         | NCicTypeChecker.AssertFailure msg -> 
-           (pp (lazy "fine typeof (fallimento)");
-           let ft = fix_sorts swap exc_to_be t in
-           if ft == t then 
-             (prerr_endline ( ("ILLTYPED: " ^ 
-                NCicPp.ppterm ~metasenv ~subst ~context t
-            ^ "\nBECAUSE:" ^ Lazy.force msg ^ 
-            ppcontext ~metasenv ~subst context ^ 
-            ppmetasenv ~subst metasenv
-            ));
-                     assert false)
-           else
-            try 
-              pp (lazy ("typeof: " ^ 
-                NCicPp.ppterm ~metasenv ~subst ~context ft));
-              ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
-            with NCicTypeChecker.AssertFailure _ -> 
-              assert false)
+         | NCicTypeChecker.AssertFailure msg as exn -> 
+              pp(lazy("we try to fix the sort\n"^
+                Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst metasenv));
+              let ft = fix_sorts swap exc_to_be t in
+              pp(lazy("unable to fix the sort"));
+              if ft == t then raise exn;
+              (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
+               with NCicTypeChecker.AssertFailure _ -> raise exn)
          | NCicTypeChecker.TypeCheckerFailure msg ->
               prerr_endline (Lazy.force msg);
-       prerr_endline (
-               "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
-          ppcontext ~metasenv ~subst context ^ 
-          ppmetasenv ~subst metasenv);
-              pp msg; assert false
+              prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+              prerr_endline (ppcontext ~metasenv ~subst context); 
+              prerr_endline (ppmetasenv ~subst metasenv);
+              assert false
        in
-       let lty = NCicSubstitution.subst_meta lc ty in
        match ty_t with
-       | NCic.Implicit _ -> 
-           raise (UnificationFailure 
-             (lazy "trying to unify a term with a type"))
-       | ty_t -> 
+       | NCic.Implicit (`Typeof _) -> 
+           raise (UnificationFailure(lazy "trying to unify a term with a type"))
+       | _ -> 
+          let lty = NCicSubstitution.subst_meta lc ty in
           pp (lazy ("On the types: " ^
-           NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
-           NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
-            ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
+              NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^ 
+              NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
           let metasenv,subst = 
-           try
-            unify test_eq_only metasenv subst context lty ty_t
+           try unify test_eq_only metasenv subst context lty ty_t
            with NCicEnvironment.BadConstraint _ as exc ->
             let ty_t = fix_sorts swap exc_to_be ty_t in 
              try unify test_eq_only metasenv subst context lty ty_t
-             with _ -> raise exc in
-          metasenv, subst, t
+             with 
+             | NCicEnvironment.BadConstraint _ 
+             | UnificationFailure _ -> raise exc 
+          in
+           metasenv, subst, t
+  in 
+  (* viral sortification *)
+  let is_sort metasenv subst context t = 
+    match NCicReduction.whd ~subst context t with
+    | NCic.Meta (i,_) ->
+         let tags, _, _ = NCicUtils.lookup_meta i metasenv in
+         has_tag ((=) `IsSort) tags
+    | NCic.Sort _ -> true
+    | _ -> false
   in
-         pp (lazy(string_of_int n ^ " := 111 = "^
-           NCicPp.ppterm ~metasenv ~subst ~context t));
+  let rec sortify metasenv subst = function
+    | NCic.Implicit (`Typeof _) -> assert false 
+    | NCic.Sort _ as t -> metasenv, subst, t, 0
+    | NCic.Meta (i,_) as t -> 
+         let tags, context, ty = NCicUtils.lookup_meta i metasenv in
+         if has_tag ((=) `IsSort) tags then metasenv, subst, t, i
+         else
+           let ty = NCicReduction.whd ~subst context ty in
+           let metasenv, subst, ty, _ = sortify metasenv subst ty in
+           let metasenv, j, m, _ = 
+             NCicMetaSubst.mk_meta metasenv ~attrs:[`IsSort] [] (`WithType ty)
+           in
+           pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j));
+           let subst_entry = i, (tags, context, m, ty) in
+           let subst = subst_entry :: subst in
+           let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
+           metasenv, subst, m, j 
+    | NCic.Appl (NCic.Meta _ as hd :: args) as t -> 
+           let metasenv, subst, lambda_Mj =
+             lambda_intros rdb metasenv subst context t args
+           in
+           let metasenv,subst= unify true metasenv subst context hd lambda_Mj in
+           let t = NCicReduction.whd ~subst context t in
+           let _result = sortify metasenv subst t in       
+           (* untested, maybe dead, code *) assert false;
+    | t -> 
+         if could_reduce t then raise (Uncertain(lazy "not a sort"))
+         else raise (UnificationFailure(lazy "not a sort"))
+  in
+  let metasenv, subst, _, n = 
+    if has_tag ((=) `IsSort) tags then
+      let m,s,x,_ = sortify metasenv subst (NCicReduction.whd ~subst context t)
+      in m,s,x,n
+    else if is_sort metasenv subst context t then
+      sortify metasenv subst (NCic.Meta (n,lc))
+    else
+      metasenv, subst, NCic.Rel ~-1,n
+  in
+  let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in
+  (* instantiation *)
+  pp (lazy(string_of_int n ^ " := 111 = "^ 
+    NCicPp.ppterm ~metasenv ~subst ~context t));
   let (metasenv, subst), t = 
     try 
       NCicMetaSubst.delift 
@@ -321,9 +324,24 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
     (* conjecture: always fail --> occur check *)
     unify test_eq_only metasenv subst context oldt t
   with NCicUtils.Subst_not_found _ -> 
+    let metasenv, tags = 
+      let rec aux = function
+        | NCic.Meta (j,lc) -> 
+            (try 
+              let _, _, t, _ = NCicUtils.lookup_subst j subst in
+              aux (NCicSubstitution.subst_meta lc t)
+            with NCicUtils.Subst_not_found _ -> 
+              let tags', ctx, ty = NCicUtils.lookup_meta j metasenv in
+              let metasenv = List.remove_assoc j metasenv in
+              let tags = tags @ tags' in
+              (j, (tags, ctx, ty)) :: metasenv, tags)
+        | _ -> metasenv, tags
+      in 
+        aux t
+    in
     (* by cumulativity when unify(?,Type_i) 
      * we could ? := Type_j with j <= i... *)
-    let subst = (n, (name, ctx, t, ty)) :: subst in
+    let subst = (n, (tags, ctx, t, ty)) :: subst in
     pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
       ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
     let metasenv = 
@@ -334,11 +352,14 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
 
 and unify rdb test_eq_only metasenv subst context t1 t2 =
  (*D*) inside 'U'; try let rc =
-   let fo_unif test_eq_only metasenv subst t1 t2 =
+   let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
     (*D*) inside 'F'; try let rc =  
      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
          NCicPp.ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
          ~subst metasenv));
+     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ 
+         NCicPp.ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
+         ~subst metasenv));
      if t1 === t2 then
        metasenv, subst
      else
@@ -349,13 +370,13 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
            assert false 
        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
            if NCicEnvironment.universe_leq a b then metasenv, subst
-           else raise (fail_exc metasenv subst context t1 t2)
+           else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
            if NCicEnvironment.universe_eq a b then metasenv, subst
-           else raise (fail_exc metasenv subst context t1 t2)
+           else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
        | (C.Sort C.Prop,C.Sort (C.Type _)) -> 
            if (not test_eq_only) then metasenv, subst
-           else raise (fail_exc metasenv subst context t1 t2)
+           else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
 
        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
@@ -399,6 +420,16 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                 let term2 = NCicSubstitution.subst_meta lc2 term in
                   unify rdb test_eq_only metasenv subst context term1 term2
               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
+
+       |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
+          NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
+            (try
+              List.fold_left2 
+                (fun (metasenv, subst) t1 t2 ->
+                  unify rdb test_eq_only metasenv subst context t1 t2)
+                (metasenv,subst) l1 l2
+            with Invalid_argument _ -> 
+              raise (UnificationFailure (mk_msg metasenv subst context t1 t2)))
        
        | _, NCic.Meta (n, _) when is_locked n subst ->
            (let (metasenv, subst), i = 
@@ -440,23 +471,15 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
               with Not_found -> assert false))
 
-       | C.Meta (n,lc), t -> 
-           (try 
-             let _,_,term,_ = NCicUtils.lookup_subst n subst in
-             let term = NCicSubstitution.subst_meta lc term in
-               unify rdb test_eq_only metasenv subst context term t
-           with NCicUtils.Subst_not_found _-> 
-             instantiate rdb test_eq_only metasenv subst context n lc 
-               (NCicReduction.head_beta_reduce ~subst t) false)
+       | C.Meta (n,lc), t when List.mem_assoc n subst -> 
+          let _,_,term,_ = NCicUtils.lookup_subst n subst in
+          let term = NCicSubstitution.subst_meta lc term in
+            unify rdb test_eq_only metasenv subst context term t
 
-       | t, C.Meta (n,lc) -> 
-           (try 
-             let _,_,term,_ = NCicUtils.lookup_subst n subst in
-             let term = NCicSubstitution.subst_meta lc term in
-               unify rdb test_eq_only metasenv subst context t term
-           with NCicUtils.Subst_not_found _-> 
-             instantiate rdb test_eq_only metasenv subst context n lc 
-              (NCicReduction.head_beta_reduce ~subst t) true)
+       | t, C.Meta (n,lc) when List.mem_assoc n subst -> 
+          let _,_,term,_ = NCicUtils.lookup_subst n subst in
+          let term = NCicSubstitution.subst_meta lc term in
+            unify rdb test_eq_only metasenv subst context t term
 
        | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
             let _,_,term,_ = NCicUtils.lookup_subst i subst in
@@ -470,23 +493,25 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
               unify rdb test_eq_only metasenv subst context t1 
                 (mk_appl ~upto:(List.length args) term args)
 
-       |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
-          NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
-            (try
-              List.fold_left2 
-                (fun (metasenv, subst) t1 t2 ->
-                  unify rdb test_eq_only metasenv subst context t1 t2)
-                (metasenv,subst) l1 l2
-            with Invalid_argument _ -> 
-              raise (fail_exc metasenv subst context t1 t2))
+       | C.Meta (n,lc), t -> 
+          instantiate rdb test_eq_only metasenv subst context n lc 
+            (NCicReduction.head_beta_reduce ~subst t) false
+
+       | t, C.Meta (n,lc) -> 
+          instantiate rdb test_eq_only metasenv subst context n lc 
+           (NCicReduction.head_beta_reduce ~subst t) true
 
        | NCic.Appl (NCic.Meta (i,l)::args), _ ->
           let metasenv, subst, lambda_Mj =
             lambda_intros rdb metasenv subst context t1 args
           in
           let metasenv, subst = 
+           try
             unify rdb test_eq_only metasenv subst context 
               (C.Meta (i,l)) lambda_Mj
+           with UnificationFailure msg | Uncertain msg ->
+            (* failure: let's try again argument vs argument *)
+            raise (KeepReducing msg)
           in
           let metasenv, subst = 
             unify rdb test_eq_only metasenv subst context t1 t2 
@@ -503,8 +528,12 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
            lambda_intros rdb metasenv subst context t2 args
          in
          let metasenv, subst =
+          try
            unify rdb test_eq_only metasenv subst context 
             lambda_Mj (C.Meta (i,l))
+          with UnificationFailure msg | Uncertain msg ->
+           (* failure: let's try again argument vs argument *)
+           raise (KeepReducing msg)
          in
          let metasenv, subst = 
            unify rdb test_eq_only metasenv subst context t1 t2 
@@ -542,8 +571,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                     in
                       metasenv, subst, relevance)
                  (metasenv, subst, relevance) tl1 tl2
-             with Invalid_argument _ -> 
-               raise (uncert_exc metasenv subst context t1 t2)
+             with
+                Invalid_argument _ -> 
+                 raise (Uncertain (mk_msg metasenv subst context t1 t2))
+              | UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
+                 raise (KeepReducing (mk_msg metasenv subst context t1 t2))
            in 
              metasenv, subst
 
@@ -565,7 +597,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
              | _ -> false 
            in
            if not (Ref.eq ref1 ref2) then 
-             raise (uncert_exc metasenv subst context t1 t2) 
+             raise (Uncertain (mk_msg metasenv subst context t1 t2))
            else
              let metasenv, subst = 
               unify rdb test_eq_only metasenv subst context outtype1 outtype2 in
@@ -581,19 +613,19 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                (metasenv, subst) pl1 pl2
              with Invalid_argument _ -> assert false)
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
-       | _ when NCicUntrusted.metas_of_term subst context t1 = [] && 
-                NCicUntrusted.metas_of_term subst context t2 = [] -> 
-                  raise (fail_exc metasenv subst context t1 t2)
-       | _ -> raise (uncert_exc metasenv subst context t1 t2)
+       | _ when norm1 && norm2 ->
+           if (could_reduce t1 || could_reduce t2) then
+            raise (Uncertain (mk_msg metasenv subst context t1 t2))
+           else
+            raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
+       | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
      (*D*)  in outside true; rc with exn -> outside false; raise exn 
     in
-    let try_hints metasenv subst t1 t2 (* exc*) =
+    let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
     (*D*) inside 'H'; try let rc =  
-(*
-      prerr_endline ("\nProblema:\n" ^
+     pp(lazy ("\nProblema:\n" ^
         NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
-        NCicPp.ppterm ~metasenv ~subst ~context t2);
-*)
+        NCicPp.ppterm ~metasenv ~subst ~context t2));
       let candidates = 
         NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
       in
@@ -612,20 +644,20 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
             try 
     (*D*) inside 'K'; try let rc =  
               let metasenv,subst = 
-                fo_unif test_eq_only metasenv subst t1 c1 in
+                fo_unif test_eq_only metasenv subst mt1 (false,c1) in
               let metasenv,subst = 
-                fo_unif test_eq_only metasenv subst c2 t2 in
+                fo_unif test_eq_only metasenv subst (false,c2) mt2 in
               let metasenv,subst = 
                 List.fold_left 
                   (fun (metasenv, subst) (x,y) ->
                      unify rdb test_eq_only metasenv subst context x y)
                   (metasenv, subst) premises
               in
+              pp(lazy("FUNZIONA!"));
               Some (metasenv, subst)
      (*D*)  in outside true; rc with exn -> outside false; raise exn 
             with
-              UnificationFailure _ | Uncertain _ ->
-                cand_iter tl
+             KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
       in
         cand_iter candidates
      (*D*)  in outside true; rc with exn -> outside false; raise exn 
@@ -646,9 +678,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
     =
      assert (not (norm1 && norm2));
      if norm1 then
-      x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
+      x1,NCicReduction.reduce_machine ~delta:0 ~subst context m2
      else if norm2 then
-      NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
+      NCicReduction.reduce_machine ~delta:0 ~subst context m1,x2
      else 
       let h1 = height_of t1 in 
       let h2 = height_of t2 in
@@ -690,37 +722,51 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           in
         let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
         try
-         let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
+         let metasenv,subst =
+          fo_unif test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
          List.fold_left
           (fun (metasenv,subst) (x1,x2,r) ->
             unif_from_stack x1 x2 r metasenv subst
           ) (metasenv,subst) todo
-        with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
+        with
+         | KeepReducing _ ->
+            assert (not (norm1 && norm2));
 	    unif_machines metasenv subst (small_delta_step ~subst m1 m2)
+         | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
+           -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
+         | UnificationFailure msg
+           when could_reduce (NCicReduction.unwind (fst m1))
+             || could_reduce (NCicReduction.unwind (fst m2))
+           -> raise (Uncertain msg)
       (*D*)  in outside true; rc with exn -> outside false; raise exn 
      in
-     try fo_unif test_eq_only metasenv subst t1 t2
+     try fo_unif test_eq_only metasenv subst (false,t1) (false,t2)
      with 
-     | UnificationFailure msg as exn ->
-          (try 
-            unif_machines metasenv subst 
-             (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
-          with 
-          | UnificationFailure _ -> raise (UnificationFailure msg)
-          | Uncertain _ -> raise exn)
-     | Uncertain msg as exn -> 
-       match try_hints metasenv subst t1 t2 with
-       | Some x -> x
-       | None -> 
-          try 
-            unif_machines metasenv subst 
-             (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
-          with 
-          | UnificationFailure _ -> raise (UnificationFailure msg)
-          | Uncertain _ -> raise exn
- (*D*)  in outside true; rc with exn -> outside false; raise exn 
+     | UnificationFailure _ as exn -> raise exn
+     | KeepReducing _ | Uncertain _ as exn ->
+       let (t1,norm1 as tm1),(t2,norm2 as tm2) =
+        put_in_whd (0,[],t1,[]) (0,[],t2,[])
+       in
+        (match 
+          try_hints metasenv subst 
+           (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+         with
+          | Some x -> x
+          | None ->
+             match exn with
+              | KeepReducing msg ->
+                 (try 
+                   unif_machines metasenv subst (tm1,tm2)
+                  with 
+                  | UnificationFailure _ -> raise (UnificationFailure msg)
+                  | Uncertain _ -> raise (Uncertain msg)
+                  | KeepReducing _ -> assert false)
+              | Uncertain _ -> raise exn
+              | _ -> assert false)
+ (*D*)  in outside true; rc with KeepReducing _ -> assert false | exn -> outside false; raise exn 
 
 and delift_type_wrt_terms rdb metasenv subst context t args =
+  let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
   let (metasenv, subst), t =
    try
     NCicMetaSubst.delift 
@@ -731,9 +777,10 @@ and delift_type_wrt_terms rdb metasenv subst context t args =
            with UnificationFailure _ | Uncertain _ -> None
          in
          indent := ind; res)
-      metasenv subst context 0 (0,NCic.Ctx (args @ 
-        List.rev (mk_irl (List.length context)))) t
-   with NCicMetaSubst.MetaSubstFailure _ -> (metasenv, subst), t
+      metasenv subst context 0 (0,NCic.Ctx lc) t
+   with
+      NCicMetaSubst.MetaSubstFailure _
+    | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
   in
    metasenv, subst, t
 ;;