more work for coercions

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 09265ef2e4c265007218bb81382aba337deb0ff0..37d89bf1f300c279d39e36eea0dd9f15c2d7b83d 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1102,7 +1102,7 @@ and type_of_aux' metasenv context t ugraph =
                    in
                    let coerced_args,metasenv',subst',t',ugraph2 =
                      eat_prods metasenv subst context
-                      (CicSubstitution.subst arg t) ugraph1 tl
+                       (CicSubstitution.subst arg t) ugraph1 tl
                    in
                      arg::coerced_args,metasenv',subst',t',ugraph2
                | _ -> assert false

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 9a87bc51bba07e6493a4666ae494a0fdce006a45..a3bc1f39a02a6fb76213c7caf54de0bc798c3a3d 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -447,11 +447,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 
@@ -697,12 +697,18 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     (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))

diff --git a/helm/ocaml/cic_unification/coercDb.ml b/helm/ocaml/cic_unification/coercDb.ml
index c56fc1fef8b24abebce93a8e03e91918c56c71bf..437ad65ae202bcddab717c3fa5e5d327f63d6dfc 100644 (file)
--- a/helm/ocaml/cic_unification/coercDb.ml
+++ b/helm/ocaml/cic_unification/coercDb.ml
@@ -56,7 +56,7 @@ let eq_carr src tgt =
 let name_of_carr = function
   | Uri u -> UriManager.name_of_uri u
   | Sort s -> CicPp.ppsort s
-  | Term _ -> assert false
+  | Term t -> CicPp.ppterm t
   
 
 let to_list () =

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index b3bc8d8b0e7ba5b94284102bfc4a68c9db1941bb..d99fc6f798f67f72ccbee796adc50b8bd0db1474 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -43,10 +43,23 @@ let look_for_coercion src tgt =
         (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) 
     in
     match l with
-    | [] -> debug_print (lazy ":( coercion non trovata"); NoCoercion
+    | [] -> 
+        debug_print 
+          (lazy 
+            (sprintf ":-( coercion non trovata da %s a %s" 
+              (CoercDb.name_of_carr src) 
+              (CoercDb.name_of_carr tgt)));
+        NoCoercion
+    | [u] -> 
+        debug_print (lazy (
+          sprintf ":-) TROVATA 1 coercion da %s a %s: %s" 
+            (CoercDb.name_of_carr src) 
+            (CoercDb.name_of_carr tgt)
+            (UriManager.name_of_uri u)));
+        SomeCoercion (CicUtil.term_of_uri u)
     | u::_ -> 
         debug_print (lazy (
-          sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
+          sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
             (List.length l)
             (CoercDb.name_of_carr src) 
             (CoercDb.name_of_carr tgt)