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