246 text {* |
246 text {* |
247 Another reason why the let-bindings in the code above are better to be |
247 Another reason why the let-bindings in the code above are better to be |
248 avoided: it is more than easy to get the intermediate values wrong, not to |
248 avoided: it is more than easy to get the intermediate values wrong, not to |
249 mention the nightmares the maintenance of this code causes! |
249 mention the nightmares the maintenance of this code causes! |
250 |
250 |
251 |
251 A ``real world'' example for a function written in the waterfall fashion might |
252 (FIXME: give a real world example involving theories) |
252 be the following: |
253 |
253 *} |
254 Similarly, the combinator @{ML "#>"} is the reverse function |
254 |
255 composition. It can be used to define the following function |
255 ML %linenosgray{*fun apply_fresh_args pred ctxt = |
|
256 pred |> fastype_of |
|
257 |> binder_types |
|
258 |> map (pair "z") |
|
259 |> Variable.variant_frees ctxt [pred] |
|
260 |> map Free |
|
261 |> (curry list_comb) pred *} |
|
262 |
|
263 text {* |
|
264 The point of this function is to extract the argument types of the given |
|
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 |
|
267 how the function is coded: in Line 2, the function @{ML fastype_of} |
|
268 calculates the type of the predicate; in Line 3, @{ML binder_types} produces |
|
269 the list of argument types; Line 4 pairs up each type with the string/name |
|
270 @{text "z"}; the function @{ML variant_frees in Variable} generates for each |
|
271 @{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs |
|
272 is turned into a list of variable terms in Line 6, which in the last line |
|
273 are applied by the function @{ML list_comb} to the predicate. We have to use |
|
274 the function @{ML curry}, because @{ML list_comb} expects the predicate and |
|
275 the argument list as a pair. |
|
276 |
|
277 |
|
278 The combinator @{ML "#>"} is the reverse function composition. It can be |
|
279 used to define the following function |
256 *} |
280 *} |
257 |
281 |
258 ML{*val inc_by_six = |
282 ML{*val inc_by_six = |
259 (fn x => x + 1) |
283 (fn x => x + 1) |
260 #> (fn x => x + 2) |
284 #> (fn x => x + 2) |
798 also returns the type of a term. |
822 also returns the type of a term. |
799 |
823 |
800 @{ML_response [display,gray] |
824 @{ML_response [display,gray] |
801 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
825 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
802 |
826 |
803 However, efficiency is gained on the expense of skiping some tests. You |
827 However, efficiency is gained on the expense of skipping some tests. You |
804 can see this in the following example |
828 can see this in the following example |
805 |
829 |
806 @{ML_response [display,gray] |
830 @{ML_response [display,gray] |
807 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"} |
831 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"} |
808 |
832 |
942 |
966 |
943 Before we can use the attribute, we need to set it up. This can be done |
967 Before we can use the attribute, we need to set it up. This can be done |
944 using the function @{ML Attrib.add_attributes} as follows. |
968 using the function @{ML Attrib.add_attributes} as follows. |
945 *} |
969 *} |
946 |
970 |
947 setup {* |
971 setup %gray {* Attrib.add_attributes |
948 Attrib.add_attributes |
|
949 [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *} |
972 [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *} |
950 |
973 |
951 text {* |
974 text {* |
952 The attribute does not expect any further arguments (unlike @{text "[OF |
975 The attribute does not expect any further arguments (unlike @{text "[OF |
953 \<dots>]"}, for example, which can take a list of theorems as argument). Therefore |
976 \<dots>]"}, for example, which can take a list of theorems as argument). Therefore |
1010 |
1033 |
1011 text {* |
1034 text {* |
1012 and set up the attributes as follows |
1035 and set up the attributes as follows |
1013 *} |
1036 *} |
1014 |
1037 |
1015 setup {* |
1038 setup %gray {* Attrib.add_attributes |
1016 Attrib.add_attributes |
1039 [("my_thms", Attrib.add_del_args my_add my_del, |
1017 [("my_thms", Attrib.add_del_args my_add my_del, |
1040 "maintaining a list of my_thms")] *} |
1018 "maintaining a list of my_thms")] *} |
|
1019 |
1041 |
1020 text {* |
1042 text {* |
1021 Now if you prove the lemma attaching the attribute @{text "[my_thms]"} |
1043 Now if you prove the lemma attaching the attribute @{text "[my_thms]"} |
1022 *} |
1044 *} |
1023 |
1045 |
1092 |
1114 |
1093 text {* |
1115 text {* |
1094 and set up the @{ML_struct FooRules} with the command |
1116 and set up the @{ML_struct FooRules} with the command |
1095 *} |
1117 *} |
1096 |
1118 |
1097 setup {* FooRules.setup *} |
1119 setup %gray {* FooRules.setup *} |
1098 |
1120 |
1099 text {* |
1121 text {* |
1100 This code declares a data slot where the theorems are stored, |
1122 This code declares a data slot where the theorems are stored, |
1101 an attribute @{text foo} (with the @{text add} and @{text del} options |
1123 an attribute @{text foo} (with the @{text add} and @{text del} options |
1102 for adding and deleting theorems) and an internal ML interface to retrieve and |
1124 for adding and deleting theorems) and an internal ML interface to retrieve and |