src/Pure/Isar/proof_display.ML
author wenzelm
Thu Jun 12 16:41:58 2008 +0200 (2008-06-12)
changeset 27176 3735b80d06fc
parent 26949 a9a1ebfb4d23
child 27857 fdf43ffceae0
permissions -rw-r--r--
Facts.dest/export_static: content difference;
tuned;
     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 pretty_full_theory: bool -> theory -> Pretty.T
    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   val pretty_consts: Proof.context ->
    31     (string * typ -> bool) -> (string * typ) list -> Pretty.T
    32 end
    33 
    34 structure ProofDisplay: PROOF_DISPLAY =
    35 struct
    36 
    37 (* toplevel pretty printing *)
    38 
    39 fun pprint_context ctxt = Pretty.pprint
    40  (if ! ProofContext.debug then
    41     Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
    42   else Pretty.str "<context>");
    43 
    44 fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
    45 
    46 val pprint_typ = pprint Syntax.pretty_typ;
    47 val pprint_term = pprint Syntax.pretty_term;
    48 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    49 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    50 val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
    51 
    52 
    53 (* theorems and theory *)
    54 
    55 fun pretty_theorems_diff prev_thys thy =
    56   let
    57     val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
    58     val thmss = Facts.extern_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
    59   in Pretty.big_list "theorems:" (map pretty_fact thmss) end;
    60 
    61 fun print_theorems_diff prev_thy thy =
    62   Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
    63 
    64 fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
    65 val print_theorems = Pretty.writeln o pretty_theorems;
    66 
    67 fun pretty_full_theory verbose thy =
    68   Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    69 
    70 val print_theory = Pretty.writeln o pretty_full_theory false;
    71 
    72 
    73 (* refinement rule *)
    74 
    75 fun pretty_rule ctxt s thm =
    76   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    77     Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
    78 
    79 val string_of_rule = Pretty.string_of ooo pretty_rule;
    80 
    81 
    82 (* results *)
    83 
    84 local
    85 
    86 fun pretty_facts ctxt =
    87   flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    88     map (single o ProofContext.pretty_fact ctxt);
    89 
    90 fun pretty_results ctxt ((kind, ""), facts) =
    91       Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
    92   | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
    93       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
    94   | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
    95       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
    96         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
    97 
    98 fun name_results "" res = res
    99   | name_results name res =
   100       let
   101         val n = length (maps snd res);
   102         fun name_res (a, ths) i =
   103           let
   104             val m = length ths;
   105             val j = i + m;
   106           in
   107             if a <> "" then ((a, ths), j)
   108             else if m = n then ((name, ths), j)
   109             else ((Facts.string_of_ref (Facts.Named ((name, Position.none),
   110               SOME ([if m = 1 then Facts.Single i else Facts.FromTo (i, j - 1)]))), ths), j)
   111           end;
   112       in fst (fold_map name_res res 1) end;
   113 
   114 in
   115 
   116 fun print_results true = Pretty.writeln oo pretty_results
   117   | print_results false = K (K ());
   118 
   119 fun present_results ctxt ((kind, name), res) =
   120   if kind = "" orelse kind = Thm.internalK then ()
   121   else (print_results true ctxt ((kind, name), res);
   122     Context.setmp_thread_data (SOME (Context.Proof ctxt))
   123       (Present.results kind) (name_results name res));
   124 
   125 end;
   126 
   127 
   128 (* consts *)
   129 
   130 local
   131 
   132 fun pretty_var ctxt (x, T) =
   133   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
   134     Pretty.quote (Syntax.pretty_typ ctxt T)];
   135 
   136 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
   137 
   138 in
   139 
   140 fun pretty_consts ctxt pred cs =
   141   (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
   142     [] => pretty_vars ctxt "constants" cs
   143   | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
   144 
   145 end;
   146 
   147 end;
   148 
   149 structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
   150 open BasicProofDisplay;