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;
     1 (*  Title:      Pure/Thy/thm_deps.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     5 Visualize dependencies of theorems.
     6 *)
     7 
     8 signature BASIC_THM_DEPS =
     9 sig
    10   val thm_deps : thm list -> unit
    11 end;
    12 
    13 signature THM_DEPS =
    14 sig
    15   include BASIC_THM_DEPS
    16   val enable : unit -> unit
    17   val disable : unit -> unit
    18 end;
    19 
    20 structure ThmDeps : THM_DEPS =
    21 struct
    22 
    23 open Proofterm;
    24 
    25 fun enable () = if ! proofs = 0 then proofs := 1 else ();
    26 fun disable () = proofs := 0;
    27 
    28 fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
    29   | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
    30   | dest_thm_axm _ = ("", MinProof ([], [], []));
    31 
    32 fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
    33   | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
    34   | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2
    35   | make_deps_graph (prf % _) = make_deps_graph prf
    36   | make_deps_graph (MinProof (thms, axms, _)) =
    37       fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
    38       fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
    39   | make_deps_graph prf = (fn p as (gra, parents) =>
    40       let val (name, prf') = dest_thm_axm prf
    41       in
    42         if name <> "" then
    43           if not (Symtab.defined gra name) then
    44             let
    45               val (gra', parents') = make_deps_graph prf' (gra, []);
    46               val prefx = #1 (Library.split_last (NameSpace.explode name));
    47               val session =
    48                 (case prefx of
    49                   (x :: _) =>
    50                     (case ThyInfo.lookup_theory x of
    51                       SOME thy =>
    52                         let val name = Present.session_name thy
    53                         in if name = "" then [] else [name] end
    54                     | NONE => [])
    55                  | _ => ["global"]);
    56             in
    57               if member (op =) parents' name then (gra', parents union parents')
    58               else (Symtab.update (name,
    59                 {name = Sign.base_name name, ID = name,
    60                  dir = space_implode "/" (session @ prefx),
    61                  unfold = false, path = "", parents = parents'}) gra',
    62                insert (op =) name parents)
    63             end
    64           else (gra, insert (op =) name parents)
    65         else
    66           make_deps_graph prf' (gra, parents)
    67       end);
    68 
    69 fun thm_deps thms =
    70   Present.display_graph
    71     (map snd (Symtab.dest (fst
    72       (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))));
    73 
    74 end;
    75 
    76 structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
    77 open BasicThmDeps;