src/Pure/Tools/class_deps.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 62848 e4140efe699e
permissions -rw-r--r--
more robust sorted_entries;
haftmann@58201
     1
(*  Title:      Pure/Tools/class_deps.ML
haftmann@58201
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@58201
     3
haftmann@58201
     4
Visualization of class dependencies.
haftmann@58201
     5
*)
haftmann@58201
     6
haftmann@58201
     7
signature CLASS_DEPS =
haftmann@58201
     8
sig
wenzelm@60092
     9
  val class_deps: Proof.context -> sort list option * sort list option -> Graph_Display.entry list
wenzelm@60090
    10
  val class_deps_cmd: Proof.context -> string list option * string list option -> unit
haftmann@58201
    11
end;
haftmann@58201
    12
wenzelm@59210
    13
structure Class_Deps: CLASS_DEPS =
haftmann@58201
    14
struct
haftmann@58201
    15
wenzelm@60092
    16
fun gen_class_deps prep_sort ctxt bounds =
haftmann@58201
    17
  let
wenzelm@60092
    18
    val (upper, lower) = apply2 ((Option.map o map) (prep_sort ctxt)) bounds;
wenzelm@60090
    19
    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
wenzelm@60092
    20
    val rel = Sorts.sort_le algebra;
wenzelm@60092
    21
    val pred =
wenzelm@60090
    22
      (case upper of
wenzelm@60092
    23
        SOME bs => (fn c => exists (fn b => rel ([c], b)) bs)
wenzelm@60090
    24
      | NONE => K true) andf
wenzelm@60090
    25
      (case lower of
wenzelm@60092
    26
        SOME bs => (fn c => exists (fn b => rel (b, [c])) bs)
wenzelm@60090
    27
      | NONE => K true);
haftmann@59423
    28
    fun node c =
haftmann@59423
    29
      Graph_Display.content_node (Name_Space.extern ctxt space c)
wenzelm@60090
    30
        (Class.pretty_specification (Proof_Context.theory_of ctxt) c);
wenzelm@59210
    31
  in
wenzelm@61262
    32
    Sorts.subalgebra (Context.Proof ctxt) pred (K NONE) algebra
wenzelm@60090
    33
    |> #2 |> Sorts.classes_of |> Graph.dest
wenzelm@59383
    34
    |> map (fn ((c, _), ds) => ((c, node c), ds))
wenzelm@59210
    35
  end;
haftmann@58202
    36
wenzelm@59301
    37
val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of);
wenzelm@60091
    38
val class_deps_cmd = Graph_Display.display_graph oo gen_class_deps Syntax.read_sort;
haftmann@58201
    39
haftmann@58201
    40
end;