# HG changeset patch # User wenzelm # Date 1236510958 -3600 # Node ID 36d0e00af606c3b95c8485d5bacf24fb3ee4db2f # Parent 8066d80cd51e98a9729275f274827988f425da74 added dest_ss; proper context fo pretty_ss; tuned; diff -r 8066d80cd51e -r 36d0e00af606 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sun Mar 08 00:41:52 2009 +0100 +++ b/src/Pure/meta_simplifier.ML Sun Mar 08 12:15:58 2009 +0100 @@ -24,7 +24,14 @@ val mk_solver: string -> (thm list -> int -> tactic) -> solver val empty_ss: simpset val merge_ss: simpset * simpset -> simpset - val pretty_ss: simpset -> Pretty.T + val dest_ss: simpset -> + {simps: (string * thm) list, + procs: (string * cterm list) list, + congs: (string * thm) list, + weak_congs: string list, + loopers: string list, + unsafe_solvers: string list, + safe_solvers: string list} type simproc val eq_simproc: simproc * simproc -> bool val morph_simproc: morphism -> simproc -> simproc @@ -325,35 +332,6 @@ end; -(* print simpsets *) - -fun pretty_ss ss = - let - val pretty_thms = map Display.pretty_thm; - - fun pretty_cong (name, {thm, lhs}) = - Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, Display.pretty_thm thm]; - fun pretty_proc (name, lhss) = - Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss); - - val Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = ss; - val smps = map #thm (Net.entries rules); - val prcs = Net.entries procs |> - map (fn Proc {name, lhs, id, ...} => ((name, lhs), id)) - |> partition_eq (eq_snd eq_procid) - |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)) - |> Library.sort_wrt fst; - in - [Pretty.big_list "simplification rules:" (pretty_thms smps), - Pretty.big_list "simplification procedures:" (map pretty_proc prcs), - Pretty.big_list "congruences:" (map pretty_cong (fst congs)), - Pretty.strs ("loopers:" :: map (quote o fst) loop_tacs), - Pretty.strs ("unsafe solvers:" :: map (quote o solver_name) (#1 solvers)), - Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))] - |> Pretty.chunks - end; - - (** simpset operations **) @@ -806,7 +784,7 @@ val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _}, {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; - + val rules' = Net.merge eq_rrule (rules1, rules2); val prems' = merge Thm.eq_thm_prop (prems1, prems2); val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; @@ -823,6 +801,22 @@ end; +(* dest_ss *) + +fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) = + {simps = Net.entries rules + |> map (fn {name, thm, ...} => (name, thm)), + procs = Net.entries procs + |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id)) + |> partition_eq (eq_snd eq_procid) + |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), + congs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs), + weak_congs = #2 congs, + loopers = map fst loop_tacs, + unsafe_solvers = map solver_name (#1 solvers), + safe_solvers = map solver_name (#2 solvers)}; + + (** rewriting **) diff -r 8066d80cd51e -r 36d0e00af606 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sun Mar 08 00:41:52 2009 +0100 +++ b/src/Pure/simplifier.ML Sun Mar 08 12:15:58 2009 +0100 @@ -42,6 +42,7 @@ signature SIMPLIFIER = sig include BASIC_SIMPLIFIER + val pretty_ss: Proof.context -> simpset -> Pretty.T val clear_ss: simpset -> simpset val debug_bounds: bool ref val inherit_context: simpset -> simpset -> simpset @@ -86,6 +87,29 @@ open MetaSimplifier; +(** pretty printing **) + +fun pretty_ss ctxt ss = + let + val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of; + val pretty_thm = ProofContext.pretty_thm ctxt; + fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss); + fun pretty_cong (name, thm) = + Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm]; + + val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss; + in + [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps), + Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)), + Pretty.big_list "congruences:" (map pretty_cong congs), + Pretty.strs ("loopers:" :: map quote loopers), + Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers), + Pretty.strs ("safe solvers:" :: map quote safe_solvers)] + |> Pretty.chunks + end; + + + (** simpset data **) structure SimpsetData = GenericDataFun