new paramodulation

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 525ed9ca2b457fcbce005fe5707b208b69ecb6be..2d5ee24ce7612527102a3f128c586fa66511145d 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 =
@@ -107,6 +107,8 @@ let compute_equality_weight ty left right =
 (*     metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *)
     w
   in
+  (* Warning: the following let cannot be expanded since it forces the
+     right evaluation order!!!! *)
   let w = (weight_of ty) + (weight_of left) + (weight_of right) in
   w + !metasw
 (*     (4 * IntSet.cardinal !metasw) *)
@@ -287,9 +289,10 @@ let rec aux_ordering ?(recursion=true) t1 t2 =
       aux_ordering h1 h2
         
   | t1, t2 ->
-      debug_print (
-        Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
-          (CicPp.ppterm t1) (CicPp.ppterm t2));
+      debug_print
+        (lazy
+           (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
+              (CicPp.ppterm t1) (CicPp.ppterm t2)));
       Incomparable
 ;;
 
@@ -316,8 +319,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 *)
@@ -331,23 +334,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