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