X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;fp=matitaB%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=d45b14fc9f3a1cfb14b0377e5d2f3ac96250d7b0;hb=1410ea677188e9e11d748c69e208d1e90b0a324e;hp=cd5c89dd33a785d4830a1ef51d79637f91e2c369;hpb=f1ef0a9e283af00cace679efd5775062c2a8f05c;p=helm.git

diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml
index cd5c89dd3..d45b14fc9 100644
--- a/matitaB/components/ng_refiner/nCicUnification.ml
+++ b/matitaB/components/ng_refiner/nCicUnification.ml
@@ -99,6 +99,8 @@ let outside exc_opt =
     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
    prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
    (match exc_opt with
+   | Some (UnificationFailure msg) ->  prerr_endline ("exception raised: NCicUnification.UnificationFailure:" ^ Lazy.force msg)
+   | Some (Uncertain msg) ->  prerr_endline ("exception raised: NCicUnification.Uncertain:" ^ Lazy.force msg)
    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
    | None -> ());
    try
@@ -132,13 +134,15 @@ let rec mk_irl stop base =
 ;;
 
 (* the argument must be a term in whd *)
-let rec could_reduce =
+let rec could_reduce status ~subst context =
  function
   | C.Meta _ -> true
   | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
-     when List.length args > recno -> could_reduce (List.nth args recno)
-  | C.Match (_,_,arg,_) -> could_reduce arg
-  | C.Appl (he::_) -> could_reduce he
+     when List.length args > recno ->
+      let t = NCicReduction.whd status ~subst context (List.nth args recno) in
+        could_reduce status subst context t
+  | C.Match (_,_,arg,_) -> could_reduce status ~subst context arg
+  | C.Appl (he::_) -> could_reduce status ~subst context he
   | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
   | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
 ;;
@@ -273,6 +277,11 @@ let tipify status exc metasenv subst context t ty =
      metasenv,subst,t
 ;;
 
+let put_in_whd status subst context m1 m2 =
+  NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
+  NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
+;;
+
 let rec instantiate status test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
   pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t));
@@ -288,14 +297,7 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap =
       ppterm status ~metasenv ~subst ~context t));
     let (metasenv, subst), t = 
       try 
-        NCicMetaSubst.delift status
-         ~unify:(fun m s c t1 t2 -> 
-           let ind = !indent in
-           let res = 
-             try Some (unify status test_eq_only m s c t1 t2 false)
-             with UnificationFailure _ | Uncertain _ -> None
-           in
-           indent := ind; res) 
+        NCicMetaSubst.delift status ~unify:(unify_for_delift status)
          metasenv subst context n lc t
       with NCicMetaSubst.Uncertain msg -> 
            pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
