src/Pure/Thy/thm_deps.ML
author wenzelm
Wed Aug 02 19:40:14 2000 +0200 (2000-08-02)
changeset 9502 50ec59aff389
parent 9450 c97dba47e504
child 11530 b6e21f6cfacd
permissions -rw-r--r--
adapted deriv;
     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 fun enable () = Thm.keep_derivs := ThmDeriv;
    24 fun disable () = Thm.keep_derivs := MinDeriv;
    25 
    26 fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags;
    27 
    28 fun is_thm_axm (Theorem x) = not (is_internal x)
    29   | is_thm_axm (Axiom x) = not (is_internal x)
    30   | is_thm_axm _ = false;
    31 
    32 fun get_name (Theorem (s, _)) = s
    33   | get_name (Axiom (s, _)) = s
    34   | get_name _ = "";
    35 
    36 fun make_deps_graph ((gra, parents), Join (ta, ders)) =
    37   let
    38     val name = get_name ta;
    39   in
    40     if is_thm_axm ta then
    41       if is_none (Symtab.lookup (gra, name)) then
    42         let
    43           val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
    44           val prefx = #1 (Library.split_last (NameSpace.unpack name));
    45           val session =
    46             (case prefx of
    47               (x :: _) =>
    48                 (case ThyInfo.lookup_theory x of
    49                   Some thy =>
    50                     let val name = #name (Present.get_info thy)
    51                     in if name = "" then [] else [name] end 
    52                 | None => [])
    53              | _ => ["global"]);
    54         in
    55           (Symtab.update ((name,
    56             {name = Sign.base_name name, ID = name,
    57              dir = space_implode "/" (session @ prefx),
    58              unfold = false, path = "", parents = parents'}), gra'), name ins parents)
    59         end
    60       else (gra, name ins parents)
    61     else
    62       foldl make_deps_graph ((gra, parents), ders)
    63   end;
    64 
    65 fun thm_deps thms =
    66   let
    67     val _ = writeln "Generating graph ...";
    68     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    69       map (#2 o #der o Thm.rep_thm) thms))));
    70     val path = File.tmp_path (Path.unpack "theorems.graph");
    71     val _ = Present.write_graph gra path;
    72     val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    73   in () end;
    74 
    75 end;
    76 
    77 structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
    78 open BasicThmDeps;