71 @{ML_response_fake [display] "warning \"any string\"" "\"any string\""} |
71 @{ML_response_fake [display] "warning \"any string\"" "\"any string\""} |
72 |
72 |
73 will print out @{text [quotes] "any string"} inside the response buffer |
73 will print out @{text [quotes] "any string"} inside the response buffer |
74 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
74 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
75 then there is a convenient, though again ``quick-and-dirty'', method for |
75 then there is a convenient, though again ``quick-and-dirty'', method for |
76 converting values into strings, for example: |
76 converting values into strings, namely @{ML makestring}: |
77 |
77 |
78 @{ML_response_fake [display] "warning (makestring 1)" "\"1\""} |
78 @{ML_response_fake [display] "warning (makestring 1)" "\"1\""} |
79 |
79 |
80 However this only works if the type of what is converted is monomorphic and is not |
80 However @{ML makestring} only works if the type of what is converted is monomorphic |
81 a function. |
81 and is not a function. |
82 |
82 |
83 The function @{ML "warning"} should only be used for testing purposes, because any |
83 The function @{ML "warning"} should only be used for testing purposes, because any |
84 output this function generates will be overwritten as soon as an error is |
84 output this function generates will be overwritten as soon as an error is |
85 raised. For printing anything more serious and elaborate, the |
85 raised. For printing anything more serious and elaborate, the |
86 function @{ML tracing} is more appropriate. This function writes all output into |
86 function @{ML tracing} is more appropriate. This function writes all output into |
87 a separate tracing buffer. For example |
87 a separate tracing buffer. For example |
88 |
88 |
89 @{ML_response_fake [display] "tracing \"foo\"" "\"foo\""} |
89 @{ML_response_fake [display] "tracing \"foo\"" "\"foo\""} |
90 |
90 |
91 It is also possible to redirect the ``channel'' where the string @{text "foo"} is |
91 It is also possible to redirect the ``channel'' where the string @{text "foo"} is |
92 printed to a separate file, e.g. to prevent Proof General from choking on massive |
92 printed to a separate file, e.g. to prevent ProofGeneral from choking on massive |
93 amounts of trace output. This redirection can be achieved using the code |
93 amounts of trace output. This redirection can be achieved using the code |
94 *} |
94 *} |
95 |
95 |
96 ML{* |
96 ML{* |
97 val strip_specials = |
97 val strip_specials = |
226 |
226 |
227 The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, |
227 The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, |
228 inserting the invisible @{text "Trueprop"}-coercions whenever necessary. |
228 inserting the invisible @{text "Trueprop"}-coercions whenever necessary. |
229 Consider for example |
229 Consider for example |
230 |
230 |
231 @{ML_response [display] "@{term \"P x\"}" "Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)"} |
231 @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>), |
232 @{ML_response [display] "@{prop \"P x\"}" |
232 Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"} |
233 "Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>))"} |
233 |
234 |
234 which inserts the coercion in the second component and |
235 which inserts the coercion in the latter case and |
235 |
236 |
236 @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
237 @{ML_response [display] "@{term \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"} |
237 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"} |
238 @{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"} |
|
239 |
238 |
240 which does not (since it is already constructed using the meta-implication). |
239 which does not (since it is already constructed using the meta-implication). |
241 |
240 |
242 Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example |
241 Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example |
243 |
242 |
253 section {* Constructing Terms and Types Manually *} |
252 section {* Constructing Terms and Types Manually *} |
254 |
253 |
255 text {* |
254 text {* |
256 |
255 |
257 While antiquotations are very convenient for constructing terms and types, |
256 While antiquotations are very convenient for constructing terms and types, |
258 they can only construct fixed terms. Unfortunately, one often needs to construct terms |
257 they can only construct fixed terms (remember they are ``linked'' at compile-time). |
|
258 However, one often needs to construct terms |
259 dynamically. For example, a function that returns the implication |
259 dynamically. For example, a function that returns the implication |
260 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"} |
260 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"} |
261 as arguments can only be written as |
261 as arguments can only be written as |
262 *} |
262 *} |
263 |
263 |
264 ML {* |
264 ML {* |
265 fun make_imp P Q tau = |
265 fun make_imp P Q tau = |
266 let |
266 let |
267 val x = Free ("x",tau) |
267 val x = Free ("x",tau) |
268 in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), |
268 in Logic.all x (Logic.mk_implies (P $ x, Q $ x)) |
269 HOLogic.mk_Trueprop (Q $ x))) |
|
270 end |
269 end |
271 *} |
270 *} |
272 |
271 |
273 text {* |
272 text {* |
274 |
273 |
275 The reason is that one cannot pass the arguments @{term P}, @{term Q} and |
274 The reason is that one cannot pass the arguments @{term P}, @{term Q} and |
276 @{term "tau"} into an antiquotation. For example the following does not work as |
275 @{term "tau"} into an antiquotation. For example the following does \emph{not} work: |
277 expected. |
|
278 *} |
276 *} |
279 |
277 |
280 ML {* |
278 ML {* |
281 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} |
279 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} |
282 *} |
280 *} |
283 |
281 |
284 text {* |
282 text {* |
285 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
283 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
286 to both functions. |
284 to both functions: |
|
285 |
|
286 @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" |
|
287 "Const \<dots> $ |
|
288 Abs (\"x\", Type (\"nat\",[]), |
|
289 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ |
|
290 (Free (\"T\",\<dots>) $ \<dots>))"} |
|
291 @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" |
|
292 "Const \<dots> $ |
|
293 Abs (\"x\", \<dots>, |
|
294 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
|
295 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
|
296 |
|
297 As can be seen, in the first case the arguments are correctly used, while in the |
|
298 second the @{term "P"} and @{text "Q"} from the antiquotation. |
287 |
299 |
288 One tricky point in constructing terms by hand is to obtain the |
300 One tricky point in constructing terms by hand is to obtain the |
289 fully qualified name for constants. For example the names for @{text "zero"} and |
301 fully qualified name for constants. For example the names for @{text "zero"} and |
290 @{text "+"} are more complex than one first expects, namely |
302 @{text "+"} are more complex than one first expects, namely |
291 |
303 |