src/Pure/Tools/thm_deps.ML
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 66037 58d2e41afbfe
child 68482 cb84beb84ca9
permissions -rw-r--r--
tuned signature;
     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 make_node name directory =
    21       Graph_Display.session_node
    22        {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
    23     fun add_dep {name = "", ...} = I
    24       | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
    25           let
    26             val prefix = #1 (split_last (Long_Name.explode name));
    27             val session =
    28               (case prefix of
    29                 a :: _ =>
    30                   (case try (Context.get_theory thy) a of
    31                     SOME thy =>
    32                       (case Present.theory_qualifier thy of
    33                         "" => []
    34                       | session => [session])
    35                   | NONE => [])
    36               | _ => ["global"]);
    37             val node = make_node name (space_implode "/" (session @ prefix));
    38             val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms');
    39           in Symtab.update (name, (node, deps)) end;
    40     val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
    41     val entries1 =
    42       Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab =>
    43         if Symtab.defined tab d then tab
    44         else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
    45   in
    46     Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
    47     |> Graph_Display.display_graph_old
    48   end;
    49 
    50 
    51 (* unused_thms *)
    52 
    53 fun unused_thms (base_thys, thys) =
    54   let
    55     fun add_fact transfer space (name, ths) =
    56       if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
    57       else
    58         let val {concealed, group, ...} = Name_Space.the_entry space name in
    59           fold_rev (fn th =>
    60             (case Thm.derivation_name th of
    61               "" => I
    62             | a => cons (a, (transfer th, concealed, group)))) ths
    63         end;
    64     fun add_facts thy =
    65       let
    66         val transfer = Global_Theory.transfer_theories thy;
    67         val facts = Global_Theory.facts_of thy;
    68       in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end;
    69 
    70     val new_thms =
    71       fold add_facts thys []
    72       |> sort_distinct (string_ord o apply2 #1);
    73 
    74     val used =
    75       Proofterm.fold_body_thms
    76         (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
    77         (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
    78         Symtab.empty;
    79 
    80     fun is_unused a = not (Symtab.defined used a);
    81 
    82     (*groups containing at least one used theorem*)
    83     val used_groups = fold (fn (a, (_, _, group)) =>
    84       if is_unused a then I
    85       else
    86         (case group of
    87           NONE => I
    88         | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
    89 
    90     val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
    91       if not concealed andalso
    92         (* FIXME replace by robust treatment of thm groups *)
    93         Thm.legacy_get_kind th = Thm.theoremK andalso 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 end;