src/Pure/Thy/thm_deps.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24562 fc3cf01e8af1
child 26138 dc578de1d3e9
permissions -rw-r--r--
Name.uu, Name.aT;
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
wenzelm@21646
    28
fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
wenzelm@21646
    29
  | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
wenzelm@21646
    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) =>
wenzelm@21646
    40
      let val (name, prf') = dest_thm_axm prf
berghofe@11530
    41
      in
wenzelm@21646
    42
        if name <> "" 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, []);
wenzelm@21858
    46
              val prefx = #1 (Library.split_last (NameSpace.explode 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 =>
wenzelm@24562
    52
                        let val name = Present.session_name thy
wenzelm@16268
    53
                        in if name = "" then [] else [name] end
skalberg@15531
    54
                    | NONE => [])
berghofe@11530
    55
                 | _ => ["global"]);
berghofe@11530
    56
            in
wenzelm@20664
    57
              if member (op =) parents' name 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',
haftmann@20854
    62
               insert (op =) name parents)
berghofe@11530
    63
            end
haftmann@20854
    64
          else (gra, insert (op =) name 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 =
wenzelm@20578
    70
  Present.display_graph
wenzelm@20578
    71
    (map snd (Symtab.dest (fst
wenzelm@20578
    72
      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))));
berghofe@7765
    73
berghofe@7765
    74
end;
berghofe@7765
    75
berghofe@7785
    76
structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
berghofe@7785
    77
open BasicThmDeps;