%
\begin{isabellebody}%
\def\isabellecontext{ML}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Isabelle/ML%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle/ML is best understood as a certain culture based on
Standard ML. Thus it is not a new programming language, but a
certain way to use SML at an advanced level within the Isabelle
environment. This covers a variety of aspects that are geared
towards an efficient and robust platform for applications of formal
logic with fully foundational proof construction --- according to
the well-known \emph{LCF principle}. There is specific
infrastructure with library modules to address the needs of this
difficult task. For example, the raw parallel programming model of
Poly/ML is presented as considerably more abstract concept of
\emph{future values}, which is then used to augment the inference
kernel, proof interpreter, and theory loader accordingly.
The main aspects of Isabelle/ML are introduced below. These
first-hand explanations should help to understand how proper
Isabelle/ML is to be read and written, and to get access to the
wealth of experience that is expressed in the source text and its
history of changes.\footnote{See
\url{http://isabelle.in.tum.de/repos/isabelle} for the full
Mercurial history. There are symbolic tags to refer to official
Isabelle releases, as opposed to arbitrary \emph{tip} versions that
merely reflect snapshots that are never really up-to-date.}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Style and orthography%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The sources of Isabelle/Isar are optimized for
\emph{readability} and \emph{maintainability}. The main purpose is
to tell an informed reader what is really going on and how things
really work. This is a non-trivial aim, but it is supported by a
certain style of writing Isabelle/ML that has emerged from long
years of system development.\footnote{See also the interesting style
guide for OCaml
\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}
which shares many of our means and ends.}
The main principle behind any coding style is \emph{consistency}.
For a single author of a small program this merely means ``choose
your style and stick to it''. A complex project like Isabelle, with
long years of development and different contributors, requires more
standardization. A coding style that is changed every few years or
with every new contributor is no style at all, because consistency
is quickly lost. Global consistency is hard to achieve, though.
Nonetheless, one should always strive at least for local consistency
of modules and sub-systems, without deviating from some general
principles how to write Isabelle/ML.
In a sense, good coding style is like an \emph{orthography} for the
sources: it helps to read quickly over the text and see through the
main points, without getting distracted by accidental presentation
of free-style code.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Header and sectioning%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle source files have a certain standardized header
format (with precise spacing) that follows ancient traditions
reaching back to the earliest versions of the system by Larry
Paulson. See \hyperlink{file.~~/src/Pure/thm.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}thm{\isaliteral{2E}{\isachardot}}ML}}}}, for example.
The header includes at least \verb|Title| and \verb|Author| entries, followed by a prose description of the purpose of
the module. The latter can range from a single line to several
paragraphs of explanations.
The rest of the file is divided into sections, subsections,
subsubsections, paragraphs etc.\ using a simple layout via ML
comments as follows.
\begin{verbatim}
(*** section ***)
(** subsection **)
(* subsubsection *)
(*short paragraph*)
(*
long paragraph,
with more text
*)
\end{verbatim}
As in regular typography, there is some extra space \emph{before}
section headings that are adjacent to plain text (not other headings
as in the example above).
\medskip The precise wording of the prose text given in these
headings is chosen carefully to introduce the main theme of the
subsequent formal ML text.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Naming conventions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Since ML is the primary medium to express the meaning of the
source text, naming of ML entities requires special care.
\paragraph{Notation.} A name consists of 1--3 \emph{words} (rarely
4, but not more) that are separated by underscore. There are three
variants concerning upper or lower case letters, which are used for
certain ML categories as follows:
\medskip
\begin{tabular}{lll}
variant & example & ML categories \\\hline
lower-case & \verb|foo_bar| & values, types, record fields \\
capitalized & \verb|Foo_Bar| & datatype constructors, structures, functors \\
upper-case & \verb|FOO_BAR| & special values, exception constructors, signatures \\
\end{tabular}
\medskip
For historical reasons, many capitalized names omit underscores,
e.g.\ old-style \verb|FooBar| instead of \verb|Foo_Bar|.
Genuine mixed-case names are \emph{not} used, bacause clear division
of words is essential for readability.\footnote{Camel-case was
invented to workaround the lack of underscore in some early
non-ASCII character sets. Later it became habitual in some language
communities that are now strong in numbers.}
A single (capital) character does not count as ``word'' in this
respect: some Isabelle/ML names are suffixed by extra markers like
this: \verb|foo_barT|.
Name variants are produced by adding 1--3 primes, e.g.\ \verb|foo'|, \verb|foo''|, or \verb|foo'''|, but not \verb|foo''''| or more. Decimal digits scale better to larger numbers,
e.g.\ \verb|foo0|, \verb|foo1|, \verb|foo42|.
\paragraph{Scopes.} Apart from very basic library modules, ML
structures are not ``opened'', but names are referenced with
explicit qualification, as in \verb|Syntax.string_of_term| for
example. When devising names for structures and their components it
is important aim at eye-catching compositions of both parts, because
this is how they are seen in the sources and documentation. For the
same reasons, aliases of well-known library functions should be
avoided.
Local names of function abstraction or case/let bindings are
typically shorter, sometimes using only rudiments of ``words'',
while still avoiding cryptic shorthands. An auxiliary function
called \verb|helper|, \verb|aux|, or \verb|f| is
considered bad style.
Example:
\begin{verbatim}
(* RIGHT *)
fun print_foo ctxt foo =
let
fun print t = ... Syntax.string_of_term ctxt t ...
in ... end;
(* RIGHT *)
fun print_foo ctxt foo =
let
val string_of_term = Syntax.string_of_term ctxt;
fun print t = ... string_of_term t ...
in ... end;
(* WRONG *)
val string_of_term = Syntax.string_of_term;
fun print_foo ctxt foo =
let
fun aux t = ... string_of_term ctxt t ...
in ... end;
\end{verbatim}
\paragraph{Specific conventions.} Here are some specific name forms
that occur frequently in the sources.
\begin{itemize}
\item A function that maps \verb|foo| to \verb|bar| is
called \verb|foo_to_bar| or \verb|bar_of_foo| (never
\verb|foo2bar|, \verb|bar_from_foo|, \verb|bar_for_foo|, or \verb|bar4foo|).
\item The name component \verb|legacy| means that the operation
is about to be discontinued soon.
\item The name component \verb|old| means that this is historic
material that might disappear at some later stage.
\item The name component \verb|global| means that this works
with the background theory instead of the regular local context
(\secref{sec:context}), sometimes for historical reasons, sometimes
due a genuine lack of locality of the concept involved, sometimes as
a fall-back for the lack of a proper context in the application
code. Whenever there is a non-global variant available, the
application should be migrated to use it with a proper local
context.
\item Variables of the main context types of the Isabelle/Isar
framework (\secref{sec:context} and \chref{ch:local-theory}) have
firm naming conventions as follows:
\begin{itemize}
\item theories are called \verb|thy|, rarely \verb|theory|
(never \verb|thry|)
\item proof contexts are called \verb|ctxt|, rarely \verb|context| (never \verb|ctx|)
\item generic contexts are called \verb|context|, rarely
\verb|ctxt|
\item local theories are called \verb|lthy|, except for local
theories that are treated as proof context (which is a semantic
super-type)
\end{itemize}
Variations with primed or decimal numbers are always possible, as
well as sematic prefixes like \verb|foo_thy| or \verb|bar_ctxt|, but the base conventions above need to be preserved.
This allows to visualize the their data flow via plain regular
expressions in the editor.
\item The main logical entities (\secref{ch:logic}) have established
naming convention as follows:
\begin{itemize}
\item sorts are called \verb|S|
\item types are called \verb|T|, \verb|U|, or \verb|ty| (never \verb|t|)
\item terms are called \verb|t|, \verb|u|, or \verb|tm| (never \verb|trm|)
\item certified types are called \verb|cT|, rarely \verb|T|, with variants as for types
\item certified terms are called \verb|ct|, rarely \verb|t|, with variants as for terms
\item theorems are called \verb|th|, or \verb|thm|
\end{itemize}
Proper semantic names override these conventions completely. For
example, the left-hand side of an equation (as a term) can be called
\verb|lhs| (not \verb|lhs_tm|). Or a term that is known
to be a variable can be called \verb|v| or \verb|x|.
\item Tactics (\secref{sec:tactics}) are sufficiently important to
have specific naming conventions. The name of a basic tactic
definition always has a \verb|_tac| suffix, the subgoal index
(if applicable) is always called \verb|i|, and the goal state
(if made explicit) is usually called \verb|st| instead of the
somewhat misleading \verb|thm|. Any other arguments are given
before the latter two, and the general context is given first.
Example:
\begin{verbatim}
fun my_tac ctxt arg1 arg2 i st = ...
\end{verbatim}
Note that the goal state \verb|st| above is rarely made
explicit, if tactic combinators (tacticals) are used as usual.
\end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{General source layout%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The general Isabelle/ML source layout imitates regular
type-setting to some extent, augmented by the requirements for
deeply nested expressions that are commonplace in functional
programming.
\paragraph{Line length} is 80 characters according to ancient
standards, but we allow as much as 100 characters (not
more).\footnote{Readability requires to keep the beginning of a line
in view while watching its end. Modern wide-screen displays do not
change the way how the human brain works. Sources also need to be
printable on plain paper with reasonable font-size.} The extra 20
characters acknowledge the space requirements due to qualified
library references in Isabelle/ML.
\paragraph{White-space} is used to emphasize the structure of
expressions, following mostly standard conventions for mathematical
typesetting, as can be seen in plain {\TeX} or {\LaTeX}. This
defines positioning of spaces for parentheses, punctuation, and
infixes as illustrated here:
\begin{verbatim}
val x = y + z * (a + b);
val pair = (a, b);
val record = {foo = 1, bar = 2};
\end{verbatim}
Lines are normally broken \emph{after} an infix operator or
punctuation character. For example:
\begin{verbatim}
val x =
a +
b +
c;
val tuple =
(a,
b,
c);
\end{verbatim}
Some special infixes (e.g.\ \verb||\verb,|,\verb|>|) work better at the
start of the line, but punctuation is always at the end.
Function application follows the tradition of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus,
not informal mathematics. For example: \verb|f a b| for a
curried function, or \verb|g (a, b)| for a tupled function.
Note that the space between \verb|g| and the pair \verb|(a, b)| follows the important principle of
\emph{compositionality}: the layout of \verb|g p| does not
change when \verb|p| is refined to the concrete pair
\verb|(a, b)|.
\paragraph{Indentation} uses plain spaces, never hard
tabulators.\footnote{Tabulators were invented to move the carriage
of a type-writer to certain predefined positions. In software they
could be used as a primitive run-length compression of consecutive
spaces, but the precise result would depend on non-standardized
editor configuration.}
Each level of nesting is indented by 2 spaces, sometimes 1, very
rarely 4, never 8 or any other odd number.
Indentation follows a simple logical format that only depends on the
nesting depth, not the accidental length of the text that initiates
a level of nesting. Example:
\begin{verbatim}
(* RIGHT *)
if b then
expr1_part1
expr1_part2
else
expr2_part1
expr2_part2
(* WRONG *)
if b then expr1_part1
expr1_part2
else expr2_part1
expr2_part2
\end{verbatim}
The second form has many problems: it assumes a fixed-width font
when viewing the sources, it uses more space on the line and thus
makes it hard to observe its strict length limit (working against
\emph{readability}), it requires extra editing to adapt the layout
to changes of the initial text (working against
\emph{maintainability}) etc.
\medskip For similar reasons, any kind of two-dimensional or tabular
layouts, ASCII-art with lines or boxes of asterisks etc.\ should be
avoided.
\paragraph{Complex expressions} that consist of multi-clausal
function definitions, \verb|handle|, \verb|case|,
\verb|let| (and combinations) require special attention. The
syntax of Standard ML is quite ambitious and admits a lot of
variance that can distort the meaning of the text.
Clauses of \verb|fun|, \verb|fn|, \verb|handle|,
\verb|case| get extra indentation to indicate the nesting
clearly. Example:
\begin{verbatim}
(* RIGHT *)
fun foo p1 =
expr1
| foo p2 =
expr2
(* WRONG *)
fun foo p1 =
expr1
| foo p2 =
expr2
\end{verbatim}
Body expressions consisting of \verb|case| or \verb|let|
require care to maintain compositionality, to prevent loss of
logical indentation where it is especially important to see the
structure of the text. Example:
\begin{verbatim}
(* RIGHT *)
fun foo p1 =
(case e of
q1 => ...
| q2 => ...)
| foo p2 =
let
...
in
...
end
(* WRONG *)
fun foo p1 = case e of
q1 => ...
| q2 => ...
| foo p2 =
let
...
in
...
end
\end{verbatim}
Extra parentheses around \verb|case| expressions are optional,
but help to analyse the nesting based on character matching in the
editor.
\medskip There are two main exceptions to the overall principle of
compositionality in the layout of complex expressions.
\begin{enumerate}
\item \verb|if| expressions are iterated as if there would be
a multi-branch conditional in SML, e.g.
\begin{verbatim}
(* RIGHT *)
if b1 then e1
else if b2 then e2
else e3
\end{verbatim}
\item \verb|fn| abstractions are often layed-out as if they
would lack any structure by themselves. This traditional form is
motivated by the possibility to shift function arguments back and
forth wrt.\ additional combinators. Example:
\begin{verbatim}
(* RIGHT *)
fun foo x y = fold (fn z =>
expr)
\end{verbatim}
Here the visual appearance is that of three arguments \verb|x|,
\verb|y|, \verb|z|.
\end{enumerate}
Such weakly structured layout should be use with great care. Here
are some counter-examples involving \verb|let| expressions:
\begin{verbatim}
(* WRONG *)
fun foo x = let
val y = ...
in ... end
fun foo x = let
val y = ...
in ... end
fun foo x =
let
val y = ...
in ... end
\end{verbatim}
\medskip In general the source layout is meant to emphasize the
structure of complex language expressions, not to pretend that SML
had a completely different syntax (say that of Haskell or Java).%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{SML embedded into Isabelle/Isar%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
ML and Isar are intertwined via an open-ended bootstrap
process that provides more and more programming facilities and
logical content in an alternating manner. Bootstrapping starts from
the raw environment of existing implementations of Standard ML
(mainly Poly/ML, but also SML/NJ).
Isabelle/Pure marks the point where the original ML toplevel is
superseded by the Isar toplevel that maintains a uniform context for
arbitrary ML values (see also \secref{sec:context}). This formal
environment holds ML compiler bindings, logical entities, and many
other things. Raw SML is never encountered again after the initial
bootstrap of Isabelle/Pure.
Object-logics like Isabelle/HOL are built within the
Isabelle/ML/Isar environment by introducing suitable theories with
associated ML modules, either inlined or as separate files. Thus
Isabelle/HOL is defined as a regular user-space application within
the Isabelle framework. Further add-on tools can be implemented in
ML within the Isar context in the same manner: ML is part of the
standard repertoire of Isabelle, and there is no distinction between
``user'' and ``developer'' in this respect.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Isar ML commands%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The primary Isar source language provides facilities to ``open
a window'' to the underlying ML compiler. Especially see the Isar
commands \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} and \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}: both work the
same way, only the source text is provided via a file vs.\ inlined,
respectively. Apart from embedding ML into the main theory
definition like that, there are many more commands that refer to ML
source, such as \indexref{}{command}{setup}\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} or \indexref{}{command}{declaration}\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}.
Even more fine-grained embedding of ML into Isar is encountered in
the proof method \indexref{}{method}{tactic}\hyperlink{method.tactic}{\mbox{\isa{tactic}}}, which refines the pending
goal state via a given expression of type \verb|tactic|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
The following artificial example demonstrates some ML
toplevel declarations within the implicit Isar theory context. This
is regular functional programming without referring to logical
entities yet.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ fun\ factorial\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\isanewline
\ \ \ \ {\isaliteral{7C}{\isacharbar}}\ factorial\ n\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ factorial\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
Here the ML environment is already managed by Isabelle, i.e.\
the \verb|factorial| function is not yet accessible in the preceding
paragraph, nor in a different theory that is independent from the
current one in the import hierarchy.
Removing the above ML declaration from the source text will remove
any trace of this definition as expected. The Isabelle/ML toplevel
environment is managed in a \emph{stateless} way: unlike the raw ML
toplevel there are no global side-effects involved
here.\footnote{Such a stateless compilation environment is also a
prerequisite for robust parallel compilation within independent
nodes of the implicit theory development graph.}
\medskip The next example shows how to embed ML into Isar proofs, using
\indexref{}{command}{ML\_prf}\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} instead of Instead of \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}.
As illustrated below, the effect on the ML environment is local to
the whole proof body, ignoring the block structure.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
\isanewline
%
\isadelimML
\ \ %
\endisadelimML
%
\isatagML
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ a\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ b\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
\ %
\isamarkupcmt{Isar block structure ignored by ML environment%
}
\isanewline
\ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ c\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
By side-stepping the normal scoping rules for Isar proof
blocks, embedded ML code can refer to the different contexts and
manipulate corresponding entities, e.g.\ export a fact from a block
context.
\medskip Two further ML commands are useful in certain situations:
\indexref{}{command}{ML\_val}\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} and \indexref{}{command}{ML\_command}\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}} are
\emph{diagnostic} in the sense that there is no effect on the
underlying environment, and can thus used anywhere (even outside a
theory). The examples below produce long strings of digits by
invoking \verb|factorial|: \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} already takes care of
printing the ML toplevel result, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}} is silent
so we produce an explicit output message.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ writeln\ {\isaliteral{28}{\isacharparenleft}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{28}{\isacharparenleft}}factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
\isanewline
\isanewline
\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
\isanewline
%
\isadelimML
\ \ %
\endisadelimML
%
\isatagML
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ \isanewline
\ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ writeln\ {\isaliteral{28}{\isacharparenleft}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{28}{\isacharparenleft}}factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Compile-time context%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Whenever the ML compiler is invoked within Isabelle/Isar, the
formal context is passed as a thread-local reference variable. Thus
ML code may access the theory context during compilation, by reading
or writing the (local) theory under construction. Note that such
direct access to the compile-time context is rare. In practice it
is typically done via some derived ML functions instead.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{ML\_Context.the\_generic\_context}\verb|ML_Context.the_generic_context: unit -> Context.generic| \\
\indexdef{}{ML}{Context.$>$$>$}\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
\indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
\indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
\end{mldecls}
\begin{description}
\item \verb|ML_Context.the_generic_context ()| refers to the theory
context of the ML toplevel --- at compile time. ML code needs to
take care to refer to \verb|ML_Context.the_generic_context ()|
correctly. Recall that evaluation of a function body is delayed
until actual run-time.
\item \verb|Context.>>|~\isa{f} applies context transformation
\isa{f} to the implicit context of the ML toplevel.
\item \verb|bind_thms|~\isa{{\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ thms{\isaliteral{29}{\isacharparenright}}} stores a list of
theorems produced in ML both in the (global) theory context and the
ML toplevel, associating it with the provided name. Theorems are
put into a global ``standard'' format before being stored.
\item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
singleton fact.
\end{description}
It is important to note that the above functions are really
restricted to the compile time, even though the ML compiler is
invoked at run-time. The majority of ML code either uses static
antiquotations (\secref{sec:ML-antiq}) or refers to the theory or
proof context at run-time, by explicit functional abstraction.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Antiquotations \label{sec:ML-antiq}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A very important consequence of embedding SML into Isar is the
concept of \emph{ML antiquotation}. The standard token language of
ML is augmented by special syntactic entities of the following form:
\indexouternonterm{antiquote}
\begin{rail}
antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym
;
\end{rail}
Here \hyperlink{syntax.nameref}{\mbox{\isa{nameref}}} and \hyperlink{syntax.args}{\mbox{\isa{args}}} are regular outer syntax
categories \cite{isabelle-isar-ref}. Attributes and proof methods
use similar syntax.
\medskip A regular antiquotation \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}name\ args{\isaliteral{7D}{\isacharbraceright}}} processes
its arguments by the usual means of the Isar source language, and
produces corresponding ML source text, either as literal
\emph{inline} text (e.g. \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term\ t{\isaliteral{7D}{\isacharbraceright}}}) or abstract
\emph{value} (e.g. \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thm\ th{\isaliteral{7D}{\isacharbraceright}}}). This pre-compilation
scheme allows to refer to formal entities in a robust manner, with
proper static scoping and with some degree of logical checking of
small portions of the code.
Special antiquotations like \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}let\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{7D}{\isacharbraceright}}} or \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}note\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{7D}{\isacharbraceright}}} augment the compilation context without generating code. The
non-ASCII braces \isa{{\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}} and \isa{{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}} allow to delimit the
effect by introducing local blocks within the pre-compilation
environment.
\medskip See also \cite{Wenzel-Chaieb:2007b} for a broader
perspective on Isabelle/ML antiquotations.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isatagmlantiq
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{ML antiquotation}{let}\hypertarget{ML antiquotation.let}{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
\indexdef{}{ML antiquotation}{note}\hypertarget{ML antiquotation.note}{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
\end{matharray}
\begin{rail}
'let' ((term + 'and') '=' term + 'and')
;
'note' (thmdef? thmrefs + 'and')
;
\end{rail}
\begin{description}
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}let\ p\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{7D}{\isacharbraceright}}} binds schematic variables in the
pattern \isa{p} by higher-order matching against the term \isa{t}. This is analogous to the regular \indexref{}{command}{let}\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} command
in the Isar proof language. The pre-compilation environment is
augmented by auxiliary term bindings, without emitting ML source.
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}note\ a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{7D}{\isacharbraceright}}} recalls existing facts \isa{b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n}, binding the result as \isa{a}. This is analogous to
the regular \indexref{}{command}{note}\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}} command in the Isar proof language.
The pre-compilation environment is augmented by auxiliary fact
bindings, without emitting ML source.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlantiq
{\isafoldmlantiq}%
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
The following artificial example gives some impression
about the antiquotation elements introduced so far, together with
the important \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thm{\isaliteral{7D}{\isacharbraceright}}} antiquotation defined later.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ {\isaliteral{5C3C6C62726163653E}{\isaantiqopen}}\isanewline
\ \ \ \ %
\isaantiq
let\ {\isaliteral{3F}{\isacharquery}}t\ {\isaliteral{3D}{\isacharequal}}\ my{\isaliteral{5F}{\isacharunderscore}}term{}%
\endisaantiq
\isanewline
\ \ \ \ %
\isaantiq
note\ my{\isaliteral{5F}{\isacharunderscore}}refl\ {\isaliteral{3D}{\isacharequal}}\ reflexive\ {\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{3F}{\isacharquery}}t{\isaliteral{5D}{\isacharbrackright}}{}%
\endisaantiq
\isanewline
\ \ \ \ fun\ foo\ th\ {\isaliteral{3D}{\isacharequal}}\ Thm{\isaliteral{2E}{\isachardot}}transitive\ th\ %
\isaantiq
thm\ my{\isaliteral{5F}{\isacharunderscore}}refl{}%
\endisaantiq
\isanewline
\ \ {\isaliteral{5C3C7262726163653E}{\isaantiqclose}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
The extra block delimiters do not affect the compiled code
itself, i.e.\ function \verb|foo| is available in the present context
of this paragraph.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Canonical argument order \label{sec:canonical-argument-order}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Standard ML is a language in the tradition of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus and \emph{higher-order functional programming},
similar to OCaml, Haskell, or Isabelle/Pure and HOL as logical
languages. Getting acquainted with the native style of representing
functions in that setting can save a lot of extra boiler-plate of
redundant shuffling of arguments, auxiliary abstractions etc.
Functions are usually \emph{curried}: the idea of turning arguments
of type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i} (for \isa{i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ n{\isaliteral{7D}{\isacharbraceright}}}) into a result of
type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is represented by the iterated function space
\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}. This is isomorphic to the well-known
encoding via tuples \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}, but the curried
version fits more smoothly into the basic calculus.\footnote{The
difference is even more significant in higher-order logic, because
the redundant tuple structure needs to be accommodated by formal
reasoning.}
Currying gives some flexiblity due to \emph{partial application}. A
function \isa{f{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isadigit{2}}\isaliteral{5C3C5E657375623E}{}\isactrlesub \ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} can be applied to \isa{x{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}
and the remaining \isa{{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} passed to another function
etc. How well this works in practice depends on the order of
arguments. In the worst case, arguments are arranged erratically,
and using a function in a certain situation always requires some
glue code. Thus we would get exponentially many oppurtunities to
decorate the code with meaningless permutations of arguments.
This can be avoided by \emph{canonical argument order}, which
observes certain standard patterns and minimizes adhoc permutations
in their application. In Isabelle/ML, large portions of text can be
written without ever using \isa{swap{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, or the
combinator \isa{C{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C67616D6D613E}{\isasymgamma}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C67616D6D613E}{\isasymgamma}}{\isaliteral{29}{\isacharparenright}}} that is not even
defined in our library.
\medskip The basic idea is that arguments that vary less are moved
further to the left than those that vary more. Two particularly
important categories of functions are \emph{selectors} and
\emph{updates}.
The subsequent scheme is based on a hypothetical set-like container
of type \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}} that manages elements of type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. Both
the names and types of the associated operations are canonical for
Isabelle/ML.
\medskip
\begin{tabular}{ll}
kind & canonical name and type \\\hline
selector & \isa{member{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ bool} \\
update & \isa{insert{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}} \\
\end{tabular}
\medskip
Given a container \isa{B{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}}, the partially applied \isa{member\ B} is a predicate over elements \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ bool}, and
thus represents the intended denotation directly. It is customary
to pass the abstract predicate to further operations, not the
concrete container. The argument order makes it easy to use other
combinators: \isa{forall\ {\isaliteral{28}{\isacharparenleft}}member\ B{\isaliteral{29}{\isacharparenright}}\ list} will check a list of
elements for membership in \isa{B} etc. Often the explicit
\isa{list} is pointless and can be contracted to \isa{forall\ {\isaliteral{28}{\isacharparenleft}}member\ B{\isaliteral{29}{\isacharparenright}}} to get directly a predicate again.
In contrast, an update operation varies the container, so it moves
to the right: \isa{insert\ a} is a function \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}} to
insert a value \isa{a}. These can be composed naturally as
\isa{insert\ c\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ insert\ b\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ insert\ a}. The slightly awkward
inversion of the composition order is due to conventional
mathematical notation, which can be easily amended as explained
below.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Forward application and composition%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Regular function application and infix notation works best for
relatively deeply structured expressions, e.g.\ \isa{h\ {\isaliteral{28}{\isacharparenleft}}f\ x\ y\ {\isaliteral{2B}{\isacharplus}}\ g\ z{\isaliteral{29}{\isacharparenright}}}. The important special case of \emph{linear transformation}
applies a cascade of functions \isa{f\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{28}{\isacharparenleft}}f\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}. This
becomes hard to read and maintain if the functions are themselves
given as complex expressions. The notation can be significantly
improved by introducing \emph{forward} versions of application and
composition as follows:
\medskip
\begin{tabular}{lll}
\isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{f\ x} \\
\isa{f\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\ g} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ g} \\
\end{tabular}
\medskip
This enables to write conveniently \isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f\isaliteral{5C3C5E7375623E}{}\isactrlsub n} or
\isa{f\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\ f\isaliteral{5C3C5E7375623E}{}\isactrlsub n} for its functional abstraction over \isa{x}.
\medskip There is an additional set of combinators to accommodate
multiple results (via pairs) that are passed on as multiple
arguments (via currying).
\medskip
\begin{tabular}{lll}
\isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ f} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{f\ x\ y} \\
\isa{f\ {\isaliteral{23}{\isacharhash}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ g} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ g} \\
\end{tabular}
\medskip%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{$\mid$$>$}\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
\indexdef{}{ML}{$\mid$-$>$}\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
\indexdef{}{ML}{\#$>$}\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
\indexdef{}{ML}{\#-$>$}\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
\end{mldecls}
%FIXME description!?%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Canonical iteration%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
As explained above, a function \isa{f{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}} can be
understood as update on a configuration of type \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}},
parametrized by arguments of type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. Given \isa{a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}
the partial application \isa{{\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}} operates
homogeneously on \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}. This can be iterated naturally over a
list of parameters \isa{{\isaliteral{5B}{\isacharbrackleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} as \isa{f\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\ f\ a\isaliteral{5C3C5E627375623E}{}\isactrlbsub n\isaliteral{5C3C5E657375623E}{}\isactrlesub \isaliteral{5C3C5E627375623E}{}\isactrlbsub \isaliteral{5C3C5E657375623E}{}\isactrlesub }. The latter expression is again a function \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}}.
It can be applied to an initial configuration \isa{b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}} to
start the iteration over the given list of arguments: each \isa{a} in \isa{a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n} is applied consecutively by updating a
cumulative configuration.
The \isa{fold} combinator in Isabelle/ML lifts a function \isa{f} as above to its iterated version over a list of arguments.
Lifting can be repeated, e.g.\ \isa{{\isaliteral{28}{\isacharparenleft}}fold\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ fold{\isaliteral{29}{\isacharparenright}}\ f} iterates
over a list of lists as expected.
The variant \isa{fold{\isaliteral{5F}{\isacharunderscore}}rev} works inside-out over the list of
arguments, such that \isa{fold{\isaliteral{5F}{\isacharunderscore}}rev\ f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ fold\ f\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ rev} holds.
The \isa{fold{\isaliteral{5F}{\isacharunderscore}}map} combinator essentially performs \isa{fold} and \isa{map} simultaneously: each application of \isa{f} produces an updated configuration together with a side-result;
the iteration collects all such side-results as a separate list.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
\indexdef{}{ML}{fold\_rev}\verb|fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
\indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
\end{mldecls}
\begin{description}
\item \verb|fold|~\isa{f} lifts the parametrized update function
\isa{f} to a list of parameters.
\item \verb|fold_rev|~\isa{f} is similar to \verb|fold|~\isa{f}, but works inside-out.
\item \verb|fold_map|~\isa{f} lifts the parametrized update
function \isa{f} (with side-result) to a list of parameters and
cumulative side-results.
\end{description}
\begin{warn}
The literature on functional programming provides a multitude of
combinators called \isa{foldl}, \isa{foldr} etc. SML97
provides its own variations as \verb|List.foldl| and \verb|List.foldr|, while the classic Isabelle library also has the
historic \verb|Library.foldl| and \verb|Library.foldr|. To avoid
further confusion, all of this should be ignored, and \verb|fold| (or
\verb|fold_rev|) used exclusively.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
The following example shows how to fill a text buffer
incrementally by adding strings, either individually or from a given
list.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ val\ s\ {\isaliteral{3D}{\isacharequal}}\isanewline
\ \ \ \ Buffer{\isaliteral{2E}{\isachardot}}empty\isanewline
\ \ \ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Buffer{\isaliteral{2E}{\isachardot}}add\ {\isaliteral{22}{\isachardoublequote}}digits{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}\isanewline
\ \ \ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ fold\ {\isaliteral{28}{\isacharparenleft}}Buffer{\isaliteral{2E}{\isachardot}}add\ o\ string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ upto\ {\isadigit{9}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Buffer{\isaliteral{2E}{\isachardot}}content{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
\ \ %
\isaantiq
assert{}%
\endisaantiq
\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}digits{\isaliteral{3A}{\isacharcolon}}\ {\isadigit{0}}{\isadigit{1}}{\isadigit{2}}{\isadigit{3}}{\isadigit{4}}{\isadigit{5}}{\isadigit{6}}{\isadigit{7}}{\isadigit{8}}{\isadigit{9}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
Note how \verb|fold (Buffer.add o string_of_int)| above saves
an extra \verb|map| over the given list. This kind of peephole
optimization reduces both the code size and the tree structures in
memory (``deforestation''), but requires some practice to read and
write it fluently.
\medskip The next example elaborates the idea of canonical
iteration, demonstrating fast accumulation of tree content using a
text buffer.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ datatype\ tree\ {\isaliteral{3D}{\isacharequal}}\ Text\ of\ string\ {\isaliteral{7C}{\isacharbar}}\ Elem\ of\ string\ {\isaliteral{2A}{\isacharasterisk}}\ tree\ list{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
\ \ fun\ slow{\isaliteral{5F}{\isacharunderscore}}content\ {\isaliteral{28}{\isacharparenleft}}Text\ txt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ txt\isanewline
\ \ \ \ {\isaliteral{7C}{\isacharbar}}\ slow{\isaliteral{5F}{\isacharunderscore}}content\ {\isaliteral{28}{\isacharparenleft}}Elem\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ name\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
\ \ \ \ \ \ \ \ implode\ {\isaliteral{28}{\isacharparenleft}}map\ slow{\isaliteral{5F}{\isacharunderscore}}content\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ name\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\isanewline
\isanewline
\ \ fun\ add{\isaliteral{5F}{\isacharunderscore}}content\ {\isaliteral{28}{\isacharparenleft}}Text\ txt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Buffer{\isaliteral{2E}{\isachardot}}add\ txt\isanewline
\ \ \ \ {\isaliteral{7C}{\isacharbar}}\ add{\isaliteral{5F}{\isacharunderscore}}content\ {\isaliteral{28}{\isacharparenleft}}Elem\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
\ \ \ \ \ \ \ \ Buffer{\isaliteral{2E}{\isachardot}}add\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ name\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\isanewline
\ \ \ \ \ \ \ \ fold\ add{\isaliteral{5F}{\isacharunderscore}}content\ ts\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\isanewline
\ \ \ \ \ \ \ \ Buffer{\isaliteral{2E}{\isachardot}}add\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ name\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
\ \ fun\ fast{\isaliteral{5F}{\isacharunderscore}}content\ tree\ {\isaliteral{3D}{\isacharequal}}\isanewline
\ \ \ \ Buffer{\isaliteral{2E}{\isachardot}}empty\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ add{\isaliteral{5F}{\isacharunderscore}}content\ tree\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Buffer{\isaliteral{2E}{\isachardot}}content{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
The slow part of \verb|slow_content| is the \verb|implode| of
the recursive results, because it copies previously produced strings
again.
The incremental \verb|add_content| avoids this by operating on a
buffer that is passed through in a linear fashion. Using \verb|#>| and contraction over the actual buffer argument saves some
additional boiler-plate. Of course, the two \verb|Buffer.add|
invocations with concatenated strings could have been split into
smaller parts, but this would have obfuscated the source without
making a big difference in allocations. Here we have done some
peephole-optimization for the sake of readability.
Another benefit of \verb|add_content| is its ``open'' form as a
function on buffers that can be continued in further linear
transformations, folding etc. Thus it is more compositional than
the naive \verb|slow_content|. As realistic example, compare the
old-style \verb|Term.maxidx_of_term: term -> int| with the newer
\verb|Term.maxidx_term: term -> int -> int| in Isabelle/Pure.
Note that \verb|fast_content| above is only defined as example. In
many practical situations, it is customary to provide the
incremental \verb|add_content| only and leave the initialization and
termination to the concrete application by the user.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Message output channels \label{sec:message-channels}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle provides output channels for different kinds of
messages: regular output, high-volume tracing information, warnings,
and errors.
Depending on the user interface involved, these messages may appear
in different text styles or colours. The standard output for
terminal sessions prefixes each line of warnings by \verb|###| and errors by \verb|***|, but leaves anything else
unchanged.
Messages are associated with the transaction context of the running
Isar command. This enables the front-end to manage commands and
resulting messages together. For example, after deleting a command
from a given theory document version, the corresponding message
output can be retracted from the display.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{writeln}\verb|writeln: string -> unit| \\
\indexdef{}{ML}{tracing}\verb|tracing: string -> unit| \\
\indexdef{}{ML}{warning}\verb|warning: string -> unit| \\
\indexdef{}{ML}{error}\verb|error: string -> 'a| \\
\end{mldecls}
\begin{description}
\item \verb|writeln|~\isa{text} outputs \isa{text} as regular
message. This is the primary message output operation of Isabelle
and should be used by default.
\item \verb|tracing|~\isa{text} outputs \isa{text} as special
tracing message, indicating potential high-volume output to the
front-end (hundreds or thousands of messages issued by a single
command). The idea is to allow the user-interface to downgrade the
quality of message display to achieve higher throughput.
Note that the user might have to take special actions to see tracing
output, e.g.\ switch to a different output window. So this channel
should not be used for regular output.
\item \verb|warning|~\isa{text} outputs \isa{text} as
warning, which typically means some extra emphasis on the front-end
side (color highlighting, icons, etc.).
\item \verb|error|~\isa{text} raises exception \verb|ERROR|~\isa{text} and thus lets the Isar toplevel print \isa{text} on the
error channel, which typically means some extra emphasis on the
front-end side (color highlighting, icons, etc.).
This assumes that the exception is not handled before the command
terminates. Handling exception \verb|ERROR|~\isa{text} is a
perfectly legal alternative: it means that the error is absorbed
without any message output.
\begin{warn}
The actual error channel is accessed via \verb|Output.error_msg|, but
the interaction protocol of Proof~General \emph{crashes} if that
function is used in regular ML code: error output and toplevel
command failure always need to coincide.
\end{warn}
\end{description}
\begin{warn}
Regular Isabelle/ML code should output messages exclusively by the
official channels. Using raw I/O on \emph{stdout} or \emph{stderr}
instead (e.g.\ via \verb|TextIO.output|) is apt to cause problems in
the presence of parallel and asynchronous processing of Isabelle
theories. Such raw output might be displayed by the front-end in
some system console log, with a low chance that the user will ever
see it. Moreover, as a genuine side-effect on global process
channels, there is no proper way to retract output when Isar command
transactions are reset by the system.
\end{warn}
\begin{warn}
The message channels should be used in a message-oriented manner.
This means that multi-line output that logically belongs together is
issued by a \emph{single} invocation of \verb|writeln| etc.\ with the
functional concatenation of all message constituents.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
The following example demonstrates a multi-line
warning. Note that in some situations the user sees only the first
line, so the most important point should be made first.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ warning\ {\isaliteral{28}{\isacharparenleft}}cat{\isaliteral{5F}{\isacharunderscore}}lines\isanewline
\ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}Beware\ the\ Jabberwock{\isaliteral{2C}{\isacharcomma}}\ my\ son{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
\ \ \ \ {\isaliteral{22}{\isachardoublequote}}The\ jaws\ that\ bite{\isaliteral{2C}{\isacharcomma}}\ the\ claws\ that\ catch{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Beware\ the\ Jubjub\ Bird{\isaliteral{2C}{\isacharcomma}}\ and\ shun{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
\ \ \ \ {\isaliteral{22}{\isachardoublequote}}The\ frumious\ Bandersnatch{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\isamarkupsection{Exceptions \label{sec:exceptions}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The Standard ML semantics of strict functional evaluation
together with exceptions is rather well defined, but some delicate
points need to be observed to avoid that ML programs go wrong
despite static type-checking. Exceptions in Isabelle/ML are
subsequently categorized as follows.
\paragraph{Regular user errors.} These are meant to provide
informative feedback about malformed input etc.
The \emph{error} function raises the corresponding \emph{ERROR}
exception, with a plain text message as argument. \emph{ERROR}
exceptions can be handled internally, in order to be ignored, turned
into other exceptions, or cascaded by appending messages. If the
corresponding Isabelle/Isar command terminates with an \emph{ERROR}
exception state, the toplevel will print the result on the error
channel (see \secref{sec:message-channels}).
It is considered bad style to refer to internal function names or
values in ML source notation in user error messages.
Grammatical correctness of error messages can be improved by
\emph{omitting} final punctuation: messages are often concatenated
or put into a larger context (e.g.\ augmented with source position).
By not insisting in the final word at the origin of the error, the
system can perform its administrative tasks more easily and
robustly.
\paragraph{Program failures.} There is a handful of standard
exceptions that indicate general failure situations, or failures of
core operations on logical entities (types, terms, theorems,
theories, see \chref{ch:logic}).
These exceptions indicate a genuine breakdown of the program, so the
main purpose is to determine quickly what has happened where.
Traditionally, the (short) exception message would include the name
of an ML function, although this is no longer necessary, because the
ML runtime system prints a detailed source position of the
corresponding \verb|raise| keyword.
\medskip User modules can always introduce their own custom
exceptions locally, e.g.\ to organize internal failures robustly
without overlapping with existing exceptions. Exceptions that are
exposed in module signatures require extra care, though, and should
\emph{not} be introduced by default. Surprise by users of a module
can be often minimized by using plain user errors instead.
\paragraph{Interrupts.} These indicate arbitrary system events:
both the ML runtime system and the Isabelle/ML infrastructure signal
various exceptional situations by raising the special
\emph{Interrupt} exception in user code.
This is the one and only way that physical events can intrude an
Isabelle/ML program. Such an interrupt can mean out-of-memory,
stack overflow, timeout, internal signaling of threads, or the user
producing a console interrupt manually etc. An Isabelle/ML program
that intercepts interrupts becomes dependent on physical effects of
the environment. Even worse, exception handling patterns that are
too general by accident, e.g.\ by mispelled exception constructors,
will cover interrupts unintentionally and thus render the program
semantics ill-defined.
Note that the Interrupt exception dates back to the original SML90
language definition. It was excluded from the SML97 version to
avoid its malign impact on ML program semantics, but without
providing a viable alternative. Isabelle/ML recovers physical
interruptibility (which is an indispensable tool to implement
managed evaluation of command transactions), but requires user code
to be strictly transparent wrt.\ interrupts.
\begin{warn}
Isabelle/ML user code needs to terminate promptly on interruption,
without guessing at its meaning to the system infrastructure.
Temporary handling of interrupts for cleanup of global resources
etc.\ needs to be followed immediately by re-raising of the original
exception.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
\indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
\indexdef{}{ML}{ERROR}\verb|ERROR: string -> exn| \\
\indexdef{}{ML}{Fail}\verb|Fail: string -> exn| \\
\indexdef{}{ML}{Exn.is\_interrupt}\verb|Exn.is_interrupt: exn -> bool| \\
\indexdef{}{ML}{reraise}\verb|reraise: exn -> 'a| \\
\indexdef{}{ML}{exception\_trace}\verb|exception_trace: (unit -> 'a) -> 'a| \\
\end{mldecls}
\begin{description}
\item \verb|try|~\isa{f\ x} makes the partiality of evaluating
\isa{f\ x} explicit via the option datatype. Interrupts are
\emph{not} handled here, i.e.\ this form serves as safe replacement
for the \emph{unsafe} version \verb|(SOME|~\isa{f\ x}~\verb|handle _ => NONE)| that is occasionally seen in
books about SML.
\item \verb|can| is similar to \verb|try| with more abstract result.
\item \verb|ERROR|~\isa{msg} represents user errors; this
exception is normally raised indirectly via the \verb|error| function
(see \secref{sec:message-channels}).
\item \verb|Fail|~\isa{msg} represents general program failures.
\item \verb|Exn.is_interrupt| identifies interrupts robustly, without
mentioning concrete exception constructors in user code. Handled
interrupts need to be re-raised promptly!
\item \verb|reraise|~\isa{exn} raises exception \isa{exn}
while preserving its implicit position information (if possible,
depending on the ML platform).
\item \verb|exception_trace|~\verb|(fn () =>|~\isa{e}\verb|)| evaluates expression \isa{e} while printing
a full trace of its stack of nested exceptions (if possible,
depending on the ML platform).\footnote{In versions of Poly/ML the
trace will appear on raw stdout of the Isabelle process.}
Inserting \verb|exception_trace| into ML code temporarily is useful
for debugging, but not suitable for production code.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isatagmlantiq
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{ML antiquotation}{assert}\hypertarget{ML antiquotation.assert}{\hyperlink{ML antiquotation.assert}{\mbox{\isa{assert}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
\end{matharray}
\begin{description}
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}assert{\isaliteral{7D}{\isacharbraceright}}} inlines a function
\verb|bool -> unit| that raises \verb|Fail| if the argument is
\verb|false|. Due to inlining the source position of failed
assertions is included in the error output.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlantiq
{\isafoldmlantiq}%
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isamarkupsection{Basic data types%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The basis library proposal of SML97 needs to be treated with
caution. Many of its operations simply do not fit with important
Isabelle/ML conventions (like ``canonical argument order'', see
\secref{sec:canonical-argument-order}), others cause problems with
the parallel evaluation model of Isabelle/ML (such as \verb|TextIO.print| or \verb|OS.Process.system|).
Subsequently we give a brief overview of important operations on
basic ML data types.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Characters%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{char}\verb|type char| \\
\end{mldecls}
\begin{description}
\item Type \verb|char| is \emph{not} used. The smallest textual
unit in Isabelle is represented as a ``symbol'' (see
\secref{sec:symbols}).
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Integers%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{int}\verb|type int| \\
\end{mldecls}
\begin{description}
\item Type \verb|int| represents regular mathematical integers,
which are \emph{unbounded}. Overflow never happens in
practice.\footnote{The size limit for integer bit patterns in memory
is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.}
This works uniformly for all supported ML platforms (Poly/ML and
SML/NJ).
Literal integers in ML text are forced to be of this one true
integer type --- overloading of SML97 is disabled.
Structure \verb|IntInf| of SML97 is obsolete and superseded by
\verb|Int|. Structure \verb|Integer| in \hyperlink{file.~~/src/Pure/General/integer.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}integer{\isaliteral{2E}{\isachardot}}ML}}}} provides some additional
operations.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Time%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{Time.time}\verb|type Time.time| \\
\indexdef{}{ML}{seconds}\verb|seconds: real -> Time.time| \\
\end{mldecls}
\begin{description}
\item Type \verb|Time.time| represents time abstractly according
to the SML97 basis library definition. This is adequate for
internal ML operations, but awkward in concrete time specifications.
\item \verb|seconds|~\isa{s} turns the concrete scalar \isa{s} (measured in seconds) into an abstract time value. Floating
point numbers are easy to use as context parameters (e.g.\ via
configuration options, see \secref{sec:config-options}) or
preferences that are maintained by external tools as well.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Options%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{Option.map}\verb|Option.map: ('a -> 'b) -> 'a option -> 'b option| \\
\indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
\indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
\indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
\indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
\indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
\indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\begin{isamarkuptext}%
Apart from \verb|Option.map| most operations defined in
structure \verb|Option| are alien to Isabelle/ML. The
operations shown above are defined in \hyperlink{file.~~/src/Pure/General/basics.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}basics{\isaliteral{2E}{\isachardot}}ML}}}}, among others.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Lists%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Lists are ubiquitous in ML as simple and light-weight
``collections'' for many everyday programming tasks. Isabelle/ML
provides important additions and improvements over operations that
are predefined in the SML97 library.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{cons}\verb|cons: 'a -> 'a list -> 'a list| \\
\indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
\indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
\indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
\indexdef{}{ML}{update}\verb|update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
\end{mldecls}
\begin{description}
\item \verb|cons|~\isa{x\ xs} evaluates to \isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs}.
Tupled infix operators are a historical accident in Standard ML.
The curried \verb|cons| amends this, but it should be only used when
partial application is required.
\item \verb|member|, \verb|insert|, \verb|remove|, \verb|update| treat
lists as a set-like container that maintains the order of elements.
See \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}library{\isaliteral{2E}{\isachardot}}ML}}}} for the full specifications
(written in ML). There are some further derived operations like
\verb|union| or \verb|inter|.
Note that \verb|insert| is conservative about elements that are
already a \verb|member| of the list, while \verb|update| ensures that
the latest entry is always put in front. The latter discipline is
often more appropriate in declarations of context data
(\secref{sec:context-data}) that are issued by the user in Isar
source: more recent declarations normally take precedence over
earlier ones.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
Using canonical \verb|fold| together with \verb|cons|, or
similar standard operations, alternates the orientation of data.
The is quite natural and should not be altered forcible by inserting
extra applications of \verb|rev|. The alternative \verb|fold_rev| can
be used in the few situations, where alternation should be
prevented.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ val\ items\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{4}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{5}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{6}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{7}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{8}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{9}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ fold\ cons\ items\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
\endisaantiq
\ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ items{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ fold{\isaliteral{5F}{\isacharunderscore}}rev\ cons\ items\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
\endisaantiq
\ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ items{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
The subsequent example demonstrates how to \emph{merge} two
lists in a natural way.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ fun\ merge{\isaliteral{5F}{\isacharunderscore}}lists\ eq\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fold{\isaliteral{5F}{\isacharunderscore}}rev\ {\isaliteral{28}{\isacharparenleft}}insert\ eq{\isaliteral{29}{\isacharparenright}}\ ys\ xs{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
Here the first list is treated conservatively: only the new
elements from the second list are inserted. The inside-out order of
insertion via \verb|fold_rev| attempts to preserve the order of
elements in the result.
This way of merging lists is typical for context data
(\secref{sec:context-data}). See also \verb|merge| as defined in
\hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}library{\isaliteral{2E}{\isachardot}}ML}}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Association lists%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The operations for association lists interpret a concrete list
of pairs as a finite function from keys to values. Redundant
representations with multiple occurrences of the same key are
implicitly normalized: lookup and update only take the first
occurrence into account.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
\indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
\indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list| \\
\end{mldecls}
\begin{description}
\item \verb|AList.lookup|, \verb|AList.defined|, \verb|AList.update|
implement the main ``framework operations'' for mappings in
Isabelle/ML, following standard conventions for their names and
types.
Note that a function called \isa{lookup} is obliged to express its
partiality via an explicit option element. There is no choice to
raise an exception, without changing the name to something like
\isa{the{\isaliteral{5F}{\isacharunderscore}}element} or \isa{get}.
The \isa{defined} operation is essentially a contraction of \verb|is_some| and \isa{lookup}, but this is sufficiently frequent to
justify its independent existence. This also gives the
implementation some opportunity for peep-hole optimization.
\end{description}
Association lists are adequate as simple and light-weight
implementation of finite mappings in many practical situations. A
more heavy-duty table structure is defined in \hyperlink{file.~~/src/Pure/General/table.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}table{\isaliteral{2E}{\isachardot}}ML}}}}; that version scales easily to
thousands or millions of elements.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Unsynchronized references%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{Unsynchronized.ref}\verb|type 'a Unsynchronized.ref| \\
\indexdef{}{ML}{Unsynchronized.ref}\verb|Unsynchronized.ref: 'a -> 'a Unsynchronized.ref| \\
\indexdef{}{ML}{!}\verb|! : 'a Unsynchronized.ref -> 'a| \\
\indexdef{}{ML}{:=}\verb|op := : 'a Unsynchronized.ref * 'a -> unit| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\begin{isamarkuptext}%
Due to ubiquitous parallelism in Isabelle/ML (see also
\secref{sec:multi-threading}), the mutable reference cells of
Standard ML are notorious for causing problems. In a highly
parallel system, both correctness \emph{and} performance are easily
degraded when using mutable data.
The unwieldy name of \verb|Unsynchronized.ref| for the constructor
for references in Isabelle/ML emphasizes the inconveniences caused by
mutability. Existing operations \verb|!| and \verb|op :=| are
unchanged, but should be used with special precautions, say in a
strictly local situation that is guaranteed to be restricted to
sequential evaluation --- now and in the future.
\begin{warn}
Never \verb|open Unsynchronized|, not even in a local scope!
Pretending that mutable state is no problem is a very bad idea.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Thread-safe programming \label{sec:multi-threading}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Multi-threaded execution has become an everyday reality in
Isabelle since Poly/ML 5.2.1 and Isabelle2008. Isabelle/ML provides
implicit and explicit parallelism by default, and there is no way
for user-space tools to ``opt out''. ML programs that are purely
functional, output messages only via the official channels
(\secref{sec:message-channels}), and do not intercept interrupts
(\secref{sec:exceptions}) can participate in the multi-threaded
environment immediately without further ado.
More ambitious tools with more fine-grained interaction with the
environment need to observe the principles explained below.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Multi-threading with shared memory%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Multiple threads help to organize advanced operations of the
system, such as real-time conditions on command transactions,
sub-components with explicit communication, general asynchronous
interaction etc. Moreover, parallel evaluation is a prerequisite to
make adequate use of the CPU resources that are available on
multi-core systems.\footnote{Multi-core computing does not mean that
there are ``spare cycles'' to be wasted. It means that the
continued exponential speedup of CPU performance due to ``Moore's
Law'' follows different rules: clock frequency has reached its peak
around 2005, and applications need to be parallelized in order to
avoid a perceived loss of performance. See also
\cite{Sutter:2005}.}
Isabelle/Isar exploits the inherent structure of theories and proofs
to support \emph{implicit parallelism} to a large extent. LCF-style
theorem provides almost ideal conditions for that, see also
\cite{Wenzel:2009}. This means, significant parts of theory and
proof checking is parallelized by default. A maximum speedup-factor
of 3.0 on 4 cores and 5.0 on 8 cores can be
expected.\footnote{Further scalability is limited due to garbage
collection, which is still sequential in Poly/ML 5.2/5.3/5.4. It
helps to provide initial heap space generously, using the
\texttt{-H} option. Initial heap size needs to be scaled-up
together with the number of CPU cores: approximately 1--2\,GB per
core..}
\medskip ML threads lack the memory protection of separate
processes, and operate concurrently on shared heap memory. This has
the advantage that results of independent computations are directly
available to other threads: abstract values can be passed without
copying or awkward serialization that is typically required for
separate processes.
To make shared-memory multi-threading work robustly and efficiently,
some programming guidelines need to be observed. While the ML
system is responsible to maintain basic integrity of the
representation of ML values in memory, the application programmer
needs to ensure that multi-threaded execution does not break the
intended semantics.
\begin{warn}
To participate in implicit parallelism, tools need to be
thread-safe. A single ill-behaved tool can affect the stability and
performance of the whole system.
\end{warn}
Apart from observing the principles of thread-safeness passively,
advanced tools may also exploit parallelism actively, e.g.\ by using
``future values'' (\secref{sec:futures}) or the more basic library
functions for parallel list operations (\secref{sec:parlist}).
\begin{warn}
Parallel computing resources are managed centrally by the
Isabelle/ML infrastructure. User programs must not fork their own
ML threads to perform computations.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Critical shared resources%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Thread-safeness is mainly concerned about concurrent
read/write access to shared resources, which are outside the purely
functional world of ML. This covers the following in particular.
\begin{itemize}
\item Global references (or arrays), i.e.\ mutable memory cells that
persist over several invocations of associated
operations.\footnote{This is independent of the visibility of such
mutable values in the toplevel scope.}
\item Global state of the running Isabelle/ML process, i.e.\ raw I/O
channels, environment variables, current working directory.
\item Writable resources in the file-system that are shared among
different threads or external processes.
\end{itemize}
Isabelle/ML provides various mechanisms to avoid critical shared
resources in most situations. As last resort there are some
mechanisms for explicit synchronization. The following guidelines
help to make Isabelle/ML programs work smoothly in a concurrent
environment.
\begin{itemize}
\item Avoid global references altogether. Isabelle/Isar maintains a
uniform context that incorporates arbitrary data declared by user
programs (\secref{sec:context-data}). This context is passed as
plain value and user tools can get/map their own data in a purely
functional manner. Configuration options within the context
(\secref{sec:config-options}) provide simple drop-in replacements
for historic reference variables.
\item Keep components with local state information re-entrant.
Instead of poking initial values into (private) global references, a
new state record can be created on each invocation, and passed
through any auxiliary functions of the component. The state record
may well contain mutable references, without requiring any special
synchronizations, as long as each invocation gets its own copy.
\item Avoid raw output on \isa{stdout} or \isa{stderr}. The
Poly/ML library is thread-safe for each individual output operation,
but the ordering of parallel invocations is arbitrary. This means
raw output will appear on some system console with unpredictable
interleaving of atomic chunks.
Note that this does not affect regular message output channels
(\secref{sec:message-channels}). An official message is associated
with the command transaction from where it originates, independently
of other transactions. This means each running Isar command has
effectively its own set of message channels, and interleaving can
only happen when commands use parallelism internally (and only at
message boundaries).
\item Treat environment variables and the current working directory
of the running process as strictly read-only.
\item Restrict writing to the file-system to unique temporary files.
Isabelle already provides a temporary directory that is unique for
the running process, and there is a centralized source of unique
serial numbers in Isabelle/ML. Thus temporary files that are passed
to to some external process will be always disjoint, and thus
thread-safe.
\end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{File.tmp\_path}\verb|File.tmp_path: Path.T -> Path.T| \\
\indexdef{}{ML}{serial\_string}\verb|serial_string: unit -> string| \\
\end{mldecls}
\begin{description}
\item \verb|File.tmp_path|~\isa{path} relocates the base
component of \isa{path} into the unique temporary directory of
the running Isabelle/ML process.
\item \verb|serial_string|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}} creates a new serial number
that is unique over the runtime of the Isabelle/ML process.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
The following example shows how to create unique
temporary file names.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ val\ tmp{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ File{\isaliteral{2E}{\isachardot}}tmp{\isaliteral{5F}{\isacharunderscore}}path\ {\isaliteral{28}{\isacharparenleft}}Path{\isaliteral{2E}{\isachardot}}basic\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}foo{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ serial{\isaliteral{5F}{\isacharunderscore}}string\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ val\ tmp{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ File{\isaliteral{2E}{\isachardot}}tmp{\isaliteral{5F}{\isacharunderscore}}path\ {\isaliteral{28}{\isacharparenleft}}Path{\isaliteral{2E}{\isachardot}}basic\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}foo{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ serial{\isaliteral{5F}{\isacharunderscore}}string\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
\endisaantiq
\ {\isaliteral{28}{\isacharparenleft}}tmp{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3E}{\isachargreater}}\ tmp{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\isamarkupsubsection{Explicit synchronization%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle/ML also provides some explicit synchronization
mechanisms, for the rare situations where mutable shared resources
are really required. These are based on the synchronizations
primitives of Poly/ML, which have been adapted to the specific
assumptions of the concurrent Isabelle/ML environment. User code
must not use the Poly/ML primitives directly!
\medskip The most basic synchronization concept is a single
\emph{critical section} (also called ``monitor'' in the literature).
A thread that enters the critical section prevents all other threads
from doing the same. A thread that is already within the critical
section may re-enter it in an idempotent manner.
Such centralized locking is convenient, because it prevents
deadlocks by construction.
\medskip More fine-grained locking works via \emph{synchronized
variables}. An explicit state component is associated with
mechanisms for locking and signaling. There are operations to
await a condition, change the state, and signal the change to all
other waiting threads.
Here the synchronized access to the state variable is \emph{not}
re-entrant: direct or indirect nesting within the same thread will
cause a deadlock!%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
\indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML type}{Synchronized.var}\verb|type 'a Synchronized.var| \\
\indexdef{}{ML}{Synchronized.var}\verb|Synchronized.var: string -> 'a -> 'a Synchronized.var| \\
\indexdef{}{ML}{Synchronized.guarded\_access}\verb|Synchronized.guarded_access: 'a Synchronized.var ->|\isasep\isanewline%
\verb| ('a -> ('b * 'a) option) -> 'b| \\
\end{mldecls}
\begin{description}
\item \verb|NAMED_CRITICAL|~\isa{name\ e} evaluates \isa{e\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}}
within the central critical section of Isabelle/ML. No other thread
may do so at the same time, but non-critical parallel execution will
continue. The \isa{name} argument is used for tracing and might
help to spot sources of congestion.
Entering the critical section without contention is very fast, and
several basic system operations do so frequently. Each thread
should stay within the critical section quickly only very briefly,
otherwise parallel performance may degrade.
\item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
name argument.
\item Type \verb|'a Synchronized.var| represents synchronized
variables with state of type \verb|'a|.
\item \verb|Synchronized.var|~\isa{name\ x} creates a synchronized
variable that is initialized with value \isa{x}. The \isa{name} is used for tracing.
\item \verb|Synchronized.guarded_access|~\isa{var\ f} lets the
function \isa{f} operate within a critical section on the state
\isa{x} as follows: if \isa{f\ x} produces \verb|NONE|, it
continues to wait on the internal condition variable, expecting that
some other thread will eventually change the content in a suitable
manner; if \isa{f\ x} produces \verb|SOME|~\isa{{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}} it is
satisfied and assigns the new state value \isa{x{\isaliteral{27}{\isacharprime}}}, broadcasts a
signal to all waiting threads on the associated condition variable,
and returns the result \isa{y}.
\end{description}
There are some further variants of the \verb|Synchronized.guarded_access| combinator, see \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}Concurrent{\isaliteral{2F}{\isacharslash}}synchronized{\isaliteral{2E}{\isachardot}}ML}}}} for details.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
The following example implements a counter that produces
positive integers that are unique over the runtime of the Isabelle
process:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ local\isanewline
\ \ \ \ val\ counter\ {\isaliteral{3D}{\isacharequal}}\ Synchronized{\isaliteral{2E}{\isachardot}}var\ {\isaliteral{22}{\isachardoublequote}}counter{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ in\isanewline
\ \ \ \ fun\ next\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
\ \ \ \ \ \ Synchronized{\isaliteral{2E}{\isachardot}}guarded{\isaliteral{5F}{\isacharunderscore}}access\ counter\isanewline
\ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}fn\ i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
\ \ \ \ \ \ \ \ \ \ let\ val\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\isanewline
\ \ \ \ \ \ \ \ \ \ in\ SOME\ {\isaliteral{28}{\isacharparenleft}}j{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
\isanewline
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ val\ a\ {\isaliteral{3D}{\isacharequal}}\ next\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ val\ b\ {\isaliteral{3D}{\isacharequal}}\ next\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
\endisaantiq
\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3E}{\isachargreater}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
\medskip See \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}Concurrent{\isaliteral{2F}{\isacharslash}}mailbox{\isaliteral{2E}{\isachardot}}ML}}}} how
to implement a mailbox as synchronized variable over a purely
functional queue.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: