src/Pure/Thy/thm_deps.ML
changeset 7765 fa28bac7903c
child 7783 9ace4017ead8
equal deleted inserted replaced
7764:9be1caad9782 7765:fa28bac7903c
       
     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 THM_DEPS =
       
     9 sig
       
    10   val thm_deps: thm list -> unit
       
    11 end;
       
    12 
       
    13 structure ThmDeps : THM_DEPS =
       
    14 struct
       
    15 
       
    16 fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
       
    17   else
       
    18     (case #session (Present.get_info thy) of
       
    19         [x] => [x, "base"]
       
    20       | xs => xs);
       
    21 
       
    22 fun put_graph gr path =
       
    23     File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
       
    24       "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
       
    25       path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
       
    26 
       
    27 fun is_thm_axm (Theorem _) = true
       
    28   | is_thm_axm (Axiom _) = true
       
    29   | is_thm_axm _ = false;
       
    30 
       
    31 fun get_name (Theorem (s, _)) = s
       
    32   | get_name (Axiom (s, _)) = s
       
    33   | get_name _ = "";
       
    34 
       
    35 fun make_deps_graph ((gra, parents), Join (ta, ders)) =
       
    36   let
       
    37     val name = get_name ta;
       
    38   in
       
    39     if is_thm_axm ta then
       
    40       if is_none (Symtab.lookup (gra, name)) then
       
    41         let
       
    42           val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
       
    43           val prefx = rev (tl (rev (NameSpace.unpack name)));
       
    44           val session = (case prefx of
       
    45                (x :: _) => (case ThyInfo.lookup_theory x of
       
    46                      (Some thy) => get_sess thy
       
    47                    | None => [])
       
    48              | _ => ["global"])
       
    49         in
       
    50           (Symtab.update_new ((name,
       
    51             {name = Sign.base_name name, ID = name,
       
    52              dir = space_implode "/" (session @ prefx),
       
    53              unfold = false, path = "", parents = parents'}), gra'), name ins parents)
       
    54         end
       
    55       else (gra, name ins parents)
       
    56     else
       
    57       foldl make_deps_graph ((gra, parents), ders)
       
    58   end;
       
    59 
       
    60 fun thm_deps thms =
       
    61   let
       
    62     val _ = writeln "Generating graph ...";
       
    63     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
       
    64       map (#der o rep_thm) thms))));
       
    65     val path = File.tmp_path (Path.unpack "theorems.graph");
       
    66     val _ = put_graph gra path;
       
    67     val _ = execute ("isatool browser -d " ^ Path.pack (Path.expand path) ^ " &");
       
    68   in () end;
       
    69 
       
    70 end;
       
    71 
       
    72 open ThmDeps;