author  wenzelm 
Tue, 12 Jan 1999 13:14:22 +0100  
changeset 6087  c8ec08fced15 
parent 5902  c39b23d752b6 
child 6279  eb4dc43023af 
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 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

13 
val pretty_thm : thm > Pretty.T 
6087  14 
val pretty_thms : thm list > Pretty.T 
4950  15 
val string_of_thm : thm > string 
16 
val pprint_thm : thm > pprint_args > unit 

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

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

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

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

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

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

27 
val pprint_cterm : cterm > pprint_args > unit 

28 
val string_of_cterm : cterm > string 

29 
val print_cterm : cterm > unit 

30 
val pretty_theory : theory > Pretty.T 

31 
val pprint_theory : theory > pprint_args > unit 

32 
val print_syntax : theory > unit 

33 
val print_theory : theory > unit 

34 
val pretty_name_space : string * NameSpace.T > Pretty.T 

35 
val show_consts : bool ref 

36 
end; 

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

37 

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

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

40 

6087  41 
(** print thm **) 
42 

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

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

45 

46 
fun pretty_tag (name, args) = Pretty.strs (name :: args); 

47 
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

48 

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

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

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

51 
val {sign, hyps, prop, ...} = rep_thm th; 
6087  52 
val xshyps = Thm.extra_shyps th; 
53 
val (_, tags) = Thm.get_name_tags th; 

54 

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

55 
val hlen = length xshyps + length hyps; 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

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

57 
if hlen = 0 then [] 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

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

59 
[Pretty.brk 2, Pretty.list "[" "]" 
3785  60 
(map (Sign.pretty_term sign) hyps @ 
61 
map (Sign.pretty_sort sign) xshyps)] 

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

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

63 
[Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")]; 
6087  64 
val tsymbs = 
65 
if null tags orelse not (! show_tags) then [] 

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

67 
in Pretty.block (Sign.pretty_term sign prop :: (hsymbs @ tsymbs)) end; 

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

68 

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

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

70 
val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm; 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

71 

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

74 

6087  75 

76 
(* toplevel commands for printing theorems *) 

77 

78 
val print_thm = Pretty.writeln o pretty_thm; 

79 
val print_thms = Pretty.writeln o pretty_thms; 

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

80 

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

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

82 

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

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

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

86 

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

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

89 

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

90 

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

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

92 

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

95 

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

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

97 
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

98 

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

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

100 
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

101 

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

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

103 

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

106 

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

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

108 
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

109 

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

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

111 
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

112 

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

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

114 

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

115 

4250  116 

117 
(** print theory **) 

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

118 

4950  119 
val pretty_theory = Sign.pretty_sg o sign_of; 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

120 
val pprint_theory = Sign.pprint_sg o sign_of; 
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 
val print_syntax = Syntax.print_syntax o syn_of; 
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

123 

4250  124 

4498  125 
(* pretty_name_space *) 
126 

127 
fun pretty_name_space (kind, space) = 

128 
let 

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

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

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

132 
in 

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

134 
> Pretty.block 

135 
end; 

136 

137 

138 

4250  139 
(* print signature *) 
140 

141 
fun print_sign sg = 

142 
let 

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

144 
fun prt_sort S = Sign.pretty_sort sg S; 

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

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

147 

148 
val ext_class = Sign.cond_extern sg Sign.classK; 

149 
val ext_tycon = Sign.cond_extern sg Sign.typeK; 

150 
val ext_const = Sign.cond_extern sg Sign.constK; 

151 

152 

153 
fun pretty_classes cs = Pretty.block 

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

155 

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

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

158 
Pretty.commas (map prt_cls cs)); 

159 

160 
fun pretty_default S = Pretty.block 

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

162 

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

5902  164 
[Pretty.str (ext_tycon t), Pretty.spc 1, Pretty.str (string_of_int n)]; 
4250  165 

166 
fun pretty_abbr (t, (vs, rhs)) = Pretty.block 

167 
[prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)), 

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

169 

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

171 

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

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

174 

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

4440  176 
val spaces' = sort_wrt fst spaces; 
4250  177 
val {classes, classrel, default, tycons, abbrs, arities} = 
178 
Type.rep_tsig tsig; 

179 
val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab)); 

180 
in 

181 
Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg)); 

4256  182 
Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data)); 
4782  183 
Pretty.writeln (Pretty.strs ["name prefix:", NameSpace.pack path]); 
4498  184 
Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces')); 
4250  185 
Pretty.writeln (pretty_classes classes); 
186 
Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel)); 

187 
Pretty.writeln (pretty_default default); 

188 
Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons)); 

189 
Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs)); 

190 
Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities arities))); 

191 
Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts)) 

192 
end; 

193 

194 

195 
(* print axioms, oracles, theorems *) 

196 

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

198 
let 
3990  199 
val {sign, axioms, oracles, ...} = rep_theory thy; 
200 
val axioms = Symtab.dest axioms; 

3811  201 
val oras = map fst (Symtab.dest oracles); 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

202 

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

206 
in 
3990  207 
Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm axioms)); 
4993  208 
Pretty.writeln (Pretty.strs ("oracles:" :: oras)) 
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset

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

210 

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

212 

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

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

215 

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

216 

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

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

218 

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

219 
open Display; 