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