src/Pure/Thy/thm_deps.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 13530 4813fdc0ef17
child 15531 08c8dad8e399
permissions -rw-r--r--
Merged in license change from Isabelle2004
     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 (nt, prf, _, _)) = (nt, prf)
    29   | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])
    30   | dest_thm_axm _ = (("", []), MinProof []);
    31 
    32 fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf)
    33   | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf)
    34   | make_deps_graph (p, prf1 %% prf2) =
    35       make_deps_graph (make_deps_graph (p, prf1), prf2)
    36   | make_deps_graph (p, prf % _) = make_deps_graph (p, prf)
    37   | make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs)
    38   | make_deps_graph (p as (gra, parents), prf) =
    39       let val ((name, tags), prf') = dest_thm_axm prf
    40       in
    41         if name <> "" andalso not (Drule.has_internal tags) then
    42           if is_none (Symtab.lookup (gra, name)) then
    43             let
    44               val (gra', parents') = make_deps_graph ((gra, []), prf');
    45               val prefx = #1 (Library.split_last (NameSpace.unpack name));
    46               val session =
    47                 (case prefx of
    48                   (x :: _) =>
    49                     (case ThyInfo.lookup_theory x of
    50                       Some thy =>
    51                         let val name = #name (Present.get_info thy)
    52                         in if name = "" then [] else [name] end 
    53                     | None => [])
    54                  | _ => ["global"]);
    55             in
    56               if name mem parents' then (gra', parents union parents')
    57               else (Symtab.update ((name,
    58                 {name = Sign.base_name name, ID = name,
    59                  dir = space_implode "/" (session @ prefx),
    60                  unfold = false, path = "", parents = parents'}), gra'),
    61                name ins parents)
    62             end
    63           else (gra, name ins parents)
    64         else
    65           make_deps_graph ((gra, parents), prf')
    66       end;
    67 
    68 fun thm_deps thms =
    69   let
    70     val _ = writeln "Generating graph ...";
    71     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    72       map Thm.proof_of thms))));
    73     val path = File.tmp_path (Path.unpack "theorems.graph");
    74     val _ = Present.write_graph gra path;
    75     val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    76   in () end;
    77 
    78 end;
    79 
    80 structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
    81 open BasicThmDeps;