src/Pure/Thy/thm_deps.ML
author berghofe
Mon, 19 Nov 2001 17:42:00 +0100
changeset 12239 ee360f910ec8
parent 11819 9283b3c11234
child 13530 4813fdc0ef17
permissions -rw-r--r--
Now handles different theorems with same name more gracefully.
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
11819
9283b3c11234 tuned comments;
wenzelm
parents: 11612
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     5
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     6
Visualize dependencies of theorems.
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
7785
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
     9
signature BASIC_THM_DEPS =
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    10
sig
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    11
  val thm_deps : thm list -> unit
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    12
end;
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    13
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    14
signature THM_DEPS =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    15
sig
7785
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    16
  include BASIC_THM_DEPS
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    17
  val enable : unit -> unit
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    18
  val disable : unit -> unit
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    19
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    20
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    21
structure ThmDeps : THM_DEPS =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    22
struct
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    23
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    24
open Proofterm;
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    25
11543
d61b913431c5 renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents: 11530
diff changeset
    26
fun enable () = if ! proofs = 0 then proofs := 1 else ();
d61b913431c5 renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents: 11530
diff changeset
    27
fun disable () = proofs := 0;
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    28
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    29
fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    30
  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    31
  | dest_thm_axm _ = (("", []), MinProof []);
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    32
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    33
fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf)
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    34
  | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf)
11612
ae8450657bf0 Exchanged % and %%.
berghofe
parents: 11543
diff changeset
    35
  | make_deps_graph (p, prf1 %% prf2) =
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    36
      make_deps_graph (make_deps_graph (p, prf1), prf2)
11612
ae8450657bf0 Exchanged % and %%.
berghofe
parents: 11543
diff changeset
    37
  | make_deps_graph (p, prf % _) = make_deps_graph (p, prf)
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    38
  | make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs)
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    39
  | make_deps_graph (p as (gra, parents), prf) =
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    40
      let val ((name, tags), prf') = dest_thm_axm prf
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    41
      in
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    42
        if name <> "" andalso not (Drule.has_internal tags) then
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    43
          if is_none (Symtab.lookup (gra, name)) then
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    44
            let
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    45
              val (gra', parents') = make_deps_graph ((gra, []), prf');
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    46
              val prefx = #1 (Library.split_last (NameSpace.unpack name));
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    47
              val session =
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    48
                (case prefx of
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    49
                  (x :: _) =>
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    50
                    (case ThyInfo.lookup_theory x of
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    51
                      Some thy =>
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    52
                        let val name = #name (Present.get_info thy)
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    53
                        in if name = "" then [] else [name] end 
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    54
                    | None => [])
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    55
                 | _ => ["global"]);
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    56
            in
12239
ee360f910ec8 Now handles different theorems with same name more gracefully.
berghofe
parents: 11819
diff changeset
    57
              if name mem parents' then (gra', parents union parents')
ee360f910ec8 Now handles different theorems with same name more gracefully.
berghofe
parents: 11819
diff changeset
    58
              else (Symtab.update ((name,
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    59
                {name = Sign.base_name name, ID = name,
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    60
                 dir = space_implode "/" (session @ prefx),
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    61
                 unfold = false, path = "", parents = parents'}), gra'),
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    62
               name ins parents)
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    63
            end
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    64
          else (gra, name ins parents)
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    65
        else
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    66
          make_deps_graph ((gra, parents), prf')
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    67
      end;
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    68
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    69
fun thm_deps thms =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    70
  let
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    71
    val _ = writeln "Generating graph ...";
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    72
    val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
9502
50ec59aff389 adapted deriv;
wenzelm
parents: 9450
diff changeset
    73
      map (#2 o #der o Thm.rep_thm) thms))));
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    74
    val path = File.tmp_path (Path.unpack "theorems.graph");
9450
wenzelm
parents: 7853
diff changeset
    75
    val _ = Present.write_graph gra path;
7853
a4acf1b4d5a8 system;
wenzelm
parents: 7786
diff changeset
    76
    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
    77
  in () end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    78
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    79
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    80
7785
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    81
structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
c06825c396e8 Added functions for enabling and disabling derivations.
berghofe
parents: 7783
diff changeset
    82
open BasicThmDeps;