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 =
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
;;
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 *)
| [], _ -> 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