--- 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 {*
--- 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