author | wenzelm |
Wed, 31 Dec 2014 14:15:52 +0100 | |
changeset 59208 | 2486d625878b |
parent 59207 | 6b030dc97a4f |
child 59210 | 8658b4290aed |
permissions | -rw-r--r-- |
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; |
|
59208
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
27 |
val gr = |
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
28 |
Sorts.classes_of algebra |
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
29 |
|> Graph.map (fn c => fn _ => |
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
30 |
Graph_Display.content_node (Name_Space.extern ctxt space c) []) |
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
31 |
in Graph_Display.display_graph ([], gr) end; |
58202 | 32 |
|
33 |
val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of); |
|
34 |
val visualize_cmd = gen_visualize Syntax.read_sort; |
|
58201 | 35 |
|
36 |
val _ = |
|
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58202
diff
changeset
|
37 |
Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies" |
58202 | 38 |
((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) => |
39 |
((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub)))); |
|
58201 | 40 |
|
41 |
end; |