All the debug_print are now lazy.

[helm.git] / helm / ocaml / paramodulation / utils.ml

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index c1c9086de1ccf4db4570125ea0f2963bcfd1495f..681a371e1a6f71c60e90d7021aa1a8aa121c0688 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -1,6 +1,6 @@
 let debug = true;;
 
-let debug_print = if debug then prerr_endline else ignore;;
+let debug_print s = if debug then prerr_endline (Lazy.force s);;
 
 
 let print_metasenv metasenv =
@@ -289,9 +289,9 @@ let rec aux_ordering ?(recursion=true) t1 t2 =
       aux_ordering h1 h2
         
   | t1, t2 ->
-      debug_print (
+      debug_print (lazy (
         Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
-          (CicPp.ppterm t1) (CicPp.ppterm t2));
+          (CicPp.ppterm t1) (CicPp.ppterm t2)));
       Incomparable
 ;;
 
@@ -318,8 +318,8 @@ let nonrec_kbo t1 t2 =
 
 
 let rec kbo t1 t2 =
-(*   debug_print ( *)
-(*     Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
+(*   debug_print (lazy ( *)
+(*     Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2))); *)
 (*   if t1 = t2 then *)
 (*     Eq *)
 (*   else *)
@@ -333,23 +333,23 @@ let rec kbo t1 t2 =
       | [], _ -> Lt
       | hd1::tl1, hd2::tl2 ->
           let o =
-(*             debug_print ( *)
+(*             debug_print (lazy ( *)
 (*               Printf.sprintf "recursion kbo on %s %s" *)
-(*                 (CicPp.ppterm hd1) (CicPp.ppterm hd2)); *)
+(*                 (CicPp.ppterm hd1) (CicPp.ppterm hd2))); *)
             kbo hd1 hd2
           in
           if o = Eq then cmp tl1 tl2
           else o
     in
     let comparison = compare_weights ~normalize:true w1 w2 in
-(*     debug_print ( *)
+(*     debug_print (lazy ( *)
 (*       Printf.sprintf "Weights are: %s %s: %s" *)
 (*         (string_of_weight w1) (string_of_weight w2) *)
-(*         (string_of_comparison comparison)); *)
+(*         (string_of_comparison comparison))); *)
     match comparison with
     | Le ->
         let r = aux t1 t2 in
-(*         debug_print ("HERE! " ^ (string_of_comparison r)); *)
+(*         debug_print (lazy ("HERE! " ^ (string_of_comparison r))); *)
         if r = Lt then Lt
         else if r = Eq then (
           match t1, t2 with