src/Pure/Isar/proof_display.ML
author wenzelm
Mon Nov 19 20:23:47 2012 +0100 (2012-11-19 ago)
changeset 50126 3dec88149176
parent 49867 d3053a55bfcb
child 51584 98029ceda8ce
permissions -rw-r--r--
theorem status about oracles/futures is no longer printed by default;
renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
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@49860
    20
  val pretty_goal_header: thm -> Pretty.T
wenzelm@49860
    21
  val string_of_goal: Proof.context -> thm -> string
wenzelm@49866
    22
  val method_error: string -> Position.T ->
wenzelm@49866
    23
    {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
wenzelm@46728
    24
  val print_results: Markup.T -> bool -> Proof.context ->
wenzelm@46728
    25
    ((string * string) * (string * thm list) list) -> unit
wenzelm@44192
    26
  val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
wenzelm@17369
    27
end
wenzelm@17369
    28
wenzelm@33389
    29
structure Proof_Display: PROOF_DISPLAY =
wenzelm@17369
    30
struct
wenzelm@17369
    31
wenzelm@20235
    32
(* toplevel pretty printing *)
wenzelm@20211
    33
wenzelm@30628
    34
fun pp_context ctxt =
wenzelm@42717
    35
 (if Config.get ctxt Proof_Context.debug then
wenzelm@42360
    36
    Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
wenzelm@20211
    37
  else Pretty.str "<context>");
wenzelm@20211
    38
wenzelm@45269
    39
fun default_context thy0 =
wenzelm@45269
    40
  (case Context.thread_data () of
wenzelm@45269
    41
    SOME (Context.Proof ctxt) => ctxt
wenzelm@45269
    42
  | SOME (Context.Theory thy) =>
wenzelm@45269
    43
      (case try Syntax.init_pretty_global thy of
wenzelm@45269
    44
        SOME ctxt => ctxt
wenzelm@45269
    45
      | NONE => Syntax.init_pretty_global thy0)
wenzelm@45269
    46
  | NONE => Syntax.init_pretty_global thy0);
wenzelm@44240
    47
wenzelm@30628
    48
fun pp_thm th =
wenzelm@50126
    49
  let val ctxt = default_context (Thm.theory_of_thm th);
wenzelm@50126
    50
  in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
wenzelm@20211
    51
wenzelm@44240
    52
fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
wenzelm@44240
    53
fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
wenzelm@30628
    54
wenzelm@30628
    55
fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
wenzelm@30628
    56
fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
wenzelm@20211
    57
wenzelm@19432
    58
wenzelm@19432
    59
(* theorems and theory *)
wenzelm@19432
    60
wenzelm@33515
    61
fun pretty_theorems_diff verbose prev_thys thy =
wenzelm@19432
    62
  let
wenzelm@42360
    63
    val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
wenzelm@39557
    64
    val facts = Global_Theory.facts_of thy;
wenzelm@33515
    65
    val thmss =
wenzelm@39557
    66
      Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
wenzelm@33515
    67
      |> not verbose ? filter_out (Facts.is_concealed facts o #1);
wenzelm@28210
    68
  in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
wenzelm@19432
    69
wenzelm@33515
    70
fun print_theorems_diff verbose prev_thy thy =
wenzelm@33515
    71
  Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
wenzelm@19432
    72
wenzelm@33515
    73
fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
wenzelm@33515
    74
val print_theorems = Pretty.writeln oo pretty_theorems;
wenzelm@19432
    75
wenzelm@22872
    76
fun pretty_full_theory verbose thy =
wenzelm@33515
    77
  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
wenzelm@20621
    78
wenzelm@22872
    79
val print_theory = Pretty.writeln o pretty_full_theory false;
aspinall@22335
    80
wenzelm@19432
    81
wenzelm@17369
    82
(* refinement rule *)
wenzelm@17369
    83
wenzelm@17369
    84
fun pretty_rule ctxt s thm =
wenzelm@17369
    85
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
wenzelm@50126
    86
    Pretty.fbrk, Display.pretty_thm ctxt thm];
wenzelm@17369
    87
wenzelm@17369
    88
val string_of_rule = Pretty.string_of ooo pretty_rule;
wenzelm@17369
    89
wenzelm@17369
    90
wenzelm@49860
    91
(* goals *)
wenzelm@49860
    92
wenzelm@49860
    93
local
wenzelm@49860
    94
wenzelm@49860
    95
fun subgoals 0 = []
wenzelm@49860
    96
  | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
wenzelm@49860
    97
  | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
wenzelm@49860
    98
wenzelm@49860
    99
in
wenzelm@49860
   100
wenzelm@49860
   101
fun pretty_goal_header goal =
wenzelm@49860
   102
  Pretty.block ([Pretty.command "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
wenzelm@49860
   103
wenzelm@49860
   104
end;
wenzelm@49860
   105
wenzelm@49860
   106
fun string_of_goal ctxt goal =
wenzelm@49860
   107
  Pretty.string_of (Pretty.chunks
wenzelm@49860
   108
    [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
wenzelm@49860
   109
wenzelm@49860
   110
wenzelm@49860
   111
(* method_error *)
wenzelm@49860
   112
wenzelm@49866
   113
fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
wenzelm@49860
   114
  let
wenzelm@49866
   115
    val pr_header =
wenzelm@49866
   116
      "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
wenzelm@49866
   117
      "proof method" ^ Position.here pos ^ ":\n";
wenzelm@49860
   118
    val pr_facts =
wenzelm@49860
   119
      if null facts then ""
wenzelm@49860
   120
      else
wenzelm@49867
   121
        (Pretty.string_of o Pretty.block o Pretty.fbreaks)
wenzelm@49867
   122
          (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
wenzelm@49867
   123
            map (Display.pretty_thm ctxt) facts) ^ "\n";
wenzelm@49860
   124
    val pr_goal = string_of_goal ctxt goal;
wenzelm@49860
   125
  in pr_header ^ pr_facts ^ pr_goal end);
wenzelm@49860
   126
wenzelm@49860
   127
wenzelm@17369
   128
(* results *)
wenzelm@17369
   129
wenzelm@28092
   130
local
wenzelm@28092
   131
wenzelm@41551
   132
fun pretty_fact_name (kind, "") = Pretty.command kind
wenzelm@41551
   133
  | pretty_fact_name (kind, name) =
wenzelm@41551
   134
      Pretty.block [Pretty.command kind, Pretty.brk 1,
wenzelm@41551
   135
        Pretty.str (Long_Name.base_name name), Pretty.str ":"];
wenzelm@28087
   136
wenzelm@17369
   137
fun pretty_facts ctxt =
wenzelm@41551
   138
  flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
wenzelm@50126
   139
    map (single o Proof_Context.pretty_fact ctxt);
wenzelm@17369
   140
wenzelm@27857
   141
in
wenzelm@27857
   142
wenzelm@46728
   143
fun print_results markup do_print ctxt ((kind, name), facts) =
wenzelm@33643
   144
  if not do_print orelse kind = "" then ()
wenzelm@28092
   145
  else if name = "" then
wenzelm@46728
   146
    (Pretty.writeln o Pretty.mark markup)
wenzelm@46728
   147
      (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
wenzelm@46728
   148
  else
wenzelm@46728
   149
    (Pretty.writeln o Pretty.mark markup)
wenzelm@46728
   150
      (case facts of
wenzelm@46728
   151
        [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
wenzelm@50126
   152
          Proof_Context.pretty_fact ctxt fact])
wenzelm@46728
   153
      | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
wenzelm@46728
   154
          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
wenzelm@17369
   155
wenzelm@17369
   156
end;
wenzelm@17369
   157
wenzelm@20889
   158
wenzelm@20889
   159
(* consts *)
wenzelm@20889
   160
wenzelm@20889
   161
local
wenzelm@20889
   162
wenzelm@20889
   163
fun pretty_var ctxt (x, T) =
wenzelm@20889
   164
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
wenzelm@24920
   165
    Pretty.quote (Syntax.pretty_typ ctxt T)];
wenzelm@20889
   166
wenzelm@20889
   167
fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
wenzelm@20889
   168
wenzelm@20889
   169
fun pretty_consts ctxt pred cs =
wenzelm@42360
   170
  (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
wenzelm@20889
   171
    [] => pretty_vars ctxt "constants" cs
wenzelm@20889
   172
  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
wenzelm@20889
   173
wenzelm@44192
   174
in
wenzelm@44192
   175
wenzelm@44192
   176
fun print_consts do_print ctxt pred cs =
wenzelm@44192
   177
  if not do_print orelse null cs then ()
wenzelm@44192
   178
  else Pretty.writeln (pretty_consts ctxt pred cs);
wenzelm@44192
   179
wenzelm@20889
   180
end;
wenzelm@20889
   181
wenzelm@17369
   182
end;