From d7eb6fad3e5afc0fc786c9a91ef64733120dfb43 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 18 Nov 2005 17:28:02 +0000
Subject: [PATCH] more work for coercions

---
 helm/ocaml/cic_unification/cicRefine.ml      |  2 +-
 helm/ocaml/cic_unification/cicUnification.ml | 16 +++++++++++-----
 helm/ocaml/cic_unification/coercDb.ml        |  2 +-
 helm/ocaml/cic_unification/coercGraph.ml     | 17 +++++++++++++++--
 4 files changed, 28 insertions(+), 9 deletions(-)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 09265ef2e..37d89bf1f 100644
--- 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 9a87bc51b..a3bc1f39a 100644
--- 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 c56fc1fef..437ad65ae 100644
--- 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 b3bc8d8b0..d99fc6f79 100644
--- 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)
-- 
2.39.2