author | wenzelm |
Thu, 06 Aug 2015 17:40:05 +0200 | |
changeset 60856 | eb21ae05ec43 |
parent 60097 | d20ca79d50e4 |
child 61262 | 7bd1eb4b056e |
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 |
|
60092 | 9 |
val class_deps: Proof.context -> sort list option * sort list option -> Graph_Display.entry list |
60090 | 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 |
||
60092 | 16 |
fun gen_class_deps prep_sort ctxt bounds = |
58201 | 17 |
let |
60092 | 18 |
val (upper, lower) = apply2 ((Option.map o map) (prep_sort ctxt)) bounds; |
60090 | 19 |
val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); |
60092 | 20 |
val rel = Sorts.sort_le algebra; |
21 |
val pred = |
|
60090 | 22 |
(case upper of |
60092 | 23 |
SOME bs => (fn c => exists (fn b => rel ([c], b)) bs) |
60090 | 24 |
| NONE => K true) andf |
25 |
(case lower of |
|
60092 | 26 |
SOME bs => (fn c => exists (fn b => rel (b, [c])) bs) |
60090 | 27 |
| NONE => K true); |
59423
3a0044e95eba
backed out obsolete workaround from ef1edfb36af7
haftmann
parents:
59422
diff
changeset
|
28 |
fun node c = |
3a0044e95eba
backed out obsolete workaround from ef1edfb36af7
haftmann
parents:
59422
diff
changeset
|
29 |
Graph_Display.content_node (Name_Space.extern ctxt space c) |
60090 | 30 |
(Class.pretty_specification (Proof_Context.theory_of ctxt) c); |
59210
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
31 |
in |
60092 | 32 |
Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra |
60090 | 33 |
|> #2 |> Sorts.classes_of |> Graph.dest |
59383
1434ef1e0ede
clarified Class.pretty_specification: imitate input source;
wenzelm
parents:
59301
diff
changeset
|
34 |
|> 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
|
35 |
end; |
58202 | 36 |
|
59301 | 37 |
val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of); |
60091 | 38 |
val class_deps_cmd = Graph_Display.display_graph oo gen_class_deps Syntax.read_sort; |
58201 | 39 |
|
60091 | 40 |
val class_bounds = |
60090 | 41 |
Parse.sort >> single || |
42 |
(@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"}); |
|
59422 | 43 |
|
58201 | 44 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59423
diff
changeset
|
45 |
Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies" |
60091 | 46 |
(Scan.option class_bounds -- Scan.option class_bounds >> (fn args => |
60097
d20ca79d50e4
discontinued pointless warnings: commands are only defined inside a theory context;
wenzelm
parents:
60092
diff
changeset
|
47 |
Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args))); |
58201 | 48 |
|
49 |
end; |