src/Pure/Isar/proof_display.ML
author wenzelm
Thu Sep 24 23:33:29 2015 +0200 (2015-09-24)
changeset 61261 ddb2da7cb2e4
parent 61258 2be9ea29f9ec
child 61266 eb9522a9d997
permissions -rw-r--r--
more explicit Defs.context: use proper name spaces as far as possible;
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@60937
    10
  val pp_thm: (unit -> theory) -> thm -> Pretty.T
wenzelm@60937
    11
  val pp_typ: (unit -> theory) -> typ -> Pretty.T
wenzelm@60937
    12
  val pp_term: (unit -> theory) -> term -> Pretty.T
wenzelm@60937
    13
  val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
wenzelm@60937
    14
  val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
wenzelm@61252
    15
  val pretty_definitions: bool -> Proof.context -> Pretty.T
wenzelm@57605
    16
  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
wenzelm@57605
    17
  val pretty_theorems: bool -> theory -> Pretty.T list
aspinall@22335
    18
  val pretty_full_theory: bool -> theory -> Pretty.T
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@51584
    22
  val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
wenzelm@49866
    23
  val method_error: string -> Position.T ->
wenzelm@49866
    24
    {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
wenzelm@56932
    25
  val print_results: bool -> Position.T -> Proof.context ->
wenzelm@56932
    26
    ((string * string) * (string * thm list) list) -> unit
wenzelm@56932
    27
  val print_consts: bool -> Position.T -> Proof.context ->
wenzelm@56932
    28
    (string * typ -> bool) -> (string * typ) list -> unit
wenzelm@17369
    29
end
wenzelm@17369
    30
wenzelm@33389
    31
structure Proof_Display: PROOF_DISPLAY =
wenzelm@17369
    32
struct
wenzelm@17369
    33
wenzelm@61252
    34
(** toplevel pretty printing **)
wenzelm@20211
    35
wenzelm@30628
    36
fun pp_context ctxt =
wenzelm@42717
    37
 (if Config.get ctxt Proof_Context.debug then
wenzelm@42360
    38
    Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
wenzelm@20211
    39
  else Pretty.str "<context>");
wenzelm@20211
    40
wenzelm@60937
    41
fun default_context mk_thy =
wenzelm@45269
    42
  (case Context.thread_data () of
wenzelm@45269
    43
    SOME (Context.Proof ctxt) => ctxt
wenzelm@45269
    44
  | SOME (Context.Theory thy) =>
wenzelm@45269
    45
      (case try Syntax.init_pretty_global thy of
wenzelm@45269
    46
        SOME ctxt => ctxt
wenzelm@60937
    47
      | NONE => Syntax.init_pretty_global (mk_thy ()))
wenzelm@60937
    48
  | NONE => Syntax.init_pretty_global (mk_thy ()));
wenzelm@60937
    49
wenzelm@60937
    50
fun pp_thm mk_thy th =
wenzelm@60937
    51
  Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
wenzelm@44240
    52
wenzelm@60937
    53
fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
wenzelm@60937
    54
fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
wenzelm@20211
    55
wenzelm@60937
    56
fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT);
wenzelm@60937
    57
fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
wenzelm@20211
    58
wenzelm@19432
    59
wenzelm@61252
    60
wenzelm@61252
    61
(** theory content **)
wenzelm@61252
    62
wenzelm@19432
    63
(* theorems and theory *)
wenzelm@19432
    64
wenzelm@33515
    65
fun pretty_theorems_diff verbose prev_thys thy =
wenzelm@19432
    66
  let
wenzelm@42360
    67
    val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
wenzelm@39557
    68
    val facts = Global_Theory.facts_of thy;
wenzelm@56158
    69
    val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
wenzelm@60924
    70
    val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
wenzelm@57605
    71
  in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
wenzelm@19432
    72
wenzelm@56868
    73
fun pretty_theorems verbose thy =
wenzelm@56868
    74
  pretty_theorems_diff verbose (Theory.parents_of thy) thy;
wenzelm@19432
    75
wenzelm@22872
    76
fun pretty_full_theory verbose thy =
wenzelm@57605
    77
  Pretty.chunks (Display.pretty_full_theory verbose thy @ pretty_theorems verbose thy);
wenzelm@20621
    78
wenzelm@61252
    79
wenzelm@61252
    80
(* definitions *)
wenzelm@61252
    81
wenzelm@61252
    82
fun pretty_definitions verbose ctxt =
wenzelm@61252
    83
  let
wenzelm@61252
    84
    val thy = Proof_Context.theory_of ctxt;
wenzelm@61261
    85
    val context = Proof_Context.defs_context ctxt;
wenzelm@61252
    86
wenzelm@61253
    87
    val const_space = Proof_Context.const_space ctxt;
wenzelm@61253
    88
    val type_space = Proof_Context.type_space ctxt;
wenzelm@61256
    89
    val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
wenzelm@61253
    90
    fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
wenzelm@61253
    91
wenzelm@61261
    92
    fun extern_item (kind, name) =
wenzelm@61261
    93
      let val xname = Name_Space.extern ctxt (item_space kind) name
wenzelm@61261
    94
      in (xname, (kind, name)) end;
wenzelm@61253
    95
wenzelm@61261
    96
    fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) =
wenzelm@61261
    97
      (case Defs.item_kind_ord (kind1, kind2) of
wenzelm@61261
    98
        EQUAL => string_ord (xname1, xname2)
wenzelm@61261
    99
      | ord => ord);
wenzelm@61253
   100
wenzelm@61261
   101
    fun sort_items f = sort (extern_item_ord o apply2 f);
wenzelm@61261
   102
wenzelm@61261
   103
    fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args);
wenzelm@61252
   104
wenzelm@61252
   105
    fun pretty_reduct (lhs, rhs) = Pretty.block
wenzelm@61253
   106
      ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
wenzelm@61253
   107
        Pretty.commas (map pretty_entry (sort_items fst rhs)));
wenzelm@61252
   108
wenzelm@61253
   109
    fun pretty_restrict (entry, name) =
wenzelm@61253
   110
      Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
wenzelm@61252
   111
wenzelm@61252
   112
    val defs = Theory.defs_of thy;
wenzelm@61252
   113
    val {restricts, reducts} = Defs.dest defs;
aspinall@22335
   114
wenzelm@61257
   115
    val (reds1, reds2) =
wenzelm@61253
   116
      filter_out (prune_item o #1 o #1) reducts
wenzelm@61252
   117
      |> map (fn (lhs, rhs) =>
wenzelm@61261
   118
        (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
wenzelm@61253
   119
      |> sort_items (#1 o #1)
wenzelm@61257
   120
      |> filter_out (null o #2)
wenzelm@61257
   121
      |> List.partition (Defs.plain_args o #2 o #1);
wenzelm@61253
   122
wenzelm@61261
   123
    val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1);
wenzelm@61252
   124
  in
wenzelm@61252
   125
    Pretty.big_list "definitions:"
wenzelm@61258
   126
      (map (Pretty.text_fold o single)
wenzelm@61258
   127
        [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1),
wenzelm@61258
   128
         Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2),
wenzelm@61258
   129
         Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)])
wenzelm@61252
   130
  end;
wenzelm@61252
   131
wenzelm@61252
   132
wenzelm@61252
   133
wenzelm@61252
   134
(** proof items **)
wenzelm@19432
   135
wenzelm@17369
   136
(* refinement rule *)
wenzelm@17369
   137
wenzelm@17369
   138
fun pretty_rule ctxt s thm =
wenzelm@17369
   139
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
wenzelm@50126
   140
    Pretty.fbrk, Display.pretty_thm ctxt thm];
wenzelm@17369
   141
wenzelm@17369
   142
val string_of_rule = Pretty.string_of ooo pretty_rule;
wenzelm@17369
   143
wenzelm@17369
   144
wenzelm@49860
   145
(* goals *)
wenzelm@49860
   146
wenzelm@49860
   147
local
wenzelm@49860
   148
wenzelm@49860
   149
fun subgoals 0 = []
wenzelm@49860
   150
  | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
wenzelm@49860
   151
  | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
wenzelm@49860
   152
wenzelm@49860
   153
in
wenzelm@49860
   154
wenzelm@49860
   155
fun pretty_goal_header goal =
wenzelm@55763
   156
  Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
wenzelm@49860
   157
wenzelm@49860
   158
end;
wenzelm@49860
   159
wenzelm@49860
   160
fun string_of_goal ctxt goal =
wenzelm@51958
   161
  Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
wenzelm@49860
   162
wenzelm@49860
   163
wenzelm@51584
   164
(* goal facts *)
wenzelm@51584
   165
wenzelm@51584
   166
fun pretty_goal_facts ctxt s ths =
wenzelm@51584
   167
  (Pretty.block o Pretty.fbreaks)
wenzelm@51601
   168
    [if s = "" then Pretty.str "this:"
wenzelm@55763
   169
     else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
wenzelm@51601
   170
     Proof_Context.pretty_fact ctxt ("", ths)];
wenzelm@51584
   171
wenzelm@51584
   172
wenzelm@49860
   173
(* method_error *)
wenzelm@49860
   174
wenzelm@49866
   175
fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
wenzelm@49860
   176
  let
wenzelm@49866
   177
    val pr_header =
wenzelm@49866
   178
      "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
wenzelm@49866
   179
      "proof method" ^ Position.here pos ^ ":\n";
wenzelm@49860
   180
    val pr_facts =
wenzelm@49860
   181
      if null facts then ""
wenzelm@51584
   182
      else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
wenzelm@49860
   183
    val pr_goal = string_of_goal ctxt goal;
wenzelm@49860
   184
  in pr_header ^ pr_facts ^ pr_goal end);
wenzelm@49860
   185
wenzelm@49860
   186
wenzelm@17369
   187
(* results *)
wenzelm@17369
   188
wenzelm@56932
   189
fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
wenzelm@56932
   190
wenzelm@28092
   191
local
wenzelm@28092
   192
wenzelm@56932
   193
fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
wenzelm@56932
   194
  | pretty_fact_name pos (kind, name) =
wenzelm@56932
   195
      Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
wenzelm@41551
   196
        Pretty.str (Long_Name.base_name name), Pretty.str ":"];
wenzelm@28087
   197
wenzelm@17369
   198
fun pretty_facts ctxt =
wenzelm@55763
   199
  flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
wenzelm@50126
   200
    map (single o Proof_Context.pretty_fact ctxt);
wenzelm@17369
   201
wenzelm@27857
   202
in
wenzelm@27857
   203
wenzelm@56932
   204
fun print_results do_print pos ctxt ((kind, name), facts) =
wenzelm@33643
   205
  if not do_print orelse kind = "" then ()
wenzelm@28092
   206
  else if name = "" then
wenzelm@59184
   207
    (Output.state o Pretty.string_of)
wenzelm@56932
   208
      (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
wenzelm@56932
   209
        pretty_facts ctxt facts))
wenzelm@46728
   210
  else
wenzelm@59184
   211
    (Output.state o Pretty.string_of)
wenzelm@46728
   212
      (case facts of
wenzelm@56932
   213
        [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
wenzelm@50126
   214
          Proof_Context.pretty_fact ctxt fact])
wenzelm@56932
   215
      | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
wenzelm@46728
   216
          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
wenzelm@17369
   217
wenzelm@17369
   218
end;
wenzelm@17369
   219
wenzelm@20889
   220
wenzelm@20889
   221
(* consts *)
wenzelm@20889
   222
wenzelm@20889
   223
local
wenzelm@20889
   224
wenzelm@20889
   225
fun pretty_var ctxt (x, T) =
wenzelm@20889
   226
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
wenzelm@24920
   227
    Pretty.quote (Syntax.pretty_typ ctxt T)];
wenzelm@20889
   228
wenzelm@56932
   229
fun pretty_vars pos ctxt kind vs =
wenzelm@56932
   230
  Pretty.block (Pretty.fbreaks (position_markup pos (Pretty.str kind) :: map (pretty_var ctxt) vs));
wenzelm@20889
   231
wenzelm@56932
   232
fun pretty_consts pos ctxt pred cs =
wenzelm@42360
   233
  (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
wenzelm@56932
   234
    [] => pretty_vars pos ctxt "constants" cs
wenzelm@56932
   235
  | ps => Pretty.chunks [pretty_vars pos ctxt "parameters" ps, pretty_vars pos ctxt "constants" cs]);
wenzelm@20889
   236
wenzelm@44192
   237
in
wenzelm@44192
   238
wenzelm@56932
   239
fun print_consts do_print pos ctxt pred cs =
wenzelm@44192
   240
  if not do_print orelse null cs then ()
wenzelm@59184
   241
  else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
wenzelm@44192
   242
wenzelm@20889
   243
end;
wenzelm@20889
   244
wenzelm@17369
   245
end;