96 code. This can be done in a ``quick-and-dirty'' fashion using the function |
95 code. This can be done in a ``quick-and-dirty'' fashion using the function |
97 @{ML_ind writeln in Output}. For example |
96 @{ML_ind writeln in Output}. For example |
98 |
97 |
99 @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} |
98 @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} |
100 |
99 |
101 will print out @{text [quotes] "any string"} inside the response buffer. |
100 will print out @{text [quotes] "any string"}. |
102 This function expects a string as argument. If you develop under |
101 This function expects a string as argument. If you develop under |
103 PolyML, then there is a convenient, though again ``quick-and-dirty'', method |
102 PolyML, then there is a convenient, though again ``quick-and-dirty'', method |
104 for converting values into strings, namely the antiquotation |
103 for converting values into strings, namely the antiquotation |
105 @{text "@{make_string}"}: |
104 @{text "@{make_string}"}: |
106 |
105 |
112 You can print out error messages with the function @{ML_ind error in Library}; |
111 You can print out error messages with the function @{ML_ind error in Library}; |
113 for example: |
112 for example: |
114 |
113 |
115 @{ML_response_fake [display,gray] |
114 @{ML_response_fake [display,gray] |
116 "if 0 = 1 then true else (error \"foo\")" |
115 "if 0 = 1 then true else (error \"foo\")" |
117 "Exception- ERROR \"foo\" raised |
116 "*** foo |
118 At command \"ML\"."} |
117 ***"} |
119 |
118 |
120 This function raises the exception @{text ERROR}, which will then |
119 This function raises the exception @{text ERROR}, which will then |
121 be displayed by the infrastructure. Note that this exception is meant |
120 be displayed by the infrastructure indicating that it is an error by |
|
121 painting the output red. Note that this exception is meant |
122 for ``user-level'' error messages seen by the ``end-user''. |
122 for ``user-level'' error messages seen by the ``end-user''. |
123 For messages where you want to indicate a genuine program error, then |
123 For messages where you want to indicate a genuine program error, then |
124 use the exception @{text Fail}. |
124 use the exception @{text Fail}. |
125 |
125 |
126 Most often you want to inspect data of Isabelle's basic data structures, |
126 Most often you want to inspect data of Isabelle's basic data structures, |
150 ML %grayML{*fun pretty_terms ctxt trms = |
150 ML %grayML{*fun pretty_terms ctxt trms = |
151 Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*} |
151 Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*} |
152 |
152 |
153 text {* |
153 text {* |
154 You can also print out terms together with their typing information. |
154 You can also print out terms together with their typing information. |
155 For this you need to set the configuration value |
155 For this you need to set the configuration value |
156 @{ML_ind show_types in Syntax} to @{ML true}. |
156 @{ML_ind show_types in Syntax} to @{ML true}. |
157 *} |
157 *} |
158 |
158 |
159 ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*} |
159 ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*} |
160 |
160 |
541 where the return value of the recursive call is bound explicitly to |
541 where the return value of the recursive call is bound explicitly to |
542 the pair @{ML "(los, grs)" for los grs}. However, this function |
542 the pair @{ML "(los, grs)" for los grs}. However, this function |
543 can be implemented more concisely as |
543 can be implemented more concisely as |
544 *} |
544 *} |
545 |
545 |
546 ML %grayML{*fun separate i [] = ([], []) |
546 ML %grayML{*fun separate _ [] = ([], []) |
547 | separate i (x::xs) = |
547 | separate i (x::xs) = |
548 if i <= x |
548 if i <= x |
549 then separate i xs ||> cons x |
549 then separate i xs ||> cons x |
550 else separate i xs |>> cons x*} |
550 else separate i xs |>> cons x*} |
551 |
551 |
770 |
770 |
771 Another important antiquotation is @{text "@{context}"}. (What the |
771 Another important antiquotation is @{text "@{context}"}. (What the |
772 difference between a theory and a context is will be described in Chapter |
772 difference between a theory and a context is will be described in Chapter |
773 \ref{chp:advanced}.) A context is for example needed in order to use the |
773 \ref{chp:advanced}.) A context is for example needed in order to use the |
774 function @{ML print_abbrevs in Proof_Context} that list of all currently |
774 function @{ML print_abbrevs in Proof_Context} that list of all currently |
775 defined abbreviations. |
775 defined abbreviations. For example |
776 |
776 |
777 @{ML_response_fake [display, gray] |
777 @{ML_response_fake [display, gray] |
778 "Proof_Context.print_abbrevs @{context}" |
778 "Proof_Context.print_abbrevs @{context}" |
779 "Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x) |
779 "\<dots> |
780 INTER \<equiv> INFI |
780 INTER \<equiv> INFI |
781 Inter \<equiv> Inf |
781 Inter \<equiv> Inf |
782 \<dots>"} |
782 \<dots>"} |
783 |
783 |
|
784 The precise output of course depends on the abbreviations that are |
|
785 currently defined; this can change over time. |
784 You can also use antiquotations to refer to proved theorems: |
786 You can also use antiquotations to refer to proved theorems: |
785 @{text "@{thm \<dots>}"} for a single theorem |
787 @{text "@{thm \<dots>}"} for a single theorem |
786 |
788 |
787 @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} |
789 @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} |
788 |
790 |
810 It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"} |
812 It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"} |
811 whose first argument is a statement (possibly many of them separated by @{text "and"}) |
813 whose first argument is a statement (possibly many of them separated by @{text "and"}) |
812 and the second is a proof. For example |
814 and the second is a proof. For example |
813 *} |
815 *} |
814 |
816 |
815 ML %grayML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *} |
817 ML %grayML{*val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *} |
816 |
818 |
817 text {* |
819 text {* |
818 The result can be printed out as follows. |
820 The result can be printed out as follows. |
819 |
821 |
820 @{ML_response_fake [gray,display] |
822 @{ML_response_fake [gray,display] |
821 "foo_thm |> pretty_thms_no_vars @{context} |
823 "foo_thms |> pretty_thms_no_vars @{context} |
822 |> pwriteln" |
824 |> pwriteln" |
823 "True, False \<Longrightarrow> P"} |
825 "True, False \<Longrightarrow> P"} |
824 |
826 |
825 You can also refer to the current simpset via an antiquotation. To illustrate |
827 You can also refer to the current simpset via an antiquotation. To illustrate |
826 this we implement the function that extracts the theorem names stored in a |
828 this we implement the function that extracts the theorem names stored in a |
827 simpset. |
829 simpset. |
913 which can be installed with |
915 which can be installed with |
914 *} |
916 *} |
915 |
917 |
916 setup %gray {* type_pat_setup *} |
918 setup %gray {* type_pat_setup *} |
917 |
919 |
918 text {* |
920 text {* |
919 However, a word of warning is in order: Introducing new antiquotations |
921 However, a word of warning is in order: Introducing new antiquotations should be done only after |
920 should be done only after careful deliberations. They can make your |
922 careful deliberations. They can potentially make your code harder to read, than making it easier. |
921 code harder to read, than making it easier. |
|
922 |
923 |
923 \begin{readmore} |
924 \begin{readmore} |
924 The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"} |
925 The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"} |
925 contain the infrastructure and definitions for most antiquotations. Most of the basic operations |
926 contain the infrastructure and definitions for most antiquotations. Most of the basic operations |
926 on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}. |
927 on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}. |
990 true"} |
991 true"} |
991 |
992 |
992 Notice that we access the integer as an integer and the boolean as |
993 Notice that we access the integer as an integer and the boolean as |
993 a boolean. If we attempt to access the integer as a boolean, then we get |
994 a boolean. If we attempt to access the integer as a boolean, then we get |
994 a runtime error. |
995 a runtime error. |
995 |
996 |
996 @{ML_response_fake [display, gray] |
997 @{ML_response_fake [display, gray] |
997 "project_bool (nth foo_list 0)" |
998 "project_bool (nth foo_list 0)" |
998 "*** Exception- Match raised"} |
999 "*** exception Match raised"} |
999 |
1000 |
1000 This runtime error is the reason why ML is still type-sound despite |
1001 This runtime error is the reason why ML is still type-sound despite |
1001 containing a universal type. |
1002 containing a universal type. |
1002 |
1003 |
1003 Now, Isabelle heavily uses this mechanism for storing all sorts of |
1004 Now, Isabelle heavily uses this mechanism for storing all sorts of |
1214 |
1215 |
1215 For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, |
1216 For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, |
1216 for treating theories and proof contexts more uniformly. This type is defined as follows |
1217 for treating theories and proof contexts more uniformly. This type is defined as follows |
1217 *} |
1218 *} |
1218 |
1219 |
1219 ML_val{*datatype generic = |
1220 ML_val %grayML{*datatype generic = |
1220 Theory of theory |
1221 Theory of theory |
1221 | Proof of proof*} |
1222 | Proof of proof*} |
1222 |
1223 |
1223 text {* |
1224 text {* |
1224 \footnote{\bf FIXME: say more about generic contexts.} |
1225 \footnote{\bf FIXME: say more about generic contexts.} |