@@ -362,13 +364,7 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap =
          NCic.Implicit (`Typeof _) ->
           let (metasenv, subst), ty_t = 
             try 
-              NCicMetaSubst.delift status
-               ~unify:(fun m s c t1 t2 -> 
-                 let ind = !indent in
-                 let res = try Some (unify status test_eq_only m s c t1 t2 false )
-                   with UnificationFailure _ | Uncertain _ -> None
-                 in
-                 indent := ind; res)
+              NCicMetaSubst.delift status ~unify:(unify_for_delift status)
                metasenv subst context n lc ty_t
             with NCicMetaSubst.Uncertain msg -> 
                  pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
@@ -391,22 +387,49 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap =
          subst)
  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
 
-and unify status test_eq_only metasenv subst context t1 t2 swap =
- (*D*) inside 'U'; try let rc =
-   let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
-    (*D*) inside 'F'; try let rc =  
-     pp (lazy("  " ^ ppterm status ~metasenv ~subst ~context t1 ^ 
-          (if swap then " ==>?== " 
-           else " ==<?==" ) ^ 
-         ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
-         ~subst metasenv));
-     pp (lazy("  " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
-          (if swap then " ==>??== " 
-           else " ==<??==" ) ^ 
-         ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
-         ~subst metasenv));
-     if t1 === t2 then
-       metasenv, subst
+and fo_unif_w_hints during_delift status swap test_eq_only metasenv subst context (_,t1 as m1) (_,t2 as m2) =
+ try fo_unif during_delift status swap test_eq_only metasenv subst context m1 m2
+ with 
+ | UnificationFailure _ as exn -> raise exn
+ | KeepReducing _ | Uncertain _ as exn ->
+   let (t1,norm1 as tm1),(t2,norm2 as tm2) =
+    put_in_whd status subst context (0,[],t1,[]) (0,[],t2,[])
+   in
+    match 
+      try_hints status swap test_eq_only metasenv subst context
+       (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
+    with
+     | Some x -> x
+     | None -> 
+         match exn with 
+         | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
+         | Uncertain _ as exn -> raise exn
+         | _ -> assert false
+
+and unify_for_delift status metasenv subst context t1 t2 =
+ let ind = !indent in
+ let res = 
+   try Some
+    (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
+      context (false,t1) (false,t2))
+   with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
+ in
+ indent := ind; res
+
+and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm1,t1 as m1) (norm2,t2 as m2) =
+ (*D*) inside 'F'; try let rc =  
+  pp (lazy("  " ^ ppterm status ~metasenv ~subst ~context t1 ^ 
+       (if swap then " ==>?== " 
+        else " ==<?==" ) ^ 
+      ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
+      ~subst metasenv));
+  pp (lazy("  " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
+       (if swap then " ==>??== " 
+        else " ==<??==" ) ^ 
+      ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
+      ~subst metasenv));
+  if t1 === t2 then
+    metasenv, subst
 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
      else if
       NCicUntrusted.metas_of_term subst context t1 = [] &&
@@ -417,368 +440,352 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
       else
        raise (UnificationFailure (lazy "Closed terms not convertible"))
 *)
-     else
-       match (t1,t2) with
-       | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl [] 
-       | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> 
-           prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
-           assert false 
-       | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
-           let a, b = if swap then b,a else a,b in
-           if NCicEnvironment.universe_leq status a b then metasenv, subst
-           else raise (UnificationFailure (mk_msg status 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 (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-       | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap -> 
-           if (not test_eq_only) then metasenv, subst
-           else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-       | (C.Sort (C.Type _), C.Sort C.Prop) when swap -> 
-           if (not test_eq_only) then metasenv, subst
-           else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-
-       | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
-       | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
-           unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
-       | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
-           let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
-           let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
-           let context = (name1, C.Def (s1,ty1))::context in
-           unify status test_eq_only metasenv subst context t1 t2 swap
-
-       | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
-          (try 
-           let l1 = NCicUtils.expand_local_context l1 in
-           let l2 = NCicUtils.expand_local_context l2 in
-           let metasenv, subst, to_restrict, _ =
-            List.fold_right2 
-             (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
-                try 
-                  let metasenv, subst = 
-                   unify status (*test_eq_only*) true metasenv subst context
-                    (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
-                     swap
-                  in
-                  metasenv, subst, to_restrict, i-1  
-                with UnificationFailure _ | Uncertain _ ->
-                  metasenv, subst, i::to_restrict, i-1)
-             l1 l2 (metasenv, subst, [], List.length l1)
-           in
-           if to_restrict <> [] then
-             let metasenv, subst, _, _ = 
-               NCicMetaSubst.restrict status metasenv subst n1 to_restrict
-             in
-               metasenv, subst
-           else metasenv, subst
-          with 
-           | Invalid_argument _ -> assert false
-           | NCicMetaSubst.MetaSubstFailure msg ->
-              try 
-                let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
-                let term1 = NCicSubstitution.subst_meta status lc1 term in
-                let term2 = NCicSubstitution.subst_meta status lc2 term in
-                  unify status test_eq_only metasenv subst context term1 term2 swap
-              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 status (*test_eq_only*) true metasenv subst context t1 
-                    t2 swap)
-                (metasenv,subst) l1 l2
-            with Invalid_argument _ -> 
-              raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
-       
-       | _, NCic.Meta (n, _) when is_locked n subst && not swap->
-           (let (metasenv, subst), i = 
-              match NCicReduction.whd status ~subst context t1 with
-              | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
-                 let metasenv, lambda_Mj =
-                   lambda_intros status metasenv subst context (List.length args)
-                    (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
-                 in
-                   unify status test_eq_only metasenv subst context 
-                    (C.Meta (i,l)) lambda_Mj false,
-                   i
-              | NCic.Meta (i,_) -> (metasenv, subst), i
-              | _ ->
-                 raise (UnificationFailure (lazy "Locked term vs non
-                  flexible term; probably not saturated enough yet!"))
-             in
-              let t1 = NCicReduction.whd status ~subst context t1 in
-              let j, lj = 
-                match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
-              in
+ else
+   match (t1,t2) with
+   | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl [] 
+   | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> 
+       prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
+       assert false 
+   | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
+       let a, b = if swap then b,a else a,b in
+       if NCicEnvironment.universe_leq status a b then metasenv, subst
+       else raise (UnificationFailure (mk_msg status 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 (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+   | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap -> 
+       if (not test_eq_only) then metasenv, subst
+       else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+   | (C.Sort (C.Type _), C.Sort C.Prop) when swap -> 
+       if (not test_eq_only) then metasenv, subst
+       else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+
+   | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
+   | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+       let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
+       unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
+   | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
+       let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
+       let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
+       let context = (name1, C.Def (s1,ty1))::context in
+       unify status test_eq_only metasenv subst context t1 t2 swap
+
+   | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
+      (try 
+       let l1 = NCicUtils.expand_local_context l1 in
+       let l2 = NCicUtils.expand_local_context l2 in
+       let metasenv, subst, to_restrict, _ =
+        List.fold_right2 
+         (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
+            try 
               let metasenv, subst = 
-                instantiate status test_eq_only metasenv subst context j lj t2 true
+               unify status (*test_eq_only*) true metasenv subst context
+                (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
+                 swap
               in
-              (* We need to remove the out_scope_tags to avoid propagation of
-                 them that triggers again the ad-hoc case *)
-              let subst =
-               List.map (fun (i,(tag,ctx,bo,ty)) ->
-                let tag =
-                 List.filter
-                  (function `InScope | `OutScope _ -> false | _ -> true) tag
-                in
-                  i,(tag,ctx,bo,ty)
-                ) subst
-              in
-              (try
-                let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
-                let term = eta_reduce status subst term in
-                let subst = List.filter (fun (j,_) -> j <> i) subst in
-                metasenv, ((i, (name, ctx, term, ty)) :: subst)
-              with Not_found -> assert false))
-       | NCic.Meta (n, _), _ when is_locked n subst && swap ->
-           unify status test_eq_only metasenv subst context t2 t1 false
-
-       | t, C.Meta (n,lc) when List.mem_assoc n subst -> 
-          let _,_,term,_ = NCicUtils.lookup_subst n subst in
-          let term = NCicSubstitution.subst_meta status lc term in
-            unify status test_eq_only metasenv subst context t term swap
-       | C.Meta (n,_), _ when List.mem_assoc n subst -> 
-            unify status test_eq_only metasenv subst context t2 t1 (not swap)
-
-       | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
-            let _,_,term,_ = NCicUtils.lookup_subst i subst in
-            let term = NCicSubstitution.subst_meta status l term in
-              unify status test_eq_only metasenv subst context t1 
-                (mk_appl status ~upto:(List.length args) term args) swap
-       | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
-            unify status test_eq_only metasenv subst context t2 t1 (not swap)
-
-       | C.Meta (n,_), C.Meta (m,lc') when 
-           let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
-           let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
-            (n < m && cc1 = cc2) ||
-             let len1 = List.length cc1 in
-             let len2 = List.length cc2 in
-              len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
-          instantiate status test_eq_only metasenv subst context m lc'
-            (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
-       | C.Meta (n,lc), C.Meta (m,lc') when
-          let _,_,tyn = NCicUtils.lookup_meta n metasenv in
-          let _,_,tym = NCicUtils.lookup_meta m metasenv in
-          let tyn = NCicSubstitution.subst_meta status lc tyn in
-          let tym = NCicSubstitution.subst_meta status lc tym in
-           match tyn,tym with
-              NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
-               NCicEnvironment.universe_lt status u1 u2
-            | _,_ -> false ->
-          instantiate status test_eq_only metasenv subst context m lc'
-            (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
-       | C.Meta (n,lc), t -> 
-          instantiate status test_eq_only metasenv subst context n lc 
-            (NCicReduction.head_beta_reduce status ~subst t) swap
-       | t, C.Meta (n,lc) -> 
-          instantiate status test_eq_only metasenv subst context n lc 
-           (NCicReduction.head_beta_reduce status ~subst t) (not swap)
-
-       (* higher order unification case *)
-       | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
-           (* this easy_case handles "(? ?) =?= (f a)", same number of 
-            * args, preferring the instantiation "f" over "\_.f a" for the
-            * metavariable in head position. Since the arguments of the meta
-            * are flexible, delift would ignore them generating a constant
-            * function even in the easy case above *)
-           let easy_case = 
-             match t2 with
-             | NCic.Appl (f :: f_args)
-               when 
-               List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
-                let mlen = List.length args in
-                let flen = List.length f_args in
-                let min_len = min mlen flen in
-                let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
-                let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
-                 (try 
-                    Some (List.fold_left2 
-                      (fun (m, s) t1 t2 -> 
-                        unify status test_eq_only m s context t1 t2 swap
-                      ) (metasenv,subst)
-                        ((NCicUntrusted.mk_appl meta mhe)::margs)
-                        ((NCicUntrusted.mk_appl f fhe)::fargs))
-                  with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
-                    None) 
-             | _ -> None
+              metasenv, subst, to_restrict, i-1  
+            with UnificationFailure _ | Uncertain _ ->
+              metasenv, subst, i::to_restrict, i-1)
+         l1 l2 (metasenv, subst, [], List.length l1)
+       in
+       if to_restrict <> [] then
+         let metasenv, subst, _, _ = 
+           NCicMetaSubst.restrict status metasenv subst n1 to_restrict
+         in
+           metasenv, subst
+       else metasenv, subst
+      with 
+       | Invalid_argument _ -> assert false
+       | NCicMetaSubst.MetaSubstFailure msg ->
+          try 
+            let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
+            let term1 = NCicSubstitution.subst_meta status lc1 term in
+            let term2 = NCicSubstitution.subst_meta status lc2 term in
+              unify status test_eq_only metasenv subst context term1 term2 swap
+          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 status (*test_eq_only*) true metasenv subst context t1 
+                t2 swap)
+            (metasenv,subst) l1 l2
+        with Invalid_argument _ -> 
+          raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
+   
+   | _, NCic.Meta (n, _) when is_locked n subst && not swap && not during_delift ->
+       (let (metasenv, subst), i = 
+          match NCicReduction.whd status ~subst context t1 with
+          | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
+             let metasenv, lambda_Mj =
+               lambda_intros status metasenv subst context (List.length args)
+                (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
+             in
+               unify status test_eq_only metasenv subst context 
+                (C.Meta (i,l)) lambda_Mj false,
+               i
+          | NCic.Meta (i,_) -> (metasenv, subst), i
+          | _ ->
+             raise (UnificationFailure (lazy "Locked term vs non
+              flexible term; probably not saturated enough yet!"))
+         in
+          let t1 = NCicReduction.whd status ~subst context t1 in
+          let j, lj = 
+            match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
+          in
+          let metasenv, subst = 
+            instantiate status test_eq_only metasenv subst context j lj t2 true
+          in
+          (* We need to remove the out_scope_tags to avoid propagation of
+             them that triggers again the ad-hoc case *)
+          let subst =
+           List.map (fun (i,(tag,ctx,bo,ty)) ->
+            let tag =
+             List.filter
+              (function `InScope | `OutScope _ -> false | _ -> true) tag
+            in
+              i,(tag,ctx,bo,ty)
+            ) subst
+          in
+          (try
+            let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+            let term = eta_reduce status subst term in
+            let subst = List.filter (fun (j,_) -> j <> i) subst in
+            metasenv, ((i, (name, ctx, term, ty)) :: subst)
+          with Not_found -> assert false))
+   | NCic.Meta (n, _), _ when is_locked n subst && swap ->
+      fo_unif0 during_delift status false test_eq_only metasenv subst context m2 m1
+
+   | _, C.Meta (n,lc) when List.mem_assoc n subst -> 
+      let _,_,term,_ = NCicUtils.lookup_subst n subst in
+      let term = NCicSubstitution.subst_meta status lc term in
+        fo_unif0 during_delift status swap test_eq_only metasenv subst context
+         m1 (false,term)
+   | C.Meta (n,_), _ when List.mem_assoc n subst -> 
+      fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
+
+   | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
+      let _,_,term,_ = NCicUtils.lookup_subst i subst in
+      let term = NCicSubstitution.subst_meta status l term in
+        fo_unif0 during_delift status swap test_eq_only metasenv subst context
+         m1 (false,mk_appl status ~upto:(List.length args) term args)
+   | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
+      fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
+
+   | C.Meta (n,_), C.Meta (m,lc') when 
+       let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
+       let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
+        (n < m && cc1 = cc2) ||
+         let len1 = List.length cc1 in
+         let len2 = List.length cc2 in
+          len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
+      instantiate status test_eq_only metasenv subst context m lc'
+        (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
+   | C.Meta (n,lc), C.Meta (m,lc') when
+      let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+      let _,_,tym = NCicUtils.lookup_meta m metasenv in
+      let tyn = NCicSubstitution.subst_meta status lc tyn in
+      let tym = NCicSubstitution.subst_meta status lc tym in
+       match tyn,tym with
+          NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+           NCicEnvironment.universe_lt u1 u2
+        | _,_ -> false ->
+      instantiate status test_eq_only metasenv subst context m lc'
+        (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
+   | C.Meta (n,lc), t -> 
+      instantiate status test_eq_only metasenv subst context n lc 
+        (NCicReduction.head_beta_reduce status ~subst t) swap
+   | t, C.Meta (n,lc) -> 
+      instantiate status test_eq_only metasenv subst context n lc 
+       (NCicReduction.head_beta_reduce status ~subst t) (not swap)
+
+   (* higher order unification case *)
+   | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
+       (* this easy_case handles "(? ?) =?= (f a)", same number of 
+        * args, preferring the instantiation "f" over "\_.f a" for the
+        * metavariable in head position. Since the arguments of the meta
+        * are flexible, delift would ignore them generating a constant
+        * function even in the easy case above *)
+       let easy_case = 
+         match t2 with
+         | NCic.Appl (f :: f_args)
+           when 
+           List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
+            let mlen = List.length args in
+            let flen = List.length f_args in
+            let min_len = min mlen flen in
+            let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
+            let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
+             (try 
+                Some (List.fold_left2 
+                  (fun (m, s) t1 t2 -> 
+                    unify status test_eq_only m s context t1 t2 swap
+                  ) (metasenv,subst)
+                    ((NCicUntrusted.mk_appl meta mhe)::margs)
+                    ((NCicUntrusted.mk_appl f fhe)::fargs))
+              with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
+                None) 
+         | _ -> None
+       in
+       (match easy_case with
+       | Some ms -> ms
+       | None ->
+           (* This case handles "(?_f ..ti..) =?= t2", abstracting every
+            * non flexible ti (delift skips local context items that are
+            * flexible) from t2 in two steps:
+            *  1) ?_f := \..xi.. .?
+            *  2) ?_f ..ti..  =?= t2 --unif_machines-->
+                  ?_f[..ti..] =?= t2 --instantiate-->
+                  delift [..ti..] t2 *)
+           let metasenv, lambda_Mj =
+             lambda_intros status metasenv subst context (List.length args)
+              (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
            in
-           (match easy_case with
-           | Some ms -> ms
-           | None ->
-               (* This case handles "(?_f ..ti..) =?= t2", abstracting every
-                * non flexible ti (delift skips local context items that are
-                * flexible) from t2 in two steps:
-                *  1) ?_f := \..xi.. .?
-                *  2) ?_f ..ti..  =?= t2 --unif_machines-->
-                      ?_f[..ti..] =?= t2 --instantiate-->
-                      delift [..ti..] t2 *)
-               let metasenv, lambda_Mj =
-                 lambda_intros status metasenv subst context (List.length args)
-                  (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
-               in
-               let metasenv, subst = 
-                 unify status test_eq_only metasenv subst context 
-                   (C.Meta (i,l)) lambda_Mj swap
-               in
-               let metasenv, subst = 
-                 unify status test_eq_only metasenv subst context t1 t2 swap
-               in
-               (try
-                 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
-                 let term = eta_reduce status subst term in
-                 let subst = List.filter (fun (j,_) -> j <> i) subst in
-                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
-               with Not_found -> assert false))
-
-       | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
-           unify status test_eq_only metasenv subst context t2 t1 (not swap)
-
-       (* processing this case here we avoid a useless small delta step *)
-       | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) 
-         when Ref.eq r1 r2 ->
-           let relevance = NCicEnvironment.get_relevance status r1 in
-           let metasenv, subst, _ = 
-             try
-               List.fold_left2 
-                 (fun (metasenv, subst, relevance) t1 t2 ->
-                    let b, relevance = 
-                      match relevance with b::tl -> b,tl | _ -> true, [] in
-                    let metasenv, subst = 
-                      try unify status test_eq_only metasenv subst context t1 t2
-                            swap
-                      with UnificationFailure _ | Uncertain _ when not b ->
-                        metasenv, subst
-                    in
-                      metasenv, subst, relevance)
-                 (metasenv, subst, relevance) tl1 tl2
-             with
-                Invalid_argument _ -> 
-                 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
-              | KeepReducing _ | KeepReducingThis _ -> assert false
-           in 
-             metasenv, subst
-
-       | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
-          C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
-           let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
-           let _,_,ty,_ = List.nth itl tyno in
-           let rec remove_prods ~subst context ty = 
-             let ty = NCicReduction.whd status ~subst context ty in
-             match ty with
-             | C.Sort _ -> ty
-             | C.Prod (name,so,ta) -> 
-                   remove_prods ~subst ((name,(C.Decl so))::context) ta
-             | _ -> assert false
+           let metasenv, subst = 
+             unify status test_eq_only metasenv subst context 
+               (C.Meta (i,l)) lambda_Mj swap
            in
-           let is_prop = 
-             match remove_prods ~subst [] ty with
-             | C.Sort C.Prop -> true
-             | _ -> false 
+           let metasenv, subst = 
+             unify status test_eq_only metasenv subst context t1 t2 swap
            in
-           (* if not (Ref.eq ref1 ref2) then 
-             raise (Uncertain (mk_msg status metasenv subst context t1 t2))
-           else*)
-             let metasenv, subst = 
-              unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
-             let metasenv, subst = 
-               try unify status test_eq_only metasenv subst context term1 term2 swap
-               with UnificationFailure _ | Uncertain _ when is_prop -> 
-                 metasenv, subst
-             in
-             (try
-              List.fold_left2 
-               (fun (metasenv,subst) t1 t2 -> 
-                  unify status test_eq_only metasenv subst context t1 t2 swap)
-               (metasenv, subst) pl1 pl2
-             with Invalid_argument _ -> assert false)
-       | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
-       | _ when norm1 && norm2 ->
-           if (could_reduce t1 || could_reduce t2) then
-            raise (Uncertain (mk_msg status metasenv subst context t1 t2))
-           else
-            raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-       | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
-     (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
-    in
-    let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
-     try fo_unif test_eq_only metasenv subst nt1 nt2
-     with
-      UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
-       raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
-    in
-    let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
-      if NCicUntrusted.metas_of_term status subst context t1 = [] &&
-         NCicUntrusted.metas_of_term status subst context t2 = [] 
-      then None 
-      else begin
-    (*D*) inside 'H'; try let rc =  
-     pp(lazy ("\nProblema:\n" ^
-        ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
-        ppterm status ~metasenv ~subst ~context t2));
-      let candidates = 
-        NCicUnifHint.look_for_hint status metasenv subst context t1 t2
-      in
-      let rec cand_iter = function
-        | [] -> None (* raise exc *)
-        | (metasenv,(c1,c2),premises)::tl -> 
-            pp (lazy ("\nProvo il candidato:\n" ^ 
-              String.concat "\n"
-                (List.map 
-                  (fun (a,b) ->
-                   ppterm status ~metasenv ~subst ~context a ^  " =?= " ^
-                   ppterm status ~metasenv ~subst ~context b) premises) ^
-              "\n-------------------------------------------\n"^
-              ppterm status ~metasenv ~subst ~context c1 ^  " = " ^
-              ppterm status ~metasenv ~subst ~context c2));
-            try 
-    (*D*) inside 'K'; try let rc =  
-              let metasenv,subst = 
-                fo_unif test_eq_only metasenv subst mt1 (false,c1) in
-              let metasenv,subst = 
-                fo_unif test_eq_only metasenv subst (false,c2) mt2 in
-              let metasenv,subst = 
-                List.fold_left 
-                  (fun (metasenv, subst) (x,y) ->
-                     unify status test_eq_only metasenv subst context x y false)
-                  (metasenv, subst) (List.rev premises)
-              in
-              pp(lazy("FUNZIONA!"));
-              Some (metasenv, subst)
-     (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
-            with
-             KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
-           | KeepReducingThis _ -> assert false
-      in
-        cand_iter candidates
-     (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
-      end
-    in
-    let put_in_whd m1 m2 =
-      NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
-      NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
-    in
-    let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
-      try fo_unif test_eq_only metasenv subst m1 m2
-      with 
-      | 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 status t1) (norm2,NCicReduction.unwind status t2)
+           (try
+             let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+             let term = eta_reduce status subst term in
+             let subst = List.filter (fun (j,_) -> j <> i) subst in
+             metasenv, ((i, (name, ctx, term, ty)) :: subst)
+           with Not_found -> assert false))
+
+   | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
+     fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
+
+   | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
+       let metasenv,subst =
+        fo_unif0 during_delift status swap test_eq_only metasenv subst context
+         (false,hd1) (false,hd2) in
+       let relevance =
+         match hd1 with
+         | C.Const r -> NCicEnvironment.get_relevance status r
+         | _ -> [] in
+       let metasenv, subst, _ = 
+         try
+           List.fold_left2 
+             (fun (metasenv, subst, relevance) t1 t2 ->
+                let b, relevance = 
+                  match relevance with b::tl -> b,tl | _ -> true, [] in
+                let metasenv, subst = 
+                  try unify status test_eq_only metasenv subst context t1 t2
+                        swap
+                  with UnificationFailure _ | Uncertain _ when not b ->
+                    metasenv, subst
+                in
+                  metasenv, subst, relevance)
+             (metasenv, subst, relevance) tl1 tl2
          with
-          | Some x -> x
-          | None -> 
-              match exn with 
-              | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
-              | Uncertain _ as exn -> raise exn
-              | _ -> assert false
-    in
+            Invalid_argument _ -> 
+             raise (Uncertain (mk_msg status metasenv subst context t1 t2))
+          | KeepReducing _ | KeepReducingThis _ -> assert false
+       in 
+         metasenv, subst
+
+   | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
+      C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
+       let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
+       let _,_,ty,_ = List.nth itl tyno in
+       let rec remove_prods ~subst context ty = 
+         let ty = NCicReduction.whd status ~subst context ty in
+         match ty with
+         | C.Sort _ -> ty
+         | C.Prod (name,so,ta) -> 
+               remove_prods ~subst ((name,(C.Decl so))::context) ta
+         | _ -> assert false
+       in
+       let is_prop = 
+         match remove_prods ~subst [] ty with
+         | C.Sort C.Prop -> true
+         | _ -> false 
+       in
+       (* if not (Ref.eq ref1 ref2) then 
+         raise (Uncertain (mk_msg status metasenv subst context t1 t2))
+       else*)
+         let metasenv, subst = 
+          unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
+         let metasenv, subst = 
+           try unify status test_eq_only metasenv subst context term1 term2 swap
+           with UnificationFailure _ | Uncertain _ when is_prop -> 
+             metasenv, subst
+         in
+         (try
+          List.fold_left2 
+           (fun (metasenv,subst) t1 t2 -> 
+              unify status test_eq_only metasenv subst context t1 t2 swap)
+           (metasenv, subst) pl1 pl2
+         with Invalid_argument _ -> assert false)
+   | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+   | _ when norm1 && norm2 ->
+       if (could_reduce status ~subst context t1 || could_reduce status ~subst context t2) then
+        raise (Uncertain (mk_msg status metasenv subst context t1 t2))
+       else
+        raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+   | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
+ (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
+
+and try_hints status swap test_eq_only metasenv subst context (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
+  if NCicUntrusted.metas_of_term status subst context t1 = [] &&
+     NCicUntrusted.metas_of_term status subst context t2 = [] 
+  then None 
+  else begin
+(*D*) inside 'H'; try let rc =  
+ pp(lazy ("\nProblema:\n" ^
+    ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
+    ppterm status ~metasenv ~subst ~context t2));
+  let candidates = 
+    NCicUnifHint.look_for_hint status metasenv subst context t1 t2
+  in
+  let rec cand_iter = function
+    | [] -> None (* raise exc *)
+    | (metasenv,(c1,c2),premises)::tl -> 
+        pp (lazy ("\nProvo il candidato:\n" ^ 
+          String.concat "\n"
+            (List.map 
+              (fun (a,b) ->
+               ppterm status ~metasenv ~subst ~context a ^  " =?= " ^
+               ppterm status ~metasenv ~subst ~context b) premises) ^
+          "\n-------------------------------------------\n"^
+          ppterm status ~metasenv ~subst ~context c1 ^  " = " ^
+          ppterm status ~metasenv ~subst ~context c2));
+        try 
+(*D*) inside 'K'; try let rc =  
+          let metasenv,subst = 
+           fo_unif false status swap test_eq_only metasenv subst context mt1 (false,c1) in
+          let metasenv,subst = 
+           fo_unif false status swap test_eq_only metasenv subst context (false,c2) mt2 in
+          let metasenv,subst = 
+            List.fold_left 
+              (fun (metasenv, subst) (x,y) ->
+                 unify status test_eq_only metasenv subst context x y false)
+              (metasenv, subst) (List.rev premises)
+          in
+          pp(lazy("FUNZIONA!"));
+          Some (metasenv, subst)
+ (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
+        with
+         KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
+       | KeepReducingThis _ -> assert false
+  in
+    cand_iter candidates
+ (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
+  end
+
+and fo_unif during_delift status swap test_eq_only metasenv subst context (norm1,t1 as nt1) (norm2,t2 as nt2)=
+ try fo_unif0 during_delift status swap test_eq_only metasenv subst context nt1 nt2
+ with
+  UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
+   raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
+
+and unify status test_eq_only metasenv subst context t1 t2 swap =
+ (*D*) inside 'U'; try let rc =
     let fo_unif_heads_and_cont_or_unwind_and_hints 
       test_eq_only metasenv subst m1 m2 cont hm1 hm2
      =
@@ -787,13 +794,13 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
            and makes unification stronger, but looks not frequent to me
            that heads unify but not the arguments and that an hints can fix 
            that *)
-        try fo_unif test_eq_only metasenv subst m1 m2, cont
+        try fo_unif false status swap test_eq_only metasenv subst context m1 m2, cont
         with 
         | UnificationFailure _ 
         | KeepReducing _ | Uncertain _ as exn ->
            let (t1,norm1),(t2,norm2) = hm1, hm2 in
            match 
-             try_hints metasenv subst 
+             try_hints status swap test_eq_only metasenv subst context
               (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
            with
             | Some x -> x, fun x -> x
@@ -846,7 +853,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
               try
                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
                 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
-                unif_machines metasenv subst (put_in_whd t1 t2)
+                unif_machines metasenv subst (put_in_whd status subst context t1 t2)
               with UnificationFailure _ | Uncertain _ when not b ->
                 metasenv, subst
           in
@@ -881,12 +888,12 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure msg
-           when could_reduce (NCicReduction.unwind status (fst m1))
-             || could_reduce (NCicReduction.unwind status (fst m2))
+           when could_reduce status ~subst context (NCicReduction.unwind status (fst m1))
+             || could_reduce status ~subst context (NCicReduction.unwind status (fst m2))
            -> raise (Uncertain msg)
       (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
      in
-     try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
+     try fo_unif_w_hints false status swap test_eq_only metasenv subst context (false,t1) (false,t2)
      with
       | KeepReducingThis (msg,tm1,tm2) ->
          (try 
@@ -903,15 +910,8 @@ and delift_type_wrt_terms status 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 status
-      ~unify:(fun m s c t1 t2 -> 
-         let ind = !indent in
-         let res = 
-           try Some (unify status false m s c t1 t2 false)
-           with UnificationFailure _ | Uncertain _ -> None
-         in
-         indent := ind; res)
-      metasenv subst context 0 (0,NCic.Ctx lc) t
+    NCicMetaSubst.delift status ~unify:(unify_for_delift status)
+      metasenv subst context (-1) (0,NCic.Ctx lc) t
    with
       NCicMetaSubst.MetaSubstFailure _
     | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t