src/Pure/Thy/thm_deps.ML
author wenzelm
Thu Sep 15 17:16:56 2005 +0200 (2005-09-15)
changeset 17412 e26cb20ef0cc
parent 17224 a78339014063
child 18799 f137c5e971f5
permissions -rw-r--r--
TableFun/Symtab: curried lookup and update;
berghofe@7765
     1
(*  Title:      Pure/Thy/thm_deps.ML
berghofe@7765
     2
    ID:         $Id$
berghofe@7765
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@7765
     4
berghofe@7765
     5
Visualize dependencies of theorems.
berghofe@7765
     6
*)
berghofe@7765
     7
berghofe@7785
     8
signature BASIC_THM_DEPS =
berghofe@7785
     9
sig
berghofe@7785
    10
  val thm_deps : thm list -> unit
berghofe@7785
    11
end;
berghofe@7785
    12
berghofe@7765
    13
signature THM_DEPS =
berghofe@7765
    14
sig
berghofe@7785
    15
  include BASIC_THM_DEPS
berghofe@7785
    16
  val enable : unit -> unit
berghofe@7785
    17
  val disable : unit -> unit
berghofe@7765
    18
end;
berghofe@7765
    19
berghofe@7765
    20
structure ThmDeps : THM_DEPS =
berghofe@7765
    21
struct
berghofe@7765
    22
berghofe@11530
    23
open Proofterm;
berghofe@7765
    24
wenzelm@11543
    25
fun enable () = if ! proofs = 0 then proofs := 1 else ();
wenzelm@11543
    26
fun disable () = proofs := 0;
berghofe@7765
    27
berghofe@11530
    28
fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
berghofe@17020
    29
  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], []))
berghofe@17020
    30
  | dest_thm_axm _ = (("", []), MinProof ([], [], []));
berghofe@7765
    31
berghofe@17020
    32
fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
berghofe@17020
    33
  | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
berghofe@17020
    34
  | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2
berghofe@17020
    35
  | make_deps_graph (prf % _) = make_deps_graph prf
berghofe@17020
    36
  | make_deps_graph (MinProof (thms, axms, _)) =
berghofe@17020
    37
      fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
berghofe@17020
    38
      fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
berghofe@17020
    39
  | make_deps_graph prf = (fn p as (gra, parents) =>
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
wenzelm@16894
    43
          if not (Symtab.defined gra name) then
berghofe@11530
    44
            let
berghofe@17020
    45
              val (gra', parents') = make_deps_graph prf' (gra, []);
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
skalberg@15531
    51
                      SOME thy =>
berghofe@11530
    52
                        let val name = #name (Present.get_info thy)
wenzelm@16268
    53
                        in if name = "" then [] else [name] end
skalberg@15531
    54
                    | NONE => [])
berghofe@11530
    55
                 | _ => ["global"]);
berghofe@11530
    56
            in
berghofe@12239
    57
              if name mem parents' then (gra', parents union parents')
wenzelm@17412
    58
              else (Symtab.update (name,
berghofe@11530
    59
                {name = Sign.base_name name, ID = name,
berghofe@11530
    60
                 dir = space_implode "/" (session @ prefx),
wenzelm@17224
    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@17020
    66
          make_deps_graph prf' (gra, parents)
berghofe@17020
    67
      end);
berghofe@7765
    68
berghofe@7765
    69
fun thm_deps thms =
berghofe@7765
    70
  let
berghofe@7765
    71
    val _ = writeln "Generating graph ...";
berghofe@17020
    72
    val gra = map snd (Symtab.dest (fst
berghofe@17020
    73
      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))));
berghofe@7765
    74
    val path = File.tmp_path (Path.unpack "theorems.graph");
wenzelm@9450
    75
    val _ = Present.write_graph gra path;
wenzelm@16268
    76
    val _ = File.isatool ("browser -d " ^ File.shell_path 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;