# HG changeset patch # User wenzelm # Date 1442940985 -7200 # Node ID c165f0472d57de8bab713c2577bf7cfceabcd632 # Parent 2da25a27a616fd92d0ae2bacf9626d74f430ab8a separate command 'print_definitions'; diff -r 2da25a27a616 -r c165f0472d57 NEWS --- 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. diff -r 2da25a27a616 -r c165f0472d57 src/Doc/Isar_Ref/Outer_Syntax.thy --- 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 \ \begin{matharray}{rcl} @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_definitions"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @@ -475,6 +476,7 @@ @{rail \ (@@{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. diff -r 2da25a27a616 -r c165f0472d57 src/Pure/Isar/isar_syn.ML --- 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))); diff -r 2da25a27a616 -r c165f0472d57 src/Pure/Isar/proof_display.ML --- 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 *) diff -r 2da25a27a616 -r c165f0472d57 src/Pure/Pure.thy --- 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" diff -r 2da25a27a616 -r c165f0472d57 src/Pure/display.ML --- 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;