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@7765: signature THM_DEPS = berghofe@7765: sig berghofe@7765: val thm_deps: thm list -> unit berghofe@7765: end; berghofe@7765: berghofe@7765: structure ThmDeps : THM_DEPS = berghofe@7765: struct berghofe@7765: berghofe@7765: fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"] berghofe@7765: else berghofe@7765: (case #session (Present.get_info thy) of berghofe@7765: [x] => [x, "base"] berghofe@7765: | xs => xs); berghofe@7765: berghofe@7765: fun put_graph gr path = berghofe@7765: File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => berghofe@7765: "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ berghofe@7765: path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); berghofe@7765: berghofe@7765: fun is_thm_axm (Theorem _) = true berghofe@7765: | is_thm_axm (Axiom _) = true berghofe@7765: | is_thm_axm _ = false; berghofe@7765: berghofe@7765: fun get_name (Theorem (s, _)) = s berghofe@7765: | get_name (Axiom (s, _)) = s berghofe@7765: | get_name _ = ""; berghofe@7765: berghofe@7765: fun make_deps_graph ((gra, parents), Join (ta, ders)) = berghofe@7765: let berghofe@7765: val name = get_name ta; berghofe@7765: in berghofe@7765: if is_thm_axm ta then berghofe@7765: if is_none (Symtab.lookup (gra, name)) then berghofe@7765: let berghofe@7765: val (gra', parents') = foldl make_deps_graph ((gra, []), ders); berghofe@7765: val prefx = rev (tl (rev (NameSpace.unpack name))); berghofe@7765: val session = (case prefx of berghofe@7765: (x :: _) => (case ThyInfo.lookup_theory x of berghofe@7765: (Some thy) => get_sess thy berghofe@7765: | None => []) berghofe@7765: | _ => ["global"]) berghofe@7765: in berghofe@7765: (Symtab.update_new ((name, berghofe@7765: {name = Sign.base_name name, ID = name, berghofe@7765: dir = space_implode "/" (session @ prefx), berghofe@7765: unfold = false, path = "", parents = parents'}), gra'), name ins parents) berghofe@7765: end berghofe@7765: else (gra, name ins parents) berghofe@7765: else berghofe@7765: foldl make_deps_graph ((gra, parents), ders) berghofe@7765: end; berghofe@7765: berghofe@7765: fun thm_deps thms = berghofe@7765: let berghofe@7765: val _ = writeln "Generating graph ..."; berghofe@7765: val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), berghofe@7765: map (#der o rep_thm) thms)))); berghofe@7765: val path = File.tmp_path (Path.unpack "theorems.graph"); berghofe@7765: val _ = put_graph gra path; berghofe@7765: val _ = execute ("isatool browser -d " ^ Path.pack (Path.expand path) ^ " &"); berghofe@7765: in () end; berghofe@7765: berghofe@7765: end; berghofe@7765: berghofe@7765: open ThmDeps;