1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,

   but the case Meta(i) vs (Appl (Meta(j),...)) that reduces to Meta(i) was
   not. As a result, a tempeted self assegniment yielded strange errors.
   Fixed by more aggressively unwinding the subst during fo_unif.
2) Major re-organization of the code to gain some speed in Oliboni's stuff.
   The idea is that of introducing a new internal exception KeepReducing
   used to signal that, after a fo_unif, it still makes sense to fall back
   to machines. Only if it does not it makes sense to distinguish between
   Failures and Uncertain and the latter test can now be implemented more
   lazily w.r.t. the old version that used to call metas_of_term on the
   unwinded machines (that are potentially HUGE).
   With this modification, all Oliboni's tests terminate, even if they are
   still very slow compared to the height=0 strategy. Moreover, the tests
   show that unification on closed terms can still be 4x slower than conversion,
   which is partially unexpected.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 5353363d507bcbac84e6e939daa89dc0a343c038..d95415d99d64d42c6e5565eb0b33bdd996fafb3a 100644 (file)
--- 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
@@ -210,7 +204,9 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
          assert(has_tag ((=)`IsSort) tags); 
          metasenv, subst, t
     | _ ->
-       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 
@@ -356,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
@@ -371,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)) ->
@@ -421,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 = 
@@ -462,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
@@ -492,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 
@@ -525,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 
@@ -564,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
 
@@ -587,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
@@ -603,13 +613,15 @@ 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 =  
      pp(lazy ("\nProblema:\n" ^
         NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
@@ -632,9 +644,9 @@ 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) ->
@@ -645,8 +657,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
               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 
@@ -667,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
@@ -711,43 +722,48 @@ 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 -> 
-(*
-       prerr_endline "PROBLEMA";
-       prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1);
-       prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2);
-*)
-       let (t1,_ as t1m),(t2,_ as t2m) = put_in_whd (0,[],t1,[]) (0,[],t2,[]) in
-       match 
-         try_hints metasenv subst 
-           (NCicReduction.unwind t1) (NCicReduction.unwind t2) 
-       with
-       | Some x -> x
-       | None -> 
-          try 
-            unif_machines metasenv subst (t1m, t2m)
-          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
@@ -762,7 +778,9 @@ and delift_type_wrt_terms rdb metasenv subst context t args =
          in
          indent := ind; res)
       metasenv subst context 0 (0,NCic.Ctx lc) t
-   with NCicMetaSubst.MetaSubstFailure _ -> (metasenv, subst), t
+   with
+      NCicMetaSubst.MetaSubstFailure _
+    | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
   in
    metasenv, subst, t
 ;;