author  wenzelm 
Wed, 15 Mar 2000 18:20:52 +0100  
changeset 8458  883b28065841 
parent 8402  84ff2d1f9a2c 
child 8720  840c75ab2a7f 
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 

34 
val print_theory : theory > unit 

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 

4250  158 
(* print signature *) 
159 

160 
fun print_sign sg = 

161 
let 

162 
fun prt_cls c = Sign.pretty_sort sg [c]; 

163 
fun prt_sort S = Sign.pretty_sort sg S; 

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

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

166 

167 

168 
fun pretty_classes cs = Pretty.block 

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

170 

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

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

173 
Pretty.commas (map prt_cls cs)); 

174 

175 
fun pretty_default S = Pretty.block 

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

177 

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

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

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

183 

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

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

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

7635  188 

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

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

192 

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

194 

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

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

197 

198 
val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg; 

6846  199 
val spaces' = Library.sort_wrt fst spaces; 
7635  200 
val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} = 
4250  201 
Type.rep_tsig tsig; 
7067  202 
val tycons = Sign.cond_extern_table sg Sign.typeK type_tab; 
6846  203 
val consts = Sign.cond_extern_table sg Sign.constK const_tab; 
4250  204 
in 
205 
Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg)); 

4256  206 
Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data)); 
4782  207 
Pretty.writeln (Pretty.strs ["name prefix:", NameSpace.pack path]); 
4498  208 
Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces')); 
4250  209 
Pretty.writeln (pretty_classes classes); 
8402  210 
Pretty.writeln (Pretty.big_list "class relation:" 
211 
(map pretty_classrel (Symtab.dest classrel))); 

4250  212 
Pretty.writeln (pretty_default default); 
7635  213 
Pretty.writeln (pretty_log_types log_types); 
214 
Pretty.writeln (pretty_witness univ_witness); 

4250  215 
Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons)); 
7067  216 
Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs))); 
8402  217 
Pretty.writeln (Pretty.big_list "type arities:" 
218 
(flat (map pretty_arities (Symtab.dest arities)))); 

4250  219 
Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts)) 
220 
end; 

221 

222 

223 
(* print axioms, oracles, theorems *) 

224 

3811  225 
fun print_thy thy = 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

226 
let 
6390  227 
val {sign, axioms, oracles, ...} = Theory.rep_theory thy; 
6846  228 
fun cond_externs kind = Sign.cond_extern_table sign kind; 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

229 

3936  230 
fun prt_axm (a, t) = Pretty.block 
6846  231 
[Pretty.str (a ^ ":"), Pretty.brk 1, Pretty.quote (Sign.pretty_term sign t)]; 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

232 
in 
6846  233 
Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm (cond_externs Theory.axiomK axioms))); 
234 
Pretty.writeln (Pretty.strs ("oracles:" :: (map #1 (cond_externs Theory.oracleK oracles)))) 

1591
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 

6390  237 
fun print_theory thy = (print_sign (Theory.sign_of thy); print_thy thy); 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

238 

4250  239 
(*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

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

241 

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

242 

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

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

244 

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

245 
open Display; 