author | wenzelm |
Fri, 15 Oct 2010 22:26:25 +0100 | |
changeset 39854 | 7480a7a159cb |
parent 39851 | 7219a771ab63 |
child 39855 | d4299b415879 |
permissions | -rw-r--r-- |
29755 | 1 |
theory "ML" |
2 |
imports Base |
|
3 |
begin |
|
18538 | 4 |
|
39822 | 5 |
chapter {* Isabelle/ML *} |
20489 | 6 |
|
39823 | 7 |
text {* Isabelle/ML is best understood as a certain culture based on |
8 |
Standard ML. Thus it is not a new programming language, but a |
|
9 |
certain way to use SML at an advanced level within the Isabelle |
|
10 |
environment. This covers a variety of aspects that are geared |
|
11 |
towards an efficient and robust platform for applications of formal |
|
12 |
logic with fully foundational proof construction --- according to |
|
13 |
the well-known \emph{LCF principle}. There are specific library |
|
14 |
modules and infrastructure to address the needs for such difficult |
|
15 |
tasks. For example, the raw parallel programming model of Poly/ML |
|
16 |
is presented as considerably more abstract concept of \emph{future |
|
17 |
values}, which is then used to augment the inference kernel, proof |
|
18 |
interpreter, and theory loader accordingly. |
|
19 |
||
20 |
The main aspects of Isabelle/ML are introduced below. These |
|
21 |
first-hand explanations should help to understand how proper |
|
22 |
Isabelle/ML is to be read and written, and to get access to the |
|
23 |
wealth of experience that is expressed in the source text and its |
|
24 |
history of changes.\footnote{See |
|
25 |
\url{http://isabelle.in.tum.de/repos/isabelle} for the full |
|
26 |
Mercurial history. There are symbolic tags to refer to official |
|
27 |
Isabelle releases, as opposed to arbitrary \emph{tip} versions that |
|
28 |
merely reflect snapshots that are never really up-to-date.} *} |
|
29 |
||
30 |
||
31 |
section {* SML embedded into Isabelle/Isar *} |
|
32 |
||
39824 | 33 |
text {* ML and Isar are intertwined via an open-ended bootstrap |
34 |
process that provides more and more programming facilities and |
|
35 |
logical content in an alternating manner. Bootstrapping starts from |
|
36 |
the raw environment of existing implementations of Standard ML |
|
37 |
(mainly Poly/ML, but also SML/NJ). |
|
39823 | 38 |
|
39824 | 39 |
Isabelle/Pure marks the point where the original ML toplevel is |
40 |
superseded by the Isar toplevel that maintains a uniform environment |
|
41 |
for arbitrary ML values (see also \secref{sec:context}). This |
|
42 |
formal context holds logical entities as well as ML compiler |
|
43 |
bindings, among many other things. Raw Standard ML is never |
|
44 |
encountered again after the initial bootstrap of Isabelle/Pure. |
|
39823 | 45 |
|
39824 | 46 |
Object-logics such as Isabelle/HOL are built within the |
47 |
Isabelle/ML/Isar environment of Pure by introducing suitable |
|
48 |
theories with associated ML text, either inlined or as separate |
|
49 |
files. Thus Isabelle/HOL is defined as a regular user-space |
|
50 |
application within the Isabelle framework. Further add-on tools can |
|
51 |
be implemented in ML within the Isar context in the same manner: ML |
|
52 |
is part of the regular user-space repertoire of Isabelle. |
|
39823 | 53 |
*} |
54 |
||
39824 | 55 |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
56 |
subsection {* Isar ML commands *} |
39823 | 57 |
|
58 |
text {* The primary Isar source language provides various facilities |
|
59 |
to open a ``window'' to the underlying ML compiler. Especially see |
|
39824 | 60 |
@{command_ref "use"} and @{command_ref "ML"}, which work exactly the |
61 |
same way, only the source text is provided via a file vs.\ inlined, |
|
62 |
respectively. Apart from embedding ML into the main theory |
|
63 |
definition like that, there are many more commands that refer to ML |
|
64 |
source, such as @{command_ref setup} or @{command_ref declaration}. |
|
65 |
An example of even more fine-grained embedding of ML into Isar is |
|
66 |
the proof method @{method_ref tactic}, which refines the pending goal state |
|
67 |
via a given expression of type @{ML_type tactic}. |
|
68 |
*} |
|
39823 | 69 |
|
39824 | 70 |
text %mlex {* The following artificial example demonstrates some ML |
71 |
toplevel declarations within the implicit Isar theory context. This |
|
72 |
is regular functional programming without referring to logical |
|
73 |
entities yet. |
|
39823 | 74 |
*} |
75 |
||
76 |
ML {* |
|
77 |
fun factorial 0 = 1 |
|
78 |
| factorial n = n * factorial (n - 1) |
|
79 |
*} |
|
80 |
||
39824 | 81 |
text {* \noindent Here the ML environment is really managed by |
82 |
Isabelle, i.e.\ the @{ML factorial} function is not yet accessible |
|
83 |
in the preceding paragraph, nor in a different theory that is |
|
84 |
independent from the current one in the import hierarchy. |
|
39823 | 85 |
|
86 |
Removing the above ML declaration from the source text will remove |
|
87 |
any trace of this definition as expected. The Isabelle/ML toplevel |
|
88 |
environment is managed in a \emph{stateless} way: unlike the raw ML |
|
39824 | 89 |
toplevel or similar command loops of Computer Algebra systems, there |
90 |
are no global side-effects involved here.\footnote{Such a stateless |
|
91 |
compilation environment is also a prerequisite for robust parallel |
|
92 |
compilation within independent nodes of the implicit theory |
|
93 |
development graph.} |
|
39823 | 94 |
|
95 |
\bigskip The next example shows how to embed ML into Isar proofs. |
|
39824 | 96 |
Instead of @{command_ref "ML"} for theory mode, we use @{command_ref |
97 |
"ML_prf"} for proof mode. As illustrated below, its effect on the |
|
98 |
ML environment is local to the whole proof body, while ignoring its |
|
99 |
internal block structure. |
|
100 |
*} |
|
39823 | 101 |
|
102 |
example_proof |
|
39851 | 103 |
ML_prf %"ML" {* val a = 1 *} |
39824 | 104 |
{ -- {* Isar block structure ignored by ML environment *} |
39851 | 105 |
ML_prf %"ML" {* val b = a + 1 *} |
39824 | 106 |
} -- {* Isar block structure ignored by ML environment *} |
39851 | 107 |
ML_prf %"ML" {* val c = b + 1 *} |
39823 | 108 |
qed |
109 |
||
39824 | 110 |
text {* \noindent By side-stepping the normal scoping rules for Isar |
111 |
proof blocks, embedded ML code can refer to the different contexts |
|
112 |
explicitly, and manipulate corresponding entities, e.g.\ export a |
|
113 |
fact from a block context. |
|
39823 | 114 |
|
39824 | 115 |
\bigskip Two further ML commands are useful in certain situations: |
116 |
@{command_ref ML_val} and @{command_ref ML_command} are both |
|
117 |
\emph{diagnostic} in the sense that there is no effect on the |
|
118 |
underlying environment, and can thus used anywhere (even outside a |
|
119 |
theory). The examples below produce long strings of digits by |
|
120 |
invoking @{ML factorial}: @{command ML_val} already takes care of |
|
121 |
printing the ML toplevel result, but @{command ML_command} is silent |
|
122 |
so we produce an explicit output message. |
|
123 |
*} |
|
39823 | 124 |
|
125 |
ML_val {* factorial 100 *} |
|
126 |
ML_command {* writeln (string_of_int (factorial 100)) *} |
|
127 |
||
128 |
example_proof |
|
39824 | 129 |
ML_val {* factorial 100 *} (* FIXME check/fix indentation *) |
39823 | 130 |
ML_command {* writeln (string_of_int (factorial 100)) *} |
131 |
qed |
|
132 |
||
133 |
||
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
134 |
subsection {* Compile-time context *} |
39823 | 135 |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
136 |
text {* Whenever the ML compiler is invoked within Isabelle/Isar, the |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
137 |
formal context is passed as a thread-local reference variable. Thus |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
138 |
ML code may access the theory context during compilation, by reading |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
139 |
or writing the (local) theory under construction. Note that such |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
140 |
direct access to the compile-time context is rare; in practice it is |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
141 |
typically via some derived ML functions. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
142 |
*} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
143 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
144 |
text %mlref {* |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
145 |
\begin{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
146 |
@{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\ |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
147 |
@{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\ |
39850 | 148 |
@{index_ML bind_thms: "string * thm list -> unit"} \\ |
149 |
@{index_ML bind_thm: "string * thm -> unit"} \\ |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
150 |
\end{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
151 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
152 |
\begin{description} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
153 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
154 |
\item @{ML "ML_Context.the_generic_context ()"} refers to the theory |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
155 |
context of the ML toplevel --- at compile time. ML code needs to |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
156 |
take care to refer to @{ML "ML_Context.the_generic_context ()"} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
157 |
correctly. Recall that evaluation of a function body is delayed |
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
158 |
until actual run-time. |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
159 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
160 |
\item @{ML "Context.>>"}~@{text f} applies context transformation |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
161 |
@{text f} to the implicit context of the ML toplevel. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
162 |
|
39850 | 163 |
\item @{ML bind_thms}~@{text "(name, thms)"} stores a list of |
164 |
theorems produced in ML both in the (global) theory context and the |
|
165 |
ML toplevel, associating it with the provided name. Theorems are |
|
166 |
put into a global ``standard'' format before being stored. |
|
167 |
||
168 |
\item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a |
|
169 |
singleton theorem. |
|
170 |
||
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
171 |
\end{description} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
172 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
173 |
It is very important to note that the above functions are really |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
174 |
restricted to the compile time, even though the ML compiler is |
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
175 |
invoked at run-time. The majority of ML code either uses static |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
176 |
antiquotations (\secref{sec:ML-antiq}) or refers to the theory or |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
177 |
proof context at run-time, by explicit functional abstraction. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
178 |
*} |
39823 | 179 |
|
180 |
||
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
181 |
subsection {* Antiquotations \label{sec:ML-antiq} *} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
182 |
|
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
183 |
text {* A very important consequence of embedding SML into Isar is the |
39829 | 184 |
concept of \emph{ML antiquotation}. First, the standard token |
185 |
language of ML is augmented by special syntactic entities of the |
|
186 |
following form: |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
187 |
|
39829 | 188 |
\indexouternonterm{antiquote} |
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
189 |
\begin{rail} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
190 |
antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
191 |
; |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
192 |
\end{rail} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
193 |
|
39829 | 194 |
\noindent Here @{syntax nameref} and @{syntax args} are regular |
195 |
outer syntax categories. Note that attributes and proof methods use |
|
196 |
similar syntax. |
|
39823 | 197 |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
198 |
\medskip A regular antiquotation @{text "@{name args}"} processes |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
199 |
its arguments by the usual means of the Isar source language, and |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
200 |
produces corresponding ML source text, either as literal |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
201 |
\emph{inline} text (e.g. @{text "@{term t}"}) or abstract |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
202 |
\emph{value} (e.g. @{text "@{thm th}"}). This pre-compilation |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
203 |
scheme allows to refer to formal entities in a robust manner, with |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
204 |
proper static scoping and with some degree of logical checking of |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
205 |
small portions of the code. |
39823 | 206 |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
207 |
Special antiquotations like @{text "@{let \<dots>}"} or @{text "@{note |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
208 |
\<dots>}"} augment the compilation context without generating code. The |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
209 |
non-ASCII braces @{text "\<lbrace>"} and @{text "\<rbrace>"} allow to delimit the |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
210 |
effect by introducing local blocks within the pre-compilation |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
211 |
environment. |
39829 | 212 |
|
213 |
\bigskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader |
|
214 |
perspective on Isabelle/ML antiquotations. |
|
215 |
*} |
|
216 |
||
39830 | 217 |
text %mlantiq {* |
39829 | 218 |
\begin{matharray}{rcl} |
219 |
@{ML_antiquotation_def "let"} & : & @{text ML_antiquotation} \\ |
|
220 |
@{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\ |
|
221 |
\end{matharray} |
|
222 |
||
223 |
\begin{rail} |
|
224 |
'let' ((term + 'and') '=' term + 'and') |
|
225 |
; |
|
226 |
||
227 |
'note' (thmdef? thmrefs + 'and') |
|
228 |
; |
|
229 |
\end{rail} |
|
230 |
||
231 |
\begin{description} |
|
232 |
||
233 |
\item @{text "@{let p = t}"} binds schematic variables in the |
|
234 |
pattern @{text "p"} by higher-order matching against the term @{text |
|
235 |
"t"}. This is analogous to the regular @{command_ref let} command |
|
236 |
in the Isar proof language. The pre-compilation environment is |
|
237 |
augmented by auxiliary term bindings, without emitting ML source. |
|
238 |
||
239 |
\item @{text "@{note a = b\<^sub>1 \<dots> b\<^sub>n}"} recalls existing facts @{text |
|
240 |
"b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. This is analogous to |
|
241 |
the regular @{command_ref note} command in the Isar proof language. |
|
242 |
The pre-compilation environment is augmented by auxiliary fact |
|
243 |
bindings, without emitting ML source. |
|
244 |
||
245 |
\end{description} |
|
246 |
*} |
|
247 |
||
248 |
text %mlex {* The following artificial example gives a first |
|
249 |
impression about using the antiquotation elements introduced so far, |
|
250 |
together with the basic @{text "@{thm}"} antiquotation defined |
|
251 |
later. |
|
252 |
*} |
|
253 |
||
254 |
ML {* |
|
255 |
\<lbrace> |
|
256 |
@{let ?t = my_term} |
|
257 |
@{note my_refl = reflexive [of ?t]} |
|
258 |
fun foo th = Thm.transitive th @{thm my_refl} |
|
259 |
\<rbrace> |
|
260 |
*} |
|
261 |
||
262 |
text {* |
|
263 |
The extra block delimiters do not affect the compiled code itself, i.e.\ |
|
264 |
function @{ML foo} is available in the present context. |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
265 |
*} |
39823 | 266 |
|
39835 | 267 |
|
39854 | 268 |
section {* Message output channels \label{sec:message-channels} *} |
39835 | 269 |
|
270 |
text {* Isabelle provides output channels for different kinds of |
|
271 |
messages: regular output, high-volume tracing information, warnings, |
|
272 |
and errors. |
|
273 |
||
274 |
Depending on the user interface involved, these messages may appear |
|
275 |
in different text styles or colours. The standard output for |
|
276 |
terminal sessions prefixes each line of warnings by @{verbatim |
|
277 |
"###"} and errors by @{verbatim "***"}, but leaves anything else |
|
278 |
unchanged. |
|
279 |
||
280 |
Messages are associated with the transaction context of the running |
|
281 |
Isar command. This enables the front-end to manage commands and |
|
282 |
resulting messages together. For example, after deleting a command |
|
283 |
from a given theory document version, the corresponding message |
|
284 |
output can be retracted from the display. *} |
|
285 |
||
286 |
text %mlref {* |
|
287 |
\begin{mldecls} |
|
288 |
@{index_ML writeln: "string -> unit"} \\ |
|
289 |
@{index_ML tracing: "string -> unit"} \\ |
|
290 |
@{index_ML warning: "string -> unit"} \\ |
|
291 |
@{index_ML error: "string -> 'a"} \\ |
|
292 |
\end{mldecls} |
|
293 |
||
294 |
\begin{description} |
|
295 |
||
296 |
\item @{ML writeln}~@{text "text"} outputs @{text "text"} as regular |
|
297 |
message. This is the primary message output operation of Isabelle |
|
298 |
and should be used by default. |
|
299 |
||
300 |
\item @{ML tracing}~@{text "text"} outputs @{text "text"} as special |
|
301 |
tracing message, indicating potential high-volume output to the |
|
302 |
front-end (hundreds or thousands of messages issued by a single |
|
303 |
command). The idea is to allow the user-interface to downgrade the |
|
304 |
quality of message display to achieve higher throughput. |
|
305 |
||
306 |
Note that the user might have to take special actions to see tracing |
|
307 |
output, e.g.\ switch to a different output window. So this channel |
|
308 |
should not be used for regular output. |
|
309 |
||
310 |
\item @{ML warning}~@{text "text"} outputs @{text "text"} as |
|
311 |
warning, which typically means some extra emphasis on the front-end |
|
312 |
side (color highlighting, icon). |
|
313 |
||
314 |
\item @{ML error}~@{text "text"} raises exception @{ML ERROR}~@{text |
|
315 |
"text"} and thus lets the Isar toplevel print @{text "text"} on the |
|
316 |
error channel, which typically means some extra emphasis on the |
|
317 |
front-end side (color highlighting, icon). |
|
318 |
||
319 |
This assumes that the exception is not handled before the command |
|
320 |
terminates. Handling exception @{ML ERROR}~@{text "text"} is a |
|
321 |
perfectly legal alternative: it means that the error is absorbed |
|
322 |
without any message output. |
|
323 |
||
324 |
\end{description} |
|
325 |
||
326 |
\begin{warn} |
|
327 |
The actual error channel is accessed via @{ML Output.error_msg}, but |
|
328 |
the interaction protocol of Proof~General \emph{crashes} if that |
|
329 |
function is used in regular ML code: error output and toplevel |
|
330 |
command failure always need to coincide here. |
|
331 |
\end{warn} |
|
332 |
||
333 |
\begin{warn} |
|
334 |
Regular Isabelle/ML code should output messages exclusively by the |
|
335 |
official channels. Using raw I/O on \emph{stdout} or \emph{stderr} |
|
336 |
instead (e.g.\ via @{ML TextIO.output}) is apt to cause problems in |
|
337 |
the presence of parallel and asynchronous processing of Isabelle |
|
338 |
theories. Such raw output might be displayed by the front-end in |
|
339 |
some system console log, with a low chance that the user will ever |
|
340 |
see it. Moreover, as a genuine side-effect on global process |
|
341 |
channels, there is no proper way to retract output when Isar command |
|
342 |
transactions are reset. |
|
343 |
\end{warn} |
|
344 |
*} |
|
345 |
||
39854 | 346 |
|
347 |
section {* Exceptions *} |
|
348 |
||
349 |
text {* The Standard ML semantics of strict functional evaluation |
|
350 |
together with exceptions is rather well defined, but some delicate |
|
351 |
points need to be observed to avoid that ML programs go wrong |
|
352 |
despite static type-checking. Exceptions in Isabelle/ML are |
|
353 |
subsequently categorized as follows. |
|
354 |
||
355 |
\paragraph{Regular user errors.} These are meant to provide |
|
356 |
informative feedback about malformed input etc. |
|
357 |
||
358 |
The \emph{error} function raises the corresponding \emph{ERROR} |
|
359 |
exception, with a plain text message as argument. \emph{ERROR} |
|
360 |
exceptions can be handled internally, in order to be ignored, turned |
|
361 |
into other exceptions, or cascaded by appending messages. If the |
|
362 |
corresponding Isabelle/Isar command terminates with an \emph{ERROR} |
|
363 |
exception state, the toplevel will take care to print the result on |
|
364 |
the error channel (see \secref{sec:message-channels}). |
|
365 |
||
366 |
It is considered bad style to refer to internal function names or |
|
367 |
values in ML source notation in user error messages. |
|
368 |
||
369 |
Grammatical correctness of error messages can be improved by |
|
370 |
\emph{omitting} final punctuation: messages are often concatenated |
|
371 |
or put into a larger context (e.g.\ augmented with source position). |
|
372 |
By not insisting in the final word at the origin of the error, the |
|
373 |
system can perform its administrative tasks more easily and |
|
374 |
robustly. |
|
375 |
||
376 |
\paragraph{Program failures.} There is a handful of standard |
|
377 |
exceptions that indicate general failure situations, or failures of |
|
378 |
core operations on logical entities (types, terms, theorems, |
|
379 |
theories). |
|
380 |
||
381 |
These exceptions indicate a genuine breakdown of the program, so the |
|
382 |
main purpose is to determine quickly what has happened where. |
|
383 |
Traditionally, the (short) exception message would normally include |
|
384 |
the name of an ML function, although this no longer necessary, |
|
385 |
because the ML runtime system prints a detailed source position of |
|
386 |
the corresponding @{verbatim raise} keyword. |
|
387 |
||
388 |
\medskip User modules can always introduce their own custom |
|
389 |
exceptions locally, e.g.\ to organize internal failures robustly |
|
390 |
without overlapping with existing exceptions. Exceptions that are |
|
391 |
exposed in module signatures require extra care, though, and should |
|
392 |
\emph{not} be introduced by default. Surprise by end-users or ML |
|
393 |
users of a module can be often minimized by using plain errors or |
|
394 |
one of the predefined exceptions. |
|
395 |
||
396 |
\paragraph{Interrupts.} These indicate arbitrary system events: |
|
397 |
both the ML runtime system and the Isabelle/ML infrastructure signal |
|
398 |
various exceptional situations by raising the special |
|
399 |
\emph{Interrupt} exception in user code. |
|
400 |
||
401 |
This is the one and only way that physical events can intrude an |
|
402 |
Isabelle/ML program. Such an interrupt can mean out-of-memory, |
|
403 |
stack overflow, timeout, internal signaling of threads, or the user |
|
404 |
producing a console interrupt manually. An Isabelle/ML program that |
|
405 |
intercepts interrupts becomes dependent on physical effects produced |
|
406 |
by the environment. Even worse, accidental use of exception |
|
407 |
handling patterns that are too general will cover interrupts |
|
408 |
unintentionally, and thus render the program semantics ill-defined. |
|
409 |
||
410 |
Note that the Interrupt exception dates back to the original SML90 |
|
411 |
language definition. It was excluded from the SML97 version to |
|
412 |
avoid its malign impact on ML program semantics, but without |
|
413 |
providing a viable alternative. Isabelle/ML recovers physical |
|
414 |
interruptibility (which an indispensable tool to implement managed |
|
415 |
evaluation of Isar command transactions), but requires user code to |
|
416 |
be strictly transparent wrt.\ interrupts. |
|
417 |
||
418 |
\begin{warn} |
|
419 |
Isabelle/ML user code needs to terminate promptly on interruption, |
|
420 |
without guessing at its meaning to the system infrastructure. |
|
421 |
Temporary handling of interrupts for cleanup of global resources |
|
422 |
etc.\ needs to be followed immediately by re-raising of the original |
|
423 |
exception. |
|
424 |
\end{warn} |
|
425 |
*} |
|
426 |
||
30270
61811c9224a6
dummy changes to produce a new changeset of these files;
wenzelm
parents:
29755
diff
changeset
|
427 |
end |