src/Pure/Tools/thy_deps.ML
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 65491 7fb81fa1d668
child 68482 cb84beb84ca9
permissions -rw-r--r--
tuned signature;
wenzelm@60093
     1
(*  Title:      Pure/Tools/thy_deps.ML
wenzelm@60093
     2
    Author:     Makarius
wenzelm@60093
     3
wenzelm@60093
     4
Visualization of theory dependencies.
wenzelm@60093
     5
*)
wenzelm@60093
     6
wenzelm@60093
     7
signature THY_DEPS =
wenzelm@60093
     8
sig
wenzelm@65491
     9
  val thy_deps: Proof.context -> theory list option * theory list option ->
wenzelm@65491
    10
    Graph_Display.entry list
wenzelm@60099
    11
  val thy_deps_cmd: Proof.context ->
wenzelm@60099
    12
    (string * Position.T) list option * (string * Position.T) list option -> unit
wenzelm@60093
    13
end;
wenzelm@60093
    14
wenzelm@60093
    15
structure Thy_Deps: THY_DEPS =
wenzelm@60093
    16
struct
wenzelm@60093
    17
wenzelm@65491
    18
fun gen_thy_deps prep_thy ctxt bounds =
wenzelm@65491
    19
  let
wenzelm@65491
    20
    val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
wenzelm@65491
    21
    val rel = Context.subthy o swap;
wenzelm@65491
    22
    val pred =
wenzelm@65491
    23
      (case upper of
wenzelm@65491
    24
        SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
wenzelm@65491
    25
      | NONE => K true) andf
wenzelm@65491
    26
      (case lower of
wenzelm@65491
    27
        SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
wenzelm@65491
    28
      | NONE => K true);
wenzelm@65491
    29
    fun node thy =
wenzelm@65491
    30
      ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
wenzelm@65491
    31
        map Context.theory_name (filter pred (Theory.parents_of thy)));
wenzelm@65491
    32
  in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
wenzelm@60093
    33
wenzelm@60099
    34
val thy_deps =
wenzelm@60099
    35
  gen_thy_deps (fn ctxt => fn thy =>
wenzelm@60099
    36
    let val thy0 = Proof_Context.theory_of ctxt
wenzelm@60948
    37
    in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
wenzelm@60099
    38
wenzelm@60099
    39
val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check;
wenzelm@60093
    40
wenzelm@60093
    41
end;