src/Pure/Isar/proof_display.ML
author wenzelm
Thu Jul 27 13:43:13 2006 +0200 (2006-07-27)
changeset 20235 3cbf73ed92f8
parent 20211 c7f907f41f7c
child 20253 636ac45d100f
permissions -rw-r--r--
ProofContext.legacy_pretty_thm;
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@20211
    17
  val debug: bool ref
wenzelm@20211
    18
  val pprint_context: ProofContext.context -> pprint_args -> unit
wenzelm@20211
    19
  val pprint_typ: theory -> typ -> pprint_args -> unit
wenzelm@20211
    20
  val pprint_term: theory -> term -> pprint_args -> unit
wenzelm@20211
    21
  val pprint_ctyp: ctyp -> pprint_args -> unit
wenzelm@20211
    22
  val pprint_cterm: cterm -> pprint_args -> unit
wenzelm@20211
    23
  val pprint_thm: thm -> pprint_args -> unit
wenzelm@19432
    24
  val print_theorems_diff: theory -> theory -> unit
wenzelm@17369
    25
  val string_of_rule: ProofContext.context -> string -> thm -> string
wenzelm@17369
    26
  val print_results: bool -> ProofContext.context ->
wenzelm@17369
    27
    ((string * string) * (string * thm list) list) -> unit
wenzelm@17369
    28
  val present_results: ProofContext.context ->
wenzelm@17369
    29
    ((string * string) * (string * thm list) list) -> unit
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
val debug = ref false;
wenzelm@20211
    38
wenzelm@20211
    39
fun pprint_context ctxt = Pretty.pprint
wenzelm@20211
    40
 (if ! debug then
wenzelm@20211
    41
    Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
wenzelm@20211
    42
  else Pretty.str "<context>");
wenzelm@20211
    43
wenzelm@20211
    44
fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
wenzelm@20211
    45
wenzelm@20211
    46
val pprint_typ = pprint ProofContext.pretty_typ;
wenzelm@20211
    47
val pprint_term = pprint ProofContext.pretty_term;
wenzelm@20211
    48
fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
wenzelm@20211
    49
fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
wenzelm@20235
    50
val pprint_thm = Pretty.pprint o ProofContext.legacy_pretty_thm true;
wenzelm@20211
    51
wenzelm@19432
    52
wenzelm@19432
    53
(* theorems and theory *)
wenzelm@19432
    54
wenzelm@19432
    55
fun pretty_theorems_diff prev_thms thy =
wenzelm@19432
    56
  let
wenzelm@19432
    57
    val ctxt = ProofContext.init thy;
wenzelm@19432
    58
    val (space, thms) = PureThy.theorems_of thy;
wenzelm@19432
    59
    val diff_thmss = Symtab.fold (fn fact =>
wenzelm@19432
    60
      if not (Symtab.member Thm.eq_thms prev_thms fact) then cons fact else I) thms [];
wenzelm@19432
    61
    val thmss = diff_thmss |> map (apfst (NameSpace.extern space)) |> Library.sort_wrt #1;
wenzelm@19432
    62
  in Pretty.big_list "theorems:" (map (ProofContext.pretty_fact ctxt) thmss) end;
wenzelm@19432
    63
wenzelm@19432
    64
fun print_theorems_diff prev_thy thy =
wenzelm@19432
    65
  Pretty.writeln (pretty_theorems_diff (#2 (PureThy.theorems_of prev_thy)) thy);
wenzelm@19432
    66
wenzelm@19432
    67
fun pretty_theorems thy = pretty_theorems_diff Symtab.empty thy;
wenzelm@19432
    68
wenzelm@19432
    69
val print_theorems = Pretty.writeln o pretty_theorems;
wenzelm@19432
    70
wenzelm@19432
    71
fun print_theory thy =
wenzelm@19432
    72
  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory thy @ [pretty_theorems thy]));
wenzelm@19432
    73
wenzelm@19432
    74
wenzelm@17369
    75
(* refinement rule *)
wenzelm@17369
    76
wenzelm@17369
    77
fun pretty_rule ctxt s thm =
wenzelm@17369
    78
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
wenzelm@17369
    79
    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
wenzelm@17369
    80
wenzelm@17369
    81
val string_of_rule = Pretty.string_of ooo pretty_rule;
wenzelm@17369
    82
wenzelm@17369
    83
wenzelm@17369
    84
(* results *)
wenzelm@17369
    85
wenzelm@17369
    86
local
wenzelm@17369
    87
wenzelm@17369
    88
fun pretty_facts ctxt =
wenzelm@19482
    89
  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
wenzelm@17369
    90
    map (single o ProofContext.pretty_fact ctxt);
wenzelm@17369
    91
wenzelm@17369
    92
fun pretty_results ctxt ((kind, ""), facts) =
wenzelm@17369
    93
      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
wenzelm@17369
    94
  | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
wenzelm@17369
    95
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
wenzelm@17369
    96
  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
wenzelm@17369
    97
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
wenzelm@17369
    98
        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
wenzelm@17369
    99
wenzelm@17369
   100
fun name_results "" res = res
wenzelm@17369
   101
  | name_results name res =
wenzelm@17369
   102
      let
wenzelm@19482
   103
        val n = length (maps snd res);
wenzelm@17369
   104
        fun name_res (a, ths) i =
wenzelm@17369
   105
          let
wenzelm@17369
   106
            val m = length ths;
wenzelm@17369
   107
            val j = i + m;
wenzelm@17369
   108
          in
wenzelm@17369
   109
            if a <> "" then ((a, ths), j)
wenzelm@17369
   110
            else if m = n then ((name, ths), j)
wenzelm@17369
   111
            else if m = 1 then
wenzelm@17369
   112
              ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
wenzelm@17369
   113
            else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
wenzelm@17369
   114
          end;
wenzelm@17756
   115
      in fst (fold_map name_res res 1) end;
wenzelm@17369
   116
wenzelm@17369
   117
in
wenzelm@17369
   118
wenzelm@17369
   119
fun print_results true = Pretty.writeln oo pretty_results
wenzelm@17369
   120
  | print_results false = K (K ());
wenzelm@17369
   121
wenzelm@17369
   122
fun present_results ctxt ((kind, name), res) =
wenzelm@18799
   123
  if kind = "" orelse kind = PureThy.internalK then ()
wenzelm@17369
   124
  else (print_results true ctxt ((kind, name), res);
wenzelm@17369
   125
    Context.setmp (SOME (ProofContext.theory_of ctxt))
wenzelm@17369
   126
      (Present.results kind) (name_results name res));
wenzelm@17369
   127
wenzelm@17369
   128
end;
wenzelm@17369
   129
wenzelm@17369
   130
end;
wenzelm@19432
   131
wenzelm@19432
   132
structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
wenzelm@19432
   133
open BasicProofDisplay;