Fixing a source of inefficiency and an artificial dependency in the

printer in the congruence tactic.

Debugging messages were always built even when not in the verbose mode
of congruence.

1 files changed, 14 insertions, 14 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc3d9ed56..5d16edfc6 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,7 +25,7 @@ let init_size=5
 let cc_verbose=ref false
 
 let debug x =
-  if !cc_verbose then msg_debug x
+  if !cc_verbose then msg_debug (x ())
 
 let _=
   let gdopt=
@@ -603,7 +603,7 @@ let add_inst state (inst,int_subst) =
   Control.check_for_interrupt ();
   if state.rew_depth > 0 then
   if is_redundant state inst.qe_hyp_id int_subst then
-    debug (str "discarding redundant (dis)equality")
+    debug (fun () -> str "discarding redundant (dis)equality")
   else
     begin
       Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -618,7 +618,7 @@ let add_inst state (inst,int_subst) =
 	    state.rew_depth<-pred state.rew_depth;
 	    if inst.qe_pol then
 	      begin
-		debug (
+		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
 	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
 			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
@@ -626,7 +626,7 @@ let add_inst state (inst,int_subst) =
 	      end
 	    else
 	      begin
-		debug (
+		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
 	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
@@ -657,7 +657,7 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (str "Linking " ++ pr_idx_term state.uf i1 ++
+  debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++
 		 str " and " ++ pr_idx_term state.uf i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
@@ -698,7 +698,7 @@ let union state i1 i2 eq=
 
 let merge eq state = (* merge and no-merge *)
   debug
-    (str "Merging " ++ pr_idx_term state.uf eq.lhs ++
+    (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++
        str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
   let uf=state.uf in
   let i=find uf eq.lhs
@@ -711,7 +711,7 @@ let merge eq state = (* merge and no-merge *)
 
 let update t state = (* update 1 and 2 *)
   debug
-    (str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
+    (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
   let rep = get_representative state.uf i in
@@ -773,7 +773,7 @@ let process_constructor_mark t i rep pac state =
 
 let process_mark t m state =
   debug
-    (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
+    (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
@@ -794,7 +794,7 @@ let check_disequalities state =
           else (str "No", check_aux q)
         in
         let _ = debug
-        (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
+        (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
          pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
         ans
     | [] -> None
@@ -979,7 +979,7 @@ let find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
-    debug (str "Running E-matching algorithm ... ");
+    debug (fun () -> str "Running E-matching algorithm ... ");
     try
       while true do
 	Control.check_for_interrupt ();
@@ -990,7 +990,7 @@ let find_instances state =
     !res
 
 let rec execute first_run state =
-  debug (str "Executing ... ");
+  debug (fun () -> str "Executing ... ");
   try
     while
       Control.check_for_interrupt ();
@@ -1000,7 +1000,7 @@ let rec execute first_run state =
 	None ->
 	  if not(Int.Set.is_empty state.pa_classes) then
 	    begin
-	      debug (str "First run was incomplete, completing ... ");
+	      debug (fun () -> str "First run was incomplete, completing ... ");
 	      complete state;
 	      execute false state
 	    end
@@ -1015,12 +1015,12 @@ let rec execute first_run state =
 		  end
 		else
 	      begin
-		debug (str "Out of instances ... ");
+		debug (fun () -> str "Out of instances ... ");
 		None
 	      end
 	    else
 	      begin
-		debug (str "Out of depth ... ");
+		debug (fun () -> str "Out of depth ... ");
 		None
 	      end
       | Some dis -> Some