src/Pure/Isar/proof_display.ML
author wenzelm
Wed Aug 17 16:46:58 2011 +0200 (2011-08-17)
changeset 44240 4b1a63678839
parent 44192 a32ca9165928
child 45269 6f8949e6c71a
permissions -rw-r--r--
improved default context for ML toplevel pretty-printing;
wenzelm@17369
     1
(*  Title:      Pure/Isar/proof_display.ML
wenzelm@17369
     2
    Author:     Makarius
wenzelm@17369
     3
wenzelm@19432
     4
Printing of theorems, goals, results etc.
wenzelm@17369
     5
*)
wenzelm@17369
     6
wenzelm@17369
     7
signature PROOF_DISPLAY =
wenzelm@17369
     8
sig
wenzelm@30628
     9
  val pp_context: Proof.context -> Pretty.T
wenzelm@30628
    10
  val pp_thm: thm -> Pretty.T
wenzelm@30628
    11
  val pp_typ: theory -> typ -> Pretty.T
wenzelm@30628
    12
  val pp_term: theory -> term -> Pretty.T
wenzelm@30628
    13
  val pp_ctyp: ctyp -> Pretty.T
wenzelm@30628
    14
  val pp_cterm: cterm -> Pretty.T
wenzelm@33515
    15
  val print_theorems_diff: bool -> theory -> theory -> unit
wenzelm@33515
    16
  val print_theorems: bool -> theory -> unit
aspinall@22335
    17
  val pretty_full_theory: bool -> theory -> Pretty.T
wenzelm@28092
    18
  val print_theory: theory -> unit
wenzelm@20311
    19
  val string_of_rule: Proof.context -> string -> thm -> string
wenzelm@27857
    20
  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
wenzelm@44192
    21
  val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
wenzelm@17369
    22
end
wenzelm@17369
    23
wenzelm@33389
    24
structure Proof_Display: PROOF_DISPLAY =
wenzelm@17369
    25
struct
wenzelm@17369
    26
wenzelm@20235
    27
(* toplevel pretty printing *)
wenzelm@20211
    28
wenzelm@30628
    29
fun pp_context ctxt =
wenzelm@42717
    30
 (if Config.get ctxt Proof_Context.debug then
wenzelm@42360
    31
    Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
wenzelm@20211
    32
  else Pretty.str "<context>");
wenzelm@20211
    33
wenzelm@44240
    34
fun default_context thy =
wenzelm@44240
    35
  Context.cases Syntax.init_pretty_global I
wenzelm@44240
    36
    (the_default (Context.Theory thy) (try ML_Context.the_generic_context ()));
wenzelm@44240
    37
wenzelm@30628
    38
fun pp_thm th =
wenzelm@30724
    39
  let
wenzelm@44240
    40
    val ctxt = default_context (Thm.theory_of_thm th);
wenzelm@30724
    41
    val flags = {quote = true, show_hyps = false, show_status = true};
wenzelm@44240
    42
  in Display.pretty_thm_raw ctxt flags th end;
wenzelm@20211
    43
wenzelm@44240
    44
fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
wenzelm@44240
    45
fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
wenzelm@30628
    46
wenzelm@30628
    47
fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
wenzelm@30628
    48
fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
wenzelm@20211
    49
wenzelm@19432
    50
wenzelm@19432
    51
(* theorems and theory *)
wenzelm@19432
    52
wenzelm@33515
    53
fun pretty_theorems_diff verbose prev_thys thy =
wenzelm@19432
    54
  let
wenzelm@42360
    55
    val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
wenzelm@39557
    56
    val facts = Global_Theory.facts_of thy;
wenzelm@33515
    57
    val thmss =
wenzelm@39557
    58
      Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
wenzelm@33515
    59
      |> not verbose ? filter_out (Facts.is_concealed facts o #1);
wenzelm@28210
    60
  in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
wenzelm@19432
    61
wenzelm@33515
    62
fun print_theorems_diff verbose prev_thy thy =
wenzelm@33515
    63
  Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
wenzelm@19432
    64
wenzelm@33515
    65
fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
wenzelm@33515
    66
val print_theorems = Pretty.writeln oo pretty_theorems;
wenzelm@19432
    67
wenzelm@22872
    68
fun pretty_full_theory verbose thy =
wenzelm@33515
    69
  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
wenzelm@20621
    70
wenzelm@22872
    71
val print_theory = Pretty.writeln o pretty_full_theory false;
aspinall@22335
    72
wenzelm@19432
    73
wenzelm@17369
    74
(* refinement rule *)
wenzelm@17369
    75
wenzelm@17369
    76
fun pretty_rule ctxt s thm =
wenzelm@17369
    77
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
wenzelm@32091
    78
    Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
wenzelm@17369
    79
wenzelm@17369
    80
val string_of_rule = Pretty.string_of ooo pretty_rule;
wenzelm@17369
    81
wenzelm@17369
    82
wenzelm@17369
    83
(* results *)
wenzelm@17369
    84
wenzelm@28092
    85
local
wenzelm@28092
    86
wenzelm@41551
    87
fun pretty_fact_name (kind, "") = Pretty.command kind
wenzelm@41551
    88
  | pretty_fact_name (kind, name) =
wenzelm@41551
    89
      Pretty.block [Pretty.command kind, Pretty.brk 1,
wenzelm@41551
    90
        Pretty.str (Long_Name.base_name name), Pretty.str ":"];
wenzelm@28087
    91
wenzelm@17369
    92
fun pretty_facts ctxt =
wenzelm@41551
    93
  flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
wenzelm@42360
    94
    map (single o Proof_Context.pretty_fact_aux ctxt false);
wenzelm@17369
    95
wenzelm@27857
    96
in
wenzelm@27857
    97
wenzelm@28092
    98
fun print_results do_print ctxt ((kind, name), facts) =
wenzelm@33643
    99
  if not do_print orelse kind = "" then ()
wenzelm@28092
   100
  else if name = "" then
wenzelm@39284
   101
    Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
wenzelm@28092
   102
  else Pretty.writeln
wenzelm@28092
   103
    (case facts of
wenzelm@28092
   104
      [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
wenzelm@42360
   105
        Proof_Context.pretty_fact_aux ctxt false fact])
wenzelm@28092
   106
    | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
wenzelm@28092
   107
        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
wenzelm@17369
   108
wenzelm@17369
   109
end;
wenzelm@17369
   110
wenzelm@20889
   111
wenzelm@20889
   112
(* consts *)
wenzelm@20889
   113
wenzelm@20889
   114
local
wenzelm@20889
   115
wenzelm@20889
   116
fun pretty_var ctxt (x, T) =
wenzelm@20889
   117
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
wenzelm@24920
   118
    Pretty.quote (Syntax.pretty_typ ctxt T)];
wenzelm@20889
   119
wenzelm@20889
   120
fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
wenzelm@20889
   121
wenzelm@20889
   122
fun pretty_consts ctxt pred cs =
wenzelm@42360
   123
  (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
wenzelm@20889
   124
    [] => pretty_vars ctxt "constants" cs
wenzelm@20889
   125
  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
wenzelm@20889
   126
wenzelm@44192
   127
in
wenzelm@44192
   128
wenzelm@44192
   129
fun print_consts do_print ctxt pred cs =
wenzelm@44192
   130
  if not do_print orelse null cs then ()
wenzelm@44192
   131
  else Pretty.writeln (pretty_consts ctxt pred cs);
wenzelm@44192
   132
wenzelm@20889
   133
end;
wenzelm@20889
   134
wenzelm@17369
   135
end;