src/Pure/Tools/class_deps.ML
author wenzelm
Mon, 03 Nov 2014 14:50:27 +0100
changeset 58893 9e0ecb66d6a7
parent 58202 be1d10595b7b
child 59058 a78612c67ec0
permissions -rw-r--r--
eliminated unused int_only flag (see also c12484a27367); just proper commands;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58201
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/Tools/class_deps.ML
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
     3
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
     4
Visualization of class dependencies.
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
     5
*)
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
     6
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
     7
signature CLASS_DEPS =
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
     8
sig
58202
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
     9
  val visualize: Proof.context -> sort -> sort option -> unit
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    10
  val visualize_cmd: Proof.context -> string -> string option -> unit
58201
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    11
end;
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    12
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    13
structure Class_deps: CLASS_DEPS =
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    14
struct
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    15
58202
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    16
fun gen_visualize prep_sort ctxt raw_super raw_sub =
58201
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    17
  let
58202
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    18
    val super = prep_sort ctxt raw_super;
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    19
    val sub = Option.map (prep_sort ctxt) raw_sub;
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    20
    val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    21
    fun le_super class = Sorts.sort_le original_algebra ([class], super);
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    22
    val sub_le = case sub of
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    23
      NONE => K true |
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    24
      SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]);
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    25
    val (_, algebra) = Sorts.subalgebra (Context.pretty ctxt)
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    26
      (le_super andf sub_le) (K NONE) original_algebra;
58201
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    27
    val classes = Sorts.classes_of algebra;
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    28
    fun entry (c, (i, (_, cs))) =
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    29
      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    30
            dir = "", unfold = true, path = "", content = []});
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    31
    val gr =
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    32
      Graph.fold (cons o entry) classes []
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    33
      |> sort (int_ord o pairself #1) |> map #2;
58202
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    34
  in Graph_Display.display_graph gr end;
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    35
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    36
val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    37
val visualize_cmd = gen_visualize Syntax.read_sort;
58201
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    38
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    39
val _ =
58893
9e0ecb66d6a7 eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents: 58202
diff changeset
    40
  Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
58202
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    41
    ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
be1d10595b7b restrictive options for class dependencies
haftmann
parents: 58201
diff changeset
    42
      ((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
58201
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    43
5bf56c758e02 separated class_deps command into separate file
haftmann
parents:
diff changeset
    44
end;