(*  Title:      Pure/Thy/thm_deps.ML
    ID:         $Id: thm_deps.ML,v 1.21 2005/09/15 15:17:00 wenzelm Exp $
    Author:     Stefan Berghofer, TU Muenchen

Visualize dependencies of theorems.
*)

signature BASIC_THM_DEPS =
sig
  val thm_deps : thm list -> unit
end;

signature THM_DEPS =
sig
  include BASIC_THM_DEPS
  val enable : unit -> unit
  val disable : unit -> unit
end;

structure ThmDeps : THM_DEPS =
struct

open Proofterm;

fun enable () = if ! proofs = 0 then proofs := 1 else ();
fun disable () = proofs := 0;

fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], []))
  | dest_thm_axm _ = (("", []), MinProof ([], [], []));

fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
  | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
  | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2
  | make_deps_graph (prf % _) = make_deps_graph prf
  | make_deps_graph (MinProof (thms, axms, _)) =
      fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
      fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
  | make_deps_graph prf = (fn p as (gra, parents) =>
      let val ((name, tags), prf') = dest_thm_axm prf
      in
        if name <> "" andalso not (Drule.has_internal tags) then
          if not (Symtab.defined gra name) then
            let
              val (gra', parents') = make_deps_graph prf' (gra, []);
              val prefx = #1 (Library.split_last (NameSpace.unpack name));
              val session =
                (case prefx of
                  (x :: _) =>
                    (case ThyInfo.lookup_theory x of
                      SOME thy =>
                        let val name = #name (Present.get_info thy)
                        in if name = "" then [] else [name] end
                    | NONE => [])
                 | _ => ["global"]);
            in
              if name mem parents' then (gra', parents union parents')
              else (Symtab.update (name,
                {name = Sign.base_name name, ID = name,
                 dir = space_implode "/" (session @ prefx),
                 unfold = false, path = "", parents = parents'}) gra',
               name ins parents)
            end
          else (gra, name ins parents)
        else
          make_deps_graph prf' (gra, parents)
      end);

fun thm_deps thms =
  let
    val _ = writeln "Generating graph ...";
    val gra = map snd (Symtab.dest (fst
      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))));
    val path = File.tmp_path (Path.unpack "theorems.graph");
    val _ = Present.write_graph gra path;
    val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &");
  in () end;

end;

structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
open BasicThmDeps;