author | wenzelm |
Thu, 23 Jul 2009 16:52:16 +0200 | |
changeset 32145 | 220c9e439d39 |
parent 32091 | 30e2ffbba718 |
child 33389 | bb3a5fa94a91 |
permissions | -rw-r--r-- |
17369 | 1 |
(* Title: Pure/Isar/proof_display.ML |
2 |
Author: Makarius |
|
3 |
||
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
4 |
Printing of theorems, goals, results etc. |
17369 | 5 |
*) |
6 |
||
7 |
signature PROOF_DISPLAY = |
|
8 |
sig |
|
30628 | 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 |
|
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
15 |
val print_theorems_diff: theory -> theory -> unit |
28092 | 16 |
val print_theorems: theory -> unit |
22335 | 17 |
val pretty_full_theory: bool -> theory -> Pretty.T |
28092 | 18 |
val print_theory: theory -> unit |
20311 | 19 |
val string_of_rule: Proof.context -> string -> thm -> string |
27857 | 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 |
|
17369 | 22 |
end |
23 |
||
24 |
structure ProofDisplay: PROOF_DISPLAY = |
|
25 |
struct |
|
26 |
||
20235 | 27 |
(* toplevel pretty printing *) |
20211 | 28 |
|
30628 | 29 |
fun pp_context ctxt = |
20311 | 30 |
(if ! ProofContext.debug then |
20211 | 31 |
Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt)) |
32 |
else Pretty.str "<context>"); |
|
33 |
||
30628 | 34 |
fun pp_thm th = |
30724
2e54e89bcce7
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
wenzelm
parents:
30628
diff
changeset
|
35 |
let |
2e54e89bcce7
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
wenzelm
parents:
30628
diff
changeset
|
36 |
val thy = Thm.theory_of_thm th; |
2e54e89bcce7
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
wenzelm
parents:
30628
diff
changeset
|
37 |
val flags = {quote = true, show_hyps = false, show_status = true}; |
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32091
diff
changeset
|
38 |
in Display.pretty_thm_raw (Syntax.init_pretty_global thy) flags th end; |
20211 | 39 |
|
30628 | 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); |
|
20211 | 45 |
|
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
46 |
|
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
47 |
(* theorems and theory *) |
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
48 |
|
27176 | 49 |
fun pretty_theorems_diff prev_thys thy = |
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
50 |
let |
27176 | 51 |
val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy); |
28210 | 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; |
|
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
54 |
|
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
55 |
fun print_theorems_diff prev_thy thy = |
27176 | 56 |
Pretty.writeln (pretty_theorems_diff [prev_thy] thy); |
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
57 |
|
27176 | 58 |
fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy; |
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
59 |
val print_theorems = Pretty.writeln o pretty_theorems; |
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
60 |
|
22872 | 61 |
fun pretty_full_theory verbose thy = |
62 |
Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]); |
|
20621 | 63 |
|
22872 | 64 |
val print_theory = Pretty.writeln o pretty_full_theory false; |
22335 | 65 |
|
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset
|
66 |
|
17369 | 67 |
(* refinement rule *) |
68 |
||
69 |
fun pretty_rule ctxt s thm = |
|
70 |
Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"), |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30724
diff
changeset
|
71 |
Pretty.fbrk, Display.pretty_thm_aux ctxt false thm]; |
17369 | 72 |
|
73 |
val string_of_rule = Pretty.string_of ooo pretty_rule; |
|
74 |
||
75 |
||
76 |
(* results *) |
|
77 |
||
28092 | 78 |
local |
79 |
||
28087
a9cccdd9d521
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
wenzelm
parents:
27857
diff
changeset
|
80 |
fun pretty_fact_name (kind, "") = Pretty.str kind |
a9cccdd9d521
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
wenzelm
parents:
27857
diff
changeset
|
81 |
| pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1, |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
82 |
Pretty.str (Long_Name.base_name name), Pretty.str ":"]; |
28087
a9cccdd9d521
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
wenzelm
parents:
27857
diff
changeset
|
83 |
|
17369 | 84 |
fun pretty_facts ctxt = |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19432
diff
changeset
|
85 |
flat o (separate [Pretty.fbrk, Pretty.str "and "]) o |
30724
2e54e89bcce7
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
wenzelm
parents:
30628
diff
changeset
|
86 |
map (single o ProofContext.pretty_fact_aux ctxt false); |
17369 | 87 |
|
27857 | 88 |
in |
89 |
||
28092 | 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, |
|
30724
2e54e89bcce7
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
wenzelm
parents:
30628
diff
changeset
|
97 |
ProofContext.pretty_fact_aux ctxt false fact]) |
28092 | 98 |
| _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, |
99 |
Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])); |
|
17369 | 100 |
|
101 |
end; |
|
102 |
||
20889 | 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, |
|
24920 | 110 |
Pretty.quote (Syntax.pretty_typ ctxt T)]; |
20889 | 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 |
||
17369 | 123 |
end; |