src/Pure/Thy/thm_deps.ML

structure Thm_Deps;

(*  Title:      Pure/Thy/thm_deps.ML
    Author:     Stefan Berghofer, TU Muenchen

Visualize dependencies of theorems.
*)

signature THM_DEPS =
sig
  val thm_deps: thm list -> unit
  val unused_thms: theory list * theory list -> (string * thm) list
end;

structure Thm_Deps: THM_DEPS =
struct

(* thm_deps *)

fun thm_deps thms =
  let
    fun add_dep ("", _, _) = I
      | add_dep (name, _, PBody {thms = thms', ...}) =
          let
            val prefix = #1 (Library.split_last (Long_Name.explode name));
            val session =
              (case prefix of
                a :: _ =>
                  (case ThyInfo.lookup_theory a of
                    SOME thy =>
                      (case Present.session_name thy of
                        "" => []
                      | session => [session])
                  | NONE => [])
               | _ => ["global"]);
            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
            val entry =
              {name = Long_Name.base_name name,
               ID = name,
               dir = space_implode "/" (session @ prefix),
               unfold = false,
               path = "",
               parents = parents};
          in cons entry end;
    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
  in Present.display_graph (sort_wrt #ID deps) end;


(* unused_thms *)

fun unused_thms (base_thys, thys) =
  let
    fun add_fact space (name, ths) =
      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
      else
        let val {concealed, group, ...} = Name_Space.the_entry space name in
          fold_rev (fn th =>
            (case Thm.get_name th of
              "" => I
            | a => cons (a, (th, concealed, group)))) ths
        end;
    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;

    val thms =
      fold (add_facts o PureThy.facts_of) thys []
      |> sort_distinct (string_ord o pairself #1);

    val tab =
      Proofterm.fold_body_thms
        (fn (a, prop, _) => a <> "" ? Symtab.insert_list (op =) (a, prop))
        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) thms) Symtab.empty;

    fun is_unused (a, th) =
      not (member (op aconv) (Symtab.lookup_list tab a) (Thm.prop_of th));

    (* groups containing at least one used theorem *)
    val used_groups = fold (fn (a, (th, _, group)) =>
      if is_unused (a, th) then I
      else
        (case group of
          NONE => I
        | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty;
    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') =>
      if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
        (Thm.get_kind th) andalso not concealed andalso is_unused (a, th)
      then
        (case group of
           NONE => ((a, th) :: thms, grps')
         | SOME grp =>
             (* do not output theorem if another theorem in group has been used *)
             if Inttab.defined used_groups grp then q
             (* output at most one unused theorem per group *)
             else if Inttab.defined grps' grp then q
             else ((a, th) :: thms, Inttab.update (grp, ()) grps'))
      else q) thms ([], Inttab.empty)
  in rev thms' end;

end;