--- a/doc-src/IsarImplementation/Thy/document/ML.tex Fri Oct 22 20:51:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Fri Oct 22 20:57:33 2010 +0100
@@ -18,252 +18,2165 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Advanced ML programming%
+\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 are specific library
+ modules and infrastructure to address the needs for such difficult
+ tasks. 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.
+ One should always strife at least for local consistency of modules
+ and sub-systems, without deviating from some general principles how
+ to write Isabelle/ML.
+
+ In a sense, a common 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 source.%
+\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. E.g.\ see \hyperlink{file.~~/src/Pure/thm.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}thm{\isachardot}ML}}}}.
+
+ 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 some a layout via ML comments
+ as follows.
+
+\begin{verbatim}
+(*** section ***)
+
+(** subsection **)
+
+(* subsubsection *)
+
+(*short paragraph*)
+
+(*
+ long paragraph
+ 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 indicate the main theme of the
+ subsequent formal ML text.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Naming conventions%
}
\isamarkuptrue%
%
-\isamarkupsection{Style%
+\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 just 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 (combinators), \\
+ & & 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 --- 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 and keywords. Later it became a 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 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 always 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/lets 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 important 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 to allow to visualize the their data flow
+ via plain regular expressions in the editor. In particular:
+
+ \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|, unless there is an
+ implicit conversion to a general proof context (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.
+
+ \item The main logical entities (\secref{ch:logic}) also have
+ established naming convention:
+
+ \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 treated
+ specifically as a variable can be called \verb|v| or \verb|x|.
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{General source layout%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Like any style guide, also this one should not be interpreted dogmatically, but
- with care and discernment. It consists of a collection of
- recommendations which have been turned out useful over long years of
- Isabelle system development and are supposed to support writing of readable
- and managable code. Special cases encourage derivations,
- as far as you know what you are doing.
- \footnote{This style guide is loosely based on
- \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}}
+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. As a rule of thumb,
+ sources need to be printable on plain paper.} 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{{\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 a concrete pair.
+
+ \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.
+
+ 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 stars etc. should be
+ avoided.
+
+ \paragraph{Complex expressions} consisting of multi-clausal function
+ definitions, \verb|case|, \verb|handle|, \verb|let|,
+ or combinations require special attention. The syntax of Standard
+ ML is a bit too ambitious in admitting too much variance that can
+ distort the meaning of the text.
+
+ Clauses of \verb|fun|, \verb|fn|, \verb|case|,
+ \verb|handle| get extra indentation to indicate the nesting
+ clearly. For 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 particularly imporant to see the
+ structure of the text later on. 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 easily based on simple string
+ 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. For 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
+ is a counter-example involving \verb|let| expressions:
+
+ \begin{verbatim}
+ (* WRONG *)
+
+ 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 environment
+ for arbitrary ML values (see also \secref{sec:context}). This
+ formal context holds logical entities as well as ML compiler
+ bindings, among many other things. Raw Standard ML is never
+ encountered again after the initial bootstrap of Isabelle/Pure.
+
+ Object-logics such as Isabelle/HOL are built within the
+ Isabelle/ML/Isar environment of Pure by introducing suitable
+ theories with associated ML text, 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 regular user-space repertoire of Isabelle.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Isar ML commands%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The primary Isar source language provides various facilities
+ to open a ``window'' to the underlying ML compiler. Especially see
+ \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} and \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which work exactly 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}}}}.
+ An example of even more fine-grained embedding of ML into Isar is
+ 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%
+\ {\isacharverbatimopen}\isanewline
+\ \ fun\ factorial\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}\isanewline
+\ \ \ \ {\isacharbar}\ factorial\ n\ {\isacharequal}\ n\ {\isacharasterisk}\ factorial\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+Here the ML environment is really 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 or similar command loops of Computer Algebra systems, 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.
+ Instead of \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} for theory mode, we use \indexref{}{command}{ML\_prf}\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} for proof mode. As illustrated below, its effect on the
+ ML environment is local to the whole proof body, while ignoring its
+ internal block structure.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ a\ {\isacharequal}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
+\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
+\ %
+\isamarkupcmt{Isar block structure ignored by ML environment%
+}
+\isanewline
+\ \ \ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ b\ {\isacharequal}\ a\ {\isacharplus}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
+\ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
+\ %
+\isamarkupcmt{Isar block structure ignored by ML environment%
+}
+\isanewline
+\ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ c\ {\isacharequal}\ b\ {\isacharplus}\ {\isadigit{1}}\ {\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
+ explicitly, 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{\isacharunderscore}val}}}} and \indexref{}{command}{ML\_command}\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are both
+ \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{\isacharunderscore}val}}}} already takes care of
+ printing the ML toplevel result, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent
+ so we produce an explicit output message.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharverbatimclose}\isanewline
+\isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\ writeln\ {\isacharparenleft}string{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isanewline
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharverbatimclose}\ \ \isanewline
+\ \ \isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\ writeln\ {\isacharparenleft}string{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\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 via some derived ML functions.%
+\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[fundamental law of programming]
- Whenever writing code, keep in mind: A program is
- written once, modified ten times, and read
- hundred times. So simplify its writing,
- always keep future modifications in mind,
- and never jeopardize readability. Every second you hesitate
- to spend on making your code more clear you will
- have to spend ten times understanding what you have
- written later on.
+ \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[white space matters]
- Treat white space in your code as if it determines
- the meaning of code.
+ \item \verb|bind_thms|~\isa{{\isacharparenleft}name{\isacharcomma}\ thms{\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.
- \begin{itemize}
+ \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
+ singleton theorem.
+
+ \end{description}
- \item The space bar is the easiest key to find on the keyboard,
- press it as often as necessary. \verb|2 + 2| is better
- than \verb|2+2|, likewise \verb|f (x, y)| is
- better than \verb|f(x,y)|.
+ It is very 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}. First, the standard token
+ language of ML is augmented by special syntactic entities of the
+ following form:
- \item Restrict your lines to 80 characters. This will allow
- you to keep the beginning of a line in view while watching
- its end.\footnote{To acknowledge the lax practice of
- text editing these days, we tolerate as much as 100
- characters per line, but anything beyond 120 is not
- considered proper source text.}
-
- \item Ban tabulators; they are a context-sensitive formatting
- feature and likely to confuse anyone not using your favorite
- editor.\footnote{Some modern programming language even
- forbid tabulators altogether according to the formal syntax
- definition.}
-
- \item Get rid of trailing whitespace. Instead, do not
- suppress a trailing newline at the end of your files.
+ \indexouternonterm{antiquote}
+ \begin{rail}
+ antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym
+ ;
+ \end{rail}
- \item Choose a generally accepted style of indentation,
- then use it systematically throughout the whole
- application. An indentation of two spaces is appropriate.
- Avoid dangling indentation.
-
- \end{itemize}
+ Here \hyperlink{syntax.nameref}{\mbox{\isa{nameref}}} and \hyperlink{syntax.args}{\mbox{\isa{args}}} are regular outer syntax
+ categories. Note that attributes and proof methods use similar
+ syntax.
- \item[cut-and-paste succeeds over copy-and-paste]
- \emph{Never} copy-and-paste code when programming. If you
- need the same piece of code twice, introduce a
- reasonable auxiliary function (if there is no
- such function, very likely you got something wrong).
- Any copy-and-paste will turn out to be painful
- when something has to be changed later on.
+ \medskip A regular antiquotation \isa{{\isacharat}{\isacharbraceleft}name\ args{\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{{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}}) or abstract
+ \emph{value} (e.g. \isa{{\isacharat}{\isacharbraceleft}thm\ th{\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.
- \item[comments]
- are a device which requires careful thinking before using
- it. The best comment for your code should be the code itself.
- Prefer efforts to write clear, understandable code
- over efforts to explain nasty code.
+ Special antiquotations like \isa{{\isacharat}{\isacharbraceleft}let\ {\isasymdots}{\isacharbraceright}} or \isa{{\isacharat}{\isacharbraceleft}note\ {\isasymdots}{\isacharbraceright}} augment the compilation context without generating code. The
+ non-ASCII braces \isa{{\isasymlbrace}} and \isa{{\isasymrbrace}} allow to delimit the
+ effect by introducing local blocks within the pre-compilation
+ environment.
- \item[functional programming is based on functions]
- Model things as abstract as appropriate. Avoid unnecessarrily
- concrete datatype representations. For example, consider a function
- taking some table data structure as argument and performing
- lookups on it. Instead of taking a table, it could likewise
- take just a lookup function. Accustom
- your way of coding to the level of expressiveness a functional
- programming language is giving onto you.
+ \medskip See also \cite{Wenzel-Chaieb:2007b} for a slightly 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{\isacharunderscore}antiquotation} \\
+ \indexdef{}{ML antiquotation}{note}\hypertarget{ML antiquotation.note}{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+ \end{matharray}
- \item[tuples]
- are often in the way. When there is no striking argument
- to tuple function arguments, just write your function curried.
+ \begin{rail}
+ 'let' ((term + 'and') '=' term + 'and')
+ ;
+
+ 'note' (thmdef? thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{description}
- \item[telling names]
- Any name should tell its purpose as exactly as possible, while
- keeping its length to the absolutely necessary minimum. Always
- give the same name to function arguments which have the same
- meaning. Separate words by underscores (\verb|int_of_string|, not \verb|intOfString|).\footnote{Some
- recent tools for Emacs include special precautions to cope with
- bumpy names in \isa{camelCase}, e.g.\ for improved on-screen
- readability. It is easier to abstain from using such names in the
- first place.}
+ \item \isa{{\isacharat}{\isacharbraceleft}let\ p\ {\isacharequal}\ t{\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{{\isacharat}{\isacharbraceleft}note\ a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isacharbraceright}} recalls existing facts \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\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%
%
-\isamarkupsection{Thread-safe programming%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following artificial example gives a first
+ impression about using the antiquotation elements introduced so far,
+ together with the basic \isa{{\isacharat}{\isacharbraceleft}thm{\isacharbraceright}} antiquotation defined
+ later.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ {\isaantiqopen}\isanewline
+\ \ \ \ %
+\isaantiq
+let\ {\isacharquery}t\ {\isacharequal}\ my{\isacharunderscore}term%
+\endisaantiq
+\isanewline
+\ \ \ \ %
+\isaantiq
+note\ my{\isacharunderscore}refl\ {\isacharequal}\ reflexive\ {\isacharbrackleft}of\ {\isacharquery}t{\isacharbrackright}%
+\endisaantiq
+\isanewline
+\ \ \ \ fun\ foo\ th\ {\isacharequal}\ Thm{\isachardot}transitive\ th\ %
+\isaantiq
+thm\ my{\isacharunderscore}refl%
+\endisaantiq
+\isanewline
+\ \ {\isaantiqclose}\isanewline
+{\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.%
+\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{{\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.
+
+ First of all, functions are usually \emph{curried}: the idea of
+ \isa{f} taking \isa{n} arguments of type \isa{{\isasymtau}\isactrlsub i} (for
+ \isa{i\ {\isasymin}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ n{\isacharbraceright}}) with result \isa{{\isasymtau}} is represented by
+ the iterated function space \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymdots}\ {\isasymrightarrow}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}. This is
+ isomorphic to the encoding via tuples \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymtimes}\ {\isasymdots}\ {\isasymtimes}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}, but
+ the curried version fits more smoothly into the basic
+ calculus.\footnote{The difference is even more significant in
+ higher-order logic, because additional the redundant tuple structure
+ needs to be accommodated by formal reasoning.}
+
+ Currying gives some flexiblity due to \emph{partial application}. A
+ function \isa{f{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymtau}\isactrlbsub {\isadigit{2}}\isactrlesub \ {\isasymrightarrow}\ {\isasymtau}} can be applied to \isa{x{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}}
+ and the remaining \isa{{\isacharparenleft}f\ x{\isacharparenright}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{2}}\ {\isasymrightarrow}\ {\isasymtau}} passed to other functions
+ 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 of function definitions and
+ minimizes adhoc permutations in their application. In Isabelle/ML,
+ large portions of non-trivial source code are written without ever
+ using the infamous function \isa{swap{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymtimes}\ {\isasymalpha}} or the
+ combinator \isa{C{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}\ {\isasymrightarrow}\ {\isacharparenleft}{\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}}, which 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{{\isasymbeta}} that manages elements of type \isa{{\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{\isacharcolon}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ bool} \\
+ update & \isa{insert{\isacharcolon}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} \\
+ \end{tabular}
+ \medskip
+
+ Given a container \isa{B{\isacharcolon}\ {\isasymbeta}}, the partially applied \isa{member\ B} is a predicate over elements \isa{{\isasymalpha}\ {\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\ {\isacharparenleft}member\ B{\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 in the application
+ \isa{forall\ {\isacharparenleft}member\ B{\isacharparenright}} to get directly a predicate again.
+
+ The update operation naturally ``varies'' the container, so it moves
+ to the right: \isa{insert\ a} is a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} to
+ insert a value \isa{a}. These can be composed naturally as
+ follows: \isa{insert\ c\ {\isasymcirc}\ insert\ b\ {\isasymcirc}\ insert\ a}. This works well,
+ apart from some awkwardness due to conventional mathematical
+ function composition, which can be easily amended as follows.%
+\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\ {\isacharparenleft}f\ x\ y\ {\isacharplus}\ g\ z{\isacharparenright}}. The important special case if \emph{linear transformation}
+ applies a cascade of functions as follows: \isa{f\isactrlsub n\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}f\isactrlsub {\isadigit{1}}\ x{\isacharparenright}{\isacharparenright}}.
+ This becomes hard to read and maintain if the functions are
+ themselves 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\ {\isacharbar}{\isachargreater}\ f} & \isa{{\isasymequiv}} & \isa{f\ x} \\
+ \isa{f\ {\isacharhash}{\isachargreater}\ g} & \isa{{\isasymequiv}} & \isa{x\ {\isacharbar}{\isachargreater}\ f\ {\isacharbar}{\isachargreater}\ g} \\
+ \end{tabular}
+ \medskip
+
+ This enables to write conveniently \isa{x\ {\isacharbar}{\isachargreater}\ f\isactrlsub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\isactrlsub n} or
+ \isa{f\isactrlsub {\isadigit{1}}\ {\isacharhash}{\isachargreater}\ {\isasymdots}\ {\isacharhash}{\isachargreater}\ f\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{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharbar}{\isacharminus}{\isachargreater}\ f} & \isa{{\isasymequiv}} & \isa{f\ x\ y} \\
+ \isa{f\ {\isacharhash}{\isacharminus}{\isachargreater}\ g} & \isa{{\isasymequiv}} & \isa{x\ {\isacharbar}{\isachargreater}\ f\ {\isacharbar}{\isacharminus}{\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{\isacharcolon}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} can be
+ understood as update on a configuration of type \isa{{\isasymbeta}} that is
+ parametrized by arguments of type \isa{{\isasymalpha}}. Given \isa{a{\isacharcolon}\ {\isasymalpha}}
+ the partial application \isa{{\isacharparenleft}f\ a{\isacharparenright}{\isacharcolon}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} operates
+ homogeneously on \isa{{\isasymbeta}}. This can be iterated naturally over a
+ list of parameters \isa{{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isacharbrackright}} as \isa{f\ a\isactrlsub {\isadigit{1}}\ {\isacharhash}{\isachargreater}\ {\isasymdots}\ {\isacharhash}{\isachargreater}\ f\ a\isactrlbsub n\isactrlesub \isactrlbsub \isactrlesub }. The latter expression is again a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}}.
+ It can be applied to an initial configuration \isa{b{\isacharcolon}\ {\isasymbeta}} to
+ start the iteration over the given list of arguments: each \isa{a} in \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\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{{\isacharparenleft}fold\ {\isasymcirc}\ fold{\isacharparenright}\ f} iterates
+ over a list of lists as expected.
+
+ The variant \isa{fold{\isacharunderscore}rev} works inside-out over the list of
+ arguments, such that \isa{fold{\isacharunderscore}rev\ f\ {\isasymequiv}\ fold\ f\ {\isasymcirc}\ rev} holds.
+
+ The \isa{fold{\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 still has the
+ slightly more convenient 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%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ s\ {\isacharequal}\isanewline
+\ \ \ \ Buffer{\isachardot}empty\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}add\ {\isachardoublequote}digits{\isacharcolon}\ {\isachardoublequote}\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ fold\ {\isacharparenleft}Buffer{\isachardot}add\ o\ string{\isacharunderscore}of{\isacharunderscore}int{\isacharparenright}\ {\isacharparenleft}{\isadigit{0}}\ upto\ {\isadigit{9}}{\isacharparenright}\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}content{\isacharsemicolon}\isanewline
+\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}s\ {\isacharequal}\ {\isachardoublequote}digits{\isacharcolon}\ {\isadigit{0}}{\isadigit{1}}{\isadigit{2}}{\isadigit{3}}{\isadigit{4}}{\isadigit{5}}{\isadigit{6}}{\isadigit{7}}{\isadigit{8}}{\isadigit{9}}{\isachardoublequote}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\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 this idea and demonstrates fast
+ accumulation of tree content using a text buffer.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ datatype\ tree\ {\isacharequal}\ Text\ of\ string\ {\isacharbar}\ Elem\ of\ string\ {\isacharasterisk}\ tree\ list{\isacharsemicolon}\isanewline
+\isanewline
+\ \ fun\ slow{\isacharunderscore}content\ {\isacharparenleft}Text\ txt{\isacharparenright}\ {\isacharequal}\ txt\isanewline
+\ \ \ \ {\isacharbar}\ slow{\isacharunderscore}content\ {\isacharparenleft}Elem\ {\isacharparenleft}name{\isacharcomma}\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharless}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}\ {\isacharcircum}\isanewline
+\ \ \ \ \ \ \ \ implode\ {\isacharparenleft}map\ slow{\isacharunderscore}content\ ts{\isacharparenright}\ {\isacharcircum}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharless}{\isacharslash}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}\isanewline
+\isanewline
+\ \ fun\ add{\isacharunderscore}content\ {\isacharparenleft}Text\ txt{\isacharparenright}\ {\isacharequal}\ Buffer{\isachardot}add\ txt\isanewline
+\ \ \ \ {\isacharbar}\ add{\isacharunderscore}content\ {\isacharparenleft}Elem\ {\isacharparenleft}name{\isacharcomma}\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ Buffer{\isachardot}add\ {\isacharparenleft}{\isachardoublequote}{\isacharless}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}{\isacharparenright}\ {\isacharhash}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ fold\ add{\isacharunderscore}content\ ts\ {\isacharhash}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Buffer{\isachardot}add\ {\isacharparenleft}{\isachardoublequote}{\isacharless}{\isacharslash}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ fun\ fast{\isacharunderscore}content\ tree\ {\isacharequal}\isanewline
+\ \ \ \ Buffer{\isachardot}empty\ {\isacharbar}{\isachargreater}\ add{\isacharunderscore}content\ tree\ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}content{\isacharsemicolon}\isanewline
+{\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
+ afresh.
+
+ 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 \verb|Buffer.T| argument
+ saves some additional boiler-plate, but requires again some
+ practice. 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 \verb|Buffer.T| that can be continued in further
+ linear transformations, folding etc. Thus it is more compositional
+ than the naive \verb|slow_content|. As a realistic example, compare
+ the slightly 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 for completeness
+ of the example. In many practical situations, it is customary to
+ defined 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, icon).
+
+ \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, icon).
+
+ 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 here.
+ \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.
+ \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
+ needs to be 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{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ warning\ {\isacharparenleft}cat{\isacharunderscore}lines\isanewline
+\ \ \ {\isacharbrackleft}{\isachardoublequote}Beware\ the\ Jabberwock{\isacharcomma}\ my\ son{\isacharbang}{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}The\ jaws\ that\ bite{\isacharcomma}\ the\ claws\ that\ catch{\isacharbang}{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}Beware\ the\ Jubjub\ Bird{\isacharcomma}\ and\ shun{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}The\ frumious\ Bandersnatch{\isacharbang}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isamarkupsection{Exceptions \label{sec:exceptions}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Recent versions of Poly/ML (5.2.1 or later) support robust
- multithreaded execution, based on native operating system threads of
- the underlying platform. Thus threads will actually be executed in
- parallel on multi-core systems. A speedup-factor of approximately
- 1.5--3 can be expected on a regular 4-core machine.\footnote{There
- is some inherent limitation of the speedup factor due to garbage
- collection, which is still sequential. It helps to provide initial
- heap space generously, using the \texttt{-H} option of Poly/ML.}
- Threads also help to organize advanced operations of the system,
- with explicit communication between sub-components, real-time
- conditions, time-outs etc.
+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 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 end-users or ML
+ users of a module can be often minimized by using plain user errors.
+
+ \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 an indispensable tool to implement managed
+ evaluation of Isar 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 always raised 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 various 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{\isacharunderscore}antiquotation} \\
+ \end{matharray}
+
+ \begin{description}
+
+ \item \isa{{\isacharat}{\isacharbraceleft}assert{\isacharbraceright}} inlines a function \isa{bool\ {\isasymRightarrow}\ 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 need 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 can cause serious
+ 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 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 (e.g.\ \verb|123456789012345678901234567890|) are forced to be of this one true
+ integer type --- overloading of SML97 is disabled.
+
+ Structure \verb|IntInf| of SML97 is obsolete, always use
+ \verb|Int|. Structure \verb|Integer| in \hyperlink{file.~~/src/Pure/General/integer.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}integer{\isachardot}ML}}}} provides some additional
+ operations.
- 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 immediately available
- to other threads, without requiring untyped character streams,
- awkward serialization etc.
+ \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{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}basics{\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\ {\isacharcolon}{\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{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}library{\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 last 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.
- On the other hand, some programming guidelines need to be observed
- in order to make unprotected parallelism work out smoothly. While
- the ML system implementation is responsible to maintain basic
- integrity of the representation of ML values in memory, the
- application programmer needs to ensure that multithreaded execution
- does not break the intended semantics.
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+Using canonical \verb|fold| together with canonical \verb|cons|, or similar standard operations, alternates the orientation of
+ data. The is quite natural and should not altered forcible by
+ inserting extra applications \verb|rev|. The alternative \verb|fold_rev| can be used in the relatively few situations, where
+ alternation should be prevented.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ items\ {\isacharequal}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{8}}{\isacharcomma}\ {\isadigit{9}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{0}}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isacharequal}\ fold\ cons\ items\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{1}}\ {\isacharequal}\ rev\ items{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{2}}\ {\isacharequal}\ fold{\isacharunderscore}rev\ cons\ items\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{2}}\ {\isacharequal}\ items{\isacharparenright}{\isacharsemicolon}\isanewline
+{\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%
+\ {\isacharverbatimopen}\isanewline
+\ \ fun\ merge{\isacharunderscore}lists\ eq\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}\ {\isacharequal}\ fold{\isacharunderscore}rev\ {\isacharparenleft}insert\ eq{\isacharparenright}\ ys\ xs{\isacharsemicolon}\isanewline
+{\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{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}library{\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, with standard conventions for 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{\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}
- \medskip \paragraph{Critical shared resources.} Actually only those
- parts outside the purely functional world of ML are critical. In
- particular, this covers
+ 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{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}table{\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.%
+\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
+ immediately available to other threads: abstract values can be
+ passed between threads without copying or awkward serialization that
+ is typically required for explicit message passing between 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.\ those 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 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 direct I/O on shared channels, notably \isa{stdin}, \isa{stdout}, \isa{stderr}.
+ \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 other processes.
\end{itemize}
- The majority of tools implemented within the Isabelle/Isar framework
- will not require any of these critical elements: nothing special
- needs to be observed when staying in the purely functional fragment
- of ML. Note that output via the official Isabelle channels does not
- count as direct I/O, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe.
-
- Moreover, ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to
- run-time invocation of the compiler are also safe, because
- Isabelle/Isar manages this as part of the theory or proof context.
-
- \paragraph{Multithreading in Isabelle/Isar.} The theory loader
- automatically exploits the overall parallelism of independent nodes
- in the development graph, as well as the inherent irrelevance of
- proofs for goals being fully specified in advance. This means,
- checking of individual Isar proofs is parallelized by default.
- Beyond that, very sophisticated proof tools may use local
- parallelism internally, via the general programming model of
- ``future values'' (see also \hyperlink{file.~~/src/Pure/Concurrent/future.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}future{\isachardot}ML}}}}).
-
- Any ML code that works relatively to the present background theory
- is already safe. Contextual data may be easily stored within the
- theory or proof context, thanks to the generic data concept of
- Isabelle/Isar (see \secref{sec:context-data}). This greatly
- diminishes the demand for global state information in the first
- place.
-
- \medskip In rare situations where actual mutable content needs to be
- manipulated, Isabelle provides a single \emph{critical section} that
- may be entered while preventing any other thread from doing the
- same. Entering the critical section without contention is very
- fast, and several basic system operations do so frequently. This
- also means that each thread should leave the critical section
- quickly, otherwise parallel execution performance may degrade
- significantly.
-
- Despite this potential bottle-neck, centralized locking is
- convenient, because it prevents deadlocks without demanding special
- precautions. Explicit communication demands other means, though.
- The high-level abstraction of synchronized variables \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} enables parallel
- components to communicate via shared state; see also \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} as canonical example.
-
- \paragraph{Good conduct of impure programs.} The following
- guidelines enable non-functional programs to participate in
- multithreading.
+ Isabelle/ML provides various mechanisms to avoid critical shared
+ resources in most practical 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 Minimize global state information. Using proper theory and
- proof context data will actually return to functional update of
- values, without any special precautions for multithreading. Apart
- from the fully general functors for theory and proof data (see
- \secref{sec:context-data}) there are drop-in replacements that
- emulate primitive references for common cases of \emph{configuration
- options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor
- \verb|Named_Thms|).
+ \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 formerly writable flags.
+
+ \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 Keep components with local state information
- \emph{re-entrant}. Instead of poking initial values into (private)
- global references, create a new state record on each invocation, and
- pass that 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 sees its
- own copy. Occasionally, one might even return to plain functional
- updates on non-mutable record values here.
+ \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{{\isacharparenleft}{\isacharparenright}} creates a new serial number
+ that is unique over the runtime of the Isabelle/ML process.
- \item Isolate process configuration flags. The main legitimate
- application of global references is to configure the whole process
- in a certain way, essentially affecting all threads. A typical
- example is the \verb|show_types| flag, which tells the pretty printer
- to output explicit type information for terms. Such flags usually
- do not affect the functionality of the core system, but only the
- view being presented to the user.
-
- Occasionally, such global process flags are treated like implicit
- arguments to certain operations, by using the \verb|setmp_CRITICAL| combinator
- for safe temporary assignment. Its traditional purpose was to
- ensure proper recovery of the original value when exceptions are
- raised in the body, now the functionality is extended to enter the
- \emph{critical section} (with its usual potential of degrading
- parallelism).
+ \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%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ tmp{\isadigit{1}}\ {\isacharequal}\ File{\isachardot}tmp{\isacharunderscore}path\ {\isacharparenleft}Path{\isachardot}basic\ {\isacharparenleft}{\isachardoublequote}foo{\isachardoublequote}\ {\isacharcircum}\ serial{\isacharunderscore}string\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ val\ tmp{\isadigit{2}}\ {\isacharequal}\ File{\isachardot}tmp{\isacharunderscore}path\ {\isacharparenleft}Path{\isachardot}basic\ {\isacharparenleft}{\isachardoublequote}foo{\isachardoublequote}\ {\isacharcircum}\ serial{\isacharunderscore}string\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}tmp{\isadigit{1}}\ {\isacharless}{\isachargreater}\ tmp{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\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!
- Note that recovery of plain value passing semantics via \verb|setmp_CRITICAL|~\isa{ref\ value} assumes that this \isa{ref} is
- exclusively manipulated within the critical section. In particular,
- any persistent global assignment of \isa{ref\ {\isacharcolon}{\isacharequal}\ value} needs to
- be marked critical as well, to prevent intruding another threads
- local view, and a lost-update in the global scope, too.
+ \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.
- \end{itemize}
+ Such centralized locking is convenient, because it prevents
+ deadlocks by construction.
- Recall that in an open ``LCF-style'' system like Isabelle/Isar, the
- user participates in constructing the overall environment. This
- means that state-based facilities offered by one component will
- require special caution later on. So minimizing critical elements,
- by staying within the plain value-oriented view relative to theory
- or proof contexts most of the time, will also reduce the chance of
- mishaps occurring to end-users.%
+ \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%
%
@@ -277,215 +2190,49 @@
\begin{mldecls}
\indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
\indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
- \indexdef{}{ML}{setmp\_CRITICAL}\verb|setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
+ \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\ f} evaluates \isa{f\ {\isacharparenleft}{\isacharparenright}}
- while staying within the critical section of Isabelle/Isar. No
- other thread may do so at the same time, but non-critical parallel
- execution will continue. The \isa{name} argument serves for
- diagnostic purposes and might help to spot sources of congestion.
+ \item \verb|NAMED_CRITICAL|~\isa{name\ e} evaluates \isa{e\ {\isacharparenleft}{\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 leave the critical section quickly, otherwise parallel
+ performance may degrade.
\item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
name argument.
- \item \verb|setmp_CRITICAL|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x}
- while staying within the critical section and having \isa{ref\ {\isacharcolon}{\isacharequal}\ value} assigned temporarily. This recovers a value-passing
- semantics involving global references, regardless of exceptions or
- concurrency.
+ \item Type \verb|'a Synchronized.var| represents synchronized
+ variables with state of type \verb|'a|.
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupchapter{Basic library functions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Beyond the proposal of the SML/NJ basis library, Isabelle comes
- with its own library, from which selected parts are given here.
- These should encourage a study of the Isabelle sources,
- in particular files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Linear transformations \label{sec:ML-linear-trans}%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{op $\mid$$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\noindent Many problems in functional programming can be thought of
- as linear transformations, i.e.~a caluclation starts with a
- particular value \verb|x : foo| which is then transformed
- by application of a function \verb|f : foo -> foo|,
- continued by an application of a function \verb|g : foo -> bar|,
- and so on. As a canoncial example, take functions enriching
- a theory by constant declararion and primitive definitions:
-
- \smallskip\begin{mldecls}
- \verb|Sign.declare_const: (binding * typ) * mixfix|\isasep\isanewline%
-\verb| -> theory -> term * theory| \\
- \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory|
- \end{mldecls}
-
- \noindent Written with naive application, an addition of constant
- \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
- a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
-
- \smallskip\begin{mldecls}
- \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
-\verb| (Sign.declare_const|\isasep\isanewline%
-\verb| ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
- \end{mldecls}
+ \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.
- \noindent With increasing numbers of applications, this code gets quite
- unreadable. Further, it is unintuitive that things are
- written down in the opposite order as they actually ``happen''.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\noindent At this stage, Isabelle offers some combinators which allow
- for more convenient notation, most notably reverse application:
-
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{op $\mid$-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
- \indexdef{}{ML}{op $\mid$$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
- \indexdef{}{ML}{op $\mid$$\mid$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
- \indexdef{}{ML}{op $\mid$$\mid$$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\begin{isamarkuptext}%
-\noindent Usually, functions involving theory updates also return
- side results; to use these conveniently, yet another
- set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->|
- which allows curried access to side results:
+ \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|, we
+ continue 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{{\isacharparenleft}y{\isacharcomma}\ x{\isacharprime}{\isacharparenright}} we
+ are satisfied and assign the new state value \isa{x{\isacharprime}}, broadcast
+ a signal to all waiting threads on the associated condition
+ variable, and return the result \isa{y}.
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
-
- \end{mldecls}
-
- \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own:
-
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false (Binding.name "bar_def", def))|\isasep\isanewline%
-
- \end{mldecls}
-
- \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation
- in the presence of side results which are left unchanged:
+ \end{description}
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
-
- \end{mldecls}
-
- \noindent \verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results:
-
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
-
- \end{mldecls}%
-\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\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
- \end{mldecls}%
+ There are some further variants of the general \verb|Synchronized.guarded_access| combinator, see \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} for details.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -496,283 +2243,68 @@
%
\endisadelimmlref
%
-\begin{isamarkuptext}%
-\noindent This principles naturally lift to \emph{lists} using
- the \verb|fold| and \verb|fold_map| combinators.
- The first lifts a single function
- \begin{quote}\footnotesize
- \verb|f : 'a -> 'b -> 'b| to \verb|'a list -> 'b -> 'b|
- \end{quote}
- such that
- \begin{quote}\footnotesize
- \verb|y |\verb,|,\verb|> fold f [x1, x2, ..., x_n]| \\
- \hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb|> f x2 |\verb,|,\verb|> ... |\verb,|,\verb|> f x_n|
- \end{quote}
- \noindent The second accumulates side results in a list by lifting
- a single function
- \begin{quote}\footnotesize
- \verb|f : 'a -> 'b -> 'c * 'b| to \verb|'a list -> 'b -> 'c list * 'b|
- \end{quote}
- such that
- \begin{quote}\footnotesize
- \verb|y |\verb,|,\verb|> fold_map f [x1, x2, ..., x_n]| \\
- \hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb||\verb,|,\verb|>> f x2 |\verb,|,\verb||\verb,|,\verb|>> ... |\verb,|,\verb||\verb,|,\verb|>> f x_n| \\
- \hspace*{6ex}\verb||\verb,|,\verb||\verb,|,\verb|> (fn ((z1, z2), ..., z_n) => [z1, z2, ..., z_n])|
- \end{quote}
-
- \noindent Example:
-
- \smallskip\begin{mldecls}
-\verb|let|\isasep\isanewline%
-\verb| val consts = ["foo", "bar"];|\isasep\isanewline%
-\verb|in|\isasep\isanewline%
-\verb| thy|\isasep\isanewline%
-\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const|\isasep\isanewline%
-\verb| ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
-\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
-\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
-\verb| Thm.add_def false false (Binding.empty, def)) defs)|\isasep\isanewline%
-\verb|end|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimmlex
%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
+\endisadelimmlex
%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
- \indexdef{}{ML}{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
- \indexdef{}{ML}{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
- \indexdef{}{ML}{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
- \indexdef{}{ML}{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
+\isatagmlex
%
\begin{isamarkuptext}%
-\noindent All those linear combinators also exist in higher-order
- variants which do not expect a value on the left hand side
- but a function.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
- \indexdef{}{ML}{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\begin{isamarkuptext}%
-\noindent These operators allow to ``query'' a context
- in a series of context transformations:
+See \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} how to
+ implement a mailbox as synchronized variable over a purely
+ functional queue.
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
-\verb| (Sign.full_name thy (Binding.name "foobar")))|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
-\verb| else Sign.declare_const|\isasep\isanewline%
-\verb| ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
-
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Options and partiality%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \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| \\
- \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
- \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
- \end{mldecls}%
+ \medskip The following example implements a counter that produces
+ positive integers that are unique over the runtime of the Isabelle
+ process:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
+\endisatagmlex
+{\isafoldmlex}%
%
-\begin{isamarkuptext}%
-Standard selector functions on \isa{option}s are provided. The
- \verb|try| and \verb|can| functions provide a convenient interface for
- handling exceptions -- both take as arguments a function \verb|f|
- together with a parameter \verb|x| and handle any exception during
- the evaluation of the application of \verb|f| to \verb|x|, either
- return a lifted result (\verb|NONE| on failure) or a boolean value
- (\verb|false| on failure).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Common data structures%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lists (as set-like data structures)%
-}
-\isamarkuptrue%
+\isadelimmlex
%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \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}{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\endisadelimmlex
%
-\begin{isamarkuptext}%
-Lists are often used as set-like data structures -- set-like in
- the sense that they support a notion of \verb|member|-ship,
- \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive.
- This is convenient when implementing a history-like mechanism:
- \verb|insert| adds an element \emph{to the front} of a list,
- if not yet present; \verb|remove| removes \emph{all} occurences
- of a particular element. Correspondingly \verb|merge| implements a
- a merge on two lists suitable for merges of context data
- (\secref{sec:context-theory}).
-
- Functions are parametrized by an explicit equality function
- to accomplish overloaded equality; in most cases of monomorphic
- equality, writing \verb|op =| should suffice.%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimML
%
-\isamarkupsubsection{Association lists%
-}
-\isamarkuptrue%
+\endisadelimML
%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML exception}{AList.DUP}\verb|exception AList.DUP| \\
- \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| \\
- \indexdef{}{ML}{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
- \indexdef{}{ML}{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
- \indexdef{}{ML}{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
-\verb| -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
- \indexdef{}{ML}{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
-\verb| -> ('a * 'b) list -> ('a * 'b) list| \\
- \indexdef{}{ML}{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
-\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
- \indexdef{}{ML}{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
-\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Association lists can be seens as an extension of set-like lists:
- on the one hand, they may be used to implement finite mappings,
- on the other hand, they remain order-sensitive and allow for
- multiple key-value-pair with the same key: \verb|AList.lookup|
- returns the \emph{first} value corresponding to a particular
- key, if present. \verb|AList.update| updates
- the \emph{first} occurence of a particular key; if no such
- key exists yet, the key-value-pair is added \emph{to the front}.
- \verb|AList.delete| only deletes the \emph{first} occurence of a key.
- \verb|AList.merge| provides an operation suitable for merges of context data
- (\secref{sec:context-theory}), where an equality parameter on
- values determines whether a merge should be considered a conflict.
- A slightly generalized operation if implementend by the \verb|AList.join|
- function which allows for explicit conflict resolution.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Tables%
-}
-\isamarkuptrue%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ local\isanewline
+\ \ \ \ val\ counter\ {\isacharequal}\ Synchronized{\isachardot}var\ {\isachardoublequote}counter{\isachardoublequote}\ {\isadigit{0}}{\isacharsemicolon}\isanewline
+\ \ in\isanewline
+\ \ \ \ fun\ next\ {\isacharparenleft}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ Synchronized{\isachardot}guarded{\isacharunderscore}access\ counter\isanewline
+\ \ \ \ \ \ \ \ {\isacharparenleft}fn\ i\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isadigit{1}}\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ SOME\ {\isacharparenleft}j{\isacharcomma}\ j{\isacharparenright}\ end{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ end{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}\isanewline
+\isanewline
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ a\ {\isacharequal}\ next\ {\isacharparenleft}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ val\ b\ {\isacharequal}\ next\ {\isacharparenleft}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}a\ {\isacharless}{\isachargreater}\ b{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML type}{'a Symtab.table}\verb|type 'a Symtab.table| \\
- \indexdef{}{ML exception}{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
- \indexdef{}{ML exception}{Symtab.SAME}\verb|exception Symtab.SAME| \\
- \indexdef{}{ML exception}{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
- \indexdef{}{ML}{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
- \indexdef{}{ML}{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
- \indexdef{}{ML}{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
-\verb| -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
- \indexdef{}{ML}{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
-\verb| -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
-\verb| -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
-\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
-\verb| -> 'a Symtab.table (*exception Symtab.DUP*)| \\
- \indexdef{}{ML}{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
-\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
-\verb| -> 'a Symtab.table (*exception Symtab.DUP*)|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimML
%
-\begin{isamarkuptext}%
-Tables are an efficient representation of finite mappings without
- any notion of order; due to their efficiency they should be used
- whenever such pure finite mappings are neccessary.
-
- The key type of tables must be given explicitly by instantiating
- the \verb|Table| functor which takes the key type
- together with its \verb|order|; for convience, we restrict
- here to the \verb|Symtab| instance with \verb|string|
- as key type.
-
- Most table functions correspond to those of association lists.%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\endisadelimML
+\isanewline
%
\isadelimtheory
+\isanewline
%
\endisadelimtheory
%