src/Pure/Thy/thm_deps.ML
author wenzelm
Sun Jul 23 12:10:11 2000 +0200 (2000-07-23)
changeset 9416 9144976964e7
parent 7853 a4acf1b4d5a8
child 9450 c97dba47e504
permissions -rw-r--r--
removed all_sessions.graph;
improved graph 'directories';
tuned;
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
berghofe@7785
    17
  val enable : unit -> unit
berghofe@7785
    18
  val disable : unit -> unit
berghofe@7765
    19
end;
berghofe@7765
    20
berghofe@7765
    21
structure ThmDeps : THM_DEPS =
berghofe@7765
    22
struct
berghofe@7765
    23
berghofe@7785
    24
fun enable () = Thm.keep_derivs := ThmDeriv;
berghofe@7785
    25
fun disable () = Thm.keep_derivs := MinDeriv;
berghofe@7785
    26
berghofe@7765
    27
fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
berghofe@7765
    28
  else
berghofe@7765
    29
    (case #session (Present.get_info thy) of
berghofe@7765
    30
        [x] => [x, "base"]
berghofe@7765
    31
      | xs => xs);
berghofe@7765
    32
berghofe@7765
    33
fun put_graph gr path =
berghofe@7765
    34
    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
berghofe@7765
    35
      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
berghofe@7765
    36
      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
berghofe@7765
    37
berghofe@7765
    38
fun is_thm_axm (Theorem _) = true
berghofe@7765
    39
  | is_thm_axm (Axiom _) = true
berghofe@7765
    40
  | is_thm_axm _ = false;
berghofe@7765
    41
berghofe@7765
    42
fun get_name (Theorem (s, _)) = s
berghofe@7765
    43
  | get_name (Axiom (s, _)) = s
berghofe@7765
    44
  | get_name _ = "";
berghofe@7765
    45
berghofe@7765
    46
fun make_deps_graph ((gra, parents), Join (ta, ders)) =
berghofe@7765
    47
  let
berghofe@7765
    48
    val name = get_name ta;
berghofe@7765
    49
  in
berghofe@7765
    50
    if is_thm_axm ta then
berghofe@7765
    51
      if is_none (Symtab.lookup (gra, name)) then
berghofe@7765
    52
        let
berghofe@7765
    53
          val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
berghofe@7765
    54
          val prefx = rev (tl (rev (NameSpace.unpack name)));
berghofe@7765
    55
          val session = (case prefx of
berghofe@7765
    56
               (x :: _) => (case ThyInfo.lookup_theory x of
berghofe@7765
    57
                     (Some thy) => get_sess thy
berghofe@7765
    58
                   | None => [])
berghofe@7765
    59
             | _ => ["global"])
berghofe@7765
    60
        in
berghofe@7786
    61
          (Symtab.update ((name,
berghofe@7765
    62
            {name = Sign.base_name name, ID = name,
berghofe@7765
    63
             dir = space_implode "/" (session @ prefx),
berghofe@7765
    64
             unfold = false, path = "", parents = parents'}), gra'), name ins parents)
berghofe@7765
    65
        end
berghofe@7765
    66
      else (gra, name ins parents)
berghofe@7765
    67
    else
berghofe@7765
    68
      foldl make_deps_graph ((gra, parents), ders)
berghofe@7765
    69
  end;
berghofe@7765
    70
berghofe@7765
    71
fun thm_deps thms =
berghofe@7765
    72
  let
berghofe@7765
    73
    val _ = writeln "Generating graph ...";
berghofe@7765
    74
    val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
berghofe@7765
    75
      map (#der o rep_thm) thms))));
berghofe@7765
    76
    val path = File.tmp_path (Path.unpack "theorems.graph");
berghofe@7765
    77
    val _ = put_graph gra path;
wenzelm@7853
    78
    val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
berghofe@7765
    79
  in () end;
berghofe@7765
    80
berghofe@7765
    81
end;
berghofe@7765
    82
berghofe@7785
    83
structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
berghofe@7785
    84
berghofe@7785
    85
open BasicThmDeps;