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