src/Pure/Isar/proof_display.ML
author wenzelm
Thu Apr 13 12:01:10 2006 +0200 (2006-04-13)
changeset 19432 cae7cc072994
parent 18799 f137c5e971f5
child 19482 9f11af8f7ef9
permissions -rw-r--r--
added print_theorems/theory, print_theorems_diff (from pure_thy.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@19432
    17
  val print_theorems_diff: theory -> theory -> unit
wenzelm@17369
    18
  val string_of_rule: ProofContext.context -> string -> thm -> string
wenzelm@17369
    19
  val print_results: bool -> ProofContext.context ->
wenzelm@17369
    20
    ((string * string) * (string * thm list) list) -> unit
wenzelm@17369
    21
  val present_results: ProofContext.context ->
wenzelm@17369
    22
    ((string * string) * (string * thm list) list) -> unit
wenzelm@17369
    23
end
wenzelm@17369
    24
wenzelm@17369
    25
structure ProofDisplay: PROOF_DISPLAY =
wenzelm@17369
    26
struct
wenzelm@17369
    27
wenzelm@19432
    28
wenzelm@19432
    29
(* theorems and theory *)
wenzelm@19432
    30
wenzelm@19432
    31
fun pretty_theorems_diff prev_thms thy =
wenzelm@19432
    32
  let
wenzelm@19432
    33
    val ctxt = ProofContext.init thy;
wenzelm@19432
    34
    val (space, thms) = PureThy.theorems_of thy;
wenzelm@19432
    35
    val diff_thmss = Symtab.fold (fn fact =>
wenzelm@19432
    36
      if not (Symtab.member Thm.eq_thms prev_thms fact) then cons fact else I) thms [];
wenzelm@19432
    37
    val thmss = diff_thmss |> map (apfst (NameSpace.extern space)) |> Library.sort_wrt #1;
wenzelm@19432
    38
  in Pretty.big_list "theorems:" (map (ProofContext.pretty_fact ctxt) thmss) end;
wenzelm@19432
    39
wenzelm@19432
    40
fun print_theorems_diff prev_thy thy =
wenzelm@19432
    41
  Pretty.writeln (pretty_theorems_diff (#2 (PureThy.theorems_of prev_thy)) thy);
wenzelm@19432
    42
wenzelm@19432
    43
fun pretty_theorems thy = pretty_theorems_diff Symtab.empty thy;
wenzelm@19432
    44
wenzelm@19432
    45
val print_theorems = Pretty.writeln o pretty_theorems;
wenzelm@19432
    46
wenzelm@19432
    47
fun print_theory thy =
wenzelm@19432
    48
  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory thy @ [pretty_theorems thy]));
wenzelm@19432
    49
wenzelm@19432
    50
wenzelm@17369
    51
(* refinement rule *)
wenzelm@17369
    52
wenzelm@17369
    53
fun pretty_rule ctxt s thm =
wenzelm@17369
    54
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
wenzelm@17369
    55
    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
wenzelm@17369
    56
wenzelm@17369
    57
val string_of_rule = Pretty.string_of ooo pretty_rule;
wenzelm@17369
    58
wenzelm@17369
    59
wenzelm@17369
    60
(* results *)
wenzelm@17369
    61
wenzelm@17369
    62
local
wenzelm@17369
    63
wenzelm@17369
    64
fun pretty_facts ctxt =
wenzelm@17369
    65
  List.concat o (separate [Pretty.fbrk, Pretty.str "and "]) o
wenzelm@17369
    66
    map (single o ProofContext.pretty_fact ctxt);
wenzelm@17369
    67
wenzelm@17369
    68
fun pretty_results ctxt ((kind, ""), facts) =
wenzelm@17369
    69
      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
wenzelm@17369
    70
  | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
wenzelm@17369
    71
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
wenzelm@17369
    72
  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
wenzelm@17369
    73
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
wenzelm@17369
    74
        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
wenzelm@17369
    75
wenzelm@17369
    76
fun name_results "" res = res
wenzelm@17369
    77
  | name_results name res =
wenzelm@17369
    78
      let
wenzelm@17756
    79
        val n = length (List.concat (map snd res));
wenzelm@17369
    80
        fun name_res (a, ths) i =
wenzelm@17369
    81
          let
wenzelm@17369
    82
            val m = length ths;
wenzelm@17369
    83
            val j = i + m;
wenzelm@17369
    84
          in
wenzelm@17369
    85
            if a <> "" then ((a, ths), j)
wenzelm@17369
    86
            else if m = n then ((name, ths), j)
wenzelm@17369
    87
            else if m = 1 then
wenzelm@17369
    88
              ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
wenzelm@17369
    89
            else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
wenzelm@17369
    90
          end;
wenzelm@17756
    91
      in fst (fold_map name_res res 1) end;
wenzelm@17369
    92
wenzelm@17369
    93
in
wenzelm@17369
    94
wenzelm@17369
    95
fun print_results true = Pretty.writeln oo pretty_results
wenzelm@17369
    96
  | print_results false = K (K ());
wenzelm@17369
    97
wenzelm@17369
    98
fun present_results ctxt ((kind, name), res) =
wenzelm@18799
    99
  if kind = "" orelse kind = PureThy.internalK then ()
wenzelm@17369
   100
  else (print_results true ctxt ((kind, name), res);
wenzelm@17369
   101
    Context.setmp (SOME (ProofContext.theory_of ctxt))
wenzelm@17369
   102
      (Present.results kind) (name_results name res));
wenzelm@17369
   103
wenzelm@17369
   104
end;
wenzelm@17369
   105
wenzelm@17369
   106
end;
wenzelm@19432
   107
wenzelm@19432
   108
structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
wenzelm@19432
   109
open BasicProofDisplay;
wenzelm@19432
   110