author  wenzelm 
Mon, 17 Apr 2000 13:57:55 +0200  
changeset 8720  840c75ab2a7f 
parent 8458  883b28065841 
child 8908  25f2bdc02123 
permissions  rwrr 
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 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

9 
signature DISPLAY = 
4950  10 
sig 
11 
val show_hyps : bool ref 

6087  12 
val show_tags : bool ref 
6976  13 
val pretty_thm_no_quote: thm > Pretty.T 
6926  14 
val pretty_thm : thm > Pretty.T 
6087  15 
val pretty_thms : thm list > Pretty.T 
4950  16 
val string_of_thm : thm > string 
17 
val pprint_thm : thm > pprint_args > unit 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

18 
val print_thm : thm > unit 
6087  19 
val print_thms : thm list > unit 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

20 
val prth : thm > thm 
4270  21 
val prthq : thm Seq.seq > thm Seq.seq 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

22 
val prths : thm list > thm list 
4950  23 
val pretty_ctyp : ctyp > Pretty.T 
24 
val pprint_ctyp : ctyp > pprint_args > unit 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

25 
val string_of_ctyp : ctyp > string 
4950  26 
val print_ctyp : ctyp > unit 
27 
val pretty_cterm : cterm > Pretty.T 

28 
val pprint_cterm : cterm > pprint_args > unit 

29 
val string_of_cterm : cterm > string 

30 
val print_cterm : cterm > unit 

31 
val pretty_theory : theory > Pretty.T 

32 
val pprint_theory : theory > pprint_args > unit 

33 
val print_syntax : theory > unit 

8720  34 
val pretty_full_theory: theory > Pretty.T list 
4950  35 
val pretty_name_space : string * NameSpace.T > Pretty.T 
36 
val show_consts : bool ref 

37 
end; 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

38 

4950  39 
structure Display: DISPLAY = 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

40 
struct 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

41 

6087  42 
(** print thm **) 
43 

44 
val show_hyps = ref true; (*false: print metahypotheses as dots*) 

45 
val show_tags = ref false; (*false: suppress tags*) 

46 

6889  47 
local 
48 

8402  49 
fun pretty_tag (name, args) = Pretty.strs (name :: map quote args); 
6087  50 
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

51 

6889  52 
fun is_oracle (Thm.Oracle _) = true 
53 
 is_oracle _ = false; 

54 

55 
fun ex_oracle (Join (der, ders)) = is_oracle der orelse exists ex_oracle ders; 

56 

6314  57 
fun pretty_thm_aux quote th = 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

58 
let 
6889  59 
val {sign, hyps, prop, der, ...} = rep_thm th; 
6087  60 
val xshyps = Thm.extra_shyps th; 
61 
val (_, tags) = Thm.get_name_tags th; 

62 

6314  63 
val prt_term = (if quote then Pretty.quote else I) o Sign.pretty_term sign; 
6279  64 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

65 
val hlen = length xshyps + length hyps; 
6894  66 
val ex_ora = ex_oracle der; 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

67 
val hsymbs = 
6894  68 
if hlen = 0 andalso not ex_ora then [] 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

69 
else if ! show_hyps then 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

70 
[Pretty.brk 2, Pretty.list "[" "]" 
6889  71 
(map prt_term hyps @ map (Sign.pretty_sort sign) xshyps @ 
6894  72 
(if ex_ora then [Pretty.str "!"] else []))] 
6889  73 
else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ 
6894  74 
(if ex_ora then "!" else "") ^ "]")]; 
6087  75 
val tsymbs = 
76 
if null tags orelse not (! show_tags) then [] 

77 
else [Pretty.brk 1, pretty_tags tags]; 

6279  78 
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

79 

6889  80 
in 
81 

6926  82 
val pretty_thm = pretty_thm_aux true; 
6314  83 
val pretty_thm_no_quote = pretty_thm_aux false; 
84 

6889  85 
end; 
86 

87 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

88 
val string_of_thm = Pretty.string_of o pretty_thm; 
6279  89 
val pprint_thm = Pretty.pprint o pretty_thm; 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

90 

6087  91 
fun pretty_thms [th] = pretty_thm th 
92 
 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

93 

6087  94 

95 
(* toplevel commands for printing theorems *) 

96 

97 
val print_thm = Pretty.writeln o pretty_thm; 

98 
val print_thms = Pretty.writeln o pretty_thms; 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

99 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

100 
fun prth th = (print_thm th; th); 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

101 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

