src/Pure/Tools/class_deps.ML
author wenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058 a78612c67ec0
parent 58893 9e0ecb66d6a7
child 59206 36808125e00f
permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
     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 visualize: Proof.context -> sort -> sort option -> unit
    10   val visualize_cmd: Proof.context -> string -> string option -> unit
    11 end;
    12 
    13 structure Class_deps: CLASS_DEPS =
    14 struct
    15 
    16 fun gen_visualize prep_sort ctxt raw_super raw_sub =
    17   let
    18     val super = prep_sort ctxt raw_super;
    19     val sub = Option.map (prep_sort ctxt) raw_sub;
    20     val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
    21     fun le_super class = Sorts.sort_le original_algebra ([class], super);
    22     val sub_le = case sub of
    23       NONE => K true |
    24       SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]);
    25     val (_, algebra) = Sorts.subalgebra (Context.pretty ctxt)
    26       (le_super andf sub_le) (K NONE) original_algebra;
    27     val classes = Sorts.classes_of algebra;
    28     fun entry (c, (i, (_, cs))) =
    29       (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
    30             dir = "", unfold = true, path = "", content = []});
    31     val gr =
    32       Graph.fold (cons o entry) classes []
    33       |> sort (int_ord o apply2 #1) |> map #2;
    34   in Graph_Display.display_graph gr end;
    35 
    36 val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
    37 val visualize_cmd = gen_visualize Syntax.read_sort;
    38 
    39 val _ =
    40   Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
    41     ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
    42       ((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
    43 
    44 end;