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