X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=3c8b077297fd5ad8da82700f4dd081fade124c19;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=c23aada3d5b40909b284ce40af0adf9aec04c9fc;hpb=45ca0fe459f75004c26e133d4cbf4659b62fd4df;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index c23aada3d..3c8b07729 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -56,25 +56,34 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
  let module S = CicSubstitution in
   match (t1, t2) with
      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
-       let ok =
+       let ok,subst,metasenv =
         List.fold_left2
-         (fun b t1 t2 ->
-           b &&
+         (fun (b,subst,metasenv) t1 t2 ->
+           if b then true,subst,metasenv else
             match t1,t2 with
                None,_
-             | _,None -> true
+             | _,None -> true,subst,metasenv
              | Some t1', Some t2' ->
                 (* First possibility:  restriction    *)
                 (* Second possibility: unification    *)
                 (* Third possibility:  convertibility *)
-                R.are_convertible subst context t1' t2'
-         ) true ln lm
+                if R.are_convertible subst context t1' t2' then
+                 true,subst,metasenv
+                else
+                 (try
+                   let subst,metasenv =
+                    fo_unif_subst subst context metasenv t1' t2'
+                   in
+                    true,subst,metasenv
+                 with
+                  Not_found -> false,subst,metasenv)
+         ) (true,subst,metasenv) ln lm
        in
         if ok then
           subst,metasenv
         else
           raise (UnificationFailure (sprintf
-            "Error trying to unify %s with %s: the algorithm only tried to check convertibility of the two substitutions"
+            "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
             (CicPp.ppterm t1) (CicPp.ppterm t2)))
    | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
        fo_unif_subst subst context metasenv t2 t1
@@ -97,13 +106,17 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
             type_of_aux' metasenv' subst'' context t
           in
            fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
-        with CicTypeChecker.SortExpectedMetaFound _ ->
+        with AssertFailure _ ->
           (* TODO huge hack!!!!
            * we keep on unifying/refining in the hope that the problem will be
            * eventually solved. In the meantime we're breaking a big invariant:
            * the terms that we are unifying are no longer well typed in the
            * current context (in the worst case we could even diverge)
            *)
+(*
+prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
+prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
+*)
           (subst'', metasenv'))
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
@@ -131,7 +144,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive constructors"
         (CicPp.ppterm t1) (CicPp.ppterm t1)))
-   | (C.Implicit, _) | (_, C.Implicit) ->  assert false
+   | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
    | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->