src/Pure/Thy/thm_deps.ML
author wenzelm
Sat Aug 20 16:06:27 2011 +0200 (2011-08-20)
changeset 44331 aa9c1e9ef2ce
parent 42473 aca720fb3936
child 44333 cc53ce50f738
permissions -rw-r--r--
clarified fulfill_norm_proof: no join_thms yet;
clarified priority of fulfill_proof_future, which is followed by explicit join_thms;
explicit Thm.future_body_of without join yet;
tuned Thm.future_result: join_promises without fulfill_norm_proof;
     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: 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 add_dep ("", _, _) = I
    21       | add_dep (name, _, PBody {thms = thms', ...}) =
    22           let
    23             val prefix = #1 (split_last (Long_Name.explode name));
    24             val session =
    25               (case prefix of
    26                 a :: _ =>
    27                   (case try (Context.get_theory thy) 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 (Future.joins (map Thm.future_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 space (name, ths) =
    52       if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
    53       else
    54         let val {concealed, group, ...} = Name_Space.the_entry space name in
    55           fold_rev (fn th =>
    56             (case Thm.derivation_name th of
    57               "" => I
    58             | a => cons (a, (th, concealed, group)))) ths
    59         end;
    60     fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
    61 
    62     val new_thms =
    63       fold (add_facts o Global_Theory.facts_of) thys []
    64       |> sort_distinct (string_ord o pairself #1);
    65 
    66     val used =
    67       Proofterm.fold_body_thms
    68         (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
    69         (map Proofterm.strip_thm (Future.joins (map (Thm.future_body_of o #1 o #2) new_thms)))
    70         Symtab.empty;
    71 
    72     fun is_unused a = not (Symtab.defined used a);
    73 
    74     (* groups containing at least one used theorem *)
    75     val used_groups = fold (fn (a, (_, _, group)) =>
    76       if is_unused a then I
    77       else
    78         (case group of
    79           NONE => I
    80         | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
    81 
    82     val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
    83       if not concealed andalso
    84         (* FIXME replace by robust treatment of thm groups *)
    85         member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
    86         is_unused a
    87       then
    88         (case group of
    89            NONE => ((a, th) :: thms, seen_groups)
    90          | SOME grp =>
    91              if Inttab.defined used_groups grp orelse
    92                Inttab.defined seen_groups grp then q
    93              else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
    94       else q) new_thms ([], Inttab.empty);
    95   in rev thms' end;
    96 
    97 end;
    98