%
\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%
%
\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.
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. {\ttfamily 2 + 2} is better
than {\ttfamily 2+2}, likewise {\ttfamily f (x, y)}
better than {\ttfamily f(x,y)}.
\item Restrict your lines to \emph{at most} 80 characters.
This will allow you to keep the beginning of a line
in view while watching its end.
\item Ban tabs; they are a context-sensitive formatting
feature and likely to confuse anyone not using your
favourite editor.
\item Get rid of trailing whitespace. Instead, do not
surpess 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'', e.g. pass a table lookup function,
rather than an actual table with lookup in body. Accustom
your way of codeing 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 neccessary 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|'')
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\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 -> theory|
and \verb|Theory.add_defs_i: bool -> bool -> (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] (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 [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}%
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}%
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}%
FIXME higher-order variants%
\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
%
\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%
%
\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: