author | berghofe |
Fri, 11 Jul 2003 14:55:17 +0200 | |
changeset 14102 | 8af7334af4b3 |
parent 13658 | c9ad3e64ddcf |
child 14178 | 14a12da7288e |
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 |
|
8402 | 67 |
fun pretty_tag (name, args) = Pretty.strs (name :: map 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 |
|
169 |
(Pretty.str (quote name ^ " =") :: Pretty.brk 1 :: |
|
170 |
Pretty.commas (map (Pretty.str o quote) accs)); |
|
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 |
||
216 |
fun pretty_const (c, ty) = Pretty.block |
|
10737 | 217 |
[Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; |
4250 | 218 |
|
8720 | 219 |
fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; |
220 |
||
221 |
||
4250 | 222 |
val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg; |
8720 | 223 |
val {axioms, oracles, ...} = Theory.rep_theory thy; |
6846 | 224 |
val spaces' = Library.sort_wrt fst spaces; |
7635 | 225 |
val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} = |
4250 | 226 |
Type.rep_tsig tsig; |
7067 | 227 |
val tycons = Sign.cond_extern_table sg Sign.typeK type_tab; |
6846 | 228 |
val consts = Sign.cond_extern_table sg Sign.constK const_tab; |
8720 | 229 |
val axms = Sign.cond_extern_table sg Theory.axiomK axioms; |
230 |
val oras = Sign.cond_extern_table sg Theory.oracleK oracles; |
|
4250 | 231 |
in |
8720 | 232 |
[Pretty.strs ("stamps:" :: Sign.stamp_names_of sg), |
233 |
Pretty.strs ("data:" :: Sign.data_kinds data), |
|
11501 | 234 |
Pretty.strs ["name prefix:", NameSpace.pack (if_none path ["-"])], |
8720 | 235 |
Pretty.big_list "name spaces:" (map pretty_name_space spaces'), |
236 |
pretty_classes classes, |
|
237 |
Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)), |
|
238 |
pretty_default default, |
|
239 |
pretty_log_types log_types, |
|
240 |
pretty_witness univ_witness, |
|
241 |
Pretty.big_list "type constructors:" (map pretty_ty tycons), |
|
242 |
Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)), |
|
243 |
Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))), |
|
244 |
Pretty.big_list "consts:" (map pretty_const consts), |
|
245 |
Pretty.big_list "axioms:" (map prt_axm axms), |
|
246 |
Pretty.strs ("oracles:" :: (map #1 oras))] |
|
4250 | 247 |
end; |
248 |
||
249 |
||
11883 | 250 |
|
251 |
(** print_goals **) |
|
252 |
||
253 |
(* print_goals etc. *) |
|
254 |
||
8908 | 255 |
(*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
|
256 |
val show_consts = ref false; |
fe9932a7cd46
print_goals: optional output of const types (set show_consts);
wenzelm
parents:
3811
diff
changeset
|
257 |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
258 |
|
11883 | 259 |
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) |
260 |
||
261 |
local |
|
262 |
||
12081 | 263 |
fun ins_entry (x, y) [] = [(x, [y])] |
264 |
| ins_entry (x, y) ((pair as (x', ys')) :: pairs) = |
|
265 |
if x = x' then (x', y ins ys') :: pairs |
|
266 |
else pair :: ins_entry (x, y) pairs; |
|
267 |
||
268 |
fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env |
|
269 |
| add_consts (t $ u, env) = add_consts (u, add_consts (t, env)) |
|
270 |
| add_consts (Abs (_, _, t), env) = add_consts (t, env) |
|
271 |
| add_consts (_, env) = env; |
|
11883 | 272 |
|
12081 | 273 |
fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env |
274 |
| add_vars (Var (xi, T), env) = ins_entry (T, xi) env |
|
275 |
| add_vars (Abs (_, _, t), env) = add_vars (t, env) |
|
276 |
| add_vars (t $ u, env) = add_vars (u, add_vars (t, env)) |
|
277 |
| add_vars (_, env) = env; |
|
11883 | 278 |
|
12081 | 279 |
fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env) |
280 |
| add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env |
|
281 |
| add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env; |
|
11883 | 282 |
|
12081 | 283 |
fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs; |
284 |
fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; |
|
285 |
||
286 |
fun consts_of t = sort_cnsts (add_consts (t, [])); |
|
287 |
fun vars_of t = sort_idxs (add_vars (t, [])); |
|
288 |
fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, []))); |
|
289 |
||
290 |
in |
|
11883 | 291 |
|
12081 | 292 |
fun pretty_goals_aux (prt_sort, prt_typ, prt_term) begin_goal (msg, main) maxgoals state = |
293 |
let |
|
294 |
fun prt_atoms prt prtT (X, xs) = Pretty.block |
|
295 |
[Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", |
|
296 |
Pretty.brk 1, prtT X]; |
|
11883 | 297 |
|
12081 | 298 |
fun prt_var (x, ~1) = prt_term (Syntax.free x) |
299 |
| prt_var xi = prt_term (Syntax.var xi); |
|
300 |
||
301 |
fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) |
|
302 |
| prt_varT xi = prt_typ (TVar (xi, [])); |
|
303 |
||
304 |
val prt_consts = prt_atoms (prt_term o Const) prt_typ; |
|
305 |
val prt_vars = prt_atoms prt_var prt_typ; |
|
306 |
val prt_varsT = prt_atoms prt_varT prt_sort; |
|
11883 | 307 |
|
308 |
||
12081 | 309 |
fun pretty_list _ _ [] = [] |
310 |
| pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; |
|
11883 | 311 |
|
12081 | 312 |
fun pretty_subgoal (n, A) = |
313 |
Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]); |
|
314 |
fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); |
|
11883 | 315 |
|
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
316 |
val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair prt_term); |
11883 | 317 |
|
12081 | 318 |
val pretty_consts = pretty_list "constants:" prt_consts o consts_of; |
319 |
val pretty_vars = pretty_list "variables:" prt_vars o vars_of; |
|
320 |
val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of; |
|
11883 | 321 |
|
322 |
||
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
323 |
val {prop, tpairs, ...} = rep_thm state; |
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
324 |
val (As, B) = Logic.strip_horn prop; |
12081 | 325 |
val ngoals = length As; |
11883 | 326 |
|
12081 | 327 |
fun pretty_gs (types, sorts) = |
328 |
(if main then [prt_term B] else []) @ |
|
329 |
(if ngoals = 0 then [Pretty.str "No subgoals!"] |
|
330 |
else if ngoals > maxgoals then |
|
331 |
pretty_subgoals (take (maxgoals, As)) @ |
|
332 |
(if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] |
|
333 |
else []) |
|
334 |
else pretty_subgoals As) @ |
|
335 |
pretty_ffpairs tpairs @ |
|
336 |
(if ! show_consts then pretty_consts prop else []) @ |
|
337 |
(if types then pretty_vars prop else []) @ |
|
338 |
(if sorts then pretty_varsT prop else []); |
|
339 |
in |
|
340 |
setmp show_no_free_types true |
|
341 |
(setmp show_types (! show_types orelse ! show_sorts) |
|
342 |
(setmp show_sorts false pretty_gs)) |
|
343 |
(! show_types orelse ! show_sorts, ! show_sorts) |
|
11883 | 344 |
end; |
345 |
||
12081 | 346 |
fun pretty_goals_marker bg n th = |
347 |
let val sg = Thm.sign_of_thm th in |
|
348 |
pretty_goals_aux (Sign.pretty_sort sg, Sign.pretty_typ sg, Sign.pretty_term sg) |
|
349 |
bg (true, true) n th |
|
350 |
end; |
|
351 |
||
352 |
val pretty_goals = pretty_goals_marker ""; |
|
12418 | 353 |
val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals_marker ""; |
12081 | 354 |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
355 |
end; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
356 |
|
11883 | 357 |
|
358 |
(* print_current_goals *) |
|
359 |
||
360 |
val current_goals_markers = ref ("", "", ""); |
|
361 |
||
12418 | 362 |
fun pretty_current_goals n m th = |
11883 | 363 |
let |
364 |
val ref (begin_state, end_state, begin_goal) = current_goals_markers; |
|
365 |
val ngoals = nprems_of th; |
|
366 |
in |
|
12418 | 367 |
(if begin_state = "" then [] else [Pretty.str begin_state]) @ |
368 |
[Pretty.str ("Level " ^ string_of_int n ^ |
|
11883 | 369 |
(if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ |
370 |
(if ngoals <> 1 then "s" else "") ^ ")" |
|
12418 | 371 |
else ""))] @ |
372 |
pretty_goals_marker begin_goal m th @ |
|
373 |
(if end_state = "" then [] else [Pretty.str end_state]) |
|
11883 | 374 |
end; |
375 |
||
12418 | 376 |
fun print_current_goals_default n m th = |
377 |
Pretty.writeln (Pretty.chunks (pretty_current_goals n m th)); |
|
378 |
||
11883 | 379 |
val print_current_goals_fn = ref print_current_goals_default; |
380 |
||
381 |
end; |
|
382 |
||
383 |
structure BasicDisplay: BASIC_DISPLAY = Display; |
|
384 |
open BasicDisplay; |