clarified thy_deps;
authorwenzelm
Thu Apr 16 13:48:10 2015 +0200 (2015-04-16 ago)
changeset 60095c48d536231fe
parent 60094 20d437414174
child 60096 96a4765ba7d1
clarified thy_deps;
NEWS
src/Doc/Isar_Ref/Spec.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/Tools/thy_deps.ML
     1.1 --- a/NEWS	Thu Apr 16 13:39:21 2015 +0200
     1.2 +++ b/NEWS	Thu Apr 16 13:48:10 2015 +0200
     1.3 @@ -77,6 +77,9 @@
     1.4  * Improved graphview panel with optional output of PNG or PDF, for
     1.5  display of 'thy_deps', 'locale_deps', 'class_deps' etc.
     1.6  
     1.7 +* Command 'thy_deps' allows optional bounds, analogously to
     1.8 +'class_deps'.
     1.9 +
    1.10  * Improved scheduling for asynchronous print commands (e.g. provers
    1.11  managed by the Sledgehammer panel) wrt. ongoing document processing.
    1.12  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 16 13:39:21 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 16 13:48:10 2015 +0200
     2.3 @@ -25,6 +25,7 @@
     2.4    \begin{matharray}{rcl}
     2.5      @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
     2.6      @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
     2.7 +    @{command_def "thy_deps"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow>"} \\
     2.8    \end{matharray}
     2.9  
    2.10    Isabelle/Isar theories are defined via theory files, which consist of an
    2.11 @@ -64,6 +65,10 @@
    2.12      ;
    2.13      keyword_decls: (@{syntax string} +)
    2.14        ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
    2.15 +    ;
    2.16 +    @@{command thy_deps} (thy_bounds thy_bounds?)?
    2.17 +    ;
    2.18 +    thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')'
    2.19    \<close>}
    2.20  
    2.21    \begin{description}
    2.22 @@ -104,6 +109,12 @@
    2.23    @{keyword "begin"} that needs to be matched by @{command (local)
    2.24    "end"}, according to the usual rules for nested blocks.
    2.25  
    2.26 +  \item @{command thy_deps} visualizes the theory hierarchy as a directed
    2.27 +  acyclic graph. By default, all imported theories are shown, taking the
    2.28 +  base session as a starting point. Alternatively, it is possibly to
    2.29 +  restrict the full theory graph by giving bounds, analogously to
    2.30 +  @{command_ref class_deps}.
    2.31 +
    2.32    \end{description}
    2.33  \<close>
    2.34  
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 13:39:21 2015 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 13:48:10 2015 +0200
     3.3 @@ -35,7 +35,6 @@
     3.4    val diag_state: Proof.context -> Toplevel.state
     3.5    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
     3.6    val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
     3.7 -  val thy_deps: Toplevel.transition -> Toplevel.transition
     3.8    val locale_deps: Toplevel.transition -> Toplevel.transition
     3.9    val print_stmts: string list * (Facts.ref * Token.src list) list
    3.10      -> Toplevel.transition -> Toplevel.transition
    3.11 @@ -270,15 +269,6 @@
    3.12  
    3.13  (* display dependencies *)
    3.14  
    3.15 -val thy_deps =
    3.16 -  Toplevel.unknown_theory o
    3.17 -  Toplevel.keep (fn st =>
    3.18 -    let
    3.19 -      val thy = Toplevel.theory_of st;
    3.20 -      val parent_session = Session.get_name ();
    3.21 -      val parent_loaded = is_some o Thy_Info.lookup_theory;
    3.22 -    in Graph_Display.display_graph (Present.session_graph parent_session parent_loaded thy) end);
    3.23 -
    3.24  val locale_deps =
    3.25    Toplevel.unknown_theory o
    3.26    Toplevel.keep (Toplevel.theory_of #> (fn thy =>
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 16 13:39:21 2015 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 16 13:48:10 2015 +0200
     4.3 @@ -800,10 +800,6 @@
     4.4        Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
     4.8 -    (Scan.succeed Isar_Cmd.thy_deps);
     4.9 -
    4.10 -val _ =
    4.11    Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
    4.12      (Scan.succeed Isar_Cmd.locale_deps);
    4.13  
     5.1 --- a/src/Pure/Pure.thy	Thu Apr 16 13:39:21 2015 +0200
     5.2 +++ b/src/Pure/Pure.thy	Thu Apr 16 13:48:10 2015 +0200
     5.3 @@ -98,6 +98,7 @@
     5.4  ML_file "Tools/rail.ML"
     5.5  ML_file "Tools/rule_insts.ML"
     5.6  ML_file "Tools/thm_deps.ML"
     5.7 +ML_file "Tools/thy_deps.ML"
     5.8  ML_file "Tools/class_deps.ML"
     5.9  ML_file "Tools/find_theorems.ML"
    5.10  ML_file "Tools/find_consts.ML"
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Tools/thy_deps.ML	Thu Apr 16 13:48:10 2015 +0200
     6.3 @@ -0,0 +1,50 @@
     6.4 +(*  Title:      Pure/Tools/thy_deps.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Visualization of theory dependencies.
     6.8 +*)
     6.9 +
    6.10 +signature THY_DEPS =
    6.11 +sig
    6.12 +  val thy_deps: theory -> theory list option * theory list option -> Graph_Display.entry list
    6.13 +  val thy_deps_cmd: theory -> string list option * string list option -> unit
    6.14 +end;
    6.15 +
    6.16 +structure Thy_Deps: THY_DEPS =
    6.17 +struct
    6.18 +
    6.19 +fun gen_thy_deps _ thy0 (NONE, NONE) =
    6.20 +      let
    6.21 +        val parent_session = Session.get_name ();
    6.22 +        val parent_loaded = is_some o Thy_Info.lookup_theory;
    6.23 +      in Present.session_graph parent_session parent_loaded thy0 end
    6.24 +  | gen_thy_deps prep_thy thy0 bounds =
    6.25 +      let
    6.26 +        val (upper, lower) = apply2 ((Option.map o map) (prep_thy thy0)) bounds;
    6.27 +        val rel = Theory.subthy o swap;
    6.28 +        val pred =
    6.29 +          (case upper of
    6.30 +            SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
    6.31 +          | NONE => K true) andf
    6.32 +          (case lower of
    6.33 +            SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
    6.34 +          | NONE => K true);
    6.35 +        fun node thy =
    6.36 +          ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
    6.37 +            map Context.theory_name (filter pred (Theory.parents_of thy)));
    6.38 +      in Theory.nodes_of thy0 |> filter pred |> map node end;
    6.39 +
    6.40 +val thy_deps = gen_thy_deps (K I);
    6.41 +val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Context.get_theory;
    6.42 +
    6.43 +val theory_bounds =
    6.44 +  Parse.theory_xname >> single ||
    6.45 +  (@{keyword "("} |-- Parse.enum "|" Parse.theory_xname --| @{keyword ")"});
    6.46 +
    6.47 +val _ =
    6.48 +  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
    6.49 +    (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args =>
    6.50 +      (Toplevel.unknown_theory o
    6.51 +       Toplevel.keep (fn st => thy_deps_cmd (Toplevel.theory_of st) args))));
    6.52 +
    6.53 +end;