src/Pure/Tools/thm_deps.ML
author wenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058 a78612c67ec0
parent 58893 9e0ecb66d6a7
child 59207 6b030dc97a4f
permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm@57934
     1
(*  Title:      Pure/Tools/thm_deps.ML
berghofe@7765
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@7765
     3
berghofe@7765
     4
Visualize dependencies of theorems.
berghofe@7765
     5
*)
berghofe@7765
     6
berghofe@7765
     7
signature THM_DEPS =
berghofe@7765
     8
sig
wenzelm@37870
     9
  val thm_deps: theory -> thm list -> unit
wenzelm@26697
    10
  val unused_thms: theory list * theory list -> (string * thm) list
berghofe@7765
    11
end;
berghofe@7765
    12
wenzelm@33391
    13
structure Thm_Deps: THM_DEPS =
berghofe@7765
    14
struct
berghofe@7765
    15
wenzelm@26697
    16
(* thm_deps *)
wenzelm@26697
    17
wenzelm@37870
    18
fun thm_deps thy thms =
wenzelm@28810
    19
  let
wenzelm@28826
    20
    fun add_dep ("", _, _) = I
wenzelm@28826
    21
      | add_dep (name, _, PBody {thms = thms', ...}) =
wenzelm@28826
    22
          let
wenzelm@41489
    23
            val prefix = #1 (split_last (Long_Name.explode name));
wenzelm@28826
    24
            val session =
wenzelm@28826
    25
              (case prefix of
wenzelm@28826
    26
                a :: _ =>
wenzelm@37870
    27
                  (case try (Context.get_theory thy) a of
wenzelm@28826
    28
                    SOME thy =>
wenzelm@28826
    29
                      (case Present.session_name thy of
wenzelm@28826
    30
                        "" => []
wenzelm@28826
    31
                      | session => [session])
wenzelm@28826
    32
                  | NONE => [])
wenzelm@28826
    33
               | _ => ["global"]);
wenzelm@28826
    34
            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
wenzelm@28826
    35
            val entry =
wenzelm@30364
    36
              {name = Long_Name.base_name name,
wenzelm@28826
    37
               ID = name,
wenzelm@28826
    38
               dir = space_implode "/" (session @ prefix),
wenzelm@28826
    39
               unfold = false,
wenzelm@28826
    40
               path = "",
wenzelm@49561
    41
               parents = parents,
wenzelm@49561
    42
               content = []};
wenzelm@28826
    43
          in cons entry end;
wenzelm@44333
    44
    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
wenzelm@49561
    45
  in Graph_Display.display_graph (sort_wrt #ID deps) end;
wenzelm@26697
    46
wenzelm@57934
    47
val _ =
wenzelm@58893
    48
  Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
wenzelm@58028
    49
    (Parse.xthms1 >> (fn args =>
wenzelm@57934
    50
      Toplevel.unknown_theory o Toplevel.keep (fn state =>
wenzelm@57934
    51
        thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
wenzelm@57934
    52
wenzelm@26697
    53
wenzelm@26697
    54
(* unused_thms *)
wenzelm@26697
    55
wenzelm@26697
    56
fun unused_thms (base_thys, thys) =
berghofe@26185
    57
  let
wenzelm@33170
    58
    fun add_fact space (name, ths) =
wenzelm@39557
    59
      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
wenzelm@33170
    60
      else
wenzelm@33170
    61
        let val {concealed, group, ...} = Name_Space.the_entry space name in
wenzelm@33170
    62
          fold_rev (fn th =>
wenzelm@36744
    63
            (case Thm.derivation_name th of
wenzelm@33170
    64
              "" => I
wenzelm@33170
    65
            | a => cons (a, (th, concealed, group)))) ths
wenzelm@33170
    66
        end;
wenzelm@33170
    67
    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
wenzelm@33170
    68
wenzelm@33769
    69
    val new_thms =
wenzelm@39557
    70
      fold (add_facts o Global_Theory.facts_of) thys []
wenzelm@59058
    71
      |> sort_distinct (string_ord o apply2 #1);
wenzelm@28810
    72
wenzelm@33769
    73
    val used =
wenzelm@32810
    74
      Proofterm.fold_body_thms
berghofe@41565
    75
        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
wenzelm@44333
    76
        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
wenzelm@44331
    77
        Symtab.empty;
wenzelm@33170
    78
berghofe@41565
    79
    fun is_unused a = not (Symtab.defined used a);
wenzelm@28810
    80
wenzelm@57934
    81
    (*groups containing at least one used theorem*)
berghofe@41565
    82
    val used_groups = fold (fn (a, (_, _, group)) =>
berghofe@41565
    83
      if is_unused a then I
wenzelm@33170
    84
      else
wenzelm@33170
    85
        (case group of
wenzelm@33170
    86
          NONE => I
wenzelm@33769
    87
        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
wenzelm@33769
    88
wenzelm@33769
    89
    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
wenzelm@33769
    90
      if not concealed andalso
wenzelm@42473
    91
        (* FIXME replace by robust treatment of thm groups *)
wenzelm@42473
    92
        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
berghofe@41565
    93
        is_unused a
wenzelm@33769
    94
      then
wenzelm@33170
    95
        (case group of
wenzelm@33769
    96
           NONE => ((a, th) :: thms, seen_groups)
berghofe@26185
    97
         | SOME grp =>
wenzelm@33769
    98
             if Inttab.defined used_groups grp orelse
wenzelm@33769
    99
               Inttab.defined seen_groups grp then q
wenzelm@33769
   100
             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
wenzelm@33769
   101
      else q) new_thms ([], Inttab.empty);
berghofe@26185
   102
  in rev thms' end;
berghofe@26185
   103
wenzelm@57934
   104
val _ =
wenzelm@58893
   105
  Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems"
wenzelm@57934
   106
    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
wenzelm@57934
   107
       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
wenzelm@57934
   108
        Toplevel.keep (fn state =>
wenzelm@57934
   109
          let
wenzelm@57934
   110
            val thy = Toplevel.theory_of state;
wenzelm@57934
   111
            val ctxt = Toplevel.context_of state;
wenzelm@57934
   112
            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
wenzelm@57934
   113
            val get_theory = Context.get_theory thy;
wenzelm@57934
   114
          in
wenzelm@57934
   115
            unused_thms
wenzelm@57934
   116
              (case opt_range of
wenzelm@57934
   117
                NONE => (Theory.parents_of thy, [thy])
wenzelm@57934
   118
              | SOME (xs, NONE) => (map get_theory xs, [thy])
wenzelm@57934
   119
              | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
wenzelm@57934
   120
            |> map pretty_thm |> Pretty.writeln_chunks
wenzelm@57934
   121
          end)));
wenzelm@57934
   122
berghofe@7765
   123
end;
berghofe@7765
   124