# HG changeset patch
# User wenzelm
# Date 1287606176 -3600
# Node ID 648c930125f6cece5d5502d294c18b2a9da5903f
# Parent  bbac63bbcffe0a2d6dfaf11f55c5944feaf8d6ba
more on "Association lists", based on more succinct version of older material;

diff -r bbac63bbcffe -r 648c930125f6 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Oct 20 20:47:06 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Oct 20 21:22:56 2010 +0100
@@ -726,6 +726,48 @@
 *}
 
 
+subsection {* Association lists *}
+
+text {* 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.
+*}
+
+text {*
+  \begin{mldecls}
+  @{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"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML AList.lookup}, @{ML AList.defined}, @{ML AList.update}
+  implement the main ``framework operations'' for mappings in
+  Isabelle/ML, with standard conventions for names and types.
+
+  Note that a function called @{text 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
+  @{text "the_element"} or @{text "get"}.
+
+  The @{text "defined"} operation is essentially a contraction of @{ML
+  is_some} and @{text "lookup"}, but this is sufficiently frequent to
+  justify its independent existence.  This also gives the
+  implementation some opportunity for peep-hole optimization.
+
+  \end{description}
+
+  Association lists are adequate as simple and light-weight
+  implementation of finite mappings in many practical situations.  A
+  more heavy-duty table structure is defined in @{"file"
+  "~~/src/Pure/General/table.ML"}; that version scales easily to
+  thousands or millions of elements.
+*}
+
+
 subsection {* Unsynchronized references *}
 
 text %mlref {*
diff -r bbac63bbcffe -r 648c930125f6 doc-src/IsarImplementation/Thy/ML_old.thy
--- a/doc-src/IsarImplementation/Thy/ML_old.thy	Wed Oct 20 20:47:06 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML_old.thy	Wed Oct 20 21:22:56 2010 +0100
@@ -318,85 +318,4 @@
   \end{mldecls}
 *}
 
-
-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