31 |
31 |
32 \isa{\isacommand{ML} |
32 \isa{\isacommand{ML} |
33 \isacharverbatimopen\isanewline |
33 \isacharverbatimopen\isanewline |
34 \hspace{5mm}@{ML "3 + 4"}\isanewline |
34 \hspace{5mm}@{ML "3 + 4"}\isanewline |
35 \isacharverbatimclose\isanewline |
35 \isacharverbatimclose\isanewline |
36 @{ML_text "> 7"}\smallskip} |
36 @{text "> 7"}\smallskip} |
37 |
37 |
38 Expressions inside \isacommand{ML}-commands are immediately evaluated, |
38 The @{text [quotes] "> 7"} indicates the response Isabelle prints out when the |
39 like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of |
39 \isacommand{ML}-command is evaluated. Like ``normal'' Isabelle proof scripts, |
|
40 \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of |
40 your Isabelle environment. The code inside the \isacommand{ML}-command |
41 your Isabelle environment. The code inside the \isacommand{ML}-command |
41 can also contain value and function bindings, and even those can be |
42 can also contain value and function bindings, and even those can be |
42 undone when the proof script is retracted. In what follows we will drop the |
43 undone when the proof script is retracted. For better readability, we will in what |
43 \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever |
44 follows drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
44 we show code and its response. |
45 whenever we show code and its response. |
45 |
46 |
46 Once a portion of code is relatively stable, one usually wants to |
47 Once a portion of code is relatively stable, one usually wants to |
47 export it to a separate ML-file. Such files can then be included in a |
48 export it to a separate ML-file. Such files can then be included in a |
48 theory by using \isacommand{uses} in the header of the theory, like |
49 theory by using \isacommand{uses} in the header of the theory, like |
49 |
50 |
50 \begin{center} |
51 \begin{center} |
51 \begin{tabular}{@ {}l} |
52 \begin{tabular}{@ {}l} |
52 \isacommand{theory} FirstSteps\\ |
53 \isacommand{theory} FirstSteps\\ |
53 \isacommand{imports} Main\\ |
54 \isacommand{imports} Main\\ |
54 \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\ |
55 \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\ |
55 \isacommand{begin}\\ |
56 \isacommand{begin}\\ |
56 \ldots |
57 \ldots |
57 \end{tabular} |
58 \end{tabular} |
58 \end{center} |
59 \end{center} |
59 |
60 |
65 |
66 |
66 During development you might find it necessary to inspect some data |
67 During development you might find it necessary to inspect some data |
67 in your code. This can be done in a ``quick-and-dirty'' fashion using |
68 in your code. This can be done in a ``quick-and-dirty'' fashion using |
68 the function @{ML "warning"}. For example |
69 the function @{ML "warning"}. For example |
69 |
70 |
70 @{ML [display] "warning \"any string\""} |
71 @{ML_response_fake [display] "warning \"any string\"" "\"any string\""} |
71 |
72 |
72 will print out @{ML_text [quotes] "any string"} inside the response buffer |
73 will print out @{text [quotes] "any string"} inside the response buffer |
73 of Isabelle. This function expects a string. If you develop under PolyML, |
74 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
74 then there is a convenient, though again ``quick-and-dirty'', method for |
75 then there is a convenient, though again ``quick-and-dirty'', method for |
75 converting values into strings, for example: |
76 converting values into strings, for example: |
76 |
77 |
77 @{ML [display] "warning (makestring 1)"} |
78 @{ML_response_fake [display] "warning (makestring 1)" "1"} |
78 |
79 |
79 However this only works if the type of what is converted is monomorphic and is not |
80 However this only works if the type of what is converted is monomorphic and is not |
80 a function. |
81 a function. |
81 |
82 |
82 The function @{ML "warning"} should only be used for testing purposes, because any |
83 The function @{ML "warning"} should only be used for testing purposes, because any |
83 output this function generates will be overwritten as soon as an error is |
84 output this function generates will be overwritten as soon as an error is |
84 raised. For printing anything more serious and elaborate, the |
85 raised. For printing anything more serious and elaborate, the |
85 function @{ML tracing} is more appropriate. This function writes all output into |
86 function @{ML tracing} is more appropriate. This function writes all output into |
86 a separate tracing buffer. For example |
87 a separate tracing buffer. For example |
87 |
88 |
88 @{ML [display] "tracing \"foo\""} |
89 @{ML_response_fake [display] "tracing \"foo\"" "\"foo\""} |
89 |
90 |
90 It is also possible to redirect the ``channel'' where the string @{ML_text "foo"} is |
91 It is also possible to redirect the ``channel'' where the string @{text "foo"} is |
91 printed to a separate file, e.g. to prevent Proof General from choking on massive |
92 printed to a separate file, e.g. to prevent Proof General from choking on massive |
92 amounts of trace output. This redirection can be achieved using the code |
93 amounts of trace output. This redirection can be achieved using the code |
93 *} |
94 *} |
94 |
95 |
95 ML{* |
96 ML{* |
108 *} |
109 *} |
109 |
110 |
110 text {* |
111 text {* |
111 |
112 |
112 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
113 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
113 will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. |
114 will cause that all tracing information is printed into the file @{text "foo.bar"}. |
114 |
115 |
115 *} |
116 *} |
116 |
117 |
117 |
118 |
118 section {* Antiquotations *} |
119 section {* Antiquotations *} |
119 |
120 |
120 text {* |
121 text {* |
121 The main advantage of embedding all code in a theory is that the code can |
122 The main advantage of embedding all code in a theory is that the code can |
122 contain references to entities defined on the logical level of Isabelle (by |
123 contain references to entities defined on the logical level of Isabelle. By |
123 this we mean definitions, theorems, terms and so on). This is done using |
124 this we mean definitions, theorems, terms and so on. This kind of reference is |
124 antiquotations. For example, one can print out the name of the current |
125 realised with antiquotations. For example, one can print out the name of the current |
125 theory by typing |
126 theory by typing |
126 |
127 |
127 |
128 |
128 @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"} |
129 @{ML_response [display] "Context.theory_name @{theory}" "\"FirstSteps\""} |
129 |
130 |
130 where @{text "@{theory}"} is an antiquotation that is substituted with the |
131 where @{text "@{theory}"} is an antiquotation that is substituted with the |
131 current theory (remember that we assumed we are inside the theory |
132 current theory (remember that we assumed we are inside the theory |
132 @{ML_text FirstSteps}). The name of this theory can be extracted using |
133 @{text FirstSteps}). The name of this theory can be extracted with |
133 the function @{ML "Context.theory_name"}. |
134 the function @{ML "Context.theory_name"}. |
134 |
135 |
135 Note, however, that antiquotations are statically scoped, that is the value is |
136 Note, however, that antiquotations are statically scoped, that is the value is |
136 determined at ``compile-time'', not ``run-time''. For example the function |
137 determined at ``compile-time'', not ``run-time''. For example the function |
137 *} |
138 *} |
140 fun not_current_thyname () = Context.theory_name @{theory} |
141 fun not_current_thyname () = Context.theory_name @{theory} |
141 *} |
142 *} |
142 |
143 |
143 text {* |
144 text {* |
144 |
145 |
145 does \emph{not} return the name of the current theory, if it is run in a |
146 does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a |
146 different theory. Instead, the code above defines the constant function |
147 different theory. Instead, the code above defines the constant function |
147 that always returns the string @{ML_text "FirstSteps"}, no matter where the |
148 that always returns the string @{text [quotes] "FirstSteps"}, no matter where the |
148 function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is |
149 function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is |
149 \emph{not} replaced with code that will look up the current theory in |
150 \emph{not} replaced with code that will look up the current theory in |
150 some data structure and return it. Instead, it is literally |
151 some data structure and return it. Instead, it is literally |
151 replaced with the value representing the theory name. |
152 replaced with the value representing the theory name. |
152 |
153 |
156 @{ML_response_fake [display] "@{simpset}" "\<dots>"} |
157 @{ML_response_fake [display] "@{simpset}" "\<dots>"} |
157 |
158 |
158 (FIXME: what does a simpset look like? It seems to be the same problem |
159 (FIXME: what does a simpset look like? It seems to be the same problem |
159 like tokens.) |
160 like tokens.) |
160 |
161 |
161 While antiquotations have many applications, they were originally introduced to |
162 While antiquotations nowadays have many applications, they were originally introduced to |
162 avoid explicit bindings for theorems such as |
163 avoid explicit bindings for theorems such as |
163 *} |
164 *} |
164 |
165 |
165 ML {* |
166 ML {* |
166 val allI = thm "allI" |
167 val allI = thm "allI" |
167 *} |
168 *} |
168 |
169 |
169 text {* |
170 text {* |
170 These bindings were difficult to maintain and also could be accidentally |
171 These bindings were difficult to maintain and also could accidentally |
171 overwritten by the user. This usually broke definitional |
172 be overwritten by the user. This usually broke definitional |
172 packages. Antiquotations solve this problem, since they are ``linked'' |
173 packages. Antiquotations solve this problem, since they are ``linked'' |
173 statically at compile-time. However, that also sometimes limits their |
174 statically at compile-time. However, that also sometimes limits their |
174 applicability. In the course of this introduction, we will learn more about |
175 usefulness. In the course of this introduction, we will learn more about |
175 these antiquotations: they greatly simplify Isabelle programming since one |
176 these antiquotations: they greatly simplify Isabelle programming since one |
176 can directly access all kinds of logical elements from ML. |
177 can directly access all kinds of logical elements from ML. |
177 |
178 |
178 *} |
179 *} |
179 |
180 |
287 One tricky point in constructing terms by hand is to obtain the |
288 One tricky point in constructing terms by hand is to obtain the |
288 fully qualified name for constants. For example the names for @{text "zero"} and |
289 fully qualified name for constants. For example the names for @{text "zero"} and |
289 @{text "+"} are more complex than one first expects, namely |
290 @{text "+"} are more complex than one first expects, namely |
290 |
291 |
291 \begin{center} |
292 \begin{center} |
292 @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}. |
293 @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. |
293 \end{center} |
294 \end{center} |
294 |
295 |
295 The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because |
296 The extra prefixes @{text zero_class} and @{text plus_class} are present because |
296 these constants are defined within type classes; the prefix @{text "HOL"} indicates in |
297 these constants are defined within type classes; the prefix @{text "HOL"} indicates in |
297 which theory they are defined. Guessing such internal names can sometimes be quite hard. |
298 which theory they are defined. Guessing such internal names can sometimes be quite hard. |
298 Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the |
299 Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the |
299 expansion automatically, for example: |
300 expansion automatically, for example: |
300 |
301 |
330 *} |
331 *} |
331 |
332 |
332 text {* |
333 text {* |
333 |
334 |
334 \begin{exercise}\label{fun:revsum} |
335 \begin{exercise}\label{fun:revsum} |
335 Write a function @{ML_text "rev_sum : term -> term"} that takes a |
336 Write a function @{text "rev_sum : term -> term"} that takes a |
336 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero) |
337 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero) |
337 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
338 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
338 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
339 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
339 associates to the left. Try your function on some examples. |
340 associates to the left. Try your function on some examples. |
340 \end{exercise} |
341 \end{exercise} |