Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added outline for Isabelle library description
authorhaftmann
Sat, 10 Feb 2007 09:26:11 +0100
changeset 22293 3593a76c9ed3
parent 22292 3b118010ec08
child 22294 4d342f77fd74
added outline for Isabelle library description
doc-src/IsarImplementation/Thy/ML.thy file | annotate | diff | comparison | revisions
doc-src/IsarImplementation/Thy/document/ML.tex file | annotate | diff | comparison | revisions 
--- a/doc-src/IsarImplementation/Thy/ML.thy	Sat Feb 10 09:26:10 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sat Feb 10 09:26:11 2007 +0100
@@ -1,4 +1,3 @@
-
 (* $Id$ *)
 
 theory "ML" imports base begin
@@ -95,8 +94,141 @@
 
 chapter {* Basic library functions *}
 
-text {* FIXME beyond the NJ basis library proposal *}
+text {*
+  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}.
+*}
+
+section {* Linear transformations *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML "(op |>)": "'a * ('a -> 'b) -> 'b"} \\
+  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
+  @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
+  \end{mldecls}
+*}
+
+text FIXME
+
+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"} \\
+  @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
+  \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 %mlref {*
+  \begin{mldecls}
+  @{index_ML "(op `)": "('b -> 'a) -> 'b -> 'a * 'b"} \\
+  @{index_ML tap: "('b -> 'a) -> 'b -> 'b"} \\
+  \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 FIXME
+
+section {* Common data structures *}
+
+text "FIXME chronicle"
+
+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 FIXME
+
+subsection {* Association lists *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML_exc 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 FIXME
+
+subsection {* Tables *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML_type Symtab.key} \\
+  @{index_ML_type "'a Symtab.table"} \\
+  @{index_ML_exc Symtab.DUP: Symtab.key} \\
+  @{index_ML_exc Symtab.DUPS: "Symtab.key list"} \\
+  @{index_ML_exc Symtab.SAME} \\
+  @{index_ML_exc Symtab.UNDEF: Symtab.key} \\
+  @{index_ML Symtab.empty: "'a Symtab.table"} \\
+  @{index_ML Symtab.dest: "'a Symtab.table -> (Symtab.key * 'a) list"} \\
+  @{index_ML Symtab.keys: "'a Symtab.table -> Symtab.key list"} \\
+  @{index_ML Symtab.lookup: "'a Symtab.table -> Symtab.key -> 'a option"} \\
+  @{index_ML Symtab.defined: "'a Symtab.table -> Symtab.key -> bool"} \\
+  @{index_ML Symtab.update: "(Symtab.key * 'a) -> 'a Symtab.table -> 'a Symtab.table"} \\
+  @{index_ML Symtab.default: "Symtab.key * 'a -> 'a Symtab.table -> 'a Symtab.table"} \\
+  @{index_ML Symtab.delete: "Symtab.key
+    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)"} \\
+  @{index_ML Symtab.map_entry: "Symtab.key -> ('a -> 'a)
+    -> 'a Symtab.table -> 'a Symtab.table"} \\
+  @{index_ML Symtab.map_default: "(Symtab.key * 'a) -> ('a -> 'a)
+    -> 'a Symtab.table -> 'a Symtab.table"} \\
+  @{index_ML Symtab.join: "(Symtab.key -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)
+    -> 'a Symtab.table * 'a Symtab.table
+    -> 'a Symtab.table (*exception Symtab.DUPS*)"} \\
+  @{index_ML Symtab.merge: "('a * 'a -> bool)
+    -> 'a Symtab.table * 'a Symtab.table
+    -> 'a Symtab.table (*exception Symtab.DUPS*)"}
+  \end{mldecls}
+*}
+
+text FIXME
 
 chapter {* Cookbook *}
 
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Feb 10 09:26:10 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Feb 10 09:26:11 2007 +0100
@@ -5,7 +5,6 @@
 \isadelimtheory
 \isanewline
 \isanewline
-\isanewline
 %
 \endisadelimtheory
 %
@@ -120,7 +119,216 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME beyond the NJ basis library proposal%
+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
+%
+\begin{isamarkuptext}%
+FIXME%
+\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%
+%
+\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%
+%
+\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
+%
+\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}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Common data structures%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME chronicle%
+\end{isamarkuptext}%
+\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}%
+FIXME%
+\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}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Tables%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{Symtab.key}\verb|type Symtab.key| \\
+  \indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
+  \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of Symtab.key| \\
+  \indexmlexception{Symtab.DUPS}\verb|exception Symtab.DUPS of Symtab.key list| \\
+  \indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
+  \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of Symtab.key| \\
+  \indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
+  \indexml{Symtab.dest}\verb|Symtab.dest: 'a Symtab.table -> (Symtab.key * 'a) list| \\
+  \indexml{Symtab.keys}\verb|Symtab.keys: 'a Symtab.table -> Symtab.key list| \\
+  \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> Symtab.key -> 'a option| \\
+  \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> Symtab.key -> bool| \\
+  \indexml{Symtab.update}\verb|Symtab.update: (Symtab.key * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
+  \indexml{Symtab.default}\verb|Symtab.default: Symtab.key * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
+  \indexml{Symtab.delete}\verb|Symtab.delete: Symtab.key|\isasep\isanewline%
+\verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
+  \indexml{Symtab.map-entry}\verb|Symtab.map_entry: Symtab.key -> ('a -> 'a)|\isasep\isanewline%
+\verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
+  \indexml{Symtab.map-default}\verb|Symtab.map_default: (Symtab.key * 'a) -> ('a -> 'a)|\isasep\isanewline%
+\verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
+  \indexml{Symtab.join}\verb|Symtab.join: (Symtab.key -> '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.DUPS*)| \\
+  \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.DUPS*)|
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
isabelle