improved simp tracing;
authorwenzelm
Wed Jul 23 11:04:19 1997 +0200 (1997-07-23)
changeset 3558258eee1a056e
parent 3557 9546f8185c43
child 3559 7a176613e5d5
improved simp tracing;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Wed Jul 23 11:03:54 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed Jul 23 11:04:19 1997 +0200
     1.3 @@ -1432,6 +1432,7 @@
     1.4  
     1.5  val trace_simp = ref false;
     1.6  
     1.7 +fun trace a = if ! trace_simp then writeln a else ();
     1.8  fun trace_warning a = if ! trace_simp then warning a else ();
     1.9  fun trace_term a sign t = if ! trace_simp then prtm a sign t else ();
    1.10  fun trace_term_warning a sign t = if ! trace_simp then prtm_warning a sign t else ();
    1.11 @@ -1817,12 +1818,13 @@
    1.12        fun proc_rews _ ([]:simproc list) = None
    1.13          | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
    1.14              if Pattern.matches tsigt (plhs, t) then
    1.15 -              (case proc signt eta_t of
    1.16 -                None => proc_rews eta_t ps
    1.17 +             (trace_term ("Trying procedure " ^ name ^ " on:") signt eta_t;
    1.18 +              case proc signt eta_t of
    1.19 +                None => (trace "FAILED"; proc_rews eta_t ps)
    1.20                | Some raw_thm =>
    1.21 -                 (trace_thm ("Procedure" ^ name ^ " proved rewrite rule:") raw_thm;
    1.22 +                 (trace_thm ("Procedure " ^ name ^ " proved rewrite rule:") raw_thm;
    1.23                     (case rews (mk_procrule raw_thm) of
    1.24 -                     None => proc_rews eta_t ps
    1.25 +                     None => (trace "IGNORED"; proc_rews eta_t ps)
    1.26                     | some => some)))
    1.27              else proc_rews eta_t ps;
    1.28    in