src/Pure/Isar/proof_display.ML
author wenzelm
Wed Aug 13 20:57:31 2008 +0200 (2008-08-13)
changeset 27857 fdf43ffceae0
parent 27176 3735b80d06fc
child 28087 a9cccdd9d521
permissions -rw-r--r--
removed obsolete present_results;
added theory_results, which is subject to hooks (formerly in present.ML);
wenzelm@17369
     1
(*  Title:      Pure/Isar/proof_display.ML
wenzelm@17369
     2
    ID:         $Id$
wenzelm@17369
     3
    Author:     Makarius
wenzelm@17369
     4
wenzelm@19432
     5
Printing of theorems, goals, results etc.
wenzelm@17369
     6
*)
wenzelm@17369
     7
wenzelm@19432
     8
signature BASIC_PROOF_DISPLAY =
wenzelm@19432
     9
sig
wenzelm@19432
    10
  val print_theorems: theory -> unit
wenzelm@19432
    11
  val print_theory: theory -> unit
wenzelm@19432
    12
end
wenzelm@19432
    13
wenzelm@17369
    14
signature PROOF_DISPLAY =
wenzelm@17369
    15
sig
wenzelm@19432
    16
  include BASIC_PROOF_DISPLAY
wenzelm@20311
    17
  val pprint_context: Proof.context -> pprint_args -> unit
wenzelm@20211
    18
  val pprint_typ: theory -> typ -> pprint_args -> unit
wenzelm@20211
    19
  val pprint_term: theory -> term -> pprint_args -> unit
wenzelm@20211
    20
  val pprint_ctyp: ctyp -> pprint_args -> unit
wenzelm@20211
    21
  val pprint_cterm: cterm -> pprint_args -> unit
wenzelm@20211
    22
  val pprint_thm: thm -> pprint_args -> unit
wenzelm@19432
    23
  val print_theorems_diff: theory -> theory -> unit
aspinall@22335
    24
  val pretty_full_theory: bool -> theory -> Pretty.T
wenzelm@20311
    25
  val string_of_rule: Proof.context -> string -> thm -> string
wenzelm@27857
    26
  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
wenzelm@27857
    27
  val add_hook: ((string * thm list) list -> unit) -> unit
wenzelm@27857
    28
  val theory_results: Proof.context -> ((string * string) * (string * thm list) list) -> unit
wenzelm@27857
    29
  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
wenzelm@17369
    30
end
wenzelm@17369
    31
wenzelm@17369
    32
structure ProofDisplay: PROOF_DISPLAY =
wenzelm@17369
    33
struct
wenzelm@17369
    34
wenzelm@20235
    35
(* toplevel pretty printing *)
wenzelm@20211
    36
wenzelm@20211
    37
fun pprint_context ctxt = Pretty.pprint
wenzelm@20311
    38
 (if ! ProofContext.debug then
wenzelm@20211
    39
    Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
wenzelm@20211
    40
  else Pretty.str "<context>");
wenzelm@20211
    41
wenzelm@26949
    42
fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
wenzelm@20211
    43
wenzelm@24920
    44
val pprint_typ = pprint Syntax.pretty_typ;
wenzelm@24920
    45
val pprint_term = pprint Syntax.pretty_term;
wenzelm@20211
    46
fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
wenzelm@20211
    47
fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
wenzelm@22872
    48
val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
wenzelm@20211
    49
wenzelm@19432
    50
wenzelm@19432
    51
(* theorems and theory *)
wenzelm@19432
    52
wenzelm@27176
    53
fun pretty_theorems_diff prev_thys thy =
wenzelm@19432
    54
  let
wenzelm@27176
    55
    val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
wenzelm@27176
    56
    val thmss = Facts.extern_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
wenzelm@27176
    57
  in Pretty.big_list "theorems:" (map pretty_fact thmss) end;
wenzelm@19432
    58
wenzelm@19432
    59
fun print_theorems_diff prev_thy thy =
wenzelm@27176
    60
  Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
wenzelm@19432
    61
wenzelm@27176
    62
fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
wenzelm@19432
    63
val print_theorems = Pretty.writeln o pretty_theorems;
wenzelm@19432
    64
wenzelm@22872
    65
fun pretty_full_theory verbose thy =
wenzelm@22872
    66
  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
wenzelm@20621
    67
wenzelm@22872
    68
val print_theory = Pretty.writeln o pretty_full_theory false;
aspinall@22335
    69
wenzelm@19432
    70
wenzelm@17369
    71
(* refinement rule *)
wenzelm@17369
    72
wenzelm@17369
    73
fun pretty_rule ctxt s thm =
wenzelm@17369
    74
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
wenzelm@17369
    75
    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
wenzelm@17369
    76
wenzelm@17369
    77
val string_of_rule = Pretty.string_of ooo pretty_rule;
wenzelm@17369
    78
wenzelm@17369
    79
wenzelm@17369
    80
(* results *)
wenzelm@17369
    81
wenzelm@17369
    82
local
wenzelm@17369
    83
wenzelm@17369
    84
fun pretty_facts ctxt =
wenzelm@19482
    85
  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
wenzelm@17369
    86
    map (single o ProofContext.pretty_fact ctxt);
wenzelm@17369
    87
wenzelm@17369
    88
fun pretty_results ctxt ((kind, ""), facts) =
wenzelm@17369
    89
      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
wenzelm@17369
    90
  | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
wenzelm@17369
    91
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
wenzelm@17369
    92
  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
wenzelm@17369
    93
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
wenzelm@17369
    94
        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
wenzelm@17369
    95
wenzelm@27857
    96
in
wenzelm@27857
    97
wenzelm@27857
    98
fun print_results true = Pretty.writeln oo pretty_results
wenzelm@27857
    99
  | print_results false = K (K ());
wenzelm@27857
   100
wenzelm@27857
   101
end;
wenzelm@27857
   102
wenzelm@27857
   103
wenzelm@27857
   104
(* theory results -- subject to hook *)
wenzelm@27857
   105
wenzelm@27857
   106
local val hooks = ref ([]: ((string * thm list) list -> unit) list) in
wenzelm@27857
   107
wenzelm@27857
   108
fun add_hook f = CRITICAL (fn () => change hooks (cons f));
wenzelm@27857
   109
fun get_hooks () = CRITICAL (fn () => ! hooks);
wenzelm@27857
   110
wenzelm@27857
   111
end;
wenzelm@27857
   112
wenzelm@27857
   113
local
wenzelm@27857
   114
wenzelm@17369
   115
fun name_results "" res = res
wenzelm@17369
   116
  | name_results name res =
wenzelm@17369
   117
      let
wenzelm@19482
   118
        val n = length (maps snd res);
wenzelm@17369
   119
        fun name_res (a, ths) i =
wenzelm@17369
   120
          let
wenzelm@17369
   121
            val m = length ths;
wenzelm@17369
   122
            val j = i + m;
wenzelm@17369
   123
          in
wenzelm@17369
   124
            if a <> "" then ((a, ths), j)
wenzelm@17369
   125
            else if m = n then ((name, ths), j)
wenzelm@26361
   126
            else ((Facts.string_of_ref (Facts.Named ((name, Position.none),
wenzelm@26361
   127
              SOME ([if m = 1 then Facts.Single i else Facts.FromTo (i, j - 1)]))), ths), j)
wenzelm@17369
   128
          end;
wenzelm@17756
   129
      in fst (fold_map name_res res 1) end;
wenzelm@17369
   130
wenzelm@17369
   131
in
wenzelm@17369
   132
wenzelm@27857
   133
fun theory_results ctxt ((kind, name), res) =
wenzelm@21437
   134
  if kind = "" orelse kind = Thm.internalK then ()
wenzelm@27857
   135
  else
wenzelm@27857
   136
    let
wenzelm@27857
   137
      val _ = print_results true ctxt ((kind, name), res);
wenzelm@27857
   138
      val res' = name_results name res;
wenzelm@27857
   139
      val _ = List.app (fn f => f res') (get_hooks ());
wenzelm@27857
   140
    in () end;
wenzelm@17369
   141
wenzelm@17369
   142
end;
wenzelm@17369
   143
wenzelm@20889
   144
wenzelm@20889
   145
(* consts *)
wenzelm@20889
   146
wenzelm@20889
   147
local
wenzelm@20889
   148
wenzelm@20889
   149
fun pretty_var ctxt (x, T) =
wenzelm@20889
   150
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
wenzelm@24920
   151
    Pretty.quote (Syntax.pretty_typ ctxt T)];
wenzelm@20889
   152
wenzelm@20889
   153
fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
wenzelm@20889
   154
wenzelm@20889
   155
in
wenzelm@20889
   156
wenzelm@20889
   157
fun pretty_consts ctxt pred cs =
wenzelm@20889
   158
  (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
wenzelm@20889
   159
    [] => pretty_vars ctxt "constants" cs
wenzelm@20889
   160
  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
wenzelm@20889
   161
wenzelm@20889
   162
end;
wenzelm@20889
   163
wenzelm@17369
   164
end;
wenzelm@19432
   165
wenzelm@19432
   166
structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
wenzelm@19432
   167
open BasicProofDisplay;