added override for \circ (notation for function composition)

[helm.git] / helm / ocaml / cic_unification / coercGraph.ml

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index d7454925a606f8a0ddd93fa9bc112a070dcbb240..c6a929619f508d65bbeb6c307093322422683b54 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,30 +25,30 @@
 
 open Printf;;
 
-let debug = true
-let debug_print = if debug then prerr_endline else ignore
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src tgt =
     try
-      let src = UriManager.uri_of_string (CicUtil.uri_of_term src) in
-      let tgt = UriManager.uri_of_string (CicUtil.uri_of_term tgt) in
+      let src = CicUtil.uri_of_term src in
+      let tgt = CicUtil.uri_of_term tgt in
       let l = 
         CoercDb.find_coercion 
           (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) 
       in
       match l with
-      | [] -> prerr_endline ":( coercion non trovata"; None
+      | [] -> debug_print (lazy ":( coercion non trovata"); None
       | u::_ -> 
-          debug_print (
+          debug_print (lazy (
             sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
               (List.length l)
               (UriManager.name_of_uri src) 
               (UriManager.name_of_uri tgt)
-              (UriManager.name_of_uri u));
-              Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
+              (UriManager.name_of_uri u)));
+              Some (CicUtil.term_of_uri u)
     with Invalid_argument s -> 
-      debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
+      debug_print (lazy (":( coercion non trovata (fallita la uri_of_term): " ^ s));
       None
 ;;
 
@@ -97,8 +97,8 @@ let generate_composite_closure c1 c2 univ =
     try 
       CicTypeChecker.type_of_aux' [] [] c univ
     with CicTypeChecker.TypeCheckerFailure s as exn ->
-      debug_print (sprintf "Generated composite coercion:\n%s\n%s" 
-        (CicPp.ppterm c) s);
+      debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" 
+        (CicPp.ppterm c) s));
       raise exn
   in
   let cleaned_ty =
@@ -133,9 +133,7 @@ let close_coercion_graph src tgt uri =
           match l with
           | [] -> assert false 
           | he :: tl ->
-              let term_of_uri' uri = 
-                CicUtil.term_of_uri (UriManager.string_of_uri uri)
-              in
+              let term_of_uri' uri = CicUtil.term_of_uri uri in
               let first_step = 
                 Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
                   obj_attrs)