273 "(1::nat, x::'a)"} |
273 "(1::nat, x::'a)"} |
274 |
274 |
275 where @{text 1} and @{text x} are displayed with their inferred type. |
275 where @{text 1} and @{text x} are displayed with their inferred type. |
276 Even more type information can be printed by setting |
276 Even more type information can be printed by setting |
277 the reference @{ML_ind show_all_types in Syntax} to @{ML true}. |
277 the reference @{ML_ind show_all_types in Syntax} to @{ML true}. |
278 We obtain then |
278 In this case we obtain |
279 *} |
279 *} |
280 (*<*)ML %linenos {*show_all_types := true*} |
280 (*<*)ML %linenos {*show_all_types := true*} |
281 (*>*) |
281 (*>*) |
282 text {* |
282 text {* |
283 @{ML_response_fake [display, gray] |
283 @{ML_response_fake [display, gray] |
284 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" |
284 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" |
285 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
285 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
286 |
286 |
287 where @{term Pair} is the term-constructor for products. |
287 where @{term Pair} is the term-constructor for products. |
288 Other references that influence printing are @{ML_ind show_brackets in Syntax} |
288 Other references that influence printing of terms are |
289 and @{ML_ind show_sorts in Syntax}. |
289 @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. |
290 *} |
290 *} |
291 (*<*)ML %linenos {*show_types := false; show_all_types := false*} |
291 (*<*)ML %linenos {*show_types := false; show_all_types := false*} |
292 (*>*) |
292 (*>*) |
293 text {* |
293 text {* |
294 A @{ML_type cterm} can be transformed into a string by the following function. |
294 A @{ML_type cterm} can be transformed into a string by the following function. |
772 \footnote{\bf FIXME: find a good exercise for combinators} |
772 \footnote{\bf FIXME: find a good exercise for combinators} |
773 \footnote{\bf FIXME: say something about calling conventions} |
773 \footnote{\bf FIXME: say something about calling conventions} |
774 *} |
774 *} |
775 |
775 |
776 |
776 |
777 section {* ML-Antiquotations *} |
777 section {* ML-Antiquotations\label{sec:antiquote} *} |
778 |
778 |
779 text {* |
779 text {* |
780 Recall from Section \ref{sec:include} that code in Isabelle is always |
780 Recall from Section \ref{sec:include} that code in Isabelle is always |
781 embedded in a theory. The main advantage of this is that the code can |
781 embedded in a theory. The main advantage of this is that the code can |
782 contain references to entities defined on the logical level of Isabelle. By |
782 contain references to entities defined on the logical level of Isabelle. By |
843 *} |
843 *} |
844 |
844 |
845 ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *} |
845 ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *} |
846 |
846 |
847 text {* |
847 text {* |
848 which can be printed out as follows |
848 The result can be printed out as follows. |
849 |
849 |
850 @{ML_response_fake [gray,display] |
850 @{ML_response_fake [gray,display] |
851 "foo_thm |> string_of_thms @{context} |
851 "foo_thm |> string_of_thms @{context} |
852 |> tracing" |
852 |> tracing" |
853 "True, True"} |
853 "True, True"} |
854 |
854 |
855 You can also refer to the current simpset via an antiquotation. To illustrate |
855 You can also refer to the current simpset via an antiquotation. To illustrate |
856 this we implement the function that extracts the theorem names stored in a |
856 this we implement the function that extracts the theorem names stored in a |
857 simpset. |
857 simpset. |
947 |
947 |
948 @{ML_response_fake [display,gray] |
948 @{ML_response_fake [display,gray] |
949 "@{term_pat \"Suc (?x::nat)\"}" |
949 "@{term_pat \"Suc (?x::nat)\"}" |
950 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"} |
950 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"} |
951 |
951 |
952 which shows the internal representation of the term @{text "Suc ?x"}. |
952 which shows the internal representation of the term @{text "Suc ?x"}. Similarly |
953 |
953 we can write an antiquotation for type patterns. |
|
954 *} |
|
955 |
|
956 ML %linenosgray{*let |
|
957 val parser = Args.context -- Scan.lift Args.name_source |
|
958 |
|
959 fun typ_pat (ctxt, str) = |
|
960 str |> Syntax.parse_typ ctxt |
|
961 |> ML_Syntax.print_typ |
|
962 |> ML_Syntax.atomic |
|
963 in |
|
964 ML_Antiquote.inline "typ_pat" (parser >> typ_pat) |
|
965 end*} |
|
966 |
|
967 text {* |
954 \begin{readmore} |
968 \begin{readmore} |
955 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions |
969 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions |
956 for most antiquotations. Most of the basic operations on ML-syntax are implemented |
970 for most antiquotations. Most of the basic operations on ML-syntax are implemented |
957 in @{ML_file "Pure/ML/ml_syntax.ML"}. |
971 in @{ML_file "Pure/ML/ml_syntax.ML"}. |
958 \end{readmore} |
972 \end{readmore} |
1265 setup %gray {* FooRules.setup *} |
1279 setup %gray {* FooRules.setup *} |
1266 |
1280 |
1267 text {* |
1281 text {* |
1268 This code declares a data container where the theorems are stored, |
1282 This code declares a data container where the theorems are stored, |
1269 an attribute @{text foo} (with the @{text add} and @{text del} options |
1283 an attribute @{text foo} (with the @{text add} and @{text del} options |
1270 for adding and deleting theorems) and an internal ML-interface to retrieve and |
1284 for adding and deleting theorems) and an internal ML-interface for retrieving and |
1271 modify the theorems. |
1285 modifying the theorems. |
1272 Furthermore, the theorems are made available on the user-level under the name |
1286 Furthermore, the theorems are made available on the user-level under the name |
1273 @{text foo}. For example you can declare three lemmas to be a member of the |
1287 @{text foo}. For example you can declare three lemmas to be a member of the |
1274 theorem list @{text foo} by: |
1288 theorem list @{text foo} by: |
1275 *} |
1289 *} |
1276 |
1290 |