src/Pure/Isar/proof_display.ML
author wenzelm
Fri Sep 12 12:04:16 2008 +0200 (2008-09-12)
changeset 28210 c164d1892553
parent 28092 5886e9359aa8
child 29606 fedb8be05f24
permissions -rw-r--r--
more procise printing of fact names;
     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 PROOF_DISPLAY =
     9 sig
    10   val pprint_context: Proof.context -> pprint_args -> unit
    11   val pprint_typ: theory -> typ -> pprint_args -> unit
    12   val pprint_term: theory -> term -> pprint_args -> unit
    13   val pprint_ctyp: ctyp -> pprint_args -> unit
    14   val pprint_cterm: cterm -> pprint_args -> unit
    15   val pprint_thm: thm -> pprint_args -> unit
    16   val print_theorems_diff: theory -> theory -> unit
    17   val print_theorems: theory -> unit
    18   val pretty_full_theory: bool -> theory -> Pretty.T
    19   val print_theory: theory -> unit
    20   val string_of_rule: Proof.context -> string -> thm -> string
    21   val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
    22   val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
    23 end
    24 
    25 structure ProofDisplay: PROOF_DISPLAY =
    26 struct
    27 
    28 (* toplevel pretty printing *)
    29 
    30 fun pprint_context ctxt = Pretty.pprint
    31  (if ! ProofContext.debug then
    32     Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
    33   else Pretty.str "<context>");
    34 
    35 fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
    36 
    37 val pprint_typ = pprint Syntax.pretty_typ;
    38 val pprint_term = pprint Syntax.pretty_term;
    39 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    40 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    41 val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
    42 
    43 
    44 (* theorems and theory *)
    45 
    46 fun pretty_theorems_diff prev_thys thy =
    47   let
    48     val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
    49     val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
    50   in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    51 
    52 fun print_theorems_diff prev_thy thy =
    53   Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
    54 
    55 fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
    56 val print_theorems = Pretty.writeln o pretty_theorems;
    57 
    58 fun pretty_full_theory verbose thy =
    59   Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    60 
    61 val print_theory = Pretty.writeln o pretty_full_theory false;
    62 
    63 
    64 (* refinement rule *)
    65 
    66 fun pretty_rule ctxt s thm =
    67   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    68     Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
    69 
    70 val string_of_rule = Pretty.string_of ooo pretty_rule;
    71 
    72 
    73 (* results *)
    74 
    75 local
    76 
    77 fun pretty_fact_name (kind, "") = Pretty.str kind
    78   | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
    79       Pretty.str (NameSpace.base name), Pretty.str ":"];
    80 
    81 fun pretty_facts ctxt =
    82   flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    83     map (single o ProofContext.pretty_fact ctxt);
    84 
    85 in
    86 
    87 fun print_results do_print ctxt ((kind, name), facts) =
    88   if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
    89   else if name = "" then
    90     Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
    91   else Pretty.writeln
    92     (case facts of
    93       [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
    94         ProofContext.pretty_fact ctxt fact])
    95     | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
    96         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
    97 
    98 end;
    99 
   100 
   101 (* consts *)
   102 
   103 local
   104 
   105 fun pretty_var ctxt (x, T) =
   106   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
   107     Pretty.quote (Syntax.pretty_typ ctxt T)];
   108 
   109 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
   110 
   111 in
   112 
   113 fun pretty_consts ctxt pred cs =
   114   (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
   115     [] => pretty_vars ctxt "constants" cs
   116   | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
   117 
   118 end;
   119 
   120 end;