src/Pure/Thy/thm_deps.ML
author bulwahn
Sat May 16 20:17:59 2009 +0200 (2009-05-16)
changeset 31174 f1f1e9b53c81
parent 30364 577edc39b501
child 31177 c39994cb152a
permissions -rw-r--r--
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
     1 (*  Title:      Pure/Thy/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: thm list -> unit
    10   val unused_thms: theory list * theory list -> (string * thm) list
    11 end;
    12 
    13 structure ThmDeps: THM_DEPS =
    14 struct
    15 
    16 (* thm_deps *)
    17 
    18 fun thm_deps thms =
    19   let
    20     fun add_dep ("", _, _) = I
    21       | add_dep (name, _, PBody {thms = thms', ...}) =
    22           let
    23             val prefix = #1 (Library.split_last (Long_Name.explode name));
    24             val session =
    25               (case prefix of
    26                 a :: _ =>
    27                   (case ThyInfo.lookup_theory 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           in cons entry end;
    43     val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
    44   in Present.display_graph (sort_wrt #ID deps) end;
    45 
    46 
    47 (* unused_thms *)
    48 
    49 fun unused_thms (base_thys, thys) =
    50   let
    51     fun add_fact (name, ths) =
    52       if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
    53       else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
    54     val thms =
    55       fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
    56       |> sort_distinct (string_ord o pairself #1);
    57 
    58     val tab = Proofterm.fold_body_thms
    59       (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
    60       (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
    61     fun is_unused (name, th) =
    62       not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
    63 
    64     (* groups containing at least one used theorem *)
    65     val grps = fold (fn p as (_, thm) => if is_unused p then I else
    66       case Thm.get_group thm of
    67         NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
    68     val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
    69       if member (op =) [Thm.theoremK, Thm.generated_theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
    70         andalso is_unused p
    71       then
    72         (case Thm.get_group thm of
    73            NONE => (p :: thms, grps')
    74          | SOME grp =>
    75              (* do not output theorem if another theorem in group has been used *)
    76              if Symtab.defined grps grp then q
    77              (* output at most one unused theorem per group *)
    78              else if Symtab.defined grps' grp then q
    79              else (p :: thms, Symtab.update (grp, ()) grps'))
    80       else q) thms ([], Symtab.empty)
    81   in rev thms' end;
    82 
    83 end;
    84