tuned;
authorwenzelm
Fri Jan 17 20:36:57 2014 +0100 (2014-01-17)
changeset 55031e58066daa065
parent 55030 9a9049d12e21
child 55032 b49366215417
tuned;
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Jan 17 20:31:39 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Fri Jan 17 20:36:57 2014 +0100
     1.3 @@ -431,7 +431,7 @@
     1.4  fun cond_warning ctxt msg =
     1.5    if Context_Position.is_visible ctxt then warning (msg ()) else ();
     1.6  
     1.7 -fun cond_tracing ctxt flag msg =
     1.8 +fun cond_tracing' ctxt flag msg =
     1.9    if Config.get ctxt flag then
    1.10      let
    1.11        val Simpset ({depth = (depth, exceeded), ...}, _) = simpset_of ctxt;
    1.12 @@ -443,6 +443,8 @@
    1.13      end
    1.14    else ();
    1.15  
    1.16 +fun cond_tracing ctxt = cond_tracing' ctxt simp_trace;
    1.17 +
    1.18  fun print_term ctxt s t =
    1.19    s ^ "\n" ^ Syntax.string_of_term ctxt t;
    1.20  
    1.21 @@ -471,7 +473,7 @@
    1.22      (cond_warning ctxt (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); ctxt);
    1.23  
    1.24  fun insert_rrule (rrule as {thm, name, ...}) ctxt =
    1.25 - (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Adding rewrite rule" (name, thm));
    1.26 + (cond_tracing ctxt (fn () => print_thm ctxt "Adding rewrite rule" (name, thm));
    1.27    ctxt |> map_simpset1 (fn (rules, prems, depth) =>
    1.28      let
    1.29        val rrule2 as {elhs, ...} = mk_rrule2 rrule;
    1.30 @@ -690,7 +692,7 @@
    1.31  local
    1.32  
    1.33  fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
    1.34 - (cond_tracing ctxt simp_trace (fn () =>
    1.35 + (cond_tracing ctxt (fn () =>
    1.36      print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") (term_of lhs));
    1.37    ctxt |> map_simpset2
    1.38      (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.39 @@ -847,7 +849,7 @@
    1.40       Thm.transitive thm (Thm.transitive
    1.41         (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
    1.42      val _ =
    1.43 -      if msg then cond_tracing ctxt simp_trace (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
    1.44 +      if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
    1.45        else ();
    1.46    in SOME thm'' end
    1.47    handle THM _ =>
    1.48 @@ -934,33 +936,29 @@
    1.49        in
    1.50          if perm andalso not (termless (rhs', lhs'))
    1.51          then
    1.52 -         (cond_tracing ctxt simp_trace (fn () =>
    1.53 +         (cond_tracing ctxt (fn () =>
    1.54              print_thm ctxt "Cannot apply permutative rewrite rule" (name, thm) ^ "\n" ^
    1.55              print_thm ctxt "Term does not become smaller:" ("", thm'));
    1.56            NONE)
    1.57          else
    1.58 -         (cond_tracing ctxt simp_trace (fn () =>
    1.59 +         (cond_tracing ctxt (fn () =>
    1.60              print_thm ctxt "Applying instance of rewrite rule" (name, thm));
    1.61            if unconditional
    1.62            then
    1.63 -           (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Rewriting:" ("", thm'));
    1.64 +           (cond_tracing ctxt (fn () => print_thm ctxt "Rewriting:" ("", thm'));
    1.65              trace_apply trace_args ctxt (fn ctxt' =>
    1.66                let
    1.67                  val lr = Logic.dest_equals prop;
    1.68                  val SOME thm'' = check_conv ctxt' false eta_thm thm';
    1.69                in SOME (thm'', uncond_skel (congs, lr)) end))
    1.70            else
    1.71 -           (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Trying to rewrite:" ("", thm'));
    1.72 +           (cond_tracing ctxt (fn () => print_thm ctxt "Trying to rewrite:" ("", thm'));
    1.73              if simp_depth ctxt > Config.get ctxt simp_depth_limit
    1.74 -            then
    1.75 -             (cond_tracing ctxt simp_trace (fn () => "simp_depth_limit exceeded - giving up");
    1.76 -               NONE)
    1.77 +            then (cond_tracing ctxt (fn () => "simp_depth_limit exceeded - giving up"); NONE)
    1.78              else
    1.79                trace_apply trace_args ctxt (fn ctxt' =>
    1.80                  (case prover ctxt' thm' of
    1.81 -                  NONE =>
    1.82 -                    (cond_tracing ctxt' simp_trace (fn () => print_thm ctxt' "FAILED" ("", thm'));
    1.83 -                      NONE)
    1.84 +                  NONE => (cond_tracing ctxt' (fn () => print_thm ctxt' "FAILED" ("", thm')); NONE)
    1.85                  | SOME thm2 =>
    1.86                      (case check_conv ctxt' true eta_thm thm2 of
    1.87                        NONE => NONE
    1.88 @@ -992,17 +990,17 @@
    1.89      fun proc_rews [] = NONE
    1.90        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
    1.91            if Pattern.matches (Proof_Context.theory_of ctxt) (term_of lhs, term_of t) then
    1.92 -            (cond_tracing ctxt simp_debug (fn () =>
    1.93 +            (cond_tracing' ctxt simp_debug (fn () =>
    1.94                print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
    1.95               (case proc ctxt eta_t' of
    1.96 -               NONE => (cond_tracing ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
    1.97 +               NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
    1.98               | SOME raw_thm =>
    1.99 -                 (cond_tracing ctxt simp_trace (fn () =>
   1.100 +                 (cond_tracing ctxt (fn () =>
   1.101                      print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:")
   1.102                        ("", raw_thm));
   1.103                    (case rews (mk_procrule ctxt raw_thm) of
   1.104                      NONE =>
   1.105 -                     (cond_tracing ctxt simp_trace (fn () =>
   1.106 +                     (cond_tracing ctxt (fn () =>
   1.107                          print_term ctxt ("IGNORED result of simproc " ^ quote name ^
   1.108                              " -- does not match") (Thm.term_of t));
   1.109                        proc_rews ps)
   1.110 @@ -1029,10 +1027,8 @@
   1.111         is handled when congc is called *)
   1.112      val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   1.113      val _ =
   1.114 -      cond_tracing ctxt simp_trace (fn () =>
   1.115 -        print_thm ctxt "Applying congruence rule:" ("", thm'));
   1.116 -    fun err (msg, thm) =
   1.117 -      (cond_tracing ctxt simp_trace (fn () => print_thm ctxt msg ("", thm)); NONE);
   1.118 +      cond_tracing ctxt (fn () => print_thm ctxt "Applying congruence rule:" ("", thm'));
   1.119 +    fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm ctxt msg ("", thm)); NONE);
   1.120    in
   1.121      (case prover thm' of
   1.122        NONE => err ("Congruence proof failed.  Could not prove", thm')
   1.123 @@ -1160,7 +1156,7 @@
   1.124      and rules_of_prem prem ctxt =
   1.125        if maxidx_of_term (term_of prem) <> ~1
   1.126        then
   1.127 -       (cond_tracing ctxt simp_trace (fn () =>
   1.128 +       (cond_tracing ctxt (fn () =>
   1.129            print_term ctxt "Cannot add premise as rewrite rule because it contains (type) unknowns:"
   1.130              (term_of prem));
   1.131          (([], NONE), ctxt))
   1.132 @@ -1307,7 +1303,7 @@
   1.133        |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = term_of ct} ctxt);
   1.134  
   1.135      val _ =
   1.136 -      cond_tracing ctxt simp_trace (fn () =>
   1.137 +      cond_tracing ctxt (fn () =>
   1.138          print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (term_of ct));
   1.139    in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
   1.140