Big bug fixed: in the case t <?= ?1, the instantiation ?1 := t was generated

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 9c2dde84b45dd1aef507d2a6a00d3c8dcfb8e818..b9f87cf9a14a4f4b3e27ecb9d2524cc90fb25471 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -92,15 +92,26 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
           raise (UnificationFailure (sprintf
             "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."
             (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
-   | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
+   | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
        fo_unif_subst subst context metasenv t2 t1
    | (C.Meta (n,l), t)   
    | (t, C.Meta (n,l)) ->
+       let swap =
+        match t1,t2 with
+           C.Meta (n,_), C.Meta (m,_) when n < m -> false
+         | _, C.Meta _ -> false
+         | _,_ -> true
+       in
+       let lower = fun x y -> if swap then y else x in
+       let upper = fun x y -> if swap then x else y in
+       let fo_unif_subst_ordered subst context metasenv m1 m2 =
+          fo_unif_subst subst context metasenv (lower m1 m2) (upper m1 m2)
+       in
        let subst'',metasenv' =
         try
          let oldt = (List.assoc n subst) in
          let lifted_oldt = S.lift_meta l oldt in
-          fo_unif_subst subst context metasenv lifted_oldt t
+          fo_unif_subst_ordered subst context metasenv t lifted_oldt
         with Not_found ->
          let t',metasenv',subst' =
           try
@@ -109,14 +120,14 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
          in
-          (n, t')::subst', metasenv'
+         (n, t')::subst', metasenv'
        in
         let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
         (try
           let tyt =
             type_of_aux' metasenv' subst'' context t
           in
-           fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
+           fo_unif_subst subst'' context metasenv' tyt (S.lift_meta l meta_type)
         with AssertFailure _ ->
           (* TODO huge hack!!!!
            * we keep on unifying/refining in the hope that the problem will be