open Printf;;
let debug = false
-let debug_print = if debug then prerr_endline else ignore
+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 =
(fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt)
in
match l with
- | [] -> debug_print ":( 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));
+ (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
;;
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 =