src/Pure/Thy/thm_deps.ML
changeset 7765 fa28bac7903c
child 7783 9ace4017ead8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Oct 07 11:36:39 1999 +0200
     1.3 @@ -0,0 +1,72 @@
     1.4 +(*  Title:      Pure/Thy/thm_deps.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer, TU Muenchen
     1.7 +
     1.8 +Visualize dependencies of theorems.
     1.9 +*)
    1.10 +
    1.11 +signature THM_DEPS =
    1.12 +sig
    1.13 +  val thm_deps: thm list -> unit
    1.14 +end;
    1.15 +
    1.16 +structure ThmDeps : THM_DEPS =
    1.17 +struct
    1.18 +
    1.19 +fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
    1.20 +  else
    1.21 +    (case #session (Present.get_info thy) of
    1.22 +        [x] => [x, "base"]
    1.23 +      | xs => xs);
    1.24 +
    1.25 +fun put_graph gr path =
    1.26 +    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
    1.27 +      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.28 +      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
    1.29 +
    1.30 +fun is_thm_axm (Theorem _) = true
    1.31 +  | is_thm_axm (Axiom _) = true
    1.32 +  | is_thm_axm _ = false;
    1.33 +
    1.34 +fun get_name (Theorem (s, _)) = s
    1.35 +  | get_name (Axiom (s, _)) = s
    1.36 +  | get_name _ = "";
    1.37 +
    1.38 +fun make_deps_graph ((gra, parents), Join (ta, ders)) =
    1.39 +  let
    1.40 +    val name = get_name ta;
    1.41 +  in
    1.42 +    if is_thm_axm ta then
    1.43 +      if is_none (Symtab.lookup (gra, name)) then
    1.44 +        let
    1.45 +          val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
    1.46 +          val prefx = rev (tl (rev (NameSpace.unpack name)));
    1.47 +          val session = (case prefx of
    1.48 +               (x :: _) => (case ThyInfo.lookup_theory x of
    1.49 +                     (Some thy) => get_sess thy
    1.50 +                   | None => [])
    1.51 +             | _ => ["global"])
    1.52 +        in
    1.53 +          (Symtab.update_new ((name,
    1.54 +            {name = Sign.base_name name, ID = name,
    1.55 +             dir = space_implode "/" (session @ prefx),
    1.56 +             unfold = false, path = "", parents = parents'}), gra'), name ins parents)
    1.57 +        end
    1.58 +      else (gra, name ins parents)
    1.59 +    else
    1.60 +      foldl make_deps_graph ((gra, parents), ders)
    1.61 +  end;
    1.62 +
    1.63 +fun thm_deps thms =
    1.64 +  let
    1.65 +    val _ = writeln "Generating graph ...";
    1.66 +    val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    1.67 +      map (#der o rep_thm) thms))));
    1.68 +    val path = File.tmp_path (Path.unpack "theorems.graph");
    1.69 +    val _ = put_graph gra path;
    1.70 +    val _ = execute ("isatool browser -d " ^ Path.pack (Path.expand path) ^ " &");
    1.71 +  in () end;
    1.72 +
    1.73 +end;
    1.74 +
    1.75 +open ThmDeps;