--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/ML_old.thy Thu Oct 07 19:05:42 2010 +0100
@@ -0,0 +1,634 @@
+theory ML_old
+imports Base
+begin
+
+chapter {* Advanced ML programming *}
+
+section {* Style *}
+
+text {*
+ 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}}
+
+ \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[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. @{verbatim "2 + 2"} is better
+ than @{verbatim "2+2"}, likewise @{verbatim "f (x, y)"} is
+ better than @{verbatim "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 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]
+ 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.
+
+ \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 (@{verbatim
+ int_of_string}, not @{verbatim intOfString}).\footnote{Some
+ recent tools for Emacs include special precautions to cope with
+ bumpy names in @{text "camelCase"}, e.g.\ for improved on-screen
+ readability. It is easier to abstain from using such names in the
+ first place.}
+
+ \end{description}
+*}
+
+
+section {* Thread-safe programming *}
+
+text {*
+ 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.
+
+ 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.
+
+ 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 direct I/O on shared channels, notably @{text "stdin"}, @{text
+ "stdout"}, @{text "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
+ count as direct I/O, so the operations @{ML "writeln"}, @{ML
+ "warning"}, @{ML "tracing"} etc.\ are safe.
+
+ Moreover, ML bindings within the toplevel environment (@{verbatim
+ "type"}, @{verbatim val}, @{verbatim "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 @{"file"
+ "~~/src/Pure/Concurrent/future.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 @{"file"
+ "~~/src/Pure/Concurrent/synchronized.ML"} enables parallel
+ components to communicate via shared state; see also @{"file"
+ "~~/src/Pure/Concurrent/mailbox.ML"} as canonical example.
+
+ \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 @{ML_type "bool"}/@{ML_type "int"}/@{ML_type
+ "string"} (see structure @{ML_struct Config} and @{ML
+ Attrib.config_bool} etc.), and lists of theorems (see functor
+ @{ML_functor Named_Thms}).
+
+ \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 @{ML 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 @{ML 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).
+
+ Note that recovery of plain value passing semantics via @{ML
+ setmp_CRITICAL}~@{text "ref value"} assumes that this @{text "ref"} is
+ exclusively manipulated within the critical section. In particular,
+ any persistent global assignment of @{text "ref := value"} needs to
+ be marked critical as well, to prevent intruding another threads
+ local view, and a lost-update in the global scope, too.
+
+ \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.
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML NAMED_CRITICAL: "string -> (unit -> 'a) -> 'a"} \\
+ @{index_ML CRITICAL: "(unit -> 'a) -> 'a"} \\
+ @{index_ML setmp_CRITICAL: "'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML NAMED_CRITICAL}~@{text "name f"} evaluates @{text "f ()"}
+ 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 @{text "name"} argument serves for
+ diagnostic purposes and might help to spot sources of congestion.
+
+ \item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty
+ name argument.
+
+ \item @{ML setmp_CRITICAL}~@{text "ref value f x"} evaluates @{text "f x"}
+ while staying within the critical section and having @{text "ref :=
+ value"} assigned temporarily. This recovers a value-passing
+ semantics involving global references, regardless of exceptions or
+ concurrency.
+
+ \end{description}
+*}
+
+
+chapter {* Basic library functions *}
+
+text {*
+ 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}.
+*}
+
+section {* Linear transformations \label{sec:ML-linear-trans} *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML "op |> ": "'a * ('a -> 'b) -> 'b"} \\
+ \end{mldecls}
+*}
+
+(*<*)
+typedecl foo
+consts foo :: foo
+ML {*
+val thy = Theory.copy @{theory}
+*}
+(*>*)
+
+text {*
+ \noindent Many problems in functional programming can be thought of
+ as linear transformations, i.e.~a caluclation starts with a
+ particular value @{ML_text "x : foo"} which is then transformed
+ by application of a function @{ML_text "f : foo -> foo"},
+ continued by an application of a function @{ML_text "g : foo -> bar"},
+ and so on. As a canoncial example, take functions enriching
+ a theory by constant declararion and primitive definitions:
+
+ \smallskip\begin{mldecls}
+ @{ML "Sign.declare_const: (binding * typ) * mixfix
+ -> theory -> term * theory"} \\
+ @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory"}
+ \end{mldecls}
+
+ \noindent Written with naive application, an addition of constant
+ @{term bar} with type @{typ "foo \<Rightarrow> foo"} and
+ a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
+
+ \smallskip\begin{mldecls}
+ @{ML "(fn (t, thy) => Thm.add_def false false
+ (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
+ (Sign.declare_const
+ ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
+ \end{mldecls}
+
+ \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''.
+*}
+
+text {*
+ \noindent At this stage, Isabelle offers some combinators which allow
+ for more convenient notation, most notably reverse application:
+
+ \smallskip\begin{mldecls}
+@{ML "thy
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> (fn (t, thy) => thy
+|> Thm.add_def false false
+ (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
+ \end{mldecls}
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML "op |-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
+ @{index_ML "op |>> ": "('a * 'c) * ('a -> 'b) -> 'b * 'c"} \\
+ @{index_ML "op ||> ": "('c * 'a) * ('a -> 'b) -> 'c * 'b"} \\
+ @{index_ML "op ||>> ": "('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b"} \\
+ \end{mldecls}
+*}
+
+text {*
+ \noindent Usually, functions involving theory updates also return
+ side results; to use these conveniently, yet another
+ set of combinators is at hand, most notably @{ML "op |->"}
+ which allows curried access to side results:
+
+ \smallskip\begin{mldecls}
+@{ML "thy
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|-> (fn t => Thm.add_def false false
+ (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+"}
+ \end{mldecls}
+
+ \noindent @{ML "op |>>"} allows for processing side results on their own:
+
+ \smallskip\begin{mldecls}
+@{ML "thy
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
+|-> (fn def => Thm.add_def false false (Binding.name \"bar_def\", def))
+"}
+ \end{mldecls}
+
+ \noindent Orthogonally, @{ML "op ||>"} applies a transformation
+ in the presence of side results which are left unchanged:
+
+ \smallskip\begin{mldecls}
+@{ML "thy
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+||> Sign.add_path \"foobar\"
+|-> (fn t => Thm.add_def false false
+ (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+||> Sign.restore_naming thy
+"}
+ \end{mldecls}
+
+ \noindent @{ML "op ||>>"} accumulates side results:
+
+ \smallskip\begin{mldecls}
+@{ML "thy
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+||>> Sign.declare_const ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
+|-> (fn (t1, t2) => Thm.add_def false false
+ (Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
+"}
+ \end{mldecls}
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
+ @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
+ \end{mldecls}
+*}
+
+text {*
+ \noindent This principles naturally lift to \emph{lists} using
+ the @{ML fold} and @{ML fold_map} combinators.
+ The first lifts a single function
+ \begin{quote}\footnotesize
+ @{ML_text "f : 'a -> 'b -> 'b"} to @{ML_text "'a list -> 'b -> 'b"}
+ \end{quote}
+ such that
+ \begin{quote}\footnotesize
+ @{ML_text "y |> fold f [x1, x2, ..., x_n]"} \\
+ \hspace*{2ex}@{text "\<leadsto>"} @{ML_text "y |> f x1 |> f x2 |> ... |> f x_n"}
+ \end{quote}
+ \noindent The second accumulates side results in a list by lifting
+ a single function
+ \begin{quote}\footnotesize
+ @{ML_text "f : 'a -> 'b -> 'c * 'b"} to @{ML_text "'a list -> 'b -> 'c list * 'b"}
+ \end{quote}
+ such that
+ \begin{quote}\footnotesize
+ @{ML_text "y |> fold_map f [x1, x2, ..., x_n]"} \\
+ \hspace*{2ex}@{text "\<leadsto>"} @{ML_text "y |> f x1 ||>> f x2 ||>> ... ||>> f x_n"} \\
+ \hspace*{6ex}@{ML_text "||> (fn ((z1, z2), ..., z_n) => [z1, z2, ..., z_n])"}
+ \end{quote}
+
+ \noindent Example:
+
+ \smallskip\begin{mldecls}
+@{ML "let
+ val consts = [\"foo\", \"bar\"];
+in
+ thy
+ |> fold_map (fn const => Sign.declare_const
+ ((Binding.name const, @{typ \"foo => foo\"}), NoSyn)) consts
+ |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
+ |-> (fn defs => fold_map (fn def =>
+ Thm.add_def false false (Binding.empty, def)) defs)
+end"}
+ \end{mldecls}
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML "op #> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
+ @{index_ML "op #-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
+ @{index_ML "op #>> ": "('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b"} \\
+ @{index_ML "op ##> ": "('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd"} \\
+ @{index_ML "op ##>> ": "('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd"} \\
+ \end{mldecls}
+*}
+
+text {*
+ \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.
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML "op ` ": "('b -> 'a) -> 'b -> 'a * 'b"} \\
+ @{index_ML tap: "('b -> 'a) -> 'b -> 'b"} \\
+ \end{mldecls}
+*}
+
+text {*
+ \noindent These operators allow to ``query'' a context
+ in a series of context transformations:
+
+ \smallskip\begin{mldecls}
+@{ML "thy
+|> tap (fn _ => writeln \"now adding constant\")
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+||>> `(fn thy => Sign.declared_const thy
+ (Sign.full_name thy (Binding.name \"foobar\")))
+|-> (fn (t, b) => if b then I
+ else Sign.declare_const
+ ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
+"}
+ \end{mldecls}
+*}
+
+section {* Options and partiality *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML is_some: "'a option -> bool"} \\
+ @{index_ML is_none: "'a option -> bool"} \\
+ @{index_ML the: "'a option -> 'a"} \\
+ @{index_ML these: "'a list option -> 'a list"} \\
+ @{index_ML the_list: "'a option -> 'a list"} \\
+ @{index_ML the_default: "'a -> 'a option -> 'a"} \\
+ @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
+ @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
+ \end{mldecls}
+*}
+
+text {*
+ Standard selector functions on @{text option}s are provided. The
+ @{ML try} and @{ML can} functions provide a convenient interface for
+ handling exceptions -- both take as arguments a function @{ML_text f}
+ together with a parameter @{ML_text x} and handle any exception during
+ the evaluation of the application of @{ML_text f} to @{ML_text x}, either
+ return a lifted result (@{ML NONE} on failure) or a boolean value
+ (@{ML false} on failure).
+*}
+
+
+section {* Common data structures *}
+
+subsection {* Lists (as set-like data structures) *}
+
+text {*
+ \begin{mldecls}
+ @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
+ @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
+ @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
+ @{index_ML merge: "('a * 'a -> bool) -> 'a list * 'a list -> 'a list"} \\
+ \end{mldecls}
+*}
+
+text {*
+ Lists are often used as set-like data structures -- set-like in
+ the sense that they support a notion of @{ML member}-ship,
+ @{ML insert}-ing and @{ML remove}-ing, but are order-sensitive.
+ This is convenient when implementing a history-like mechanism:
+ @{ML insert} adds an element \emph{to the front} of a list,
+ if not yet present; @{ML remove} removes \emph{all} occurences
+ of a particular element. Correspondingly @{ML 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 @{ML "op ="} should suffice.
+*}
+
+subsection {* Association lists *}
+
+text {*
+ \begin{mldecls}
+ @{index_ML_exn AList.DUP} \\
+ @{index_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\
+ @{index_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\
+ @{index_ML AList.update: "('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list"} \\
+ @{index_ML AList.default: "('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list"} \\
+ @{index_ML AList.delete: "('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list"} \\
+ @{index_ML AList.map_entry: "('a * 'b -> bool) -> 'a
+ -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list"} \\
+ @{index_ML AList.map_default: "('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)
+ -> ('a * 'b) list -> ('a * 'b) list"} \\
+ @{index_ML AList.join: "('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)
+ -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)"} \\
+ @{index_ML AList.merge: "('a * 'a -> bool) -> ('b * 'b -> bool)
+ -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)"}
+ \end{mldecls}
+*}
+
+text {*
+ 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: @{ML AList.lookup}
+ returns the \emph{first} value corresponding to a particular
+ key, if present. @{ML 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}.
+ @{ML AList.delete} only deletes the \emph{first} occurence of a key.
+ @{ML 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 @{ML AList.join}
+ function which allows for explicit conflict resolution.
+*}
+
+subsection {* Tables *}
+
+text {*
+ \begin{mldecls}
+ @{index_ML_type "'a Symtab.table"} \\
+ @{index_ML_exn Symtab.DUP: string} \\
+ @{index_ML_exn Symtab.SAME} \\
+ @{index_ML_exn Symtab.UNDEF: string} \\
+ @{index_ML Symtab.empty: "'a Symtab.table"} \\
+ @{index_ML Symtab.lookup: "'a Symtab.table -> string -> 'a option"} \\
+ @{index_ML Symtab.defined: "'a Symtab.table -> string -> bool"} \\
+ @{index_ML Symtab.update: "(string * 'a) -> 'a Symtab.table -> 'a Symtab.table"} \\
+ @{index_ML Symtab.default: "string * 'a -> 'a Symtab.table -> 'a Symtab.table"} \\
+ @{index_ML Symtab.delete: "string
+ -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)"} \\
+ @{index_ML Symtab.map_entry: "string -> ('a -> 'a)
+ -> 'a Symtab.table -> 'a Symtab.table"} \\
+ @{index_ML Symtab.map_default: "(string * 'a) -> ('a -> 'a)
+ -> 'a Symtab.table -> 'a Symtab.table"} \\
+ @{index_ML Symtab.join: "(string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)
+ -> 'a Symtab.table * 'a Symtab.table
+ -> 'a Symtab.table (*exception Symtab.DUP*)"} \\
+ @{index_ML Symtab.merge: "('a * 'a -> bool)
+ -> 'a Symtab.table * 'a Symtab.table
+ -> 'a Symtab.table (*exception Symtab.DUP*)"}
+ \end{mldecls}
+*}
+
+text {*
+ 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 @{ML_functor Table} functor which takes the key type
+ together with its @{ML_type order}; for convience, we restrict
+ here to the @{ML_struct Symtab} instance with @{ML_type string}
+ as key type.
+
+ Most table functions correspond to those of association lists.
+*}
+
+end
\ No newline at end of file