clarified Simplifier diagnostics -- simplified ML;
authorwenzelm
Fri Jan 17 18:12:35 2014 +0100 (2014-01-17)
changeset 5502800e849f5b397
parent 55027 a74ea6d75571
child 55029 61a6bf7d4b02
clarified Simplifier diagnostics -- simplified ML;
unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Jan 17 10:02:50 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Fri Jan 17 18:12:35 2014 +0100
     1.3 @@ -405,16 +405,6 @@
     1.4    (fn _ => Config.Int (! simp_trace_depth_limit_default));
     1.5  val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
     1.6  
     1.7 -fun trace_depth ctxt msg =
     1.8 -  let
     1.9 -    val Simpset ({depth = (depth, exceeded), ...}, _) = simpset_of ctxt;
    1.10 -    val depth_limit = Config.get ctxt simp_trace_depth_limit;
    1.11 -  in
    1.12 -    if depth > depth_limit then
    1.13 -      if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
    1.14 -    else (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false)
    1.15 -  end;
    1.16 -
    1.17  fun inc_simp_depth ctxt =
    1.18    ctxt |> map_simpset1 (fn (rules, prems, (depth, exceeded)) =>
    1.19      (rules, prems,
    1.20 @@ -438,32 +428,26 @@
    1.21  val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
    1.22  val simp_trace = Config.bool simp_trace_raw;
    1.23  
    1.24 -fun if_enabled ctxt flag f = if Config.get ctxt flag then f ctxt else ();
    1.25 -
    1.26 -fun prnt ctxt warn a = if warn then warning a else trace_depth ctxt a;
    1.27 -
    1.28 -fun print_term ctxt warn a t = prnt ctxt warn (a () ^ "\n" ^ Syntax.string_of_term ctxt t);
    1.29 -
    1.30 -fun debug ctxt warn a = if_enabled ctxt simp_debug (fn _ => prnt ctxt warn (a ()));
    1.31 -fun trace ctxt warn a = if_enabled ctxt simp_trace (fn _ => prnt ctxt warn (a ()));
    1.32 -
    1.33 -fun debug_term ctxt warn a t = if_enabled ctxt simp_debug (fn _ => print_term ctxt warn a t);
    1.34 -fun trace_term ctxt warn a t = if_enabled ctxt simp_trace (fn _ => print_term ctxt warn a t);
    1.35 +fun cond_warning ctxt msg =
    1.36 +  if Context_Position.is_visible ctxt then warning (msg ()) else ();
    1.37  
    1.38 -fun trace_cterm ctxt warn a ct =
    1.39 -  if_enabled ctxt simp_trace (fn _ => print_term ctxt warn a (Thm.term_of ct));
    1.40 -
    1.41 -fun trace_thm ctxt a th =
    1.42 -  if_enabled ctxt simp_trace (fn _ => print_term ctxt false a (Thm.full_prop_of th));
    1.43 +fun cond_tracing ctxt flag msg =
    1.44 +  if Config.get ctxt flag then
    1.45 +    let
    1.46 +      val Simpset ({depth = (depth, exceeded), ...}, _) = simpset_of ctxt;
    1.47 +      val depth_limit = Config.get ctxt simp_trace_depth_limit;
    1.48 +    in
    1.49 +      if depth > depth_limit then
    1.50 +        if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
    1.51 +      else (tracing (enclose "[" "]" (string_of_int depth) ^ msg ()); exceeded := false)
    1.52 +    end
    1.53 +  else ();
    1.54  
    1.55 -fun trace_named_thm ctxt a (th, name) =
    1.56 -  if_enabled ctxt simp_trace (fn _ =>
    1.57 -    print_term ctxt false
    1.58 -      (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
    1.59 -      (Thm.full_prop_of th));
    1.60 +fun print_term ctxt s t =
    1.61 +  s ^ "\n" ^ Syntax.string_of_term ctxt t;
    1.62  
    1.63 -fun warn_thm ctxt a th = print_term ctxt true a (Thm.full_prop_of th);
    1.64 -fun cond_warn_thm ctxt a th = Context_Position.if_visible ctxt (fn () => warn_thm ctxt a th) ();
    1.65 +fun print_thm ctxt s (name, th) =
    1.66 +  print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th);
    1.67  
    1.68  
    1.69  
    1.70 @@ -483,16 +467,19 @@
    1.71  fun del_rrule (rrule as {thm, elhs, ...}) ctxt =
    1.72    ctxt |> map_simpset1 (fn (rules, prems, depth) =>
    1.73      (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, depth))
    1.74 -  handle Net.DELETE => (cond_warn_thm ctxt (fn () => "Rewrite rule not in simpset:") thm; ctxt);
    1.75 +  handle Net.DELETE =>
    1.76 +    (cond_warning ctxt (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); ctxt);
    1.77  
    1.78  fun insert_rrule (rrule as {thm, name, ...}) ctxt =
    1.79 - (trace_named_thm ctxt (fn () => "Adding rewrite rule") (thm, name);
    1.80 + (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Adding rewrite rule" (name, thm));
    1.81    ctxt |> map_simpset1 (fn (rules, prems, depth) =>
    1.82      let
    1.83        val rrule2 as {elhs, ...} = mk_rrule2 rrule;
    1.84        val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
    1.85      in (rules', prems, depth) end)
    1.86 -  handle Net.INSERT => (cond_warn_thm ctxt (fn () => "Ignoring duplicate rewrite rule:") thm; ctxt));
    1.87 +  handle Net.INSERT =>
    1.88 +    (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
    1.89 +      ctxt));
    1.90  
    1.91  local
    1.92  
    1.93 @@ -644,8 +631,7 @@
    1.94        val (xs, weak) = congs;
    1.95        val _ =
    1.96          if AList.defined (op =) xs a then
    1.97 -          Context_Position.if_visible ctxt
    1.98 -            warning ("Overwriting congruence rule for " ^ quote (#2 a))
    1.99 +          cond_warning ctxt (fn () => "Overwriting congruence rule for " ^ quote (#2 a))
   1.100          else ();
   1.101        val xs' = AList.update (op =) (a, thm) xs;
   1.102        val weak' = if is_full_cong thm then weak else a :: weak;
   1.103 @@ -694,7 +680,7 @@
   1.104  
   1.105  fun mk_simproc name lhss proc =
   1.106    make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct =>
   1.107 -    proc ctxt (Thm.term_of ct), identifier = []};
   1.108 +    proc ctxt (term_of ct), identifier = []};
   1.109  
   1.110  (* FIXME avoid global thy and Logic.varify_global *)
   1.111  fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
   1.112 @@ -704,14 +690,15 @@
   1.113  local
   1.114  
   1.115  fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
   1.116 - (trace_cterm ctxt false (fn () => "Adding simplification procedure " ^ quote name ^ " for") lhs;
   1.117 + (cond_tracing ctxt simp_trace (fn () =>
   1.118 +    print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") (term_of lhs));
   1.119    ctxt |> map_simpset2
   1.120      (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.121        (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
   1.122          mk_rews, termless, subgoal_tac, loop_tacs, solvers))
   1.123    handle Net.INSERT =>
   1.124 -    (Context_Position.if_visible ctxt
   1.125 -      warning ("Ignoring duplicate simplification procedure " ^ quote name); ctxt));
   1.126 +    (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
   1.127 +      ctxt));
   1.128  
   1.129  fun del_proc (proc as Proc {name, lhs, ...}) ctxt =
   1.130    ctxt |> map_simpset2
   1.131 @@ -719,8 +706,8 @@
   1.132        (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
   1.133          mk_rews, termless, subgoal_tac, loop_tacs, solvers))
   1.134    handle Net.DELETE =>
   1.135 -    (Context_Position.if_visible ctxt
   1.136 -      warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ctxt);
   1.137 +    (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
   1.138 +      ctxt);
   1.139  
   1.140  fun prep_procs (Simproc {name, lhss, proc, id}) =
   1.141    lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
   1.142 @@ -797,10 +784,8 @@
   1.143    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.144      (congs, procs, mk_rews, termless, subgoal_tac,
   1.145       (if AList.defined (op =) loop_tacs name then ()
   1.146 -      else
   1.147 -        Context_Position.if_visible ctxt
   1.148 -          warning ("No such looper in simpset: " ^ quote name);
   1.149 -        AList.delete (op =) name loop_tacs), solvers));
   1.150 +      else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name);
   1.151 +      AList.delete (op =) name loop_tacs), solvers));
   1.152  
   1.153  fun ctxt setSSolver solver = ctxt |> map_simpset2
   1.154    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
   1.155 @@ -861,15 +846,18 @@
   1.156      val thm'' = Thm.transitive thm thm' handle THM _ =>
   1.157       Thm.transitive thm (Thm.transitive
   1.158         (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
   1.159 -  in if msg then trace_thm ctxt (fn () => "SUCCEEDED") thm' else (); SOME thm'' end
   1.160 +    val _ =
   1.161 +      if msg then cond_tracing ctxt simp_trace (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
   1.162 +      else ();
   1.163 +  in SOME thm'' end
   1.164    handle THM _ =>
   1.165      let
   1.166        val _ $ _ $ prop0 = Thm.prop_of thm;
   1.167 -    in
   1.168 -      trace_thm ctxt (fn () => "Proved wrong thm (Check subgoaler?)") thm';
   1.169 -      trace_term ctxt false (fn () => "Should have proved:") prop0;
   1.170 -      NONE
   1.171 -    end;
   1.172 +      val _ =
   1.173 +        warning
   1.174 +         (print_thm ctxt "Simplifier: proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^
   1.175 +          print_term ctxt "Should have proved:" prop0);
   1.176 +    in NONE end;
   1.177  
   1.178  
   1.179  (* mk_procrule *)
   1.180 @@ -877,7 +865,7 @@
   1.181  fun mk_procrule ctxt thm =
   1.182    let val (prems, lhs, elhs, rhs, _) = decomp_simp thm in
   1.183      if rewrite_rule_extra_vars prems lhs rhs
   1.184 -    then (cond_warn_thm ctxt (fn () => "Extra vars on rhs:") thm; [])
   1.185 +    then (cond_warning ctxt (fn () => print_thm ctxt "Extra vars on rhs:" ("", thm)); [])
   1.186      else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
   1.187    end;
   1.188  
   1.189 @@ -946,32 +934,33 @@
   1.190        in
   1.191          if perm andalso not (termless (rhs', lhs'))
   1.192          then
   1.193 -         (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name);
   1.194 -          trace_thm ctxt (fn () => "Term does not become smaller:") thm';
   1.195 +         (cond_tracing ctxt simp_trace (fn () =>
   1.196 +            print_thm ctxt "Cannot apply permutative rewrite rule" (name, thm) ^ "\n" ^
   1.197 +            print_thm ctxt "Term does not become smaller:" ("", thm'));
   1.198            NONE)
   1.199          else
   1.200 -         (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name);
   1.201 +         (cond_tracing ctxt simp_trace (fn () =>
   1.202 +            print_thm ctxt "Applying instance of rewrite rule" (name, thm));
   1.203            if unconditional
   1.204            then
   1.205 -           (trace_thm ctxt (fn () => "Rewriting:") thm';
   1.206 +           (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Rewriting:" ("", thm'));
   1.207              trace_apply trace_args ctxt (fn ctxt' =>
   1.208                let
   1.209                  val lr = Logic.dest_equals prop;
   1.210                  val SOME thm'' = check_conv ctxt' false eta_thm thm';
   1.211                in SOME (thm'', uncond_skel (congs, lr)) end))
   1.212            else
   1.213 -           (trace_thm ctxt (fn () => "Trying to rewrite:") thm';
   1.214 +           (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Trying to rewrite:" ("", thm'));
   1.215              if simp_depth ctxt > Config.get ctxt simp_depth_limit
   1.216              then
   1.217 -              let
   1.218 -                val s = "simp_depth_limit exceeded - giving up";
   1.219 -                val _ = trace ctxt false (fn () => s);
   1.220 -                val _ = Context_Position.if_visible ctxt warning s;
   1.221 -              in NONE end
   1.222 +             (cond_tracing ctxt simp_trace (fn () => "simp_depth_limit exceeded - giving up");
   1.223 +               NONE)
   1.224              else
   1.225                trace_apply trace_args ctxt (fn ctxt' =>
   1.226                  (case prover ctxt' thm' of
   1.227 -                  NONE => (trace_thm ctxt' (fn () => "FAILED") thm'; NONE)
   1.228 +                  NONE =>
   1.229 +                    (cond_tracing ctxt' simp_trace (fn () => print_thm ctxt' "FAILED" ("", thm'));
   1.230 +                      NONE)
   1.231                  | SOME thm2 =>
   1.232                      (case check_conv ctxt' true eta_thm thm2 of
   1.233                        NONE => NONE
   1.234 @@ -1002,16 +991,21 @@
   1.235  
   1.236      fun proc_rews [] = NONE
   1.237        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
   1.238 -          if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then
   1.239 -            (debug_term ctxt false (fn () => "Trying procedure " ^ quote name ^ " on:") eta_t;
   1.240 +          if Pattern.matches (Proof_Context.theory_of ctxt) (term_of lhs, term_of t) then
   1.241 +            (cond_tracing ctxt simp_debug (fn () =>
   1.242 +              print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
   1.243               (case proc ctxt eta_t' of
   1.244 -               NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps)
   1.245 +               NONE => (cond_tracing ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
   1.246               | SOME raw_thm =>
   1.247 -                 (trace_thm ctxt (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
   1.248 -                   raw_thm;
   1.249 +                 (cond_tracing ctxt simp_trace (fn () =>
   1.250 +                    print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:")
   1.251 +                      ("", raw_thm));
   1.252                    (case rews (mk_procrule ctxt raw_thm) of
   1.253 -                    NONE => (trace_cterm ctxt true (fn () => "IGNORED result of simproc " ^ quote name ^
   1.254 -                      " -- does not match") t; proc_rews ps)
   1.255 +                    NONE =>
   1.256 +                     (cond_tracing ctxt simp_trace (fn () =>
   1.257 +                        print_term ctxt ("IGNORED result of simproc " ^ quote name ^
   1.258 +                            " -- does not match") (Thm.term_of t));
   1.259 +                      proc_rews ps)
   1.260                    | some => some))))
   1.261            else proc_rews ps;
   1.262    in
   1.263 @@ -1034,8 +1028,11 @@
   1.264      (* Thm.match can raise Pattern.MATCH;
   1.265         is handled when congc is called *)
   1.266      val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   1.267 -    val _ = trace_thm ctxt (fn () => "Applying congruence rule:") thm';
   1.268 -    fun err (msg, thm) = (trace_thm ctxt (fn () => msg) thm; NONE);
   1.269 +    val _ =
   1.270 +      cond_tracing ctxt simp_trace (fn () =>
   1.271 +        print_thm ctxt "Applying congruence rule:" ("", thm'));
   1.272 +    fun err (msg, thm) =
   1.273 +      (cond_tracing ctxt simp_trace (fn () => print_thm ctxt msg ("", thm)); NONE);
   1.274    in
   1.275      (case prover thm' of
   1.276        NONE => err ("Congruence proof failed.  Could not prove", thm')
   1.277 @@ -1088,7 +1085,7 @@
   1.278                  let
   1.279                      val (b, ctxt') = Variable.next_bound (a, T) ctxt;
   1.280                      val (v, t') = Thm.dest_abs (SOME b) t0;
   1.281 -                    val b' = #1 (Term.dest_Free (Thm.term_of v));
   1.282 +                    val b' = #1 (Term.dest_Free (term_of v));
   1.283                      val _ =
   1.284                        if b <> b' then
   1.285                          warning ("Simplifier: renamed bound variable " ^
   1.286 @@ -1162,9 +1159,11 @@
   1.287  
   1.288      and rules_of_prem prem ctxt =
   1.289        if maxidx_of_term (term_of prem) <> ~1
   1.290 -      then (trace_cterm ctxt true
   1.291 -        (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
   1.292 -        prem; (([], NONE), ctxt))
   1.293 +      then
   1.294 +       (cond_tracing ctxt simp_trace (fn () =>
   1.295 +          print_term ctxt "Cannot add premise as rewrite rule because it contains (type) unknowns:"
   1.296 +            (term_of prem));
   1.297 +        (([], NONE), ctxt))
   1.298        else
   1.299          let val (asm, ctxt') = Thm.assume_hyps prem ctxt
   1.300          in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end
   1.301 @@ -1305,9 +1304,11 @@
   1.302        raw_ctxt
   1.303        |> Context_Position.set_visible false
   1.304        |> inc_simp_depth
   1.305 -      |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);
   1.306 +      |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = term_of ct} ctxt);
   1.307  
   1.308 -    val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
   1.309 +    val _ =
   1.310 +      cond_tracing ctxt simp_trace (fn () =>
   1.311 +        print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (term_of ct));
   1.312    in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
   1.313  
   1.314  val simple_prover =