diff -r a16b18fd6299 -r 6a3f7941c3a0 doc-src/IsarImplementation/Thy/document/ML.tex --- 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 %