src/Pure/Isar/proof_display.ML
author wenzelm
Tue Sep 19 23:15:26 2006 +0200 (2006-09-19)
changeset 20621 29d57880ba00
parent 20311 3666316adad6
child 20889 f625a65bfed5
permissions -rw-r--r--
'print_theory': bang option for full verbosity;
     1 (*  Title:      Pure/Isar/proof_display.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Printing of theorems, goals, results etc.
     6 *)
     7 
     8 signature BASIC_PROOF_DISPLAY =
     9 sig
    10   val print_theorems: theory -> unit
    11   val print_theory: theory -> unit
    12 end
    13 
    14 signature PROOF_DISPLAY =
    15 sig
    16   include BASIC_PROOF_DISPLAY
    17   val pprint_context: Proof.context -> pprint_args -> unit
    18   val pprint_typ: theory -> typ -> pprint_args -> unit
    19   val pprint_term: theory -> term -> pprint_args -> unit
    20   val pprint_ctyp: ctyp -> pprint_args -> unit
    21   val pprint_cterm: cterm -> pprint_args -> unit
    22   val pprint_thm: thm -> pprint_args -> unit
    23   val print_theorems_diff: theory -> theory -> unit
    24   val print_full_theory: bool -> theory -> unit
    25   val string_of_rule: Proof.context -> string -> thm -> string
    26   val print_results: bool -> Proof.context ->
    27     ((string * string) * (string * thm list) list) -> unit
    28   val present_results: Proof.context ->
    29     ((string * string) * (string * thm list) list) -> unit
    30 end
    31 
    32 structure ProofDisplay: PROOF_DISPLAY =
    33 struct
    34 
    35 (* toplevel pretty printing *)
    36 
    37 fun pprint_context ctxt = Pretty.pprint
    38  (if ! ProofContext.debug then
    39     Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
    40   else Pretty.str "<context>");
    41 
    42 fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
    43 
    44 val pprint_typ = pprint ProofContext.pretty_typ;
    45 val pprint_term = pprint ProofContext.pretty_term;
    46 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    47 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    48 val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy true;
    49 
    50 
    51 (* theorems and theory *)
    52 
    53 fun pretty_theorems_diff prev_thms thy =
    54   let
    55     val ctxt = ProofContext.init thy;
    56     val (space, thms) = PureThy.theorems_of thy;
    57     val diff_thmss = Symtab.fold (fn fact =>
    58       if not (Symtab.member Thm.eq_thms prev_thms fact) then cons fact else I) thms [];
    59     val thmss = diff_thmss |> map (apfst (NameSpace.extern space)) |> Library.sort_wrt #1;
    60   in Pretty.big_list "theorems:" (map (ProofContext.pretty_fact ctxt) thmss) end;
    61 
    62 fun print_theorems_diff prev_thy thy =
    63   Pretty.writeln (pretty_theorems_diff (#2 (PureThy.theorems_of prev_thy)) thy);
    64 
    65 fun pretty_theorems thy = pretty_theorems_diff Symtab.empty thy;
    66 
    67 val print_theorems = Pretty.writeln o pretty_theorems;
    68 
    69 fun print_full_theory verbose thy =
    70   Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]));
    71 
    72 val print_theory = print_full_theory false;
    73 
    74 
    75 (* refinement rule *)
    76 
    77 fun pretty_rule ctxt s thm =
    78   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    79     Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
    80 
    81 val string_of_rule = Pretty.string_of ooo pretty_rule;
    82 
    83 
    84 (* results *)
    85 
    86 local
    87 
    88 fun pretty_facts ctxt =
    89   flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    90     map (single o ProofContext.pretty_fact ctxt);
    91 
    92 fun pretty_results ctxt ((kind, ""), facts) =
    93       Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
    94   | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
    95       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
    96   | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
    97       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
    98         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
    99 
   100 fun name_results "" res = res
   101   | name_results name res =
   102       let
   103         val n = length (maps snd res);
   104         fun name_res (a, ths) i =
   105           let
   106             val m = length ths;
   107             val j = i + m;
   108           in
   109             if a <> "" then ((a, ths), j)
   110             else if m = n then ((name, ths), j)
   111             else if m = 1 then
   112               ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
   113             else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
   114           end;
   115       in fst (fold_map name_res res 1) end;
   116 
   117 in
   118 
   119 fun print_results true = Pretty.writeln oo pretty_results
   120   | print_results false = K (K ());
   121 
   122 fun present_results ctxt ((kind, name), res) =
   123   if kind = "" orelse kind = PureThy.internalK then ()
   124   else (print_results true ctxt ((kind, name), res);
   125     Context.setmp (SOME (ProofContext.theory_of ctxt))
   126       (Present.results kind) (name_results name res));
   127 
   128 end;
   129 
   130 end;
   131 
   132 structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
   133 open BasicProofDisplay;