src/Pure/Isar/proof_display.ML
author wenzelm
Wed Apr 16 21:53:04 2008 +0200 (2008-04-16)
changeset 26696 1cd71fb32831
parent 26415 1b624d6e9163
child 26949 a9a1ebfb4d23
permissions -rw-r--r--
pretty_theorems: use proper PureThy.facts_of;
     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 (ProofContext.init 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_facts thy =
    56   let
    57     val ctxt = ProofContext.init thy;
    58     val facts = PureThy.facts_of thy;
    59     val thmss = Facts.fold_static (fn (name, ths) =>
    60       if exists (fn prev => Facts.defined prev name) prev_facts then I
    61       else cons (Facts.extern facts name, ths)) facts [];
    62   in Pretty.big_list "theorems:" (map (ProofContext.pretty_fact ctxt) (sort_wrt #1 thmss)) end;
    63 
    64 fun print_theorems_diff prev_thy thy =
    65   Pretty.writeln (pretty_theorems_diff [PureThy.facts_of prev_thy] thy);
    66 
    67 fun pretty_theorems thy = pretty_theorems_diff (map PureThy.facts_of (Theory.parents_of thy)) thy;
    68 val print_theorems = Pretty.writeln o pretty_theorems;
    69 
    70 fun pretty_full_theory verbose thy =
    71   Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    72 
    73 val print_theory = Pretty.writeln o pretty_full_theory false;
    74 
    75 
    76 (* refinement rule *)
    77 
    78 fun pretty_rule ctxt s thm =
    79   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    80     Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
    81 
    82 val string_of_rule = Pretty.string_of ooo pretty_rule;
    83 
    84 
    85 (* results *)
    86 
    87 local
    88 
    89 fun pretty_facts ctxt =
    90   flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    91     map (single o ProofContext.pretty_fact ctxt);
    92 
    93 fun pretty_results ctxt ((kind, ""), facts) =
    94       Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
    95   | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
    96       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
    97   | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
    98       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
    99         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
   100 
   101 fun name_results "" res = res
   102   | name_results name res =
   103       let
   104         val n = length (maps snd res);
   105         fun name_res (a, ths) i =
   106           let
   107             val m = length ths;
   108             val j = i + m;
   109           in
   110             if a <> "" then ((a, ths), j)
   111             else if m = n then ((name, ths), j)
   112             else ((Facts.string_of_ref (Facts.Named ((name, Position.none),
   113               SOME ([if m = 1 then Facts.Single i else Facts.FromTo (i, j - 1)]))), ths), j)
   114           end;
   115       in fst (fold_map name_res res 1) end;
   116 
   117 in
   118 
   119 fun print_results true = Pretty.writeln oo pretty_results
   120   | print_results false = K (K ());
   121 
   122 fun present_results ctxt ((kind, name), res) =
   123   if kind = "" orelse kind = Thm.internalK then ()
   124   else (print_results true ctxt ((kind, name), res);
   125     Context.setmp_thread_data (SOME (Context.Proof ctxt))
   126       (Present.results kind) (name_results name res));
   127 
   128 end;
   129 
   130 
   131 (* consts *)
   132 
   133 local
   134 
   135 fun pretty_var ctxt (x, T) =
   136   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
   137     Pretty.quote (Syntax.pretty_typ ctxt T)];
   138 
   139 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
   140 
   141 in
   142 
   143 fun pretty_consts ctxt pred cs =
   144   (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
   145     [] => pretty_vars ctxt "constants" cs
   146   | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
   147 
   148 end;
   149 
   150 end;
   151 
   152 structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
   153 open BasicProofDisplay;