X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=0e119f34b73949079b03cce21be67e0173f8d6ef;hb=a338e0effc313d4da419d6df91397232c24170d9;hp=fa3ba4988477dd0aa777a462b5e350a65eee9f5c;hpb=84a5fc74efc30a2b2fca18726cf988edd356353e;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index fa3ba4988..0e119f34b 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -17,6 +17,12 @@ exception AssertFailure of string Lazy.t;;
 
 let (===) x y = Pervasives.compare x y = 0 ;;
 
+let uncert_exc metasenv subst context t1 t2 = 
+  Uncertain (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 ^
@@ -39,105 +45,213 @@ let flexible l =
 
 exception WrongShape;;
 
-let eta_reduce after_beta_expansion after_beta_expansion_body
-     before_beta_expansion
- =
- try
-  match before_beta_expansion,after_beta_expansion_body with
-  | NCic.Appl l1, NCic.Appl l2 ->
-      let rec all_but_last check_last = function
-        | [] -> assert false
-        | [NCic.Rel 1] -> []
-        | [_] -> if check_last then raise WrongShape else []
-        | he::tl -> he::(all_but_last check_last tl)
-      in
-      let all_but_last check_last l =
-        match all_but_last check_last l with
-        | [] -> assert false
-        | [he] -> he
-        | l -> NCic.Appl l
-      in
-      let t = 
-        NCicSubstitution.subst (NCic.Sort NCic.Prop) (all_but_last true l2) in
-      let all_but_last = all_but_last false l in
-      if t = all_but_last then all_but_last else after_beta_expansion
-  | _ -> after_beta_expansion
- with WrongShape -> after_beta_expansion
+let eta_reduce = 
+  let delift_if_not_occur body orig =
+    try 
+        NCicSubstitution.psubst ~avoid_beta_redexes:true
+          (fun () -> raise WrongShape) [()] body
+    with WrongShape -> orig
+  in
+  function
+  | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
+      delift_if_not_occur hd orig
+  | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
+    when HExtlib.list_last l = NCic.Rel 1 ->
+       let body = 
+         let args, _ = HExtlib.split_nth (List.length l - 1) l in
+         NCic.Appl (hd::args)
+       in
+       delift_if_not_occur body orig
+  | t -> t
+;;
+ 
+module C = NCic;;
+module Ref = NReference;;
+
+let indent = ref "";;
+let inside c = indent := !indent ^ String.make 1 c;;
+let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
+
+(*
+let pp s = 
+  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+;;  
+*)
+
+let pp _ = ();;
+
+let fix_sorts swap metasenv subst context meta t =
+  let rec aux () = function
+    | NCic.Sort (NCic.Type u) as orig ->
+        if swap then
+         match NCicEnvironment.sup u with
+         | None -> prerr_endline "no sup for" ;
+            raise (fail_exc metasenv subst context meta t)
+         | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
+        else
+         NCic.Sort (NCic.Type (
+           match NCicEnvironment.sup NCicEnvironment.type0 with 
+           | Some x -> x 
+           | _ -> assert false))
+    | NCic.Meta _ as orig -> orig
+    | t -> NCicUtils.map (fun _ _ -> ()) () aux t
+  in
+    aux () t
 ;;
 
-let rec beta_expand num test_equality_only metasenv subst context t arg =
-  let rec aux (n,context as k) (metasenv, subst as acc) t' =
+let rec beta_expand num test_eq_only swap metasenv subst context t arg =
+  let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
    try
     let metasenv, subst =
-     unify (* test_equality_only *) metasenv subst context
-      (NCicSubstitution.lift n arg) t'
+     if swap then
+      unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
+     else
+      unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
     in
-     (metasenv, subst), C.Rel (1 + n)
+     (metasenv, subst), NCic.Rel (1 + n)
    with Uncertain _ | UnificationFailure _ ->
        match t' with
-       | NCic.Rel m  -> 
-           (metasenv, subst), if m <= n then NCic.Rel m else NCic.Rel (m+1)
+       | NCic.Rel m as orig -> 
+           (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
        (* andrea: in general, beta_expand can create badly typed
         terms. This happens quite seldom in practice, UNLESS we
         iterate on the local context. For this reason, we renounce
         to iterate and just lift *)
        | NCic.Meta (i,(shift,lc)) ->
            (metasenv,subst), NCic.Meta (i,(shift+1,lc))
+       | NCic.Prod (name, src, tgt) as orig ->
+           let (metasenv, subst), src1 = aux (n,context,true) acc src in 
+           let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
+           let ms, tgt1 = aux k (metasenv, subst) tgt in 
+           if src == src1 && tgt == tgt1 then ms, orig else
+           ms, NCic.Prod (name, src1, tgt1)
        | t -> 
            NCicUntrusted.map_term_fold_a 
-             (fun e (n,ctx) -> n+i,e::ctx) k aux acc t
+             (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
 
   in
   let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
   let fresh_name = "Hbeta" ^ string_of_int num in
-  let (metasenv,subst), t = aux (0, context) (metasenv, subst) t in
-  let t = eta_reduce (C.Lambda (fresh_name,argty,t)) t t in
-  metasenv, subst, t
+  let (metasenv,subst), t1 = 
+    aux (0, context, test_eq_only) (metasenv, subst) t in
+  let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
+  try 
+    ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
+    metasenv, subst, t2
+  with NCicTypeChecker.TypeCheckerFailure _ -> 
+    metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
 
-and beta_expand_many test_equality_only metasenv subst context t args ugraph =
+and beta_expand_many test_equality_only swap metasenv subst context t args =
+(* (*D*)  inside 'B'; try let rc = *)
+  pp (lazy (String.concat ", "
+     (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
+     args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
   let _, subst, metasenv, hd =
     List.fold_right
       (fun arg (num,subst,metasenv,t) ->
-         let subst, metasenv, t =
-           beta_expand num test_equality_only metasenv subst context t arg
+         let metasenv, subst, t =
+           beta_expand num test_equality_only swap metasenv subst context t arg
          in
            num+1,subst,metasenv,t)
       args (1,subst,metasenv,t) 
   in
+  pp (lazy ("Head syntesized by b-exp: " ^ 
+    NCicPp.ppterm ~metasenv ~subst ~context hd));
     metasenv, subst, hd
+(* (*D*)  in outside (); rc with exn -> outside (); raise exn *)
 
 and instantiate test_eq_only metasenv subst context n lc t swap =
-  let unif m s c t1 t2 =
-    if swap then unify m s c t2 t1 else unify m s c t1 t2
-  in
-  let ty_t = 
-    try NCicTypeChecker.typeof ~subst ~metasenv context t 
-    with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ (*D*)  inside 'I'; try let rc =  
+         pp (lazy(string_of_int n ^ " :=?= "^
+           NCicPp.ppterm ~metasenv ~subst ~context t));
+  let unify test_eq_only m s c t1 t2 = 
+    if swap then unify test_eq_only m s c t2 t1 
+    else unify test_eq_only m s c t1 t2
   in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  let ty = NCicSubstitution.subst_meta lc ty in
-  let metasenv, subst = unify metasenv susbt context ty ty_t in
+  let metasenv, subst, t = 
+    match ty with 
+    | NCic.Implicit (`Typeof _) -> 
+       metasenv,subst, t
+         (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
+    | _ ->
+       pp (lazy (
+         "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
+          NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
+          NCicPp.ppmetasenv ~subst metasenv));
+       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 metasenv subst context (NCic.Meta (n,lc)) t
+           in
+           if ft == t then 
+             (prerr_endline ( ("ILLTYPED: " ^ 
+                NCicPp.ppterm ~metasenv ~subst ~context t
+            ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
+            NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
+            NCicPp.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.TypeCheckerFailure msg ->
+              pp msg; assert false
+       in
+       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)); 
+       let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
+       metasenv, subst, t
+  in
+         pp (lazy(string_of_int n ^ " := 111 = "^
+           NCicPp.ppterm ~metasenv ~subst ~context t));
   let (metasenv, subst), t = 
-    NCicMetaSubst.delift metasenv subst context n lc t
+    try NCicMetaSubst.delift metasenv subst context n lc t
+    with NCicMetaSubst.Uncertain msg -> 
+         pp (lazy ("delift fails: " ^ Lazy.force msg));
+         raise (Uncertain msg)
+    | NCicMetaSubst.MetaSubstFailure msg -> 
+         pp (lazy ("delift fails: " ^ Lazy.force msg));
+         raise (UnificationFailure msg)
   in
+         pp (lazy(string_of_int n ^ " := 222 = "^
+           NCicPp.ppterm ~metasenv ~subst ~context:ctx t
+         ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv));
   (* Unifying the types may have already instantiated n. *)
   try
-    let _, _,oldt,_ = CicUtil.lookup_subst n subst in
+    let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
     let oldt = NCicSubstitution.subst_meta lc oldt in
+    let t = NCicSubstitution.subst_meta lc t in
     (* conjecture: always fail --> occur check *)
     unify test_eq_only metasenv subst context oldt t
-  with CicUtil.Subst_not_found _ -> 
+  with NCicUtils.Subst_not_found _ -> 
     (* by cumulativity when unify(?,Type_i) 
      * we could ? := Type_j with j <= i... *)
     let subst = (n, (name, ctx, t, ty)) :: subst in
+    pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
+      ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
     let metasenv = 
       List.filter (fun (m,_) -> not (n = m)) metasenv 
     in
-    subst, metasenv
+    metasenv, subst
+ (*D*)  in outside(); rc with exn -> outside (); raise exn 
 
-and unify metasenv subst context t1 t2 =
- let rec aux test_eq_only metasenv subst context t1 t2 =
+and unify test_eq_only metasenv subst context t1 t2 =
+ (*D*) inside 'U'; try let rc = 
    let fo_unif test_eq_only metasenv subst t1 t2 =
+    (*D*) inside 'F'; try let rc =  
+     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
+         NCicPp.ppterm ~metasenv ~subst ~context t2));
      if t1 === t2 then
        metasenv, subst
      else
@@ -154,13 +268,13 @@ and unify 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 = aux true metasenv subst context s1 s2 in
-           aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
+           let metasenv, subst = unify true metasenv subst context s1 s2 in
+           unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
-           let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
-           let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
+           let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
+           let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
            let context = (name1, C.Def (s1,ty1))::context in
-           aux test_eq_only metasenv subst context t1 t2
+           unify test_eq_only metasenv subst context t1 t2
 
        | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
           (try 
@@ -170,17 +284,21 @@ and unify metasenv subst context t1 t2 =
             List.fold_right2 
              (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
                 try 
-                  aux test_eq_only metasenv subst context 
-                    (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2),
-                  to_restrict, i-1  
+                  let metasenv, subst = 
+                   unify test_eq_only metasenv subst context 
+                    (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
+                  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
-           let metasenv, subst, _ = 
-             NCicMetaSubst.restrict metasenv subst n1 to_restrict
-           in
-             metasenv, subst
+           if to_restrict <> [] then
+             let metasenv, subst, _ = 
+               NCicMetaSubst.restrict metasenv subst n1 to_restrict
+             in
+               metasenv, subst
+           else metasenv, subst
           with 
            | Invalid_argument _ -> assert false
            | NCicMetaSubst.MetaSubstFailure msg ->
@@ -188,113 +306,99 @@ and unify metasenv subst context t1 t2 =
                 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
                 let term1 = NCicSubstitution.subst_meta lc1 term in
                 let term2 = NCicSubstitution.subst_meta lc2 term in
-                  aux test_eq_only metasenv subst context term1 term2
+                  unify test_eq_only metasenv subst context term1 term2
               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
 
        | C.Meta (n,lc), t -> 
-           try 
+           (try 
              let _,_,term,_ = NCicUtils.lookup_subst n subst in
              let term = NCicSubstitution.subst_meta lc term in
-               aux test_eq_only metasenv subst context term t
+               unify test_eq_only metasenv subst context term t
            with NCicUtils.Subst_not_found _-> 
-             instantiate test_eq_only metasenv subst context n lc t false
+             instantiate test_eq_only metasenv subst context n lc t false)
 
        | t, C.Meta (n,lc) -> 
-           try 
+           (try 
              let _,_,term,_ = NCicUtils.lookup_subst n subst in
              let term = NCicSubstitution.subst_meta lc term in
-               aux test_eq_only metasenv subst context t term
+               unify test_eq_only metasenv subst context t term
            with NCicUtils.Subst_not_found _-> 
-             instantiate test_eq_only metasenv subst context n lc t true
+             instantiate test_eq_only metasenv subst context n lc t true)
 
        | 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 l term in
-              aux test_eq_only metasenv subst context (mk_appl term args) t2
+              unify test_eq_only metasenv subst context (mk_appl term args) t2
 
        | _, 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 l term in
-              aux test_eq_only metasenv subst context t1 (mk_appl term args)
+              unify test_eq_only metasenv subst context t1 (mk_appl term args)
 
        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
           NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
-            try
+            (try
               List.fold_left2 
                 (fun (metasenv, subst) t1 t2 ->
-                  aux test_eq_only metasenv subst context t1 t2)
+                  unify test_eq_only metasenv subst context t1 t2)
                 (metasenv,subst) l1 l2
             with Invalid_argument _ -> 
-              raise (fail_exc metasenv subst context t1 t2)
+              raise (fail_exc metasenv subst context t1 t2))
 
        | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
            (* we verify that none of the args is a Meta, 
               since beta expanding w.r.t a metavariable makes no sense  *)
-              let subst, metasenv, beta_expanded =
+              let metasenv, subst, beta_expanded =
                 beta_expand_many 
-                  test_equality_only metasenv subst context t2 args ugraph 
+                  test_eq_only false 
+                  metasenv subst context t2 args
               in
-                aux test_eq_only metasenv subst context 
+                unify test_eq_only metasenv subst context 
                   (C.Meta (i,l)) beta_expanded 
+
        | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
-                 let subst,metasenv,beta_expanded =
-                   beta_expand_many 
-                     test_equality_only 
-                     metasenv subst context t1 args ugraph 
-                 in
-                   fo_unif_subst test_equality_only subst context metasenv 
-                     (C.Meta (i,l)) beta_expanded ugraph1
-          | _,_ ->
-.......       
+              let metasenv, subst, beta_expanded =
+                beta_expand_many 
+                  test_eq_only true 
+                  metasenv subst context t1 args
+              in
+                unify test_eq_only metasenv subst context 
+                  beta_expanded (C.Meta (i,l))
+
+       (* 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 && 
-             List.length (E.get_relevance r1) >= List.length tl1) ->
-         let relevance = E.get_relevance r1 in
-         let relevance = match r1 with
+         when Ref.eq r1 r2 ->
+           let relevance = NCicEnvironment.get_relevance r1 in
+           let relevance = match r1 with
              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
                  let _,relevance = HExtlib.split_nth lno relevance in
                    HExtlib.mk_list false lno @ relevance
              | _ -> relevance
-         in
-	 let fail = ref ~-1 in
-         let res = (try
-             HExtlib.list_forall_default3
-              (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
-              tl1 tl2 true relevance
-            with Invalid_argument _ -> false)
-         in res
-	 (* if res then true
-         else
-	   let relevance = get_relevance_p ~subst context _hd1 tl1 in
-	   let _,relevance = HExtlib.split_nth !fail relevance in
-	   let b,relevance = (match relevance with
-	     | [] -> assert false
-	     | b::tl -> b,tl) in
-	   let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
-	   let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
-	   if (not b) then
-             (dance ();
-	      try
-               HExtlib.list_forall_default3
-                (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
-                tl1 tl2 true relevance
-             with Invalid_argument _ -> false)
-	   else false *)
-       | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
-           aux test_eq_only context hd1 hd2 &&
-	   let relevance = get_relevance ~subst context hd1 tl1 in
-           (try
-             HExtlib.list_forall_default3
-              (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
-              tl1 tl2 true relevance
-            with Invalid_argument _ -> false)
+           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 test_eq_only metasenv subst context t1 t2
+                      with UnificationFailure _ | Uncertain _ when not b ->
+                        metasenv, subst
+                    in
+                      metasenv, subst, relevance)
+                 (metasenv, subst, relevance) tl1 tl2
+             with Invalid_argument _ -> 
+               raise (uncert_exc metasenv subst context t1 t2)
+           in 
+             metasenv, subst
 
        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
           C.Match (ref2,outtype2,term2,pl2)) ->
-	   let _,_,itl,_,_ = E.get_checked_indtys ref1 in
+	   let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
 	   let _,_,ty,_ = List.nth itl tyno in
 	   let rec remove_prods ~subst context ty = 
-             let ty = whd ~subst context ty in
+             let ty = NCicReduction.whd ~subst context ty in
              match ty with
              | C.Sort _ -> ty
 	     | C.Prod (name,so,ta) -> 
@@ -307,7 +411,7 @@ and unify metasenv subst context t1 t2 =
              | _ -> false 
            in
 	   let rec remove_prods ~subst context ty = 
-             let ty = whd ~subst context ty in
+             let ty = NCicReduction.whd ~subst context ty in
              match ty with
              | C.Sort _ -> ty
 	     | C.Prod (name,so,ta) -> 
@@ -318,96 +422,104 @@ and unify metasenv subst context t1 t2 =
              raise (uncert_exc metasenv subst context t1 t2) 
            else
              let metasenv, subst = 
-               aux test_eq_only metasenv subst context outtype1 outtype2 in
+               unify test_eq_only metasenv subst context outtype1 outtype2 in
              let metasenv, subst = 
-               try aux test_eq_only metasenv subst context term1 term2 
+               try unify test_eq_only metasenv subst context term1 term2 
                with UnificationFailure _ | Uncertain _ when is_prop -> 
                  metasenv, subst
              in
-             try
+             (try
               List.fold_left2 
-               (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
+               (fun (metasenv,subst) -> 
+                  unify test_eq_only metasenv subst context)
                (metasenv, subst) pl1 pl2
              with Invalid_argument _ -> 
-               raise (uncert_exc metasenv subst context t1 t2)
+               raise (uncert_exc metasenv subst context t1 t2))
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
+     (*D*)  in outside(); rc with exn -> outside (); raise exn 
     in
-    let rec unif_machines metasenv subst = function
-      | ((k1,e1,NCic.Meta _ as t1,s1 as m1),(k2,e2,t2,s2 as m2),delta)
-      | ((k1,e1,t1,s1 as m1),(k2,e2,NCic.Meta _ as t2,s2 as m2),delta) ->
-          try 
-            fo_unif test_eq_only metasenv subst (R.unwind m1) (R.unwind m2)
-          with UnificationFailure _ | Uncertain _ when delta > 0 ->
-            let delta = delta - 1 in 
-            let red = R.reduce ~delta ~subst context in
-            unif_machines metasenv subst (red m1,red m2,delta)
-      | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
-        try
-          let metasenv, subst = 
-            fo_unif test_eq_only metasenv subst
-              (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[]))
-          in
-          let relevance =
+    let height_of = function
+     | NCic.Const (Ref.Ref (_,Ref.Def h)) 
+     | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
+     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) 
+     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
+     | _ -> 0
+    in
+    let put_in_whd m1 m2 =
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m2
+    in
+    let small_delta_step 
+      ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
+    =
+     assert (not (norm1 && norm2));
+     if norm1 then
+      x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
+     else if norm2 then
+      NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
+     else 
+      let h1 = height_of t1 in 
+      let h2 = height_of t2 in
+      let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
+      NCicReduction.reduce_machine ~delta ~subst context m1,
+      NCicReduction.reduce_machine ~delta ~subst context m2
+    in
+    let rec unif_machines metasenv subst = 
+      function
+      | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
+     (*D*) inside 'M'; try let rc = 
+(*
+         pp (lazy((if are_normal then "*" else " ") ^ " " ^
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
+           " === " ^ 
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
+*)
+          let relevance = [] (* TO BE UNDERSTOOD 
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
-            | _ -> [] in
-          try
-            let rec check_stack f l1 l2 r a =
-              match l1,l2,r with
-              | x1::tl1, x2::tl2, r::tr ->
-                  check_stack f tl1 tl2 tr (f x1 x2 r a)
-              | x1::tl1, x2::tl2, [] ->
-                  check_stack f tl1 tl2 tr (f x1 x2 true a)
-              | [], [], _ -> a
-              | _ -> raise (Invalid_argument "check_stack")
-            in
-            check_stack
-              (fun t1 t2 b (metasenv,subst) ->
-                try
-                  let t1 = RS.from_stack t1 in
-                  let t2 = RS.from_stack t2 in
-                  unif_machines metasenv subst (small_delta_step t1 t2)
-                with UnificationFailure _ | Uncertain _ when not b ->
-                  metasenv, subst)
-              s1 s2 relevance (metasenv,subst)
-          with Invalid_argument _ -> 
-            raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm
-            ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm
-            ~metasenv ~subst ~context (R.unwind m2))))
-        with UnificationFailure _ | Uncertain _ when delta > 0 ->
-          let delta = delta - 1 in 
-          let red = R.reduce ~delta ~subst context in
-          unif_machines metasenv subst (red m1,red m2,delta)
-     in
-     let height_of = function
-      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
-      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
-      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) 
-      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
-      | NCic.Meta _ -> max_int
-      | _ -> 0
-     in
-     let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
-       let h1 = height_of t1 in 
-       let h2 = height_of t2 in
-       let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
-       R.reduce ~delta ~subst context m1,
-       R.reduce ~delta ~subst context m2,
-       delta
+            | _ -> [] *) in
+          let unif_from_stack t1 t2 b metasenv subst =
+              try
+                let t1 = NCicReduction.from_stack t1 in
+                let t2 = NCicReduction.from_stack t2 in
+                unif_machines metasenv subst (put_in_whd t1 t2)
+              with UnificationFailure _ | Uncertain _ when not b ->
+                metasenv, subst
+          in
+          let rec check_stack l1 l2 r (metasenv, subst) =
+            match l1,l2,r with
+            | x1::tl1, x2::tl2, r::tr ->
+                check_stack tl1 tl2 tr 
+                  (unif_from_stack x1 x2 r metasenv subst)
+            | x1::tl1, x2::tl2, [] ->
+                check_stack tl1 tl2 [] 
+                  (unif_from_stack x1 x2 true metasenv subst)
+            | l1, l2, _ -> 
+                fo_unif test_eq_only metasenv subst
+                   (NCicReduction.unwind (k1,e1,t1,List.rev l1)) 
+                   (NCicReduction.unwind (k2,e2,t2,List.rev l2))
+          in
+        try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
+        with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
+	    unif_machines metasenv subst (small_delta_step m1 m2)
+      (*D*)  in outside(); rc with exn -> outside (); raise exn 
      in
      try fo_unif test_eq_only metasenv subst t1 t2
-     with UnificationFailure msg |Uncertain msg as exn -> 
+     with UnificationFailure msg | Uncertain msg as exn -> 
        try 
          unif_machines metasenv subst 
-          (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
+          (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
        with 
        | UnificationFailure _ -> raise (UnificationFailure msg)
        | Uncertain _ -> raise exn
- in
-  aux false metasenv subst context t1 t2
+ (*D*)  in outside(); rc with exn -> outside (); raise exn 
 ;;
 
+let unify = 
+  indent := "";      
+  unify false;;
+
 
 
 (*