X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=9db77c5d526200246379772cd0a9a1d8cf78c67a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7c0d0e387c8c1c278f4fceb6baa168f022d39439;hpb=3813bdd5d0b4139a682b5faa50611791ac9278c2;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 7c0d0e387..9db77c5d5 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -29,6 +29,7 @@ exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
+let verbose = false;;
 let debug_print = fun _ -> () 
 
 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
@@ -46,6 +47,17 @@ let foo () =
          lazy
           (sprintf
            "Kernel Type checking error: 
+%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
+             (CicMetaSubst.ppterm subst term)
+             (CicMetaSubst.ppterm [] term)
+             (CicMetaSubst.ppcontext subst context)
+             (CicMetaSubst.ppmetasenv subst metasenv) 
+             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+        raise (AssertFailure msg)
+    | CicTypeChecker.AssertFailure msg ->
+        let msg = lazy
+         (sprintf
+           "Kernel Type checking assertion failure: 
 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
              (CicMetaSubst.ppterm subst term)
              (CicMetaSubst.ppterm [] term)
@@ -436,11 +448,11 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
         exp_named_subst1 exp_named_subst2 ugraph
       else
-       raise (UnificationFailure (lazy "3"))
-         (* (sprintf
+       raise (UnificationFailure (lazy 
+          (sprintf
             "Can't unify %s with %s due to different constants"
             (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2))) *)
+            (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 
@@ -583,11 +595,11 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        if t1 = t2 then
          subst, metasenv,ugraph
        else
-        raise (UnificationFailure (lazy "6.2"))
-          (* (sprintf
+        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))))
    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
        let subst,metasenv,beta_expanded,ugraph1 =
          beta_expand_many 
@@ -680,21 +692,50 @@ let fo_unif metasenv context t1 t2 ugraph =
  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 
 let enrich_msg msg subst context metasenv t1 t2 ugraph =
- lazy
-  (sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
+ lazy (
+  if verbose then
+   sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
     (CicMetaSubst.ppterm subst t1)
     (try
       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
       CicPp.ppterm ty_t1
-    with _ -> "MALFORMED")
+    with 
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
     (CicMetaSubst.ppterm subst t2)
     (try
       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
       CicPp.ppterm ty_t2
-    with _ -> "MALFORMED")
+    with
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppcontext subst context)
+    (CicMetaSubst.ppmetasenv subst metasenv)
+    (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+ else
+   sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
+    (CicMetaSubst.ppterm_in_context subst t1 context)
+    (try
+      let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+      CicMetaSubst.ppterm_in_context subst ty_t1 context
+    with 
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppterm_in_context subst t2 context)
+    (try
+      let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+      CicMetaSubst.ppterm_in_context subst ty_t2 context
+    with
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
     (CicMetaSubst.ppcontext subst context)
     (CicMetaSubst.ppmetasenv subst metasenv)
-    (CicMetaSubst.ppsubst subst) (Lazy.force msg))
+    (Lazy.force msg)
+ )
 
 let fo_unif_subst subst context metasenv t1 t2 ugraph =
   try