%
\begin{isabellebody}%
\def\isabellecontext{ML}%
%
\isadelimtheory
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Aesthetics of ML programming%
}
\isamarkuptrue%
%
\isamarkupsection{Style%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
This style guide is loosely based on
\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}.
% FIMXE \url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm}
Like any style guide, it should not be interpreted dogmatically, but
with care and discernment. Instead, it forms a collection of
recommendations which, if obeyed, result in code that is not
considered to be obfuscated. In certain cases, derivations are
encouraged, as far as you know what you are doing.
\begin{description}
\item[fundamental law of programming]
Whenever writing code, keep in mind: A program is
written once, modified ten times, and read
100 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[white space matters]
Treat white space in your code as if it determines
the meaning of code.
\begin{itemize}
\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)|.
\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.
\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}
\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 or fixed later on.
\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.
\item[functional programming is based on functions]
Avoid ``constructivisms'', i.e.\ unnecessary concrete datatype
representations. Instead model things as abstract as
appropriate. For example, pass a table lookup function rather
than a concrete table with lookup performed in body. Accustom
your way of coding to the level of expressiveness a functional
programming language is giving onto you.
\item[tuples]
are often in the way. When there is no striking argument
to tuple function arguments, just write your function curried.
\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.}
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Thread-safe programming%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Recent versions of Poly/ML (5.1 or later) support 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
2--4 can be expected for large well-structured Isabelle sessions,
where theories are organized as a graph with sufficiently many
independent nodes.
Threads lack the memory protection of separate processes, but
operate concurrently on shared heap memory. This has the advantage
that results of independent computations are immediately available
to other threads, without requiring explicit communication,
reloading, or even recoding of data.
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.
\medskip \paragraph{Critical shared resources.} Actually only those
parts outside the purely functional world of ML are critical. In
particular, this covers
\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 ML bindings in the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to
run-time invocation of the compiler,
\item direct I/O on shared channels, notably \isa{stdin}, \isa{stdout}, \isa{stderr}.
\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
even count as direct I/O in the above sense, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe.
\paragraph{Multithreading in Isabelle/Isar.} Our parallel execution
model is centered around the theory loader. Whenever a given
subgraph of theories needs to be updated, the system schedules a
number of threads to process the sources as required, while
observing their dependencies. Thus concurrency is limited to
independent nodes according to the theory import relation.
Any user-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, we refrain from fine-grained
locking mechanisms: the restriction to a single lock prevents
deadlocks without demanding further considerations in user programs.
\paragraph{Good conduct of impure programs.} The following
guidelines enable non-functional programs to participate in
multithreading.
\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|NamedThmsFun|).
\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 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| 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).
Note that recovery of plain value passing semantics via \verb|setmp|~\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.
\item Minimize global ML bindings. Processing theories occasionally
affects the global ML environment as well. While each ML
compilation unit is safe, the order of scheduling of independent
declarations might cause problems when composing several modules
later on, due to hiding of previous ML names.
This cannot be helped in general, because the ML toplevel lacks the
graph structure of the Isabelle theory space. Nevertheless, some
sound conventions of keeping global ML names essentially disjoint
(e.g.\ with the help of ML structures) prevents the problem to occur
in most practical situations.
\end{itemize}
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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{NAMED-CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
\indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
\indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
\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|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
name argument.
\item \verb|setmp|~\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.
\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.
See further files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Linear transformations%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
\indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
\indexml{fold-rev}\verb|fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimML
%
\endisadelimML
%
\isatagML
%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
Many problems in functional programming can be thought of
as linear transformations, i.e.~a caluclation starts with a
particular value \isa{x\ {\isasymColon}\ foo} which is then transformed
by application of a function \isa{f\ {\isasymColon}\ foo\ {\isasymRightarrow}\ foo},
continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar},
and so on. As a canoncial example, take primitive functions enriching
theories by constants and definitions:
\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory|\isasep\isanewline%
\verb|-> theory|
and \verb|Theory.add_defs_i: bool -> bool|\isasep\isanewline%
\verb|-> (bstring * term) list -> theory -> theory|.
Written with naive application, an addition of a constant with
a corresponding definition would look like:
\verb|Theory.add_defs_i false false [dummy_def]|\isasep\isanewline%
\verb| (Sign.add_consts_i [dummy_const] thy)|.
With increasing numbers of applications, this code gets quite unreadable.
Using composition, at least the nesting of brackets may be reduced:
\verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i|\isasep\isanewline%
\verb| [dummy_const]) thy|.
What remains unsatisfactory is that things are written down in the opposite order
as they actually ``happen''.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
At this stage, Isabelle offers some combinators which allow for more convenient
notation, most notably reverse application:
\isasep\isanewline%
\verb|thy|\isasep\isanewline%
\verb||\verb,|,\verb|> Sign.add_consts_i [dummy_const]|\isasep\isanewline%
\verb||\verb,|,\verb|> Theory.add_defs_i false false [dummy_def]|%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent When iterating over a list of parameters \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymColon}\ {\isacharprime}a\ list},
the \verb|fold| combinator lifts a single function \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}:
\isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
\indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
\indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
\indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
\indexml{fold-map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\begin{isamarkuptext}%
\noindent FIXME transformations involving side results%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
\indexml{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
\indexml{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
\indexml{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
\indexml{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\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}
\indexml{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
\indexml{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\begin{isamarkuptext}%
\noindent FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Options and partiality%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{is-some}\verb|is_some: 'a option -> bool| \\
\indexml{is-none}\verb|is_none: 'a option -> bool| \\
\indexml{the}\verb|the: 'a option -> 'a| \\
\indexml{these}\verb|these: 'a list option -> 'a list| \\
\indexml{the-list}\verb|the_list: 'a option -> 'a list| \\
\indexml{the-default}\verb|the_default: 'a -> 'a option -> 'a| \\
\indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
\indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\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 \isa{f}
together with a parameter \isa{x} and handle any exception during
the evaluation of the application of \isa{f} to \isa{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%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
\indexml{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
\indexml{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
\indexml{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
Lists are often used as set-like data structures -- set-like in
then sense that they support 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%
%
\isamarkupsubsection{Association lists%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmlexception{AList.DUP}\verb|exception AList.DUP| \\
\indexml{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
\indexml{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
\indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
\indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
\indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
\indexml{AList.map-entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
\verb| -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
\indexml{AList.map-default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
\verb| -> ('a * 'b) list -> ('a * 'b) list| \\
\indexml{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*)| \\
\indexml{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%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
\indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
\indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
\indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
\indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
\indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
\indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
\indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
\indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
\indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
\verb| -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
\indexml{Symtab.map-entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\
\indexml{Symtab.map-default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\
\indexml{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*)| \\
\indexml{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%
%
\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|TableFun| 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%
%
\isamarkupchapter{Cookbook%
}
\isamarkuptrue%
%
\isamarkupsection{A method that depends on declarations in the context%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: