src/Pure/Tools/class_deps.ML
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 62848 e4140efe699e
permissions -rw-r--r--
tuned signature;
     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
     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
    11 end;
    12 
    13 structure Class_Deps: CLASS_DEPS =
    14 struct
    15 
    16 fun 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 
    37 val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of);
    38 val class_deps_cmd = Graph_Display.display_graph oo gen_class_deps Syntax.read_sort;
    39 
    40 end;