berghofe@7765: (*  Title:      Pure/Thy/thm_deps.ML
berghofe@7765:     ID:         $Id$
berghofe@7765:     Author:     Stefan Berghofer, TU Muenchen
berghofe@7765: 
berghofe@7765: Visualize dependencies of theorems.
berghofe@7765: *)
berghofe@7765: 
berghofe@7785: signature BASIC_THM_DEPS =
berghofe@7785: sig
berghofe@7785:   val thm_deps : thm list -> unit
berghofe@7785: end;
berghofe@7785: 
berghofe@7765: signature THM_DEPS =
berghofe@7765: sig
berghofe@7785:   include BASIC_THM_DEPS
berghofe@7785:   val enable : unit -> unit
berghofe@7785:   val disable : unit -> unit
berghofe@7765: end;
berghofe@7765: 
berghofe@7765: structure ThmDeps : THM_DEPS =
berghofe@7765: struct
berghofe@7765: 
berghofe@11530: open Proofterm;
berghofe@7765: 
wenzelm@11543: fun enable () = if ! proofs = 0 then proofs := 1 else ();
wenzelm@11543: fun disable () = proofs := 0;
berghofe@7765: 
berghofe@11530: fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
berghofe@11530:   | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])
berghofe@11530:   | dest_thm_axm _ = (("", []), MinProof []);
berghofe@7765: 
berghofe@11530: fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf)
berghofe@11530:   | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf)
berghofe@11612:   | make_deps_graph (p, prf1 %% prf2) =
berghofe@11530:       make_deps_graph (make_deps_graph (p, prf1), prf2)
berghofe@11612:   | make_deps_graph (p, prf % _) = make_deps_graph (p, prf)
skalberg@15570:   | make_deps_graph (p, MinProof prfs) = Library.foldl make_deps_graph (p, prfs)
berghofe@11530:   | make_deps_graph (p as (gra, parents), prf) =
berghofe@11530:       let val ((name, tags), prf') = dest_thm_axm prf
berghofe@11530:       in
berghofe@11530:         if name <> "" andalso not (Drule.has_internal tags) then
berghofe@11530:           if is_none (Symtab.lookup (gra, name)) then
berghofe@11530:             let
berghofe@11530:               val (gra', parents') = make_deps_graph ((gra, []), prf');
berghofe@11530:               val prefx = #1 (Library.split_last (NameSpace.unpack name));
berghofe@11530:               val session =
berghofe@11530:                 (case prefx of
berghofe@11530:                   (x :: _) =>
berghofe@11530:                     (case ThyInfo.lookup_theory x of
skalberg@15531:                       SOME thy =>
berghofe@11530:                         let val name = #name (Present.get_info thy)
berghofe@11530:                         in if name = "" then [] else [name] end 
skalberg@15531:                     | NONE => [])
berghofe@11530:                  | _ => ["global"]);
berghofe@11530:             in
berghofe@12239:               if name mem parents' then (gra', parents union parents')
berghofe@12239:               else (Symtab.update ((name,
berghofe@11530:                 {name = Sign.base_name name, ID = name,
berghofe@11530:                  dir = space_implode "/" (session @ prefx),
berghofe@11530:                  unfold = false, path = "", parents = parents'}), gra'),
berghofe@11530:                name ins parents)
berghofe@11530:             end
berghofe@11530:           else (gra, name ins parents)
berghofe@11530:         else
berghofe@11530:           make_deps_graph ((gra, parents), prf')
berghofe@11530:       end;
berghofe@7765: 
berghofe@7765: fun thm_deps thms =
berghofe@7765:   let
berghofe@7765:     val _ = writeln "Generating graph ...";
skalberg@15570:     val gra = map snd (Symtab.dest (fst (Library.foldl make_deps_graph ((Symtab.empty, []),
wenzelm@13530:       map Thm.proof_of thms))));
berghofe@7765:     val path = File.tmp_path (Path.unpack "theorems.graph");
wenzelm@9450:     val _ = Present.write_graph gra path;
wenzelm@7853:     val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
berghofe@7765:   in () end;
berghofe@7765: 
berghofe@7765: end;
berghofe@7765: 
berghofe@7785: structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
berghofe@7785: open BasicThmDeps;