102 
(*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

103 
fun prthq thseq = 
4270  104 
(Seq.print (fn _ => print_thm) 100000 thseq; thseq); 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

105 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

106 
(*Print and return a list of theorems, separated by blank lines. *) 
4210  107 
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

108 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

109 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

110 
(* other printing commands *) 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

111 

4126  112 
fun pretty_ctyp cT = 
113 
let val {sign, T} = rep_ctyp cT in Sign.pretty_typ sign T end; 

114 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

115 
fun pprint_ctyp cT = 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

116 
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

117 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

118 
fun string_of_ctyp cT = 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

119 
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

120 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

121 
val print_ctyp = writeln o string_of_ctyp; 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

122 

3547  123 
fun pretty_cterm ct = 
124 
let val {sign, t, ...} = rep_cterm ct in Sign.pretty_term sign t end; 

125 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

126 
fun pprint_cterm ct = 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

127 
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

128 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

129 
fun string_of_cterm ct = 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

130 
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

131 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

132 
val print_cterm = writeln o string_of_cterm; 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

133 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

134 

4250  135 

136 
(** print theory **) 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

137 

6390  138 
val pretty_theory = Sign.pretty_sg o Theory.sign_of; 
139 
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

140 

6390  141 
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

142 

4250  143 

4498  144 
(* pretty_name_space *) 
145 

146 
fun pretty_name_space (kind, space) = 

147 
let 

148 
fun prt_entry (name, accs) = Pretty.block 

149 
(Pretty.str (quote name ^ " =") :: Pretty.brk 1 :: 

150 
Pretty.commas (map (Pretty.str o quote) accs)); 

151 
in 

152 
Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space)) 

153 
> Pretty.block 

154 
end; 

155 

156 

157 

8720  158 
(* print theory *) 
4250  159 

8720  160 
fun pretty_full_theory thy = 
4250  161 
let 
8720  162 
val sg = Theory.sign_of thy; 
163 

4250  164 
fun prt_cls c = Sign.pretty_sort sg [c]; 
165 
fun prt_sort S = Sign.pretty_sort sg S; 

166 
fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]); 

167 
fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty); 

8720  168 
fun prt_term t = Pretty.quote (Sign.pretty_term sg t); 
4250  169 

170 
fun pretty_classes cs = Pretty.block 

171 
(Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs)); 

172 

173 
fun pretty_classrel (c, cs) = Pretty.block 

174 
(prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: 

175 
Pretty.commas (map prt_cls cs)); 

176 

177 
fun pretty_default S = Pretty.block 

178 
[Pretty.str "default:", Pretty.brk 1, prt_sort S]; 

179 

180 
fun pretty_ty (t, n) = Pretty.block 

8458  181 
[Pretty.str t, Pretty.brk 1, Pretty.str (string_of_int n)]; 
4250  182 

7635  183 
fun pretty_log_types ts = Pretty.block 
184 
(Pretty.breaks (Pretty.str "logical types:" :: map Pretty.str ts)); 

185 

186 
fun pretty_witness None = Pretty.str "universal nonemptiness witness: " 

187 
 pretty_witness (Some (T, S)) = Pretty.block 

8402  188 
[Pretty.str "universal nonemptiness witness:", Pretty.brk 1, prt_typ T, 
189 
Pretty.brk 1, prt_sort S]; 

7635  190 

4250  191 
fun pretty_abbr (t, (vs, rhs)) = Pretty.block 
192 
[prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)), 

193 
Pretty.str " =", Pretty.brk 1, prt_typ rhs]; 

194 

195 
fun pretty_arities (t, ars) = map (prt_arity t) ars; 

196 

197 
fun pretty_const (c, ty) = Pretty.block 

198 
[Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty]; 

199 

8720  200 
fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; 
201 

202 

4250  203 
val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg; 
8720  204 
val {axioms, oracles, ...} = Theory.rep_theory thy; 
6846  205 
val spaces' = Library.sort_wrt fst spaces; 
7635  206 
val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} = 
4250  207 
Type.rep_tsig tsig; 
7067  208 
val tycons = Sign.cond_extern_table sg Sign.typeK type_tab; 
6846  209 
val consts = Sign.cond_extern_table sg Sign.constK const_tab; 
8720  210 
val axms = Sign.cond_extern_table sg Theory.axiomK axioms; 
211 
val oras = Sign.cond_extern_table sg Theory.oracleK oracles; 

4250  212 
in 
8720  213 
[Pretty.strs ("stamps:" :: Sign.stamp_names_of sg), 
214 
Pretty.strs ("data:" :: Sign.data_kinds data), 

215 
Pretty.strs ["name prefix:", NameSpace.pack path], 

216 
Pretty.big_list "name spaces:" (map pretty_name_space spaces'), 

217 
pretty_classes classes, 

218 
Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)), 

219 
pretty_default default, 

220 
pretty_log_types log_types, 

221 
pretty_witness univ_witness, 

222 
Pretty.big_list "type constructors:" (map pretty_ty tycons), 

223 
Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)), 

224 
Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))), 

225 
Pretty.big_list "consts:" (map pretty_const consts), 

226 
Pretty.big_list "axioms:" (map prt_axm axms), 

227 
Pretty.strs ("oracles:" :: (map #1 oras))] 

4250  228 
end; 
229 

230 

231 
(*also show consts in case of showing types?*) 

3851
fe9932a7cd46
print_goals: optional output of const types (set show_consts);
wenzelm
parents:
3811
diff
changeset

232 
val show_consts = ref false; 
fe9932a7cd46
print_goals: optional output of const types (set show_consts);
wenzelm
parents:
3811
diff
changeset

233 

1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

234 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

235 
end; 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

236 

7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

237 
open Display; 