Unification improved to handle beta-delta conversion in most cases.

This is required to match Coq's unification for the porting of setoids.ma.

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 683b3f9df8cdae48a073e85d3e61a69ef81b8386..437d541ea3617a66d77e3b311bd186fe8bfecc2f 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -669,26 +669,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        in
          fo_unif_subst test_equality_only subst context metasenv 
            beta_expanded (C.Meta (i,l)) ugraph1
-   | (C.Sort _ ,_) | (_, C.Sort _)
-   | (C.Const _, _) | (_, C.Const _)
-   | (C.MutInd  _, _) | (_, C.MutInd _)
-   | (C.MutConstruct _, _) | (_, C.MutConstruct _)
-   | (C.Fix _, _) | (_, C.Fix _) 
-   | (C.CoFix _, _) | (_, C.CoFix _) -> 
-       if t1 = t2 then
-         subst, metasenv, ugraph
-       else 
-         let b,ugraph1 = 
-           R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
-         in
-           if b then 
-             subst, metasenv, ugraph1
-           else
-             raise
-                (UnificationFailure (lazy (sprintf
-                  "Can't unify %s with %s because they are not convertible"
-                  (CicMetaSubst.ppterm subst t1) 
-                  (CicMetaSubst.ppterm subst t2))))
+(* The following idea could be exploited again; right now we have no
+   longer any example requiring it
    | (C.Prod _, t2) ->
        let t2' = R.whd ~subst context t2 in
        (match t2' with
@@ -708,12 +690,38 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                    "Can't unify %s with %s because they are not convertible"
                    (CicMetaSubst.ppterm subst t1) 
                    (CicMetaSubst.ppterm subst t2)))))
+*)
    | (_,_) ->
-       raise (UnificationFailure (lazy "10"))
-         (* (sprintf
+     (* delta-beta reduction should almost never be a problem for
+        unification since:
+         1. long computations require iota reduction
+         2. it is extremely rare that a close term t1 (that could be unified
+            to t2) beta-delta reduces to t1' while t2 does not beta-delta
+            reduces in the same way. This happens only if one meta of t2
+            occurs in head position during beta reduction. In this unluky
+            case too much reduction will be performed on t1 and unification
+            will surely fail. *)
+     let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
+     let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
+      if t1 = t1' && t2 = t2' then
+       raise (UnificationFailure
+        (lazy 
+          (sprintf
             "Can't unify %s with %s because they are not convertible"
             (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2))) *)
+            (CicMetaSubst.ppterm subst t2))))
+      else
+       try
+        fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
+       with
+          UnificationFailure _
+        | Uncertain _ ->
+           raise (UnificationFailure
+            (lazy 
+              (sprintf
+                "Can't unify %s with %s because they are not convertible"
+                (CicMetaSubst.ppterm subst t1) 
+                (CicMetaSubst.ppterm subst t2))))
 
 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
  exp_named_subst1 exp_named_subst2 ugraph