author | haftmann |
Thu, 22 Jan 2015 12:39:44 +0100 | |
changeset 59423 | 3a0044e95eba |
parent 59422 | db6ecef63d5b |
child 59936 | b8ffc3dc9e24 |
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 |
|
59422 | 9 |
val class_deps: Proof.context -> sort list option -> sort list option -> unit |
10 |
val class_deps_cmd: Proof.context -> string list option -> string list option -> unit |
|
58201 | 11 |
end; |
12 |
||
59210
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
13 |
structure Class_Deps: CLASS_DEPS = |
58201 | 14 |
struct |
15 |
||
59422 | 16 |
fun gen_class_deps prep_sort ctxt raw_subs raw_supers = |
58201 | 17 |
let |
59296
002d817b4c37
formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
haftmann
parents:
59210
diff
changeset
|
18 |
val thy = Proof_Context.theory_of ctxt; |
59422 | 19 |
val some_subs = (Option.map o map) (prep_sort ctxt) raw_subs; |
20 |
val some_supers = (Option.map o map) (prep_sort ctxt) raw_supers; |
|
58202 | 21 |
val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); |
59422 | 22 |
val sort_le = curry (Sorts.sort_le original_algebra); |
23 |
val le_sub = case some_subs of |
|
24 |
SOME subs => (fn class => exists (sort_le [class]) subs) |
|
25 |
| NONE => K true; |
|
26 |
val super_le = case some_supers of |
|
27 |
SOME supers => (fn class => exists (fn super => sort_le super [class]) supers) |
|
28 |
| NONE => K true |
|
59210
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
29 |
val (_, algebra) = |
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
30 |
Sorts.subalgebra (Context.pretty ctxt) |
59422 | 31 |
(le_sub andf super_le) (K NONE) original_algebra; |
59423
3a0044e95eba
backed out obsolete workaround from ef1edfb36af7
haftmann
parents:
59422
diff
changeset
|
32 |
fun node c = |
3a0044e95eba
backed out obsolete workaround from ef1edfb36af7
haftmann
parents:
59422
diff
changeset
|
33 |
Graph_Display.content_node (Name_Space.extern ctxt space c) |
3a0044e95eba
backed out obsolete workaround from ef1edfb36af7
haftmann
parents:
59422
diff
changeset
|
34 |
(Class.pretty_specification thy c); |
59210
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
35 |
in |
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
36 |
Sorts.classes_of algebra |
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
37 |
|> Graph.dest |
59383
1434ef1e0ede
clarified Class.pretty_specification: imitate input source;
wenzelm
parents:
59301
diff
changeset
|
38 |
|> map (fn ((c, _), ds) => ((c, node c), ds)) |
59210
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
39 |
|> Graph_Display.display_graph |
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
40 |
end; |
58202 | 41 |
|
59301 | 42 |
val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of); |
43 |
val class_deps_cmd = gen_class_deps Syntax.read_sort; |
|
58201 | 44 |
|
59422 | 45 |
val parse_sort_list = (Parse.sort >> single) |
46 |
|| (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"}); |
|
47 |
||
58201 | 48 |
val _ = |
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58202
diff
changeset
|
49 |
Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies" |
59422 | 50 |
((Scan.option parse_sort_list -- Scan.option parse_sort_list) >> (fn (super, sub) => |
59210
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
51 |
(Toplevel.unknown_theory o |
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
52 |
Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub)))); |
58201 | 53 |
|
54 |
end; |