--- a/doc-src/IsarImplementation/Thy/document/ML.tex Fri Oct 22 20:51:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Fri Oct 22 20:57:33 2010 +0100
@@ -18,252 +18,2165 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Advanced ML programming%
+\isamarkupchapter{Isabelle/ML%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/ML is best understood as a certain culture based on
+ Standard ML. Thus it is not a new programming language, but a
+ certain way to use SML at an advanced level within the Isabelle
+ environment. This covers a variety of aspects that are geared
+ towards an efficient and robust platform for applications of formal
+ logic with fully foundational proof construction --- according to
+ the well-known \emph{LCF principle}. There are specific library
+ modules and infrastructure to address the needs for such difficult
+ tasks. For example, the raw parallel programming model of Poly/ML
+ is presented as considerably more abstract concept of \emph{future
+ values}, which is then used to augment the inference kernel, proof
+ interpreter, and theory loader accordingly.
+
+ The main aspects of Isabelle/ML are introduced below. These
+ first-hand explanations should help to understand how proper
+ Isabelle/ML is to be read and written, and to get access to the
+ wealth of experience that is expressed in the source text and its
+ history of changes.\footnote{See
+ \url{http://isabelle.in.tum.de/repos/isabelle} for the full
+ Mercurial history. There are symbolic tags to refer to official
+ Isabelle releases, as opposed to arbitrary \emph{tip} versions that
+ merely reflect snapshots that are never really up-to-date.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Style and orthography%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The sources of Isabelle/Isar are optimized for
+ \emph{readability} and \emph{maintainability}. The main purpose is
+ to tell an informed reader what is really going on and how things
+ really work. This is a non-trivial aim, but it is supported by a
+ certain style of writing Isabelle/ML that has emerged from long
+ years of system development.\footnote{See also the interesting style
+ guide for OCaml
+ \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}
+ which shares many of our means and ends.}
+
+ The main principle behind any coding style is \emph{consistency}.
+ For a single author of a small program this merely means ``choose
+ your style and stick to it''. A complex project like Isabelle, with
+ long years of development and different contributors, requires more
+ standardization. A coding style that is changed every few years or
+ with every new contributor is no style at all, because consistency
+ is quickly lost. Global consistency is hard to achieve, though.
+ One should always strife at least for local consistency of modules
+ and sub-systems, without deviating from some general principles how
+ to write Isabelle/ML.
+
+ In a sense, a common coding style is like an \emph{orthography} for
+ the sources: it helps to read quickly over the text and see through
+ the main points, without getting distracted by accidental
+ presentation of free-style source.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Header and sectioning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle source files have a certain standardized header
+ format (with precise spacing) that follows ancient traditions
+ reaching back to the earliest versions of the system by Larry
+ Paulson. E.g.\ see \hyperlink{file.~~/src/Pure/thm.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}thm{\isachardot}ML}}}}.
+
+ The header includes at least \verb|Title| and \verb|Author| entries, followed by a prose description of the purpose of
+ the module. The latter can range from a single line to several
+ paragraphs of explanations.
+
+ The rest of the file is divided into sections, subsections,
+ subsubsections, paragraphs etc.\ using some a layout via ML comments
+ as follows.
+
+\begin{verbatim}
+(*** section ***)
+
+(** subsection **)
+
+(* subsubsection *)
+
+(*short paragraph*)
+
+(*
+ long paragraph
+ more text
+*)
+\end{verbatim}
+
+ As in regular typography, there is some extra space \emph{before}
+ section headings that are adjacent to plain text (not other headings
+ as in the example above).
+
+ \medskip The precise wording of the prose text given in these
+ headings is chosen carefully to indicate the main theme of the
+ subsequent formal ML text.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Naming conventions%
}
\isamarkuptrue%
%
-\isamarkupsection{Style%
+\begin{isamarkuptext}%
+Since ML is the primary medium to express the meaning of the
+ source text, naming of ML entities requires special care.
+
+ \paragraph{Notation.} A name consists of 1--3 \emph{words} (rarely
+ 4, but not more) that are separated by underscore. There are three
+ variants concerning upper or lower case letters, which are just for
+ certain ML categories as follows:
+
+ \medskip
+ \begin{tabular}{lll}
+ variant & example & ML categories \\\hline
+ lower-case & \verb|foo_bar| & values, types, record fields \\
+ capitalized & \verb|Foo_Bar| & datatype constructors, \\
+ & & structures, functors \\
+ upper-case & \verb|FOO_BAR| & special values (combinators), \\
+ & & exception constructors, signatures \\
+ \end{tabular}
+ \medskip
+
+ For historical reasons, many capitalized names omit underscores,
+ e.g.\ old-style \verb|FooBar| instead of \verb|Foo_Bar|.
+ Genuine mixed-case names are \emph{not} used --- clear division of
+ words is essential for readability.\footnote{Camel-case was invented
+ to workaround the lack of underscore in some early non-ASCII
+ character sets and keywords. Later it became a habitual in some
+ language communities that are now strong in numbers.}
+
+ A single (capital) character does not count as ``word'' in this
+ respect: some Isabelle/ML are suffixed by extra markers like this:
+ \verb|foo_barT|.
+
+ Name variants are produced by adding 1--3 primes, e.g.\ \verb|foo'|, \verb|foo''|, or \verb|foo'''|, but not \verb|foo''''| or more. Decimal digits scale better to larger numbers,
+ e.g.\ \verb|foo0|, \verb|foo1|, \verb|foo42|.
+
+ \paragraph{Scopes.} Apart from very basic library modules, ML
+ structures are not ``opened'', but names are referenced with
+ explicit qualification, as in \verb|Syntax.string_of_term| for
+ example. When devising names for structures and their components it
+ is important aim at eye-catching compositions of both parts, because
+ this is how they are always seen in the sources and documentation.
+ For the same reasons, aliases of well-known library functions should
+ be avoided.
+
+ Local names of function abstraction or case/lets bindings are
+ typically shorter, sometimes using only rudiments of ``words'',
+ while still avoiding cryptic shorthands. An auxiliary function
+ called \verb|helper|, \verb|aux|, or \verb|f| is
+ considered bad style.
+
+ Example:
+
+ \begin{verbatim}
+ (* RIGHT *)
+
+ fun print_foo ctxt foo =
+ let
+ fun print t = ... Syntax.string_of_term ctxt t ...
+ in ... end;
+
+
+ (* RIGHT *)
+
+ fun print_foo ctxt foo =
+ let
+ val string_of_term = Syntax.string_of_term ctxt;
+ fun print t = ... string_of_term t ...
+ in ... end;
+
+
+ (* WRONG *)
+
+ val string_of_term = Syntax.string_of_term;
+
+ fun print_foo ctxt foo =
+ let
+ fun aux t = ... string_of_term ctxt t ...
+ in ... end;
+
+ \end{verbatim}
+
+
+ \paragraph{Specific conventions.} Here are some important specific
+ name forms that occur frequently in the sources.
+
+ \begin{itemize}
+
+ \item A function that maps \verb|foo| to \verb|bar| is
+ called \verb|foo_to_bar| or \verb|bar_of_foo| (never
+ \verb|foo2bar|, \verb|bar_from_foo|, \verb|bar_for_foo|, or \verb|bar4foo|).
+
+ \item The name component \verb|legacy| means that the operation
+ is about to be discontinued soon.
+
+ \item The name component \verb|old| means that this is historic
+ material that might disappear at some later stage.
+
+ \item The name component \verb|global| means that this works
+ with the background theory instead of the regular local context
+ (\secref{sec:context}), sometimes for historical reasons, sometimes
+ due a genuine lack of locality of the concept involved, sometimes as
+ a fall-back for the lack of a proper context in the application
+ code. Whenever there is a non-global variant available, the
+ application should be migrated to use it with a proper local
+ context.
+
+ \item Variables of the main context types of the Isabelle/Isar
+ framework (\secref{sec:context} and \chref{ch:local-theory}) have
+ firm naming conventions to allow to visualize the their data flow
+ via plain regular expressions in the editor. In particular:
+
+ \begin{itemize}
+
+ \item theories are called \verb|thy|, rarely \verb|theory|
+ (never \verb|thry|)
+
+ \item proof contexts are called \verb|ctxt|, rarely \verb|context| (never \verb|ctx|)
+
+ \item generic contexts are called \verb|context|, rarely
+ \verb|ctxt|
+
+ \item local theories are called \verb|lthy|, unless there is an
+ implicit conversion to a general proof context (semantic super-type)
+
+ \end{itemize}
+
+ Variations with primed or decimal numbers are always possible, as
+ well as ``sematic prefixes'' like \verb|foo_thy| or \verb|bar_ctxt|, but the base conventions above need to be preserved.
+
+ \item The main logical entities (\secref{ch:logic}) also have
+ established naming convention:
+
+ \begin{itemize}
+
+ \item sorts are called \verb|S|
+
+ \item types are called \verb|T|, \verb|U|, or \verb|ty| (never \verb|t|)
+
+ \item terms are called \verb|t|, \verb|u|, or \verb|tm| (never \verb|trm|)
+
+ \item certified types are called \verb|cT|, rarely \verb|T|, with variants as for types
+
+ \item certified terms are called \verb|ct|, rarely \verb|t|, with variants as for terms
+
+ \item theorems are called \verb|th|, or \verb|thm|
+
+ \end{itemize}
+
+ Proper semantic names override these conventions completely. For
+ example, the left-hand side of an equation (as a term) can be called
+ \verb|lhs| (not \verb|lhs_tm|). Or a term that is treated
+ specifically as a variable can be called \verb|v| or \verb|x|.
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{General source layout%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Like any style guide, also this one should not be interpreted dogmatically, but
- with care and discernment. It consists of a collection of
- recommendations which have been turned out useful over long years of
- Isabelle system development and are supposed to support writing of readable
- and managable code. Special cases encourage derivations,
- as far as you know what you are doing.
- \footnote{This style guide is loosely based on
- \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}}
+The general Isabelle/ML source layout imitates regular
+ type-setting to some extent, augmented by the requirements for
+ deeply nested expressions that are commonplace in functional
+ programming.
+
+ \paragraph{Line length} is 80 characters according to ancient
+ standards, but we allow as much as 100 characters, not
+ more.\footnote{Readability requires to keep the beginning of a line
+ in view while watching its end. Modern wide-screen displays do not
+ change the way how the human brain works. As a rule of thumb,
+ sources need to be printable on plain paper.} The extra 20
+ characters acknowledge the space requirements due to qualified
+ library references in Isabelle/ML.
+
+ \paragraph{White-space} is used to emphasize the structure of
+ expressions, following mostly standard conventions for mathematical
+ typesetting, as can be seen in plain {\TeX} or {\LaTeX}. This
+ defines positioning of spaces for parentheses, punctuation, and
+ infixes as illustrated here:
+
+ \begin{verbatim}
+ val x = y + z * (a + b);
+ val pair = (a, b);
+ val record = {foo = 1, bar = 2};
+ \end{verbatim}
+
+ Lines are normally broken \emph{after} an infix operator or
+ punctuation character. For example:
+
+ \begin{verbatim}
+ val x =
+ a +
+ b +
+ c;
+
+ val tuple =
+ (a,
+ b,
+ c);
+ \end{verbatim}
+
+ Some special infixes (e.g.\ \verb||\verb,|,\verb|>|) work better at the
+ start of the line, but punctuation is always at the end.
+
+ Function application follows the tradition of \isa{{\isasymlambda}}-calculus,
+ not informal mathematics. For example: \verb|f a b| for a
+ curried function, or \verb|g (a, b)| for a tupled function.
+ Note that the space between \verb|g| and the pair \verb|(a, b)| follows the important principle of
+ \emph{compositionality}: the layout of \verb|g p| does not
+ change when \verb|p| is refined to a concrete pair.
+
+ \paragraph{Indentation} uses plain spaces, never hard
+ tabulators.\footnote{Tabulators were invented to move the carriage
+ of a type-writer to certain predefined positions. In software they
+ could be used as a primitive run-length compression of consecutive
+ spaces, but the precise result would depend on non-standardized
+ editor configuration.}
+
+ Each level of nesting is indented by 2 spaces, sometimes 1, very
+ rarely 4, never 8.
+
+ Indentation follows a simple logical format that only depends on the
+ nesting depth, not the accidental length of the text that initiates
+ a level of nesting. Example:
+
+ \begin{verbatim}
+ (* RIGHT *)
+
+ if b then
+ expr1_part1
+ expr1_part2
+ else
+ expr2_part1
+ expr2_part2
+
+
+ (* WRONG *)
+
+ if b then expr1_part1
+ expr1_part2
+ else expr2_part1
+ expr2_part2
+ \end{verbatim}
+
+ The second form has many problems: it assumes a fixed-width font
+ when viewing the sources, it uses more space on the line and thus
+ makes it hard to observe its strict length limit (working against
+ \emph{readability}), it requires extra editing to adapt the layout
+ to changes of the initial text (working against
+ \emph{maintainability}) etc.
+
+ \medskip For similar reasons, any kind of two-dimensional or tabular
+ layouts, ASCII-art with lines or boxes of stars etc. should be
+ avoided.
+
+ \paragraph{Complex expressions} consisting of multi-clausal function
+ definitions, \verb|case|, \verb|handle|, \verb|let|,
+ or combinations require special attention. The syntax of Standard
+ ML is a bit too ambitious in admitting too much variance that can
+ distort the meaning of the text.
+
+ Clauses of \verb|fun|, \verb|fn|, \verb|case|,
+ \verb|handle| get extra indentation to indicate the nesting
+ clearly. For example:
+
+ \begin{verbatim}
+ (* RIGHT *)
+
+ fun foo p1 =
+ expr1
+ | foo p2 =
+ expr2
+
+
+ (* WRONG *)
+
+ fun foo p1 =
+ expr1
+ | foo p2 =
+ expr2
+ \end{verbatim}
+
+ Body expressions consisting of \verb|case| or \verb|let|
+ require care to maintain compositionality, to prevent loss of
+ logical indentation where it is particularly imporant to see the
+ structure of the text later on. Example:
+
+ \begin{verbatim}
+ (* RIGHT *)
+
+ fun foo p1 =
+ (case e of
+ q1 => ...
+ | q2 => ...)
+ | foo p2 =
+ let
+ ...
+ in
+ ...
+ end
+
+
+ (* WRONG *)
+
+ fun foo p1 = case e of
+ q1 => ...
+ | q2 => ...
+ | foo p2 =
+ let
+ ...
+ in
+ ...
+ end
+ \end{verbatim}
+
+ Extra parentheses around \verb|case| expressions are optional,
+ but help to analyse the nesting easily based on simple string
+ matching in the editor.
+
+ \medskip There are two main exceptions to the overall principle of
+ compositionality in the layout of complex expressions.
+
+ \begin{enumerate}
+
+ \item \verb|if| expressions are iterated as if there would be
+ a multi-branch conditional in SML, e.g.
+
+ \begin{verbatim}
+ (* RIGHT *)
+
+ if b1 then e1
+ else if b2 then e2
+ else e3
+ \end{verbatim}
+
+ \item \verb|fn| abstractions are often layed-out as if they
+ would lack any structure by themselves. This traditional form is
+ motivated by the possibility to shift function arguments back and
+ forth wrt.\ additional combinators. For example:
+
+ \begin{verbatim}
+ (* RIGHT *)
+
+ fun foo x y = fold (fn z =>
+ expr)
+ \end{verbatim}
+
+ Here the visual appearance is that of three arguments \verb|x|,
+ \verb|y|, \verb|z|.
+
+ \end{enumerate}
+
+ Such weakly structured layout should be use with great care. Here
+ is a counter-example involving \verb|let| expressions:
+
+ \begin{verbatim}
+ (* WRONG *)
+
+ fun foo x = let
+ val y = ...
+ in ... end
+
+ fun foo x =
+ let
+ val y = ...
+ in ... end
+ \end{verbatim}
+
+ \medskip In general the source layout is meant to emphasize the
+ structure of complex language expressions, not to pretend that SML
+ had a completely different syntax (say that of Haskell or Java).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{SML embedded into Isabelle/Isar%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+ML and Isar are intertwined via an open-ended bootstrap
+ process that provides more and more programming facilities and
+ logical content in an alternating manner. Bootstrapping starts from
+ the raw environment of existing implementations of Standard ML
+ (mainly Poly/ML, but also SML/NJ).
+
+ Isabelle/Pure marks the point where the original ML toplevel is
+ superseded by the Isar toplevel that maintains a uniform environment
+ for arbitrary ML values (see also \secref{sec:context}). This
+ formal context holds logical entities as well as ML compiler
+ bindings, among many other things. Raw Standard ML is never
+ encountered again after the initial bootstrap of Isabelle/Pure.
+
+ Object-logics such as Isabelle/HOL are built within the
+ Isabelle/ML/Isar environment of Pure by introducing suitable
+ theories with associated ML text, either inlined or as separate
+ files. Thus Isabelle/HOL is defined as a regular user-space
+ application within the Isabelle framework. Further add-on tools can
+ be implemented in ML within the Isar context in the same manner: ML
+ is part of the regular user-space repertoire of Isabelle.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Isar ML commands%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The primary Isar source language provides various facilities
+ to open a ``window'' to the underlying ML compiler. Especially see
+ \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} and \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which work exactly the
+ same way, only the source text is provided via a file vs.\ inlined,
+ respectively. Apart from embedding ML into the main theory
+ definition like that, there are many more commands that refer to ML
+ source, such as \indexref{}{command}{setup}\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} or \indexref{}{command}{declaration}\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}.
+ An example of even more fine-grained embedding of ML into Isar is
+ the proof method \indexref{}{method}{tactic}\hyperlink{method.tactic}{\mbox{\isa{tactic}}}, which refines the pending goal state
+ via a given expression of type \verb|tactic|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following artificial example demonstrates some ML
+ toplevel declarations within the implicit Isar theory context. This
+ is regular functional programming without referring to logical
+ entities yet.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ fun\ factorial\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}\isanewline
+\ \ \ \ {\isacharbar}\ factorial\ n\ {\isacharequal}\ n\ {\isacharasterisk}\ factorial\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+Here the ML environment is really managed by Isabelle, i.e.\
+ the \verb|factorial| function is not yet accessible in the preceding
+ paragraph, nor in a different theory that is independent from the
+ current one in the import hierarchy.
+
+ Removing the above ML declaration from the source text will remove
+ any trace of this definition as expected. The Isabelle/ML toplevel
+ environment is managed in a \emph{stateless} way: unlike the raw ML
+ toplevel or similar command loops of Computer Algebra systems, there
+ are no global side-effects involved here.\footnote{Such a stateless
+ compilation environment is also a prerequisite for robust parallel
+ compilation within independent nodes of the implicit theory
+ development graph.}
+
+ \medskip The next example shows how to embed ML into Isar proofs.
+ Instead of \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} for theory mode, we use \indexref{}{command}{ML\_prf}\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} for proof mode. As illustrated below, its effect on the
+ ML environment is local to the whole proof body, while ignoring its
+ internal block structure.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ a\ {\isacharequal}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
+\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
+\ %
+\isamarkupcmt{Isar block structure ignored by ML environment%
+}
+\isanewline
+\ \ \ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ b\ {\isacharequal}\ a\ {\isacharplus}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
+\ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
+\ %
+\isamarkupcmt{Isar block structure ignored by ML environment%
+}
+\isanewline
+\ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ c\ {\isacharequal}\ b\ {\isacharplus}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+By side-stepping the normal scoping rules for Isar proof
+ blocks, embedded ML code can refer to the different contexts
+ explicitly, and manipulate corresponding entities, e.g.\ export a
+ fact from a block context.
+
+ \medskip Two further ML commands are useful in certain situations:
+ \indexref{}{command}{ML\_val}\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \indexref{}{command}{ML\_command}\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are both
+ \emph{diagnostic} in the sense that there is no effect on the
+ underlying environment, and can thus used anywhere (even outside a
+ theory). The examples below produce long strings of digits by
+ invoking \verb|factorial|: \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} already takes care of
+ printing the ML toplevel result, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent
+ so we produce an explicit output message.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharverbatimclose}\isanewline
+\isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\ writeln\ {\isacharparenleft}string{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isanewline
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharverbatimclose}\ \ \isanewline
+\ \ \isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\ writeln\ {\isacharparenleft}string{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Compile-time context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Whenever the ML compiler is invoked within Isabelle/Isar, the
+ formal context is passed as a thread-local reference variable. Thus
+ ML code may access the theory context during compilation, by reading
+ or writing the (local) theory under construction. Note that such
+ direct access to the compile-time context is rare; in practice it is
+ typically via some derived ML functions.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{ML\_Context.the\_generic\_context}\verb|ML_Context.the_generic_context: unit -> Context.generic| \\
+ \indexdef{}{ML}{Context.$>$$>$}\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
+ \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
+ \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
+ \end{mldecls}
\begin{description}
- \item[fundamental law of programming]
- Whenever writing code, keep in mind: A program is
- written once, modified ten times, and read
- hundred times. So simplify its writing,
- always keep future modifications in mind,
- and never jeopardize readability. Every second you hesitate
- to spend on making your code more clear you will
- have to spend ten times understanding what you have
- written later on.
+ \item \verb|ML_Context.the_generic_context ()| refers to the theory
+ context of the ML toplevel --- at compile time. ML code needs to
+ take care to refer to \verb|ML_Context.the_generic_context ()|
+ correctly. Recall that evaluation of a function body is delayed
+ until actual run-time.
+
+ \item \verb|Context.>>|~\isa{f} applies context transformation
+ \isa{f} to the implicit context of the ML toplevel.
- \item[white space matters]
- Treat white space in your code as if it determines
- the meaning of code.
+ \item \verb|bind_thms|~\isa{{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}} stores a list of
+ theorems produced in ML both in the (global) theory context and the
+ ML toplevel, associating it with the provided name. Theorems are
+ put into a global ``standard'' format before being stored.
- \begin{itemize}
+ \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
+ singleton theorem.
+
+ \end{description}
- \item The space bar is the easiest key to find on the keyboard,
- press it as often as necessary. \verb|2 + 2| is better
- than \verb|2+2|, likewise \verb|f (x, y)| is
- better than \verb|f(x,y)|.
+ It is very important to note that the above functions are really
+ restricted to the compile time, even though the ML compiler is
+ invoked at run-time. The majority of ML code either uses static
+ antiquotations (\secref{sec:ML-antiq}) or refers to the theory or
+ proof context at run-time, by explicit functional abstraction.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Antiquotations \label{sec:ML-antiq}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A very important consequence of embedding SML into Isar is the
+ concept of \emph{ML antiquotation}. First, the standard token
+ language of ML is augmented by special syntactic entities of the
+ following form:
- \item Restrict your lines to 80 characters. This will allow
- you to keep the beginning of a line in view while watching
- its end.\footnote{To acknowledge the lax practice of
- text editing these days, we tolerate as much as 100
- characters per line, but anything beyond 120 is not
- considered proper source text.}
-
- \item Ban tabulators; they are a context-sensitive formatting
- feature and likely to confuse anyone not using your favorite
- editor.\footnote{Some modern programming language even
- forbid tabulators altogether according to the formal syntax
- definition.}
-
- \item Get rid of trailing whitespace. Instead, do not
- suppress a trailing newline at the end of your files.
+ \indexouternonterm{antiquote}
+ \begin{rail}
+ antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym
+ ;
+ \end{rail}
- \item Choose a generally accepted style of indentation,
- then use it systematically throughout the whole
- application. An indentation of two spaces is appropriate.
- Avoid dangling indentation.
-
- \end{itemize}
+ Here \hyperlink{syntax.nameref}{\mbox{\isa{nameref}}} and \hyperlink{syntax.args}{\mbox{\isa{args}}} are regular outer syntax
+ categories. Note that attributes and proof methods use similar
+ syntax.
- \item[cut-and-paste succeeds over copy-and-paste]
- \emph{Never} copy-and-paste code when programming. If you
- need the same piece of code twice, introduce a
- reasonable auxiliary function (if there is no
- such function, very likely you got something wrong).
- Any copy-and-paste will turn out to be painful
- when something has to be changed later on.
+ \medskip A regular antiquotation \isa{{\isacharat}{\isacharbraceleft}name\ args{\isacharbraceright}} processes
+ its arguments by the usual means of the Isar source language, and
+ produces corresponding ML source text, either as literal
+ \emph{inline} text (e.g. \isa{{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}}) or abstract
+ \emph{value} (e.g. \isa{{\isacharat}{\isacharbraceleft}thm\ th{\isacharbraceright}}). This pre-compilation
+ scheme allows to refer to formal entities in a robust manner, with
+ proper static scoping and with some degree of logical checking of
+ small portions of the code.
- \item[comments]
- are a device which requires careful thinking before using
- it. The best comment for your code should be the code itself.
- Prefer efforts to write clear, understandable code
- over efforts to explain nasty code.
+ Special antiquotations like \isa{{\isacharat}{\isacharbraceleft}let\ {\isasymdots}{\isacharbraceright}} or \isa{{\isacharat}{\isacharbraceleft}note\ {\isasymdots}{\isacharbraceright}} augment the compilation context without generating code. The
+ non-ASCII braces \isa{{\isasymlbrace}} and \isa{{\isasymrbrace}} allow to delimit the
+ effect by introducing local blocks within the pre-compilation
+ environment.
- \item[functional programming is based on functions]
- Model things as abstract as appropriate. Avoid unnecessarrily
- concrete datatype representations. For example, consider a function
- taking some table data structure as argument and performing
- lookups on it. Instead of taking a table, it could likewise
- take just a lookup function. Accustom
- your way of coding to the level of expressiveness a functional
- programming language is giving onto you.
+ \medskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader
+ perspective on Isabelle/ML antiquotations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isatagmlantiq
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{ML antiquotation}{let}\hypertarget{ML antiquotation.let}{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+ \indexdef{}{ML antiquotation}{note}\hypertarget{ML antiquotation.note}{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+ \end{matharray}
- \item[tuples]
- are often in the way. When there is no striking argument
- to tuple function arguments, just write your function curried.
+ \begin{rail}
+ 'let' ((term + 'and') '=' term + 'and')
+ ;
+
+ 'note' (thmdef? thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{description}
- \item[telling names]
- Any name should tell its purpose as exactly as possible, while
- keeping its length to the absolutely necessary minimum. Always
- give the same name to function arguments which have the same
- meaning. Separate words by underscores (\verb|int_of_string|, not \verb|intOfString|).\footnote{Some
- recent tools for Emacs include special precautions to cope with
- bumpy names in \isa{camelCase}, e.g.\ for improved on-screen
- readability. It is easier to abstain from using such names in the
- first place.}
+ \item \isa{{\isacharat}{\isacharbraceleft}let\ p\ {\isacharequal}\ t{\isacharbraceright}} binds schematic variables in the
+ pattern \isa{p} by higher-order matching against the term \isa{t}. This is analogous to the regular \indexref{}{command}{let}\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} command
+ in the Isar proof language. The pre-compilation environment is
+ augmented by auxiliary term bindings, without emitting ML source.
+
+ \item \isa{{\isacharat}{\isacharbraceleft}note\ a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isacharbraceright}} recalls existing facts \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n}, binding the result as \isa{a}. This is analogous to
+ the regular \indexref{}{command}{note}\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}} command in the Isar proof language.
+ The pre-compilation environment is augmented by auxiliary fact
+ bindings, without emitting ML source.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Thread-safe programming%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following artificial example gives a first
+ impression about using the antiquotation elements introduced so far,
+ together with the basic \isa{{\isacharat}{\isacharbraceleft}thm{\isacharbraceright}} antiquotation defined
+ later.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ {\isaantiqopen}\isanewline
+\ \ \ \ %
+\isaantiq
+let\ {\isacharquery}t\ {\isacharequal}\ my{\isacharunderscore}term%
+\endisaantiq
+\isanewline
+\ \ \ \ %
+\isaantiq
+note\ my{\isacharunderscore}refl\ {\isacharequal}\ reflexive\ {\isacharbrackleft}of\ {\isacharquery}t{\isacharbrackright}%
+\endisaantiq
+\isanewline
+\ \ \ \ fun\ foo\ th\ {\isacharequal}\ Thm{\isachardot}transitive\ th\ %
+\isaantiq
+thm\ my{\isacharunderscore}refl%
+\endisaantiq
+\isanewline
+\ \ {\isaantiqclose}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+The extra block delimiters do not affect the compiled code itself, i.e.\
+ function \verb|foo| is available in the present context.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Canonical argument order \label{sec:canonical-argument-order}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Standard ML is a language in the tradition of \isa{{\isasymlambda}}-calculus and \emph{higher-order functional programming},
+ similar to OCaml, Haskell, or Isabelle/Pure and HOL as logical
+ languages. Getting acquainted with the native style of representing
+ functions in that setting can save a lot of extra boiler-plate of
+ redundant shuffling of arguments, auxiliary abstractions etc.
+
+ First of all, functions are usually \emph{curried}: the idea of
+ \isa{f} taking \isa{n} arguments of type \isa{{\isasymtau}\isactrlsub i} (for
+ \isa{i\ {\isasymin}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ n{\isacharbraceright}}) with result \isa{{\isasymtau}} is represented by
+ the iterated function space \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymdots}\ {\isasymrightarrow}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}. This is
+ isomorphic to the encoding via tuples \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymtimes}\ {\isasymdots}\ {\isasymtimes}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}, but
+ the curried version fits more smoothly into the basic
+ calculus.\footnote{The difference is even more significant in
+ higher-order logic, because additional the redundant tuple structure
+ needs to be accommodated by formal reasoning.}
+
+ Currying gives some flexiblity due to \emph{partial application}. A
+ function \isa{f{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymtau}\isactrlbsub {\isadigit{2}}\isactrlesub \ {\isasymrightarrow}\ {\isasymtau}} can be applied to \isa{x{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}}
+ and the remaining \isa{{\isacharparenleft}f\ x{\isacharparenright}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{2}}\ {\isasymrightarrow}\ {\isasymtau}} passed to other functions
+ etc. How well this works in practice depends on the order of
+ arguments. In the worst case, arguments are arranged erratically,
+ and using a function in a certain situation always requires some
+ glue code. Thus we would get exponentially many oppurtunities to
+ decorate the code with meaningless permutations of arguments.
+
+ This can be avoided by \emph{canonical argument order}, which
+ observes certain standard patterns of function definitions and
+ minimizes adhoc permutations in their application. In Isabelle/ML,
+ large portions of non-trivial source code are written without ever
+ using the infamous function \isa{swap{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymtimes}\ {\isasymalpha}} or the
+ combinator \isa{C{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}\ {\isasymrightarrow}\ {\isacharparenleft}{\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}}, which is not even
+ defined in our library.
+
+ \medskip The basic idea is that arguments that vary less are moved
+ further to the left than those that vary more. Two particularly
+ important categories of functions are \emph{selectors} and
+ \emph{updates}.
+
+ The subsequent scheme is based on a hypothetical set-like container
+ of type \isa{{\isasymbeta}} that manages elements of type \isa{{\isasymalpha}}. Both
+ the names and types of the associated operations are canonical for
+ Isabelle/ML.
+
+ \medskip
+ \begin{tabular}{ll}
+ kind & canonical name and type \\\hline
+ selector & \isa{member{\isacharcolon}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ bool} \\
+ update & \isa{insert{\isacharcolon}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} \\
+ \end{tabular}
+ \medskip
+
+ Given a container \isa{B{\isacharcolon}\ {\isasymbeta}}, the partially applied \isa{member\ B} is a predicate over elements \isa{{\isasymalpha}\ {\isasymrightarrow}\ bool}, and
+ thus represents the intended denotation directly. It is customary
+ to pass the abstract predicate to further operations, not the
+ concrete container. The argument order makes it easy to use other
+ combinators: \isa{forall\ {\isacharparenleft}member\ B{\isacharparenright}\ list} will check a list of
+ elements for membership in \isa{B} etc. Often the explicit
+ \isa{list} is pointless and can be contracted in the application
+ \isa{forall\ {\isacharparenleft}member\ B{\isacharparenright}} to get directly a predicate again.
+
+ The update operation naturally ``varies'' the container, so it moves
+ to the right: \isa{insert\ a} is a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} to
+ insert a value \isa{a}. These can be composed naturally as
+ follows: \isa{insert\ c\ {\isasymcirc}\ insert\ b\ {\isasymcirc}\ insert\ a}. This works well,
+ apart from some awkwardness due to conventional mathematical
+ function composition, which can be easily amended as follows.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Forward application and composition%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Regular function application and infix notation works best for
+ relatively deeply structured expressions, e.g.\ \isa{h\ {\isacharparenleft}f\ x\ y\ {\isacharplus}\ g\ z{\isacharparenright}}. The important special case if \emph{linear transformation}
+ applies a cascade of functions as follows: \isa{f\isactrlsub n\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}f\isactrlsub {\isadigit{1}}\ x{\isacharparenright}{\isacharparenright}}.
+ This becomes hard to read and maintain if the functions are
+ themselves complex expressions. The notation can be significantly
+ improved by introducing \emph{forward} versions of application and
+ composition as follows:
+
+ \medskip
+ \begin{tabular}{lll}
+ \isa{x\ {\isacharbar}{\isachargreater}\ f} & \isa{{\isasymequiv}} & \isa{f\ x} \\
+ \isa{f\ {\isacharhash}{\isachargreater}\ g} & \isa{{\isasymequiv}} & \isa{x\ {\isacharbar}{\isachargreater}\ f\ {\isacharbar}{\isachargreater}\ g} \\
+ \end{tabular}
+ \medskip
+
+ This enables to write conveniently \isa{x\ {\isacharbar}{\isachargreater}\ f\isactrlsub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\isactrlsub n} or
+ \isa{f\isactrlsub {\isadigit{1}}\ {\isacharhash}{\isachargreater}\ {\isasymdots}\ {\isacharhash}{\isachargreater}\ f\isactrlsub n} for its functional abstraction over \isa{x}.
+
+ \medskip There is an additional set of combinators to accommodate
+ multiple results (via pairs) that are passed on as multiple
+ arguments (via currying).
+
+ \medskip
+ \begin{tabular}{lll}
+ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharbar}{\isacharminus}{\isachargreater}\ f} & \isa{{\isasymequiv}} & \isa{f\ x\ y} \\
+ \isa{f\ {\isacharhash}{\isacharminus}{\isachargreater}\ g} & \isa{{\isasymequiv}} & \isa{x\ {\isacharbar}{\isachargreater}\ f\ {\isacharbar}{\isacharminus}{\isachargreater}\ g} \\
+ \end{tabular}
+ \medskip%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{$\mid$$>$}\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
+ \indexdef{}{ML}{$\mid$-$>$}\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
+ \indexdef{}{ML}{\#$>$}\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
+ \indexdef{}{ML}{\#-$>$}\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
+ \end{mldecls}
+
+ %FIXME description!?%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Canonical iteration%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+As explained above, a function \isa{f{\isacharcolon}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} can be
+ understood as update on a configuration of type \isa{{\isasymbeta}} that is
+ parametrized by arguments of type \isa{{\isasymalpha}}. Given \isa{a{\isacharcolon}\ {\isasymalpha}}
+ the partial application \isa{{\isacharparenleft}f\ a{\isacharparenright}{\isacharcolon}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} operates
+ homogeneously on \isa{{\isasymbeta}}. This can be iterated naturally over a
+ list of parameters \isa{{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isacharbrackright}} as \isa{f\ a\isactrlsub {\isadigit{1}}\ {\isacharhash}{\isachargreater}\ {\isasymdots}\ {\isacharhash}{\isachargreater}\ f\ a\isactrlbsub n\isactrlesub \isactrlbsub \isactrlesub }. The latter expression is again a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}}.
+ It can be applied to an initial configuration \isa{b{\isacharcolon}\ {\isasymbeta}} to
+ start the iteration over the given list of arguments: each \isa{a} in \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} is applied consecutively by updating a
+ cumulative configuration.
+
+ The \isa{fold} combinator in Isabelle/ML lifts a function \isa{f} as above to its iterated version over a list of arguments.
+ Lifting can be repeated, e.g.\ \isa{{\isacharparenleft}fold\ {\isasymcirc}\ fold{\isacharparenright}\ f} iterates
+ over a list of lists as expected.
+
+ The variant \isa{fold{\isacharunderscore}rev} works inside-out over the list of
+ arguments, such that \isa{fold{\isacharunderscore}rev\ f\ {\isasymequiv}\ fold\ f\ {\isasymcirc}\ rev} holds.
+
+ The \isa{fold{\isacharunderscore}map} combinator essentially performs \isa{fold} and \isa{map} simultaneously: each application of \isa{f} produces an updated configuration together with a side-result;
+ the iteration collects all such side-results as a separate list.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
+ \indexdef{}{ML}{fold\_rev}\verb|fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
+ \indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|fold|~\isa{f} lifts the parametrized update function
+ \isa{f} to a list of parameters.
+
+ \item \verb|fold_rev|~\isa{f} is similar to \verb|fold|~\isa{f}, but works inside-out.
+
+ \item \verb|fold_map|~\isa{f} lifts the parametrized update
+ function \isa{f} (with side-result) to a list of parameters and
+ cumulative side-results.
+
+ \end{description}
+
+ \begin{warn}
+ The literature on functional programming provides a multitude of
+ combinators called \isa{foldl}, \isa{foldr} etc. SML97
+ provides its own variations as \verb|List.foldl| and \verb|List.foldr|, while the classic Isabelle library still has the
+ slightly more convenient historic \verb|Library.foldl| and \verb|Library.foldr|. To avoid further confusion, all of this should be
+ ignored, and \verb|fold| (or \verb|fold_rev|) used exclusively.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example shows how to fill a text buffer
+ incrementally by adding strings, either individually or from a given
+ list.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ s\ {\isacharequal}\isanewline
+\ \ \ \ Buffer{\isachardot}empty\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}add\ {\isachardoublequote}digits{\isacharcolon}\ {\isachardoublequote}\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ fold\ {\isacharparenleft}Buffer{\isachardot}add\ o\ string{\isacharunderscore}of{\isacharunderscore}int{\isacharparenright}\ {\isacharparenleft}{\isadigit{0}}\ upto\ {\isadigit{9}}{\isacharparenright}\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}content{\isacharsemicolon}\isanewline
+\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}s\ {\isacharequal}\ {\isachardoublequote}digits{\isacharcolon}\ {\isadigit{0}}{\isadigit{1}}{\isadigit{2}}{\isadigit{3}}{\isadigit{4}}{\isadigit{5}}{\isadigit{6}}{\isadigit{7}}{\isadigit{8}}{\isadigit{9}}{\isachardoublequote}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+Note how \verb|fold (Buffer.add o string_of_int)| above saves
+ an extra \verb|map| over the given list. This kind of peephole
+ optimization reduces both the code size and the tree structures in
+ memory (``deforestation''), but requires some practice to read and
+ write it fluently.
+
+ \medskip The next example elaborates this idea and demonstrates fast
+ accumulation of tree content using a text buffer.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ datatype\ tree\ {\isacharequal}\ Text\ of\ string\ {\isacharbar}\ Elem\ of\ string\ {\isacharasterisk}\ tree\ list{\isacharsemicolon}\isanewline
+\isanewline
+\ \ fun\ slow{\isacharunderscore}content\ {\isacharparenleft}Text\ txt{\isacharparenright}\ {\isacharequal}\ txt\isanewline
+\ \ \ \ {\isacharbar}\ slow{\isacharunderscore}content\ {\isacharparenleft}Elem\ {\isacharparenleft}name{\isacharcomma}\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharless}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}\ {\isacharcircum}\isanewline
+\ \ \ \ \ \ \ \ implode\ {\isacharparenleft}map\ slow{\isacharunderscore}content\ ts{\isacharparenright}\ {\isacharcircum}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharless}{\isacharslash}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}\isanewline
+\isanewline
+\ \ fun\ add{\isacharunderscore}content\ {\isacharparenleft}Text\ txt{\isacharparenright}\ {\isacharequal}\ Buffer{\isachardot}add\ txt\isanewline
+\ \ \ \ {\isacharbar}\ add{\isacharunderscore}content\ {\isacharparenleft}Elem\ {\isacharparenleft}name{\isacharcomma}\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ Buffer{\isachardot}add\ {\isacharparenleft}{\isachardoublequote}{\isacharless}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}{\isacharparenright}\ {\isacharhash}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ fold\ add{\isacharunderscore}content\ ts\ {\isacharhash}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Buffer{\isachardot}add\ {\isacharparenleft}{\isachardoublequote}{\isacharless}{\isacharslash}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ fun\ fast{\isacharunderscore}content\ tree\ {\isacharequal}\isanewline
+\ \ \ \ Buffer{\isachardot}empty\ {\isacharbar}{\isachargreater}\ add{\isacharunderscore}content\ tree\ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}content{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+The slow part of \verb|slow_content| is the \verb|implode| of
+ the recursive results, because it copies previously produced strings
+ afresh.
+
+ The incremental \verb|add_content| avoids this by operating on a
+ buffer that is passed-through in a linear fashion. Using \verb|#>| and contraction over the actual \verb|Buffer.T| argument
+ saves some additional boiler-plate, but requires again some
+ practice. Of course, the two \verb|Buffer.add| invocations with
+ concatenated strings could have been split into smaller parts, but
+ this would have obfuscated the source without making a big
+ difference in allocations. Here we have done some
+ peephole-optimization for the sake of readability.
+
+ Another benefit of \verb|add_content| is its ``open'' form as a
+ function on \verb|Buffer.T| that can be continued in further
+ linear transformations, folding etc. Thus it is more compositional
+ than the naive \verb|slow_content|. As a realistic example, compare
+ the slightly old-style \verb|Term.maxidx_of_term: term -> int| with
+ the newer \verb|Term.maxidx_term: term -> int -> int| in
+ Isabelle/Pure.
+
+ Note that \verb|fast_content| above is only defined for completeness
+ of the example. In many practical situations, it is customary to
+ defined the incremental \verb|add_content| only and leave the
+ initialization and termination to the concrete application by the
+ user.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Message output channels \label{sec:message-channels}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle provides output channels for different kinds of
+ messages: regular output, high-volume tracing information, warnings,
+ and errors.
+
+ Depending on the user interface involved, these messages may appear
+ in different text styles or colours. The standard output for
+ terminal sessions prefixes each line of warnings by \verb|###| and errors by \verb|***|, but leaves anything else
+ unchanged.
+
+ Messages are associated with the transaction context of the running
+ Isar command. This enables the front-end to manage commands and
+ resulting messages together. For example, after deleting a command
+ from a given theory document version, the corresponding message
+ output can be retracted from the display.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{writeln}\verb|writeln: string -> unit| \\
+ \indexdef{}{ML}{tracing}\verb|tracing: string -> unit| \\
+ \indexdef{}{ML}{warning}\verb|warning: string -> unit| \\
+ \indexdef{}{ML}{error}\verb|error: string -> 'a| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|writeln|~\isa{text} outputs \isa{text} as regular
+ message. This is the primary message output operation of Isabelle
+ and should be used by default.
+
+ \item \verb|tracing|~\isa{text} outputs \isa{text} as special
+ tracing message, indicating potential high-volume output to the
+ front-end (hundreds or thousands of messages issued by a single
+ command). The idea is to allow the user-interface to downgrade the
+ quality of message display to achieve higher throughput.
+
+ Note that the user might have to take special actions to see tracing
+ output, e.g.\ switch to a different output window. So this channel
+ should not be used for regular output.
+
+ \item \verb|warning|~\isa{text} outputs \isa{text} as
+ warning, which typically means some extra emphasis on the front-end
+ side (color highlighting, icon).
+
+ \item \verb|error|~\isa{text} raises exception \verb|ERROR|~\isa{text} and thus lets the Isar toplevel print \isa{text} on the
+ error channel, which typically means some extra emphasis on the
+ front-end side (color highlighting, icon).
+
+ This assumes that the exception is not handled before the command
+ terminates. Handling exception \verb|ERROR|~\isa{text} is a
+ perfectly legal alternative: it means that the error is absorbed
+ without any message output.
+
+ \begin{warn}
+ The actual error channel is accessed via \verb|Output.error_msg|, but
+ the interaction protocol of Proof~General \emph{crashes} if that
+ function is used in regular ML code: error output and toplevel
+ command failure always need to coincide here.
+ \end{warn}
+
+ \end{description}
+
+ \begin{warn}
+ Regular Isabelle/ML code should output messages exclusively by the
+ official channels. Using raw I/O on \emph{stdout} or \emph{stderr}
+ instead (e.g.\ via \verb|TextIO.output|) is apt to cause problems in
+ the presence of parallel and asynchronous processing of Isabelle
+ theories. Such raw output might be displayed by the front-end in
+ some system console log, with a low chance that the user will ever
+ see it. Moreover, as a genuine side-effect on global process
+ channels, there is no proper way to retract output when Isar command
+ transactions are reset.
+ \end{warn}
+
+ \begin{warn}
+ The message channels should be used in a message-oriented manner.
+ This means that multi-line output that logically belongs together
+ needs to be issued by a \emph{single} invocation of \verb|writeln|
+ etc. with the functional concatenation of all message constituents.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example demonstrates a multi-line
+ warning. Note that in some situations the user sees only the first
+ line, so the most important point should be made first.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ warning\ {\isacharparenleft}cat{\isacharunderscore}lines\isanewline
+\ \ \ {\isacharbrackleft}{\isachardoublequote}Beware\ the\ Jabberwock{\isacharcomma}\ my\ son{\isacharbang}{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}The\ jaws\ that\ bite{\isacharcomma}\ the\ claws\ that\ catch{\isacharbang}{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}Beware\ the\ Jubjub\ Bird{\isacharcomma}\ and\ shun{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}The\ frumious\ Bandersnatch{\isacharbang}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isamarkupsection{Exceptions \label{sec:exceptions}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Recent versions of Poly/ML (5.2.1 or later) support robust
- multithreaded execution, based on native operating system threads of
- the underlying platform. Thus threads will actually be executed in
- parallel on multi-core systems. A speedup-factor of approximately
- 1.5--3 can be expected on a regular 4-core machine.\footnote{There
- is some inherent limitation of the speedup factor due to garbage
- collection, which is still sequential. It helps to provide initial
- heap space generously, using the \texttt{-H} option of Poly/ML.}
- Threads also help to organize advanced operations of the system,
- with explicit communication between sub-components, real-time
- conditions, time-outs etc.
+The Standard ML semantics of strict functional evaluation
+ together with exceptions is rather well defined, but some delicate
+ points need to be observed to avoid that ML programs go wrong
+ despite static type-checking. Exceptions in Isabelle/ML are
+ subsequently categorized as follows.
+
+ \paragraph{Regular user errors.} These are meant to provide
+ informative feedback about malformed input etc.
+
+ The \emph{error} function raises the corresponding \emph{ERROR}
+ exception, with a plain text message as argument. \emph{ERROR}
+ exceptions can be handled internally, in order to be ignored, turned
+ into other exceptions, or cascaded by appending messages. If the
+ corresponding Isabelle/Isar command terminates with an \emph{ERROR}
+ exception state, the toplevel will print the result on the error
+ channel (see \secref{sec:message-channels}).
+
+ It is considered bad style to refer to internal function names or
+ values in ML source notation in user error messages.
+
+ Grammatical correctness of error messages can be improved by
+ \emph{omitting} final punctuation: messages are often concatenated
+ or put into a larger context (e.g.\ augmented with source position).
+ By not insisting in the final word at the origin of the error, the
+ system can perform its administrative tasks more easily and
+ robustly.
+
+ \paragraph{Program failures.} There is a handful of standard
+ exceptions that indicate general failure situations, or failures of
+ core operations on logical entities (types, terms, theorems,
+ theories, see \chref{ch:logic}).
+
+ These exceptions indicate a genuine breakdown of the program, so the
+ main purpose is to determine quickly what has happened where.
+ Traditionally, the (short) exception message would include the name
+ of an ML function, although this no longer necessary, because the ML
+ runtime system prints a detailed source position of the
+ corresponding \verb|raise| keyword.
+
+ \medskip User modules can always introduce their own custom
+ exceptions locally, e.g.\ to organize internal failures robustly
+ without overlapping with existing exceptions. Exceptions that are
+ exposed in module signatures require extra care, though, and should
+ \emph{not} be introduced by default. Surprise by end-users or ML
+ users of a module can be often minimized by using plain user errors.
+
+ \paragraph{Interrupts.} These indicate arbitrary system events:
+ both the ML runtime system and the Isabelle/ML infrastructure signal
+ various exceptional situations by raising the special
+ \emph{Interrupt} exception in user code.
+
+ This is the one and only way that physical events can intrude an
+ Isabelle/ML program. Such an interrupt can mean out-of-memory,
+ stack overflow, timeout, internal signaling of threads, or the user
+ producing a console interrupt manually etc. An Isabelle/ML program
+ that intercepts interrupts becomes dependent on physical effects of
+ the environment. Even worse, exception handling patterns that are
+ too general by accident, e.g.\ by mispelled exception constructors,
+ will cover interrupts unintentionally, and thus render the program
+ semantics ill-defined.
+
+ Note that the Interrupt exception dates back to the original SML90
+ language definition. It was excluded from the SML97 version to
+ avoid its malign impact on ML program semantics, but without
+ providing a viable alternative. Isabelle/ML recovers physical
+ interruptibility (which an indispensable tool to implement managed
+ evaluation of Isar command transactions), but requires user code to
+ be strictly transparent wrt.\ interrupts.
+
+ \begin{warn}
+ Isabelle/ML user code needs to terminate promptly on interruption,
+ without guessing at its meaning to the system infrastructure.
+ Temporary handling of interrupts for cleanup of global resources
+ etc.\ needs to be followed immediately by re-raising of the original
+ exception.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
+ \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
+ \indexdef{}{ML}{ERROR}\verb|ERROR: string -> exn| \\
+ \indexdef{}{ML}{Fail}\verb|Fail: string -> exn| \\
+ \indexdef{}{ML}{Exn.is\_interrupt}\verb|Exn.is_interrupt: exn -> bool| \\
+ \indexdef{}{ML}{reraise}\verb|reraise: exn -> 'a| \\
+ \indexdef{}{ML}{exception\_trace}\verb|exception_trace: (unit -> 'a) -> 'a| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|try|~\isa{f\ x} makes the partiality of evaluating
+ \isa{f\ x} explicit via the option datatype. Interrupts are
+ \emph{not} handled here, i.e.\ this form serves as safe replacement
+ for the \emph{unsafe} version \verb|(SOME|~\isa{f\ x}~\verb|handle _ => NONE)| that is occasionally seen in
+ books about SML.
+
+ \item \verb|can| is similar to \verb|try| with more abstract result.
+
+ \item \verb|ERROR|~\isa{msg} represents user errors; this
+ exception is always raised via the \verb|error| function (see
+ \secref{sec:message-channels}).
+
+ \item \verb|Fail|~\isa{msg} represents general program failures.
+
+ \item \verb|Exn.is_interrupt| identifies interrupts robustly, without
+ mentioning concrete exception constructors in user code. Handled
+ interrupts need to be re-raised promptly!
+
+ \item \verb|reraise|~\isa{exn} raises exception \isa{exn}
+ while preserving its implicit position information (if possible,
+ depending on the ML platform).
+
+ \item \verb|exception_trace|~\verb|(fn _ =>|~\isa{e}\verb|)| evaluates expression \isa{e} while printing
+ a full trace of its stack of nested exceptions (if possible,
+ depending on the ML platform).\footnote{In various versions of
+ Poly/ML the trace will appear on raw stdout of the Isabelle
+ process.}
+
+ Inserting \verb|exception_trace| into ML code temporarily is useful
+ for debugging, but not suitable for production code.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isatagmlantiq
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{ML antiquotation}{assert}\hypertarget{ML antiquotation.assert}{\hyperlink{ML antiquotation.assert}{\mbox{\isa{assert}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+ \end{matharray}
+
+ \begin{description}
+
+ \item \isa{{\isacharat}{\isacharbraceleft}assert{\isacharbraceright}} inlines a function \isa{bool\ {\isasymRightarrow}\ unit}
+ that raises \verb|Fail| if the argument is \verb|false|. Due to
+ inlining the source position of failed assertions is included in the
+ error output.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isamarkupsection{Basic data types%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The basis library proposal of SML97 need to be treated with
+ caution. Many of its operations simply do not fit with important
+ Isabelle/ML conventions (like ``canonical argument order'', see
+ \secref{sec:canonical-argument-order}), others can cause serious
+ problems with the parallel evaluation model of Isabelle/ML (such as
+ \verb|TextIO.print| or \verb|OS.Process.system|).
+
+ Subsequently we give a brief overview of important operations on
+ basic ML data types.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Characters%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML type}{char}\verb|type char| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item Type \verb|char| is \emph{not} used. The smallest textual
+ unit in Isabelle is represented a ``symbol'' (see
+ \secref{sec:symbols}).
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Integers%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML type}{int}\verb|type int| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item Type \verb|int| represents regular mathematical integers,
+ which are \emph{unbounded}. Overflow never happens in
+ practice.\footnote{The size limit for integer bit patterns in memory
+ is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.}
+ This works uniformly for all supported ML platforms (Poly/ML and
+ SML/NJ).
+
+ Literal integers in ML text (e.g.\ \verb|123456789012345678901234567890|) are forced to be of this one true
+ integer type --- overloading of SML97 is disabled.
+
+ Structure \verb|IntInf| of SML97 is obsolete, always use
+ \verb|Int|. Structure \verb|Integer| in \hyperlink{file.~~/src/Pure/General/integer.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}integer{\isachardot}ML}}}} provides some additional
+ operations.
- Threads lack the memory protection of separate processes, and
- operate concurrently on shared heap memory. This has the advantage
- that results of independent computations are immediately available
- to other threads, without requiring untyped character streams,
- awkward serialization etc.
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Options%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{Option.map}\verb|Option.map: ('a -> 'b) -> 'a option -> 'b option| \\
+ \indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
+ \indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
+ \indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
+ \indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
+ \indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
+ \indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
+ \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\begin{isamarkuptext}%
+Apart from \verb|Option.map| most operations defined in
+ structure \verb|Option| are alien to Isabelle/ML. The
+ operations shown above are defined in \hyperlink{file.~~/src/Pure/General/basics.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}basics{\isachardot}ML}}}}, among others.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Lists are ubiquitous in ML as simple and light-weight
+ ``collections'' for many everyday programming tasks. Isabelle/ML
+ provides important additions and improvements over operations that
+ are predefined in the SML97 library.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{cons}\verb|cons: 'a -> 'a list -> 'a list| \\
+ \indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
+ \indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
+ \indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
+ \indexdef{}{ML}{update}\verb|update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|cons|~\isa{x\ xs} evaluates to \isa{x\ {\isacharcolon}{\isacharcolon}\ xs}.
+
+ Tupled infix operators are a historical accident in Standard ML.
+ The curried \verb|cons| amends this, but it should be only used when
+ partial application is required.
+
+ \item \verb|member|, \verb|insert|, \verb|remove|, \verb|update| treat
+ lists as a set-like container that maintains the order of elements.
+ See \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}library{\isachardot}ML}}}} for the full specifications
+ (written in ML). There are some further derived operations like
+ \verb|union| or \verb|inter|.
+
+ Note that \verb|insert| is conservative about elements that are
+ already a \verb|member| of the list, while \verb|update| ensures that
+ the last entry is always put in front. The latter discipline is
+ often more appropriate in declarations of context data
+ (\secref{sec:context-data}) that are issued by the user in Isar
+ source: more recent declarations normally take precedence over
+ earlier ones.
- On the other hand, some programming guidelines need to be observed
- in order to make unprotected parallelism work out smoothly. While
- the ML system implementation is responsible to maintain basic
- integrity of the representation of ML values in memory, the
- application programmer needs to ensure that multithreaded execution
- does not break the intended semantics.
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+Using canonical \verb|fold| together with canonical \verb|cons|, or similar standard operations, alternates the orientation of
+ data. The is quite natural and should not altered forcible by
+ inserting extra applications \verb|rev|. The alternative \verb|fold_rev| can be used in the relatively few situations, where
+ alternation should be prevented.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ items\ {\isacharequal}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{8}}{\isacharcomma}\ {\isadigit{9}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{0}}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isacharequal}\ fold\ cons\ items\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{1}}\ {\isacharequal}\ rev\ items{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{2}}\ {\isacharequal}\ fold{\isacharunderscore}rev\ cons\ items\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{2}}\ {\isacharequal}\ items{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+The subsequent example demonstrates how to \emph{merge} two
+ lists in a natural way.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ fun\ merge{\isacharunderscore}lists\ eq\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}\ {\isacharequal}\ fold{\isacharunderscore}rev\ {\isacharparenleft}insert\ eq{\isacharparenright}\ ys\ xs{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+Here the first list is treated conservatively: only the new
+ elements from the second list are inserted. The inside-out order of
+ insertion via \verb|fold_rev| attempts to preserve the order of
+ elements in the result.
+
+ This way of merging lists is typical for context data
+ (\secref{sec:context-data}). See also \verb|merge| as defined in
+ \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}library{\isachardot}ML}}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Association lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The operations for association lists interpret a concrete list
+ of pairs as a finite function from keys to values. Redundant
+ representations with multiple occurrences of the same key are
+ implicitly normalized: lookup and update only take the first
+ occurrence into account.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
+ \indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
+ \indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|AList.lookup|, \verb|AList.defined|, \verb|AList.update|
+ implement the main ``framework operations'' for mappings in
+ Isabelle/ML, with standard conventions for names and types.
+
+ Note that a function called \isa{lookup} is obliged to express its
+ partiality via an explicit option element. There is no choice to
+ raise an exception, without changing the name to something like
+ \isa{the{\isacharunderscore}element} or \isa{get}.
+
+ The \isa{defined} operation is essentially a contraction of \verb|is_some| and \isa{lookup}, but this is sufficiently frequent to
+ justify its independent existence. This also gives the
+ implementation some opportunity for peep-hole optimization.
+
+ \end{description}
- \medskip \paragraph{Critical shared resources.} Actually only those
- parts outside the purely functional world of ML are critical. In
- particular, this covers
+ Association lists are adequate as simple and light-weight
+ implementation of finite mappings in many practical situations. A
+ more heavy-duty table structure is defined in \hyperlink{file.~~/src/Pure/General/table.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}table{\isachardot}ML}}}}; that version scales easily to
+ thousands or millions of elements.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Unsynchronized references%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML type}{Unsynchronized.ref}\verb|type 'a Unsynchronized.ref| \\
+ \indexdef{}{ML}{Unsynchronized.ref}\verb|Unsynchronized.ref: 'a -> 'a Unsynchronized.ref| \\
+ \indexdef{}{ML}{!}\verb|! : 'a Unsynchronized.ref -> 'a| \\
+ \indexdef{}{ML}{:=}\verb|op := : 'a Unsynchronized.ref * 'a -> unit| \\
+ \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\begin{isamarkuptext}%
+Due to ubiquitous parallelism in Isabelle/ML (see also
+ \secref{sec:multi-threading}), the mutable reference cells of
+ Standard ML are notorious for causing problems. In a highly
+ parallel system, both correctness \emph{and} performance are easily
+ degraded when using mutable data.
+
+ The unwieldy name of \verb|Unsynchronized.ref| for the constructor
+ for references in Isabelle/ML emphasizes the inconveniences caused by
+ mutability. Existing operations \verb|!| and \verb|op :=| are
+ unchanged, but should be used with special precautions, say in a
+ strictly local situation that is guaranteed to be restricted to
+ sequential evaluation --- now and in the future.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Thread-safe programming \label{sec:multi-threading}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Multi-threaded execution has become an everyday reality in
+ Isabelle since Poly/ML 5.2.1 and Isabelle2008. Isabelle/ML provides
+ implicit and explicit parallelism by default, and there is no way
+ for user-space tools to ``opt out''. ML programs that are purely
+ functional, output messages only via the official channels
+ (\secref{sec:message-channels}), and do not intercept interrupts
+ (\secref{sec:exceptions}) can participate in the multi-threaded
+ environment immediately without further ado.
+
+ More ambitious tools with more fine-grained interaction with the
+ environment need to observe the principles explained below.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Multi-threading with shared memory%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Multiple threads help to organize advanced operations of the
+ system, such as real-time conditions on command transactions,
+ sub-components with explicit communication, general asynchronous
+ interaction etc. Moreover, parallel evaluation is a prerequisite to
+ make adequate use of the CPU resources that are available on
+ multi-core systems.\footnote{Multi-core computing does not mean that
+ there are ``spare cycles'' to be wasted. It means that the
+ continued exponential speedup of CPU performance due to ``Moore's
+ Law'' follows different rules: clock frequency has reached its peak
+ around 2005, and applications need to be parallelized in order to
+ avoid a perceived loss of performance. See also
+ \cite{Sutter:2005}.}
+
+ Isabelle/Isar exploits the inherent structure of theories and proofs
+ to support \emph{implicit parallelism} to a large extent. LCF-style
+ theorem provides almost ideal conditions for that; see also
+ \cite{Wenzel:2009}. This means, significant parts of theory and
+ proof checking is parallelized by default. A maximum speedup-factor
+ of 3.0 on 4 cores and 5.0 on 8 cores can be
+ expected.\footnote{Further scalability is limited due to garbage
+ collection, which is still sequential in Poly/ML 5.2/5.3/5.4. It
+ helps to provide initial heap space generously, using the
+ \texttt{-H} option. Initial heap size needs to be scaled-up
+ together with the number of CPU cores: approximately 1--2\,GB per
+ core..}
+
+ \medskip ML threads lack the memory protection of separate
+ processes, and operate concurrently on shared heap memory. This has
+ the advantage that results of independent computations are
+ immediately available to other threads: abstract values can be
+ passed between threads without copying or awkward serialization that
+ is typically required for explicit message passing between separate
+ processes.
+
+ To make shared-memory multi-threading work robustly and efficiently,
+ some programming guidelines need to be observed. While the ML
+ system is responsible to maintain basic integrity of the
+ representation of ML values in memory, the application programmer
+ needs to ensure that multi-threaded execution does not break the
+ intended semantics.
+
+ \begin{warn}
+ To participate in implicit parallelism, tools need to be
+ thread-safe. A single ill-behaved tool can affect the stability and
+ performance of the whole system.
+ \end{warn}
+
+ Apart from observing the principles of thread-safeness passively,
+ advanced tools may also exploit parallelism actively, e.g.\ by using
+ ``future values'' (\secref{sec:futures}) or the more basic library
+ functions for parallel list operations (\secref{sec:parlist}).
+
+ \begin{warn}
+ Parallel computing resources are managed centrally by the
+ Isabelle/ML infrastructure. User programs must not fork their own
+ ML threads to perform computations.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Critical shared resources%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Thread-safeness is mainly concerned about concurrent
+ read/write access to shared resources, which are outside the purely
+ functional world of ML. This covers the following in particular.
\begin{itemize}
- \item global references (or arrays), i.e.\ those that persist over
- several invocations of associated operations,\footnote{This is
- independent of the visibility of such mutable values in the toplevel
- scope.}
+ \item Global references (or arrays), i.e.\ mutable memory cells that
+ persist over several invocations of associated
+ operations.\footnote{This is independent of the visibility of such
+ mutable values in the toplevel scope.}
- \item direct I/O on shared channels, notably \isa{stdin}, \isa{stdout}, \isa{stderr}.
+ \item Global state of the running Isabelle/ML process, i.e.\ raw I/O
+ channels, environment variables, current working directory.
+
+ \item Writable resources in the file-system that are shared among
+ different threads or other processes.
\end{itemize}
- The majority of tools implemented within the Isabelle/Isar framework
- will not require any of these critical elements: nothing special
- needs to be observed when staying in the purely functional fragment
- of ML. Note that output via the official Isabelle channels does not
- count as direct I/O, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe.
-
- Moreover, ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to
- run-time invocation of the compiler are also safe, because
- Isabelle/Isar manages this as part of the theory or proof context.
-
- \paragraph{Multithreading in Isabelle/Isar.} The theory loader
- automatically exploits the overall parallelism of independent nodes
- in the development graph, as well as the inherent irrelevance of
- proofs for goals being fully specified in advance. This means,
- checking of individual Isar proofs is parallelized by default.
- Beyond that, very sophisticated proof tools may use local
- parallelism internally, via the general programming model of
- ``future values'' (see also \hyperlink{file.~~/src/Pure/Concurrent/future.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}future{\isachardot}ML}}}}).
-
- Any ML code that works relatively to the present background theory
- is already safe. Contextual data may be easily stored within the
- theory or proof context, thanks to the generic data concept of
- Isabelle/Isar (see \secref{sec:context-data}). This greatly
- diminishes the demand for global state information in the first
- place.
-
- \medskip In rare situations where actual mutable content needs to be
- manipulated, Isabelle provides a single \emph{critical section} that
- may be entered while preventing any other thread from doing the
- same. Entering the critical section without contention is very
- fast, and several basic system operations do so frequently. This
- also means that each thread should leave the critical section
- quickly, otherwise parallel execution performance may degrade
- significantly.
-
- Despite this potential bottle-neck, centralized locking is
- convenient, because it prevents deadlocks without demanding special
- precautions. Explicit communication demands other means, though.
- The high-level abstraction of synchronized variables \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} enables parallel
- components to communicate via shared state; see also \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} as canonical example.
-
- \paragraph{Good conduct of impure programs.} The following
- guidelines enable non-functional programs to participate in
- multithreading.
+ Isabelle/ML provides various mechanisms to avoid critical shared
+ resources in most practical situations. As last resort there are
+ some mechanisms for explicit synchronization. The following
+ guidelines help to make Isabelle/ML programs work smoothly in a
+ concurrent environment.
\begin{itemize}
- \item Minimize global state information. Using proper theory and
- proof context data will actually return to functional update of
- values, without any special precautions for multithreading. Apart
- from the fully general functors for theory and proof data (see
- \secref{sec:context-data}) there are drop-in replacements that
- emulate primitive references for common cases of \emph{configuration
- options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor
- \verb|Named_Thms|).
+ \item Avoid global references altogether. Isabelle/Isar maintains a
+ uniform context that incorporates arbitrary data declared by user
+ programs (\secref{sec:context-data}). This context is passed as
+ plain value and user tools can get/map their own data in a purely
+ functional manner. Configuration options within the context
+ (\secref{sec:config-options}) provide simple drop-in replacements
+ for formerly writable flags.
+
+ \item Keep components with local state information re-entrant.
+ Instead of poking initial values into (private) global references, a
+ new state record can be created on each invocation, and passed
+ through any auxiliary functions of the component. The state record
+ may well contain mutable references, without requiring any special
+ synchronizations, as long as each invocation gets its own copy.
+
+ \item Avoid raw output on \isa{stdout} or \isa{stderr}. The
+ Poly/ML library is thread-safe for each individual output operation,
+ but the ordering of parallel invocations is arbitrary. This means
+ raw output will appear on some system console with unpredictable
+ interleaving of atomic chunks.
+
+ Note that this does not affect regular message output channels
+ (\secref{sec:message-channels}). An official message is associated
+ with the command transaction from where it originates, independently
+ of other transactions. This means each running Isar command has
+ effectively its own set of message channels, and interleaving can
+ only happen when commands use parallelism internally (and only at
+ message boundaries).
+
+ \item Treat environment variables and the current working directory
+ of the running process as strictly read-only.
- \item Keep components with local state information
- \emph{re-entrant}. Instead of poking initial values into (private)
- global references, create a new state record on each invocation, and
- pass that through any auxiliary functions of the component. The
- state record may well contain mutable references, without requiring
- any special synchronizations, as long as each invocation sees its
- own copy. Occasionally, one might even return to plain functional
- updates on non-mutable record values here.
+ \item Restrict writing to the file-system to unique temporary files.
+ Isabelle already provides a temporary directory that is unique for
+ the running process, and there is a centralized source of unique
+ serial numbers in Isabelle/ML. Thus temporary files that are passed
+ to to some external process will be always disjoint, and thus
+ thread-safe.
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{File.tmp\_path}\verb|File.tmp_path: Path.T -> Path.T| \\
+ \indexdef{}{ML}{serial\_string}\verb|serial_string: unit -> string| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|File.tmp_path|~\isa{path} relocates the base
+ component of \isa{path} into the unique temporary directory of
+ the running Isabelle/ML process.
+
+ \item \verb|serial_string|~\isa{{\isacharparenleft}{\isacharparenright}} creates a new serial number
+ that is unique over the runtime of the Isabelle/ML process.
- \item Isolate process configuration flags. The main legitimate
- application of global references is to configure the whole process
- in a certain way, essentially affecting all threads. A typical
- example is the \verb|show_types| flag, which tells the pretty printer
- to output explicit type information for terms. Such flags usually
- do not affect the functionality of the core system, but only the
- view being presented to the user.
-
- Occasionally, such global process flags are treated like implicit
- arguments to certain operations, by using the \verb|setmp_CRITICAL| combinator
- for safe temporary assignment. Its traditional purpose was to
- ensure proper recovery of the original value when exceptions are
- raised in the body, now the functionality is extended to enter the
- \emph{critical section} (with its usual potential of degrading
- parallelism).
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example shows how to create unique
+ temporary file names.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ tmp{\isadigit{1}}\ {\isacharequal}\ File{\isachardot}tmp{\isacharunderscore}path\ {\isacharparenleft}Path{\isachardot}basic\ {\isacharparenleft}{\isachardoublequote}foo{\isachardoublequote}\ {\isacharcircum}\ serial{\isacharunderscore}string\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ val\ tmp{\isadigit{2}}\ {\isacharequal}\ File{\isachardot}tmp{\isacharunderscore}path\ {\isacharparenleft}Path{\isachardot}basic\ {\isacharparenleft}{\isachardoublequote}foo{\isachardoublequote}\ {\isacharcircum}\ serial{\isacharunderscore}string\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}tmp{\isadigit{1}}\ {\isacharless}{\isachargreater}\ tmp{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isamarkupsubsection{Explicit synchronization%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/ML also provides some explicit synchronization
+ mechanisms, for the rare situations where mutable shared resources
+ are really required. These are based on the synchronizations
+ primitives of Poly/ML, which have been adapted to the specific
+ assumptions of the concurrent Isabelle/ML environment. User code
+ must not use the Poly/ML primitives directly!
- Note that recovery of plain value passing semantics via \verb|setmp_CRITICAL|~\isa{ref\ value} assumes that this \isa{ref} is
- exclusively manipulated within the critical section. In particular,
- any persistent global assignment of \isa{ref\ {\isacharcolon}{\isacharequal}\ value} needs to
- be marked critical as well, to prevent intruding another threads
- local view, and a lost-update in the global scope, too.
+ \medskip The most basic synchronization concept is a single
+ \emph{critical section} (also called ``monitor'' in the literature).
+ A thread that enters the critical section prevents all other threads
+ from doing the same. A thread that is already within the critical
+ section may re-enter it in an idempotent manner.
- \end{itemize}
+ Such centralized locking is convenient, because it prevents
+ deadlocks by construction.
- Recall that in an open ``LCF-style'' system like Isabelle/Isar, the
- user participates in constructing the overall environment. This
- means that state-based facilities offered by one component will
- require special caution later on. So minimizing critical elements,
- by staying within the plain value-oriented view relative to theory
- or proof contexts most of the time, will also reduce the chance of
- mishaps occurring to end-users.%
+ \medskip More fine-grained locking works via \emph{synchronized
+ variables}. An explicit state component is associated with
+ mechanisms for locking and signaling. There are operations to
+ await a condition, change the state, and signal the change to all
+ other waiting threads.
+
+ Here the synchronized access to the state variable is \emph{not}
+ re-entrant: direct or indirect nesting within the same thread will
+ cause a deadlock!%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -277,215 +2190,49 @@
\begin{mldecls}
\indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
\indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
- \indexdef{}{ML}{setmp\_CRITICAL}\verb|setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
+ \end{mldecls}
+ \begin{mldecls}
+ \indexdef{}{ML type}{Synchronized.var}\verb|type 'a Synchronized.var| \\
+ \indexdef{}{ML}{Synchronized.var}\verb|Synchronized.var: string -> 'a -> 'a Synchronized.var| \\
+ \indexdef{}{ML}{Synchronized.guarded\_access}\verb|Synchronized.guarded_access: 'a Synchronized.var ->|\isasep\isanewline%
+\verb| ('a -> ('b * 'a) option) -> 'b| \\
\end{mldecls}
\begin{description}
- \item \verb|NAMED_CRITICAL|~\isa{name\ f} evaluates \isa{f\ {\isacharparenleft}{\isacharparenright}}
- while staying within the critical section of Isabelle/Isar. No
- other thread may do so at the same time, but non-critical parallel
- execution will continue. The \isa{name} argument serves for
- diagnostic purposes and might help to spot sources of congestion.
+ \item \verb|NAMED_CRITICAL|~\isa{name\ e} evaluates \isa{e\ {\isacharparenleft}{\isacharparenright}}
+ within the central critical section of Isabelle/ML. No other thread
+ may do so at the same time, but non-critical parallel execution will
+ continue. The \isa{name} argument is used for tracing and might
+ help to spot sources of congestion.
+
+ Entering the critical section without contention is very fast, and
+ several basic system operations do so frequently. Each thread
+ should leave the critical section quickly, otherwise parallel
+ performance may degrade.
\item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
name argument.
- \item \verb|setmp_CRITICAL|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x}
- while staying within the critical section and having \isa{ref\ {\isacharcolon}{\isacharequal}\ value} assigned temporarily. This recovers a value-passing
- semantics involving global references, regardless of exceptions or
- concurrency.
+ \item Type \verb|'a Synchronized.var| represents synchronized
+ variables with state of type \verb|'a|.
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupchapter{Basic library functions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Beyond the proposal of the SML/NJ basis library, Isabelle comes
- with its own library, from which selected parts are given here.
- These should encourage a study of the Isabelle sources,
- in particular files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Linear transformations \label{sec:ML-linear-trans}%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{op $\mid$$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\noindent Many problems in functional programming can be thought of
- as linear transformations, i.e.~a caluclation starts with a
- particular value \verb|x : foo| which is then transformed
- by application of a function \verb|f : foo -> foo|,
- continued by an application of a function \verb|g : foo -> bar|,
- and so on. As a canoncial example, take functions enriching
- a theory by constant declararion and primitive definitions:
-
- \smallskip\begin{mldecls}
- \verb|Sign.declare_const: (binding * typ) * mixfix|\isasep\isanewline%
-\verb| -> theory -> term * theory| \\
- \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory|
- \end{mldecls}
-
- \noindent Written with naive application, an addition of constant
- \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
- a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
-
- \smallskip\begin{mldecls}
- \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
-\verb| (Sign.declare_const|\isasep\isanewline%
-\verb| ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
- \end{mldecls}
+ \item \verb|Synchronized.var|~\isa{name\ x} creates a synchronized
+ variable that is initialized with value \isa{x}. The \isa{name} is used for tracing.
- \noindent With increasing numbers of applications, this code gets quite
- unreadable. Further, it is unintuitive that things are
- written down in the opposite order as they actually ``happen''.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\noindent At this stage, Isabelle offers some combinators which allow
- for more convenient notation, most notably reverse application:
-
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{op $\mid$-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
- \indexdef{}{ML}{op $\mid$$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
- \indexdef{}{ML}{op $\mid$$\mid$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
- \indexdef{}{ML}{op $\mid$$\mid$$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\begin{isamarkuptext}%
-\noindent Usually, functions involving theory updates also return
- side results; to use these conveniently, yet another
- set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->|
- which allows curried access to side results:
+ \item \verb|Synchronized.guarded_access|~\isa{var\ f} lets the
+ function \isa{f} operate within a critical section on the state
+ \isa{x} as follows: if \isa{f\ x} produces \verb|NONE|, we
+ continue to wait on the internal condition variable, expecting that
+ some other thread will eventually change the content in a suitable
+ manner; if \isa{f\ x} produces \verb|SOME|~\isa{{\isacharparenleft}y{\isacharcomma}\ x{\isacharprime}{\isacharparenright}} we
+ are satisfied and assign the new state value \isa{x{\isacharprime}}, broadcast
+ a signal to all waiting threads on the associated condition
+ variable, and return the result \isa{y}.
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
-
- \end{mldecls}
-
- \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own:
-
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false (Binding.name "bar_def", def))|\isasep\isanewline%
-
- \end{mldecls}
-
- \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation
- in the presence of side results which are left unchanged:
+ \end{description}
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
-
- \end{mldecls}
-
- \noindent \verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results:
-
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
-\verb| (Binding.name "bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
-
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
- \indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
- \end{mldecls}%
+ There are some further variants of the general \verb|Synchronized.guarded_access| combinator, see \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} for details.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -496,283 +2243,68 @@
%
\endisadelimmlref
%
-\begin{isamarkuptext}%
-\noindent This principles naturally lift to \emph{lists} using
- the \verb|fold| and \verb|fold_map| combinators.
- The first lifts a single function
- \begin{quote}\footnotesize
- \verb|f : 'a -> 'b -> 'b| to \verb|'a list -> 'b -> 'b|
- \end{quote}
- such that
- \begin{quote}\footnotesize
- \verb|y |\verb,|,\verb|> fold f [x1, x2, ..., x_n]| \\
- \hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb|> f x2 |\verb,|,\verb|> ... |\verb,|,\verb|> f x_n|
- \end{quote}
- \noindent The second accumulates side results in a list by lifting
- a single function
- \begin{quote}\footnotesize
- \verb|f : 'a -> 'b -> 'c * 'b| to \verb|'a list -> 'b -> 'c list * 'b|
- \end{quote}
- such that
- \begin{quote}\footnotesize
- \verb|y |\verb,|,\verb|> fold_map f [x1, x2, ..., x_n]| \\
- \hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb||\verb,|,\verb|>> f x2 |\verb,|,\verb||\verb,|,\verb|>> ... |\verb,|,\verb||\verb,|,\verb|>> f x_n| \\
- \hspace*{6ex}\verb||\verb,|,\verb||\verb,|,\verb|> (fn ((z1, z2), ..., z_n) => [z1, z2, ..., z_n])|
- \end{quote}
-
- \noindent Example:
-
- \smallskip\begin{mldecls}
-\verb|let|\isasep\isanewline%
-\verb| val consts = ["foo", "bar"];|\isasep\isanewline%
-\verb|in|\isasep\isanewline%
-\verb| thy|\isasep\isanewline%
-\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const|\isasep\isanewline%
-\verb| ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
-\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
-\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
-\verb| Thm.add_def false false (Binding.empty, def)) defs)|\isasep\isanewline%
-\verb|end|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimmlex
%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
+\endisadelimmlex
%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
- \indexdef{}{ML}{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
- \indexdef{}{ML}{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
- \indexdef{}{ML}{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
- \indexdef{}{ML}{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
+\isatagmlex
%
\begin{isamarkuptext}%
-\noindent All those linear combinators also exist in higher-order
- variants which do not expect a value on the left hand side
- but a function.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
- \indexdef{}{ML}{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\begin{isamarkuptext}%
-\noindent These operators allow to ``query'' a context
- in a series of context transformations:
+See \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} how to
+ implement a mailbox as synchronized variable over a purely
+ functional queue.
- \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
-\verb| (Sign.full_name thy (Binding.name "foobar")))|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
-\verb| else Sign.declare_const|\isasep\isanewline%
-\verb| ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
-
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Options and partiality%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
- \indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
- \indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
- \indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
- \indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
- \indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
- \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
- \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
- \end{mldecls}%
+ \medskip The following example implements a counter that produces
+ positive integers that are unique over the runtime of the Isabelle
+ process:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
+\endisatagmlex
+{\isafoldmlex}%
%
-\begin{isamarkuptext}%
-Standard selector functions on \isa{option}s are provided. The
- \verb|try| and \verb|can| functions provide a convenient interface for
- handling exceptions -- both take as arguments a function \verb|f|
- together with a parameter \verb|x| and handle any exception during
- the evaluation of the application of \verb|f| to \verb|x|, either
- return a lifted result (\verb|NONE| on failure) or a boolean value
- (\verb|false| on failure).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Common data structures%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lists (as set-like data structures)%
-}
-\isamarkuptrue%
+\isadelimmlex
%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
- \indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
- \indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
- \indexdef{}{ML}{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\endisadelimmlex
%
-\begin{isamarkuptext}%
-Lists are often used as set-like data structures -- set-like in
- the sense that they support a notion of \verb|member|-ship,
- \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive.
- This is convenient when implementing a history-like mechanism:
- \verb|insert| adds an element \emph{to the front} of a list,
- if not yet present; \verb|remove| removes \emph{all} occurences
- of a particular element. Correspondingly \verb|merge| implements a
- a merge on two lists suitable for merges of context data
- (\secref{sec:context-theory}).
-
- Functions are parametrized by an explicit equality function
- to accomplish overloaded equality; in most cases of monomorphic
- equality, writing \verb|op =| should suffice.%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimML
%
-\isamarkupsubsection{Association lists%
-}
-\isamarkuptrue%
+\endisadelimML
%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML exception}{AList.DUP}\verb|exception AList.DUP| \\
- \indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
- \indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
- \indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
- \indexdef{}{ML}{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
- \indexdef{}{ML}{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
- \indexdef{}{ML}{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
-\verb| -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
- \indexdef{}{ML}{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
-\verb| -> ('a * 'b) list -> ('a * 'b) list| \\
- \indexdef{}{ML}{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
-\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
- \indexdef{}{ML}{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
-\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Association lists can be seens as an extension of set-like lists:
- on the one hand, they may be used to implement finite mappings,
- on the other hand, they remain order-sensitive and allow for
- multiple key-value-pair with the same key: \verb|AList.lookup|
- returns the \emph{first} value corresponding to a particular
- key, if present. \verb|AList.update| updates
- the \emph{first} occurence of a particular key; if no such
- key exists yet, the key-value-pair is added \emph{to the front}.
- \verb|AList.delete| only deletes the \emph{first} occurence of a key.
- \verb|AList.merge| provides an operation suitable for merges of context data
- (\secref{sec:context-theory}), where an equality parameter on
- values determines whether a merge should be considered a conflict.
- A slightly generalized operation if implementend by the \verb|AList.join|
- function which allows for explicit conflict resolution.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Tables%
-}
-\isamarkuptrue%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ local\isanewline
+\ \ \ \ val\ counter\ {\isacharequal}\ Synchronized{\isachardot}var\ {\isachardoublequote}counter{\isachardoublequote}\ {\isadigit{0}}{\isacharsemicolon}\isanewline
+\ \ in\isanewline
+\ \ \ \ fun\ next\ {\isacharparenleft}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ Synchronized{\isachardot}guarded{\isacharunderscore}access\ counter\isanewline
+\ \ \ \ \ \ \ \ {\isacharparenleft}fn\ i\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isadigit{1}}\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ SOME\ {\isacharparenleft}j{\isacharcomma}\ j{\isacharparenright}\ end{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ end{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}\isanewline
+\isanewline
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ a\ {\isacharequal}\ next\ {\isacharparenleft}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ val\ b\ {\isacharequal}\ next\ {\isacharparenleft}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}a\ {\isacharless}{\isachargreater}\ b{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML type}{'a Symtab.table}\verb|type 'a Symtab.table| \\
- \indexdef{}{ML exception}{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
- \indexdef{}{ML exception}{Symtab.SAME}\verb|exception Symtab.SAME| \\
- \indexdef{}{ML exception}{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
- \indexdef{}{ML}{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
- \indexdef{}{ML}{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
- \indexdef{}{ML}{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
-\verb| -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
- \indexdef{}{ML}{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
-\verb| -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
-\verb| -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexdef{}{ML}{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
-\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
-\verb| -> 'a Symtab.table (*exception Symtab.DUP*)| \\
- \indexdef{}{ML}{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
-\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
-\verb| -> 'a Symtab.table (*exception Symtab.DUP*)|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimML
%
-\begin{isamarkuptext}%
-Tables are an efficient representation of finite mappings without
- any notion of order; due to their efficiency they should be used
- whenever such pure finite mappings are neccessary.
-
- The key type of tables must be given explicitly by instantiating
- the \verb|Table| functor which takes the key type
- together with its \verb|order|; for convience, we restrict
- here to the \verb|Symtab| instance with \verb|string|
- as key type.
-
- Most table functions correspond to those of association lists.%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\endisadelimML
+\isanewline
%
\isadelimtheory
+\isanewline
%
\endisadelimtheory
%
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Oct 22 20:51:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Oct 22 20:57:33 2010 +0100
@@ -159,13 +159,13 @@
\medskip There is a separate notion of \emph{theory reference} for
maintaining a live link to an evolving theory context: updates on
- drafts are propagated automatically. Dynamic updating stops after
- an explicit \isa{end} only.
+ drafts are propagated automatically. Dynamic updating stops when
+ the next \isa{checkpoint} is reached.
Derived entities may store a theory reference in order to indicate
- the context they belong to. This implicitly assumes monotonic
- reasoning, because the referenced context may become larger without
- further notice.%
+ the formal context from which they are derived. This implicitly
+ assumes monotonic reasoning, because the referenced context may
+ become larger without further notice.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -178,11 +178,14 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{theory}\verb|type theory| \\
+ \indexdef{}{ML}{Theory.eq\_thy}\verb|Theory.eq_thy: theory * theory -> bool| \\
\indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
\indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
\indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\
\indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
\indexdef{}{ML}{Theory.begin\_theory}\verb|Theory.begin_theory: string -> theory list -> theory| \\
+ \indexdef{}{ML}{Theory.parents\_of}\verb|Theory.parents_of: theory -> theory list| \\
+ \indexdef{}{ML}{Theory.ancestors\_of}\verb|Theory.ancestors_of: theory -> theory list| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\
@@ -192,10 +195,15 @@
\begin{description}
- \item \verb|theory| represents theory contexts. This is
- essentially a linear type, with explicit runtime checking! Most
- internal theory operations destroy the original version, which then
- becomes ``stale''.
+ \item Type \verb|theory| represents theory contexts. This is
+ essentially a linear type, with explicit runtime checking.
+ Primitive theory operations destroy the original version, which then
+ becomes ``stale''. This can be prevented by explicit checkpointing,
+ which the system does at least at the boundary of toplevel command
+ transactions \secref{sec:isar-toplevel}.
+
+ \item \verb|Theory.eq_thy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} check strict
+ identity of two theories.
\item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} compares theories
according to the intrinsic graph structure of the construction.
@@ -216,11 +224,17 @@
This version of ad-hoc theory merge fails for unrelated theories!
\item \verb|Theory.begin_theory|~\isa{name\ parents} constructs
- a new theory based on the given parents. This {\ML} function is
+ a new theory based on the given parents. This ML function is
normally not invoked directly.
- \item \verb|theory_ref| represents a sliding reference to an
- always valid theory; updates on the original are propagated
+ \item \verb|Theory.parents_of|~\isa{thy} returns the direct
+ ancestors of \isa{thy}.
+
+ \item \verb|Theory.ancestors_of|~\isa{thy} returns all
+ ancestors of \isa{thy} (not including \isa{thy} itself).
+
+ \item Type \verb|theory_ref| represents a sliding reference to
+ an always valid theory; updates on the original are propagated
automatically.
\item \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} turns a \verb|theory_ref| into an \verb|theory| value. As the referenced
@@ -239,14 +253,54 @@
%
\endisadelimmlref
%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isatagmlantiq
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+ \indexdef{}{ML antiquotation}{theory\_ref}\hypertarget{ML antiquotation.theory-ref}{\hyperlink{ML antiquotation.theory-ref}{\mbox{\isa{theory{\isacharunderscore}ref}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('theory' | 'theory\_ref') nameref?
+ ;
+ \end{rail}
+
+ \begin{description}
+
+ \item \isa{{\isacharat}{\isacharbraceleft}theory{\isacharbraceright}} refers to the background theory of the
+ current context --- as abstract value.
+
+ \item \isa{{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}} refers to an explicitly named ancestor
+ theory \isa{A} of the background theory of the current context
+ --- as abstract value.
+
+ \item \isa{{\isacharat}{\isacharbraceleft}theory{\isacharunderscore}ref{\isacharbraceright}} is similar to \isa{{\isacharat}{\isacharbraceleft}theory{\isacharbraceright}}, but
+ produces a \verb|theory_ref| via \verb|Theory.check_thy| as
+ explained above.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
\isamarkupsubsection{Proof context \label{sec:context-proof}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A proof context is a container for pure data with a
- back-reference to the theory it belongs to. The \isa{init}
- operation creates a proof context from a given theory.
+ back-reference to the theory from which it is derived. The \isa{init} operation creates a proof context from a given theory.
Modifications to draft theories are propagated to the proof context
as usual, but there is also an explicit \isa{transfer} operation
to force resynchronization with more substantial updates to the
@@ -289,9 +343,9 @@
\begin{description}
- \item \verb|Proof.context| represents proof contexts. Elements
- of this type are essentially pure values, with a sliding reference
- to the background theory.
+ \item Type \verb|Proof.context| represents proof contexts.
+ Elements of this type are essentially pure values, with a sliding
+ reference to the background theory.
\item \verb|ProofContext.init_global|~\isa{thy} produces a proof context
derived from \isa{thy}, initializing all data.
@@ -314,6 +368,37 @@
%
\endisadelimmlref
%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isatagmlantiq
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{ML antiquotation}{context}\hypertarget{ML antiquotation.context}{\hyperlink{ML antiquotation.context}{\mbox{\isa{context}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+ \end{matharray}
+
+ \begin{description}
+
+ \item \isa{{\isacharat}{\isacharbraceleft}context{\isacharbraceright}} refers to \emph{the} context at
+ compile-time --- as abstract value. Independently of (local) theory
+ or proof mode, this always produces a meaningful result.
+
+ This is probably the most common antiquotation in interactive
+ experimentation with ML inside Isar.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
\isamarkupsubsection{Generic contexts \label{sec:generic-context}%
}
\isamarkuptrue%
@@ -348,7 +433,7 @@
\begin{description}
- \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
+ \item Type \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
constructors \verb|Context.Theory| and \verb|Context.Proof|.
\item \verb|Context.theory_of|~\isa{context} always produces a
@@ -391,8 +476,9 @@
\end{tabular}
\medskip
- \noindent The \isa{empty} value acts as initial default for
- \emph{any} theory that does not declare actual data content; \isa{extend} is acts like a unitary version of \isa{merge}.
+ The \isa{empty} value acts as initial default for \emph{any}
+ theory that does not declare actual data content; \isa{extend}
+ is acts like a unitary version of \isa{merge}.
Implementing \isa{merge} can be tricky. The general idea is
that \isa{merge\ {\isacharparenleft}data\isactrlsub {\isadigit{1}}{\isacharcomma}\ data\isactrlsub {\isadigit{2}}{\isacharparenright}} inserts those parts of \isa{data\isactrlsub {\isadigit{2}}} into \isa{data\isactrlsub {\isadigit{1}}} that are not yet present, while
@@ -413,19 +499,24 @@
\end{tabular}
\medskip
- \noindent The \isa{init} operation is supposed to produce a pure
- value from the given background theory and should be somehow
+ The \isa{init} operation is supposed to produce a pure value
+ from the given background theory and should be somehow
``immediate''. Whenever a proof context is initialized, which
happens frequently, the the system invokes the \isa{init}
- operation of \emph{all} theory data slots ever declared.
+ operation of \emph{all} theory data slots ever declared. This also
+ means that one needs to be economic about the total number of proof
+ data declarations in the system, i.e.\ each ML module should declare
+ at most one, sometimes two data slots for its internal use.
+ Repeated data declarations to simulate a record type should be
+ avoided!
\paragraph{Generic data} provides a hybrid interface for both theory
and proof data. The \isa{init} operation for proof contexts is
predefined to select the current data value from the background
theory.
- \bigskip Any of these data declaration over type \isa{T} result
- in an ML structure with the following signature:
+ \bigskip Any of the above data declarations over type \isa{T}
+ result in an ML structure with the following signature:
\medskip
\begin{tabular}{ll}
@@ -435,12 +526,12 @@
\end{tabular}
\medskip
- \noindent These other operations provide exclusive access for the
- particular kind of context (theory, proof, or generic context).
- This interface fully observes the ML discipline for types and
- scopes: there is no other way to access the corresponding data slot
- of a context. By keeping these operations private, an Isabelle/ML
- module may maintain abstract values authentically.%
+ These other operations provide exclusive access for the particular
+ kind of context (theory, proof, or generic context). This interface
+ observes the ML discipline for types and scopes: there is no other
+ way to access the corresponding data slot of a context. By keeping
+ these operations private, an Isabelle/ML module may maintain
+ abstract values authentically.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -522,9 +613,9 @@
\endisadelimML
%
\begin{isamarkuptext}%
-\noindent The implementation uses private theory data
- internally, and only exposes an operation that involves explicit
- argument checking wrt.\ the given theory.%
+The implementation uses private theory data internally, and
+ only exposes an operation that involves explicit argument checking
+ wrt.\ the given theory.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -545,13 +636,16 @@
\ \ \ \ val\ extend\ {\isacharequal}\ I{\isacharsemicolon}\isanewline
\ \ \ \ fun\ merge\ {\isacharparenleft}ts{\isadigit{1}}{\isacharcomma}\ ts{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ Ord{\isacharunderscore}List{\isachardot}union\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
-\ \ {\isacharparenright}\isanewline
+\ \ {\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
\ \ val\ get\ {\isacharequal}\ Terms{\isachardot}get{\isacharsemicolon}\isanewline
\isanewline
\ \ fun\ add\ raw{\isacharunderscore}t\ thy\ {\isacharequal}\isanewline
-\ \ \ \ let\ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t\isanewline
-\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}Ord{\isacharunderscore}List{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
+\ \ \ \ let\isanewline
+\ \ \ \ \ \ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t{\isacharsemicolon}\isanewline
+\ \ \ \ in\isanewline
+\ \ \ \ \ \ Terms{\isachardot}map\ {\isacharparenleft}Ord{\isacharunderscore}List{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\isanewline
+\ \ \ \ end{\isacharsemicolon}\isanewline
\isanewline
\ \ end{\isacharsemicolon}\isanewline
{\isacharverbatimclose}%
@@ -563,17 +657,17 @@
\endisadelimML
%
\begin{isamarkuptext}%
-We use \verb|term Ord_List.T| for reasonably efficient
- representation of a set of terms: all operations are linear in the
- number of stored elements. Here we assume that our users do not
- care about the declaration order, since that data structure forces
- its own arrangement of elements.
+Type \verb|term Ord_List.T| is used for reasonably
+ efficient representation of a set of terms: all operations are
+ linear in the number of stored elements. Here we assume that users
+ of this module do not care about the declaration order, since that
+ data structure forces its own arrangement of elements.
Observe how the \verb|merge| operation joins the data slots of
the two constituents: \verb|Ord_List.union| prevents duplication of
common data from different branches, thus avoiding the danger of
- exponential blowup. (Plain list append etc.\ must never be used for
- theory data merges.)
+ exponential blowup. Plain list append etc.\ must never be used for
+ theory data merges!
\medskip Our intended invariant is achieved as follows:
\begin{enumerate}
@@ -594,7 +688,7 @@
type-inference via \verb|Syntax.check_term| (cf.\
\secref{sec:term-check}) is not necessarily monotonic wrt.\ the
background theory, since constraints of term constants can be
- strengthened by later declarations, for example.
+ modified by later declarations, for example.
In most cases, user-space context data does not have to take such
invariants too seriously. The situation is different in the
@@ -603,6 +697,333 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Configuration options \label{sec:config-options}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A \emph{configuration option} is a named optional value of
+ some basic type (Boolean, integer, string) that is stored in the
+ context. It is a simple application of general context data
+ (\secref{sec:context-data}) that is sufficiently common to justify
+ customized setup, which includes some concrete declarations for
+ end-users using existing notation for attributes (cf.\
+ \secref{sec:attributes}).
+
+ For example, the predefined configuration option \hyperlink{attribute.show-types}{\mbox{\isa{show{\isacharunderscore}types}}} controls output of explicit type constraints for
+ variables in printed terms (cf.\ \secref{sec:read-print}). Its
+ value can be modified within Isar text like this:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{declare}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}show{\isacharunderscore}types\ {\isacharequal}\ false{\isacharbrackright}{\isacharbrackright}\isanewline
+\ \ %
+\isamarkupcmt{declaration within (local) theory context%
+}
+\isanewline
+\isanewline
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{note}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}show{\isacharunderscore}types\ {\isacharequal}\ true{\isacharbrackright}{\isacharbrackright}\isanewline
+\ \ \ \ %
+\isamarkupcmt{declaration within proof (forward mode)%
+}
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\ \ \isacommand{term}\isamarkupfalse%
+\ x\isanewline
+%
+\isadelimproof
+\isanewline
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{using}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}show{\isacharunderscore}types\ {\isacharequal}\ false{\isacharbrackright}{\isacharbrackright}\isanewline
+\ \ \ \ \ \ %
+\isamarkupcmt{declaration within proof (backward mode)%
+}
+\isanewline
+\ \ \ \ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Configuration options that are not set explicitly hold a
+ default value that can depend on the application context. This
+ allows to retrieve the value from another slot within the context,
+ or fall back on a global preference mechanism, for example.
+
+ The operations to declare configuration options and get/map their
+ values are modeled as direct replacements for historic global
+ references, only that the context is made explicit. This allows
+ easy configuration of tools, without relying on the execution order
+ as required for old-style mutable references.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{Config.get}\verb|Config.get: Proof.context -> 'a Config.T -> 'a| \\
+ \indexdef{}{ML}{Config.map}\verb|Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context| \\
+ \indexdef{}{ML}{Attrib.config\_bool}\verb|Attrib.config_bool: string -> (Context.generic -> bool) ->|\isasep\isanewline%
+\verb| bool Config.T * (theory -> theory)| \\
+ \indexdef{}{ML}{Attrib.config\_int}\verb|Attrib.config_int: string -> (Context.generic -> int) ->|\isasep\isanewline%
+\verb| int Config.T * (theory -> theory)| \\
+ \indexdef{}{ML}{Attrib.config\_string}\verb|Attrib.config_string: string -> (Context.generic -> string) ->|\isasep\isanewline%
+\verb| string Config.T * (theory -> theory)| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Config.get|~\isa{ctxt\ config} gets the value of
+ \isa{config} in the given context.
+
+ \item \verb|Config.map|~\isa{config\ f\ ctxt} updates the context
+ by updating the value of \isa{config}.
+
+ \item \isa{{\isacharparenleft}config{\isacharcomma}\ setup{\isacharparenright}\ {\isacharequal}}~\verb|Attrib.config_bool|~\isa{name\ default} creates a named configuration option of type
+ \verb|bool|, with the given \isa{default} depending on the
+ application context. The resulting \isa{config} can be used to
+ get/map its value in a given context. The \isa{setup} function
+ needs to be applied to the theory initially, in order to make
+ concrete declaration syntax available to the user.
+
+ \item \verb|Attrib.config_int| and \verb|Attrib.config_string| work
+ like \verb|Attrib.config_bool|, but for types \verb|int| and
+ \verb|string|, respectively.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example shows how to declare and use a
+ Boolean configuration option called \isa{my{\isacharunderscore}flag} with constant
+ default value \verb|false|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ {\isacharparenleft}my{\isacharunderscore}flag{\isacharcomma}\ my{\isacharunderscore}flag{\isacharunderscore}setup{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ Attrib{\isachardot}config{\isacharunderscore}bool\ {\isachardoublequote}my{\isacharunderscore}flag{\isachardoublequote}\ {\isacharparenleft}K\ false{\isacharparenright}\isanewline
+{\isacharverbatimclose}\isanewline
+\isacommand{setup}\isamarkupfalse%
+\ my{\isacharunderscore}flag{\isacharunderscore}setup%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+Now the user can refer to \hyperlink{attribute.my-flag}{\mbox{\isa{my{\isacharunderscore}flag}}} in
+ declarations, while we can retrieve the current value from the
+ context via \verb|Config.get|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}Config{\isachardot}get\ %
+\isaantiq
+context%
+\endisaantiq
+\ my{\isacharunderscore}flag\ {\isacharequal}\ false{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}my{\isacharunderscore}flag\ {\isacharequal}\ true{\isacharbrackright}{\isacharbrackright}\isanewline
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}Config{\isachardot}get\ %
+\isaantiq
+context%
+\endisaantiq
+\ my{\isacharunderscore}flag\ {\isacharequal}\ true{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+\isanewline
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isacharbraceleft}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{note}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}my{\isacharunderscore}flag\ {\isacharequal}\ false{\isacharbrackright}{\isacharbrackright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+%
+\isadelimML
+\ \ \ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}Config{\isachardot}get\ %
+\isaantiq
+context%
+\endisaantiq
+\ my{\isacharunderscore}flag\ {\isacharequal}\ false{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isacharbraceright}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}Config{\isachardot}get\ %
+\isaantiq
+context%
+\endisaantiq
+\ my{\isacharunderscore}flag\ {\isacharequal}\ true{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
\isamarkupsection{Names \label{sec:names}%
}
\isamarkuptrue%
@@ -635,7 +1056,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Strings of symbols%
+\isamarkupsubsection{Strings of symbols \label{sec:symbols}%
}
\isamarkuptrue%
%
@@ -669,11 +1090,11 @@
\end{enumerate}
- \noindent The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many
- regular symbols and control symbols, but a fixed collection of
- standard symbols is treated specifically. For example,
- ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
- may occur within regular Isabelle identifiers.
+ The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many regular symbols and
+ control symbols, but a fixed collection of standard symbols is
+ treated specifically. For example, ``\verb,\,\verb,<alpha>,'' is
+ classified as a letter, which means it may occur within regular
+ Isabelle identifiers.
The character set underlying Isabelle symbols is 7-bit ASCII, but
8-bit character sequences are passed-through unchanged. Unicode/UCS
@@ -718,22 +1139,22 @@
\begin{description}
- \item \verb|Symbol.symbol| represents individual Isabelle
+ \item Type \verb|Symbol.symbol| represents individual Isabelle
symbols.
\item \verb|Symbol.explode|~\isa{str} produces a symbol list
- from the packed form. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
+ from the packed form. This function supersedes \verb|String.explode| for virtually all purposes of manipulating text in
Isabelle!\footnote{The runtime overhead for exploded strings is
mainly that of the list structure: individual symbols that happen to
- be a singleton string --- which is the most common case --- do not
- require extra memory in Poly/ML.}
+ be a singleton string do not require extra memory in Poly/ML.}
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
symbols according to fixed syntactic conventions of Isabelle, cf.\
\cite{isabelle-isar-ref}.
- \item \verb|Symbol.sym| is a concrete datatype that represents
- the different kinds of symbols explicitly, with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.UTF8|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.
+ \item Type \verb|Symbol.sym| is a concrete datatype that
+ represents the different kinds of symbols explicitly, with
+ constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.UTF8|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.
\item \verb|Symbol.decode| converts the string representation of a
symbol into the datatype version.
@@ -823,8 +1244,8 @@
\item \verb|Name.skolem|~\isa{name} produces a Skolem name by
adding two underscores.
- \item \verb|Name.context| represents the context of already used
- names; the initial value is \verb|Name.context|.
+ \item Type \verb|Name.context| represents the context of already
+ used names; the initial value is \verb|Name.context|.
\item \verb|Name.declare|~\isa{name} enters a used name into the
context.
@@ -853,6 +1274,102 @@
%
\endisadelimmlref
%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following simple examples demonstrate how to produce
+ fresh names from the initial \verb|Name.context|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isacharequal}\ Name{\isachardot}invents\ Name{\isachardot}context\ {\isachardoublequote}a{\isachardoublequote}\ {\isadigit{5}}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{1}}\ {\isacharequal}\ {\isacharbrackleft}{\isachardoublequote}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}b{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}c{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}d{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}e{\isachardoublequote}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{2}}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharhash}{\isadigit{1}}\ {\isacharparenleft}Name{\isachardot}variants\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}{\isacharprime}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}{\isacharprime}a{\isachardoublequote}{\isacharbrackright}\ Name{\isachardot}context{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{2}}\ {\isacharequal}\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}xa{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}aa{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}{\isacharprime}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}{\isacharprime}aa{\isachardoublequote}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\medskip The same works reletively to the formal context as
+ follows.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{locale}\isamarkupfalse%
+\ ex\ {\isacharequal}\ \isakeyword{fixes}\ a\ b\ c\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ names\ {\isacharequal}\ Variable{\isachardot}names{\isacharunderscore}of\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isacharequal}\ Name{\isachardot}invents\ names\ {\isachardoublequote}a{\isachardoublequote}\ {\isadigit{5}}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{1}}\ {\isacharequal}\ {\isacharbrackleft}{\isachardoublequote}d{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}e{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}f{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}g{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}h{\isachardoublequote}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{2}}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharhash}{\isadigit{1}}\ {\isacharparenleft}Name{\isachardot}variants\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}{\isacharprime}a{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}{\isacharprime}a{\isachardoublequote}{\isacharbrackright}\ names{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{2}}\ {\isacharequal}\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}xa{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}aa{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}ab{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}{\isacharprime}aa{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}{\isacharprime}ab{\isachardoublequote}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
\isamarkupsubsection{Indexed names \label{sec:indexname}%
}
\isamarkuptrue%
@@ -901,15 +1418,14 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML type}{indexname}\verb|type indexname| \\
+ \indexdef{}{ML type}{indexname}\verb|type indexname = string * int| \\
\end{mldecls}
\begin{description}
- \item \verb|indexname| represents indexed names. This is an
- abbreviation for \verb|string * int|. The second component is
- usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
- is used to inject basic names into this type. Other negative
+ \item Type \verb|indexname| represents indexed names. This is
+ an abbreviation for \verb|string * int|. The second component
+ is usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used to inject basic names into this type. Other negative
indexes should not be used.
\end{description}%
@@ -1017,13 +1533,12 @@
main equation of this ``chemical reaction'' when binding new
entities in a context is as follows:
- \smallskip
+ \medskip
\begin{tabular}{l}
\isa{binding\ {\isacharplus}\ naming\ {\isasymlongrightarrow}\ long\ name\ {\isacharplus}\ name\ space\ accesses}
\end{tabular}
- \smallskip
- \medskip As a general principle, there is a separate name space for
+ \bigskip As a general principle, there is a separate name space for
each kind of formal entity, e.g.\ fact, logical constant, type
constructor, type class. It is usually clear from the occurrence in
concrete syntax (or from the scope) which kind of entity a name
@@ -1036,10 +1551,17 @@
constant \isa{c}. This technique of mapping names from one
space into another requires some care in order to avoid conflicts.
In particular, theorem names derived from a type constructor or type
- class are better suffixed in addition to the usual qualification,
- e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for
- theorems related to type \isa{c} and class \isa{c},
- respectively.%
+ class should get an additional suffix in addition to the usual
+ qualification. This leads to the following conventions for derived
+ names:
+
+ \medskip
+ \begin{tabular}{ll}
+ logical entity & fact name \\\hline
+ constant \isa{c} & \isa{c{\isachardot}intro} \\
+ type \isa{c} & \isa{c{\isacharunderscore}type{\isachardot}intro} \\
+ class \isa{c} & \isa{c{\isacharunderscore}class{\isachardot}intro} \\
+ \end{tabular}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1078,13 +1600,14 @@
\begin{description}
- \item \verb|binding| represents the abstract concept of name
- bindings.
+ \item Type \verb|binding| represents the abstract concept of
+ name bindings.
\item \verb|Binding.empty| is the empty binding.
\item \verb|Binding.name|~\isa{name} produces a binding with base
- name \isa{name}.
+ name \isa{name}. Note that this lacks proper source position
+ information; see also the ML antiquotation \hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}.
\item \verb|Binding.qualify|~\isa{mandatory\ name\ binding}
prefixes qualifier \isa{name} to \isa{binding}. The \isa{mandatory} flag tells if this name component always needs to be
@@ -1107,8 +1630,8 @@
representation for human-readable output, together with some formal
markup that might get used in GUI front-ends, for example.
- \item \verb|Name_Space.naming| represents the abstract concept of
- a naming policy.
+ \item Type \verb|Name_Space.naming| represents the abstract
+ concept of a naming policy.
\item \verb|Name_Space.default_naming| is the default naming policy.
In a theory context, this is usually augmented by a path prefix
@@ -1121,7 +1644,7 @@
name binding (usually a basic name) into the fully qualified
internal name, according to the given naming policy.
- \item \verb|Name_Space.T| represents name spaces.
+ \item Type \verb|Name_Space.T| represents name spaces.
\item \verb|Name_Space.empty|~\isa{kind} and \verb|Name_Space.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
maintaining name spaces according to theory data management
@@ -1161,6 +1684,111 @@
%
\endisadelimmlref
%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isatagmlantiq
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{ML antiquotation}{binding}\hypertarget{ML antiquotation.binding}{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'binding' name
+ ;
+ \end{rail}
+
+ \begin{description}
+
+ \item \isa{{\isacharat}{\isacharbraceleft}binding\ name{\isacharbraceright}} produces a binding with base name
+ \isa{name} and the source position taken from the concrete
+ syntax of this antiquotation. In many situations this is more
+ appropriate than the more basic \verb|Binding.name| function.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example yields the source position of some
+ concrete binding inlined into the text.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Binding{\isachardot}pos{\isacharunderscore}of\ %
+\isaantiq
+binding\ here%
+\endisaantiq
+\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\medskip That position can be also printed in a message as
+ follows.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ writeln\isanewline
+\ \ \ \ {\isacharparenleft}{\isachardoublequote}Look\ here{\isachardoublequote}\ {\isacharcircum}\ Position{\isachardot}str{\isacharunderscore}of\ {\isacharparenleft}Binding{\isachardot}pos{\isacharunderscore}of\ %
+\isaantiq
+binding\ here%
+\endisaantiq
+{\isacharparenright}{\isacharparenright}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+This illustrates a key virtue of formalized bindings as
+ opposed to raw specifications of base names: the system can use this
+ additional information for advanced feedback given to the user.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory