src/Pure/Isar/proof_display.ML
author wenzelm
Fri Sep 12 12:04:16 2008 +0200 (2008-09-12)
changeset 28210 c164d1892553
parent 28092 5886e9359aa8
child 29606 fedb8be05f24
permissions -rw-r--r--
more procise printing of fact names;
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@17369
     8
signature PROOF_DISPLAY =
wenzelm@17369
     9
sig
wenzelm@20311
    10
  val pprint_context: Proof.context -> pprint_args -> unit
wenzelm@20211
    11
  val pprint_typ: theory -> typ -> pprint_args -> unit
wenzelm@20211
    12
  val pprint_term: theory -> term -> pprint_args -> unit
wenzelm@20211
    13
  val pprint_ctyp: ctyp -> pprint_args -> unit
wenzelm@20211
    14
  val pprint_cterm: cterm -> pprint_args -> unit
wenzelm@20211
    15
  val pprint_thm: thm -> pprint_args -> unit
wenzelm@19432
    16
  val print_theorems_diff: theory -> theory -> unit
wenzelm@28092
    17
  val print_theorems: theory -> unit
aspinall@22335
    18
  val pretty_full_theory: bool -> theory -> Pretty.T
wenzelm@28092
    19
  val print_theory: theory -> unit
wenzelm@20311
    20
  val string_of_rule: Proof.context -> string -> thm -> string
wenzelm@27857
    21
  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
wenzelm@27857
    22
  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
wenzelm@17369
    23
end
wenzelm@17369
    24
wenzelm@17369
    25
structure ProofDisplay: PROOF_DISPLAY =
wenzelm@17369
    26
struct
wenzelm@17369
    27
wenzelm@20235
    28
(* toplevel pretty printing *)
wenzelm@20211
    29
wenzelm@20211
    30
fun pprint_context ctxt = Pretty.pprint
wenzelm@20311
    31
 (if ! ProofContext.debug then
wenzelm@20211
    32
    Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
wenzelm@20211
    33
  else Pretty.str "<context>");
wenzelm@20211
    34
wenzelm@26949
    35
fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
wenzelm@20211
    36
wenzelm@24920
    37
val pprint_typ = pprint Syntax.pretty_typ;
wenzelm@24920
    38
val pprint_term = pprint Syntax.pretty_term;
wenzelm@20211
    39
fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
wenzelm@20211
    40
fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
wenzelm@22872
    41
val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
wenzelm@20211
    42
wenzelm@19432
    43
wenzelm@19432
    44
(* theorems and theory *)
wenzelm@19432
    45
wenzelm@27176
    46
fun pretty_theorems_diff prev_thys thy =
wenzelm@19432
    47
  let
wenzelm@27176
    48
    val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
wenzelm@28210
    49
    val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
wenzelm@28210
    50
  in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
wenzelm@19432
    51
wenzelm@19432
    52
fun print_theorems_diff prev_thy thy =
wenzelm@27176
    53
  Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
wenzelm@19432
    54
wenzelm@27176
    55
fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
wenzelm@19432
    56
val print_theorems = Pretty.writeln o pretty_theorems;
wenzelm@19432
    57
wenzelm@22872
    58
fun pretty_full_theory verbose thy =
wenzelm@22872
    59
  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
wenzelm@20621
    60
wenzelm@22872
    61
val print_theory = Pretty.writeln o pretty_full_theory false;
aspinall@22335
    62
wenzelm@19432
    63
wenzelm@17369
    64
(* refinement rule *)
wenzelm@17369
    65
wenzelm@17369
    66
fun pretty_rule ctxt s thm =
wenzelm@17369
    67
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
wenzelm@17369
    68
    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
wenzelm@17369
    69
wenzelm@17369
    70
val string_of_rule = Pretty.string_of ooo pretty_rule;
wenzelm@17369
    71
wenzelm@17369
    72
wenzelm@17369
    73
(* results *)
wenzelm@17369
    74
wenzelm@28092
    75
local
wenzelm@28092
    76
wenzelm@28087
    77
fun pretty_fact_name (kind, "") = Pretty.str kind
wenzelm@28087
    78
  | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
wenzelm@28087
    79
      Pretty.str (NameSpace.base name), Pretty.str ":"];
wenzelm@28087
    80
wenzelm@17369
    81
fun pretty_facts ctxt =
wenzelm@19482
    82
  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
wenzelm@17369
    83
    map (single o ProofContext.pretty_fact ctxt);
wenzelm@17369
    84
wenzelm@27857
    85
in
wenzelm@27857
    86
wenzelm@28092
    87
fun print_results do_print ctxt ((kind, name), facts) =
wenzelm@28092
    88
  if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
wenzelm@28092
    89
  else if name = "" then
wenzelm@28092
    90
    Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
wenzelm@28092
    91
  else Pretty.writeln
wenzelm@28092
    92
    (case facts of
wenzelm@28092
    93
      [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
wenzelm@28092
    94
        ProofContext.pretty_fact ctxt fact])
wenzelm@28092
    95
    | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
wenzelm@28092
    96
        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
wenzelm@17369
    97
wenzelm@17369
    98
end;
wenzelm@17369
    99
wenzelm@20889
   100
wenzelm@20889
   101
(* consts *)
wenzelm@20889
   102
wenzelm@20889
   103
local
wenzelm@20889
   104
wenzelm@20889
   105
fun pretty_var ctxt (x, T) =
wenzelm@20889
   106
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
wenzelm@24920
   107
    Pretty.quote (Syntax.pretty_typ ctxt T)];
wenzelm@20889
   108
wenzelm@20889
   109
fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
wenzelm@20889
   110
wenzelm@20889
   111
in
wenzelm@20889
   112
wenzelm@20889
   113
fun pretty_consts ctxt pred cs =
wenzelm@20889
   114
  (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
wenzelm@20889
   115
    [] => pretty_vars ctxt "constants" cs
wenzelm@20889
   116
  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
wenzelm@20889
   117
wenzelm@20889
   118
end;
wenzelm@20889
   119
wenzelm@17369
   120
end;