src/Pure/Thy/thm_deps.ML

added command 'thm_oracles';

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

Dependencies of theorems wrt. internal derivation.
*)

signature THM_DEPS =
sig
  val all_oracles: thm list -> Proofterm.oracle list
  val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
  val thm_deps: theory -> thm list -> unit
  val unused_thms: theory list * theory list -> (string * thm) list
end;

structure Thm_Deps: THM_DEPS =
struct

(* oracles *)

fun all_oracles thms =
  Proofterm.all_oracles_of (map Thm.proof_body_of thms);

fun pretty_thm_oracles ctxt thms =
  let
    fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name]
      | prt_oracle (name, SOME prop) =
          [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, Syntax.pretty_term ctxt prop];
  in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;


(* thm_deps *)

fun thm_deps thy thms =
  let
    fun make_node name directory =
      Graph_Display.session_node
       {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
    fun add_dep {name = "", ...} = I
      | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
          let
            val prefix = #1 (split_last (Long_Name.explode name));
            val session =
              (case prefix of
                a :: _ =>
                  (case try (Context.get_theory {long = false} thy) a of
                    SOME thy =>
                      (case Present.theory_qualifier thy of
                        "" => []
                      | session => [session])
                  | NONE => [])
              | _ => ["global"]);
            val node = make_node name (space_implode "/" (session @ prefix));
            val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms');
          in Symtab.update (name, (node, deps)) end;
    val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
    val entries1 =
      Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab =>
        if Symtab.defined tab d then tab
        else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
  in
    Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
    |> Graph_Display.display_graph_old
  end;


(* unused_thms *)

fun unused_thms (base_thys, thys) =
  let
    fun add_fact transfer space (name, ths) =
      if exists (fn thy => Global_Theory.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.derivation_name th of
              "" => I
            | a => cons (a, (transfer th, concealed, group)))) ths
        end;
    fun add_facts thy =
      let
        val transfer = Global_Theory.transfer_theories thy;
        val facts = Global_Theory.facts_of thy;
      in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end;

    val new_thms =
      fold add_facts thys []
      |> sort_distinct (string_ord o apply2 #1);

    val used =
      Proofterm.fold_body_thms
        (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
        Symtab.empty;

    fun is_unused a = not (Symtab.defined used a);

    (*groups containing at least one used theorem*)
    val used_groups = fold (fn (a, (_, _, group)) =>
      if is_unused a then I
      else
        (case group of
          NONE => I
        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;

    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
      if not concealed andalso
        (* FIXME replace by robust treatment of thm groups *)
        Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a
      then
        (case group of
           NONE => ((a, th) :: thms, seen_groups)
         | SOME grp =>
             if Inttab.defined used_groups grp orelse
               Inttab.defined seen_groups grp then q
             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
      else q) new_thms ([], Inttab.empty);
  in rev thms' end;

end;