src/Pure/Isar/proof_display.ML
author wenzelm
Mon Nov 19 20:23:47 2012 +0100 (2012-11-19 ago)
changeset 50126 3dec88149176
parent 49867 d3053a55bfcb
child 51584 98029ceda8ce
permissions -rw-r--r--
theorem status about oracles/futures is no longer printed by default;
renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
     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 pretty_goal_header: thm -> Pretty.T
    21   val string_of_goal: Proof.context -> thm -> string
    22   val method_error: string -> Position.T ->
    23     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
    24   val print_results: Markup.T -> bool -> Proof.context ->
    25     ((string * string) * (string * thm list) list) -> unit
    26   val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
    27 end
    28 
    29 structure Proof_Display: PROOF_DISPLAY =
    30 struct
    31 
    32 (* toplevel pretty printing *)
    33 
    34 fun pp_context ctxt =
    35  (if Config.get ctxt Proof_Context.debug then
    36     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
    37   else Pretty.str "<context>");
    38 
    39 fun default_context thy0 =
    40   (case Context.thread_data () of
    41     SOME (Context.Proof ctxt) => ctxt
    42   | SOME (Context.Theory thy) =>
    43       (case try Syntax.init_pretty_global thy of
    44         SOME ctxt => ctxt
    45       | NONE => Syntax.init_pretty_global thy0)
    46   | NONE => Syntax.init_pretty_global thy0);
    47 
    48 fun pp_thm th =
    49   let val ctxt = default_context (Thm.theory_of_thm th);
    50   in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
    51 
    52 fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
    53 fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
    54 
    55 fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    56 fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    57 
    58 
    59 (* theorems and theory *)
    60 
    61 fun pretty_theorems_diff verbose prev_thys thy =
    62   let
    63     val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
    64     val facts = Global_Theory.facts_of thy;
    65     val thmss =
    66       Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
    67       |> not verbose ? filter_out (Facts.is_concealed facts o #1);
    68   in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    69 
    70 fun print_theorems_diff verbose prev_thy thy =
    71   Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
    72 
    73 fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
    74 val print_theorems = Pretty.writeln oo pretty_theorems;
    75 
    76 fun pretty_full_theory verbose thy =
    77   Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
    78 
    79 val print_theory = Pretty.writeln o pretty_full_theory false;
    80 
    81 
    82 (* refinement rule *)
    83 
    84 fun pretty_rule ctxt s thm =
    85   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    86     Pretty.fbrk, Display.pretty_thm ctxt thm];
    87 
    88 val string_of_rule = Pretty.string_of ooo pretty_rule;
    89 
    90 
    91 (* goals *)
    92 
    93 local
    94 
    95 fun subgoals 0 = []
    96   | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
    97   | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
    98 
    99 in
   100 
   101 fun pretty_goal_header goal =
   102   Pretty.block ([Pretty.command "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
   103 
   104 end;
   105 
   106 fun string_of_goal ctxt goal =
   107   Pretty.string_of (Pretty.chunks
   108     [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
   109 
   110 
   111 (* method_error *)
   112 
   113 fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
   114   let
   115     val pr_header =
   116       "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
   117       "proof method" ^ Position.here pos ^ ":\n";
   118     val pr_facts =
   119       if null facts then ""
   120       else
   121         (Pretty.string_of o Pretty.block o Pretty.fbreaks)
   122           (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
   123             map (Display.pretty_thm ctxt) facts) ^ "\n";
   124     val pr_goal = string_of_goal ctxt goal;
   125   in pr_header ^ pr_facts ^ pr_goal end);
   126 
   127 
   128 (* results *)
   129 
   130 local
   131 
   132 fun pretty_fact_name (kind, "") = Pretty.command kind
   133   | pretty_fact_name (kind, name) =
   134       Pretty.block [Pretty.command kind, Pretty.brk 1,
   135         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
   136 
   137 fun pretty_facts ctxt =
   138   flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
   139     map (single o Proof_Context.pretty_fact ctxt);
   140 
   141 in
   142 
   143 fun print_results markup do_print ctxt ((kind, name), facts) =
   144   if not do_print orelse kind = "" then ()
   145   else if name = "" then
   146     (Pretty.writeln o Pretty.mark markup)
   147       (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   148   else
   149     (Pretty.writeln o Pretty.mark markup)
   150       (case facts of
   151         [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
   152           Proof_Context.pretty_fact ctxt fact])
   153       | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
   154           Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
   155 
   156 end;
   157 
   158 
   159 (* consts *)
   160 
   161 local
   162 
   163 fun pretty_var ctxt (x, T) =
   164   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
   165     Pretty.quote (Syntax.pretty_typ ctxt T)];
   166 
   167 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
   168 
   169 fun pretty_consts ctxt pred cs =
   170   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
   171     [] => pretty_vars ctxt "constants" cs
   172   | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
   173 
   174 in
   175 
   176 fun print_consts do_print ctxt pred cs =
   177   if not do_print orelse null cs then ()
   178   else Pretty.writeln (pretty_consts ctxt pred cs);
   179 
   180 end;
   181 
   182 end;