- Improved error messaging.

- Invalid_argument was raised by List.fold_left2 ;-(
  I want checked excecptions!

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 83daf60a636309401e7637a9d2bdbc30caca9093..e7b0e3661387d3b986a292858962532f9c4588a5 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -593,7 +593,7 @@ let delift n subst context metasenv l t =
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
 debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
-debug_print "\nCicMetaSubst: UNCERTAIN" ;
+print_string "\nCicMetaSubst: UNCERTAIN" ;
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 55781422c0d031c249910222e22bfe1d354eb187..d33230eb0f3d41f4154952ef563b187536279dee 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -403,6 +403,7 @@ and type_of_aux' metasenv context t =
      in
       aux 1 canonical_context
     in
+    try
      List.fold_left2 
       (fun (subst,metasenv) t ct -> 
         match (t,ct) with
@@ -426,6 +427,14 @@ and type_of_aux' metasenv context t =
               (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
               (CicMetaSubst.ppcontext subst canonical_context)))
       ) (subst,metasenv) l lifted_canonical_context 
+    with
+     Invalid_argument _ ->
+      raise
+       (NotRefinable
+         (sprintf
+           "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
+             (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+             (CicMetaSubst.ppcontext subst canonical_context)))
 
  and check_exp_named_subst metasubst metasenv context =
   let rec check_exp_named_subst_aux metasubst metasenv substs =
@@ -533,14 +542,20 @@ and type_of_aux' metasenv context t =
        | (hete, hety)::tl ->
         (match hetype with
             Cic.Prod (n,s,t) ->
+(*
              (try
+*)
               let subst,metasenv =
                CicUnification.fo_unif_subst subst context metasenv s hety
               in
                eat_prods metasenv subst context
                 (CicMetaSubst.subst subst hete t) tl
-             with
-              e -> raise (RefineFailure ("XXX " ^ Printexc.to_string e)))
+(*
+              with
+               e ->
+                raise
+                 (RefineFailure ("XXX " ^ Printexc.to_string e)))
+*)
           | _ -> assert false
         )
    in

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index fb1ca113f23e7f3b40035b8c68f47cd74bf9048d..37f8621c8980d5fa50d2d8dd90114db33130c747 100644 (file)
--- 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,13 +81,17 @@ 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)))
+            (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm substt2)))
    | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
        fo_unif_subst subst context metasenv t2 t1
    | (C.Meta (n,l), t)   
@@ -132,7 +137,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 +145,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 +154,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 +186,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 +212,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.                                             *)