src/Pure/Isar/proof_display.ML
author wenzelm
Mon Nov 14 16:52:19 2011 +0100 (2011-11-14 ago)
changeset 45488 6d71d9e52369
parent 45269 6f8949e6c71a
child 46728 85f8e3932712
permissions -rw-r--r--
pass positions for named targets, for formal links in the document model;
     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: bool -> theory -> theory -> unit
    16   val print_theorems: bool -> 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 print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
    22 end
    23 
    24 structure Proof_Display: PROOF_DISPLAY =
    25 struct
    26 
    27 (* toplevel pretty printing *)
    28 
    29 fun pp_context ctxt =
    30  (if Config.get ctxt Proof_Context.debug then
    31     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
    32   else Pretty.str "<context>");
    33 
    34 fun default_context thy0 =
    35   (case Context.thread_data () of
    36     SOME (Context.Proof ctxt) => ctxt
    37   | SOME (Context.Theory thy) =>
    38       (case try Syntax.init_pretty_global thy of
    39         SOME ctxt => ctxt
    40       | NONE => Syntax.init_pretty_global thy0)
    41   | NONE => Syntax.init_pretty_global thy0);
    42 
    43 fun pp_thm th =
    44   let
    45     val ctxt = default_context (Thm.theory_of_thm th);
    46     val flags = {quote = true, show_hyps = false, show_status = true};
    47   in Display.pretty_thm_raw ctxt flags th end;
    48 
    49 fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
    50 fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
    51 
    52 fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    53 fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    54 
    55 
    56 (* theorems and theory *)
    57 
    58 fun pretty_theorems_diff verbose prev_thys thy =
    59   let
    60     val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
    61     val facts = Global_Theory.facts_of thy;
    62     val thmss =
    63       Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
    64       |> not verbose ? filter_out (Facts.is_concealed facts o #1);
    65   in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    66 
    67 fun print_theorems_diff verbose prev_thy thy =
    68   Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
    69 
    70 fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
    71 val print_theorems = Pretty.writeln oo pretty_theorems;
    72 
    73 fun pretty_full_theory verbose thy =
    74   Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
    75 
    76 val print_theory = Pretty.writeln o pretty_full_theory false;
    77 
    78 
    79 (* refinement rule *)
    80 
    81 fun pretty_rule ctxt s thm =
    82   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    83     Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
    84 
    85 val string_of_rule = Pretty.string_of ooo pretty_rule;
    86 
    87 
    88 (* results *)
    89 
    90 local
    91 
    92 fun pretty_fact_name (kind, "") = Pretty.command kind
    93   | pretty_fact_name (kind, name) =
    94       Pretty.block [Pretty.command kind, Pretty.brk 1,
    95         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
    96 
    97 fun pretty_facts ctxt =
    98   flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
    99     map (single o Proof_Context.pretty_fact_aux ctxt false);
   100 
   101 in
   102 
   103 fun print_results do_print ctxt ((kind, name), facts) =
   104   if not do_print orelse kind = "" then ()
   105   else if name = "" then
   106     Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   107   else Pretty.writeln
   108     (case facts of
   109       [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
   110         Proof_Context.pretty_fact_aux ctxt false fact])
   111     | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
   112         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
   113 
   114 end;
   115 
   116 
   117 (* consts *)
   118 
   119 local
   120 
   121 fun pretty_var ctxt (x, T) =
   122   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
   123     Pretty.quote (Syntax.pretty_typ ctxt T)];
   124 
   125 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
   126 
   127 fun pretty_consts ctxt pred cs =
   128   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
   129     [] => pretty_vars ctxt "constants" cs
   130   | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
   131 
   132 in
   133 
   134 fun print_consts do_print ctxt pred cs =
   135   if not do_print orelse null cs then ()
   136   else Pretty.writeln (pretty_consts ctxt pred cs);
   137 
   138 end;
   139 
   140 end;