equal
deleted
inserted
replaced
55 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
55 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
56 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
56 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
57 code, rather they indicate what the response is when the code is evaluated. |
57 code, rather they indicate what the response is when the code is evaluated. |
58 There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for |
58 There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for |
59 including ML-code. The first evaluates the given code, but any effect on the |
59 including ML-code. The first evaluates the given code, but any effect on the |
60 ambient theory is suppressed. The second needs to be used if ML-code is defined |
60 `ambient' theory is suppressed. The second needs to be used if ML-code is defined |
61 inside a proof. For example |
61 inside a proof. For example |
62 |
62 |
63 \begin{quote} |
63 \begin{quote} |
64 \begin{isabelle} |
64 \begin{isabelle} |
65 \isacommand{lemma}~@{text "test:"}\isanewline |
65 \isacommand{lemma}~@{text "test:"}\isanewline |
67 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline |
67 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline |
68 \isacommand{oops} |
68 \isacommand{oops} |
69 \end{isabelle} |
69 \end{isabelle} |
70 \end{quote} |
70 \end{quote} |
71 |
71 |
72 However, both commands will not play any role in this tutorial (we, for example, |
72 However, both commands will only play minor roles in this tutorial (we will always |
73 always assume the ML-code is defined outside proofs). |
73 arrange that the ML-code is defined outside of proofs). |
74 |
74 |
75 Once a portion of code is relatively stable, you usually want to export it |
75 Once a portion of code is relatively stable, you usually want to export it |
76 to a separate ML-file. Such files can then be included somewhere inside a |
76 to a separate ML-file. Such files can then be included somewhere inside a |
77 theory by using the command \isacommand{use}. For example |
77 theory by using the command \isacommand{use}. For example |
78 |
78 |
100 \isacommand{begin}\\ |
100 \isacommand{begin}\\ |
101 \ldots |
101 \ldots |
102 \end{tabular} |
102 \end{tabular} |
103 \end{quote} |
103 \end{quote} |
104 |
104 |
105 Note that no parentheses are given this time. |
105 Note that no parentheses are given this time. Note also that the |
|
106 `used' file should not contain any |
|
107 \isacommand{use} itself. Otherwise Isabelle is unable to record all |
|
108 file dependencies, which is a nuisance if you have to track down |
|
109 errors. |
106 *} |
110 *} |
107 |
111 |
108 section {* Debugging and Printing\label{sec:printing} *} |
112 section {* Debugging and Printing\label{sec:printing} *} |
109 |
113 |
110 text {* |
114 text {* |
228 "writeln (string_of_thm @{context} @{thm conjI})" |
232 "writeln (string_of_thm @{context} @{thm conjI})" |
229 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
233 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
230 |
234 |
231 In order to improve the readability of theorems we convert |
235 In order to improve the readability of theorems we convert |
232 these schematic variables into free variables using the |
236 these schematic variables into free variables using the |
233 function @{ML [index] import_thms in Variable}. |
237 function @{ML [index] import in Variable}. |
234 *} |
238 *} |
235 |
239 |
236 ML{*fun no_vars ctxt thm = |
240 ML{*fun no_vars ctxt thm = |
237 let |
241 let |
238 val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt |
242 val ((_, [thm']), _) = Variable.import true [thm] ctxt |
239 in |
243 in |
240 thm' |
244 thm' |
241 end |
245 end |
242 |
246 |
243 fun string_of_thm_no_vars ctxt thm = |
247 fun string_of_thm_no_vars ctxt thm = |
628 course of this chapter you will learn more about antiquotations: |
632 course of this chapter you will learn more about antiquotations: |
629 they can simplify Isabelle programming since one can directly access all |
633 they can simplify Isabelle programming since one can directly access all |
630 kinds of logical elements from the ML-level. |
634 kinds of logical elements from the ML-level. |
631 *} |
635 *} |
632 |
636 |
|
637 text {* FIXME: an example of a user defined antiquotation *} |
|
638 |
|
639 ML{*ML_Antiquote.inline "term_pat" |
|
640 (Args.context -- Scan.lift Args.name_source >> |
|
641 (fn (ctxt, s) => |
|
642 let |
|
643 val t = ProofContext.read_term_pattern ctxt s |
|
644 in |
|
645 ML_Syntax.atomic (ML_Syntax.print_term t) |
|
646 end))*} |
|
647 |
|
648 ML{*@{term_pat "?x + ?y"}*} |
|
649 |
|
650 text {* |
|
651 |
|
652 \begin{readmore} |
|
653 @{ML_file "Pure/ML/ml_antiquote.ML"} |
|
654 \end{readmore} |
|
655 *} |
|
656 |
633 section {* Terms and Types *} |
657 section {* Terms and Types *} |
634 |
658 |
635 text {* |
659 text {* |
636 One way to construct Isabelle terms, is by using the antiquotation |
660 One way to construct Isabelle terms, is by using the antiquotation |
637 \mbox{@{text "@{term \<dots>}"}}. For example |
661 \mbox{@{text "@{term \<dots>}"}}. For example |
1698 using the function @{ML FooRules.get}: |
1722 using the function @{ML FooRules.get}: |
1699 |
1723 |
1700 @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} |
1724 @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} |
1701 |
1725 |
1702 \begin{readmore} |
1726 \begin{readmore} |
1703 For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also |
1727 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
1704 the recipe in Section~\ref{recipe:storingdata} about storing arbitrary |
|
1705 data. |
|
1706 \end{readmore} |
1728 \end{readmore} |
1707 |
1729 |
1708 (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?) |
1730 (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?) |
1709 |
1731 |
1710 |
1732 |