rebuilt

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index c1c9086de1ccf4db4570125ea0f2963bcfd1495f..27934674808bf339ec9c797c00de0375786da493 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,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
 ;;
 
@@ -318,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 *)
@@ -333,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
@@ -512,3 +513,12 @@ let string_of_pos = function
   | Left -> "Left"
   | Right -> "Right"
 ;;
+
+
+let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
+let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_XURI () =
+  let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+  UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
+let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())