src/Pure/Isar/proof_display.ML
author wenzelm
Thu Jul 23 16:52:16 2009 +0200 (2009-07-23)
changeset 32145 220c9e439d39
parent 32091 30e2ffbba718
child 33389 bb3a5fa94a91
permissions -rw-r--r--
clarified pretty_goals, pretty_thm_aux: plain context;
explicit pretty_goals_without_context, print_goals_without_context;
tuned;
     1 (*  Title:      Pure/Isar/proof_display.ML
     2     Author:     Makarius
     3 
     4 Printing of theorems, goals, results etc.
     5 *)
     6 
     7 signature PROOF_DISPLAY =
     8 sig
     9   val pp_context: Proof.context -> Pretty.T
    10   val pp_thm: thm -> Pretty.T
    11   val pp_typ: theory -> typ -> Pretty.T
    12   val pp_term: theory -> term -> Pretty.T
    13   val pp_ctyp: ctyp -> Pretty.T
    14   val pp_cterm: cterm -> Pretty.T
    15   val print_theorems_diff: theory -> theory -> unit
    16   val print_theorems: theory -> unit
    17   val pretty_full_theory: bool -> theory -> Pretty.T
    18   val print_theory: theory -> unit
    19   val string_of_rule: Proof.context -> string -> thm -> string
    20   val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
    21   val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
    22 end
    23 
    24 structure ProofDisplay: PROOF_DISPLAY =
    25 struct
    26 
    27 (* toplevel pretty printing *)
    28 
    29 fun pp_context ctxt =
    30  (if ! ProofContext.debug then
    31     Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
    32   else Pretty.str "<context>");
    33 
    34 fun pp_thm th =
    35   let
    36     val thy = Thm.theory_of_thm th;
    37     val flags = {quote = true, show_hyps = false, show_status = true};
    38   in Display.pretty_thm_raw (Syntax.init_pretty_global thy) flags th end;
    39 
    40 val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
    41 val pp_term = Pretty.quote oo Syntax.pretty_term_global;
    42 
    43 fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    44 fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    45 
    46 
    47 (* theorems and theory *)
    48 
    49 fun pretty_theorems_diff prev_thys thy =
    50   let
    51     val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
    52     val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
    53   in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    54 
    55 fun print_theorems_diff prev_thy thy =
    56   Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
    57 
    58 fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
    59 val print_theorems = Pretty.writeln o pretty_theorems;
    60 
    61 fun pretty_full_theory verbose thy =
    62   Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    63 
    64 val print_theory = Pretty.writeln o pretty_full_theory false;
    65 
    66 
    67 (* refinement rule *)
    68 
    69 fun pretty_rule ctxt s thm =
    70   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    71     Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
    72 
    73 val string_of_rule = Pretty.string_of ooo pretty_rule;
    74 
    75 
    76 (* results *)
    77 
    78 local
    79 
    80 fun pretty_fact_name (kind, "") = Pretty.str kind
    81   | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
    82       Pretty.str (Long_Name.base_name name), Pretty.str ":"];
    83 
    84 fun pretty_facts ctxt =
    85   flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    86     map (single o ProofContext.pretty_fact_aux ctxt false);
    87 
    88 in
    89 
    90 fun print_results do_print ctxt ((kind, name), facts) =
    91   if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
    92   else if name = "" then
    93     Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
    94   else Pretty.writeln
    95     (case facts of
    96       [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
    97         ProofContext.pretty_fact_aux ctxt false fact])
    98     | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
    99         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
   100 
   101 end;
   102 
   103 
   104 (* consts *)
   105 
   106 local
   107 
   108 fun pretty_var ctxt (x, T) =
   109   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
   110     Pretty.quote (Syntax.pretty_typ ctxt T)];
   111 
   112 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
   113 
   114 in
   115 
   116 fun pretty_consts ctxt pred cs =
   117   (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
   118     [] => pretty_vars ctxt "constants" cs
   119   | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
   120 
   121 end;
   122 
   123 end;