# HG changeset patch # User wenzelm # Date 1389978755 -3600 # Node ID 00e849f5b397e9b5c56dc7018af50be7739fac4b # Parent a74ea6d755717e1994fb9b19de2c1f603c1b0d31 clarified Simplifier diagnostics -- simplified ML; unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective); diff -r a74ea6d75571 -r 00e849f5b397 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Jan 17 10:02:50 2014 +0100 +++ b/src/Pure/raw_simplifier.ML Fri Jan 17 18:12:35 2014 +0100 @@ -405,16 +405,6 @@ (fn _ => Config.Int (! simp_trace_depth_limit_default)); val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw; -fun trace_depth ctxt msg = - let - val Simpset ({depth = (depth, exceeded), ...}, _) = simpset_of ctxt; - val depth_limit = Config.get ctxt simp_trace_depth_limit; - in - if depth > depth_limit then - if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true) - else (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false) - end; - fun inc_simp_depth ctxt = ctxt |> map_simpset1 (fn (rules, prems, (depth, exceeded)) => (rules, prems, @@ -438,32 +428,26 @@ val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default)); val simp_trace = Config.bool simp_trace_raw; -fun if_enabled ctxt flag f = if Config.get ctxt flag then f ctxt else (); - -fun prnt ctxt warn a = if warn then warning a else trace_depth ctxt a; - -fun print_term ctxt warn a t = prnt ctxt warn (a () ^ "\n" ^ Syntax.string_of_term ctxt t); - -fun debug ctxt warn a = if_enabled ctxt simp_debug (fn _ => prnt ctxt warn (a ())); -fun trace ctxt warn a = if_enabled ctxt simp_trace (fn _ => prnt ctxt warn (a ())); - -fun debug_term ctxt warn a t = if_enabled ctxt simp_debug (fn _ => print_term ctxt warn a t); -fun trace_term ctxt warn a t = if_enabled ctxt simp_trace (fn _ => print_term ctxt warn a t); +fun cond_warning ctxt msg = + if Context_Position.is_visible ctxt then warning (msg ()) else (); -fun trace_cterm ctxt warn a ct = - if_enabled ctxt simp_trace (fn _ => print_term ctxt warn a (Thm.term_of ct)); - -fun trace_thm ctxt a th = - if_enabled ctxt simp_trace (fn _ => print_term ctxt false a (Thm.full_prop_of th)); +fun cond_tracing ctxt flag msg = + if Config.get ctxt flag then + let + val Simpset ({depth = (depth, exceeded), ...}, _) = simpset_of ctxt; + val depth_limit = Config.get ctxt simp_trace_depth_limit; + in + if depth > depth_limit then + if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true) + else (tracing (enclose "[" "]" (string_of_int depth) ^ msg ()); exceeded := false) + end + else (); -fun trace_named_thm ctxt a (th, name) = - if_enabled ctxt simp_trace (fn _ => - print_term ctxt false - (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":") - (Thm.full_prop_of th)); +fun print_term ctxt s t = + s ^ "\n" ^ Syntax.string_of_term ctxt t; -fun warn_thm ctxt a th = print_term ctxt true a (Thm.full_prop_of th); -fun cond_warn_thm ctxt a th = Context_Position.if_visible ctxt (fn () => warn_thm ctxt a th) (); +fun print_thm ctxt s (name, th) = + print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th); @@ -483,16 +467,19 @@ fun del_rrule (rrule as {thm, elhs, ...}) ctxt = ctxt |> map_simpset1 (fn (rules, prems, depth) => (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, depth)) - handle Net.DELETE => (cond_warn_thm ctxt (fn () => "Rewrite rule not in simpset:") thm; ctxt); + handle Net.DELETE => + (cond_warning ctxt (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); ctxt); fun insert_rrule (rrule as {thm, name, ...}) ctxt = - (trace_named_thm ctxt (fn () => "Adding rewrite rule") (thm, name); + (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Adding rewrite rule" (name, thm)); ctxt |> map_simpset1 (fn (rules, prems, depth) => let val rrule2 as {elhs, ...} = mk_rrule2 rrule; val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules; in (rules', prems, depth) end) - handle Net.INSERT => (cond_warn_thm ctxt (fn () => "Ignoring duplicate rewrite rule:") thm; ctxt)); + handle Net.INSERT => + (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm)); + ctxt)); local @@ -644,8 +631,7 @@ val (xs, weak) = congs; val _ = if AList.defined (op =) xs a then - Context_Position.if_visible ctxt - warning ("Overwriting congruence rule for " ^ quote (#2 a)) + cond_warning ctxt (fn () => "Overwriting congruence rule for " ^ quote (#2 a)) else (); val xs' = AList.update (op =) (a, thm) xs; val weak' = if is_full_cong thm then weak else a :: weak; @@ -694,7 +680,7 @@ fun mk_simproc name lhss proc = make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct => - proc ctxt (Thm.term_of ct), identifier = []}; + proc ctxt (term_of ct), identifier = []}; (* FIXME avoid global thy and Logic.varify_global *) fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global); @@ -704,14 +690,15 @@ local fun add_proc (proc as Proc {name, lhs, ...}) ctxt = - (trace_cterm ctxt false (fn () => "Adding simplification procedure " ^ quote name ^ " for") lhs; + (cond_tracing ctxt simp_trace (fn () => + print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") (term_of lhs)); ctxt |> 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)) handle Net.INSERT => - (Context_Position.if_visible ctxt - warning ("Ignoring duplicate simplification procedure " ^ quote name); ctxt)); + (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name); + ctxt)); fun del_proc (proc as Proc {name, lhs, ...}) ctxt = ctxt |> map_simpset2 @@ -719,8 +706,8 @@ (congs, Net.delete_term eq_proc (term_of lhs, proc) procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)) handle Net.DELETE => - (Context_Position.if_visible ctxt - warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ctxt); + (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset"); + ctxt); fun prep_procs (Simproc {name, lhss, proc, id}) = lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id}); @@ -797,10 +784,8 @@ map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => (congs, procs, mk_rews, termless, subgoal_tac, (if AList.defined (op =) loop_tacs name then () - else - Context_Position.if_visible ctxt - warning ("No such looper in simpset: " ^ quote name); - AList.delete (op =) name loop_tacs), solvers)); + else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name); + AList.delete (op =) name loop_tacs), solvers)); fun ctxt setSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _)) => @@ -861,15 +846,18 @@ val thm'' = Thm.transitive thm thm' handle THM _ => Thm.transitive thm (Thm.transitive (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm') - in if msg then trace_thm ctxt (fn () => "SUCCEEDED") thm' else (); SOME thm'' end + val _ = + if msg then cond_tracing ctxt simp_trace (fn () => print_thm ctxt "SUCCEEDED" ("", thm')) + else (); + in SOME thm'' end handle THM _ => let val _ $ _ $ prop0 = Thm.prop_of thm; - in - trace_thm ctxt (fn () => "Proved wrong thm (Check subgoaler?)") thm'; - trace_term ctxt false (fn () => "Should have proved:") prop0; - NONE - end; + val _ = + warning + (print_thm ctxt "Simplifier: proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^ + print_term ctxt "Should have proved:" prop0); + in NONE end; (* mk_procrule *) @@ -877,7 +865,7 @@ fun mk_procrule ctxt thm = let val (prems, lhs, elhs, rhs, _) = decomp_simp thm in if rewrite_rule_extra_vars prems lhs rhs - then (cond_warn_thm ctxt (fn () => "Extra vars on rhs:") thm; []) + then (cond_warning ctxt (fn () => print_thm ctxt "Extra vars on rhs:" ("", thm)); []) else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}] end; @@ -946,32 +934,33 @@ in if perm andalso not (termless (rhs', lhs')) then - (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name); - trace_thm ctxt (fn () => "Term does not become smaller:") thm'; + (cond_tracing ctxt simp_trace (fn () => + print_thm ctxt "Cannot apply permutative rewrite rule" (name, thm) ^ "\n" ^ + print_thm ctxt "Term does not become smaller:" ("", thm')); NONE) else - (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name); + (cond_tracing ctxt simp_trace (fn () => + print_thm ctxt "Applying instance of rewrite rule" (name, thm)); if unconditional then - (trace_thm ctxt (fn () => "Rewriting:") thm'; + (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Rewriting:" ("", thm')); trace_apply trace_args ctxt (fn ctxt' => let val lr = Logic.dest_equals prop; val SOME thm'' = check_conv ctxt' false eta_thm thm'; in SOME (thm'', uncond_skel (congs, lr)) end)) else - (trace_thm ctxt (fn () => "Trying to rewrite:") thm'; + (cond_tracing ctxt simp_trace (fn () => print_thm ctxt "Trying to rewrite:" ("", thm')); if simp_depth ctxt > Config.get ctxt simp_depth_limit then - let - val s = "simp_depth_limit exceeded - giving up"; - val _ = trace ctxt false (fn () => s); - val _ = Context_Position.if_visible ctxt warning s; - in NONE end + (cond_tracing ctxt simp_trace (fn () => "simp_depth_limit exceeded - giving up"); + NONE) else trace_apply trace_args ctxt (fn ctxt' => (case prover ctxt' thm' of - NONE => (trace_thm ctxt' (fn () => "FAILED") thm'; NONE) + NONE => + (cond_tracing ctxt' simp_trace (fn () => print_thm ctxt' "FAILED" ("", thm')); + NONE) | SOME thm2 => (case check_conv ctxt' true eta_thm thm2 of NONE => NONE @@ -1002,16 +991,21 @@ fun proc_rews [] = NONE | proc_rews (Proc {name, proc, lhs, ...} :: ps) = - if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then - (debug_term ctxt false (fn () => "Trying procedure " ^ quote name ^ " on:") eta_t; + if Pattern.matches (Proof_Context.theory_of ctxt) (term_of lhs, term_of t) then + (cond_tracing ctxt simp_debug (fn () => + print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t); (case proc ctxt eta_t' of - NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps) + NONE => (cond_tracing ctxt simp_debug (fn () => "FAILED"); proc_rews ps) | SOME raw_thm => - (trace_thm ctxt (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:") - raw_thm; + (cond_tracing ctxt simp_trace (fn () => + print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:") + ("", raw_thm)); (case rews (mk_procrule ctxt raw_thm) of - NONE => (trace_cterm ctxt true (fn () => "IGNORED result of simproc " ^ quote name ^ - " -- does not match") t; proc_rews ps) + NONE => + (cond_tracing ctxt simp_trace (fn () => + print_term ctxt ("IGNORED result of simproc " ^ quote name ^ + " -- does not match") (Thm.term_of t)); + proc_rews ps) | some => some)))) else proc_rews ps; in @@ -1034,8 +1028,11 @@ (* Thm.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 _ = trace_thm ctxt (fn () => "Applying congruence rule:") thm'; - fun err (msg, thm) = (trace_thm ctxt (fn () => msg) thm; NONE); + val _ = + cond_tracing ctxt simp_trace (fn () => + print_thm ctxt "Applying congruence rule:" ("", thm')); + fun err (msg, thm) = + (cond_tracing ctxt simp_trace (fn () => print_thm ctxt msg ("", thm)); NONE); in (case prover thm' of NONE => err ("Congruence proof failed. Could not prove", thm') @@ -1088,7 +1085,7 @@ let val (b, ctxt') = Variable.next_bound (a, T) ctxt; val (v, t') = Thm.dest_abs (SOME b) t0; - val b' = #1 (Term.dest_Free (Thm.term_of v)); + val b' = #1 (Term.dest_Free (term_of v)); val _ = if b <> b' then warning ("Simplifier: renamed bound variable " ^ @@ -1162,9 +1159,11 @@ and rules_of_prem prem ctxt = if maxidx_of_term (term_of prem) <> ~1 - then (trace_cterm ctxt true - (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:") - prem; (([], NONE), ctxt)) + then + (cond_tracing ctxt simp_trace (fn () => + print_term ctxt "Cannot add premise as rewrite rule because it contains (type) unknowns:" + (term_of prem)); + (([], NONE), ctxt)) else let val (asm, ctxt') = Thm.assume_hyps prem ctxt in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end @@ -1305,9 +1304,11 @@ raw_ctxt |> Context_Position.set_visible false |> inc_simp_depth - |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt); + |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = term_of ct} ctxt); - val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct; + val _ = + cond_tracing ctxt simp_trace (fn () => + print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (term_of ct)); in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end; val simple_prover =