# HG changeset patch
# User berghofe
# Date 939288999 -7200
# Node ID fa28bac7903c863499b3042220ca62d5ea563ca2
# Parent  9be1caad9782bf467dc0213d2aef2ec73b6e908a
New function thm_deps for visualizing dependencies of theorems.

diff -r 9be1caad9782 -r fa28bac7903c src/Pure/Thy/thm_deps.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thm_deps.ML	Thu Oct 07 11:36:39 1999 +0200
@@ -0,0 +1,72 @@
+(*  Title:      Pure/Thy/thm_deps.ML
+    ID:         $Id$
+    Author:     Stefan Berghofer, TU Muenchen
+
+Visualize dependencies of theorems.
+*)
+
+signature THM_DEPS =
+sig
+  val thm_deps: thm list -> unit
+end;
+
+structure ThmDeps : THM_DEPS =
+struct
+
+fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
+  else
+    (case #session (Present.get_info thy) of
+        [x] => [x, "base"]
+      | xs => xs);
+
+fun put_graph gr path =
+    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
+      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
+      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
+
+fun is_thm_axm (Theorem _) = true
+  | is_thm_axm (Axiom _) = true
+  | is_thm_axm _ = false;
+
+fun get_name (Theorem (s, _)) = s
+  | get_name (Axiom (s, _)) = s
+  | get_name _ = "";
+
+fun make_deps_graph ((gra, parents), Join (ta, ders)) =
+  let
+    val name = get_name ta;
+  in
+    if is_thm_axm ta then
+      if is_none (Symtab.lookup (gra, name)) then
+        let
+          val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
+          val prefx = rev (tl (rev (NameSpace.unpack name)));
+          val session = (case prefx of
+               (x :: _) => (case ThyInfo.lookup_theory x of
+                     (Some thy) => get_sess thy
+                   | None => [])
+             | _ => ["global"])
+        in
+          (Symtab.update_new ((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
+      foldl make_deps_graph ((gra, parents), ders)
+  end;
+
+fun thm_deps thms =
+  let
+    val _ = writeln "Generating graph ...";
+    val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
+      map (#der o rep_thm) thms))));
+    val path = File.tmp_path (Path.unpack "theorems.graph");
+    val _ = put_graph gra path;
+    val _ = execute ("isatool browser -d " ^ Path.pack (Path.expand path) ^ " &");
+  in () end;
+
+end;
+
+open ThmDeps;