--- a/NEWS Tue Sep 22 18:06:49 2015 +0200
+++ b/NEWS Tue Sep 22 18:56:25 2015 +0200
@@ -177,6 +177,9 @@
*** Pure ***
+* Command 'print_definitions' prints dependencies of definitional
+specifications. This functionality used to be part of 'print_theory'.
+
* The vacuous fact "TERM x" may be established "by fact" or as `TERM x`
as well, not just "by this" or "." as before.
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Tue Sep 22 18:06:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Tue Sep 22 18:56:25 2015 +0200
@@ -462,6 +462,7 @@
text \<open>
\begin{matharray}{rcl}
@{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_definitions"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -475,6 +476,7 @@
@{rail \<open>
(@@{command print_theory} |
+ @@{command print_definitions} |
@@{command print_methods} |
@@{command print_attributes} |
@@{command print_theorems} |
@@ -504,6 +506,12 @@
\item @{command "print_theory"} prints the main logical content of the
background theory; the ``@{text "!"}'' option indicates extra verbosity.
+ \item @{command "print_definitions"} prints dependencies of definitional
+ specifications within the background theory, which may be constants
+ \secref{sec:consts} or types (\secref{sec:types-pure},
+ \secref{sec:hol-typedef}); the ``@{text "!"}'' option indicates extra
+ verbosity.
+
\item @{command "print_methods"} prints all proof methods available in the
current theory context; the ``@{text "!"}'' option indicates extra
verbosity.
--- a/src/Pure/Isar/isar_syn.ML Tue Sep 22 18:06:49 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Sep 22 18:56:25 2015 +0200
@@ -770,6 +770,12 @@
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
val _ =
+ Outer_Syntax.command @{command_keyword print_definitions}
+ "print dependencies of definitional theory content"
+ (Parse.opt_bang >> (fn b =>
+ Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
+
+val _ =
Outer_Syntax.command @{command_keyword print_syntax}
"print inner syntax of context"
(Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
--- a/src/Pure/Isar/proof_display.ML Tue Sep 22 18:06:49 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML Tue Sep 22 18:56:25 2015 +0200
@@ -12,10 +12,10 @@
val pp_term: (unit -> theory) -> term -> Pretty.T
val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
+ val pretty_definitions: bool -> Proof.context -> Pretty.T
val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
val pretty_theorems: bool -> theory -> Pretty.T list
val pretty_full_theory: bool -> theory -> Pretty.T
- val print_theory: theory -> unit
val string_of_rule: Proof.context -> string -> thm -> string
val pretty_goal_header: thm -> Pretty.T
val string_of_goal: Proof.context -> thm -> string
@@ -31,7 +31,7 @@
structure Proof_Display: PROOF_DISPLAY =
struct
-(* toplevel pretty printing *)
+(** toplevel pretty printing **)
fun pp_context ctxt =
(if Config.get ctxt Proof_Context.debug then
@@ -57,6 +57,9 @@
fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
+
+(** theory content **)
+
(* theorems and theory *)
fun pretty_theorems_diff verbose prev_thys thy =
@@ -73,8 +76,54 @@
fun pretty_full_theory verbose thy =
Pretty.chunks (Display.pretty_full_theory verbose thy @ pretty_theorems verbose thy);
-val print_theory = Pretty.writeln o pretty_full_theory false;
+
+(* definitions *)
+
+fun pretty_definitions verbose ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+
+ val prt_item = Defs.pretty_item ctxt;
+ fun sort_item_by f = sort (Defs.item_ord o apply2 f);
+
+ fun pretty_finals reds = Pretty.block
+ (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_item o fst) reds));
+
+ fun pretty_reduct (lhs, rhs) = Pretty.block
+ ([prt_item lhs, Pretty.str " ->", Pretty.brk 2] @
+ Pretty.commas (map prt_item (sort_item_by #1 rhs)));
+
+ fun pretty_restrict (const, name) =
+ Pretty.block ([prt_item const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
+
+ val defs = Theory.defs_of thy;
+ val {restricts, reducts} = Defs.dest defs;
+ val const_space = Proof_Context.const_space ctxt;
+ val type_space = Proof_Context.type_space ctxt;
+ val item_space = fn Defs.Constant => const_space | Defs.Type => type_space;
+
+ fun extern_item (k, c) = (k, Name_Space.extern ctxt (item_space k) c);
+ fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
+
+ val (reds0, (reds1, reds2)) = filter_out (prune_item o fst o fst) reducts
+ |> map (fn (lhs, rhs) =>
+ (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
+ |> sort_item_by (#1 o #1)
+ |> List.partition (null o #2)
+ ||> List.partition (Defs.plain_args o #2 o #1);
+ val rests = restricts |> map (apfst (apfst extern_item)) |> sort_item_by (#1 o #1);
+ in
+ Pretty.big_list "definitions:"
+ [pretty_finals reds0,
+ Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
+ Pretty.big_list "overloaded:" (map pretty_reduct reds2),
+ Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]
+ end;
+
+
+
+(** proof items **)
(* refinement rule *)
--- a/src/Pure/Pure.thy Tue Sep 22 18:06:49 2015 +0200
+++ b/src/Pure/Pure.thy Tue Sep 22 18:56:25 2015 +0200
@@ -74,8 +74,8 @@
and "also" "moreover" :: prf_decl % "proof"
and "finally" "ultimately" :: prf_chain % "proof"
and "back" :: prf_script % "proof"
- and "help" "print_commands" "print_options" "print_context"
- "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
+ and "help" "print_commands" "print_options" "print_context" "print_theory"
+ "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules"
"print_theorems" "print_locales" "print_classes" "print_locale"
"print_interps" "print_dependencies" "print_attributes"
"print_simpset" "print_rules" "print_trans_rules" "print_methods"
--- a/src/Pure/display.ML Tue Sep 22 18:06:49 2015 +0200
+++ b/src/Pure/display.ML Tue Sep 22 18:56:25 2015 +0200
@@ -104,8 +104,6 @@
fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
val prt_term_no_vars = prt_term o Logic.unvarify_global;
fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
- val prt_item = Defs.pretty_item ctxt;
- fun sort_item_by f = sort (Defs.item_ord o apply2 f);
fun pretty_classrel (c, []) = prt_cls c
| pretty_classrel (c, cs) = Pretty.block
@@ -134,18 +132,6 @@
fun pretty_axm (a, t) =
Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
- fun pretty_finals reds = Pretty.block
- (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_item o fst) reds));
-
- fun pretty_reduct (lhs, rhs) = Pretty.block
- ([prt_item lhs, Pretty.str " ->", Pretty.brk 2] @
- Pretty.commas (map prt_item (sort_item_by #1 rhs)));
-
- fun pretty_restrict (const, name) =
- Pretty.block ([prt_item const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
-
- val defs = Theory.defs_of thy;
- val {restricts, reducts} = Defs.dest defs;
val tsig = Sign.tsig_of thy;
val consts = Sign.consts_of thy;
val {const_space, constants, constraints} = Consts.dest consts;
@@ -155,10 +141,6 @@
val classes = Sorts.classes_of class_algebra;
val arities = Sorts.arities_of class_algebra;
- val item_space = fn Defs.Constant => const_space | Defs.Type => type_space;
- fun extern_item (k, c) = (k, Name_Space.extern ctxt (item_space k) c);
- fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
-
val clsses =
Name_Space.extern_entries verbose ctxt class_space
(map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
@@ -174,14 +156,6 @@
val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
-
- val (reds0, (reds1, reds2)) = filter_out (prune_item o fst o fst) reducts
- |> map (fn (lhs, rhs) =>
- (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
- |> sort_item_by (#1 o #1)
- |> List.partition (null o #2)
- ||> List.partition (Defs.plain_args o #2 o #1);
- val rests = restricts |> map (apfst (apfst extern_item)) |> sort_item_by (#1 o #1);
in
[Pretty.strs ("names:" :: Context.display_names thy)] @
[Pretty.big_list "classes:" (map pretty_classrel clsses),
@@ -195,12 +169,7 @@
Pretty.big_list "axioms:" (map pretty_axm axms),
Pretty.block
(Pretty.breaks (Pretty.str "oracles:" ::
- map Pretty.mark_str (Thm.extern_oracles verbose ctxt))),
- Pretty.big_list "definitions:"
- [pretty_finals reds0,
- Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
- Pretty.big_list "overloaded:" (map pretty_reduct reds2),
- Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
+ map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]
end;
end;