src/Pure/Thy/thm_deps.ML
author wenzelm
Wed, 02 Aug 2000 19:40:14 +0200
changeset 9502 50ec59aff389
parent 9450 c97dba47e504
child 11530 b6e21f6cfacd
permissions -rw-r--r--
adapted deriv;
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
7785
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
     8
signature BASIC_THM_DEPS =
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
     9
sig
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    10
  val thm_deps : thm list -> unit
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    11
end;
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    12
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    13
signature THM_DEPS =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    14
sig
7785
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    15
  include BASIC_THM_DEPS
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    16
  val enable : unit -> unit
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    17
  val disable : unit -> unit
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    18
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    19
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    20
structure ThmDeps : THM_DEPS =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    21
struct
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    22
7785
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    23
fun enable () = Thm.keep_derivs := ThmDeriv;
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    24
fun disable () = Thm.keep_derivs := MinDeriv;
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    25
9450
wenzelm
parents: 7853
diff changeset
    26
fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags;
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    27
9450
wenzelm
parents: 7853
diff changeset
    28
fun is_thm_axm (Theorem x) = not (is_internal x)
wenzelm
parents: 7853
diff changeset
    29
  | is_thm_axm (Axiom x) = not (is_internal x)
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    30
  | is_thm_axm _ = false;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    31
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    32
fun get_name (Theorem (s, _)) = s
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    33
  | get_name (Axiom (s, _)) = s
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    34
  | get_name _ = "";
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    35
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    36
fun make_deps_graph ((gra, parents), Join (ta, ders)) =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    37
  let
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    38
    val name = get_name ta;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    39
  in
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    40
    if is_thm_axm ta then
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    41
      if is_none (Symtab.lookup (gra, name)) then
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    42
        let
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    43
          val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
9450
wenzelm
parents: 7853
diff changeset
    44
          val prefx = #1 (Library.split_last (NameSpace.unpack name));
wenzelm
parents: 7853
diff changeset
    45
          val session =
wenzelm
parents: 7853
diff changeset
    46
            (case prefx of
wenzelm
parents: 7853
diff changeset
    47
              (x :: _) =>
wenzelm
parents: 7853
diff changeset
    48
                (case ThyInfo.lookup_theory x of
wenzelm
parents: 7853
diff changeset
    49
                  Some thy =>
wenzelm
parents: 7853
diff changeset
    50
                    let val name = #name (Present.get_info thy)
wenzelm
parents: 7853
diff changeset
    51
                    in if name = "" then [] else [name] end 
wenzelm
parents: 7853
diff changeset
    52
                | None => [])
wenzelm
parents: 7853
diff changeset
    53
             | _ => ["global"]);
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    54
        in
7786
cf9d07ad62af Replaced update_new by update.
berghofe
parents: 7785
diff changeset
    55
          (Symtab.update ((name,
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    56
            {name = Sign.base_name name, ID = name,
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    57
             dir = space_implode "/" (session @ prefx),
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    58
             unfold = false, path = "", parents = parents'}), gra'), name ins parents)
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    59
        end
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    60
      else (gra, name ins parents)
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    61
    else
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    62
      foldl make_deps_graph ((gra, parents), ders)
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    63
  end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    64
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    65
fun thm_deps thms =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    66
  let
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    67
    val _ = writeln "Generating graph ...";
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    68
    val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
9502
50ec59aff389 adapted deriv;
wenzelm
parents: 9450
diff changeset
    69
      map (#2 o #der o Thm.rep_thm) thms))));
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    70
    val path = File.tmp_path (Path.unpack "theorems.graph");
9450
wenzelm
parents: 7853
diff changeset
    71
    val _ = Present.write_graph gra path;
7853
a4acf1b4d5a8 system;
wenzelm
parents: 7786
diff changeset
    72
    val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    73
  in () end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    74
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    75
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    76
7785
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    77
structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    78
open BasicThmDeps;