All the debug_print are now lazy.

[helm.git] / helm / ocaml / tactics / tacticals.ml

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 934b88a5ab6b1ebb0fccbdc8564cb8bff0bcd56f..94b5d379d19837cbaa96dd2f722771d13eeb48fc 100644 (file)
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -34,9 +34,7 @@ let debug = false
 let debug_print = fun _ -> ()
 
   (** debugging print *)
-let warn s =
-  if debug then
-    debug_print ("TACTICALS WARNING: " ^ s)
+let warn s = debug_print (lazy ("TACTICALS WARNING: " ^ (Lazy.force s)))
 
 let id_tac = 
  let id_tac (proof,goal) = 
@@ -100,13 +98,13 @@ type tactic = S.tactic
   *)
 let first ~tactics =
  let rec first ~(tactics: (string * tactic) list) status =
-  warn "in Tacticals.first";
+  warn (lazy "in Tacticals.first");
   match tactics with
   | (descr, tac)::tactics ->
-      warn ("Tacticals.first IS TRYING " ^ descr);
+      warn (lazy ("Tacticals.first IS TRYING " ^ descr));
       (try
         let res = S.apply_tactic tac status in
-        warn ("Tacticals.first: " ^ descr ^ " succedeed!!!");
+        warn (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
         res
        with
         e ->
@@ -114,9 +112,9 @@ let first ~tactics =
             (Fail _)
           | (CicTypeChecker.TypeCheckerFailure _)
           | (CicUnification.UnificationFailure _) ->
-              warn (
+              warn (lazy (
                 "Tacticals.first failed with exn: " ^
-                Printexc.to_string e);
+                Printexc.to_string e));
               first ~tactics status
         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
       )
@@ -181,7 +179,7 @@ let rec seq ~tactics =
 
 let repeat_tactic ~tactic =
  let rec repeat_tactic ~tactic status =
-  warn "in repeat_tactic";
+  warn (lazy "in repeat_tactic");
   try
    let output_status = S.apply_tactic tactic status in
    let goallist = S.goals output_status in
@@ -199,7 +197,7 @@ let repeat_tactic ~tactic =
      S.set_goals output_status goallist
   with 
    (Fail _) as e ->
-    warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+    warn (lazy ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ;
     S.apply_tactic S.id_tac status
  in 
   S.mk_tactic (repeat_tactic ~tactic)
@@ -228,7 +226,7 @@ let do_tactic ~n ~tactic =
       S.set_goals output_status goals
    with 
     (Fail _) as e ->
-     warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+     warn (lazy ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ;
      S.apply_tactic S.id_tac status
  in
   S.mk_tactic (do_tactic ~n ~tactic)
@@ -238,12 +236,12 @@ let do_tactic ~n ~tactic =
 (* This applies tactic and catches its possible failure *)
 let try_tactic ~tactic =
  let rec try_tactic ~tactic status =
-  warn "in Tacticals.try_tactic";
+  warn (lazy "in Tacticals.try_tactic");
   try
    S.apply_tactic tactic status
   with
    (Fail _) as e -> 
-    warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
+    warn (lazy ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
     S.apply_tactic S.id_tac status
  in
   S.mk_tactic (try_tactic ~tactic)
@@ -252,26 +250,26 @@ let try_tactic ~tactic =
 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
 let solve_tactics ~tactics =
  let rec solve_tactics ~(tactics: (string * tactic) list) status =
-  warn "in Tacticals.solve_tactics";
+  warn (lazy "in Tacticals.solve_tactics");
   match tactics with
   | (descr, currenttactic)::moretactics ->
-      warn ("Tacticals.solve_tactics is trying " ^ descr);
+      warn (lazy ("Tacticals.solve_tactics is trying " ^ descr));
       (try
         let output_status = S.apply_tactic currenttactic status in
         let goallist = S.goals output_status in
          match goallist with 
-            [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ 
-                  " solved the goal!!!");
+            [] -> warn (lazy ("Tacticals.solve_tactics: " ^ descr ^ 
+                  " solved the goal!!!"));
 (* questo significa che non ci sono piu' goal, o che current_tactic non ne 
    ha aperti di nuovi? (la 2a!) ##### 
    nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
                   output_status
-          | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
+          | _ -> warn (lazy ("Tacticals.solve_tactics: try the next tactic"));
                  solve_tactics ~tactics:(moretactics) status
        with
         (Fail _) as e ->
-         warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ 
-         Printexc.to_string e);
+         warn (lazy ("Tacticals.solve_tactics: current tactic failed with exn: " ^ 
+         Printexc.to_string e));
          solve_tactics ~tactics status
       )
   | [] -> raise (Fail "solve_tactics cannot solve the goal");