src/Pure/Thy/thm_deps.ML
author wenzelm
Thu, 07 Oct 1999 14:32:18 +0200
changeset 7783 9ace4017ead8
parent 7765 fa28bac7903c
child 7785 c06825c396e8
permissions -rw-r--r--
$ISATOOL;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thm_deps.ML
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     4
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     5
Visualize dependencies of theorems.
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     6
*)
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     7
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     8
signature THM_DEPS =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     9
sig
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    10
  val thm_deps: thm list -> unit
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    11
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    12
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    13
structure ThmDeps : THM_DEPS =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    14
struct
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    15
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    16
fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    17
  else
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    18
    (case #session (Present.get_info thy) of
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    19
        [x] => [x, "base"]
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    20
      | xs => xs);
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    21
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    22
fun put_graph gr path =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    23
    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    24
      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    25
      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    26
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    27
fun is_thm_axm (Theorem _) = true
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    28
  | is_thm_axm (Axiom _) = true
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    29
  | is_thm_axm _ = false;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    30
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    31
fun get_name (Theorem (s, _)) = s
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    32
  | get_name (Axiom (s, _)) = s
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    33
  | get_name _ = "";
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    34
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    35
fun make_deps_graph ((gra, parents), Join (ta, ders)) =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    36
  let
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    37
    val name = get_name ta;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    38
  in
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    39
    if is_thm_axm ta then
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    40
      if is_none (Symtab.lookup (gra, name)) then
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    41
        let
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    42
          val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    43
          val prefx = rev (tl (rev (NameSpace.unpack name)));
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    44
          val session = (case prefx of
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    45
               (x :: _) => (case ThyInfo.lookup_theory x of
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    46
                     (Some thy) => get_sess thy
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    47
                   | None => [])
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    48
             | _ => ["global"])
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    49
        in
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    50
          (Symtab.update_new ((name,
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    51
            {name = Sign.base_name name, ID = name,
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    52
             dir = space_implode "/" (session @ prefx),
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    53
             unfold = false, path = "", parents = parents'}), gra'), name ins parents)
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    54
        end
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    55
      else (gra, name ins parents)
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    56
    else
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    57
      foldl make_deps_graph ((gra, parents), ders)
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    58
  end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    59
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    60
fun thm_deps thms =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    61
  let
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    62
    val _ = writeln "Generating graph ...";
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    63
    val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    64
      map (#der o rep_thm) thms))));
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    65
    val path = File.tmp_path (Path.unpack "theorems.graph");
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    66
    val _ = put_graph gra path;
7783
9ace4017ead8 $ISATOOL;
wenzelm
parents: 7765
diff changeset
    67
    val _ = execute ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    68
  in () end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    69
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    70
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    71
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    72
open ThmDeps;