1(* Title: Pure/Tools/class_deps.ML 2 Author: Florian Haftmann, TU Muenchen 3 4Visualization of class dependencies. 5*) 6 7signature CLASS_DEPS = 8sig 9 val class_deps: Proof.context -> sort list option * sort list option -> Graph_Display.entry list 10 val class_deps_cmd: Proof.context -> string list option * string list option -> unit 11end; 12 13structure Class_Deps: CLASS_DEPS = 14struct 15 16fun gen_class_deps prep_sort ctxt bounds = 17 let 18 val (upper, lower) = apply2 ((Option.map o map) (prep_sort ctxt)) bounds; 19 val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); 20 val rel = Sorts.sort_le algebra; 21 val pred = 22 (case upper of 23 SOME bs => (fn c => exists (fn b => rel ([c], b)) bs) 24 | NONE => K true) andf 25 (case lower of 26 SOME bs => (fn c => exists (fn b => rel (b, [c])) bs) 27 | NONE => K true); 28 fun node c = 29 Graph_Display.content_node (Name_Space.extern ctxt space c) 30 (Class.pretty_specification (Proof_Context.theory_of ctxt) c); 31 in 32 Sorts.subalgebra (Context.Proof ctxt) pred (K NONE) algebra 33 |> #2 |> Sorts.classes_of |> Graph.dest 34 |> map (fn ((c, _), ds) => ((c, node c), ds)) 35 end; 36 37val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of); 38val class_deps_cmd = Graph_Display.display_graph oo gen_class_deps Syntax.read_sort; 39 40end; 41