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