# HG changeset patch # User wenzelm # Date 1386886727 -3600 # Node ID 92fa590bdfe0ead99b6f8c43f21f9977e737799c # Parent 22b888402278d85d9261253640ba62c6b0feb579# Parent b01bb3d09928d7a638230ac21e5dc99075b78010 merged diff -r 22b888402278 -r 92fa590bdfe0 NEWS --- a/NEWS Thu Dec 12 17:02:52 2013 +0100 +++ b/NEWS Thu Dec 12 23:18:47 2013 +0100 @@ -12,6 +12,10 @@ * Document antiquotation @{file_unchecked} is like @{file}, but does not check existence within the file-system. +* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML +workaround in Isabelle2013-1. The prover process no longer accepts +old identifier syntax with \<^isub> or \<^isup>. + *** Prover IDE -- Isabelle/Scala/jEdit *** diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/General/symbol.ML Thu Dec 12 23:18:47 2013 +0100 @@ -517,8 +517,6 @@ (* bump string -- treat as base 26 or base 1 numbers *) fun symbolic_end (_ :: "\\<^sub>" :: _) = true - | symbolic_end (_ :: "\\<^isub>" :: _) = true (*legacy*) - | symbolic_end (_ :: "\\<^isup>" :: _) = true (*legacy*) | symbolic_end ("'" :: ss) = symbolic_end ss | symbolic_end (s :: _) = is_symbolic s | symbolic_end [] = false; diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/General/symbol_pos.ML Thu Dec 12 23:18:47 2013 +0100 @@ -220,10 +220,7 @@ val letter = Scan.one (symbol #> Symbol.is_letter); val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig); -val sub = - Scan.one (symbol #> (fn s => - if ! legacy_isub_isup then s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>" - else s = "\\<^sub>")); +val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>")); in diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Thu Dec 12 23:18:47 2013 +0100 @@ -81,12 +81,7 @@ fun max_threads_result m = if m > 0 then m - else - let val n = - (case Thread.numPhysicalProcessors () of - SOME n => n - | NONE => Thread.numProcessors ()) - in Int.min (Int.max (n, 1), 8) end; + else Int.min (Int.max (Thread.numProcessors (), 1), 8); val max_threads = ref 1; diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/ML-Systems/polyml-5.5.2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/polyml-5.5.2.ML Thu Dec 12 23:18:47 2013 +0100 @@ -0,0 +1,23 @@ +(* Title: Pure/ML-Systems/polyml-5.5.2.ML + Author: Makarius + +Compatibility wrapper for Poly/ML 5.5.2. +*) + +structure Thread = +struct + open Thread; + + structure Thread = + struct + open Thread; + + fun numProcessors () = + (case Thread.numPhysicalProcessors () of + SOME n => n + | NONE => Thread.numProcessors ()); + end; +end; + +use "ML-Systems/polyml.ML"; + diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Thu Dec 12 23:18:47 2013 +0100 @@ -44,9 +44,6 @@ else use "ML-Systems/single_assignment_polyml.ML"; open Thread; -if ML_System.name = "polyml-5.5.2" then () -else use "ML-Systems/thread_physical_processors.ML"; - use "ML-Systems/multithreading.ML"; use "ML-Systems/multithreading_polyml.ML"; diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/ML-Systems/thread_physical_processors.ML --- a/src/Pure/ML-Systems/thread_physical_processors.ML Thu Dec 12 17:02:52 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -(* Title: Pure/ML-Systems/thread_physical_processors.ML - Author: Makarius - -Emulation of structure Thread in Poly/ML 5.5.2 (SVN 1890). -*) - -structure Thread = -struct - open Thread; - - fun numPhysicalProcessors () : int option = NONE; -end; diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/Pure.thy Thu Dec 12 23:18:47 2013 +0100 @@ -107,6 +107,7 @@ ML_file "Tools/find_theorems.ML" ML_file "Tools/find_consts.ML" ML_file "Tools/proof_general_pure.ML" +ML_file "Tools/simplifier_trace.ML" section {* Further content for the Pure theory *} diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/ROOT --- a/src/Pure/ROOT Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/ROOT Thu Dec 12 23:18:47 2013 +0100 @@ -12,6 +12,7 @@ "ML-Systems/multithreading_polyml.ML" "ML-Systems/overloading_smlnj.ML" "ML-Systems/polyml.ML" + "ML-Systems/polyml-5.5.2.ML" "ML-Systems/pp_dummy.ML" "ML-Systems/proper_int.ML" "ML-Systems/single_assignment.ML" @@ -19,7 +20,6 @@ "ML-Systems/share_common_data_polyml-5.3.0.ML" "ML-Systems/smlnj.ML" "ML-Systems/thread_dummy.ML" - "ML-Systems/thread_physical_processors.ML" "ML-Systems/universal.ML" "ML-Systems/unsynchronized.ML" "ML-Systems/use_context.ML" @@ -36,13 +36,13 @@ "ML-Systems/multithreading_polyml.ML" "ML-Systems/overloading_smlnj.ML" "ML-Systems/polyml.ML" + "ML-Systems/polyml-5.5.2.ML" "ML-Systems/pp_dummy.ML" "ML-Systems/proper_int.ML" "ML-Systems/single_assignment.ML" "ML-Systems/single_assignment_polyml.ML" "ML-Systems/smlnj.ML" "ML-Systems/thread_dummy.ML" - "ML-Systems/thread_physical_processors.ML" "ML-Systems/universal.ML" "ML-Systems/unsynchronized.ML" "ML-Systems/use_context.ML" diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/Syntax/lexicon.ML Thu Dec 12 23:18:47 2013 +0100 @@ -295,8 +295,6 @@ fun idxname cs ds = (implode (rev cs), nat 0 ds); fun chop_idx [] ds = idxname [] ds | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds - | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds (*legacy*) - | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds (*legacy*) | chop_idx (c :: cs) ds = if Symbol.is_digit c then chop_idx cs (c :: ds) else idxname (c :: cs) ds; diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/Thy/thy_info.ML Thu Dec 12 23:18:47 2013 +0100 @@ -328,7 +328,7 @@ val (current, deps, theory_pos, imports, keywords) = check_deps dir' name handle ERROR msg => cat_error msg - (loader_msg "the error(s) above occurred while examining theory" [name] ^ + (loader_msg "the error(s) above occurred for theory" [name] ^ Position.here require_pos ^ required_by "\n" initiators); val parents = map (base_name o #1) imports; diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/Thy/thy_info.scala Thu Dec 12 23:18:47 2013 +0100 @@ -89,8 +89,7 @@ else if (thy_load.loaded_theories(name.theory)) required + name else { def message: String = - "The error(s) above occurred while examining theory " + - quote(name.theory) + required_by(initiators) + "The error(s) above occurred for theory " + quote(name.theory) + required_by(initiators) try { if (initiators.contains(name)) error(cycle_msg(initiators)) diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/Tools/simplifier_trace.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/simplifier_trace.ML Thu Dec 12 23:18:47 2013 +0100 @@ -0,0 +1,38 @@ +(* Title: Pure/Tools/simplifier_trace.ML + Author: Lars Hupel, TU Muenchen + +Interactive Simplifier trace. +*) + +signature SIMPLIFIER_TRACE = +sig + val simp_trace_test: bool Config.T +end + +structure Simplifier_Trace: SIMPLIFIER_TRACE = +struct + +(* Simplifier trace operations *) + +val simp_trace_test = + Attrib.setup_config_bool @{binding simp_trace_test} (K false) + +val _ = Theory.setup + (Simplifier.set_trace_ops + {trace_invoke = fn {depth, term} => fn ctxt => + (if Config.get ctxt simp_trace_test then + tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^ + Syntax.string_of_term ctxt term) + else (); ctxt), + trace_apply = fn args => fn ctxt => fn cont => + (if Config.get ctxt simp_trace_test then + tracing ("Simplifier " ^ @{make_string} args) + else (); cont ctxt)}) + + +(* PIDE protocol *) + +val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" + +end + diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/Tools/simplifier_trace.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/simplifier_trace.scala Thu Dec 12 23:18:47 2013 +0100 @@ -0,0 +1,18 @@ +/* Title: Pure/Tools/simplifier_trace.scala + Author: Lars Hupel, TU Muenchen + +Interactive Simplifier trace. +*/ + +package isabelle + + +object Simplifier_Trace +{ + /* PIDE protocol */ + + class Handler extends Session.Protocol_Handler + { + val functions = Map.empty[String, (Session.Prover, Isabelle_Process.Protocol_Output) => Boolean] + } +} diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/build-jars --- a/src/Pure/build-jars Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/build-jars Thu Dec 12 23:18:47 2013 +0100 @@ -78,6 +78,7 @@ Tools/keywords.scala Tools/main.scala Tools/ml_statistics.scala + Tools/simplifier_trace.scala Tools/sledgehammer_params.scala Tools/task_statistics.scala library.scala diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/raw_simplifier.ML Thu Dec 12 23:18:47 2013 +0100 @@ -72,11 +72,9 @@ sig include BASIC_RAW_SIMPLIFIER exception SIMPLIFIER of string * thm + type trace_ops + val set_trace_ops: trace_ops -> theory -> theory val internal_ss: simpset -> - {rules: rrule Net.net, - prems: thm list, - bounds: int * ((string * typ) * string) list, - depth: int * bool Unsynchronized.ref} * {congs: (cong_name * thm) list * cong_name list, procs: proc Net.net, mk_rews: @@ -287,7 +285,7 @@ loop_tacs: (string * (Proof.context -> int -> tactic)) list, solvers: solver list * solver list}; -fun internal_ss (Simpset args) = args; +fun internal_ss (Simpset (_, ss2)) = ss2; fun make_ss1 (rules, prems, bounds, depth) = {rules = rules, prems = prems, bounds = bounds, depth = depth}; @@ -384,9 +382,11 @@ fun simpset_map ctxt f ss = ctxt |> map_simpset (K ss) |> f |> Context.Proof |> Simpset.get; -fun put_simpset (Simpset ({rules, prems, ...}, ss2)) = (* FIXME prems from context (!?) *) - map_simpset (fn Simpset ({bounds, depth, ...}, _) => - Simpset (make_ss1 (rules, prems, bounds, depth), ss2)); +fun put_simpset ss = map_simpset (fn context_ss => + let + val Simpset ({rules, prems, ...}, ss2) = ss; (* FIXME prems from context (!?) *) + val Simpset ({bounds, depth, ...}, _) = context_ss; + in Simpset (make_ss1 (rules, prems, bounds, depth), ss2) end); fun global_context thy ss = Proof_Context.init_global thy |> put_simpset ss; @@ -665,8 +665,8 @@ in -fun add_eqcong thm ctxt = ctxt |> - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => +fun add_eqcong thm ctxt = ctxt |> map_simpset2 + (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => let val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); @@ -683,8 +683,8 @@ val weak' = if is_full_cong thm then weak else a :: weak; in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); -fun del_eqcong thm ctxt = ctxt |> - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => +fun del_eqcong thm ctxt = ctxt |> map_simpset2 + (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => let val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); @@ -737,17 +737,19 @@ fun add_proc (proc as Proc {name, lhs, ...}) ctxt = (trace_cterm ctxt false (fn () => "Adding simplification procedure " ^ quote name ^ " for") 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)) + 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)); fun del_proc (proc as Proc {name, lhs, ...}) ctxt = - ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - (congs, Net.delete_term eq_proc (term_of lhs, proc) procs, - mk_rews, termless, subgoal_tac, loop_tacs, solvers)) + ctxt |> map_simpset2 + (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => + (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); @@ -767,14 +769,15 @@ local -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient}, - termless, subgoal_tac, loop_tacs, solvers) => - let - val (mk', mk_cong', mk_sym', mk_eq_True', reorient') = - f (mk, mk_cong, mk_sym, mk_eq_True, reorient); - val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', - reorient = reorient'}; - in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); +fun map_mk_rews f = + map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => + let + val {mk, mk_cong, mk_sym, mk_eq_True, reorient} = mk_rews; + val (mk', mk_cong', mk_sym', mk_eq_True', reorient') = + f (mk, mk_cong, mk_sym, mk_eq_True, reorient); + val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', + reorient = reorient'}; + in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); in @@ -831,8 +834,8 @@ warning ("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, _)) => +fun ctxt setSSolver solver = ctxt |> map_simpset2 + (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _)) => (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, @@ -852,6 +855,30 @@ subgoal_tac, loop_tacs, (solvers, solvers))); +(* trace operations *) + +type trace_ops = + {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context, + trace_apply: {unconditional: bool, term: term, thm: thm, name: string} -> + Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option}; + +structure Trace_Ops = Theory_Data +( + type T = trace_ops; + val empty: T = + {trace_invoke = fn _ => fn ctxt => ctxt, + trace_apply = fn _ => fn ctxt => fn cont => cont ctxt}; + val extend = I; + fun merge (trace_ops, _) = trace_ops; +); + +val set_trace_ops = Trace_Ops.put; + +val trace_ops = Trace_Ops.get o Proof_Context.theory_of; +fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt; +fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt; + + (** rewriting **) @@ -946,45 +973,51 @@ val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); val prop' = Thm.prop_of thm'; val unconditional = (Logic.count_prems prop' = 0); - val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop') + val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop'); + val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', name = name}; 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'; NONE) - else (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name); - if unconditional - then - (trace_thm ctxt (fn () => "Rewriting:") thm'; + then + (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name); + trace_thm ctxt (fn () => "Term does not become smaller:") thm'; + NONE) + else + (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name); + if unconditional + then + (trace_thm ctxt (fn () => "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'; - 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 - else - case prover ctxt thm' of - NONE => (trace_thm ctxt (fn () => "FAILED") thm'; NONE) - | SOME thm2 => - (case check_conv ctxt true eta_thm thm2 of - NONE => NONE - | SOME thm2' => - let - val concl = Logic.strip_imp_concl prop; - val lr = Logic.dest_equals concl; - in SOME (thm2', cond_skel (congs, lr)) end))) + 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'; + 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 + else + trace_apply trace_args ctxt (fn ctxt' => + (case prover ctxt' thm' of + NONE => (trace_thm ctxt' (fn () => "FAILED") thm'; NONE) + | SOME thm2 => + (case check_conv ctxt' true eta_thm thm2 of + NONE => NONE + | SOME thm2' => + let + val concl = Logic.strip_imp_concl prop; + val lr = Logic.dest_equals concl; + in SOME (thm2', cond_skel (congs, lr)) end))))) end; fun rews [] = NONE | rews (rrule :: rrules) = let val opt = rew rrule handle Pattern.MATCH => NONE - in case opt of NONE => rews rrules | some => some end; + in (case opt of NONE => rews rrules | some => some) end; fun sort_rrules rrs = let @@ -1003,7 +1036,7 @@ | 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; - case proc ctxt eta_t' of + (case proc ctxt eta_t' of NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps) | SOME raw_thm => (trace_thm ctxt (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:") @@ -1011,7 +1044,7 @@ (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) - | some => some))) + | some => some)))) else proc_rews ps; in (case eta_t of @@ -1052,7 +1085,7 @@ fun transitive1 NONE NONE = NONE | transitive1 (SOME thm1) NONE = SOME thm1 | transitive1 NONE (SOME thm2) = SOME thm2 - | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2) + | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2); fun transitive2 thm = transitive1 (SOME thm); fun transitive3 thm = transitive1 thm o SOME; @@ -1060,25 +1093,25 @@ fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) = let fun botc skel ctxt t = - if is_Var skel then NONE - else - (case subc skel ctxt t of - some as SOME thm1 => - (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of - SOME (thm2, skel2) => - transitive2 (Thm.transitive thm1 thm2) - (botc skel2 ctxt (Thm.rhs_of thm2)) - | NONE => some) - | NONE => - (case rewritec (prover, maxidx) ctxt t of - SOME (thm2, skel2) => transitive2 thm2 + if is_Var skel then NONE + else + (case subc skel ctxt t of + some as SOME thm1 => + (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of + SOME (thm2, skel2) => + transitive2 (Thm.transitive thm1 thm2) (botc skel2 ctxt (Thm.rhs_of thm2)) - | NONE => NONE)) + | NONE => some) + | NONE => + (case rewritec (prover, maxidx) ctxt t of + SOME (thm2, skel2) => transitive2 thm2 + (botc skel2 ctxt (Thm.rhs_of thm2)) + | NONE => NONE)) and try_botc ctxt t = - (case botc skel0 ctxt t of - SOME trec1 => trec1 - | NONE => (Thm.reflexive t)) + (case botc skel0 ctxt t of + SOME trec1 => trec1 + | NONE => Thm.reflexive t) and subc skel ctxt t0 = let val Simpset ({bounds, ...}, {congs, ...}) = simpset_of ctxt in @@ -1094,64 +1127,71 @@ quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ())) else (); val ctxt' = add_bound ((b', T), a) ctxt; - val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; + val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0); in (case botc skel' ctxt' t' of SOME thm => SOME (Thm.abstract_rule a v thm) | NONE => NONE) end - | t $ _ => (case t of + | t $ _ => + (case t of Const ("==>", _) $ _ => impc t0 ctxt | Abs _ => let val thm = Thm.beta_conversion false t0 - in case subc skel0 ctxt (Thm.rhs_of thm) of - NONE => SOME thm - | SOME thm' => SOME (Thm.transitive thm thm') + in + (case subc skel0 ctxt (Thm.rhs_of thm) of + NONE => SOME thm + | SOME thm' => SOME (Thm.transitive thm thm')) end | _ => - let fun appc () = - let - val (tskel, uskel) = case skel of - tskel $ uskel => (tskel, uskel) - | _ => (skel0, skel0); - val (ct, cu) = Thm.dest_comb t0 - in + let + fun appc () = + let + val (tskel, uskel) = + (case skel of + tskel $ uskel => (tskel, uskel) + | _ => (skel0, skel0)); + val (ct, cu) = Thm.dest_comb t0; + in (case botc tskel ctxt ct of - SOME thm1 => - (case botc uskel ctxt cu of - SOME thm2 => SOME (Thm.combination thm1 thm2) - | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu))) - | NONE => - (case botc uskel ctxt cu of - SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1) - | NONE => NONE)) - end - val (h, ts) = strip_comb t - in case cong_name h of - SOME a => - (case AList.lookup (op =) (fst congs) a of - NONE => appc () - | SOME cong => + SOME thm1 => + (case botc uskel ctxt cu of + SOME thm2 => SOME (Thm.combination thm1 thm2) + | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu))) + | NONE => + (case botc uskel ctxt cu of + SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1) + | NONE => NONE)) + end; + val (h, ts) = strip_comb t; + in + (case cong_name h of + SOME a => + (case AList.lookup (op =) (fst congs) a of + NONE => appc () + | SOME cong => (*post processing: some partial applications h t1 ... tj, j <= length ts, may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) - (let - val thm = congc (prover ctxt) ctxt maxidx cong t0; - val t = the_default t0 (Option.map Thm.rhs_of thm); - val (cl, cr) = Thm.dest_comb t - val dVar = Var(("", 0), dummyT) - val skel = - list_comb (h, replicate (length ts) dVar) - in case botc skel ctxt cl of - NONE => thm - | SOME thm' => transitive3 thm - (Thm.combination thm' (Thm.reflexive cr)) - end handle Pattern.MATCH => appc ())) - | _ => appc () + (let + val thm = congc (prover ctxt) ctxt maxidx cong t0; + val t = the_default t0 (Option.map Thm.rhs_of thm); + val (cl, cr) = Thm.dest_comb t + val dVar = Var(("", 0), dummyT) + val skel = + list_comb (h, replicate (length ts) dVar) + in + (case botc skel ctxt cl of + NONE => thm + | SOME thm' => + transitive3 thm (Thm.combination thm' (Thm.reflexive cr))) + end handle Pattern.MATCH => appc ())) + | _ => appc ()) end) | _ => NONE) end and impc ct ctxt = - if mutsimp then mut_impc0 [] ct [] [] ctxt else nonmut_impc ct ctxt + if mutsimp then mut_impc0 [] ct [] [] ctxt + else nonmut_impc ct ctxt and rules_of_prem ctxt prem = if maxidx_of_term (term_of prem) <> ~1 @@ -1168,19 +1208,23 @@ and disch r prem eq = let val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); - val eq' = Thm.implies_elim (Thm.instantiate - ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) - (Thm.implies_intr prem eq) - in if not r then eq' else - let - val (prem', concl) = Thm.dest_implies lhs; - val (prem'', _) = Thm.dest_implies rhs - in Thm.transitive (Thm.transitive - (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) - Drule.swap_prems_eq) eq') - (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) - Drule.swap_prems_eq) - end + val eq' = + Thm.implies_elim + (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) + (Thm.implies_intr prem eq); + in + if not r then eq' + else + let + val (prem', concl) = Thm.dest_implies lhs; + val (prem'', _) = Thm.dest_implies rhs; + in + Thm.transitive + (Thm.transitive + (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq) + eq') + (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) Drule.swap_prems_eq) + end end and rebuild [] _ _ _ _ eq = eq @@ -1189,19 +1233,19 @@ val ctxt' = add_rrules (rev rrss, rev asms) ctxt; val concl' = Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq)); - val dprem = Option.map (disch false prem) + val dprem = Option.map (disch false prem); in (case rewritec (prover, maxidx) ctxt' concl' of NONE => rebuild prems concl' rrss asms ctxt (dprem eq) - | SOME (eq', _) => transitive2 (fold (disch false) - prems (the (transitive3 (dprem eq) eq'))) - (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ctxt)) + | SOME (eq', _) => + transitive2 (fold (disch false) prems (the (transitive3 (dprem eq) eq'))) + (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ctxt)) end and mut_impc0 prems concl rrss asms ctxt = let val prems' = strip_imp_prems concl; - val (rrss', asms') = split_list (map (rules_of_prem ctxt) prems') + val (rrss', asms') = split_list (map (rules_of_prem ctxt) prems'); in mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss') (asms @ asms') [] [] [] [] ctxt ~1 ~1 @@ -1218,27 +1262,29 @@ | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) prems' rrss' asms' eqns ctxt changed k = - case (if k = 0 then NONE else botc skel0 (add_rrules + (case (if k = 0 then NONE else botc skel0 (add_rrules (rev rrss' @ rrss, rev asms' @ asms) ctxt) prem) of NONE => mut_impc prems concl rrss asms (prem :: prems') (rrs :: rrss') (asm :: asms') (NONE :: eqns) ctxt changed (if k = 0 then 0 else k - 1) - | SOME eqn => + | SOME eqn => let val prem' = Thm.rhs_of eqn; val tprems = map term_of prems; val i = 1 + fold Integer.max (map (fn p => find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1; val (rrs', asm') = rules_of_prem ctxt prem'; - in mut_impc prems concl rrss asms (prem' :: prems') - (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true) - (take i prems) - (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies - (drop i prems, concl))))) :: eqns) - ctxt (length prems') ~1 - end + in + mut_impc prems concl rrss asms (prem' :: prems') + (rrs' :: rrss') (asm' :: asms') + (SOME (fold_rev (disch true) + (take i prems) + (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies + (drop i prems, concl))))) :: eqns) + ctxt (length prems') ~1 + end) - (*legacy code - only for backwards compatibility*) + (*legacy code -- only for backwards compatibility*) and nonmut_impc ct ctxt = let val (prem, conc) = Thm.dest_implies ct; @@ -1260,9 +1306,9 @@ | SOME thm1' => SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2')) end) - end + end; - in try_botc end; + in try_botc end; (* Meta-rewriting: rewrites t to u and returns the theorem t==u *) @@ -1299,11 +1345,7 @@ fun rewrite_cterm mode prover raw_ctxt raw_ct = let - val ctxt = - raw_ctxt - |> Context_Position.set_visible false - |> inc_simp_depth; - val thy = Proof_Context.theory_of ctxt; + val thy = Proof_Context.theory_of raw_ctxt; val ct = Thm.adjust_maxidx_cterm ~1 raw_ct; val {maxidx, ...} = Thm.rep_cterm ct; @@ -1311,11 +1353,12 @@ Theory.subthy (theory_of_cterm ct, thy) orelse raise CTERM ("rewrite_cterm: bad background theory", [ct]); - val depth = simp_depth ctxt; - val _ = - if depth mod 20 = 0 then - Context_Position.if_visible ctxt warning ("Simplification depth " ^ string_of_int depth) - else (); + val ctxt = + raw_ctxt + |> Context_Position.set_visible false + |> inc_simp_depth + |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt); + val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct; val _ = check_bounds ctxt ct; in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end; diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/simplifier.ML Thu Dec 12 23:18:47 2013 +0100 @@ -47,6 +47,8 @@ val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context val set_termless: (term * term -> bool) -> Proof.context -> Proof.context val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context + type trace_ops + val set_trace_ops: trace_ops -> theory -> theory val simproc_global_i: theory -> string -> term list -> (Proof.context -> term -> thm option) -> simproc val simproc_global: theory -> string -> string list -> @@ -190,14 +192,14 @@ fun solve_all_tac solvers ctxt = let - val (_, {subgoal_tac, ...}) = Raw_Simplifier.internal_ss (simpset_of ctxt); + val {subgoal_tac, ...} = Raw_Simplifier.internal_ss (simpset_of ctxt); val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt) THEN_ALL_NEW (K no_tac); in DEPTH_SOLVE (solve_tac 1) end; (*NOTE: may instantiate unknowns that appear also in other subgoals*) fun generic_simp_tac safe mode ctxt = let - val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = + val {loop_tacs, solvers = (unsafe_solvers, solvers), ...} = Raw_Simplifier.internal_ss (simpset_of ctxt); val loop_tac = FIRST' (map (fn (_, tac) => tac ctxt) (rev loop_tacs)); val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt) @@ -212,7 +214,7 @@ fun simp rew mode ctxt thm = let - val (_, {solvers = (unsafe_solvers, _), ...}) = Raw_Simplifier.internal_ss (simpset_of ctxt); + val {solvers = (unsafe_solvers, _), ...} = Raw_Simplifier.internal_ss (simpset_of ctxt); val tacf = solve_all_tac (rev unsafe_solvers); fun prover s th = Option.map #1 (Seq.pull (tacf s th)); in rew mode prover ctxt thm end; diff -r 22b888402278 -r 92fa590bdfe0 src/Pure/term.ML --- a/src/Pure/term.ML Thu Dec 12 17:02:52 2013 +0100 +++ b/src/Pure/term.ML Thu Dec 12 23:18:47 2013 +0100 @@ -979,8 +979,6 @@ val dot = (case rev (Symbol.explode x) of _ :: "\\<^sub>" :: _ => false - | _ :: "\\<^isub>" :: _ => false (*legacy*) - | _ :: "\\<^isup>" :: _ => false (*legacy*) | c :: _ => Symbol.is_digit c | _ => true); in