src/Pure/Thy/thm_deps.ML
author wenzelm
Sun Nov 16 22:12:44 2008 +0100 (2008-11-16)
changeset 28817 c8cc94a470d4
parent 28814 463c9e9111ae
child 28826 3b460b6eadae
permissions -rw-r--r--
proof_body/pthm: removed redundant types field;
berghofe@7765
     1
(*  Title:      Pure/Thy/thm_deps.ML
berghofe@7765
     2
    ID:         $Id$
berghofe@7765
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@7765
     4
berghofe@7765
     5
Visualize dependencies of theorems.
berghofe@7765
     6
*)
berghofe@7765
     7
berghofe@7765
     8
signature THM_DEPS =
berghofe@7765
     9
sig
wenzelm@26697
    10
  val thm_deps: thm list -> unit
wenzelm@26697
    11
  val unused_thms: theory list * theory list -> (string * thm) list
berghofe@7765
    12
end;
berghofe@7765
    13
wenzelm@26697
    14
structure ThmDeps: THM_DEPS =
berghofe@7765
    15
struct
berghofe@7765
    16
wenzelm@26697
    17
(* thm_deps *)
wenzelm@26697
    18
wenzelm@28817
    19
fun add_dep (name, _, PBody {thms = thms', ...}) =
wenzelm@28810
    20
  name <> "" ?
wenzelm@28810
    21
    Graph.new_node (name, ()) #>
wenzelm@28817
    22
    fold (fn (_, (name', _, _)) => name <> "" ? Graph.add_edge (name', name)) thms';
wenzelm@26697
    23
berghofe@7765
    24
fun thm_deps thms =
wenzelm@28810
    25
  let
wenzelm@28814
    26
    val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) Graph.empty;
wenzelm@28810
    27
    fun add_entry (name, (_, (preds, _))) =
wenzelm@28810
    28
      let
wenzelm@28810
    29
        val prefix = #1 (Library.split_last (NameSpace.explode name));
wenzelm@28810
    30
        val session =
wenzelm@28810
    31
          (case prefix of
wenzelm@28810
    32
            a :: _ =>
wenzelm@28810
    33
              (case ThyInfo.lookup_theory a of
wenzelm@28810
    34
                SOME thy =>
wenzelm@28810
    35
                  (case Present.session_name thy of
wenzelm@28810
    36
                    "" => []
wenzelm@28810
    37
                  | session => [session])
wenzelm@28810
    38
              | NONE => [])
wenzelm@28810
    39
           | _ => ["global"]);
wenzelm@28810
    40
        val entry =
wenzelm@28810
    41
          {name = Sign.base_name name,
wenzelm@28810
    42
           ID = name,
wenzelm@28810
    43
           dir = space_implode "/" (session @ prefix),
wenzelm@28810
    44
           unfold = false,
wenzelm@28810
    45
           path = "",
wenzelm@28810
    46
           parents = preds};
wenzelm@28810
    47
      in cons entry end;
wenzelm@28810
    48
  in Present.display_graph (sort_wrt #ID (Graph.fold add_entry graph [])) 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@26697
    55
    fun add_fact (name, ths) =
wenzelm@26697
    56
      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
wenzelm@26697
    57
      else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
wenzelm@26699
    58
    val thms =
wenzelm@26699
    59
      fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
wenzelm@26699
    60
      |> sort_distinct (string_ord o pairself #1);
wenzelm@28810
    61
wenzelm@28810
    62
    val tab = Proofterm.fold_body_thms
wenzelm@28817
    63
      (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
wenzelm@28814
    64
      (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
wenzelm@28810
    65
    fun is_unused (name, th) =
wenzelm@28810
    66
      not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
wenzelm@28810
    67
berghofe@26185
    68
    (* groups containing at least one used theorem *)
berghofe@26185
    69
    val grps = fold (fn p as (_, thm) => if is_unused p then I else
wenzelm@27865
    70
      case Thm.get_group thm of
berghofe@26185
    71
        NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
berghofe@26185
    72
    val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
wenzelm@27865
    73
      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
berghofe@26185
    74
        andalso is_unused p
berghofe@26185
    75
      then
wenzelm@27865
    76
        (case Thm.get_group thm of
berghofe@26185
    77
           NONE => (p :: thms, grps')
berghofe@26185
    78
         | SOME grp =>
berghofe@26185
    79
             (* do not output theorem if another theorem in group has been used *)
wenzelm@26697
    80
             if Symtab.defined grps grp then q
berghofe@26185
    81
             (* output at most one unused theorem per group *)
wenzelm@26697
    82
             else if Symtab.defined grps' grp then q
berghofe@26185
    83
             else (p :: thms, Symtab.update (grp, ()) grps'))
berghofe@26185
    84
      else q) thms ([], Symtab.empty)
berghofe@26185
    85
  in rev thms' end;
berghofe@26185
    86
berghofe@7765
    87
end;
berghofe@7765
    88