172 | TVar of indexname * sort *} |
172 | TVar of indexname * sort *} |
173 |
173 |
174 text {* |
174 text {* |
175 Like with terms, there is the distinction between free type |
175 Like with terms, there is the distinction between free type |
176 variables (term-constructor @{ML "TFree"}) and schematic |
176 variables (term-constructor @{ML "TFree"}) and schematic |
177 type variables (term-constructor @{ML "TVar"}). A type constant, |
177 type variables (term-constructor @{ML "TVar"} and printed with |
|
178 a leading question mark). A type constant, |
178 like @{typ "int"} or @{typ bool}, are types with an empty list |
179 like @{typ "int"} or @{typ bool}, are types with an empty list |
179 of argument types. However, it is a bit difficult to show an |
180 of argument types. However, it needs a bit of effort to show an |
180 example, because Isabelle always pretty-prints types (unlike terms). |
181 example, because Isabelle always pretty prints types (unlike terms). |
181 Here is a contrived example: |
182 Using just the antiquotation @{text "@{typ \"bool\"}"} we only see |
182 |
183 |
183 @{ML_response [display, gray] |
184 @{ML_response [display, gray] |
184 "if Type (\"bool\", []) = @{typ \"bool\"} then true else false" |
185 "@{typ \"bool\"}" |
185 "true"} |
186 "bool"} |
|
187 |
|
188 the pretty printed version of @{text "bool"}. However, in PolyML it is |
|
189 easy to install your own pretty printer. With the function below we |
|
190 mimic the behaviour of the usual pretty printer for |
|
191 datatypes.\footnote{Thanks to David Matthews for providing this |
|
192 code.} |
|
193 *} |
|
194 |
|
195 ML{*fun typ_raw_pretty_printer depth _ ty = |
|
196 let |
|
197 fun cond str a = |
|
198 if depth <= 0 |
|
199 then PolyML.PrettyString "..." |
|
200 else PolyML.PrettyBlock(1, false, [], |
|
201 [PolyML.PrettyString str, PolyML.PrettyBreak(1, 0), a]) |
|
202 in |
|
203 case ty of |
|
204 Type a => cond "Type" (PolyML.prettyRepresentation(a, depth - 1)) |
|
205 | TFree a => cond "TFree" (PolyML.prettyRepresentation(a, depth - 1)) |
|
206 | TVar a => cond "TVar" (PolyML.prettyRepresentation(a, depth - 1)) |
|
207 end*} |
|
208 |
|
209 text {* |
|
210 We can install this pretty printer with the function |
|
211 @{ML_ind addPrettyPrinter in PolyML} as follows. |
|
212 *} |
|
213 |
|
214 ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*} |
|
215 |
|
216 text {* |
|
217 Now the type bool is printed out as expected. |
|
218 |
|
219 @{ML_response [display,gray] |
|
220 "@{typ \"bool\"}" |
|
221 "Type (\"bool\", [])"} |
|
222 |
|
223 When printing out a list-type |
|
224 |
|
225 @{ML_response [display,gray] |
|
226 "@{typ \"'a list\"}" |
|
227 "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"} |
|
228 |
|
229 we can see the full name of the type is actually @{text "List.list"}, indicating |
|
230 that it is defined in the theory @{text "List"}. However, one has to be |
|
231 careful with finding out the right name of a type, because even if |
|
232 @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the |
|
233 theories @{text "HOL"} and @{text "Nat"}, respectively, they are |
|
234 still represented by their simple name. |
|
235 |
|
236 @{ML_response [display,gray] |
|
237 "@{typ \"bool \<Rightarrow> nat\"}" |
|
238 "Type (\"fun\", [Type (\"bool\", []), Type (\"nat\", [])])"} |
|
239 |
|
240 We can restore the usual behaviour of Isabelle's pretty printer |
|
241 with the code |
|
242 *} |
|
243 |
|
244 ML{*fun stnd_pretty_printer _ _ = |
|
245 ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy; |
|
246 |
|
247 PolyML.addPrettyPrinter stnd_pretty_printer*} |
|
248 |
|
249 text {* |
|
250 After that the types for booleans, lists and so on are printed out again |
|
251 the standard Isabelle way. |
|
252 |
|
253 @{ML_response_fake [display, gray] |
|
254 "@{typ \"bool\"}; |
|
255 @{typ \"'a list\"}" |
|
256 "\"bool\" |
|
257 \"'a List.list\""} |
186 |
258 |
187 \begin{readmore} |
259 \begin{readmore} |
188 Types are described in detail in \isccite{sec:types}. Their |
260 Types are described in detail in \isccite{sec:types}. Their |
189 definition and many useful operations are implemented |
261 definition and many useful operations are implemented |
190 in @{ML_file "Pure/type.ML"}. |
262 in @{ML_file "Pure/type.ML"}. |
1117 "Thm.get_tags @{thm foo_data}" |
1189 "Thm.get_tags @{thm foo_data}" |
1118 "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"} |
1190 "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"} |
1119 |
1191 |
1120 consisting of a name and a kind. When we store lemmas in the theorem database, |
1192 consisting of a name and a kind. When we store lemmas in the theorem database, |
1121 we might want to explicitly extend this data by attaching case names to the |
1193 we might want to explicitly extend this data by attaching case names to the |
1122 two premises of the lemma. This can be done with the function @{ML_ind name in RuleCases} |
1194 two premises of the lemma. This can be done with the function @{ML_ind name in Rule_Cases} |
1123 from the structure @{ML_struct RuleCases}. |
1195 from the structure @{ML_struct Rule_Cases}. |
1124 *} |
1196 *} |
1125 |
1197 |
1126 local_setup %gray {* |
1198 local_setup %gray {* |
1127 LocalTheory.note Thm.lemmaK |
1199 LocalTheory.note Thm.lemmaK |
1128 ((@{binding "foo_data'"}, []), |
1200 ((@{binding "foo_data'"}, []), |
1129 [(RuleCases.name ["foo_case_one", "foo_case_two"] |
1201 [(Rule_Cases.name ["foo_case_one", "foo_case_two"] |
1130 @{thm foo_data})]) #> snd *} |
1202 @{thm foo_data})]) #> snd *} |
1131 |
1203 |
1132 text {* |
1204 text {* |
1133 The data of the theorem @{thm [source] foo_data'} is then as follows: |
1205 The data of the theorem @{thm [source] foo_data'} is then as follows: |
1134 |
1206 |