author | berghofe |
Fri, 16 Apr 2004 18:45:56 +0200 | |
changeset 14598 | 7009f59711e3 |
parent 14472 | cba7c0a3ffb3 |
child 14644 | 3224082514f9 |
permissions | -rw-r--r-- |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
1 |
(* Title: Pure/display.ML |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
4 |
Copyright 1993 University of Cambridge |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
5 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
6 |
Printing of theories, theorems, etc. |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
7 |
*) |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
8 |
|
11883 | 9 |
signature BASIC_DISPLAY = |
10 |
sig |
|
12081 | 11 |
val goals_limit: int ref |
11883 | 12 |
val show_hyps: bool ref |
13 |
val show_tags: bool ref |
|
14 |
val string_of_thm: thm -> string |
|
15 |
val print_thm: thm -> unit |
|
16 |
val print_thms: thm list -> unit |
|
17 |
val prth: thm -> thm |
|
18 |
val prthq: thm Seq.seq -> thm Seq.seq |
|
19 |
val prths: thm list -> thm list |
|
20 |
val string_of_ctyp: ctyp -> string |
|
21 |
val print_ctyp: ctyp -> unit |
|
22 |
val string_of_cterm: cterm -> string |
|
23 |
val print_cterm: cterm -> unit |
|
24 |
val print_syntax: theory -> unit |
|
25 |
val show_consts: bool ref |
|
26 |
end; |
|
27 |
||
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
28 |
signature DISPLAY = |
4950 | 29 |
sig |
11883 | 30 |
include BASIC_DISPLAY |
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
31 |
val pretty_flexpair: (term -> Pretty.T) -> term * term -> Pretty.T |
12081 | 32 |
val pretty_thm_aux: (sort -> Pretty.T) * (term -> Pretty.T) -> bool -> thm -> Pretty.T |
6976 | 33 |
val pretty_thm_no_quote: thm -> Pretty.T |
11883 | 34 |
val pretty_thm: thm -> Pretty.T |
35 |
val pretty_thms: thm list -> Pretty.T |
|
36 |
val pretty_thm_sg: Sign.sg -> thm -> Pretty.T |
|
37 |
val pretty_thms_sg: Sign.sg -> thm list -> Pretty.T |
|
38 |
val pprint_thm: thm -> pprint_args -> unit |
|
39 |
val pretty_ctyp: ctyp -> Pretty.T |
|
40 |
val pprint_ctyp: ctyp -> pprint_args -> unit |
|
41 |
val pretty_cterm: cterm -> Pretty.T |
|
42 |
val pprint_cterm: cterm -> pprint_args -> unit |
|
43 |
val pretty_theory: theory -> Pretty.T |
|
44 |
val pprint_theory: theory -> pprint_args -> unit |
|
8720 | 45 |
val pretty_full_theory: theory -> Pretty.T list |
11883 | 46 |
val pretty_name_space: string * NameSpace.T -> Pretty.T |
12081 | 47 |
val pretty_goals_aux: (sort -> Pretty.T) * (typ -> Pretty.T) * (term -> Pretty.T) |
48 |
-> string -> bool * bool -> int -> thm -> Pretty.T list |
|
11883 | 49 |
val pretty_goals: int -> thm -> Pretty.T list |
50 |
val print_goals: int -> thm -> unit |
|
51 |
val current_goals_markers: (string * string * string) ref |
|
12418 | 52 |
val pretty_current_goals: int -> int -> thm -> Pretty.T list |
53 |
val print_current_goals_default: int -> int -> thm -> unit |
|
54 |
val print_current_goals_fn: (int -> int -> thm -> unit) ref |
|
4950 | 55 |
end; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
56 |
|
4950 | 57 |
structure Display: DISPLAY = |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
58 |
struct |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
59 |
|
11883 | 60 |
|
6087 | 61 |
(** print thm **) |
62 |
||
12081 | 63 |
val goals_limit = ref 10; (*max number of goals to print -- set by user*) |
12831
a2a3896f9c48
reset show_hyps by default (in accordance to existing Isar practice);
wenzelm
parents:
12418
diff
changeset
|
64 |
val show_hyps = ref false; (*false: print meta-hypotheses as dots*) |
11883 | 65 |
val show_tags = ref false; (*false: suppress tags*) |
6087 | 66 |
|
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14472
diff
changeset
|
67 |
fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args); |
6087 | 68 |
val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
69 |
|
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
70 |
fun pretty_flexpair pretty_term (t, u) = Pretty.block |
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
71 |
[pretty_term t, Pretty.str " =?=", Pretty.brk 1, pretty_term u]; |
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
72 |
|
12081 | 73 |
fun pretty_thm_aux (pretty_sort, pretty_term) quote th = |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
74 |
let |
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
75 |
val {hyps, tpairs, prop, der = (ora, _), ...} = rep_thm th; |
6087 | 76 |
val xshyps = Thm.extra_shyps th; |
77 |
val (_, tags) = Thm.get_name_tags th; |
|
78 |
||
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
79 |
val q = if quote then Pretty.quote else I; |
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
80 |
val prt_term = q o pretty_term; |
6279 | 81 |
|
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
82 |
val hlen = length xshyps + length hyps + length tpairs; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
83 |
val hsymbs = |
9500 | 84 |
if hlen = 0 andalso not ora then [] |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
85 |
else if ! show_hyps then |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
86 |
[Pretty.brk 2, Pretty.list "[" "]" |
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
87 |
(map (q o pretty_flexpair pretty_term) tpairs @ map prt_term hyps @ |
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
88 |
map pretty_sort xshyps @ |
9500 | 89 |
(if ora then [Pretty.str "!"] else []))] |
6889 | 90 |
else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ |
9500 | 91 |
(if ora then "!" else "") ^ "]")]; |
6087 | 92 |
val tsymbs = |
93 |
if null tags orelse not (! show_tags) then [] |
|
94 |
else [Pretty.brk 1, pretty_tags tags]; |
|
6279 | 95 |
in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
96 |
|
12067 | 97 |
fun gen_pretty_thm quote th = |
98 |
let val sg = Thm.sign_of_thm th |
|
12081 | 99 |
in pretty_thm_aux (Sign.pretty_sort sg, Sign.pretty_term sg) quote th end; |
6889 | 100 |
|
12067 | 101 |
val pretty_thm = gen_pretty_thm true; |
102 |
val pretty_thm_no_quote = gen_pretty_thm false; |
|
6889 | 103 |
|
104 |
||
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
105 |
val string_of_thm = Pretty.string_of o pretty_thm; |
6279 | 106 |
val pprint_thm = Pretty.pprint o pretty_thm; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
107 |
|
6087 | 108 |
fun pretty_thms [th] = pretty_thm th |
109 |
| pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths)); |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
110 |
|
10010 | 111 |
val pretty_thm_sg = pretty_thm oo Thm.transfer_sg; |
112 |
val pretty_thms_sg = pretty_thms oo (map o Thm.transfer_sg); |
|
113 |
||
6087 | 114 |
|
115 |
(* top-level commands for printing theorems *) |
|
116 |
||
117 |
val print_thm = Pretty.writeln o pretty_thm; |
|
118 |
val print_thms = Pretty.writeln o pretty_thms; |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
119 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
120 |
fun prth th = (print_thm th; th); |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
121 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
122 |
(*Print and return a sequence of theorems, separated by blank lines. *) |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
123 |
fun prthq thseq = |
4270 | 124 |
(Seq.print (fn _ => print_thm) 100000 thseq; thseq); |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
125 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
126 |
(*Print and return a list of theorems, separated by blank lines. *) |
4210 | 127 |
fun prths ths = (seq (fn th => (print_thm th; writeln "")) ths; ths); |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
128 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
129 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
130 |
(* other printing commands *) |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
131 |
|
4126 | 132 |
fun pretty_ctyp cT = |
133 |
let val {sign, T} = rep_ctyp cT in Sign.pretty_typ sign T end; |
|
134 |
||
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
135 |
fun pprint_ctyp cT = |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
136 |
let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
137 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
138 |
fun string_of_ctyp cT = |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
139 |
let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
140 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
141 |
val print_ctyp = writeln o string_of_ctyp; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
142 |
|
3547 | 143 |
fun pretty_cterm ct = |
144 |
let val {sign, t, ...} = rep_cterm ct in Sign.pretty_term sign t end; |
|
145 |
||
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
146 |
fun pprint_cterm ct = |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
147 |
let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
148 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
149 |
fun string_of_cterm ct = |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
150 |
let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
151 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
152 |
val print_cterm = writeln o string_of_cterm; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
153 |
|
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
154 |
|
4250 | 155 |
|
156 |
(** print theory **) |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
157 |
|
6390 | 158 |
val pretty_theory = Sign.pretty_sg o Theory.sign_of; |
159 |
val pprint_theory = Sign.pprint_sg o Theory.sign_of; |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
160 |
|
6390 | 161 |
val print_syntax = Syntax.print_syntax o Theory.syn_of; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
162 |
|
4250 | 163 |
|
4498 | 164 |
(* pretty_name_space *) |
165 |
||
166 |
fun pretty_name_space (kind, space) = |
|
167 |
let |
|
168 |
fun prt_entry (name, accs) = Pretty.block |
|
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14472
diff
changeset
|
169 |
(Pretty.str (Library.quote name ^ " =") :: Pretty.brk 1 :: |
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14472
diff
changeset
|
170 |
Pretty.commas (map (Pretty.quote o Pretty.str) accs)); |
4498 | 171 |
in |
172 |
Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space)) |
|
173 |
|> Pretty.block |
|
174 |
end; |
|
175 |
||
176 |
||
11883 | 177 |
(* pretty_full_theory *) |
4250 | 178 |
|
8720 | 179 |
fun pretty_full_theory thy = |
4250 | 180 |
let |
8720 | 181 |
val sg = Theory.sign_of thy; |
182 |
||
4250 | 183 |
fun prt_cls c = Sign.pretty_sort sg [c]; |
184 |
fun prt_sort S = Sign.pretty_sort sg S; |
|
185 |
fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]); |
|
10737 | 186 |
fun prt_typ_no_tvars ty = Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty))); |
8720 | 187 |
fun prt_term t = Pretty.quote (Sign.pretty_term sg t); |
4250 | 188 |
|
189 |
fun pretty_classes cs = Pretty.block |
|
190 |
(Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs)); |
|
191 |
||
192 |
fun pretty_classrel (c, cs) = Pretty.block |
|
193 |
(prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: |
|
194 |
Pretty.commas (map prt_cls cs)); |
|
195 |
||
196 |
fun pretty_default S = Pretty.block |
|
197 |
[Pretty.str "default:", Pretty.brk 1, prt_sort S]; |
|
198 |
||
199 |
fun pretty_ty (t, n) = Pretty.block |
|
8458 | 200 |
[Pretty.str t, Pretty.brk 1, Pretty.str (string_of_int n)]; |
4250 | 201 |
|
7635 | 202 |
fun pretty_log_types ts = Pretty.block |
203 |
(Pretty.breaks (Pretty.str "logical types:" :: map Pretty.str ts)); |
|
204 |
||
205 |
fun pretty_witness None = Pretty.str "universal non-emptiness witness: --" |
|
206 |
| pretty_witness (Some (T, S)) = Pretty.block |
|
10737 | 207 |
[Pretty.str "universal non-emptiness witness:", Pretty.brk 1, prt_typ_no_tvars T, |
8402 | 208 |
Pretty.brk 1, prt_sort S]; |
7635 | 209 |
|
4250 | 210 |
fun pretty_abbr (t, (vs, rhs)) = Pretty.block |
10737 | 211 |
[prt_typ_no_tvars (Type (t, map (fn v => TVar ((v, 0), [])) vs)), |
212 |
Pretty.str " =", Pretty.brk 1, prt_typ_no_tvars rhs]; |
|
4250 | 213 |
|
214 |
fun pretty_arities (t, ars) = map (prt_arity t) ars; |
|
215 |
||
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14178
diff
changeset
|
216 |
fun pretty_final (c:string, tys:typ list) = Pretty.block |
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14178
diff
changeset
|
217 |
([Pretty.str c, Pretty.str " ::", Pretty.brk 1] @ |
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14178
diff
changeset
|
218 |
(if null tys then [Pretty.str "<all instances>"] |
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14178
diff
changeset
|
219 |
else Pretty.commas (map prt_typ_no_tvars tys))); |
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14178
diff
changeset
|
220 |
|
4250 | 221 |
fun pretty_const (c, ty) = Pretty.block |
10737 | 222 |
[Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; |
4250 | 223 |
|
8720 | 224 |
fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; |
225 |
||
226 |
||
4250 | 227 |
val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg; |
8720 | 228 |
val {axioms, oracles, ...} = Theory.rep_theory thy; |
6846 | 229 |
val spaces' = Library.sort_wrt fst spaces; |
7635 | 230 |
val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} = |
4250 | 231 |
Type.rep_tsig tsig; |
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14178
diff
changeset
|
232 |
val finals = Symtab.dest (#final_consts (rep_theory thy)); |
7067 | 233 |
val tycons = Sign.cond_extern_table sg Sign.typeK type_tab; |
6846 | 234 |
val consts = Sign.cond_extern_table sg Sign.constK const_tab; |
8720 | 235 |
val axms = Sign.cond_extern_table sg Theory.axiomK axioms; |
236 |
val oras = Sign.cond_extern_table sg Theory.oracleK oracles; |
|
4250 | 237 |
in |
8720 | 238 |
[Pretty.strs ("stamps:" :: Sign.stamp_names_of sg), |
239 |
Pretty.strs ("data:" :: Sign.data_kinds data), |
|
11501 | 240 |
Pretty.strs ["name prefix:", NameSpace.pack (if_none path ["-"])], |
8720 | 241 |
Pretty.big_list "name spaces:" (map pretty_name_space spaces'), |
242 |
pretty_classes classes, |
|
243 |
Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)), |
|
244 |
pretty_default default, |
|
245 |
pretty_log_types log_types, |
|
246 |
pretty_witness univ_witness, |
|
247 |
Pretty.big_list "type constructors:" (map pretty_ty tycons), |
|
248 |
Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)), |
|
249 |
Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))), |
|
250 |
Pretty.big_list "consts:" (map pretty_const consts), |
|
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14178
diff
changeset
|
251 |
Pretty.big_list "finals:" (map pretty_final finals), |
8720 | 252 |
Pretty.big_list "axioms:" (map prt_axm axms), |
253 |
Pretty.strs ("oracles:" :: (map #1 oras))] |
|
4250 | 254 |
end; |
255 |
||
256 |
||
11883 | 257 |
|
258 |
(** print_goals **) |
|
259 |
||
260 |
(* print_goals etc. *) |
|
261 |
||
8908 | 262 |
(*show consts with types in proof state output?*) |
3851
fe9932a7cd46
print_goals: optional output of const types (set show_consts);
wenzelm
parents:
3811
diff
changeset
|
263 |
val show_consts = ref false; |
fe9932a7cd46
print_goals: optional output of const types (set show_consts);
wenzelm
parents:
3811
diff
changeset
|
264 |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
265 |
|
11883 | 266 |
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) |
267 |
||
268 |
local |
|
269 |
||
12081 | 270 |
fun ins_entry (x, y) [] = [(x, [y])] |
271 |
| ins_entry (x, y) ((pair as (x', ys')) :: pairs) = |
|
272 |
if x = x' then (x', y ins ys') :: pairs |
|
273 |
else pair :: ins_entry (x, y) pairs; |
|
274 |
||
275 |
fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env |
|
276 |
| add_consts (t $ u, env) = add_consts (u, add_consts (t, env)) |
|
277 |
| add_consts (Abs (_, _, t), env) = add_consts (t, env) |
|
278 |
| add_consts (_, env) = env; |
|
11883 | 279 |
|
12081 | 280 |
fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env |
281 |
| add_vars (Var (xi, T), env) = ins_entry (T, xi) env |
|
282 |
| add_vars (Abs (_, _, t), env) = add_vars (t, env) |
|
283 |
| add_vars (t $ u, env) = add_vars (u, add_vars (t, env)) |
|
284 |
| add_vars (_, env) = env; |
|
11883 | 285 |
|
12081 | 286 |
fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env) |
287 |
| add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env |
|
288 |
| add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env; |
|
11883 | 289 |
|
14472
cba7c0a3ffb3
Removing the datatype declaration of "order" allows the standard General.order
paulson
parents:
14223
diff
changeset
|
290 |
fun sort_idxs vs = map (apsnd (sort (prod_ord String.compare Int.compare))) vs; |
12081 | 291 |
fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; |
292 |
||
293 |
fun consts_of t = sort_cnsts (add_consts (t, [])); |
|
294 |
fun vars_of t = sort_idxs (add_vars (t, [])); |
|
295 |
fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, []))); |
|
296 |
||
297 |
in |
|
11883 | 298 |
|
12081 | 299 |
fun pretty_goals_aux (prt_sort, prt_typ, prt_term) begin_goal (msg, main) maxgoals state = |
300 |
let |
|
301 |
fun prt_atoms prt prtT (X, xs) = Pretty.block |
|
302 |
[Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", |
|
303 |
Pretty.brk 1, prtT X]; |
|
11883 | 304 |
|
12081 | 305 |
fun prt_var (x, ~1) = prt_term (Syntax.free x) |
306 |
| prt_var xi = prt_term (Syntax.var xi); |
|
307 |
||
308 |
fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) |
|
309 |
| prt_varT xi = prt_typ (TVar (xi, [])); |
|
310 |
||
311 |
val prt_consts = prt_atoms (prt_term o Const) prt_typ; |
|
312 |
val prt_vars = prt_atoms prt_var prt_typ; |
|
313 |
val prt_varsT = prt_atoms prt_varT prt_sort; |
|
11883 | 314 |
|
315 |
||
12081 | 316 |
fun pretty_list _ _ [] = [] |
317 |
| pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; |
|
11883 | 318 |
|
12081 | 319 |
fun pretty_subgoal (n, A) = |
320 |
Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]); |
|
321 |
fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); |
|
11883 | 322 |
|
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
323 |
val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair prt_term); |
11883 | 324 |
|
12081 | 325 |
val pretty_consts = pretty_list "constants:" prt_consts o consts_of; |
326 |
val pretty_vars = pretty_list "variables:" prt_vars o vars_of; |
|
327 |
val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of; |
|
11883 | 328 |
|
329 |
||
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
330 |
val {prop, tpairs, ...} = rep_thm state; |
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
331 |
val (As, B) = Logic.strip_horn prop; |
12081 | 332 |
val ngoals = length As; |
11883 | 333 |
|
12081 | 334 |
fun pretty_gs (types, sorts) = |
335 |
(if main then [prt_term B] else []) @ |
|
336 |
(if ngoals = 0 then [Pretty.str "No subgoals!"] |
|
337 |
else if ngoals > maxgoals then |
|
338 |
pretty_subgoals (take (maxgoals, As)) @ |
|
339 |
(if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] |
|
340 |
else []) |
|
341 |
else pretty_subgoals As) @ |
|
342 |
pretty_ffpairs tpairs @ |
|
343 |
(if ! show_consts then pretty_consts prop else []) @ |
|
344 |
(if types then pretty_vars prop else []) @ |
|
345 |
(if sorts then pretty_varsT prop else []); |
|
346 |
in |
|
347 |
setmp show_no_free_types true |
|
14178
14a12da7288e
Makes interactive proof scripting recognize the show_all_types flag.
skalberg
parents:
13658
diff
changeset
|
348 |
(setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types) |
12081 | 349 |
(setmp show_sorts false pretty_gs)) |
14178
14a12da7288e
Makes interactive proof scripting recognize the show_all_types flag.
skalberg
parents:
13658
diff
changeset
|
350 |
(! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) |
11883 | 351 |
end; |
352 |
||
12081 | 353 |
fun pretty_goals_marker bg n th = |
354 |
let val sg = Thm.sign_of_thm th in |
|
355 |
pretty_goals_aux (Sign.pretty_sort sg, Sign.pretty_typ sg, Sign.pretty_term sg) |
|
356 |
bg (true, true) n th |
|
357 |
end; |
|
358 |
||
359 |
val pretty_goals = pretty_goals_marker ""; |
|
12418 | 360 |
val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals_marker ""; |
12081 | 361 |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
362 |
end; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
363 |
|
11883 | 364 |
|
365 |
(* print_current_goals *) |
|
366 |
||
367 |
val current_goals_markers = ref ("", "", ""); |
|
368 |
||
12418 | 369 |
fun pretty_current_goals n m th = |
11883 | 370 |
let |
371 |
val ref (begin_state, end_state, begin_goal) = current_goals_markers; |
|
372 |
val ngoals = nprems_of th; |
|
373 |
in |
|
12418 | 374 |
(if begin_state = "" then [] else [Pretty.str begin_state]) @ |
375 |
[Pretty.str ("Level " ^ string_of_int n ^ |
|
11883 | 376 |
(if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ |
377 |
(if ngoals <> 1 then "s" else "") ^ ")" |
|
12418 | 378 |
else ""))] @ |
379 |
pretty_goals_marker begin_goal m th @ |
|
380 |
(if end_state = "" then [] else [Pretty.str end_state]) |
|
11883 | 381 |
end; |
382 |
||
12418 | 383 |
fun print_current_goals_default n m th = |
384 |
Pretty.writeln (Pretty.chunks (pretty_current_goals n m th)); |
|
385 |
||
11883 | 386 |
val print_current_goals_fn = ref print_current_goals_default; |
387 |
||
388 |
end; |
|
389 |
||
390 |
structure BasicDisplay: BASIC_DISPLAY = Display; |
|
391 |
open BasicDisplay; |