5 *) |
5 *) |
6 |
6 |
7 signature CLASS_DEPS = |
7 signature CLASS_DEPS = |
8 sig |
8 sig |
9 val inlined_class_specs: bool Config.T |
9 val inlined_class_specs: bool Config.T |
10 val class_deps: Proof.context -> sort -> sort option -> unit |
10 val class_deps: Proof.context -> sort list option -> sort list option -> unit |
11 val class_deps_cmd: Proof.context -> string -> string option -> unit |
11 val class_deps_cmd: Proof.context -> string list option -> string list option -> unit |
12 end; |
12 end; |
13 |
13 |
14 structure Class_Deps: CLASS_DEPS = |
14 structure Class_Deps: CLASS_DEPS = |
15 struct |
15 struct |
16 |
16 |
17 val inlined_class_specs = Attrib.setup_config_bool @{binding "inlined_class_specs"} (K false); |
17 val inlined_class_specs = Attrib.setup_config_bool @{binding "inlined_class_specs"} (K false); |
18 |
18 |
19 val stringify = XML.content_of o YXML.parse_body o Pretty.string_of; |
19 val stringify = XML.content_of o YXML.parse_body o Pretty.string_of; |
20 |
20 |
21 fun gen_class_deps prep_sort ctxt raw_super raw_sub = |
21 fun gen_class_deps prep_sort ctxt raw_subs raw_supers = |
22 let |
22 let |
23 val thy = Proof_Context.theory_of ctxt; |
23 val thy = Proof_Context.theory_of ctxt; |
24 val super = prep_sort ctxt raw_super; |
24 val some_subs = (Option.map o map) (prep_sort ctxt) raw_subs; |
25 val sub = Option.map (prep_sort ctxt) raw_sub; |
25 val some_supers = (Option.map o map) (prep_sort ctxt) raw_supers; |
26 val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); |
26 val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); |
27 fun le_super class = Sorts.sort_le original_algebra ([class], super); |
27 val sort_le = curry (Sorts.sort_le original_algebra); |
28 val sub_le = |
28 val le_sub = case some_subs of |
29 (case sub of |
29 SOME subs => (fn class => exists (sort_le [class]) subs) |
30 NONE => K true |
30 | NONE => K true; |
31 | SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class])); |
31 val super_le = case some_supers of |
|
32 SOME supers => (fn class => exists (fn super => sort_le super [class]) supers) |
|
33 | NONE => K true |
32 val (_, algebra) = |
34 val (_, algebra) = |
33 Sorts.subalgebra (Context.pretty ctxt) |
35 Sorts.subalgebra (Context.pretty ctxt) |
34 (le_super andf sub_le) (K NONE) original_algebra; |
36 (le_sub andf super_le) (K NONE) original_algebra; |
35 val inlined = Config.get ctxt inlined_class_specs; |
37 val inlined = Config.get ctxt inlined_class_specs; |
36 fun label_for c = |
38 fun label_for c = |
37 if inlined |
39 if inlined |
38 then (stringify o Pretty.block o op @) (Class.pretty_specification thy c) |
40 then (stringify o Pretty.block o op @) (Class.pretty_specification thy c) |
39 else Name_Space.extern ctxt space c; |
41 else Name_Space.extern ctxt space c; |
57 end; |
59 end; |
58 |
60 |
59 val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of); |
61 val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of); |
60 val class_deps_cmd = gen_class_deps Syntax.read_sort; |
62 val class_deps_cmd = gen_class_deps Syntax.read_sort; |
61 |
63 |
|
64 val parse_sort_list = (Parse.sort >> single) |
|
65 || (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"}); |
|
66 |
62 val _ = |
67 val _ = |
63 Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies" |
68 Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies" |
64 ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (super, sub) => |
69 ((Scan.option parse_sort_list -- Scan.option parse_sort_list) >> (fn (super, sub) => |
65 (Toplevel.unknown_theory o |
70 (Toplevel.unknown_theory o |
66 Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub)))); |
71 Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub)))); |
67 |
72 |
68 end; |
73 end; |