author | wenzelm |
Mon, 30 Nov 2020 19:08:58 +0100 | |
changeset 72793 | 35d200023993 |
parent 69597 | ff784d5a5bfb |
child 73552 | 08bef311d382 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
57347 | 2 |
|
29755 | 3 |
theory "ML" |
4 |
imports Base |
|
5 |
begin |
|
18538 | 6 |
|
58618 | 7 |
chapter \<open>Isabelle/ML\<close> |
8 |
||
61854 | 9 |
text \<open> |
10 |
Isabelle/ML is best understood as a certain culture based on Standard ML. |
|
11 |
Thus it is not a new programming language, but a certain way to use SML at |
|
12 |
an advanced level within the Isabelle environment. This covers a variety of |
|
13 |
aspects that are geared towards an efficient and robust platform for |
|
14 |
applications of formal logic with fully foundational proof construction --- |
|
15 |
according to the well-known \<^emph>\<open>LCF principle\<close>. There is specific |
|
16 |
infrastructure with library modules to address the needs of this difficult |
|
17 |
task. For example, the raw parallel programming model of Poly/ML is |
|
18 |
presented as considerably more abstract concept of \<^emph>\<open>futures\<close>, which is then |
|
19 |
used to augment the inference kernel, Isar theory and proof interpreter, and |
|
20 |
PIDE document management. |
|
39823 | 21 |
|
61854 | 22 |
The main aspects of Isabelle/ML are introduced below. These first-hand |
23 |
explanations should help to understand how proper Isabelle/ML is to be read |
|
24 |
and written, and to get access to the wealth of experience that is expressed |
|
63680 | 25 |
in the source text and its history of changes.\<^footnote>\<open>See |
67744 | 26 |
\<^url>\<open>https://isabelle.in.tum.de/repos/isabelle\<close> for the full Mercurial history. |
61854 | 27 |
There are symbolic tags to refer to official Isabelle releases, as opposed |
28 |
to arbitrary \<^emph>\<open>tip\<close> versions that merely reflect snapshots that are never |
|
29 |
really up-to-date.\<close> |
|
30 |
\<close> |
|
58618 | 31 |
|
32 |
||
33 |
section \<open>Style and orthography\<close> |
|
34 |
||
61854 | 35 |
text \<open> |
36 |
The sources of Isabelle/Isar are optimized for \<^emph>\<open>readability\<close> and |
|
37 |
\<^emph>\<open>maintainability\<close>. The main purpose is to tell an informed reader what is |
|
38 |
really going on and how things really work. This is a non-trivial aim, but |
|
39 |
it is supported by a certain style of writing Isabelle/ML that has emerged |
|
40 |
from long years of system development.\<^footnote>\<open>See also the interesting style guide |
|
68224 | 41 |
for OCaml \<^url>\<open>https://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close> |
63680 | 42 |
which shares many of our means and ends.\<close> |
39878 | 43 |
|
61854 | 44 |
The main principle behind any coding style is \<^emph>\<open>consistency\<close>. For a single |
45 |
author of a small program this merely means ``choose your style and stick to |
|
46 |
it''. A complex project like Isabelle, with long years of development and |
|
47 |
different contributors, requires more standardization. A coding style that |
|
48 |
is changed every few years or with every new contributor is no style at all, |
|
49 |
because consistency is quickly lost. Global consistency is hard to achieve, |
|
50 |
though. Nonetheless, one should always strive at least for local consistency |
|
51 |
of modules and sub-systems, without deviating from some general principles |
|
52 |
how to write Isabelle/ML. |
|
39878 | 53 |
|
61854 | 54 |
In a sense, good coding style is like an \<^emph>\<open>orthography\<close> for the sources: it |
55 |
helps to read quickly over the text and see through the main points, without |
|
56 |
getting distracted by accidental presentation of free-style code. |
|
58618 | 57 |
\<close> |
58 |
||
59 |
||
60 |
subsection \<open>Header and sectioning\<close> |
|
61 |
||
61854 | 62 |
text \<open> |
63 |
Isabelle source files have a certain standardized header format (with |
|
64 |
precise spacing) that follows ancient traditions reaching back to the |
|
63680 | 65 |
earliest versions of the system by Larry Paulson. See |
66 |
\<^file>\<open>~~/src/Pure/thm.ML\<close>, for example. |
|
39878 | 67 |
|
61854 | 68 |
The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries, followed by a |
69 |
prose description of the purpose of the module. The latter can range from a |
|
70 |
single line to several paragraphs of explanations. |
|
39878 | 71 |
|
63610 | 72 |
The rest of the file is divided into chapters, sections, subsections, |
73 |
subsubsections, paragraphs etc.\ using a simple layout via ML comments as |
|
74 |
follows. |
|
39878 | 75 |
|
61458 | 76 |
@{verbatim [display] |
63610 | 77 |
\<open> (**** chapter ****) |
78 |
||
79 |
(*** section ***) |
|
58723 | 80 |
|
81 |
(** subsection **) |
|
82 |
||
83 |
(* subsubsection *) |
|
84 |
||
85 |
(*short paragraph*) |
|
86 |
||
87 |
(* |
|
88 |
long paragraph, |
|
89 |
with more text |
|
61458 | 90 |
*)\<close>} |
39878 | 91 |
|
61854 | 92 |
As in regular typography, there is some extra space \<^emph>\<open>before\<close> section |
93 |
headings that are adjacent to plain text, but not other headings as in the |
|
94 |
example above. |
|
39878 | 95 |
|
61416 | 96 |
\<^medskip> |
61854 | 97 |
The precise wording of the prose text given in these headings is chosen |
98 |
carefully to introduce the main theme of the subsequent formal ML text. |
|
58618 | 99 |
\<close> |
100 |
||
101 |
||
102 |
subsection \<open>Naming conventions\<close> |
|
103 |
||
61854 | 104 |
text \<open> |
105 |
Since ML is the primary medium to express the meaning of the source text, |
|
106 |
naming of ML entities requires special care. |
|
107 |
\<close> |
|
61506 | 108 |
|
109 |
paragraph \<open>Notation.\<close> |
|
61854 | 110 |
text \<open> |
111 |
A name consists of 1--3 \<^emph>\<open>words\<close> (rarely 4, but not more) that are separated |
|
112 |
by underscore. There are three variants concerning upper or lower case |
|
113 |
letters, which are used for certain ML categories as follows: |
|
39880 | 114 |
|
61416 | 115 |
\<^medskip> |
39880 | 116 |
\begin{tabular}{lll} |
117 |
variant & example & ML categories \\\hline |
|
69597 | 118 |
lower-case & \<^ML_text>\<open>foo_bar\<close> & values, types, record fields \\ |
119 |
capitalized & \<^ML_text>\<open>Foo_Bar\<close> & datatype constructors, structures, functors \\ |
|
120 |
upper-case & \<^ML_text>\<open>FOO_BAR\<close> & special values, exception constructors, signatures \\ |
|
39880 | 121 |
\end{tabular} |
61416 | 122 |
\<^medskip> |
39880 | 123 |
|
61854 | 124 |
For historical reasons, many capitalized names omit underscores, e.g.\ |
69597 | 125 |
old-style \<^ML_text>\<open>FooBar\<close> instead of \<^ML_text>\<open>Foo_Bar\<close>. Genuine |
61854 | 126 |
mixed-case names are \<^emph>\<open>not\<close> used, because clear division of words is |
127 |
essential for readability.\<^footnote>\<open>Camel-case was invented to workaround the lack |
|
128 |
of underscore in some early non-ASCII character sets. Later it became |
|
129 |
habitual in some language communities that are now strong in numbers.\<close> |
|
39880 | 130 |
|
61854 | 131 |
A single (capital) character does not count as ``word'' in this respect: |
69597 | 132 |
some Isabelle/ML names are suffixed by extra markers like this: \<^ML_text>\<open>foo_barT\<close>. |
133 |
||
134 |
Name variants are produced by adding 1--3 primes, e.g.\ \<^ML_text>\<open>foo'\<close>, |
|
135 |
\<^ML_text>\<open>foo''\<close>, or \<^ML_text>\<open>foo'''\<close>, but not \<^ML_text>\<open>foo''''\<close> or more. |
|
136 |
Decimal digits scale better to larger numbers, e.g.\ \<^ML_text>\<open>foo0\<close>, |
|
137 |
\<^ML_text>\<open>foo1\<close>, \<^ML_text>\<open>foo42\<close>. |
|
61506 | 138 |
\<close> |
139 |
||
64464 | 140 |
paragraph \<open>Scopes.\<close> |
61854 | 141 |
text \<open> |
142 |
Apart from very basic library modules, ML structures are not ``opened'', but |
|
69597 | 143 |
names are referenced with explicit qualification, as in \<^ML>\<open>Syntax.string_of_term\<close> for example. When devising names for structures and |
61506 | 144 |
their components it is important to aim at eye-catching compositions of both |
145 |
parts, because this is how they are seen in the sources and documentation. |
|
146 |
For the same reasons, aliases of well-known library functions should be |
|
40126 | 147 |
avoided. |
39880 | 148 |
|
61854 | 149 |
Local names of function abstraction or case/let bindings are typically |
150 |
shorter, sometimes using only rudiments of ``words'', while still avoiding |
|
69597 | 151 |
cryptic shorthands. An auxiliary function called \<^ML_text>\<open>helper\<close>, |
152 |
\<^ML_text>\<open>aux\<close>, or \<^ML_text>\<open>f\<close> is considered bad style. |
|
39880 | 153 |
|
154 |
Example: |
|
155 |
||
61458 | 156 |
@{verbatim [display] |
157 |
\<open> (* RIGHT *) |
|
39880 | 158 |
|
159 |
fun print_foo ctxt foo = |
|
160 |
let |
|
39881 | 161 |
fun print t = ... Syntax.string_of_term ctxt t ... |
162 |
in ... end; |
|
163 |
||
164 |
||
165 |
(* RIGHT *) |
|
166 |
||
167 |
fun print_foo ctxt foo = |
|
168 |
let |
|
39880 | 169 |
val string_of_term = Syntax.string_of_term ctxt; |
170 |
fun print t = ... string_of_term t ... |
|
171 |
in ... end; |
|
172 |
||
173 |
||
174 |
(* WRONG *) |
|
175 |
||
176 |
val string_of_term = Syntax.string_of_term; |
|
177 |
||
178 |
fun print_foo ctxt foo = |
|
179 |
let |
|
180 |
fun aux t = ... string_of_term ctxt t ... |
|
61458 | 181 |
in ... end;\<close>} |
61506 | 182 |
\<close> |
183 |
||
184 |
paragraph \<open>Specific conventions.\<close> |
|
61854 | 185 |
text \<open> |
186 |
Here are some specific name forms that occur frequently in the sources. |
|
39881 | 187 |
|
69597 | 188 |
\<^item> A function that maps \<^ML_text>\<open>foo\<close> to \<^ML_text>\<open>bar\<close> is called \<^ML_text>\<open>foo_to_bar\<close> or \<^ML_text>\<open>bar_of_foo\<close> (never \<^ML_text>\<open>foo2bar\<close>, nor |
189 |
\<^ML_text>\<open>bar_from_foo\<close>, nor \<^ML_text>\<open>bar_for_foo\<close>, nor \<^ML_text>\<open>bar4foo\<close>). |
|
190 |
||
191 |
\<^item> The name component \<^ML_text>\<open>legacy\<close> means that the operation is about to |
|
61854 | 192 |
be discontinued soon. |
39881 | 193 |
|
69597 | 194 |
\<^item> The name component \<^ML_text>\<open>global\<close> means that this works with the |
61854 | 195 |
background theory instead of the regular local context |
196 |
(\secref{sec:context}), sometimes for historical reasons, sometimes due a |
|
197 |
genuine lack of locality of the concept involved, sometimes as a fall-back |
|
198 |
for the lack of a proper context in the application code. Whenever there is |
|
199 |
a non-global variant available, the application should be migrated to use it |
|
200 |
with a proper local context. |
|
39881 | 201 |
|
61854 | 202 |
\<^item> Variables of the main context types of the Isabelle/Isar framework |
203 |
(\secref{sec:context} and \chref{ch:local-theory}) have firm naming |
|
204 |
conventions as follows: |
|
39881 | 205 |
|
69597 | 206 |
\<^item> theories are called \<^ML_text>\<open>thy\<close>, rarely \<^ML_text>\<open>theory\<close> |
207 |
(never \<^ML_text>\<open>thry\<close>) |
|
208 |
||
209 |
\<^item> proof contexts are called \<^ML_text>\<open>ctxt\<close>, rarely \<^ML_text>\<open>context\<close> (never \<^ML_text>\<open>ctx\<close>) |
|
210 |
||
211 |
\<^item> generic contexts are called \<^ML_text>\<open>context\<close> |
|
212 |
||
213 |
\<^item> local theories are called \<^ML_text>\<open>lthy\<close>, except for local |
|
61458 | 214 |
theories that are treated as proof context (which is a semantic |
215 |
super-type) |
|
39881 | 216 |
|
61854 | 217 |
Variations with primed or decimal numbers are always possible, as well as |
69597 | 218 |
semantic prefixes like \<^ML_text>\<open>foo_thy\<close> or \<^ML_text>\<open>bar_ctxt\<close>, but the |
61854 | 219 |
base conventions above need to be preserved. This allows to emphasize their |
220 |
data flow via plain regular expressions in the text editor. |
|
39881 | 221 |
|
61854 | 222 |
\<^item> The main logical entities (\secref{ch:logic}) have established naming |
223 |
convention as follows: |
|
39881 | 224 |
|
69597 | 225 |
\<^item> sorts are called \<^ML_text>\<open>S\<close> |
226 |
||
227 |
\<^item> types are called \<^ML_text>\<open>T\<close>, \<^ML_text>\<open>U\<close>, or \<^ML_text>\<open>ty\<close> (never |
|
228 |
\<^ML_text>\<open>t\<close>) |
|
229 |
||
230 |
\<^item> terms are called \<^ML_text>\<open>t\<close>, \<^ML_text>\<open>u\<close>, or \<^ML_text>\<open>tm\<close> (never |
|
231 |
\<^ML_text>\<open>trm\<close>) |
|
232 |
||
233 |
\<^item> certified types are called \<^ML_text>\<open>cT\<close>, rarely \<^ML_text>\<open>T\<close>, with |
|
61854 | 234 |
variants as for types |
61458 | 235 |
|
69597 | 236 |
\<^item> certified terms are called \<^ML_text>\<open>ct\<close>, rarely \<^ML_text>\<open>t\<close>, with |
237 |
variants as for terms (never \<^ML_text>\<open>ctrm\<close>) |
|
238 |
||
239 |
\<^item> theorems are called \<^ML_text>\<open>th\<close>, or \<^ML_text>\<open>thm\<close> |
|
39881 | 240 |
|
61854 | 241 |
Proper semantic names override these conventions completely. For example, |
69597 | 242 |
the left-hand side of an equation (as a term) can be called \<^ML_text>\<open>lhs\<close> |
243 |
(not \<^ML_text>\<open>lhs_tm\<close>). Or a term that is known to be a variable can be |
|
244 |
called \<^ML_text>\<open>v\<close> or \<^ML_text>\<open>x\<close>. |
|
39881 | 245 |
|
61854 | 246 |
\<^item> Tactics (\secref{sec:tactics}) are sufficiently important to have specific |
247 |
naming conventions. The name of a basic tactic definition always has a |
|
69597 | 248 |
\<^ML_text>\<open>_tac\<close> suffix, the subgoal index (if applicable) is always called |
249 |
\<^ML_text>\<open>i\<close>, and the goal state (if made explicit) is usually called |
|
250 |
\<^ML_text>\<open>st\<close> instead of the somewhat misleading \<^ML_text>\<open>thm\<close>. Any other |
|
61854 | 251 |
arguments are given before the latter two, and the general context is given |
252 |
first. Example: |
|
40310 | 253 |
|
61458 | 254 |
@{verbatim [display] \<open> fun my_tac ctxt arg1 arg2 i st = ...\<close>} |
40310 | 255 |
|
69597 | 256 |
Note that the goal state \<^ML_text>\<open>st\<close> above is rarely made explicit, if |
61854 | 257 |
tactic combinators (tacticals) are used as usual. |
40310 | 258 |
|
57421 | 259 |
A tactic that requires a proof context needs to make that explicit as seen |
61854 | 260 |
in the \<^verbatim>\<open>ctxt\<close> argument above. Do not refer to the background theory of |
261 |
\<^verbatim>\<open>st\<close> -- it is not a proper context, but merely a formal certificate. |
|
58618 | 262 |
\<close> |
263 |
||
264 |
||
265 |
subsection \<open>General source layout\<close> |
|
266 |
||
267 |
text \<open> |
|
57421 | 268 |
The general Isabelle/ML source layout imitates regular type-setting |
269 |
conventions, augmented by the requirements for deeply nested expressions |
|
61854 | 270 |
that are commonplace in functional programming. |
271 |
\<close> |
|
61506 | 272 |
|
273 |
paragraph \<open>Line length\<close> |
|
61854 | 274 |
text \<open> |
275 |
is limited to 80 characters according to ancient standards, but we allow as |
|
276 |
much as 100 characters (not more).\<^footnote>\<open>Readability requires to keep the |
|
277 |
beginning of a line in view while watching its end. Modern wide-screen |
|
61506 | 278 |
displays do not change the way how the human brain works. Sources also need |
61572 | 279 |
to be printable on plain paper with reasonable font-size.\<close> The extra 20 |
61506 | 280 |
characters acknowledge the space requirements due to qualified library |
61854 | 281 |
references in Isabelle/ML. |
282 |
\<close> |
|
61506 | 283 |
|
284 |
paragraph \<open>White-space\<close> |
|
61854 | 285 |
text \<open> |
286 |
is used to emphasize the structure of expressions, following mostly standard |
|
287 |
conventions for mathematical typesetting, as can be seen in plain {\TeX} or |
|
288 |
{\LaTeX}. This defines positioning of spaces for parentheses, punctuation, |
|
289 |
and infixes as illustrated here: |
|
39878 | 290 |
|
61458 | 291 |
@{verbatim [display] |
292 |
\<open> val x = y + z * (a + b); |
|
39878 | 293 |
val pair = (a, b); |
61458 | 294 |
val record = {foo = 1, bar = 2};\<close>} |
39878 | 295 |
|
61854 | 296 |
Lines are normally broken \<^emph>\<open>after\<close> an infix operator or punctuation |
297 |
character. For example: |
|
39878 | 298 |
|
61458 | 299 |
@{verbatim [display] |
300 |
\<open> |
|
39878 | 301 |
val x = |
302 |
a + |
|
303 |
b + |
|
304 |
c; |
|
305 |
||
306 |
val tuple = |
|
307 |
(a, |
|
308 |
b, |
|
309 |
c); |
|
61458 | 310 |
\<close>} |
39878 | 311 |
|
69597 | 312 |
Some special infixes (e.g.\ \<^ML_text>\<open>|>\<close>) work better at the start of the |
61854 | 313 |
line, but punctuation is always at the end. |
39878 | 314 |
|
61854 | 315 |
Function application follows the tradition of \<open>\<lambda>\<close>-calculus, not informal |
69597 | 316 |
mathematics. For example: \<^ML_text>\<open>f a b\<close> for a curried function, or |
317 |
\<^ML_text>\<open>g (a, b)\<close> for a tupled function. Note that the space between |
|
318 |
\<^ML_text>\<open>g\<close> and the pair \<^ML_text>\<open>(a, b)\<close> follows the important |
|
319 |
principle of \<^emph>\<open>compositionality\<close>: the layout of \<^ML_text>\<open>g p\<close> does not |
|
320 |
change when \<^ML_text>\<open>p\<close> is refined to the concrete pair \<^ML_text>\<open>(a, |
|
321 |
b)\<close>. |
|
61506 | 322 |
\<close> |
323 |
||
324 |
paragraph \<open>Indentation\<close> |
|
61854 | 325 |
text \<open> |
326 |
uses plain spaces, never hard tabulators.\<^footnote>\<open>Tabulators were invented to move |
|
327 |
the carriage of a type-writer to certain predefined positions. In software |
|
328 |
they could be used as a primitive run-length compression of consecutive |
|
329 |
spaces, but the precise result would depend on non-standardized text editor |
|
330 |
configuration.\<close> |
|
39878 | 331 |
|
61854 | 332 |
Each level of nesting is indented by 2 spaces, sometimes 1, very rarely 4, |
333 |
never 8 or any other odd number. |
|
39878 | 334 |
|
61854 | 335 |
Indentation follows a simple logical format that only depends on the nesting |
336 |
depth, not the accidental length of the text that initiates a level of |
|
337 |
nesting. Example: |
|
39878 | 338 |
|
61458 | 339 |
@{verbatim [display] |
340 |
\<open> (* RIGHT *) |
|
39880 | 341 |
|
39878 | 342 |
if b then |
39879 | 343 |
expr1_part1 |
344 |
expr1_part2 |
|
39878 | 345 |
else |
39879 | 346 |
expr2_part1 |
347 |
expr2_part2 |
|
39878 | 348 |
|
39880 | 349 |
|
350 |
(* WRONG *) |
|
351 |
||
39879 | 352 |
if b then expr1_part1 |
353 |
expr1_part2 |
|
354 |
else expr2_part1 |
|
61458 | 355 |
expr2_part2\<close>} |
39878 | 356 |
|
61854 | 357 |
The second form has many problems: it assumes a fixed-width font when |
358 |
viewing the sources, it uses more space on the line and thus makes it hard |
|
359 |
to observe its strict length limit (working against \<^emph>\<open>readability\<close>), it |
|
360 |
requires extra editing to adapt the layout to changes of the initial text |
|
361 |
(working against \<^emph>\<open>maintainability\<close>) etc. |
|
39878 | 362 |
|
61416 | 363 |
\<^medskip> |
61854 | 364 |
For similar reasons, any kind of two-dimensional or tabular layouts, |
365 |
ASCII-art with lines or boxes of asterisks etc.\ should be avoided. |
|
61506 | 366 |
\<close> |
367 |
||
368 |
paragraph \<open>Complex expressions\<close> |
|
61854 | 369 |
text \<open> |
69597 | 370 |
that consist of multi-clausal function definitions, \<^ML_text>\<open>handle\<close>, |
371 |
\<^ML_text>\<open>case\<close>, \<^ML_text>\<open>let\<close> (and combinations) require special |
|
61506 | 372 |
attention. The syntax of Standard ML is quite ambitious and admits a lot of |
40126 | 373 |
variance that can distort the meaning of the text. |
39881 | 374 |
|
69597 | 375 |
Multiple clauses of \<^ML_text>\<open>fun\<close>, \<^ML_text>\<open>fn\<close>, \<^ML_text>\<open>handle\<close>, |
376 |
\<^ML_text>\<open>case\<close> get extra indentation to indicate the nesting clearly. |
|
61854 | 377 |
Example: |
39881 | 378 |
|
61458 | 379 |
@{verbatim [display] |
380 |
\<open> (* RIGHT *) |
|
39881 | 381 |
|
382 |
fun foo p1 = |
|
383 |
expr1 |
|
384 |
| foo p2 = |
|
385 |
expr2 |
|
386 |
||
387 |
||
388 |
(* WRONG *) |
|
389 |
||
390 |
fun foo p1 = |
|
391 |
expr1 |
|
392 |
| foo p2 = |
|
61458 | 393 |
expr2\<close>} |
39881 | 394 |
|
69597 | 395 |
Body expressions consisting of \<^ML_text>\<open>case\<close> or \<^ML_text>\<open>let\<close> require |
61854 | 396 |
care to maintain compositionality, to prevent loss of logical indentation |
397 |
where it is especially important to see the structure of the text. Example: |
|
39881 | 398 |
|
61458 | 399 |
@{verbatim [display] |
400 |
\<open> (* RIGHT *) |
|
39881 | 401 |
|
402 |
fun foo p1 = |
|
403 |
(case e of |
|
404 |
q1 => ... |
|
405 |
| q2 => ...) |
|
406 |
| foo p2 = |
|
407 |
let |
|
408 |
... |
|
409 |
in |
|
410 |
... |
|
411 |
end |
|
412 |
||
413 |
||
414 |
(* WRONG *) |
|
415 |
||
416 |
fun foo p1 = case e of |
|
417 |
q1 => ... |
|
418 |
| q2 => ... |
|
419 |
| foo p2 = |
|
420 |
let |
|
421 |
... |
|
422 |
in |
|
423 |
... |
|
61458 | 424 |
end\<close>} |
39881 | 425 |
|
69597 | 426 |
Extra parentheses around \<^ML_text>\<open>case\<close> expressions are optional, but help |
61854 | 427 |
to analyse the nesting based on character matching in the text editor. |
39881 | 428 |
|
61416 | 429 |
\<^medskip> |
61854 | 430 |
There are two main exceptions to the overall principle of compositionality |
431 |
in the layout of complex expressions. |
|
39881 | 432 |
|
69597 | 433 |
\<^enum> \<^ML_text>\<open>if\<close> expressions are iterated as if ML had multi-branch |
57421 | 434 |
conditionals, e.g. |
39881 | 435 |
|
61458 | 436 |
@{verbatim [display] |
437 |
\<open> (* RIGHT *) |
|
39881 | 438 |
|
439 |
if b1 then e1 |
|
440 |
else if b2 then e2 |
|
61458 | 441 |
else e3\<close>} |
39881 | 442 |
|
69597 | 443 |
\<^enum> \<^ML_text>\<open>fn\<close> abstractions are often layed-out as if they would lack any |
61854 | 444 |
structure by themselves. This traditional form is motivated by the |
445 |
possibility to shift function arguments back and forth wrt.\ additional |
|
446 |
combinators. Example: |
|
39881 | 447 |
|
61458 | 448 |
@{verbatim [display] |
449 |
\<open> (* RIGHT *) |
|
39881 | 450 |
|
451 |
fun foo x y = fold (fn z => |
|
61458 | 452 |
expr)\<close>} |
39881 | 453 |
|
69597 | 454 |
Here the visual appearance is that of three arguments \<^ML_text>\<open>x\<close>, |
455 |
\<^ML_text>\<open>y\<close>, \<^ML_text>\<open>z\<close> in a row. |
|
39881 | 456 |
|
457 |
||
61854 | 458 |
Such weakly structured layout should be use with great care. Here are some |
69597 | 459 |
counter-examples involving \<^ML_text>\<open>let\<close> expressions: |
39881 | 460 |
|
61458 | 461 |
@{verbatim [display] |
462 |
\<open> (* WRONG *) |
|
39881 | 463 |
|
464 |
fun foo x = let |
|
465 |
val y = ... |
|
466 |
in ... end |
|
467 |
||
41162 | 468 |
|
469 |
(* WRONG *) |
|
470 |
||
40153 | 471 |
fun foo x = let |
472 |
val y = ... |
|
473 |
in ... end |
|
474 |
||
41162 | 475 |
|
476 |
(* WRONG *) |
|
477 |
||
39881 | 478 |
fun foo x = |
479 |
let |
|
480 |
val y = ... |
|
481 |
in ... end |
|
57421 | 482 |
|
483 |
||
484 |
(* WRONG *) |
|
485 |
||
486 |
fun foo x = |
|
487 |
let |
|
488 |
val y = ... |
|
489 |
in |
|
61458 | 490 |
... end\<close>} |
39881 | 491 |
|
61416 | 492 |
\<^medskip> |
61854 | 493 |
In general the source layout is meant to emphasize the structure of complex |
494 |
language expressions, not to pretend that SML had a completely different |
|
495 |
syntax (say that of Haskell, Scala, Java). |
|
58618 | 496 |
\<close> |
497 |
||
498 |
||
499 |
section \<open>ML embedded into Isabelle/Isar\<close> |
|
500 |
||
61854 | 501 |
text \<open> |
502 |
ML and Isar are intertwined via an open-ended bootstrap process that |
|
503 |
provides more and more programming facilities and logical content in an |
|
504 |
alternating manner. Bootstrapping starts from the raw environment of |
|
62354 | 505 |
existing implementations of Standard ML (mainly Poly/ML). |
39823 | 506 |
|
57421 | 507 |
Isabelle/Pure marks the point where the raw ML toplevel is superseded by |
508 |
Isabelle/ML within the Isar theory and proof language, with a uniform |
|
509 |
context for arbitrary ML values (see also \secref{sec:context}). This formal |
|
510 |
environment holds ML compiler bindings, logical entities, and many other |
|
511 |
things. |
|
512 |
||
513 |
Object-logics like Isabelle/HOL are built within the Isabelle/ML/Isar |
|
514 |
environment by introducing suitable theories with associated ML modules, |
|
61503 | 515 |
either inlined within \<^verbatim>\<open>.thy\<close> files, or as separate \<^verbatim>\<open>.ML\<close> files that are |
61854 | 516 |
loading from some theory. Thus Isabelle/HOL is defined as a regular |
517 |
user-space application within the Isabelle framework. Further add-on tools |
|
518 |
can be implemented in ML within the Isar context in the same manner: ML is |
|
519 |
part of the standard repertoire of Isabelle, and there is no distinction |
|
520 |
between ``users'' and ``developers'' in this respect. |
|
58618 | 521 |
\<close> |
522 |
||
523 |
||
524 |
subsection \<open>Isar ML commands\<close> |
|
525 |
||
526 |
text \<open> |
|
57421 | 527 |
The primary Isar source language provides facilities to ``open a window'' to |
528 |
the underlying ML compiler. Especially see the Isar commands @{command_ref |
|
529 |
"ML_file"} and @{command_ref "ML"}: both work the same way, but the source |
|
530 |
text is provided differently, via a file vs.\ inlined, respectively. Apart |
|
531 |
from embedding ML into the main theory definition like that, there are many |
|
532 |
more commands that refer to ML source, such as @{command_ref setup} or |
|
533 |
@{command_ref declaration}. Even more fine-grained embedding of ML into Isar |
|
534 |
is encountered in the proof method @{method_ref tactic}, which refines the |
|
69597 | 535 |
pending goal state via a given expression of type \<^ML_type>\<open>tactic\<close>. |
58618 | 536 |
\<close> |
537 |
||
61854 | 538 |
text %mlex \<open> |
539 |
The following artificial example demonstrates some ML toplevel declarations |
|
540 |
within the implicit Isar theory context. This is regular functional |
|
541 |
programming without referring to logical entities yet. |
|
58618 | 542 |
\<close> |
543 |
||
544 |
ML \<open> |
|
39823 | 545 |
fun factorial 0 = 1 |
546 |
| factorial n = n * factorial (n - 1) |
|
58618 | 547 |
\<close> |
548 |
||
61854 | 549 |
text \<open> |
69597 | 550 |
Here the ML environment is already managed by Isabelle, i.e.\ the \<^ML>\<open>factorial\<close> function is not yet accessible in the preceding paragraph, nor in |
61854 | 551 |
a different theory that is independent from the current one in the import |
552 |
hierarchy. |
|
39823 | 553 |
|
57421 | 554 |
Removing the above ML declaration from the source text will remove any trace |
555 |
of this definition, as expected. The Isabelle/ML toplevel environment is |
|
61854 | 556 |
managed in a \<^emph>\<open>stateless\<close> way: in contrast to the raw ML toplevel, there are |
557 |
no global side-effects involved here.\<^footnote>\<open>Such a stateless compilation |
|
558 |
environment is also a prerequisite for robust parallel compilation within |
|
559 |
independent nodes of the implicit theory development graph.\<close> |
|
39823 | 560 |
|
61416 | 561 |
\<^medskip> |
61854 | 562 |
The next example shows how to embed ML into Isar proofs, using @{command_ref |
563 |
"ML_prf"} instead of @{command_ref "ML"}. As illustrated below, the effect |
|
564 |
on the ML environment is local to the whole proof body, but ignoring the |
|
565 |
block structure. |
|
566 |
\<close> |
|
39823 | 567 |
|
40964 | 568 |
notepad |
569 |
begin |
|
58618 | 570 |
ML_prf %"ML" \<open>val a = 1\<close> |
40126 | 571 |
{ |
58618 | 572 |
ML_prf %"ML" \<open>val b = a + 1\<close> |
61580 | 573 |
} \<comment> \<open>Isar block structure ignored by ML environment\<close> |
58618 | 574 |
ML_prf %"ML" \<open>val c = b + 1\<close> |
40964 | 575 |
end |
39823 | 576 |
|
61854 | 577 |
text \<open> |
578 |
By side-stepping the normal scoping rules for Isar proof blocks, embedded ML |
|
579 |
code can refer to the different contexts and manipulate corresponding |
|
580 |
entities, e.g.\ export a fact from a block context. |
|
39823 | 581 |
|
61416 | 582 |
\<^medskip> |
61854 | 583 |
Two further ML commands are useful in certain situations: @{command_ref |
584 |
ML_val} and @{command_ref ML_command} are \<^emph>\<open>diagnostic\<close> in the sense that |
|
585 |
there is no effect on the underlying environment, and can thus be used |
|
69597 | 586 |
anywhere. The examples below produce long strings of digits by invoking \<^ML>\<open>factorial\<close>: @{command ML_val} takes care of printing the ML toplevel result, |
61854 | 587 |
but @{command ML_command} is silent so we produce an explicit output |
588 |
message. |
|
58618 | 589 |
\<close> |
590 |
||
591 |
ML_val \<open>factorial 100\<close> |
|
592 |
ML_command \<open>writeln (string_of_int (factorial 100))\<close> |
|
39823 | 593 |
|
40964 | 594 |
notepad |
595 |
begin |
|
58618 | 596 |
ML_val \<open>factorial 100\<close> |
597 |
ML_command \<open>writeln (string_of_int (factorial 100))\<close> |
|
40964 | 598 |
end |
39823 | 599 |
|
600 |
||
58618 | 601 |
subsection \<open>Compile-time context\<close> |
602 |
||
61854 | 603 |
text \<open> |
604 |
Whenever the ML compiler is invoked within Isabelle/Isar, the formal context |
|
605 |
is passed as a thread-local reference variable. Thus ML code may access the |
|
606 |
theory context during compilation, by reading or writing the (local) theory |
|
607 |
under construction. Note that such direct access to the compile-time context |
|
608 |
is rare. In practice it is typically done via some derived ML functions |
|
609 |
instead. |
|
58618 | 610 |
\<close> |
611 |
||
612 |
text %mlref \<open> |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
613 |
\begin{mldecls} |
62876 | 614 |
@{index_ML Context.the_generic_context: "unit -> Context.generic"} \\ |
40126 | 615 |
@{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\ |
56199 | 616 |
@{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\ |
617 |
@{index_ML ML_Thms.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
|
618 |
\end{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
619 |
|
69597 | 620 |
\<^descr> \<^ML>\<open>Context.the_generic_context ()\<close> refers to the theory context of |
61854 | 621 |
the ML toplevel --- at compile time. ML code needs to take care to refer to |
69597 | 622 |
\<^ML>\<open>Context.the_generic_context ()\<close> correctly. Recall that evaluation |
61854 | 623 |
of a function body is delayed 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
|
624 |
|
69597 | 625 |
\<^descr> \<^ML>\<open>Context.>>\<close>~\<open>f\<close> applies context transformation \<open>f\<close> to the implicit |
61854 | 626 |
context of the ML toplevel. |
61493 | 627 |
|
69597 | 628 |
\<^descr> \<^ML>\<open>ML_Thms.bind_thms\<close>~\<open>(name, thms)\<close> stores a list of theorems produced |
61854 | 629 |
in ML both in the (global) theory context and the ML toplevel, associating |
630 |
it with the provided name. |
|
39850 | 631 |
|
69597 | 632 |
\<^descr> \<^ML>\<open>ML_Thms.bind_thm\<close> is similar to \<^ML>\<open>ML_Thms.bind_thms\<close> but refers to |
61854 | 633 |
a singleton fact. |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
634 |
|
61854 | 635 |
It is important to note that the above functions are really restricted to |
636 |
the compile time, even though the ML compiler is invoked at run-time. The |
|
637 |
majority of ML code either uses static antiquotations |
|
638 |
(\secref{sec:ML-antiq}) or refers to the theory or proof context at |
|
639 |
run-time, by explicit functional abstraction. |
|
58618 | 640 |
\<close> |
641 |
||
642 |
||
643 |
subsection \<open>Antiquotations \label{sec:ML-antiq}\<close> |
|
644 |
||
61854 | 645 |
text \<open> |
646 |
A very important consequence of embedding ML into Isar is the concept of |
|
647 |
\<^emph>\<open>ML antiquotation\<close>. The standard token language of ML is augmented by |
|
648 |
special syntactic entities of the following form: |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
649 |
|
69597 | 650 |
\<^rail>\<open> |
62969 | 651 |
@{syntax_def antiquote}: '@{' name args '}' |
69597 | 652 |
\<close> |
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
653 |
|
62969 | 654 |
Here @{syntax name} and @{syntax args} are outer syntax categories, as |
58555 | 655 |
defined in @{cite "isabelle-isar-ref"}. |
39823 | 656 |
|
61416 | 657 |
\<^medskip> |
61854 | 658 |
A regular antiquotation \<open>@{name args}\<close> processes its arguments by the usual |
659 |
means of the Isar source language, and produces corresponding ML source |
|
660 |
text, either as literal \<^emph>\<open>inline\<close> text (e.g.\ \<open>@{term t}\<close>) or abstract |
|
661 |
\<^emph>\<open>value\<close> (e.g. \<open>@{thm th}\<close>). This pre-compilation scheme allows to refer to |
|
662 |
formal entities in a robust manner, with proper static scoping and with some |
|
663 |
degree of logical checking of small portions of the code. |
|
58618 | 664 |
\<close> |
665 |
||
666 |
||
667 |
subsection \<open>Printing ML values\<close> |
|
668 |
||
61854 | 669 |
text \<open> |
670 |
The ML compiler knows about the structure of values according to their |
|
671 |
static type, and can print them in the manner of its toplevel, although the |
|
672 |
details are non-portable. The antiquotations @{ML_antiquotation_def |
|
673 |
"make_string"} and @{ML_antiquotation_def "print"} provide a quasi-portable |
|
674 |
way to refer to this potential capability of the underlying ML system in |
|
56399 | 675 |
generic Isabelle/ML sources. |
676 |
||
61854 | 677 |
This is occasionally useful for diagnostic or demonstration purposes. Note |
678 |
that production-quality tools require proper user-level error messages, |
|
679 |
avoiding raw ML values in the output. |
|
680 |
\<close> |
|
58618 | 681 |
|
682 |
text %mlantiq \<open> |
|
51636
e49bf0be79ba
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents:
51295
diff
changeset
|
683 |
\begin{matharray}{rcl} |
61493 | 684 |
@{ML_antiquotation_def "make_string"} & : & \<open>ML_antiquotation\<close> \\ |
685 |
@{ML_antiquotation_def "print"} & : & \<open>ML_antiquotation\<close> \\ |
|
51636
e49bf0be79ba
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents:
51295
diff
changeset
|
686 |
\end{matharray} |
e49bf0be79ba
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents:
51295
diff
changeset
|
687 |
|
69597 | 688 |
\<^rail>\<open> |
51636
e49bf0be79ba
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents:
51295
diff
changeset
|
689 |
@@{ML_antiquotation make_string} |
56399 | 690 |
; |
67146 | 691 |
@@{ML_antiquotation print} embedded? |
69597 | 692 |
\<close> |
51636
e49bf0be79ba
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents:
51295
diff
changeset
|
693 |
|
61854 | 694 |
\<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to |
695 |
the ML toplevel. The result is compiler dependent and may fall back on "?" |
|
696 |
in certain situations. The value of configuration option @{attribute_ref |
|
697 |
ML_print_depth} determines further details of output. |
|
56399 | 698 |
|
61854 | 699 |
\<^descr> \<open>@{print f}\<close> uses the ML function \<open>f: string -> unit\<close> to output the result |
700 |
of \<open>@{make_string}\<close> above, together with the source position of the |
|
69597 | 701 |
antiquotation. The default output function is \<^ML>\<open>writeln\<close>. |
58618 | 702 |
\<close> |
703 |
||
61854 | 704 |
text %mlex \<open> |
705 |
The following artificial examples show how to produce adhoc output of ML |
|
706 |
values for debugging purposes. |
|
707 |
\<close> |
|
58618 | 708 |
|
59902 | 709 |
ML_val \<open> |
51636
e49bf0be79ba
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents:
51295
diff
changeset
|
710 |
val x = 42; |
e49bf0be79ba
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents:
51295
diff
changeset
|
711 |
val y = true; |
e49bf0be79ba
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents:
51295
diff
changeset
|
712 |
|
69597 | 713 |
writeln (\<^make_string> {x = x, y = y}); |
714 |
||
715 |
\<^print> {x = x, y = y}; |
|
716 |
\<^print>\<open>tracing\<close> {x = x, y = y}; |
|
58618 | 717 |
\<close> |
718 |
||
719 |
||
720 |
section \<open>Canonical argument order \label{sec:canonical-argument-order}\<close> |
|
721 |
||
61854 | 722 |
text \<open> |
723 |
Standard ML is a language in the tradition of \<open>\<lambda>\<close>-calculus and |
|
724 |
\<^emph>\<open>higher-order functional programming\<close>, similar to OCaml, Haskell, or |
|
725 |
Isabelle/Pure and HOL as logical languages. Getting acquainted with the |
|
726 |
native style of representing functions in that setting can save a lot of |
|
727 |
extra boiler-plate of redundant shuffling of arguments, auxiliary |
|
728 |
abstractions etc. |
|
39883 | 729 |
|
61854 | 730 |
Functions are usually \<^emph>\<open>curried\<close>: the idea of turning arguments of type |
731 |
\<open>\<tau>\<^sub>i\<close> (for \<open>i \<in> {1, \<dots> n}\<close>) into a result of type \<open>\<tau>\<close> is represented by the |
|
732 |
iterated function space \<open>\<tau>\<^sub>1 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>\<close>. This is isomorphic to the |
|
733 |
well-known encoding via tuples \<open>\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<rightarrow> \<tau>\<close>, but the curried version |
|
734 |
fits more smoothly into the basic calculus.\<^footnote>\<open>The difference is even more |
|
735 |
significant in HOL, because the redundant tuple structure needs to be |
|
736 |
accommodated extraneous proof steps.\<close> |
|
39883 | 737 |
|
61854 | 738 |
Currying gives some flexibility due to \<^emph>\<open>partial application\<close>. A function |
739 |
\<open>f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>\<close> can be applied to \<open>x: \<tau>\<^sub>1\<close> and the remaining \<open>(f x): \<tau>\<^sub>2 |
|
740 |
\<rightarrow> \<tau>\<close> passed to another function etc. How well this works in practice depends |
|
741 |
on the order of arguments. In the worst case, arguments are arranged |
|
742 |
erratically, and using a function in a certain situation always requires |
|
743 |
some glue code. Thus we would get exponentially many opportunities to |
|
39883 | 744 |
decorate the code with meaningless permutations of arguments. |
745 |
||
61854 | 746 |
This can be avoided by \<^emph>\<open>canonical argument order\<close>, which observes certain |
747 |
standard patterns and minimizes adhoc permutations in their application. In |
|
748 |
Isabelle/ML, large portions of text can be written without auxiliary |
|
749 |
operations like \<open>swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times> \<alpha>\<close> or \<open>C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)\<close> (the |
|
750 |
latter is not present in the Isabelle/ML library). |
|
39883 | 751 |
|
61416 | 752 |
\<^medskip> |
61854 | 753 |
The main idea is that arguments that vary less are moved further to the left |
754 |
than those that vary more. Two particularly important categories of |
|
755 |
functions are \<^emph>\<open>selectors\<close> and \<^emph>\<open>updates\<close>. |
|
39883 | 756 |
|
61854 | 757 |
The subsequent scheme is based on a hypothetical set-like container of type |
758 |
\<open>\<beta>\<close> that manages elements of type \<open>\<alpha>\<close>. Both the names and types of the |
|
759 |
associated operations are canonical for Isabelle/ML. |
|
39883 | 760 |
|
52416 | 761 |
\begin{center} |
39883 | 762 |
\begin{tabular}{ll} |
763 |
kind & canonical name and type \\\hline |
|
61493 | 764 |
selector & \<open>member: \<beta> \<rightarrow> \<alpha> \<rightarrow> bool\<close> \\ |
765 |
update & \<open>insert: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>\<close> \\ |
|
39883 | 766 |
\end{tabular} |
52416 | 767 |
\end{center} |
39883 | 768 |
|
61854 | 769 |
Given a container \<open>B: \<beta>\<close>, the partially applied \<open>member B\<close> is a predicate |
770 |
over elements \<open>\<alpha> \<rightarrow> bool\<close>, and thus represents the intended denotation |
|
771 |
directly. It is customary to pass the abstract predicate to further |
|
772 |
operations, not the concrete container. The argument order makes it easy to |
|
773 |
use other combinators: \<open>forall (member B) list\<close> will check a list of |
|
774 |
elements for membership in \<open>B\<close> etc. Often the explicit \<open>list\<close> is pointless |
|
775 |
and can be contracted to \<open>forall (member B)\<close> to get directly a predicate |
|
776 |
again. |
|
39883 | 777 |
|
61854 | 778 |
In contrast, an update operation varies the container, so it moves to the |
779 |
right: \<open>insert a\<close> is a function \<open>\<beta> \<rightarrow> \<beta>\<close> to insert a value \<open>a\<close>. These can be |
|
780 |
composed naturally as \<open>insert c \<circ> insert b \<circ> insert a\<close>. The slightly awkward |
|
781 |
inversion of the composition order is due to conventional mathematical |
|
782 |
notation, which can be easily amended as explained below. |
|
58618 | 783 |
\<close> |
784 |
||
785 |
||
786 |
subsection \<open>Forward application and composition\<close> |
|
787 |
||
61854 | 788 |
text \<open> |
789 |
Regular function application and infix notation works best for relatively |
|
790 |
deeply structured expressions, e.g.\ \<open>h (f x y + g z)\<close>. The important |
|
791 |
special case of \<^emph>\<open>linear transformation\<close> applies a cascade of functions \<open>f\<^sub>n |
|
792 |
(\<dots> (f\<^sub>1 x))\<close>. This becomes hard to read and maintain if the functions are |
|
793 |
themselves given as complex expressions. The notation can be significantly |
|
794 |
improved by introducing \<^emph>\<open>forward\<close> versions of application and composition |
|
795 |
as follows: |
|
39883 | 796 |
|
61416 | 797 |
\<^medskip> |
39883 | 798 |
\begin{tabular}{lll} |
61493 | 799 |
\<open>x |> f\<close> & \<open>\<equiv>\<close> & \<open>f x\<close> \\ |
800 |
\<open>(f #> g) x\<close> & \<open>\<equiv>\<close> & \<open>x |> f |> g\<close> \\ |
|
39883 | 801 |
\end{tabular} |
61416 | 802 |
\<^medskip> |
39883 | 803 |
|
61854 | 804 |
This enables to write conveniently \<open>x |> f\<^sub>1 |> \<dots> |> f\<^sub>n\<close> or \<open>f\<^sub>1 #> \<dots> #> |
805 |
f\<^sub>n\<close> for its functional abstraction over \<open>x\<close>. |
|
39883 | 806 |
|
61416 | 807 |
\<^medskip> |
61854 | 808 |
There is an additional set of combinators to accommodate multiple results |
809 |
(via pairs) that are passed on as multiple arguments (via currying). |
|
39883 | 810 |
|
61416 | 811 |
\<^medskip> |
39883 | 812 |
\begin{tabular}{lll} |
61493 | 813 |
\<open>(x, y) |-> f\<close> & \<open>\<equiv>\<close> & \<open>f x y\<close> \\ |
814 |
\<open>(f #-> g) x\<close> & \<open>\<equiv>\<close> & \<open>x |> f |-> g\<close> \\ |
|
39883 | 815 |
\end{tabular} |
61416 | 816 |
\<^medskip> |
58618 | 817 |
\<close> |
818 |
||
819 |
text %mlref \<open> |
|
39883 | 820 |
\begin{mldecls} |
46262 | 821 |
@{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\ |
822 |
@{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\ |
|
823 |
@{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\ |
|
824 |
@{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\ |
|
39883 | 825 |
\end{mldecls} |
58618 | 826 |
\<close> |
827 |
||
828 |
||
829 |
subsection \<open>Canonical iteration\<close> |
|
830 |
||
61854 | 831 |
text \<open> |
832 |
As explained above, a function \<open>f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>\<close> can be understood as update on |
|
833 |
a configuration of type \<open>\<beta>\<close>, parameterized by an argument of type \<open>\<alpha>\<close>. Given |
|
834 |
\<open>a: \<alpha>\<close> the partial application \<open>(f a): \<beta> \<rightarrow> \<beta>\<close> operates homogeneously on \<open>\<beta>\<close>. |
|
835 |
This can be iterated naturally over a list of parameters \<open>[a\<^sub>1, \<dots>, a\<^sub>n]\<close> as |
|
836 |
\<open>f a\<^sub>1 #> \<dots> #> f a\<^sub>n\<close>. The latter expression is again a function \<open>\<beta> \<rightarrow> \<beta>\<close>. It |
|
837 |
can be applied to an initial configuration \<open>b: \<beta>\<close> to start the iteration |
|
838 |
over the given list of arguments: each \<open>a\<close> in \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> is applied |
|
839 |
consecutively by updating a cumulative configuration. |
|
39883 | 840 |
|
61854 | 841 |
The \<open>fold\<close> combinator in Isabelle/ML lifts a function \<open>f\<close> as above to its |
842 |
iterated version over a list of arguments. Lifting can be repeated, e.g.\ |
|
843 |
\<open>(fold \<circ> fold) f\<close> iterates over a list of lists as expected. |
|
39883 | 844 |
|
61854 | 845 |
The variant \<open>fold_rev\<close> works inside-out over the list of arguments, such |
846 |
that \<open>fold_rev f \<equiv> fold f \<circ> rev\<close> holds. |
|
61493 | 847 |
|
61854 | 848 |
The \<open>fold_map\<close> combinator essentially performs \<open>fold\<close> and \<open>map\<close> |
849 |
simultaneously: each application of \<open>f\<close> produces an updated configuration |
|
850 |
together with a side-result; the iteration collects all such side-results as |
|
851 |
a separate list. |
|
58618 | 852 |
\<close> |
853 |
||
854 |
text %mlref \<open> |
|
39883 | 855 |
\begin{mldecls} |
856 |
@{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ |
|
857 |
@{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ |
|
858 |
@{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\ |
|
859 |
\end{mldecls} |
|
860 |
||
69597 | 861 |
\<^descr> \<^ML>\<open>fold\<close>~\<open>f\<close> lifts the parametrized update function \<open>f\<close> to a list of |
61854 | 862 |
parameters. |
61493 | 863 |
|
69597 | 864 |
\<^descr> \<^ML>\<open>fold_rev\<close>~\<open>f\<close> is similar to \<^ML>\<open>fold\<close>~\<open>f\<close>, but works inside-out, as |
61854 | 865 |
if the list would be reversed. |
61493 | 866 |
|
69597 | 867 |
\<^descr> \<^ML>\<open>fold_map\<close>~\<open>f\<close> lifts the parametrized update function \<open>f\<close> (with |
61854 | 868 |
side-result) to a list of parameters and cumulative side-results. |
39883 | 869 |
|
870 |
||
871 |
\begin{warn} |
|
57421 | 872 |
The literature on functional programming provides a confusing multitude of |
61854 | 873 |
combinators called \<open>foldl\<close>, \<open>foldr\<close> etc. SML97 provides its own variations |
69597 | 874 |
as \<^ML>\<open>List.foldl\<close> and \<^ML>\<open>List.foldr\<close>, while the classic Isabelle library |
875 |
also has the historic \<^ML>\<open>Library.foldl\<close> and \<^ML>\<open>Library.foldr\<close>. To avoid |
|
61854 | 876 |
unnecessary complication, all these historical versions should be ignored, |
69597 | 877 |
and the canonical \<^ML>\<open>fold\<close> (or \<^ML>\<open>fold_rev\<close>) used exclusively. |
39883 | 878 |
\end{warn} |
58618 | 879 |
\<close> |
880 |
||
61854 | 881 |
text %mlex \<open> |
882 |
The following example shows how to fill a text buffer incrementally by |
|
883 |
adding strings, either individually or from a given list. |
|
58618 | 884 |
\<close> |
885 |
||
59902 | 886 |
ML_val \<open> |
39883 | 887 |
val s = |
888 |
Buffer.empty |
|
889 |
|> Buffer.add "digits: " |
|
890 |
|> fold (Buffer.add o string_of_int) (0 upto 9) |
|
891 |
|> Buffer.content; |
|
892 |
||
69597 | 893 |
\<^assert> (s = "digits: 0123456789"); |
58618 | 894 |
\<close> |
895 |
||
61854 | 896 |
text \<open> |
69597 | 897 |
Note how \<^ML>\<open>fold (Buffer.add o string_of_int)\<close> above saves an extra \<^ML>\<open>map\<close> over the given list. This kind of peephole optimization reduces both |
61854 | 898 |
the code size and the tree structures in memory (``deforestation''), but it |
899 |
requires some practice to read and write fluently. |
|
39883 | 900 |
|
61416 | 901 |
\<^medskip> |
61854 | 902 |
The next example elaborates the idea of canonical iteration, demonstrating |
903 |
fast accumulation of tree content using a text buffer. |
|
58618 | 904 |
\<close> |
905 |
||
906 |
ML \<open> |
|
39883 | 907 |
datatype tree = Text of string | Elem of string * tree list; |
908 |
||
909 |
fun slow_content (Text txt) = txt |
|
910 |
| slow_content (Elem (name, ts)) = |
|
911 |
"<" ^ name ^ ">" ^ |
|
912 |
implode (map slow_content ts) ^ |
|
913 |
"</" ^ name ^ ">" |
|
914 |
||
915 |
fun add_content (Text txt) = Buffer.add txt |
|
916 |
| add_content (Elem (name, ts)) = |
|
917 |
Buffer.add ("<" ^ name ^ ">") #> |
|
918 |
fold add_content ts #> |
|
919 |
Buffer.add ("</" ^ name ^ ">"); |
|
920 |
||
921 |
fun fast_content tree = |
|
922 |
Buffer.empty |> add_content tree |> Buffer.content; |
|
58618 | 923 |
\<close> |
924 |
||
61854 | 925 |
text \<open> |
69597 | 926 |
The slowness of \<^ML>\<open>slow_content\<close> is due to the \<^ML>\<open>implode\<close> of the |
61854 | 927 |
recursive results, because it copies previously produced strings again and |
928 |
again. |
|
39883 | 929 |
|
69597 | 930 |
The incremental \<^ML>\<open>add_content\<close> avoids this by operating on a buffer that |
931 |
is passed through in a linear fashion. Using \<^ML_text>\<open>#>\<close> and contraction |
|
61854 | 932 |
over the actual buffer argument saves some additional boiler-plate. Of |
69597 | 933 |
course, the two \<^ML>\<open>Buffer.add\<close> invocations with concatenated strings |
61854 | 934 |
could have been split into smaller parts, but this would have obfuscated the |
935 |
source without making a big difference in performance. Here we have done |
|
936 |
some peephole-optimization for the sake of readability. |
|
39883 | 937 |
|
69597 | 938 |
Another benefit of \<^ML>\<open>add_content\<close> is its ``open'' form as a function on |
61854 | 939 |
buffers that can be continued in further linear transformations, folding |
69597 | 940 |
etc. Thus it is more compositional than the naive \<^ML>\<open>slow_content\<close>. As |
66663 | 941 |
realistic example, compare the old-style |
69597 | 942 |
\<^ML>\<open>Term.maxidx_of_term: term -> int\<close> with the newer \<^ML>\<open>Term.maxidx_term: term -> int -> int\<close> in Isabelle/Pure. |
943 |
||
944 |
Note that \<^ML>\<open>fast_content\<close> above is only defined as example. In many |
|
945 |
practical situations, it is customary to provide the incremental \<^ML>\<open>add_content\<close> only and leave the initialization and termination to the |
|
61854 | 946 |
concrete application to the user. |
58618 | 947 |
\<close> |
948 |
||
949 |
||
950 |
section \<open>Message output channels \label{sec:message-channels}\<close> |
|
951 |
||
61854 | 952 |
text \<open> |
953 |
Isabelle provides output channels for different kinds of messages: regular |
|
954 |
output, high-volume tracing information, warnings, and errors. |
|
39835 | 955 |
|
61854 | 956 |
Depending on the user interface involved, these messages may appear in |
957 |
different text styles or colours. The standard output for batch sessions |
|
958 |
prefixes each line of warnings by \<^verbatim>\<open>###\<close> and errors by \<^verbatim>\<open>***\<close>, but leaves |
|
959 |
anything else unchanged. The message body may contain further markup and |
|
960 |
formatting, which is routinely used in the Prover IDE @{cite |
|
961 |
"isabelle-jedit"}. |
|
39835 | 962 |
|
61854 | 963 |
Messages are associated with the transaction context of the running Isar |
964 |
command. This enables the front-end to manage commands and resulting |
|
965 |
messages together. For example, after deleting a command from a given theory |
|
966 |
document version, the corresponding message output can be retracted from the |
|
967 |
display. |
|
58618 | 968 |
\<close> |
969 |
||
970 |
text %mlref \<open> |
|
39835 | 971 |
\begin{mldecls} |
972 |
@{index_ML writeln: "string -> unit"} \\ |
|
973 |
@{index_ML tracing: "string -> unit"} \\ |
|
974 |
@{index_ML warning: "string -> unit"} \\ |
|
57421 | 975 |
@{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\ |
39835 | 976 |
\end{mldecls} |
977 |
||
69597 | 978 |
\<^descr> \<^ML>\<open>writeln\<close>~\<open>text\<close> outputs \<open>text\<close> as regular message. This is the |
61854 | 979 |
primary message output operation of Isabelle and should be used by default. |
39835 | 980 |
|
69597 | 981 |
\<^descr> \<^ML>\<open>tracing\<close>~\<open>text\<close> outputs \<open>text\<close> as special tracing message, indicating |
61854 | 982 |
potential high-volume output to the front-end (hundreds or thousands of |
983 |
messages issued by a single command). The idea is to allow the |
|
984 |
user-interface to downgrade the quality of message display to achieve higher |
|
985 |
throughput. |
|
39835 | 986 |
|
61854 | 987 |
Note that the user might have to take special actions to see tracing output, |
988 |
e.g.\ switch to a different output window. So this channel should not be |
|
989 |
used for regular output. |
|
39835 | 990 |
|
69597 | 991 |
\<^descr> \<^ML>\<open>warning\<close>~\<open>text\<close> outputs \<open>text\<close> as warning, which typically means some |
61854 | 992 |
extra emphasis on the front-end side (color highlighting, icons, etc.). |
39835 | 993 |
|
69597 | 994 |
\<^descr> \<^ML>\<open>error\<close>~\<open>text\<close> raises exception \<^ML>\<open>ERROR\<close>~\<open>text\<close> and thus lets the |
61854 | 995 |
Isar toplevel print \<open>text\<close> on the error channel, which typically means some |
996 |
extra emphasis on the front-end side (color highlighting, icons, etc.). |
|
39835 | 997 |
|
998 |
This assumes that the exception is not handled before the command |
|
69597 | 999 |
terminates. Handling exception \<^ML>\<open>ERROR\<close>~\<open>text\<close> is a perfectly legal |
61854 | 1000 |
alternative: it means that the error is absorbed without any message output. |
39835 | 1001 |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
1002 |
\begin{warn} |
69597 | 1003 |
The actual error channel is accessed via \<^ML>\<open>Output.error_message\<close>, but |
58842 | 1004 |
this is normally not used directly in user code. |
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
1005 |
\end{warn} |
39835 | 1006 |
|
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
1007 |
|
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
1008 |
\begin{warn} |
61854 | 1009 |
Regular Isabelle/ML code should output messages exclusively by the official |
69597 | 1010 |
channels. Using raw I/O on \<^emph>\<open>stdout\<close> or \<^emph>\<open>stderr\<close> instead (e.g.\ via \<^ML>\<open>TextIO.output\<close>) is apt to cause problems in the presence of parallel and |
61854 | 1011 |
asynchronous processing of Isabelle theories. Such raw output might be |
1012 |
displayed by the front-end in some system console log, with a low chance |
|
1013 |
that the user will ever see it. Moreover, as a genuine side-effect on global |
|
1014 |
process channels, there is no proper way to retract output when Isar command |
|
40126 | 1015 |
transactions are reset by the system. |
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39859
diff
changeset
|
1016 |
\end{warn} |
39872 | 1017 |
|
1018 |
\begin{warn} |
|
61854 | 1019 |
The message channels should be used in a message-oriented manner. This means |
1020 |
that multi-line output that logically belongs together is issued by a single |
|
69597 | 1021 |
invocation of \<^ML>\<open>writeln\<close> etc.\ with the functional concatenation of all |
61854 | 1022 |
message constituents. |
39872 | 1023 |
\end{warn} |
58618 | 1024 |
\<close> |
1025 |
||
61854 | 1026 |
text %mlex \<open> |
1027 |
The following example demonstrates a multi-line warning. Note that in some |
|
1028 |
situations the user sees only the first line, so the most important point |
|
1029 |
should be made first. |
|
58618 | 1030 |
\<close> |
1031 |
||
1032 |
ML_command \<open> |
|
39872 | 1033 |
warning (cat_lines |
1034 |
["Beware the Jabberwock, my son!", |
|
1035 |
"The jaws that bite, the claws that catch!", |
|
1036 |
"Beware the Jubjub Bird, and shun", |
|
1037 |
"The frumious Bandersnatch!"]); |
|
58618 | 1038 |
\<close> |
1039 |
||
59902 | 1040 |
text \<open> |
61416 | 1041 |
\<^medskip> |
61854 | 1042 |
An alternative is to make a paragraph of freely-floating words as follows. |
59902 | 1043 |
\<close> |
1044 |
||
1045 |
ML_command \<open> |
|
1046 |
warning (Pretty.string_of (Pretty.para |
|
1047 |
"Beware the Jabberwock, my son! \ |
|
1048 |
\The jaws that bite, the claws that catch! \ |
|
1049 |
\Beware the Jubjub Bird, and shun \ |
|
1050 |
\The frumious Bandersnatch!")) |
|
1051 |
\<close> |
|
1052 |
||
1053 |
text \<open> |
|
1054 |
This has advantages with variable window / popup sizes, but might make it |
|
1055 |
harder to search for message content systematically, e.g.\ by other tools or |
|
1056 |
by humans expecting the ``verse'' of a formal message in a fixed layout. |
|
1057 |
\<close> |
|
1058 |
||
58618 | 1059 |
|
1060 |
section \<open>Exceptions \label{sec:exceptions}\<close> |
|
1061 |
||
61854 | 1062 |
text \<open> |
1063 |
The Standard ML semantics of strict functional evaluation together with |
|
1064 |
exceptions is rather well defined, but some delicate points need to be |
|
1065 |
observed to avoid that ML programs go wrong despite static type-checking. |
|
1066 |
Exceptions in Isabelle/ML are subsequently categorized as follows. |
|
1067 |
\<close> |
|
61506 | 1068 |
|
1069 |
paragraph \<open>Regular user errors.\<close> |
|
61854 | 1070 |
text \<open> |
1071 |
These are meant to provide informative feedback about malformed input etc. |
|
1072 |
||
69597 | 1073 |
The \<^emph>\<open>error\<close> function raises the corresponding \<^ML>\<open>ERROR\<close> exception, with a |
1074 |
plain text message as argument. \<^ML>\<open>ERROR\<close> exceptions can be handled |
|
61854 | 1075 |
internally, in order to be ignored, turned into other exceptions, or |
1076 |
cascaded by appending messages. If the corresponding Isabelle/Isar command |
|
69597 | 1077 |
terminates with an \<^ML>\<open>ERROR\<close> exception state, the system will print the |
61854 | 1078 |
result on the error channel (see \secref{sec:message-channels}). |
39854 | 1079 |
|
61854 | 1080 |
It is considered bad style to refer to internal function names or values in |
1081 |
ML source notation in user error messages. Do not use \<open>@{make_string}\<close> nor |
|
1082 |
\<open>@{here}\<close>! |
|
39854 | 1083 |
|
61854 | 1084 |
Grammatical correctness of error messages can be improved by \<^emph>\<open>omitting\<close> |
1085 |
final punctuation: messages are often concatenated or put into a larger |
|
1086 |
context (e.g.\ augmented with source position). Note that punctuation after |
|
1087 |
formal entities (types, terms, theorems) is particularly prone to user |
|
1088 |
confusion. |
|
61506 | 1089 |
\<close> |
1090 |
||
1091 |
paragraph \<open>Program failures.\<close> |
|
61854 | 1092 |
text \<open> |
1093 |
There is a handful of standard exceptions that indicate general failure |
|
61506 | 1094 |
situations, or failures of core operations on logical entities (types, |
1095 |
terms, theorems, theories, see \chref{ch:logic}). |
|
39854 | 1096 |
|
61854 | 1097 |
These exceptions indicate a genuine breakdown of the program, so the main |
1098 |
purpose is to determine quickly what has happened where. Traditionally, the |
|
1099 |
(short) exception message would include the name of an ML function, although |
|
1100 |
this is no longer necessary, because the ML runtime system attaches detailed |
|
69597 | 1101 |
source position stemming from the corresponding \<^ML_text>\<open>raise\<close> keyword. |
39854 | 1102 |
|
61416 | 1103 |
\<^medskip> |
61854 | 1104 |
User modules can always introduce their own custom exceptions locally, e.g.\ |
1105 |
to organize internal failures robustly without overlapping with existing |
|
1106 |
exceptions. Exceptions that are exposed in module signatures require extra |
|
1107 |
care, though, and should \<^emph>\<open>not\<close> be introduced by default. Surprise by users |
|
1108 |
of a module can be often minimized by using plain user errors instead. |
|
61506 | 1109 |
\<close> |
1110 |
||
1111 |
paragraph \<open>Interrupts.\<close> |
|
61854 | 1112 |
text \<open> |
1113 |
These indicate arbitrary system events: both the ML runtime system and the |
|
1114 |
Isabelle/ML infrastructure signal various exceptional situations by raising |
|
69597 | 1115 |
the special \<^ML>\<open>Exn.Interrupt\<close> exception in user code. |
57421 | 1116 |
|
1117 |
This is the one and only way that physical events can intrude an Isabelle/ML |
|
1118 |
program. Such an interrupt can mean out-of-memory, stack overflow, timeout, |
|
1119 |
internal signaling of threads, or a POSIX process signal. An Isabelle/ML |
|
1120 |
program that intercepts interrupts becomes dependent on physical effects of |
|
1121 |
the environment. Even worse, exception handling patterns that are too |
|
1122 |
general by accident, e.g.\ by misspelled exception constructors, will cover |
|
1123 |
interrupts unintentionally and thus render the program semantics |
|
1124 |
ill-defined. |
|
39854 | 1125 |
|
61854 | 1126 |
Note that the Interrupt exception dates back to the original SML90 language |
1127 |
definition. It was excluded from the SML97 version to avoid its malign |
|
1128 |
impact on ML program semantics, but without providing a viable alternative. |
|
1129 |
Isabelle/ML recovers physical interruptibility (which is an indispensable |
|
1130 |
tool to implement managed evaluation of command transactions), but requires |
|
1131 |
user code to be strictly transparent wrt.\ interrupts. |
|
39854 | 1132 |
|
1133 |
\begin{warn} |
|
61854 | 1134 |
Isabelle/ML user code needs to terminate promptly on interruption, without |
1135 |
guessing at its meaning to the system infrastructure. Temporary handling of |
|
1136 |
interrupts for cleanup of global resources etc.\ needs to be followed |
|
1137 |
immediately by re-raising of the original exception. |
|
39854 | 1138 |
\end{warn} |
58618 | 1139 |
\<close> |
1140 |
||
1141 |
text %mlref \<open> |
|
39855 | 1142 |
\begin{mldecls} |
1143 |
@{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\ |
|
1144 |
@{index_ML can: "('a -> 'b) -> 'a -> bool"} \\ |
|
55838 | 1145 |
@{index_ML_exception ERROR: string} \\ |
1146 |
@{index_ML_exception Fail: string} \\ |
|
39856 | 1147 |
@{index_ML Exn.is_interrupt: "exn -> bool"} \\ |
62505 | 1148 |
@{index_ML Exn.reraise: "exn -> 'a"} \\ |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56199
diff
changeset
|
1149 |
@{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\ |
39855 | 1150 |
\end{mldecls} |
1151 |
||
69597 | 1152 |
\<^descr> \<^ML>\<open>try\<close>~\<open>f x\<close> makes the partiality of evaluating \<open>f x\<close> explicit via the |
61854 | 1153 |
option datatype. Interrupts are \<^emph>\<open>not\<close> handled here, i.e.\ this form serves |
69597 | 1154 |
as safe replacement for the \<^emph>\<open>unsafe\<close> version \<^ML_text>\<open>(SOME\<close>~\<open>f |
1155 |
x\<close>~\<^ML_text>\<open>handle _ => NONE)\<close> that is occasionally seen in books about |
|
61854 | 1156 |
SML97, but not in Isabelle/ML. |
39855 | 1157 |
|
69597 | 1158 |
\<^descr> \<^ML>\<open>can\<close> is similar to \<^ML>\<open>try\<close> with more abstract result. |
1159 |
||
1160 |
\<^descr> \<^ML>\<open>ERROR\<close>~\<open>msg\<close> represents user errors; this exception is normally |
|
1161 |
raised indirectly via the \<^ML>\<open>error\<close> function (see |
|
61854 | 1162 |
\secref{sec:message-channels}). |
39856 | 1163 |
|
69597 | 1164 |
\<^descr> \<^ML>\<open>Fail\<close>~\<open>msg\<close> represents general program failures. |
1165 |
||
1166 |
\<^descr> \<^ML>\<open>Exn.is_interrupt\<close> identifies interrupts robustly, without mentioning |
|
61854 | 1167 |
concrete exception constructors in user code. Handled interrupts need to be |
1168 |
re-raised promptly! |
|
1169 |
||
69597 | 1170 |
\<^descr> \<^ML>\<open>Exn.reraise\<close>~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit |
61854 | 1171 |
position information (if possible, depending on the ML platform). |
39856 | 1172 |
|
69597 | 1173 |
\<^descr> \<^ML>\<open>Runtime.exn_trace\<close>~\<^ML_text>\<open>(fn () =>\<close>~\<open>e\<close>\<^ML_text>\<open>)\<close> evaluates |
61854 | 1174 |
expression \<open>e\<close> while printing a full trace of its stack of nested exceptions |
1175 |
(if possible, depending on the ML platform). |
|
39855 | 1176 |
|
69597 | 1177 |
Inserting \<^ML>\<open>Runtime.exn_trace\<close> into ML code temporarily is useful for |
61854 | 1178 |
debugging, but not suitable for production code. |
58618 | 1179 |
\<close> |
1180 |
||
1181 |
text %mlantiq \<open> |
|
39866
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
1182 |
\begin{matharray}{rcl} |
61493 | 1183 |
@{ML_antiquotation_def "assert"} & : & \<open>ML_antiquotation\<close> \\ |
64465
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1184 |
@{ML_antiquotation_def "undefined"} & : & \<open>ML_antiquotation\<close> \\ |
39866
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
1185 |
\end{matharray} |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
1186 |
|
69597 | 1187 |
\<^descr> \<open>@{assert}\<close> inlines a function \<^ML_type>\<open>bool -> unit\<close> that raises \<^ML>\<open>Fail\<close> if the argument is \<^ML>\<open>false\<close>. Due to inlining the source position of |
61854 | 1188 |
failed assertions is included in the error output. |
64465
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1189 |
|
69597 | 1190 |
\<^descr> \<open>@{undefined}\<close> inlines \<^verbatim>\<open>raise\<close>~\<^ML>\<open>Match\<close>, i.e.\ the ML program |
64465
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1191 |
behaves as in some function application of an undefined case. |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1192 |
\<close> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1193 |
|
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1194 |
text %mlex \<open> |
69597 | 1195 |
The ML function \<^ML>\<open>undefined\<close> is defined in \<^file>\<open>~~/src/Pure/library.ML\<close> |
64465
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1196 |
as follows: |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1197 |
\<close> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1198 |
|
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1199 |
ML \<open>fun undefined _ = raise Match\<close> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1200 |
|
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1201 |
text \<open> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1202 |
\<^medskip> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1203 |
The following variant uses the antiquotation @{ML_antiquotation undefined} |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1204 |
instead: |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1205 |
\<close> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1206 |
|
69597 | 1207 |
ML \<open>fun undefined _ = \<^undefined>\<close> |
64465
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1208 |
|
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1209 |
text \<open> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1210 |
\<^medskip> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1211 |
Here is the same, using control-symbol notation for the antiquotation, with |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1212 |
special rendering of \<^verbatim>\<open>\<^undefined>\<close>: |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1213 |
\<close> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1214 |
|
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1215 |
ML \<open>fun undefined _ = \<^undefined>\<close> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1216 |
|
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1217 |
text \<open> |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1218 |
\medskip Semantically, all forms are equivalent to a function definition |
73069f272f42
documentation of @{undefined} (actually introduced in Isabelle2016);
wenzelm
parents:
64464
diff
changeset
|
1219 |
without any clauses, but that is syntactically not allowed in ML. |
58618 | 1220 |
\<close> |
1221 |
||
1222 |
||
1223 |
section \<open>Strings of symbols \label{sec:symbols}\<close> |
|
1224 |
||
61854 | 1225 |
text \<open> |
1226 |
A \<^emph>\<open>symbol\<close> constitutes the smallest textual unit in Isabelle/ML --- raw ML |
|
1227 |
characters are normally not encountered at all. Isabelle strings consist of |
|
1228 |
a sequence of symbols, represented as a packed string or an exploded list of |
|
1229 |
strings. Each symbol is in itself a small string, which has either one of |
|
61504 | 1230 |
the following forms: |
1231 |
||
1232 |
\<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'', |
|
1233 |
||
1234 |
\<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence), |
|
1235 |
||
1236 |
\<^enum> a regular symbol ``\<^verbatim>\<open>\<ident>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'', |
|
1237 |
||
1238 |
\<^enum> a control symbol ``\<^verbatim>\<open>\<^ident>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'', |
|
1239 |
||
1240 |
The \<open>ident\<close> syntax for symbol names is \<open>letter (letter | digit)\<^sup>*\<close>, where |
|
1241 |
\<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular |
|
1242 |
symbols and control symbols, but a fixed collection of standard symbols is |
|
1243 |
treated specifically. For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is classified as a letter, which |
|
1244 |
means it may occur within regular Isabelle identifiers. |
|
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1245 |
|
57421 | 1246 |
The character set underlying Isabelle symbols is 7-bit ASCII, but 8-bit |
1247 |
character sequences are passed-through unchanged. Unicode/UCS data in UTF-8 |
|
1248 |
encoding is processed in a non-strict fashion, such that well-formed code |
|
1249 |
sequences are recognized accordingly. Unicode provides its own collection of |
|
1250 |
mathematical symbols, but within the core Isabelle/ML world there is no link |
|
1251 |
to the standard collection of Isabelle regular symbols. |
|
1252 |
||
61416 | 1253 |
\<^medskip> |
61504 | 1254 |
Output of Isabelle symbols depends on the print mode. For example, the |
1255 |
standard {\LaTeX} setup of the Isabelle document preparation system would |
|
1256 |
present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering usually |
|
1257 |
works by mapping a finite subset of Isabelle symbols to suitable Unicode |
|
1258 |
characters. |
|
58618 | 1259 |
\<close> |
1260 |
||
1261 |
text %mlref \<open> |
|
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1262 |
\begin{mldecls} |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1263 |
@{index_ML_type "Symbol.symbol": string} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1264 |
@{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1265 |
@{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1266 |
@{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1267 |
@{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1268 |
@{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1269 |
\end{mldecls} |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1270 |
\begin{mldecls} |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1271 |
@{index_ML_type "Symbol.sym"} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1272 |
@{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1273 |
\end{mldecls} |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1274 |
|
69597 | 1275 |
\<^descr> Type \<^ML_type>\<open>Symbol.symbol\<close> represents individual Isabelle symbols. |
1276 |
||
1277 |
\<^descr> \<^ML>\<open>Symbol.explode\<close>~\<open>str\<close> produces a symbol list from the packed form. |
|
1278 |
This function supersedes \<^ML>\<open>String.explode\<close> for virtually all purposes |
|
61854 | 1279 |
of manipulating text in Isabelle!\<^footnote>\<open>The runtime overhead for exploded strings |
1280 |
is mainly that of the list structure: individual symbols that happen to be a |
|
1281 |
singleton string do not require extra memory in Poly/ML.\<close> |
|
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1282 |
|
69597 | 1283 |
\<^descr> \<^ML>\<open>Symbol.is_letter\<close>, \<^ML>\<open>Symbol.is_digit\<close>, \<^ML>\<open>Symbol.is_quasi\<close>, \<^ML>\<open>Symbol.is_blank\<close> classify standard symbols |
61854 | 1284 |
according to fixed syntactic conventions of Isabelle, cf.\ @{cite |
1285 |
"isabelle-isar-ref"}. |
|
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1286 |
|
69597 | 1287 |
\<^descr> Type \<^ML_type>\<open>Symbol.sym\<close> is a concrete datatype that represents the |
1288 |
different kinds of symbols explicitly, with constructors \<^ML>\<open>Symbol.Char\<close>, \<^ML>\<open>Symbol.UTF8\<close>, \<^ML>\<open>Symbol.Sym\<close>, \<^ML>\<open>Symbol.Control\<close>, \<^ML>\<open>Symbol.Malformed\<close>. |
|
1289 |
||
1290 |
\<^descr> \<^ML>\<open>Symbol.decode\<close> converts the string representation of a symbol into |
|
61854 | 1291 |
the datatype version. |
61506 | 1292 |
\<close> |
1293 |
||
1294 |
paragraph \<open>Historical note.\<close> |
|
61854 | 1295 |
text \<open> |
69597 | 1296 |
In the original SML90 standard the primitive ML type \<^ML_type>\<open>char\<close> did not |
1297 |
exists, and \<^ML_text>\<open>explode: string -> string list\<close> produced a list of |
|
1298 |
singleton strings like \<^ML>\<open>raw_explode: string -> string list\<close> in |
|
61506 | 1299 |
Isabelle/ML today. When SML97 came out, Isabelle did not adopt its somewhat |
1300 |
anachronistic 8-bit or 16-bit characters, but the idea of exploding a string |
|
1301 |
into a list of small strings was extended to ``symbols'' as explained above. |
|
1302 |
Thus Isabelle sources can refer to an infinite store of user-defined |
|
1303 |
symbols, without having to worry about the multitude of Unicode encodings |
|
61854 | 1304 |
that have emerged over the years. |
1305 |
\<close> |
|
58618 | 1306 |
|
1307 |
||
1308 |
section \<open>Basic data types\<close> |
|
1309 |
||
61854 | 1310 |
text \<open> |
1311 |
The basis library proposal of SML97 needs to be treated with caution. Many |
|
1312 |
of its operations simply do not fit with important Isabelle/ML conventions |
|
1313 |
(like ``canonical argument order'', see |
|
1314 |
\secref{sec:canonical-argument-order}), others cause problems with the |
|
69597 | 1315 |
parallel evaluation model of Isabelle/ML (such as \<^ML>\<open>TextIO.print\<close> or \<^ML>\<open>OS.Process.system\<close>). |
39859 | 1316 |
|
61854 | 1317 |
Subsequently we give a brief overview of important operations on basic ML |
1318 |
data types. |
|
58618 | 1319 |
\<close> |
1320 |
||
1321 |
||
1322 |
subsection \<open>Characters\<close> |
|
1323 |
||
1324 |
text %mlref \<open> |
|
39863 | 1325 |
\begin{mldecls} |
1326 |
@{index_ML_type char} \\ |
|
1327 |
\end{mldecls} |
|
1328 |
||
69597 | 1329 |
\<^descr> Type \<^ML_type>\<open>char\<close> is \<^emph>\<open>not\<close> used. The smallest textual unit in Isabelle |
61854 | 1330 |
is represented as a ``symbol'' (see \secref{sec:symbols}). |
58618 | 1331 |
\<close> |
1332 |
||
1333 |
||
1334 |
subsection \<open>Strings\<close> |
|
1335 |
||
1336 |
text %mlref \<open> |
|
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1337 |
\begin{mldecls} |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1338 |
@{index_ML_type string} \\ |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1339 |
\end{mldecls} |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1340 |
|
69597 | 1341 |
\<^descr> Type \<^ML_type>\<open>string\<close> represents immutable vectors of 8-bit characters. |
61854 | 1342 |
There are operations in SML to convert back and forth to actual byte |
1343 |
vectors, which are seldom used. |
|
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1344 |
|
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1345 |
This historically important raw text representation is used for |
61854 | 1346 |
Isabelle-specific purposes with the following implicit substructures packed |
1347 |
into the string content: |
|
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1348 |
|
69597 | 1349 |
\<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with \<^ML>\<open>Symbol.explode\<close> as key operation; |
61458 | 1350 |
|
61854 | 1351 |
\<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}), with |
69597 | 1352 |
\<^ML>\<open>YXML.parse_body\<close> as key operation. |
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1353 |
|
58723 | 1354 |
Note that Isabelle/ML string literals may refer Isabelle symbols like |
61854 | 1355 |
``\<^verbatim>\<open>\<alpha>\<close>'' natively, \<^emph>\<open>without\<close> escaping the backslash. This is a consequence |
1356 |
of Isabelle treating all source text as strings of symbols, instead of raw |
|
1357 |
characters. |
|
58618 | 1358 |
\<close> |
1359 |
||
61854 | 1360 |
text %mlex \<open> |
1361 |
The subsequent example illustrates the difference of physical addressing of |
|
1362 |
bytes versus logical addressing of symbols in Isabelle strings. |
|
58618 | 1363 |
\<close> |
1364 |
||
1365 |
ML_val \<open> |
|
52421
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1366 |
val s = "\<A>"; |
6d93140a206c
clarified strings of symbols, including ML string literals;
wenzelm
parents:
52420
diff
changeset
|
1367 |
|
69597 | 1368 |
\<^assert> (length (Symbol.explode s) = 1); |
1369 |
\<^assert> (size s = 4); |
|
58618 | 1370 |
\<close> |
1371 |
||
61854 | 1372 |
text \<open> |
1373 |
Note that in Unicode renderings of the symbol \<open>\<A>\<close>, variations of encodings |
|
1374 |
like UTF-8 or UTF-16 pose delicate questions about the multi-byte |
|
1375 |
representations of its codepoint, which is outside of the 16-bit address |
|
1376 |
space of the original Unicode standard from the 1990-ies. In Isabelle/ML it |
|
1377 |
is just ``\<^verbatim>\<open>\<A>\<close>'' literally, using plain ASCII characters beyond any |
|
1378 |
doubts. |
|
1379 |
\<close> |
|
58618 | 1380 |
|
1381 |
||
1382 |
subsection \<open>Integers\<close> |
|
1383 |
||
1384 |
text %mlref \<open> |
|
39862 | 1385 |
\begin{mldecls} |
1386 |
@{index_ML_type int} \\ |
|
1387 |
\end{mldecls} |
|
1388 |
||
69597 | 1389 |
\<^descr> Type \<^ML_type>\<open>int\<close> represents regular mathematical integers, which are |
61854 | 1390 |
\<^emph>\<open>unbounded\<close>. Overflow is treated properly, but should never happen in |
1391 |
practice.\<^footnote>\<open>The size limit for integer bit patterns in memory is 64\,MB for |
|
62354 | 1392 |
32-bit Poly/ML, and much higher for 64-bit systems.\<close> |
39862 | 1393 |
|
69597 | 1394 |
Structure \<^ML_structure>\<open>IntInf\<close> of SML97 is obsolete and superseded by |
1395 |
\<^ML_structure>\<open>Int\<close>. Structure \<^ML_structure>\<open>Integer\<close> in |
|
63680 | 1396 |
\<^file>\<open>~~/src/Pure/General/integer.ML\<close> provides some additional operations. |
58618 | 1397 |
\<close> |
1398 |
||
1399 |
||
63215 | 1400 |
subsection \<open>Rational numbers\<close> |
1401 |
||
1402 |
text %mlref \<open> |
|
1403 |
\begin{mldecls} |
|
1404 |
@{index_ML_type Rat.rat} \\ |
|
1405 |
\end{mldecls} |
|
1406 |
||
69597 | 1407 |
\<^descr> Type \<^ML_type>\<open>Rat.rat\<close> represents rational numbers, based on the |
63215 | 1408 |
unbounded integers of Poly/ML. |
1409 |
||
1410 |
Literal rationals may be written with special antiquotation syntax |
|
1411 |
\<^verbatim>\<open>@\<close>\<open>int\<close>\<^verbatim>\<open>/\<close>\<open>nat\<close> or \<^verbatim>\<open>@\<close>\<open>int\<close> (without any white space). For example |
|
1412 |
\<^verbatim>\<open>@~1/4\<close> or \<^verbatim>\<open>@10\<close>. The ML toplevel pretty printer uses the same format. |
|
1413 |
||
1414 |
Standard operations are provided via ad-hoc overloading of \<^verbatim>\<open>+\<close>, \<^verbatim>\<open>-\<close>, \<^verbatim>\<open>*\<close>, |
|
1415 |
\<^verbatim>\<open>/\<close>, etc. |
|
1416 |
\<close> |
|
1417 |
||
1418 |
||
58618 | 1419 |
subsection \<open>Time\<close> |
1420 |
||
1421 |
text %mlref \<open> |
|
40302 | 1422 |
\begin{mldecls} |
1423 |
@{index_ML_type Time.time} \\ |
|
1424 |
@{index_ML seconds: "real -> Time.time"} \\ |
|
1425 |
\end{mldecls} |
|
1426 |
||
69597 | 1427 |
\<^descr> Type \<^ML_type>\<open>Time.time\<close> represents time abstractly according to the |
61854 | 1428 |
SML97 basis library definition. This is adequate for internal ML operations, |
1429 |
but awkward in concrete time specifications. |
|
40302 | 1430 |
|
69597 | 1431 |
\<^descr> \<^ML>\<open>seconds\<close>~\<open>s\<close> turns the concrete scalar \<open>s\<close> (measured in seconds) into |
61854 | 1432 |
an abstract time value. Floating point numbers are easy to use as |
1433 |
configuration options in the context (see \secref{sec:config-options}) or |
|
1434 |
system options that are maintained externally. |
|
58618 | 1435 |
\<close> |
1436 |
||
1437 |
||
1438 |
subsection \<open>Options\<close> |
|
1439 |
||
1440 |
text %mlref \<open> |
|
39859 | 1441 |
\begin{mldecls} |
1442 |
@{index_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\ |
|
1443 |
@{index_ML is_some: "'a option -> bool"} \\ |
|
1444 |
@{index_ML is_none: "'a option -> bool"} \\ |
|
1445 |
@{index_ML the: "'a option -> 'a"} \\ |
|
1446 |
@{index_ML these: "'a list option -> 'a list"} \\ |
|
1447 |
@{index_ML the_list: "'a option -> 'a list"} \\ |
|
1448 |
@{index_ML the_default: "'a -> 'a option -> 'a"} \\ |
|
1449 |
\end{mldecls} |
|
58618 | 1450 |
\<close> |
1451 |
||
61854 | 1452 |
text \<open> |
69597 | 1453 |
Apart from \<^ML>\<open>Option.map\<close> most other operations defined in structure |
1454 |
\<^ML_structure>\<open>Option\<close> are alien to Isabelle/ML and never used. The |
|
63680 | 1455 |
operations shown above are defined in \<^file>\<open>~~/src/Pure/General/basics.ML\<close>. |
61854 | 1456 |
\<close> |
58618 | 1457 |
|
1458 |
||
1459 |
subsection \<open>Lists\<close> |
|
1460 |
||
61854 | 1461 |
text \<open> |
1462 |
Lists are ubiquitous in ML as simple and light-weight ``collections'' for |
|
1463 |
many everyday programming tasks. Isabelle/ML provides important additions |
|
1464 |
and improvements over operations that are predefined in the SML97 library. |
|
1465 |
\<close> |
|
58618 | 1466 |
|
1467 |
text %mlref \<open> |
|
39863 | 1468 |
\begin{mldecls} |
1469 |
@{index_ML cons: "'a -> 'a list -> 'a list"} \\ |
|
39874 | 1470 |
@{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\ |
1471 |
@{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\ |
|
1472 |
@{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\ |
|
1473 |
@{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\ |
|
39863 | 1474 |
\end{mldecls} |
1475 |
||
69597 | 1476 |
\<^descr> \<^ML>\<open>cons\<close>~\<open>x xs\<close> evaluates to \<open>x :: xs\<close>. |
39863 | 1477 |
|
61854 | 1478 |
Tupled infix operators are a historical accident in Standard ML. The curried |
69597 | 1479 |
\<^ML>\<open>cons\<close> amends this, but it should be only used when partial application |
61854 | 1480 |
is required. |
39863 | 1481 |
|
69597 | 1482 |
\<^descr> \<^ML>\<open>member\<close>, \<^ML>\<open>insert\<close>, \<^ML>\<open>remove\<close>, \<^ML>\<open>update\<close> treat lists as a |
63680 | 1483 |
set-like container that maintains the order of elements. See |
1484 |
\<^file>\<open>~~/src/Pure/library.ML\<close> for the full specifications (written in ML). |
|
69597 | 1485 |
There are some further derived operations like \<^ML>\<open>union\<close> or \<^ML>\<open>inter\<close>. |
1486 |
||
1487 |
Note that \<^ML>\<open>insert\<close> is conservative about elements that are already a |
|
1488 |
\<^ML>\<open>member\<close> of the list, while \<^ML>\<open>update\<close> ensures that the latest entry |
|
61854 | 1489 |
is always put in front. The latter discipline is often more appropriate in |
1490 |
declarations of context data (\secref{sec:context-data}) that are issued by |
|
1491 |
the user in Isar source: later declarations take precedence over earlier |
|
1492 |
ones. \<close> |
|
58618 | 1493 |
|
61854 | 1494 |
text %mlex \<open> |
69597 | 1495 |
Using canonical \<^ML>\<open>fold\<close> together with \<^ML>\<open>cons\<close> (or similar standard |
61854 | 1496 |
operations) alternates the orientation of data. The is quite natural and |
69597 | 1497 |
should not be altered forcible by inserting extra applications of \<^ML>\<open>rev\<close>. |
1498 |
The alternative \<^ML>\<open>fold_rev\<close> can be used in the few situations, where |
|
61854 | 1499 |
alternation should be prevented. |
58618 | 1500 |
\<close> |
1501 |
||
59902 | 1502 |
ML_val \<open> |
39863 | 1503 |
val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]; |
1504 |
||
1505 |
val list1 = fold cons items []; |
|
69597 | 1506 |
\<^assert> (list1 = rev items); |
39866
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39864
diff
changeset
|
1507 |
|
39863 | 1508 |
val list2 = fold_rev cons items []; |
69597 | 1509 |
\<^assert> (list2 = items); |
58618 | 1510 |
\<close> |
1511 |
||
61854 | 1512 |
text \<open> |
1513 |
The subsequent example demonstrates how to \<^emph>\<open>merge\<close> two lists in a natural |
|
1514 |
way. |
|
1515 |
\<close> |
|
58618 | 1516 |
|
59902 | 1517 |
ML_val \<open> |
39883 | 1518 |
fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs; |
58618 | 1519 |
\<close> |
1520 |
||
61854 | 1521 |
text \<open> |
1522 |
Here the first list is treated conservatively: only the new elements from |
|
69597 | 1523 |
the second list are inserted. The inside-out order of insertion via \<^ML>\<open>fold_rev\<close> attempts to preserve the order of elements in the result. |
39883 | 1524 |
|
1525 |
This way of merging lists is typical for context data |
|
69597 | 1526 |
(\secref{sec:context-data}). See also \<^ML>\<open>merge\<close> as defined in |
63680 | 1527 |
\<^file>\<open>~~/src/Pure/library.ML\<close>. |
58618 | 1528 |
\<close> |
1529 |
||
1530 |
||
1531 |
subsection \<open>Association lists\<close> |
|
1532 |
||
61854 | 1533 |
text \<open> |
1534 |
The operations for association lists interpret a concrete list of pairs as a |
|
1535 |
finite function from keys to values. Redundant representations with multiple |
|
1536 |
occurrences of the same key are implicitly normalized: lookup and update |
|
1537 |
only take the first occurrence into account. |
|
58618 | 1538 |
\<close> |
1539 |
||
1540 |
text \<open> |
|
39875
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1541 |
\begin{mldecls} |
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1542 |
@{index_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\ |
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1543 |
@{index_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\ |
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1544 |
@{index_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\ |
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1545 |
\end{mldecls} |
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1546 |
|
69597 | 1547 |
\<^descr> \<^ML>\<open>AList.lookup\<close>, \<^ML>\<open>AList.defined\<close>, \<^ML>\<open>AList.update\<close> implement the |
61854 | 1548 |
main ``framework operations'' for mappings in Isabelle/ML, following |
1549 |
standard conventions for their names and types. |
|
39875
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1550 |
|
61854 | 1551 |
Note that a function called \<^verbatim>\<open>lookup\<close> is obliged to express its partiality |
1552 |
via an explicit option element. There is no choice to raise an exception, |
|
1553 |
without changing the name to something like \<open>the_element\<close> or \<open>get\<close>. |
|
61493 | 1554 |
|
69597 | 1555 |
The \<open>defined\<close> operation is essentially a contraction of \<^ML>\<open>is_some\<close> and |
61854 | 1556 |
\<^verbatim>\<open>lookup\<close>, but this is sufficiently frequent to justify its independent |
1557 |
existence. This also gives the implementation some opportunity for peep-hole |
|
1558 |
optimization. |
|
39875
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1559 |
|
648c930125f6
more on "Association lists", based on more succinct version of older material;
wenzelm
parents:
39874
diff
changeset
|
1560 |
|
57421 | 1561 |
Association lists are adequate as simple implementation of finite mappings |
1562 |
in many practical situations. A more advanced table structure is defined in |
|
63680 | 1563 |
\<^file>\<open>~~/src/Pure/General/table.ML\<close>; that version scales easily to thousands or |
1564 |
millions of elements. |
|
58618 | 1565 |
\<close> |
1566 |
||
1567 |
||
1568 |
subsection \<open>Unsynchronized references\<close> |
|
1569 |
||
1570 |
text %mlref \<open> |
|
39859 | 1571 |
\begin{mldecls} |
39870 | 1572 |
@{index_ML_type "'a Unsynchronized.ref"} \\ |
39859 | 1573 |
@{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\ |
1574 |
@{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\ |
|
46262 | 1575 |
@{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\ |
39859 | 1576 |
\end{mldecls} |
58618 | 1577 |
\<close> |
1578 |
||
61854 | 1579 |
text \<open> |
1580 |
Due to ubiquitous parallelism in Isabelle/ML (see also |
|
1581 |
\secref{sec:multi-threading}), the mutable reference cells of Standard ML |
|
1582 |
are notorious for causing problems. In a highly parallel system, both |
|
1583 |
correctness \<^emph>\<open>and\<close> performance are easily degraded when using mutable data. |
|
39859 | 1584 |
|
69597 | 1585 |
The unwieldy name of \<^ML>\<open>Unsynchronized.ref\<close> for the constructor for |
61854 | 1586 |
references in Isabelle/ML emphasizes the inconveniences caused by |
69597 | 1587 |
mutability. Existing operations \<^ML>\<open>!\<close> and \<^ML_op>\<open>:=\<close> are unchanged, |
61854 | 1588 |
but should be used with special precautions, say in a strictly local |
1589 |
situation that is guaranteed to be restricted to sequential evaluation --- |
|
1590 |
now and in the future. |
|
40508 | 1591 |
|
1592 |
\begin{warn} |
|
69597 | 1593 |
Never \<^ML_text>\<open>open Unsynchronized\<close>, not even in a local scope! |
40508 | 1594 |
Pretending that mutable state is no problem is a very bad idea. |
1595 |
\end{warn} |
|
58618 | 1596 |
\<close> |
1597 |
||
1598 |
||
1599 |
section \<open>Thread-safe programming \label{sec:multi-threading}\<close> |
|
1600 |
||
61854 | 1601 |
text \<open> |
1602 |
Multi-threaded execution has become an everyday reality in Isabelle since |
|
1603 |
Poly/ML 5.2.1 and Isabelle2008. Isabelle/ML provides implicit and explicit |
|
1604 |
parallelism by default, and there is no way for user-space tools to ``opt |
|
1605 |
out''. ML programs that are purely functional, output messages only via the |
|
1606 |
official channels (\secref{sec:message-channels}), and do not intercept |
|
1607 |
interrupts (\secref{sec:exceptions}) can participate in the multi-threaded |
|
39868 | 1608 |
environment immediately without further ado. |
1609 |
||
61854 | 1610 |
More ambitious tools with more fine-grained interaction with the environment |
1611 |
need to observe the principles explained below. |
|
58618 | 1612 |
\<close> |
1613 |
||
1614 |
||
1615 |
subsection \<open>Multi-threading with shared memory\<close> |
|
1616 |
||
61854 | 1617 |
text \<open> |
1618 |
Multiple threads help to organize advanced operations of the system, such as |
|
1619 |
real-time conditions on command transactions, sub-components with explicit |
|
1620 |
communication, general asynchronous interaction etc. Moreover, parallel |
|
1621 |
evaluation is a prerequisite to make adequate use of the CPU resources that |
|
1622 |
are available on multi-core systems.\<^footnote>\<open>Multi-core computing does not mean |
|
1623 |
that there are ``spare cycles'' to be wasted. It means that the continued |
|
1624 |
exponential speedup of CPU performance due to ``Moore's Law'' follows |
|
1625 |
different rules: clock frequency has reached its peak around 2005, and |
|
1626 |
applications need to be parallelized in order to avoid a perceived loss of |
|
1627 |
performance. See also @{cite "Sutter:2005"}.\<close> |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1628 |
|
57421 | 1629 |
Isabelle/Isar exploits the inherent structure of theories and proofs to |
61854 | 1630 |
support \<^emph>\<open>implicit parallelism\<close> to a large extent. LCF-style theorem proving |
1631 |
provides almost ideal conditions for that, see also @{cite "Wenzel:2009"}. |
|
1632 |
This means, significant parts of theory and proof checking is parallelized |
|
1633 |
by default. In Isabelle2013, a maximum speedup-factor of 3.5 on 4 cores and |
|
1634 |
6.5 on 8 cores can be expected @{cite "Wenzel:2013:ITP"}. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1635 |
|
61416 | 1636 |
\<^medskip> |
61854 | 1637 |
ML threads lack the memory protection of separate processes, and operate |
1638 |
concurrently on shared heap memory. This has the advantage that results of |
|
1639 |
independent computations are directly available to other threads: abstract |
|
1640 |
values can be passed without copying or awkward serialization that is |
|
1641 |
typically required for separate processes. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1642 |
|
61854 | 1643 |
To make shared-memory multi-threading work robustly and efficiently, some |
1644 |
programming guidelines need to be observed. While the ML system is |
|
1645 |
responsible to maintain basic integrity of the representation of ML values |
|
1646 |
in memory, the application programmer needs to ensure that multi-threaded |
|
1647 |
execution does not break the intended semantics. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1648 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1649 |
\begin{warn} |
61854 | 1650 |
To participate in implicit parallelism, tools need to be thread-safe. A |
1651 |
single ill-behaved tool can affect the stability and performance of the |
|
1652 |
whole system. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1653 |
\end{warn} |
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1654 |
|
57421 | 1655 |
Apart from observing the principles of thread-safeness passively, advanced |
1656 |
tools may also exploit parallelism actively, e.g.\ by using library |
|
39868 | 1657 |
functions for parallel list operations (\secref{sec:parlist}). |
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1658 |
|
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1659 |
\begin{warn} |
61854 | 1660 |
Parallel computing resources are managed centrally by the Isabelle/ML |
1661 |
infrastructure. User programs should not fork their own ML threads to |
|
1662 |
perform heavy computations. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1663 |
\end{warn} |
58618 | 1664 |
\<close> |
1665 |
||
1666 |
||
1667 |
subsection \<open>Critical shared resources\<close> |
|
1668 |
||
61854 | 1669 |
text \<open> |
1670 |
Thread-safeness is mainly concerned about concurrent read/write access to |
|
1671 |
shared resources, which are outside the purely functional world of ML. This |
|
1672 |
covers the following in particular. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1673 |
|
61854 | 1674 |
\<^item> Global references (or arrays), i.e.\ mutable memory cells that persist |
1675 |
over several invocations of associated operations.\<^footnote>\<open>This is independent of |
|
1676 |
the visibility of such mutable values in the toplevel scope.\<close> |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1677 |
|
61854 | 1678 |
\<^item> Global state of the running Isabelle/ML process, i.e.\ raw I/O channels, |
1679 |
environment variables, current working directory. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1680 |
|
61854 | 1681 |
\<^item> Writable resources in the file-system that are shared among different |
1682 |
threads or external processes. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1683 |
|
61854 | 1684 |
Isabelle/ML provides various mechanisms to avoid critical shared resources |
1685 |
in most situations. As last resort there are some mechanisms for explicit |
|
1686 |
synchronization. The following guidelines help to make Isabelle/ML programs |
|
1687 |
work smoothly in a concurrent environment. |
|
1688 |
||
1689 |
\<^item> Avoid global references altogether. Isabelle/Isar maintains a uniform |
|
1690 |
context that incorporates arbitrary data declared by user programs |
|
1691 |
(\secref{sec:context-data}). This context is passed as plain value and user |
|
1692 |
tools can get/map their own data in a purely functional manner. |
|
1693 |
Configuration options within the context (\secref{sec:config-options}) |
|
1694 |
provide simple drop-in replacements for historic reference variables. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1695 |
|
61854 | 1696 |
\<^item> Keep components with local state information re-entrant. Instead of poking |
1697 |
initial values into (private) global references, a new state record can be |
|
1698 |
created on each invocation, and passed through any auxiliary functions of |
|
1699 |
the component. The state record contain mutable references in special |
|
1700 |
situations, without requiring any synchronization, as long as each |
|
1701 |
invocation gets its own copy and the tool itself is single-threaded. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1702 |
|
61854 | 1703 |
\<^item> Avoid raw output on \<open>stdout\<close> or \<open>stderr\<close>. The Poly/ML library is |
1704 |
thread-safe for each individual output operation, but the ordering of |
|
1705 |
parallel invocations is arbitrary. This means raw output will appear on some |
|
1706 |
system console with unpredictable interleaving of atomic chunks. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1707 |
|
39868 | 1708 |
Note that this does not affect regular message output channels |
61854 | 1709 |
(\secref{sec:message-channels}). An official message id is associated with |
1710 |
the command transaction from where it originates, independently of other |
|
1711 |
transactions. This means each running Isar command has effectively its own |
|
1712 |
set of message channels, and interleaving can only happen when commands use |
|
1713 |
parallelism internally (and only at message boundaries). |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1714 |
|
61854 | 1715 |
\<^item> Treat environment variables and the current working directory of the |
1716 |
running process as read-only. |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1717 |
|
61854 | 1718 |
\<^item> Restrict writing to the file-system to unique temporary files. Isabelle |
1719 |
already provides a temporary directory that is unique for the running |
|
1720 |
process, and there is a centralized source of unique serial numbers in |
|
1721 |
Isabelle/ML. Thus temporary files that are passed to to some external |
|
1722 |
process will be always disjoint, and thus thread-safe. |
|
58618 | 1723 |
\<close> |
1724 |
||
1725 |
text %mlref \<open> |
|
39868 | 1726 |
\begin{mldecls} |
1727 |
@{index_ML File.tmp_path: "Path.T -> Path.T"} \\ |
|
1728 |
@{index_ML serial_string: "unit -> string"} \\ |
|
1729 |
\end{mldecls} |
|
1730 |
||
69597 | 1731 |
\<^descr> \<^ML>\<open>File.tmp_path\<close>~\<open>path\<close> relocates the base component of \<open>path\<close> into the |
61854 | 1732 |
unique temporary directory of the running Isabelle/ML process. |
39868 | 1733 |
|
69597 | 1734 |
\<^descr> \<^ML>\<open>serial_string\<close>~\<open>()\<close> creates a new serial number that is unique over |
61854 | 1735 |
the runtime of the Isabelle/ML process. |
58618 | 1736 |
\<close> |
1737 |
||
61854 | 1738 |
text %mlex \<open> |
1739 |
The following example shows how to create unique temporary file names. |
|
58618 | 1740 |
\<close> |
1741 |
||
59902 | 1742 |
ML_val \<open> |
39868 | 1743 |
val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ())); |
1744 |
val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ())); |
|
69597 | 1745 |
\<^assert> (tmp1 <> tmp2); |
58618 | 1746 |
\<close> |
1747 |
||
1748 |
||
1749 |
subsection \<open>Explicit synchronization\<close> |
|
1750 |
||
61854 | 1751 |
text \<open> |
1752 |
Isabelle/ML provides explicit synchronization for mutable variables over |
|
59180
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59138
diff
changeset
|
1753 |
immutable data, which may be updated atomically and exclusively. This |
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59138
diff
changeset
|
1754 |
addresses the rare situations where mutable shared resources are really |
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59138
diff
changeset
|
1755 |
required. Synchronization in Isabelle/ML is based on primitives of Poly/ML, |
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59138
diff
changeset
|
1756 |
which have been adapted to the specific assumptions of the concurrent |
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59138
diff
changeset
|
1757 |
Isabelle environment. User code should not break this abstraction, but stay |
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59138
diff
changeset
|
1758 |
within the confines of concurrent Isabelle/ML. |
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59138
diff
changeset
|
1759 |
|
61854 | 1760 |
A \<^emph>\<open>synchronized variable\<close> is an explicit state component associated with |
1761 |
mechanisms for locking and signaling. There are operations to await a |
|
59180
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59138
diff
changeset
|
1762 |
condition, change the state, and signal the change to all other waiting |
61477 | 1763 |
threads. Synchronized access to the state variable is \<^emph>\<open>not\<close> re-entrant: |
61854 | 1764 |
direct or indirect nesting within the same thread will cause a deadlock! |
1765 |
\<close> |
|
58618 | 1766 |
|
1767 |
text %mlref \<open> |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1768 |
\begin{mldecls} |
39871 | 1769 |
@{index_ML_type "'a Synchronized.var"} \\ |
1770 |
@{index_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\ |
|
1771 |
@{index_ML Synchronized.guarded_access: "'a Synchronized.var -> |
|
1772 |
('a -> ('b * 'a) option) -> 'b"} \\ |
|
1773 |
\end{mldecls} |
|
39867
a8363532cd4d
somewhat modernized version of "Thread-safe programming";
wenzelm
parents:
39866
diff
changeset
|
1774 |
|
69597 | 1775 |
\<^descr> Type \<^ML_type>\<open>'a Synchronized.var\<close> represents synchronized variables |
1776 |
with state of type \<^ML_type>\<open>'a\<close>. |
|
1777 |
||
1778 |
\<^descr> \<^ML>\<open>Synchronized.var\<close>~\<open>name x\<close> creates a synchronized variable that is |
|
61854 | 1779 |
initialized with value \<open>x\<close>. The \<open>name\<close> is used for tracing. |
61493 | 1780 |
|
69597 | 1781 |
\<^descr> \<^ML>\<open>Synchronized.guarded_access\<close>~\<open>var f\<close> lets the function \<open>f\<close> operate |
61854 | 1782 |
within a critical section on the state \<open>x\<close> as follows: if \<open>f x\<close> produces |
69597 | 1783 |
\<^ML>\<open>NONE\<close>, it continues to wait on the internal condition variable, |
61854 | 1784 |
expecting that some other thread will eventually change the content in a |
69597 | 1785 |
suitable manner; if \<open>f x\<close> produces \<^ML>\<open>SOME\<close>~\<open>(y, x')\<close> it is satisfied and |
61854 | 1786 |
assigns the new state value \<open>x'\<close>, broadcasts a signal to all waiting threads |
1787 |
on the associated condition variable, and returns the result \<open>y\<close>. |
|
39871 | 1788 |
|
69597 | 1789 |
There are some further variants of the \<^ML>\<open>Synchronized.guarded_access\<close> |
63680 | 1790 |
combinator, see \<^file>\<open>~~/src/Pure/Concurrent/synchronized.ML\<close> for details. |
58618 | 1791 |
\<close> |
1792 |
||
61854 | 1793 |
text %mlex \<open> |
1794 |
The following example implements a counter that produces positive integers |
|
1795 |
that are unique over the runtime of the Isabelle process: |
|
1796 |
\<close> |
|
58618 | 1797 |
|
59902 | 1798 |
ML_val \<open> |
39871 | 1799 |
local |
1800 |
val counter = Synchronized.var "counter" 0; |
|
1801 |
in |
|
1802 |
fun next () = |
|
1803 |
Synchronized.guarded_access counter |
|
1804 |
(fn i => |
|
1805 |
let val j = i + 1 |
|
1806 |
in SOME (j, j) end); |
|
1807 |
end; |
|
59902 | 1808 |
|
39871 | 1809 |
val a = next (); |
1810 |
val b = next (); |
|
69597 | 1811 |
\<^assert> (a <> b); |
58618 | 1812 |
\<close> |
1813 |
||
61416 | 1814 |
text \<open> |
1815 |
\<^medskip> |
|
63680 | 1816 |
See \<^file>\<open>~~/src/Pure/Concurrent/mailbox.ML\<close> how to implement a mailbox as |
1817 |
synchronized variable over a purely functional list. |
|
61854 | 1818 |
\<close> |
58618 | 1819 |
|
1820 |
||
1821 |
section \<open>Managed evaluation\<close> |
|
1822 |
||
61854 | 1823 |
text \<open> |
1824 |
Execution of Standard ML follows the model of strict functional evaluation |
|
1825 |
with optional exceptions. Evaluation happens whenever some function is |
|
1826 |
applied to (sufficiently many) arguments. The result is either an explicit |
|
1827 |
value or an implicit exception. |
|
52419 | 1828 |
|
61854 | 1829 |
\<^emph>\<open>Managed evaluation\<close> in Isabelle/ML organizes expressions and results to |
1830 |
control certain physical side-conditions, to say more specifically when and |
|
1831 |
how evaluation happens. For example, the Isabelle/ML library supports lazy |
|
1832 |
evaluation with memoing, parallel evaluation via futures, asynchronous |
|
1833 |
evaluation via promises, evaluation with time limit etc. |
|
52419 | 1834 |
|
61416 | 1835 |
\<^medskip> |
66663 | 1836 |
An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction |
1837 |
\<^verbatim>\<open>fn () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of |
|
1838 |
type \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required |
|
1839 |
to tell them apart --- the static type-system of SML is only of limited help |
|
61854 | 1840 |
here. |
52419 | 1841 |
|
66663 | 1842 |
The first form is more intuitive: some combinator \<^verbatim>\<open>(unit -> 'a) -> 'a\<close> |
1843 |
applies the given function to \<^verbatim>\<open>()\<close> to initiate the postponed evaluation |
|
1844 |
process. The second form is more flexible: some combinator |
|
1845 |
\<^verbatim>\<open>('a -> 'b) -> 'a -> 'b\<close> acts like a modified form of function application; |
|
1846 |
several such combinators may be cascaded to modify a given function, before |
|
1847 |
it is ultimately applied to some argument. |
|
52419 | 1848 |
|
61416 | 1849 |
\<^medskip> |
61854 | 1850 |
\<^emph>\<open>Reified results\<close> make the disjoint sum of regular values versions |
1851 |
exceptional situations explicit as ML datatype: \<open>'a result = Res of 'a | Exn |
|
1852 |
of exn\<close>. This is typically used for administrative purposes, to store the |
|
1853 |
overall outcome of an evaluation process. |
|
52419 | 1854 |
|
61854 | 1855 |
\<^emph>\<open>Parallel exceptions\<close> aggregate reified results, such that multiple |
1856 |
exceptions are digested as a collection in canonical form that identifies |
|
1857 |
exceptions according to their original occurrence. This is particular |
|
1858 |
important for parallel evaluation via futures \secref{sec:futures}, which |
|
1859 |
are organized as acyclic graph of evaluations that depend on other |
|
1860 |
evaluations: exceptions stemming from shared sub-graphs are exposed exactly |
|
1861 |
once and in the order of their original occurrence (e.g.\ when printed at |
|
1862 |
the toplevel). Interrupt counts as neutral element here: it is treated as |
|
1863 |
minimal information about some canceled evaluation process, and is absorbed |
|
1864 |
by the presence of regular program exceptions. |
|
1865 |
\<close> |
|
58618 | 1866 |
|
1867 |
text %mlref \<open> |
|
52419 | 1868 |
\begin{mldecls} |
1869 |
@{index_ML_type "'a Exn.result"} \\ |
|
1870 |
@{index_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ |
|
1871 |
@{index_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ |
|
1872 |
@{index_ML Exn.release: "'a Exn.result -> 'a"} \\ |
|
1873 |
@{index_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\ |
|
1874 |
@{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\ |
|
1875 |
\end{mldecls} |
|
1876 |
||
69597 | 1877 |
\<^descr> Type \<^ML_type>\<open>'a Exn.result\<close> represents the disjoint sum of ML results |
1878 |
explicitly, with constructor \<^ML>\<open>Exn.Res\<close> for regular values and \<^ML>\<open>Exn.Exn\<close> for exceptions. |
|
1879 |
||
1880 |
\<^descr> \<^ML>\<open>Exn.capture\<close>~\<open>f x\<close> manages the evaluation of \<open>f x\<close> such that |
|
1881 |
exceptions are made explicit as \<^ML>\<open>Exn.Exn\<close>. Note that this includes |
|
61854 | 1882 |
physical interrupts (see also \secref{sec:exceptions}), so the same |
1883 |
precautions apply to user code: interrupts must not be absorbed |
|
1884 |
accidentally! |
|
52419 | 1885 |
|
69597 | 1886 |
\<^descr> \<^ML>\<open>Exn.interruptible_capture\<close> is similar to \<^ML>\<open>Exn.capture\<close>, but |
61854 | 1887 |
interrupts are immediately re-raised as required for user code. |
52419 | 1888 |
|
69597 | 1889 |
\<^descr> \<^ML>\<open>Exn.release\<close>~\<open>result\<close> releases the original runtime result, exposing |
61854 | 1890 |
its regular value or raising the reified exception. |
52419 | 1891 |
|
69597 | 1892 |
\<^descr> \<^ML>\<open>Par_Exn.release_all\<close>~\<open>results\<close> combines results that were produced |
61854 | 1893 |
independently (e.g.\ by parallel evaluation). If all results are regular |
1894 |
values, that list is returned. Otherwise, the collection of all exceptions |
|
1895 |
is raised, wrapped-up as collective parallel exception. Note that the latter |
|
1896 |
prevents access to individual exceptions by conventional \<^verbatim>\<open>handle\<close> of ML. |
|
52419 | 1897 |
|
69597 | 1898 |
\<^descr> \<^ML>\<open>Par_Exn.release_first\<close> is similar to \<^ML>\<open>Par_Exn.release_all\<close>, but |
61854 | 1899 |
only the first (meaningful) exception that has occurred in the original |
1900 |
evaluation process is raised again, the others are ignored. That single |
|
1901 |
exception may get handled by conventional means in ML. |
|
58618 | 1902 |
\<close> |
1903 |
||
1904 |
||
1905 |
subsection \<open>Parallel skeletons \label{sec:parlist}\<close> |
|
1906 |
||
1907 |
text \<open> |
|
61854 | 1908 |
Algorithmic skeletons are combinators that operate on lists in parallel, in |
1909 |
the manner of well-known \<open>map\<close>, \<open>exists\<close>, \<open>forall\<close> etc. Management of |
|
1910 |
futures (\secref{sec:futures}) and their results as reified exceptions is |
|
1911 |
wrapped up into simple programming interfaces that resemble the sequential |
|
1912 |
versions. |
|
52420 | 1913 |
|
61854 | 1914 |
What remains is the application-specific problem to present expressions with |
1915 |
suitable \<^emph>\<open>granularity\<close>: each list element corresponds to one evaluation |
|
1916 |
task. If the granularity is too coarse, the available CPUs are not |
|
1917 |
saturated. If it is too fine-grained, CPU cycles are wasted due to the |
|
1918 |
overhead of organizing parallel processing. In the worst case, parallel |
|
52420 | 1919 |
performance will be less than the sequential counterpart! |
58618 | 1920 |
\<close> |
1921 |
||
1922 |
text %mlref \<open> |
|
52420 | 1923 |
\begin{mldecls} |
1924 |
@{index_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\ |
|
1925 |
@{index_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\ |
|
1926 |
\end{mldecls} |
|
1927 |
||
69597 | 1928 |
\<^descr> \<^ML>\<open>Par_List.map\<close>~\<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> is like \<^ML>\<open>map\<close>~\<open>f [x\<^sub>1, \<dots>, |
61854 | 1929 |
x\<^sub>n]\<close>, but the evaluation of \<open>f x\<^sub>i\<close> for \<open>i = 1, \<dots>, n\<close> is performed in |
1930 |
parallel. |
|
61493 | 1931 |
|
61854 | 1932 |
An exception in any \<open>f x\<^sub>i\<close> cancels the overall evaluation process. The |
69597 | 1933 |
final result is produced via \<^ML>\<open>Par_Exn.release_first\<close> as explained above, |
61854 | 1934 |
which means the first program exception that happened to occur in the |
1935 |
parallel evaluation is propagated, and all other failures are ignored. |
|
52420 | 1936 |
|
69597 | 1937 |
\<^descr> \<^ML>\<open>Par_List.get_some\<close>~\<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> produces some \<open>f x\<^sub>i\<close> that is of |
61854 | 1938 |
the form \<open>SOME y\<^sub>i\<close>, if that exists, otherwise \<open>NONE\<close>. Thus it is similar to |
69597 | 1939 |
\<^ML>\<open>Library.get_first\<close>, but subject to a non-deterministic parallel choice |
61854 | 1940 |
process. The first successful result cancels the overall evaluation process; |
69597 | 1941 |
other exceptions are propagated as for \<^ML>\<open>Par_List.map\<close>. |
52420 | 1942 |
|
61854 | 1943 |
This generic parallel choice combinator is the basis for derived forms, such |
69597 | 1944 |
as \<^ML>\<open>Par_List.find_some\<close>, \<^ML>\<open>Par_List.exists\<close>, \<^ML>\<open>Par_List.forall\<close>. |
58618 | 1945 |
\<close> |
1946 |
||
61854 | 1947 |
text %mlex \<open> |
1948 |
Subsequently, the Ackermann function is evaluated in parallel for some |
|
1949 |
ranges of arguments. |
|
1950 |
\<close> |
|
58618 | 1951 |
|
1952 |
ML_val \<open> |
|
52420 | 1953 |
fun ackermann 0 n = n + 1 |
1954 |
| ackermann m 0 = ackermann (m - 1) 1 |
|
1955 |
| ackermann m n = ackermann (m - 1) (ackermann m (n - 1)); |
|
1956 |
||
1957 |
Par_List.map (ackermann 2) (500 upto 1000); |
|
1958 |
Par_List.map (ackermann 3) (5 upto 10); |
|
58618 | 1959 |
\<close> |
1960 |
||
1961 |
||
1962 |
subsection \<open>Lazy evaluation\<close> |
|
1963 |
||
1964 |
text \<open> |
|
61854 | 1965 |
Classic lazy evaluation works via the \<open>lazy\<close>~/ \<open>force\<close> pair of operations: |
1966 |
\<open>lazy\<close> to wrap an unevaluated expression, and \<open>force\<close> to evaluate it once |
|
1967 |
and store its result persistently. Later invocations of \<open>force\<close> retrieve the |
|
1968 |
stored result without another evaluation. Isabelle/ML refines this idea to |
|
1969 |
accommodate the aspects of multi-threading, synchronous program exceptions |
|
1970 |
and asynchronous interrupts. |
|
57347 | 1971 |
|
61854 | 1972 |
The first thread that invokes \<open>force\<close> on an unfinished lazy value changes |
1973 |
its state into a \<^emph>\<open>promise\<close> of the eventual result and starts evaluating it. |
|
1974 |
Any other threads that \<open>force\<close> the same lazy value in the meantime need to |
|
1975 |
wait for it to finish, by producing a regular result or program exception. |
|
1976 |
If the evaluation attempt is interrupted, this event is propagated to all |
|
1977 |
waiting threads and the lazy value is reset to its original state. |
|
57347 | 1978 |
|
1979 |
This means a lazy value is completely evaluated at most once, in a |
|
1980 |
thread-safe manner. There might be multiple interrupted evaluation attempts, |
|
1981 |
and multiple receivers of intermediate interrupt events. Interrupts are |
|
61477 | 1982 |
\<^emph>\<open>not\<close> made persistent: later evaluation attempts start again from the |
57347 | 1983 |
original expression. |
58618 | 1984 |
\<close> |
1985 |
||
1986 |
text %mlref \<open> |
|
57347 | 1987 |
\begin{mldecls} |
1988 |
@{index_ML_type "'a lazy"} \\ |
|
1989 |
@{index_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\ |
|
1990 |
@{index_ML Lazy.value: "'a -> 'a lazy"} \\ |
|
1991 |
@{index_ML Lazy.force: "'a lazy -> 'a"} \\ |
|
1992 |
\end{mldecls} |
|
1993 |
||
69597 | 1994 |
\<^descr> Type \<^ML_type>\<open>'a lazy\<close> represents lazy values over type \<^verbatim>\<open>'a\<close>. |
1995 |
||
1996 |
\<^descr> \<^ML>\<open>Lazy.lazy\<close>~\<open>(fn () => e)\<close> wraps the unevaluated expression \<open>e\<close> as |
|
61854 | 1997 |
unfinished lazy value. |
61493 | 1998 |
|
69597 | 1999 |
\<^descr> \<^ML>\<open>Lazy.value\<close>~\<open>a\<close> wraps the value \<open>a\<close> as finished lazy value. When |
61854 | 2000 |
forced, it returns \<open>a\<close> without any further evaluation. |
57347 | 2001 |
|
57349 | 2002 |
There is very low overhead for this proforma wrapping of strict values as |
2003 |
lazy values. |
|
57347 | 2004 |
|
69597 | 2005 |
\<^descr> \<^ML>\<open>Lazy.force\<close>~\<open>x\<close> produces the result of the lazy value in a |
57347 | 2006 |
thread-safe manner as explained above. Thus it may cause the current thread |
2007 |
to wait on a pending evaluation attempt by another thread. |
|
58618 | 2008 |
\<close> |
2009 |
||
2010 |
||
2011 |
subsection \<open>Futures \label{sec:futures}\<close> |
|
2012 |
||
2013 |
text \<open> |
|
57349 | 2014 |
Futures help to organize parallel execution in a value-oriented manner, with |
61854 | 2015 |
\<open>fork\<close>~/ \<open>join\<close> as the main pair of operations, and some further variants; |
2016 |
see also @{cite "Wenzel:2009" and "Wenzel:2013:ITP"}. Unlike lazy values, |
|
2017 |
futures are evaluated strictly and spontaneously on separate worker threads. |
|
2018 |
Futures may be canceled, which leads to interrupts on running evaluation |
|
2019 |
attempts, and forces structurally related futures to fail for all time; |
|
2020 |
already finished futures remain unchanged. Exceptions between related |
|
57350 | 2021 |
futures are propagated as well, and turned into parallel exceptions (see |
2022 |
above). |
|
57349 | 2023 |
|
2024 |
Technically, a future is a single-assignment variable together with a |
|
61854 | 2025 |
\<^emph>\<open>task\<close> that serves administrative purposes, notably within the \<^emph>\<open>task |
2026 |
queue\<close> where new futures are registered for eventual evaluation and the |
|
2027 |
worker threads retrieve their work. |
|
57349 | 2028 |
|
57350 | 2029 |
The pool of worker threads is limited, in correlation with the number of |
2030 |
physical cores on the machine. Note that allocation of runtime resources may |
|
2031 |
be distorted either if workers yield CPU time (e.g.\ via system sleep or |
|
2032 |
wait operations), or if non-worker threads contend for significant runtime |
|
2033 |
resources independently. There is a limited number of replacement worker |
|
2034 |
threads that get activated in certain explicit wait conditions, after a |
|
2035 |
timeout. |
|
2036 |
||
61416 | 2037 |
\<^medskip> |
61854 | 2038 |
Each future task belongs to some \<^emph>\<open>task group\<close>, which represents the |
2039 |
hierarchic structure of related tasks, together with the exception status a |
|
2040 |
that point. By default, the task group of a newly created future is a new |
|
2041 |
sub-group of the presently running one, but it is also possible to indicate |
|
2042 |
different group layouts under program control. |
|
57349 | 2043 |
|
2044 |
Cancellation of futures actually refers to the corresponding task group and |
|
2045 |
all its sub-groups. Thus interrupts are propagated down the group hierarchy. |
|
2046 |
Regular program exceptions are treated likewise: failure of the evaluation |
|
2047 |
of some future task affects its own group and all sub-groups. Given a |
|
61854 | 2048 |
particular task group, its \<^emph>\<open>group status\<close> cumulates all relevant exceptions |
2049 |
according to its position within the group hierarchy. Interrupted tasks that |
|
2050 |
lack regular result information, will pick up parallel exceptions from the |
|
2051 |
cumulative group status. |
|
57349 | 2052 |
|
61416 | 2053 |
\<^medskip> |
61854 | 2054 |
A \<^emph>\<open>passive future\<close> or \<^emph>\<open>promise\<close> is a future with slightly different |
2055 |
evaluation policies: there is only a single-assignment variable and some |
|
2056 |
expression to evaluate for the \<^emph>\<open>failed\<close> case (e.g.\ to clean up resources |
|
2057 |
when canceled). A regular result is produced by external means, using a |
|
2058 |
separate \<^emph>\<open>fulfill\<close> operation. |
|
57349 | 2059 |
|
2060 |
Promises are managed in the same task queue, so regular futures may depend |
|
2061 |
on them. This allows a form of reactive programming, where some promises are |
|
2062 |
used as minimal elements (or guards) within the future dependency graph: |
|
2063 |
when these promises are fulfilled the evaluation of subsequent futures |
|
2064 |
starts spontaneously, according to their own inter-dependencies. |
|
58618 | 2065 |
\<close> |
2066 |
||
2067 |
text %mlref \<open> |
|
57348 | 2068 |
\begin{mldecls} |
2069 |
@{index_ML_type "'a future"} \\ |
|
2070 |
@{index_ML Future.fork: "(unit -> 'a) -> 'a future"} \\ |
|
2071 |
@{index_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\ |
|
57349 | 2072 |
@{index_ML Future.join: "'a future -> 'a"} \\ |
2073 |
@{index_ML Future.joins: "'a future list -> 'a list"} \\ |
|
57348 | 2074 |
@{index_ML Future.value: "'a -> 'a future"} \\ |
2075 |
@{index_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\ |
|
2076 |
@{index_ML Future.cancel: "'a future -> unit"} \\ |
|
2077 |
@{index_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex] |
|
2078 |
@{index_ML Future.promise: "(unit -> unit) -> 'a future"} \\ |
|
2079 |
@{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\ |
|
2080 |
\end{mldecls} |
|
2081 |
||
69597 | 2082 |
\<^descr> Type \<^ML_type>\<open>'a future\<close> represents future values over type \<^verbatim>\<open>'a\<close>. |
2083 |
||
2084 |
\<^descr> \<^ML>\<open>Future.fork\<close>~\<open>(fn () => e)\<close> registers the unevaluated expression \<open>e\<close> |
|
61854 | 2085 |
as unfinished future value, to be evaluated eventually on the parallel |
69597 | 2086 |
worker-thread farm. This is a shorthand for \<^ML>\<open>Future.forks\<close> below, with |
61854 | 2087 |
default parameters and a single expression. |
57348 | 2088 |
|
69597 | 2089 |
\<^descr> \<^ML>\<open>Future.forks\<close>~\<open>params exprs\<close> is the general interface to fork several |
61854 | 2090 |
futures simultaneously. The \<open>params\<close> consist of the following fields: |
57348 | 2091 |
|
69597 | 2092 |
\<^item> \<open>name : string\<close> (default \<^ML>\<open>""\<close>) specifies a common name for the |
61854 | 2093 |
tasks of the forked futures, which serves diagnostic purposes. |
61458 | 2094 |
|
69597 | 2095 |
\<^item> \<open>group : Future.group option\<close> (default \<^ML>\<open>NONE\<close>) specifies an optional |
2096 |
task group for the forked futures. \<^ML>\<open>NONE\<close> means that a new sub-group |
|
61854 | 2097 |
of the current worker-thread task context is created. If this is not a |
2098 |
worker thread, the group will be a new root in the group hierarchy. |
|
61458 | 2099 |
|
69597 | 2100 |
\<^item> \<open>deps : Future.task list\<close> (default \<^ML>\<open>[]\<close>) specifies dependencies on |
61854 | 2101 |
other future tasks, i.e.\ the adjacency relation in the global task queue. |
2102 |
Dependencies on already finished tasks are ignored. |
|
61458 | 2103 |
|
69597 | 2104 |
\<^item> \<open>pri : int\<close> (default \<^ML>\<open>0\<close>) specifies a priority within the task |
61854 | 2105 |
queue. |
61458 | 2106 |
|
69597 | 2107 |
Typically there is only little deviation from the default priority \<^ML>\<open>0\<close>. As a rule of thumb, \<^ML>\<open>~1\<close> means ``low priority" and \<^ML>\<open>1\<close> means |
61458 | 2108 |
``high priority''. |
2109 |
||
61854 | 2110 |
Note that the task priority only affects the position in the queue, not |
2111 |
the thread priority. When a worker thread picks up a task for processing, |
|
2112 |
it runs with the normal thread priority to the end (or until canceled). |
|
2113 |
Higher priority tasks that are queued later need to wait until this (or |
|
2114 |
another) worker thread becomes free again. |
|
61458 | 2115 |
|
69597 | 2116 |
\<^item> \<open>interrupts : bool\<close> (default \<^ML>\<open>true\<close>) tells whether the worker thread |
61854 | 2117 |
that processes the corresponding task is initially put into interruptible |
2118 |
state. This state may change again while running, by modifying the thread |
|
2119 |
attributes. |
|
61458 | 2120 |
|
61854 | 2121 |
With interrupts disabled, a running future task cannot be canceled. It is |
61458 | 2122 |
the responsibility of the programmer that this special state is retained |
2123 |
only briefly. |
|
57348 | 2124 |
|
69597 | 2125 |
\<^descr> \<^ML>\<open>Future.join\<close>~\<open>x\<close> retrieves the value of an already finished future, |
61854 | 2126 |
which may lead to an exception, according to the result of its previous |
2127 |
evaluation. |
|
57348 | 2128 |
|
2129 |
For an unfinished future there are several cases depending on the role of |
|
2130 |
the current thread and the status of the future. A non-worker thread waits |
|
2131 |
passively until the future is eventually evaluated. A worker thread |
|
2132 |
temporarily changes its task context and takes over the responsibility to |
|
57349 | 2133 |
evaluate the future expression on the spot. The latter is done in a |
2134 |
thread-safe manner: other threads that intend to join the same future need |
|
2135 |
to wait until the ongoing evaluation is finished. |
|
2136 |
||
2137 |
Note that excessive use of dynamic dependencies of futures by adhoc joining |
|
2138 |
may lead to bad utilization of CPU cores, due to threads waiting on other |
|
2139 |
threads to finish required futures. The future task farm has a limited |
|
2140 |
amount of replacement threads that continue working on unrelated tasks after |
|
2141 |
some timeout. |
|
57348 | 2142 |
|
2143 |
Whenever possible, static dependencies of futures should be specified |
|
61854 | 2144 |
explicitly when forked (see \<open>deps\<close> above). Thus the evaluation can work from |
2145 |
the bottom up, without join conflicts and wait states. |
|
57349 | 2146 |
|
69597 | 2147 |
\<^descr> \<^ML>\<open>Future.joins\<close>~\<open>xs\<close> joins the given list of futures simultaneously, |
2148 |
which is more efficient than \<^ML>\<open>map Future.join\<close>~\<open>xs\<close>. |
|
57349 | 2149 |
|
2150 |
Based on the dependency graph of tasks, the current thread takes over the |
|
2151 |
responsibility to evaluate future expressions that are required for the main |
|
2152 |
result, working from the bottom up. Waiting on future results that are |
|
2153 |
presently evaluated on other threads only happens as last resort, when no |
|
2154 |
other unfinished futures are left over. |
|
2155 |
||
69597 | 2156 |
\<^descr> \<^ML>\<open>Future.value\<close>~\<open>a\<close> wraps the value \<open>a\<close> as finished future value, |
61854 | 2157 |
bypassing the worker-thread farm. When joined, it returns \<open>a\<close> without any |
2158 |
further evaluation. |
|
57349 | 2159 |
|
2160 |
There is very low overhead for this proforma wrapping of strict values as |
|
57421 | 2161 |
futures. |
57348 | 2162 |
|
69597 | 2163 |
\<^descr> \<^ML>\<open>Future.map\<close>~\<open>f x\<close> is a fast-path implementation of \<^ML>\<open>Future.fork\<close>~\<open>(fn () => f (\<close>\<^ML>\<open>Future.join\<close>~\<open>x))\<close>, which avoids the full |
61854 | 2164 |
overhead of the task queue and worker-thread farm as far as possible. The |
2165 |
function \<open>f\<close> is supposed to be some trivial post-processing or projection of |
|
2166 |
the future result. |
|
57348 | 2167 |
|
69597 | 2168 |
\<^descr> \<^ML>\<open>Future.cancel\<close>~\<open>x\<close> cancels the task group of the given future, using |
2169 |
\<^ML>\<open>Future.cancel_group\<close> below. |
|
2170 |
||
2171 |
\<^descr> \<^ML>\<open>Future.cancel_group\<close>~\<open>group\<close> cancels all tasks of the given task |
|
61854 | 2172 |
group for all time. Threads that are presently processing a task of the |
2173 |
given group are interrupted: it may take some time until they are actually |
|
2174 |
terminated. Tasks that are queued but not yet processed are dequeued and |
|
2175 |
forced into interrupted state. Since the task group is itself invalidated, |
|
2176 |
any further attempt to fork a future that belongs to it will yield a |
|
2177 |
canceled result as well. |
|
57348 | 2178 |
|
69597 | 2179 |
\<^descr> \<^ML>\<open>Future.promise\<close>~\<open>abort\<close> registers a passive future with the given |
61854 | 2180 |
\<open>abort\<close> operation: it is invoked when the future task group is canceled. |
57348 | 2181 |
|
69597 | 2182 |
\<^descr> \<^ML>\<open>Future.fulfill\<close>~\<open>x a\<close> finishes the passive future \<open>x\<close> by the given |
61854 | 2183 |
value \<open>a\<close>. If the promise has already been canceled, the attempt to fulfill |
2184 |
it causes an exception. |
|
58618 | 2185 |
\<close> |
57348 | 2186 |
|
47180 | 2187 |
end |