X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=c56fb087423c457c3c599053544ec4e1ce0ab4f4;hb=78cf601fd8b8dbb386b0db315dcbfdbe8256c15f;hp=fb1ca113f23e7f3b40035b8c68f47cd74bf9048d;hpb=22d6cd4a655dcb53de42877ea3faf5432e201111;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index fb1ca113f..c56fb0874 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -59,6 +59,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
   match (t1, t2) with
      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
        let ok,subst,metasenv =
+       try
         List.fold_left2
          (fun (b,subst,metasenv) t1 t2 ->
            if b then true,subst,metasenv else
@@ -80,22 +81,39 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
                  with
                   Not_found -> false,subst,metasenv)
          ) (true,subst,metasenv) ln lm
+       with
+        Invalid_argument _ ->
+         raise (UnificationFailure (sprintf
+           "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
        in
         if ok then
           subst,metasenv
         else
           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."
-            (CicPp.ppterm t1) (CicPp.ppterm t2)))
-   | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
+            (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+   | (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 fo_unif_subst =
+        let (lower,upper) =
+         match t1,t2 with
+            C.Meta (n,_), C.Meta (m,_) when n < m ->
+             (fun t1 t2 -> t1), (fun t1 t2 -> t2)
+          | _, C.Meta _ ->
+             (fun t1 t2 -> t1), (fun t1 t2 -> t2)
+          | _,_ ->
+             (fun t1 t2 -> t2), (fun t1 t2 -> t1)
+        in
+         fun 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 subst context metasenv t lifted_oldt
         with Not_found ->
          let t',metasenv',subst' =
           try
@@ -111,7 +129,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
           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
@@ -132,7 +150,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different constants"
-        (CicPp.ppterm t1) (CicPp.ppterm t2)))
+        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
       if UriManager.eq uri1 uri2 && i1 = i2 then
        fo_unif_subst_exp_named_subst subst context metasenv
@@ -140,7 +158,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive principles"
-        (CicPp.ppterm t1) (CicPp.ppterm t1)))
+        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
      C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
@@ -149,7 +167,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive constructors"
-        (CicPp.ppterm t1) (CicPp.ppterm t1)))
+        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
    | (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
@@ -181,15 +199,20 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
              fo_unif_l subst' metasenv' (l1,l2)
        in
         fo_unif_l subst metasenv (lr1, lr2) 
-   | (C.MutCase (_,_,outt1,t1,pl1), C.MutCase (_,_,outt2,t2,pl2))->
+   | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv' = 
         fo_unif_subst subst context metasenv outt1 outt2 in
        let subst'',metasenv'' = 
-        fo_unif_subst subst' context metasenv' t1 t2 in
-       List.fold_left2 
-        (function (subst,metasenv) ->
-          fo_unif_subst subst context metasenv
-        ) (subst'',metasenv'') pl1 pl2 
+        fo_unif_subst subst' context metasenv' t1' t2' in
+       (try
+         List.fold_left2 
+          (function (subst,metasenv) ->
+            fo_unif_subst subst context metasenv
+          ) (subst'',metasenv'') pl1 pl2 
+        with
+         Invalid_argument _ ->
+          raise (UnificationFailure (sprintf
+            "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
    | (C.Rel _, _) | (_,  C.Rel _)
    | (C.Sort _ ,_) | (_, C.Sort _)
    | (C.Const _, _) | (_, C.Const _)
@@ -202,29 +225,35 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
        else
         raise (UnificationFailure (sprintf
           "Can't unify %s with %s because they are not convertible"
-          (CicPp.ppterm t1) (CicPp.ppterm t2)))
+          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
    | (_,_) ->
        if R.are_convertible subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf
           "Can't unify %s with %s because they are not convertible"
-          (CicPp.ppterm t1) (CicPp.ppterm t2)))
+          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 
 and fo_unif_subst_exp_named_subst subst context metasenv
  exp_named_subst1 exp_named_subst2
 =
-try
- List.fold_left2
-  (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
-    assert (uri1=uri2) ;
-    fo_unif_subst subst context metasenv t1 t2
-  ) (subst,metasenv) exp_named_subst1 exp_named_subst2
-with
-e ->
-let uri = UriManager.uri_of_string "cic:/dummy.var" in
-debug_print ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
-" <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e
+ try
+  List.fold_left2
+   (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
+     assert (uri1=uri2) ;
+     fo_unif_subst subst context metasenv t1 t2
+   ) (subst,metasenv) exp_named_subst1 exp_named_subst2
+ with
+  Invalid_argument _ ->
+   let print_ens ens =
+    String.concat " ; "
+     (List.map
+       (fun (uri,t) ->
+         UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
+       ) ens) 
+   in
+    raise (UnificationFailure (sprintf
+     "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))
 
 (* A substitution is a (int * Cic.term) list that associates a               *)
 (* metavariable i with its body.                                             *)