# HG changeset patch
# User wenzelm
# Date 1170786751 -3600
# Node ID 420625970f31fa4286b988285360349b05a4f4c9
# Parent  7a1bf42992545d92a09eff73b423ab867eef8313
trace/debug: avoid eager string concatenation;

diff -r 7a1bf4299254 -r 420625970f31 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Tue Feb 06 18:02:28 2007 +0100
+++ b/src/Pure/meta_simplifier.ML	Tue Feb 06 19:32:31 2007 +0100
@@ -284,21 +284,23 @@
 fun print_term warn a ss thy t = prnt warn (a ^ "\n" ^
   Sign.string_of_term thy (if ! debug_simp then t else show_bounds ss t));
 
-fun debug warn a = if ! debug_simp then prnt warn a else ();
-fun trace warn a = if ! trace_simp then prnt warn a else ();
+fun debug warn a = if ! debug_simp then prnt warn (a ()) else ();
+fun trace warn a = if ! trace_simp then prnt warn (a ()) else ();
 
-fun debug_term warn a ss thy t = if ! debug_simp then print_term warn a ss thy t else ();
-fun trace_term warn a ss thy t = if ! trace_simp then print_term warn a ss thy t else ();
+fun debug_term warn a ss thy t = if ! debug_simp then print_term warn (a ()) ss thy t else ();
+fun trace_term warn a ss thy t = if ! trace_simp then print_term warn (a ()) ss thy t else ();
 
 fun trace_cterm warn a ss ct =
-  if ! trace_simp then print_term warn a ss (Thm.theory_of_cterm ct) (Thm.term_of ct) else ();
+  if ! trace_simp then print_term warn (a ()) ss (Thm.theory_of_cterm ct) (Thm.term_of ct)
+  else ();
 
 fun trace_thm a ss th =
-  if ! trace_simp then print_term false a ss (Thm.theory_of_thm th) (Thm.full_prop_of th) else ();
+  if ! trace_simp then print_term false (a ()) ss (Thm.theory_of_thm th) (Thm.full_prop_of th)
+  else ();
 
 fun trace_named_thm a ss (th, name) =
   if ! trace_simp then
-    print_term false (if name = "" then a else a ^ " " ^ quote name ^ ":") ss
+    print_term false (if name = "" then a () else a () ^ " " ^ quote name ^ ":") ss
       (Thm.theory_of_thm th) (Thm.full_prop_of th)
   else ();
 
@@ -404,7 +406,7 @@
   handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
 
 fun insert_rrule (rrule as {thm, name, elhs, ...}) ss =
- (trace_named_thm "Adding rewrite rule" ss (thm, name);
+ (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
   ss |> map_simpset1 (fn (rules, prems, bounds, context) =>
     let
       val rrule2 as {elhs, ...} = mk_rrule2 rrule;
@@ -639,7 +641,7 @@
 local
 
 fun add_proc (proc as Proc {name, lhs, ...}) ss =
- (trace_cterm false ("Adding simplification procedure " ^ quote name ^ " for") ss lhs;
+ (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
       mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
@@ -814,11 +816,11 @@
   let
     val thm'' = transitive thm (transitive
       (symmetric (Drule.beta_eta_conversion (Drule.lhs_of thm'))) thm')
-  in if msg then trace_thm "SUCCEEDED" ss thm' else (); SOME thm'' end
+  in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
   handle THM _ =>
     let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
-      trace_thm "Proved wrong thm (Check subgoaler?)" ss thm';
-      trace_term false "Should have proved:" ss thy prop0;
+      trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
+      trace_term false (fn () => "Should have proved:") ss thy prop0;
       NONE
     end;
 
@@ -891,23 +893,23 @@
         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
       in
         if perm andalso not (termless (rhs', lhs'))
-        then (trace_named_thm "Cannot apply permutative rewrite rule" ss (thm, name);
-              trace_thm "Term does not become smaller:" ss thm'; NONE)
-        else (trace_named_thm "Applying instance of rewrite rule" ss (thm, name);
+        then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
+              trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
+        else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
            if unconditional
            then
-             (trace_thm "Rewriting:" ss thm';
+             (trace_thm (fn () => "Rewriting:") ss thm';
               let val lr = Logic.dest_equals prop;
                   val SOME thm'' = check_conv false ss eta_thm thm'
               in SOME (thm'', uncond_skel (congs, lr)) end)
            else
-             (trace_thm "Trying to rewrite:" ss thm';
+             (trace_thm (fn () => "Trying to rewrite:") ss thm';
               if !simp_depth > !simp_depth_limit
               then let val s = "simp_depth_limit exceeded - giving up"
-                   in trace false s; warning s; NONE end
+                   in trace false (fn () => s); warning s; NONE end
               else
               case prover ss thm' of
-                NONE => (trace_thm "FAILED" ss thm'; NONE)
+                NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
               | SOME thm2 =>
                   (case check_conv true ss eta_thm thm2 of
                      NONE => NONE |
@@ -935,14 +937,15 @@
     fun proc_rews [] = NONE
       | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
           if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
-            (debug_term false ("Trying procedure " ^ quote name ^ " on:") ss thyt eta_t;
+            (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss thyt eta_t;
              case transform_failure (curry SIMPROC_FAIL name)
                  (fn () => proc ss eta_t') () of
-               NONE => (debug false "FAILED"; proc_rews ps)
+               NONE => (debug false (fn () => "FAILED"); proc_rews ps)
              | SOME raw_thm =>
-                 (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") ss raw_thm;
+                 (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
+                   ss raw_thm;
                   (case rews (mk_procrule ss raw_thm) of
-                    NONE => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^
+                    NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
                       " -- does not match") ss t; proc_rews ps)
                   | some => some)))
           else proc_rews ps;
@@ -964,8 +967,8 @@
       (* Pattern.match can raise Pattern.MATCH;
          is handled when congc is called *)
       val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
-      val unit = trace_thm "Applying congruence rule:" ss thm';
-      fun err (msg, thm) = (trace_thm msg ss thm; NONE)
+      val unit = trace_thm (fn () => "Applying congruence rule:") ss thm';
+      fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
   in case prover thm' of
        NONE => err ("Congruence proof failed.  Could not prove", thm')
      | SOME thm2 => (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
@@ -1081,7 +1084,8 @@
     and rules_of_prem ss prem =
       if maxidx_of_term (term_of prem) <> ~1
       then (trace_cterm true
-        "Cannot add premise as rewrite rule because it contains (type) unknowns:" ss prem; ([], NONE))
+        (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
+          ss prem; ([], NONE))
       else
         let val asm = assume prem
         in (extract_safe_rrules (ss, asm), SOME asm) end
@@ -1220,7 +1224,7 @@
       if ! simp_depth mod 20 = 0 then
         warning ("Simplification depth " ^ string_of_int (! simp_depth))
       else ();
-    val _ = trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ss ct;
+    val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
     val _ = check_bounds ss ct;
     val res = bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct
   in dec simp_depth; res end