src/Pure/Thy/thm_deps.ML
author wenzelm
Tue Aug 27 11:06:20 2002 +0200 (2002-08-27)
changeset 13530 4813fdc0ef17
parent 12239 ee360f910ec8
child 14981 e73f8140af78
permissions -rw-r--r--
Thm.proof_of;
berghofe@7765
     1
(*  Title:      Pure/Thy/thm_deps.ML
berghofe@7765
     2
    ID:         $Id$
berghofe@7765
     3
    Author:     Stefan Berghofer, TU Muenchen
wenzelm@11819
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@7765
     5
berghofe@7765
     6
Visualize dependencies of theorems.
berghofe@7765
     7
*)
berghofe@7765
     8
berghofe@7785
     9
signature BASIC_THM_DEPS =
berghofe@7785
    10
sig
berghofe@7785
    11
  val thm_deps : thm list -> unit
berghofe@7785
    12
end;
berghofe@7785
    13
berghofe@7765
    14
signature THM_DEPS =
berghofe@7765
    15
sig
berghofe@7785
    16
  include BASIC_THM_DEPS
berghofe@7785
    17
  val enable : unit -> unit
berghofe@7785
    18
  val disable : unit -> unit
berghofe@7765
    19
end;
berghofe@7765
    20
berghofe@7765
    21
structure ThmDeps : THM_DEPS =
berghofe@7765
    22
struct
berghofe@7765
    23
berghofe@11530
    24
open Proofterm;
berghofe@7765
    25
wenzelm@11543
    26
fun enable () = if ! proofs = 0 then proofs := 1 else ();
wenzelm@11543
    27
fun disable () = proofs := 0;
berghofe@7765
    28
berghofe@11530
    29
fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
berghofe@11530
    30
  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])
berghofe@11530
    31
  | dest_thm_axm _ = (("", []), MinProof []);
berghofe@7765
    32
berghofe@11530
    33
fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf)
berghofe@11530
    34
  | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf)
berghofe@11612
    35
  | make_deps_graph (p, prf1 %% prf2) =
berghofe@11530
    36
      make_deps_graph (make_deps_graph (p, prf1), prf2)
berghofe@11612
    37
  | make_deps_graph (p, prf % _) = make_deps_graph (p, prf)
berghofe@11530
    38
  | make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs)
berghofe@11530
    39
  | make_deps_graph (p as (gra, parents), prf) =
berghofe@11530
    40
      let val ((name, tags), prf') = dest_thm_axm prf
berghofe@11530
    41
      in
berghofe@11530
    42
        if name <> "" andalso not (Drule.has_internal tags) then
berghofe@11530
    43
          if is_none (Symtab.lookup (gra, name)) then
berghofe@11530
    44
            let
berghofe@11530
    45
              val (gra', parents') = make_deps_graph ((gra, []), prf');
berghofe@11530
    46
              val prefx = #1 (Library.split_last (NameSpace.unpack name));
berghofe@11530
    47
              val session =
berghofe@11530
    48
                (case prefx of
berghofe@11530
    49
                  (x :: _) =>
berghofe@11530
    50
                    (case ThyInfo.lookup_theory x of
berghofe@11530
    51
                      Some thy =>
berghofe@11530
    52
                        let val name = #name (Present.get_info thy)
berghofe@11530
    53
                        in if name = "" then [] else [name] end 
berghofe@11530
    54
                    | None => [])
berghofe@11530
    55
                 | _ => ["global"]);
berghofe@11530
    56
            in
berghofe@12239
    57
              if name mem parents' then (gra', parents union parents')
berghofe@12239
    58
              else (Symtab.update ((name,
berghofe@11530
    59
                {name = Sign.base_name name, ID = name,
berghofe@11530
    60
                 dir = space_implode "/" (session @ prefx),
berghofe@11530
    61
                 unfold = false, path = "", parents = parents'}), gra'),
berghofe@11530
    62
               name ins parents)
berghofe@11530
    63
            end
berghofe@11530
    64
          else (gra, name ins parents)
berghofe@11530
    65
        else
berghofe@11530
    66
          make_deps_graph ((gra, parents), prf')
berghofe@11530
    67
      end;
berghofe@7765
    68
berghofe@7765
    69
fun thm_deps thms =
berghofe@7765
    70
  let
berghofe@7765
    71
    val _ = writeln "Generating graph ...";
berghofe@7765
    72
    val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
wenzelm@13530
    73
      map Thm.proof_of thms))));
berghofe@7765
    74
    val path = File.tmp_path (Path.unpack "theorems.graph");
wenzelm@9450
    75
    val _ = Present.write_graph gra path;
wenzelm@7853
    76
    val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
berghofe@7765
    77
  in () end;
berghofe@7765
    78
berghofe@7765
    79
end;
berghofe@7765
    80
berghofe@7785
    81
structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
berghofe@7785
    82
open BasicThmDeps;