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@17020: | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], [])) berghofe@17020: | dest_thm_axm _ = (("", []), MinProof ([], [], [])); berghofe@7765: berghofe@17020: fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf berghofe@17020: | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf berghofe@17020: | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2 berghofe@17020: | make_deps_graph (prf % _) = make_deps_graph prf berghofe@17020: | make_deps_graph (MinProof (thms, axms, _)) = berghofe@17020: fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #> berghofe@17020: fold (make_deps_graph o Proofterm.proof_of_min_axm) axms berghofe@17020: | make_deps_graph prf = (fn p as (gra, parents) => berghofe@11530: let val ((name, tags), prf') = dest_thm_axm prf berghofe@11530: in wenzelm@18799: if name <> "" andalso not (PureThy.has_internal tags) then wenzelm@16894: if not (Symtab.defined gra name) then berghofe@11530: let berghofe@17020: val (gra', parents') = make_deps_graph prf' (gra, []); 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) wenzelm@16268: in if name = "" then [] else [name] end skalberg@15531: | NONE => []) berghofe@11530: | _ => ["global"]); berghofe@11530: in wenzelm@20664: if member (op =) parents' name then (gra', parents union parents') wenzelm@17412: else (Symtab.update (name, berghofe@11530: {name = Sign.base_name name, ID = name, berghofe@11530: dir = space_implode "/" (session @ prefx), wenzelm@17224: unfold = false, path = "", parents = parents'}) gra', haftmann@20854: insert (op =) name parents) berghofe@11530: end haftmann@20854: else (gra, insert (op =) name parents) berghofe@11530: else berghofe@17020: make_deps_graph prf' (gra, parents) berghofe@17020: end); berghofe@7765: berghofe@7765: fun thm_deps thms = wenzelm@20578: Present.display_graph wenzelm@20578: (map snd (Symtab.dest (fst wenzelm@20578: (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))); berghofe@7765: berghofe@7765: end; berghofe@7765: berghofe@7785: structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps; berghofe@7785: open BasicThmDeps;