58201
|
1 |
(* Title: Pure/Tools/class_deps.ML
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
|
|
4 |
Visualization of class dependencies.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature CLASS_DEPS =
|
|
8 |
sig
|
58202
|
9 |
val visualize: Proof.context -> sort -> sort option -> unit
|
|
10 |
val visualize_cmd: Proof.context -> string -> string option -> unit
|
58201
|
11 |
end;
|
|
12 |
|
|
13 |
structure Class_deps: CLASS_DEPS =
|
|
14 |
struct
|
|
15 |
|
58202
|
16 |
fun gen_visualize prep_sort ctxt raw_super raw_sub =
|
58201
|
17 |
let
|
58202
|
18 |
val super = prep_sort ctxt raw_super;
|
|
19 |
val sub = Option.map (prep_sort ctxt) raw_sub;
|
|
20 |
val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
|
|
21 |
fun le_super class = Sorts.sort_le original_algebra ([class], super);
|
|
22 |
val sub_le = case sub of
|
|
23 |
NONE => K true |
|
|
24 |
SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]);
|
|
25 |
val (_, algebra) = Sorts.subalgebra (Context.pretty ctxt)
|
|
26 |
(le_super andf sub_le) (K NONE) original_algebra;
|
58201
|
27 |
val classes = Sorts.classes_of algebra;
|
|
28 |
fun entry (c, (i, (_, cs))) =
|
|
29 |
(i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
|
|
30 |
dir = "", unfold = true, path = "", content = []});
|
|
31 |
val gr =
|
|
32 |
Graph.fold (cons o entry) classes []
|
|
33 |
|> sort (int_ord o pairself #1) |> map #2;
|
58202
|
34 |
in Graph_Display.display_graph gr end;
|
|
35 |
|
|
36 |
val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
|
|
37 |
val visualize_cmd = gen_visualize Syntax.read_sort;
|
58201
|
38 |
|
|
39 |
val _ =
|
|
40 |
Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
|
58202
|
41 |
((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
|
|
42 |
((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
|
58201
|
43 |
|
|
44 |
end;
|