src/Pure/Isar/proof_display.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 17756 d4a35f82fbb4
child 18799 f137c5e971f5
permissions -rw-r--r--
simplified type attribute;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/proof_display.ML
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     4
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     5
Printing of Isar proof configurations etc.
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     6
*)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     7
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     8
signature PROOF_DISPLAY =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     9
sig
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    10
  val string_of_rule: ProofContext.context -> string -> thm -> string
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    11
  val print_results: bool -> ProofContext.context ->
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    12
    ((string * string) * (string * thm list) list) -> unit
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    13
  val present_results: ProofContext.context ->
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    14
    ((string * string) * (string * thm list) list) -> unit
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    15
end
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    16
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    17
structure ProofDisplay: PROOF_DISPLAY =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    18
struct
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    19
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    20
(* refinement rule *)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    21
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    22
fun pretty_rule ctxt s thm =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    23
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    24
    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    25
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    26
val string_of_rule = Pretty.string_of ooo pretty_rule;
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    27
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    28
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    29
(* results *)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    30
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    31
local
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    32
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    33
fun pretty_facts ctxt =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    34
  List.concat o (separate [Pretty.fbrk, Pretty.str "and "]) o
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    35
    map (single o ProofContext.pretty_fact ctxt);
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    36
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    37
fun pretty_results ctxt ((kind, ""), facts) =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    38
      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    39
  | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    40
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    41
  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    42
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    43
        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    44
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    45
fun name_results "" res = res
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    46
  | name_results name res =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    47
      let
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17369
diff changeset
    48
        val n = length (List.concat (map snd res));
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    49
        fun name_res (a, ths) i =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    50
          let
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    51
            val m = length ths;
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    52
            val j = i + m;
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    53
          in
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    54
            if a <> "" then ((a, ths), j)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    55
            else if m = n then ((name, ths), j)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    56
            else if m = 1 then
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    57
              ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    58
            else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    59
          end;
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17369
diff changeset
    60
      in fst (fold_map name_res res 1) end;
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    61
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    62
in
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    63
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    64
fun print_results true = Pretty.writeln oo pretty_results
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    65
  | print_results false = K (K ());
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    66
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    67
fun present_results ctxt ((kind, name), res) =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    68
  if kind = "" orelse kind = Drule.internalK then ()
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    69
  else (print_results true ctxt ((kind, name), res);
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    70
    Context.setmp (SOME (ProofContext.theory_of ctxt))
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    71
      (Present.results kind) (name_results name res));
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    72
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    73
end;
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    74
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    75
end;