author | wenzelm |
Tue, 19 Oct 2010 21:01:34 +0100 | |
changeset 39872 | 2b88d00d6790 |
parent 39871 | b905971407a1 |
child 39874 | bbac63bbcffe |
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 |
||
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
81 |
text {* Here the ML environment is really managed by Isabelle, i.e.\ |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
82 |
the @{ML factorial} function is not yet accessible in the preceding |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
83 |
paragraph, nor in a different theory that is independent from the |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
84 |
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 |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
95 |
\medskip 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 |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
99 |
internal block structure. *} |
39823 | 100 |
|
101 |
example_proof |
|
39851 | 102 |
ML_prf %"ML" {* val a = 1 *} |
39824 | 103 |
{ -- {* Isar block structure ignored by ML environment *} |
39851 | 104 |
ML_prf %"ML" {* val b = a + 1 *} |
39824 | 105 |
} -- {* Isar block structure ignored by ML environment *} |
39851 | 106 |
ML_prf %"ML" {* val c = b + 1 *} |
39823 | 107 |
qed |
108 |
||
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
109 |
text {* By side-stepping the normal scoping rules for Isar proof |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
110 |
blocks, embedded ML code can refer to the different contexts |
39824 | 111 |
explicitly, and manipulate corresponding entities, e.g.\ export a |
112 |
fact from a block context. |
|
39823 | 113 |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
114 |
\medskip Two further ML commands are useful in certain situations: |
39824 | 115 |
@{command_ref ML_val} and @{command_ref ML_command} are both |
116 |
\emph{diagnostic} in the sense that there is no effect on the |
|
117 |
underlying environment, and can thus used anywhere (even outside a |
|
118 |
theory). The examples below produce long strings of digits by |
|
119 |
invoking @{ML factorial}: @{command ML_val} already takes care of |
|
120 |
printing the ML toplevel result, but @{command ML_command} is silent |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
121 |
so we produce an explicit output message. *} |
39823 | 122 |
|
123 |
ML_val {* factorial 100 *} |
|
124 |
ML_command {* writeln (string_of_int (factorial 100)) *} |
|
125 |
||
126 |
example_proof |
|
39824 | 127 |
ML_val {* factorial 100 *} (* FIXME check/fix indentation *) |
39823 | 128 |
ML_command {* writeln (string_of_int (factorial 100)) *} |
129 |
qed |
|
130 |
||
131 |
||
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
132 |
subsection {* Compile-time context *} |
39823 | 133 |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
134 |
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
|
135 |
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
|
136 |
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
|
137 |
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
|
138 |
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
|
139 |
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
|
140 |
*} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
141 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
142 |
text %mlref {* |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
143 |
\begin{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
144 |
@{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
|
145 |
@{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\ |
39850 | 146 |
@{index_ML bind_thms: "string * thm list -> unit"} \\ |
147 |
@{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
|
148 |
\end{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
149 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
150 |
\begin{description} |
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 |
\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
|
153 |
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
|
154 |
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
|
155 |
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
|
156 |
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
|
157 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
158 |
\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
|
159 |
@{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
|
160 |
|
39850 | 161 |
\item @{ML bind_thms}~@{text "(name, thms)"} stores a list of |
162 |
theorems produced in ML both in the (global) theory context and the |
|
163 |
ML toplevel, associating it with the provided name. Theorems are |
|
164 |
put into a global ``standard'' format before being stored. |
|
165 |
||
166 |
\item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a |
|
167 |
singleton theorem. |
|
168 |
||
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
169 |
\end{description} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
170 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
171 |
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
|
172 |
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
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
*} |
39823 | 177 |
|
178 |
||
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
179 |
subsection {* Antiquotations \label{sec:ML-antiq} *} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
180 |
|
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
181 |
text {* A very important consequence of embedding SML into Isar is the |
39829 | 182 |
concept of \emph{ML antiquotation}. First, the standard token |
183 |
language of ML is augmented by special syntactic entities of the |
|
184 |
following form: |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
185 |
|
39829 | 186 |
\indexouternonterm{antiquote} |
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
187 |
\begin{rail} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
188 |
antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
189 |
; |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
190 |
\end{rail} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
191 |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
192 |
Here @{syntax nameref} and @{syntax args} are regular outer syntax |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
193 |
categories. Note that attributes and proof methods use similar |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
194 |
syntax. |
39823 | 195 |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
196 |
\medskip A regular antiquotation @{text "@{name args}"} processes |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
197 |
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
|
198 |
produces corresponding ML source text, either as literal |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
199 |
\emph{inline} text (e.g. @{text "@{term t}"}) or abstract |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
200 |
\emph{value} (e.g. @{text "@{thm th}"}). This pre-compilation |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
201 |
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
|
202 |
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
|
203 |
small portions of the code. |
39823 | 204 |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
205 |
Special antiquotations like @{text "@{let \<dots>}"} or @{text "@{note |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
206 |
\<dots>}"} augment the compilation context without generating code. The |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
207 |
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
|
208 |
effect by introducing local blocks within the pre-compilation |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
209 |
environment. |
39829 | 210 |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
211 |
\medskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
212 |
perspective on Isabelle/ML antiquotations. *} |
39829 | 213 |
|
39830 | 214 |
text %mlantiq {* |
39829 | 215 |
\begin{matharray}{rcl} |
216 |
@{ML_antiquotation_def "let"} & : & @{text ML_antiquotation} \\ |
|
217 |
@{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\ |
|
218 |
\end{matharray} |
|
219 |
||
220 |
\begin{rail} |
|
221 |
'let' ((term + 'and') '=' term + 'and') |
|
222 |
; |
|
223 |
||
224 |
'note' (thmdef? thmrefs + 'and') |
|
225 |
; |
|
226 |
\end{rail} |
|
227 |
||
228 |
\begin{description} |
|
229 |
||
230 |
\item @{text "@{let p = t}"} binds schematic variables in the |
|
231 |
pattern @{text "p"} by higher-order matching against the term @{text |
|
232 |
"t"}. This is analogous to the regular @{command_ref let} command |
|
233 |
in the Isar proof language. The pre-compilation environment is |
|
234 |
augmented by auxiliary term bindings, without emitting ML source. |
|
235 |
||
236 |
\item @{text "@{note a = b\<^sub>1 \<dots> b\<^sub>n}"} recalls existing facts @{text |
|
237 |
"b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. This is analogous to |
|
238 |
the regular @{command_ref note} command in the Isar proof language. |
|
239 |
The pre-compilation environment is augmented by auxiliary fact |
|
240 |
bindings, without emitting ML source. |
|
241 |
||
242 |
\end{description} |
|
243 |
*} |
|
244 |
||
245 |
text %mlex {* The following artificial example gives a first |
|
246 |
impression about using the antiquotation elements introduced so far, |
|
247 |
together with the basic @{text "@{thm}"} antiquotation defined |
|
248 |
later. |
|
249 |
*} |
|
250 |
||
251 |
ML {* |
|
252 |
\<lbrace> |
|
253 |
@{let ?t = my_term} |
|
254 |
@{note my_refl = reflexive [of ?t]} |
|
255 |
fun foo th = Thm.transitive th @{thm my_refl} |
|
256 |
\<rbrace> |
|
257 |
*} |
|
258 |
||
259 |
text {* |
|
260 |
The extra block delimiters do not affect the compiled code itself, i.e.\ |
|
261 |
function @{ML foo} is available in the present context. |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
262 |
*} |
39823 | 263 |
|
39835 | 264 |
|
39854 | 265 |
section {* Message output channels \label{sec:message-channels} *} |
39835 | 266 |
|
267 |
text {* Isabelle provides output channels for different kinds of |
|
268 |
messages: regular output, high-volume tracing information, warnings, |
|
269 |
and errors. |
|
270 |
||
271 |
Depending on the user interface involved, these messages may appear |
|
272 |
in different text styles or colours. The standard output for |
|
273 |
terminal sessions prefixes each line of warnings by @{verbatim |
|
274 |
"###"} and errors by @{verbatim "***"}, but leaves anything else |
|
275 |
unchanged. |
|
276 |
||
277 |
Messages are associated with the transaction context of the running |
|
278 |
Isar command. This enables the front-end to manage commands and |
|
279 |
resulting messages together. For example, after deleting a command |
|
280 |
from a given theory document version, the corresponding message |
|
39872 | 281 |
output can be retracted from the display. |
282 |
*} |
|
39835 | 283 |
|
284 |
text %mlref {* |
|
285 |
\begin{mldecls} |
|
286 |
@{index_ML writeln: "string -> unit"} \\ |
|
287 |
@{index_ML tracing: "string -> unit"} \\ |
|
288 |
@{index_ML warning: "string -> unit"} \\ |
|
289 |
@{index_ML error: "string -> 'a"} \\ |
|
290 |
\end{mldecls} |
|
291 |
||
292 |
\begin{description} |
|
293 |
||
294 |
\item @{ML writeln}~@{text "text"} outputs @{text "text"} as regular |
|
295 |
message. This is the primary message output operation of Isabelle |
|
296 |
and should be used by default. |
|
297 |
||
298 |
\item @{ML tracing}~@{text "text"} outputs @{text "text"} as special |
|
299 |
tracing message, indicating potential high-volume output to the |
|
300 |
front-end (hundreds or thousands of messages issued by a single |
|
301 |
command). The idea is to allow the user-interface to downgrade the |
|
302 |
quality of message display to achieve higher throughput. |
|
303 |
||
304 |
Note that the user might have to take special actions to see tracing |
|
305 |
output, e.g.\ switch to a different output window. So this channel |
|
306 |
should not be used for regular output. |
|
307 |
||
308 |
\item @{ML warning}~@{text "text"} outputs @{text "text"} as |
|
309 |
warning, which typically means some extra emphasis on the front-end |
|
310 |
side (color highlighting, icon). |
|
311 |
||
312 |
\item @{ML error}~@{text "text"} raises exception @{ML ERROR}~@{text |
|
313 |
"text"} and thus lets the Isar toplevel print @{text "text"} on the |
|
314 |
error channel, which typically means some extra emphasis on the |
|
315 |
front-end side (color highlighting, icon). |
|
316 |
||
317 |
This assumes that the exception is not handled before the command |
|
318 |
terminates. Handling exception @{ML ERROR}~@{text "text"} is a |
|
319 |
perfectly legal alternative: it means that the error is absorbed |
|
320 |
without any message output. |
|
321 |
||
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
322 |
\begin{warn} |
39835 | 323 |
The actual error channel is accessed via @{ML Output.error_msg}, but |
324 |
the interaction protocol of Proof~General \emph{crashes} if that |
|
325 |
function is used in regular ML code: error output and toplevel |
|
326 |
command failure always need to coincide here. |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
327 |
\end{warn} |
39835 | 328 |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
329 |
\end{description} |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
330 |
|
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
331 |
\begin{warn} |
39835 | 332 |
Regular Isabelle/ML code should output messages exclusively by the |
333 |
official channels. Using raw I/O on \emph{stdout} or \emph{stderr} |
|
334 |
instead (e.g.\ via @{ML TextIO.output}) is apt to cause problems in |
|
335 |
the presence of parallel and asynchronous processing of Isabelle |
|
336 |
theories. Such raw output might be displayed by the front-end in |
|
337 |
some system console log, with a low chance that the user will ever |
|
338 |
see it. Moreover, as a genuine side-effect on global process |
|
339 |
channels, there is no proper way to retract output when Isar command |
|
340 |
transactions are reset. |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
341 |
\end{warn} |
39872 | 342 |
|
343 |
\begin{warn} |
|
344 |
The message channels should be used in a message-oriented manner. |
|
345 |
This means that multi-line output that logically belongs together |
|
346 |
needs to be issued by a \emph{single} invocation of @{ML writeln} |
|
347 |
etc. with the functional concatenation of all message constituents. |
|
348 |
\end{warn} |
|
349 |
*} |
|
350 |
||
351 |
text %mlex {* The following example demonstrates a multi-line |
|
352 |
warning. Note that in some situations the user sees only the first |
|
353 |
line, so the most important point should be made first. |
|
354 |
*} |
|
355 |
||
356 |
ML_command {* |
|
357 |
warning (cat_lines |
|
358 |
["Beware the Jabberwock, my son!", |
|
359 |
"The jaws that bite, the claws that catch!", |
|
360 |
"Beware the Jubjub Bird, and shun", |
|
361 |
"The frumious Bandersnatch!"]); |
|
39835 | 362 |
*} |
363 |
||
39854 | 364 |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
365 |
section {* Exceptions \label{sec:exceptions} *} |
39854 | 366 |
|
367 |
text {* The Standard ML semantics of strict functional evaluation |
|
368 |
together with exceptions is rather well defined, but some delicate |
|
369 |
points need to be observed to avoid that ML programs go wrong |
|
370 |
despite static type-checking. Exceptions in Isabelle/ML are |
|
371 |
subsequently categorized as follows. |
|
372 |
||
373 |
\paragraph{Regular user errors.} These are meant to provide |
|
374 |
informative feedback about malformed input etc. |
|
375 |
||
376 |
The \emph{error} function raises the corresponding \emph{ERROR} |
|
377 |
exception, with a plain text message as argument. \emph{ERROR} |
|
378 |
exceptions can be handled internally, in order to be ignored, turned |
|
379 |
into other exceptions, or cascaded by appending messages. If the |
|
380 |
corresponding Isabelle/Isar command terminates with an \emph{ERROR} |
|
39855 | 381 |
exception state, the toplevel will print the result on the error |
382 |
channel (see \secref{sec:message-channels}). |
|
39854 | 383 |
|
384 |
It is considered bad style to refer to internal function names or |
|
385 |
values in ML source notation in user error messages. |
|
386 |
||
387 |
Grammatical correctness of error messages can be improved by |
|
388 |
\emph{omitting} final punctuation: messages are often concatenated |
|
389 |
or put into a larger context (e.g.\ augmented with source position). |
|
390 |
By not insisting in the final word at the origin of the error, the |
|
391 |
system can perform its administrative tasks more easily and |
|
392 |
robustly. |
|
393 |
||
394 |
\paragraph{Program failures.} There is a handful of standard |
|
395 |
exceptions that indicate general failure situations, or failures of |
|
396 |
core operations on logical entities (types, terms, theorems, |
|
39856 | 397 |
theories, see \chref{ch:logic}). |
39854 | 398 |
|
399 |
These exceptions indicate a genuine breakdown of the program, so the |
|
400 |
main purpose is to determine quickly what has happened where. |
|
39855 | 401 |
Traditionally, the (short) exception message would include the name |
402 |
of an ML function, although this no longer necessary, because the ML |
|
403 |
runtime system prints a detailed source position of the |
|
404 |
corresponding @{verbatim raise} keyword. |
|
39854 | 405 |
|
406 |
\medskip User modules can always introduce their own custom |
|
407 |
exceptions locally, e.g.\ to organize internal failures robustly |
|
408 |
without overlapping with existing exceptions. Exceptions that are |
|
409 |
exposed in module signatures require extra care, though, and should |
|
410 |
\emph{not} be introduced by default. Surprise by end-users or ML |
|
39855 | 411 |
users of a module can be often minimized by using plain user errors. |
39854 | 412 |
|
413 |
\paragraph{Interrupts.} These indicate arbitrary system events: |
|
414 |
both the ML runtime system and the Isabelle/ML infrastructure signal |
|
415 |
various exceptional situations by raising the special |
|
416 |
\emph{Interrupt} exception in user code. |
|
417 |
||
418 |
This is the one and only way that physical events can intrude an |
|
419 |
Isabelle/ML program. Such an interrupt can mean out-of-memory, |
|
420 |
stack overflow, timeout, internal signaling of threads, or the user |
|
39855 | 421 |
producing a console interrupt manually etc. An Isabelle/ML program |
422 |
that intercepts interrupts becomes dependent on physical effects of |
|
423 |
the environment. Even worse, exception handling patterns that are |
|
424 |
too general by accident, e.g.\ by mispelled exception constructors, |
|
425 |
will cover interrupts unintentionally, and thus render the program |
|
426 |
semantics ill-defined. |
|
39854 | 427 |
|
428 |
Note that the Interrupt exception dates back to the original SML90 |
|
429 |
language definition. It was excluded from the SML97 version to |
|
430 |
avoid its malign impact on ML program semantics, but without |
|
431 |
providing a viable alternative. Isabelle/ML recovers physical |
|
432 |
interruptibility (which an indispensable tool to implement managed |
|
433 |
evaluation of Isar command transactions), but requires user code to |
|
434 |
be strictly transparent wrt.\ interrupts. |
|
435 |
||
436 |
\begin{warn} |
|
437 |
Isabelle/ML user code needs to terminate promptly on interruption, |
|
438 |
without guessing at its meaning to the system infrastructure. |
|
439 |
Temporary handling of interrupts for cleanup of global resources |
|
440 |
etc.\ needs to be followed immediately by re-raising of the original |
|
441 |
exception. |
|
442 |
\end{warn} |
|
443 |
*} |
|
444 |
||
39855 | 445 |
text %mlref {* |
446 |
\begin{mldecls} |
|
447 |
@{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\ |
|
448 |
@{index_ML can: "('a -> 'b) -> 'a -> bool"} \\ |
|
39856 | 449 |
@{index_ML ERROR: "string -> exn"} \\ |
450 |
@{index_ML Fail: "string -> exn"} \\ |
|
451 |
@{index_ML Exn.is_interrupt: "exn -> bool"} \\ |
|
39855 | 452 |
@{index_ML reraise: "exn -> 'a"} \\ |
453 |
@{index_ML exception_trace: "(unit -> 'a) -> 'a"} \\ |
|
454 |
\end{mldecls} |
|
455 |
||
456 |
\begin{description} |
|
457 |
||
458 |
\item @{ML try}~@{text "f x"} makes the partiality of evaluating |
|
459 |
@{text "f x"} explicit via the option datatype. Interrupts are |
|
460 |
\emph{not} handled here, i.e.\ this form serves as safe replacement |
|
461 |
for the \emph{unsafe} version @{verbatim "(SOME"}~@{text "f |
|
462 |
x"}~@{verbatim "handle _ => NONE)"} that is occasionally seen in |
|
463 |
books about SML. |
|
464 |
||
465 |
\item @{ML can} is similar to @{ML try} with more abstract result. |
|
466 |
||
39856 | 467 |
\item @{ML ERROR}~@{text "msg"} represents user errors; this |
468 |
exception is always raised via the @{ML error} function (see |
|
469 |
\secref{sec:message-channels}). |
|
470 |
||
471 |
\item @{ML Fail}~@{text "msg"} represents general program failures. |
|
472 |
||
473 |
\item @{ML Exn.is_interrupt} identifies interrupts robustly, without |
|
474 |
mentioning concrete exception constructors in user code. Handled |
|
475 |
interrupts need to be re-raised promptly! |
|
476 |
||
39855 | 477 |
\item @{ML reraise}~@{text "exn"} raises exception @{text "exn"} |
478 |
while preserving its implicit position information (if possible, |
|
479 |
depending on the ML platform). |
|
480 |
||
481 |
\item @{ML exception_trace}~@{verbatim "(fn _ =>"}~@{text |
|
482 |
"e"}@{verbatim ")"} evaluates expression @{text "e"} while printing |
|
483 |
a full trace of its stack of nested exceptions (if possible, |
|
484 |
depending on the ML platform).\footnote{In various versions of |
|
485 |
Poly/ML the trace will appear on raw stdout of the Isabelle |
|
486 |
process.} |
|
487 |
||
488 |
Inserting @{ML exception_trace} into ML code temporarily is useful |
|
489 |
for debugging, but not suitable for production code. |
|
490 |
||
491 |
\end{description} |
|
492 |
*} |
|
493 |
||
39866
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
494 |
text %mlantiq {* |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
495 |
\begin{matharray}{rcl} |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
496 |
@{ML_antiquotation_def "assert"} & : & @{text ML_antiquotation} \\ |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
497 |
\end{matharray} |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
498 |
|
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
499 |
\begin{description} |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
500 |
|
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
501 |
\item @{text "@{assert}"} inlines a function @{text "bool \<Rightarrow> unit"} |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
502 |
that raises @{ML Fail} if the argument is @{ML false}. Due to |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
503 |
inlining the source position of failed assertions is included in the |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
504 |
error output. |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
505 |
|
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
506 |
\end{description} |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
507 |
*} |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
508 |
|
39859 | 509 |
|
39863 | 510 |
section {* Basic data types *} |
39859 | 511 |
|
512 |
text {* The basis library proposal of SML97 need to be treated with |
|
513 |
caution. Many of its operations simply do not fit with important |
|
514 |
Isabelle/ML conventions (like ``canonical argument order'', see |
|
515 |
\secref{sec:canonical-argument-order}), others can cause serious |
|
516 |
problems with the parallel evaluation model of Isabelle/ML (such as |
|
517 |
@{ML TextIO.print} or @{ML OS.Process.system}). |
|
518 |
||
519 |
Subsequently we give a brief overview of important operations on |
|
520 |
basic ML data types. |
|
521 |
*} |
|
522 |
||
523 |
||
39863 | 524 |
subsection {* Characters *} |
525 |
||
526 |
text %mlref {* |
|
527 |
\begin{mldecls} |
|
528 |
@{index_ML_type char} \\ |
|
529 |
\end{mldecls} |
|
530 |
||
531 |
\begin{description} |
|
532 |
||
39864 | 533 |
\item Type @{ML_type char} is \emph{not} used. The smallest textual |
534 |
unit in Isabelle is represented a ``symbol'' (see |
|
535 |
\secref{sec:symbols}). |
|
39863 | 536 |
|
537 |
\end{description} |
|
538 |
*} |
|
539 |
||
540 |
||
39862 | 541 |
subsection {* Integers *} |
542 |
||
543 |
text %mlref {* |
|
544 |
\begin{mldecls} |
|
545 |
@{index_ML_type int} \\ |
|
546 |
\end{mldecls} |
|
547 |
||
548 |
\begin{description} |
|
549 |
||
39864 | 550 |
\item Type @{ML_type int} represents regular mathematical integers, |
551 |
which are \emph{unbounded}. Overflow never happens in |
|
39862 | 552 |
practice.\footnote{The size limit for integer bit patterns in memory |
553 |
is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.} |
|
554 |
This works uniformly for all supported ML platforms (Poly/ML and |
|
555 |
SML/NJ). |
|
556 |
||
557 |
Literal integers in ML text (e.g.\ @{ML |
|
558 |
123456789012345678901234567890}) are forced to be of this one true |
|
559 |
integer type --- overloading of SML97 is disabled. |
|
560 |
||
561 |
Structure @{ML_struct IntInf} of SML97 is obsolete, always use |
|
562 |
@{ML_struct Int}. Structure @{ML_struct Integer} in @{"file" |
|
563 |
"~~/src/Pure/General/integer.ML"} provides some additional |
|
564 |
operations. |
|
565 |
||
566 |
\end{description} |
|
567 |
*} |
|
568 |
||
569 |
||
39859 | 570 |
subsection {* Options *} |
571 |
||
572 |
text %mlref {* |
|
573 |
\begin{mldecls} |
|
574 |
@{index_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\ |
|
575 |
@{index_ML is_some: "'a option -> bool"} \\ |
|
576 |
@{index_ML is_none: "'a option -> bool"} \\ |
|
577 |
@{index_ML the: "'a option -> 'a"} \\ |
|
578 |
@{index_ML these: "'a list option -> 'a list"} \\ |
|
579 |
@{index_ML the_list: "'a option -> 'a list"} \\ |
|
580 |
@{index_ML the_default: "'a -> 'a option -> 'a"} \\ |
|
581 |
\end{mldecls} |
|
582 |
*} |
|
583 |
||
584 |
text {* Apart from @{ML Option.map} most operations defined in |
|
585 |
structure @{ML_struct Option} are alien to Isabelle/ML. The |
|
586 |
operations shown above are defined in @{"file" |
|
587 |
"~~/src/Pure/General/basics.ML"}, among others. *} |
|
588 |
||
589 |
||
39863 | 590 |
subsection {* Lists *} |
591 |
||
592 |
text {* Lists are ubiquitous in ML as simple and light-weight |
|
593 |
``collections'' for many everyday programming tasks. Isabelle/ML |
|
594 |
provides some important refinements over the predefined operations |
|
595 |
in SML97. *} |
|
596 |
||
597 |
text %mlref {* |
|
598 |
\begin{mldecls} |
|
599 |
@{index_ML cons: "'a -> 'a list -> 'a list"} \\ |
|
600 |
\end{mldecls} |
|
601 |
||
602 |
\begin{description} |
|
603 |
||
604 |
\item @{ML cons}~@{text "x xs"} evaluates to @{text "x :: xs"}. |
|
605 |
||
606 |
Tupled infix operators are a historical accident in Standard ML. |
|
607 |
The curried @{ML cons} amends this, but it should be only used when |
|
608 |
partial application is required. |
|
609 |
||
610 |
\end{description} |
|
611 |
*} |
|
612 |
||
613 |
||
614 |
subsubsection {* Canonical iteration *} |
|
615 |
||
616 |
text {* A function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be understood as update |
|
617 |
on a configuration of type @{text "\<beta>"} that is parametrized by |
|
618 |
arguments of type @{text "\<alpha>"}. Given @{text "a: \<alpha>"} the partial |
|
619 |
application @{text "(f a): \<beta> \<rightarrow> \<beta>"} operates homogeneously on @{text |
|
620 |
"\<beta>"}. This can be iterated naturally over a list of parameters |
|
621 |
@{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1; \<dots>; f a\<^bsub>n\<^esub>\<^bsub>\<^esub>"} (where the |
|
622 |
semicolon represents left-to-right composition). The latter |
|
623 |
expression is again a function @{text "\<beta> \<rightarrow> \<beta>"}. It can be applied |
|
624 |
to an initial configuration @{text "b: \<beta>"} to start the iteration |
|
625 |
over the given list of arguments: each @{text "a"} in @{text "a\<^sub>1, \<dots>, |
|
626 |
a\<^sub>n"} is applied consecutively by updating a cumulative |
|
627 |
configuration. |
|
628 |
||
629 |
The @{text fold} combinator in Isabelle/ML lifts a function @{text |
|
630 |
"f"} as above to its iterated version over a list of arguments. |
|
631 |
Lifting can be repeated, e.g.\ @{text "(fold \<circ> fold) f"} iterates |
|
632 |
over a list of lists as expected. |
|
633 |
||
634 |
The variant @{text "fold_rev"} works inside-out over the list of |
|
635 |
arguments, such that @{text "fold_rev f \<equiv> fold f \<circ> rev"} holds. |
|
636 |
||
637 |
The @{text "fold_map"} combinator essentially performs @{text |
|
638 |
"fold"} and @{text "map"} simultaneously: each application of @{text |
|
639 |
"f"} produces an updated configuration together with a side-result; |
|
640 |
the iteration collects all such side-results as a separate list. |
|
641 |
*} |
|
642 |
||
643 |
text %mlref {* |
|
644 |
\begin{mldecls} |
|
645 |
@{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ |
|
646 |
@{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ |
|
647 |
@{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\ |
|
648 |
\end{mldecls} |
|
649 |
||
650 |
\begin{description} |
|
651 |
||
652 |
\item @{ML fold}~@{text f} lifts the parametrized update function |
|
653 |
@{text "f"} to a list of parameters. |
|
654 |
||
655 |
\item @{ML fold_rev}~@{text "f"} is similar to @{ML fold}~@{text |
|
656 |
"f"}, but works inside-out. |
|
657 |
||
658 |
\item @{ML fold_map}~@{text "f"} lifts the parametrized update |
|
659 |
function @{text "f"} (with side-result) to a list of parameters and |
|
660 |
cumulative side-results. |
|
661 |
||
662 |
\end{description} |
|
663 |
||
664 |
\begin{warn} |
|
665 |
The literature on functional programming provides a multitude of |
|
666 |
combinators called @{text "foldl"}, @{text "foldr"} etc. SML97 |
|
667 |
provides its own variations as @{ML List.foldl} and @{ML |
|
668 |
List.foldr}, while the classic Isabelle library still has the |
|
669 |
slightly more convenient historic @{ML Library.foldl} and @{ML |
|
670 |
Library.foldr}. To avoid further confusion, all of this should be |
|
671 |
ignored, and @{ML fold} (or @{ML fold_rev}) used exclusively. |
|
672 |
\end{warn} |
|
673 |
*} |
|
674 |
||
675 |
text %mlex {* Using canonical @{ML fold} together with canonical @{ML |
|
676 |
cons}, or similar standard operations, alternates the orientation of |
|
677 |
data. The is quite natural and should not altered forcible by |
|
678 |
inserting extra applications @{ML rev}. The alternative @{ML |
|
679 |
fold_rev} can be used in the relatively few situations, where |
|
680 |
alternation should be prevented. |
|
681 |
*} |
|
682 |
||
683 |
ML {* |
|
684 |
val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]; |
|
685 |
||
686 |
val list1 = fold cons items []; |
|
39866
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
687 |
@{assert} (list1 = rev items); |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
688 |
|
39863 | 689 |
val list2 = fold_rev cons items []; |
39866
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
690 |
@{assert} (list2 = items); |
39863 | 691 |
*} |
692 |
||
693 |
||
39859 | 694 |
subsection {* Unsynchronized references *} |
695 |
||
696 |
text %mlref {* |
|
697 |
\begin{mldecls} |
|
39870 | 698 |
@{index_ML_type "'a Unsynchronized.ref"} \\ |
39859 | 699 |
@{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\ |
700 |
@{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\ |
|
701 |
@{index_ML "op :=": "'a Unsynchronized.ref * 'a -> unit"} \\ |
|
702 |
\end{mldecls} |
|
703 |
*} |
|
704 |
||
705 |
text {* Due to ubiquitous parallelism in Isabelle/ML (see also |
|
706 |
\secref{sec:multi-threading}), the mutable reference cells of |
|
707 |
Standard ML are notorious for causing problems. In a highly |
|
708 |
parallel system, both correctness \emph{and} performance are easily |
|
709 |
degraded when using mutable data. |
|
710 |
||
711 |
The unwieldy name of @{ML Unsynchronized.ref} for the constructor |
|
712 |
for references in Isabelle/ML emphasizes the inconveniences caused by |
|
713 |
mutability. Existing operations @{ML "!"} and @{ML "op :="} are |
|
714 |
unchanged, but should be used with special precautions, say in a |
|
715 |
strictly local situation that is guaranteed to be restricted to |
|
39870 | 716 |
sequential evaluation --- now and in the future. *} |
39859 | 717 |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
718 |
|
39870 | 719 |
section {* Thread-safe programming \label{sec:multi-threading} *} |
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
720 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
721 |
text {* Multi-threaded execution has become an everyday reality in |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
722 |
Isabelle since Poly/ML 5.2.1 and Isabelle2008. Isabelle/ML provides |
39868 | 723 |
implicit and explicit parallelism by default, and there is no way |
724 |
for user-space tools to ``opt out''. ML programs that are purely |
|
725 |
functional, output messages only via the official channels |
|
726 |
(\secref{sec:message-channels}), and do not intercept interrupts |
|
727 |
(\secref{sec:exceptions}) can participate in the multi-threaded |
|
728 |
environment immediately without further ado. |
|
729 |
||
730 |
More ambitious tools with more fine-grained interaction with the |
|
731 |
environment need to observe the principles explained below. |
|
732 |
*} |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
733 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
734 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
735 |
subsection {* Multi-threading with shared memory *} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
736 |
|
39868 | 737 |
text {* Multiple threads help to organize advanced operations of the |
738 |
system, such as real-time conditions on command transactions, |
|
739 |
sub-components with explicit communication, general asynchronous |
|
740 |
interaction etc. Moreover, parallel evaluation is a prerequisite to |
|
741 |
make adequate use of the CPU resources that are available on |
|
742 |
multi-core systems.\footnote{Multi-core computing does not mean that |
|
743 |
there are ``spare cycles'' to be wasted. It means that the |
|
744 |
continued exponential speedup of CPU performance due to ``Moore's |
|
745 |
Law'' follows different rules: clock frequency has reached its peak |
|
746 |
around 2005, and applications need to be parallelized in order to |
|
747 |
avoid a perceived loss of performance. See also |
|
748 |
\cite{Sutter:2005}.} |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
749 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
750 |
Isabelle/Isar exploits the inherent structure of theories and proofs |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
751 |
to support \emph{implicit parallelism} to a large extent. LCF-style |
39868 | 752 |
theorem provides almost ideal conditions for that; see also |
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
753 |
\cite{Wenzel:2009}. This means, significant parts of theory and |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
754 |
proof checking is parallelized by default. A maximum speedup-factor |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
755 |
of 3.0 on 4 cores and 5.0 on 8 cores can be |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
756 |
expected.\footnote{Further scalability is limited due to garbage |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
757 |
collection, which is still sequential in Poly/ML 5.2/5.3/5.4. It |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
758 |
helps to provide initial heap space generously, using the |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
759 |
\texttt{-H} option. Initial heap size needs to be scaled-up |
39868 | 760 |
together with the number of CPU cores: approximately 1--2\,GB per |
761 |
core..} |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
762 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
763 |
\medskip ML threads lack the memory protection of separate |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
764 |
processes, and operate concurrently on shared heap memory. This has |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
765 |
the advantage that results of independent computations are |
39868 | 766 |
immediately available to other threads: abstract values can be |
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
767 |
passed between threads without copying or awkward serialization that |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
768 |
is typically required for explicit message passing between separate |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
769 |
processes. |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
770 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
771 |
To make shared-memory multi-threading work robustly and efficiently, |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
772 |
some programming guidelines need to be observed. While the ML |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
773 |
system is responsible to maintain basic integrity of the |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
774 |
representation of ML values in memory, the application programmer |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
775 |
needs to ensure that multi-threaded execution does not break the |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
776 |
intended semantics. |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
777 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
778 |
\begin{warn} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
779 |
To participate in implicit parallelism, tools need to be |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
780 |
thread-safe. A single ill-behaved tool can affect the stability and |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
781 |
performance of the whole system. |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
782 |
\end{warn} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
783 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
784 |
Apart from observing the principles of thread-safeness passively, |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
785 |
advanced tools may also exploit parallelism actively, e.g.\ by using |
39868 | 786 |
``future values'' (\secref{sec:futures}) or the more basic library |
787 |
functions for parallel list operations (\secref{sec:parlist}). |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
788 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
789 |
\begin{warn} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
790 |
Parallel computing resources are managed centrally by the |
39868 | 791 |
Isabelle/ML infrastructure. User programs must not fork their own |
792 |
ML threads to perform computations. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
793 |
\end{warn} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
794 |
*} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
795 |
|
39868 | 796 |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
797 |
subsection {* Critical shared resources *} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
798 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
799 |
text {* Thread-safeness is mainly concerned about concurrent |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
800 |
read/write access to shared resources, which are outside the purely |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
801 |
functional world of ML. This covers the following in particular. |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
802 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
803 |
\begin{itemize} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
804 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
805 |
\item Global references (or arrays), i.e.\ mutable memory cells that |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
806 |
persist over several invocations of associated |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
807 |
operations.\footnote{This is independent of the visibility of such |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
808 |
mutable values in the toplevel scope.} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
809 |
|
39868 | 810 |
\item Global state of the running Isabelle/ML process, i.e.\ raw I/O |
811 |
channels, environment variables, current working directory. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
812 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
813 |
\item Writable resources in the file-system that are shared among |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
814 |
different threads or other processes. |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
815 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
816 |
\end{itemize} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
817 |
|
39868 | 818 |
Isabelle/ML provides various mechanisms to avoid critical shared |
819 |
resources in most practical situations. As last resort there are |
|
820 |
some mechanisms for explicit synchronization. The following |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
821 |
guidelines help to make Isabelle/ML programs work smoothly in a |
39868 | 822 |
concurrent environment. |
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
823 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
824 |
\begin{itemize} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
825 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
826 |
\item Avoid global references altogether. Isabelle/Isar maintains a |
39868 | 827 |
uniform context that incorporates arbitrary data declared by user |
828 |
programs (\secref{sec:context-data}). This context is passed as |
|
829 |
plain value and user tools can get/map their own data in a purely |
|
830 |
functional manner. Configuration options within the context |
|
831 |
(\secref{sec:config-options}) provide simple drop-in replacements |
|
832 |
for formerly writable flags. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
833 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
834 |
\item Keep components with local state information re-entrant. |
39868 | 835 |
Instead of poking initial values into (private) global references, a |
836 |
new state record can be created on each invocation, and passed |
|
837 |
through any auxiliary functions of the component. The state record |
|
838 |
may well contain mutable references, without requiring any special |
|
839 |
synchronizations, as long as each invocation gets its own copy. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
840 |
|
39868 | 841 |
\item Avoid raw output on @{text "stdout"} or @{text "stderr"}. The |
842 |
Poly/ML library is thread-safe for each individual output operation, |
|
843 |
but the ordering of parallel invocations is arbitrary. This means |
|
844 |
raw output will appear on some system console with unpredictable |
|
845 |
interleaving of atomic chunks. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
846 |
|
39868 | 847 |
Note that this does not affect regular message output channels |
848 |
(\secref{sec:message-channels}). An official message is associated |
|
849 |
with the command transaction from where it originates, independently |
|
850 |
of other transactions. This means each running Isar command has |
|
851 |
effectively its own set of message channels, and interleaving can |
|
852 |
only happen when commands use parallelism internally (and only at |
|
853 |
message boundaries). |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
854 |
|
39868 | 855 |
\item Treat environment variables and the current working directory |
856 |
of the running process as strictly read-only. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
857 |
|
39868 | 858 |
\item Restrict writing to the file-system to unique temporary files. |
859 |
Isabelle already provides a temporary directory that is unique for |
|
860 |
the running process, and there is a centralized source of unique |
|
861 |
serial numbers in Isabelle/ML. Thus temporary files that are passed |
|
862 |
to to some external process will be always disjoint, and thus |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
863 |
thread-safe. |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
864 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
865 |
\end{itemize} |
39868 | 866 |
*} |
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
867 |
|
39868 | 868 |
text %mlref {* |
869 |
\begin{mldecls} |
|
870 |
@{index_ML File.tmp_path: "Path.T -> Path.T"} \\ |
|
871 |
@{index_ML serial_string: "unit -> string"} \\ |
|
872 |
\end{mldecls} |
|
873 |
||
874 |
\begin{description} |
|
875 |
||
876 |
\item @{ML File.tmp_path}~@{text "path"} relocates the base |
|
877 |
component of @{text "path"} into the unique temporary directory of |
|
878 |
the running Isabelle/ML process. |
|
879 |
||
880 |
\item @{ML serial_string}~@{text "()"} creates a new serial number |
|
881 |
that is unique over the runtime of the Isabelle/ML process. |
|
882 |
||
883 |
\end{description} |
|
884 |
*} |
|
885 |
||
886 |
text %mlex {* The following example shows how to create unique |
|
887 |
temporary file names. |
|
888 |
*} |
|
889 |
||
890 |
ML {* |
|
891 |
val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ())); |
|
892 |
val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ())); |
|
893 |
@{assert} (tmp1 <> tmp2); |
|
894 |
*} |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
895 |
|
39868 | 896 |
|
897 |
subsection {* Explicit synchronization *} |
|
898 |
||
899 |
text {* Isabelle/ML also provides some explicit synchronization |
|
900 |
mechanisms, for the rare situations where mutable shared resources |
|
901 |
are really required. These are based on the synchronizations |
|
902 |
primitives of Poly/ML, which have been adapted to the specific |
|
903 |
assumptions of the concurrent Isabelle/ML environment. User code |
|
904 |
must not use the Poly/ML primitives directly! |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
905 |
|
39868 | 906 |
\medskip The most basic synchronization concept is a single |
907 |
\emph{critical section} (also called ``monitor'' in the literature). |
|
908 |
A thread that enters the critical section prevents all other threads |
|
909 |
from doing the same. A thread that is already within the critical |
|
910 |
section may re-enter it in an idempotent manner. |
|
911 |
||
912 |
Such centralized locking is convenient, because it prevents |
|
913 |
deadlocks by construction. |
|
914 |
||
915 |
\medskip More fine-grained locking works via \emph{synchronized |
|
916 |
variables}. An explicit state component is associated with |
|
917 |
mechanisms for locking and signaling. There are operations to |
|
918 |
await a condition, change the state, and signal the change to all |
|
919 |
other waiting threads. |
|
920 |
||
921 |
Here the synchronized access to the state variable is \emph{not} |
|
922 |
re-entrant: direct or indirect nesting within the same thread will |
|
923 |
cause a deadlock! |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
924 |
*} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
925 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
926 |
text %mlref {* |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
927 |
\begin{mldecls} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
928 |
@{index_ML NAMED_CRITICAL: "string -> (unit -> 'a) -> 'a"} \\ |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
929 |
@{index_ML CRITICAL: "(unit -> 'a) -> 'a"} \\ |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
930 |
\end{mldecls} |
39871 | 931 |
\begin{mldecls} |
932 |
@{index_ML_type "'a Synchronized.var"} \\ |
|
933 |
@{index_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\ |
|
934 |
@{index_ML Synchronized.guarded_access: "'a Synchronized.var -> |
|
935 |
('a -> ('b * 'a) option) -> 'b"} \\ |
|
936 |
\end{mldecls} |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
937 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
938 |
\begin{description} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
939 |
|
39868 | 940 |
\item @{ML NAMED_CRITICAL}~@{text "name e"} evaluates @{text "e ()"} |
941 |
within the central critical section of Isabelle/ML. No other thread |
|
942 |
may do so at the same time, but non-critical parallel execution will |
|
39871 | 943 |
continue. The @{text "name"} argument is used for tracing and might |
39868 | 944 |
help to spot sources of congestion. |
945 |
||
946 |
Entering the critical section without contention is very fast, and |
|
947 |
several basic system operations do so frequently. Each thread |
|
948 |
should leave the critical section quickly, otherwise parallel |
|
949 |
performance may degrade. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
950 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
951 |
\item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
952 |
name argument. |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
953 |
|
39871 | 954 |
\item Type @{ML_type "'a Synchronized.var"} represents synchronized |
955 |
variables with state of type @{ML_type 'a}. |
|
956 |
||
957 |
\item @{ML Synchronized.var}~@{text "name x"} creates a synchronized |
|
958 |
variable that is initialized with value @{text "x"}. The @{text |
|
959 |
"name"} is used for tracing. |
|
960 |
||
961 |
\item @{ML Synchronized.guarded_access}~@{text "var f"} lets the |
|
962 |
function @{text "f"} operate within a critical section on the state |
|
963 |
@{text "x"} as follows: if @{text "f x"} produces @{ML NONE}, we |
|
964 |
continue to wait on the internal condition variable, expecting that |
|
965 |
some other thread will eventually change the content in a suitable |
|
966 |
manner; if @{text "f x"} produces @{ML SOME}~@{text "(y, x')"} we |
|
967 |
are satisfied and assign the new state value @{text "x'"}, broadcast |
|
968 |
a signal to all waiting threads on the associated condition |
|
969 |
variable, and return the result @{text "y"}. |
|
970 |
||
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
971 |
\end{description} |
39871 | 972 |
|
973 |
There are some further variants of the general @{ML |
|
974 |
Synchronized.guarded_access} combinator, see @{"file" |
|
975 |
"~~/src/Pure/Concurrent/synchronized.ML"} for details. |
|
976 |
*} |
|
977 |
||
978 |
text %mlex {* See @{"file" "~~/src/Pure/Concurrent/mailbox.ML"} how to |
|
979 |
implement a mailbox as synchronized variable over a purely |
|
980 |
functional queue. |
|
981 |
||
982 |
\medskip The following example implements a counter that produces |
|
983 |
positive integers that are unique over the runtime of the Isabelle |
|
984 |
process: |
|
985 |
*} |
|
986 |
||
987 |
ML {* |
|
988 |
local |
|
989 |
val counter = Synchronized.var "counter" 0; |
|
990 |
in |
|
991 |
fun next () = |
|
992 |
Synchronized.guarded_access counter |
|
993 |
(fn i => |
|
994 |
let val j = i + 1 |
|
995 |
in SOME (j, j) end); |
|
996 |
end; |
|
997 |
*} |
|
998 |
||
999 |
ML {* |
|
1000 |
val a = next (); |
|
1001 |
val b = next (); |
|
1002 |
@{assert} (a <> b); |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1003 |
*} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1004 |
|
30270
61811c9224a6
dummy changes to produce a new changeset of these files;
wenzelm
parents:
29755
diff
changeset
|
1005 |
end |