259 |> Variable.variant_frees ctxt [pred] |
259 |> Variable.variant_frees ctxt [pred] |
260 |> map Free |
260 |> map Free |
261 |> (curry list_comb) pred *} |
261 |> (curry list_comb) pred *} |
262 |
262 |
263 text {* |
263 text {* |
264 The point of this code is to extract the argument types of the given |
264 This code extracts the argument types of the given |
265 predicate and then generate for each type a distinct variable; finally it |
265 predicate and then generate for each type a distinct variable; finally it |
266 applies the generated variables to the predicate. You can read this off from |
266 applies the generated variables to the predicate. For example |
267 how the function is coded: in Line 2, the function @{ML fastype_of} |
267 |
268 calculates the type of the predicate; in Line 3, @{ML binder_types} produces |
268 @{ML_response_fake [display,gray] |
269 the list of argument types; Line 4 pairs up each type with the string (or name) |
269 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} |
270 @{text "z"}; the function @{ML variant_frees in Variable} generates for each |
270 |> Syntax.string_of_term @{context} |
271 @{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs |
271 |> warning" |
272 is turned into a list of variable terms in Line 6, which in the last line |
272 "P z za zb"} |
273 are applied by the function @{ML list_comb} to the predicate. We have to use |
273 |
274 the function @{ML curry}, because @{ML list_comb} expects the predicate and |
274 You can read this off this behaviour from how @{ML apply_fresh_args} is |
275 the argument list as a pair. |
275 coded: in Line 2, the function @{ML fastype_of} calculates the type of the |
276 |
276 predicate; in Line 3, @{ML binder_types} produces the list of argument |
|
277 types (in the case above the list @{text "[nat, int, unit]"}); Line 4 pairs up each |
|
278 type with the string @{text "z"}; the |
|
279 function @{ML variant_frees in Variable} generates for each @{text "z"} a |
|
280 unique name avoiding @{text pred}; the list of name-type pairs is turned |
|
281 into a list of variable terms in Line 6, which in the last line are applied |
|
282 by the function @{ML list_comb} to the predicate. We have to use the |
|
283 function @{ML curry}, because @{ML list_comb} expects the predicate and the |
|
284 argument list as a pair. |
277 |
285 |
278 The combinator @{ML "#>"} is the reverse function composition. It can be |
286 The combinator @{ML "#>"} is the reverse function composition. It can be |
279 used to define the following function |
287 used to define the following function |
280 *} |
288 *} |
281 |
289 |
459 statically at compile-time. However, this static linkage also limits their |
467 statically at compile-time. However, this static linkage also limits their |
460 usefulness in cases where data needs to be build up dynamically. In the |
468 usefulness in cases where data needs to be build up dynamically. In the |
461 course of this chapter you will learn more about these antiquotations: |
469 course of this chapter you will learn more about these antiquotations: |
462 they can simplify Isabelle programming since one can directly access all |
470 they can simplify Isabelle programming since one can directly access all |
463 kinds of logical elements from th ML-level. |
471 kinds of logical elements from th ML-level. |
|
472 *} |
|
473 |
|
474 text {* |
|
475 (FIXME: say something about @{text "@{binding \<dots>}"} |
464 *} |
476 *} |
465 |
477 |
466 section {* Terms and Types *} |
478 section {* Terms and Types *} |
467 |
479 |
468 text {* |
480 text {* |
581 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" |
593 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" |
582 "Const \<dots> $ |
594 "Const \<dots> $ |
583 Abs (\"x\", \<dots>, |
595 Abs (\"x\", \<dots>, |
584 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
596 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
585 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
597 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
|
598 |
|
599 (FIXME: handy functions for constructing terms @{ML list_comb}, @{ML lambda}) |
|
600 |
586 |
601 |
587 Although types of terms can often be inferred, there are many |
602 Although types of terms can often be inferred, there are many |
588 situations where you need to construct types manually, especially |
603 situations where you need to construct types manually, especially |
589 when defining constants. For example the function returning a function |
604 when defining constants. For example the function returning a function |
590 type is as follows: |
605 type is as follows: |