improved print_ss; tuned;
authorwenzelm
Sun Jul 11 20:34:50 2004 +0200 (2004-07-11)
changeset 15034e1282c4b39be
parent 15033 255bc508a756
child 15035 8c57751cd43f
improved print_ss; tuned;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Sun Jul 11 20:34:25 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sun Jul 11 20:34:50 2004 +0200
     1.3 @@ -73,8 +73,6 @@
     1.4  sig
     1.5    include BASIC_META_SIMPLIFIER
     1.6    exception SIMPLIFIER of string * thm
     1.7 -  val dest_ss: simpset ->
     1.8 -    {simps: thm list, congs: thm list, procs: (string * cterm list) list}
     1.9    val clear_ss: simpset -> simpset
    1.10    exception SIMPROC_FAIL of string * exn
    1.11    val simproc_i: Sign.sg -> string -> term list
    1.12 @@ -184,8 +182,8 @@
    1.13  
    1.14  fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()};
    1.15  
    1.16 +fun solver_name (Solver {name, ...}) = name;
    1.17  fun solver ths (Solver {solver = tacf, ...}) = tacf ths;
    1.18 -
    1.19  fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
    1.20  val merge_solvers = gen_merge_lists eq_solver;
    1.21  
    1.22 @@ -266,26 +264,30 @@
    1.23  
    1.24  (* print simpsets *)
    1.25  
    1.26 -fun dest_ss (Simpset ({rules, ...}, {congs = (congs, _), procs, ...})) =
    1.27 -  {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
    1.28 -   congs = map (fn (_, {thm, ...}) => thm) congs,
    1.29 -   procs =
    1.30 -     map (fn (_, Proc {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
    1.31 -     |> partition_eq eq_snd
    1.32 -     |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
    1.33 -     |> Library.sort_wrt #1};
    1.34 -
    1.35  fun print_ss ss =
    1.36    let
    1.37 -    val {simps, procs, congs} = dest_ss ss;
    1.38 +    val pretty_thms = map Display.pretty_thm;
    1.39  
    1.40 -    val pretty_thms = map Display.pretty_thm;
    1.41 +    fun pretty_cong (name, th) =
    1.42 +      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, Display.pretty_thm th];
    1.43      fun pretty_proc (name, lhss) =
    1.44        Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
    1.45 +
    1.46 +    val Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = ss;
    1.47 +    val smps = map (#thm o #2) (Net.dest rules);
    1.48 +    val cngs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs);
    1.49 +    val prcs = Net.dest procs |>
    1.50 +      map (fn (_, Proc {name, lhs, id, ...}) => ((name, lhs), id))
    1.51 +      |> partition_eq eq_snd
    1.52 +      |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
    1.53 +      |> Library.sort_wrt #1;
    1.54    in
    1.55 -    [Pretty.big_list "simplification rules:" (pretty_thms simps),
    1.56 -      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
    1.57 -      Pretty.big_list "congruences:" (pretty_thms congs)]
    1.58 +    [Pretty.big_list "simplification rules:" (pretty_thms smps),
    1.59 +      Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
    1.60 +      Pretty.big_list "congruences:" (map pretty_cong cngs),
    1.61 +      Pretty.strs ("loopers:" :: map #1 loop_tacs),
    1.62 +      Pretty.strs ("unsafe solvers:" :: map solver_name (#1 solvers)),
    1.63 +      Pretty.strs ("safe solvers:" :: map solver_name (#2 solvers))]
    1.64      |> Pretty.chunks |> Pretty.writeln
    1.65    end;
    1.66  
    1.67 @@ -664,9 +666,10 @@
    1.68  
    1.69  fun ss delloop name = ss |>
    1.70    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.71 -    let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
    1.72 -      if null del then warning ("No such looper in simpset: " ^ quote name) else ();
    1.73 -      (congs, procs, mk_rews, termless, subgoal_tac, rest, solvers)
    1.74 +    let val loop_tacs' = filter_out (equal name o #1) loop_tacs in
    1.75 +      if length loop_tacs <> length loop_tacs' then ()
    1.76 +      else warning ("No such looper in simpset: " ^ quote name);
    1.77 +      (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs', solvers)
    1.78      end);
    1.79  
    1.80  fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,