\chapter{General Purpose and List Processing Functions}
\label{MLfuns}

This chapter describes a selection of commonly useful \ML\ functions applicable
to pairs, lists and other \ML\ values. All the functions are definable in \ML.
Each function is documented by:

\begin{myenumerate}
\item Its name and type.
\item A brief description.
\item An \ML\ declaration defining the 
function (note that this is not necessarily
the definition used: some of the functions are coded directly in Lisp).
\end{myenumerate}

\noindent Functions preceded by {\small\verb%$%}\index{ escape, in ML parser@{\small\verb+$+} (escape, in \ML\ parser)}\index{infixes, in ML@infixes, in \ML}\index{dollared infixes, in ML@dollared infixes, in \ML}
may be used as infix operators
(without the {\small\verb%$%}), or in normal prefix form or as arguments to other
functions (with the {\small\verb%$%}).

The functions usually fail with failure string\index{failure strings, in ML@failure strings, in \ML!of general purpose functions} equal to their name; sometimes,
however, the failure string is the one generated by the subfunction that caused the
failure.


\section{General purpose functions and combinators}

\noindent The standard primitive combinators\index{combinators, in ML@combinators, in \ML|(} are:

\begin{boxed}
\index{I, the constant in ML@\ml{I}, the constant in \ML|pin}
\index{K, the constant in ML@\ml{K}, the constant in \ML|pin}
\index{S, the constant in ML@\ml{S}, the constant in \ML|pin}
\begin{verbatim}
   I : * -> *
   K : * -> ** -> *
   S : (* -> ** -> ***) -> (* -> **) -> * -> ***
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{I}\ x = x\qquad \ml{K}\ x\ y = x\qquad \ml{S}\ f\ g\ x = f\ x\ (g\ x) \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let I x = x

   let K x y = x

   let S f g x = f x (g x)
\end{verbatim}\end{hol}


\noindent The derived combinators \ml{KI} (the dual of \ml{K}), \ml{C} (the
permutator), \ml{W} (the duplicator), \ml{B} (the compositor) and \ml{CB}
(which is declared to be infix) have types:

\begin{boxed}

\index{KI@\ml{KI}|pin}
\index{C@\ml{C}|pin}
\index{W@\ml{W}|pin}
\index{B@\ml{B}|pin}
\index{CB@\ml{CB}|pin}
\begin{verbatim}
   KI : * -> ** -> **
   C  : (* -> ** -> ***) -> ** -> * -> ***
   W  : (* -> * -> **) -> * -> **
   B  : (* -> **) -> (*** -> *) -> *** -> **
   CB : (* -> **) -> (** -> ***) -> * -> ***
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{KI}\ x\ y = y\qquad
\ml{C}\ f\ x\ y = f\ y\ x\qquad
\ml{B}\ f\ g\ x = f(g\ x)\qquad
\ml{W}\ f\ x = f\ x\ x \]
\[ \ml{CB}\ f\ g\ x = g(f\ x) \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let KI = K I

   let C f x y = f y x

   let W f x = f x x

   let B f g x = f(g x)

   let (f CB g) x = g(f x)
\end{verbatim}\end{hol}


\noindent The next group of functions are various useful infixed
function-composition\index{function composition, in ML@function composition, in \ML} operators:

\begin{boxed}
\index{ function composition operator, in ML@{\small\verb+o+} (function composition operator, in \ML)|pin}
\index{ product function operator, in ML@{\small\verb+#+} (product function operator, in \ML)|pin}
\index{product function operator, in ML@product function operator, in \ML}
\index{Co@\ml{Co}|pin}\begin{verbatim}
   $o  : ((* -> **) # (*** -> *)) -> *** -> **
   $#  : ((* -> **) # (*** -> ****)) -> (* # ***) -> (** # ****)
   $Co : ((* -> ** -> ***) # (**** -> *)) -> ** -> **** -> ***
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \begin{array}{ll}
(f\ \ml{o}\ g)\ x &= f(g\ x)\\
 & \\
(f\ {\mbox\small\verb%#%}\ g)(x,y) &= (f\ x,\ g\ y)\\
 & \\
(f\ \ml{Co}\ g)\ x\ y &= \ml{C}(f\ \ml{o}\ g)\ x\ y = f\ (g\ y)\ x
\end{array} \]
\index{combinators, in ML@combinators, in \ML|)}

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   ml_paired_infix `o`
   let (f o g) x = f(g x)

   ml_paired_infix `#`
   let (f # g)(x,y) = (f x, g y)

   ml_paired_infix `Co`
   let (f Co g) x y = f (g y) x
\end{verbatim}\end{hol}


\noindent The following two functions convert between curried and uncurried
versions of a binary function.

\begin{boxed}
\index{curry@\ml{curry}|pin}
\index{uncurry@\ml{uncurry}|pin}
\begin{verbatim}
   curry   : ((* # **) -> ***) -> (* -> ** -> ***)
   uncurry : (* -> ** -> ***) -> ((* # **) -> ***)
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{curry}\ f\ x\ y = f(x,y)\qquad \ml{uncurry}\ f\ (x,y) = f\ x\ y \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let curry f x y = f (x,y)

   let uncurry f (x,y) = f x y
\end{verbatim}\end{hol}


\noindent The next function tests for failure\index{failure, in ML@failure, in \ML!test for}.

\begin{boxed}
\index{can@\ml{can}|pin}
\begin{verbatim}
   can : (* -> **) -> * -> bool
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{can\ $f$\ $x$} evaluates to \ml{true} if the application of $f$ to $x$
succeeds; it evaluates to \ml{false} if the evaluation fails.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let can f x = (f x; true) ? false
\end{verbatim}\end{hol}


\noindent The next function iterates\index{function application, in ML@function application, in \ML!iteration of}\index{iterated function application, in ML@iterated function application, in \ML} a function a fixed number of times.

\begin{boxed}
\index{funpow@\ml{funpow}|pin}
\begin{verbatim}
   funpow : int -> (* -> *) -> * -> *
\end{verbatim}\end{boxed}

\subsubsection*{Description}

$\ml{funpow}\ n\ f\ x$ applies $f$ to $x$ $n$-times:
$\ml{funpow}\ n\ f = f^n$

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec funpow n f x = if n=0 then x else funpow (n-1) f (f x)
\end{verbatim}\end{hol}


\section{Miscellaneous list processing functions}

The function {\small\verb%length%}
computes the length of a list.

\begin{boxed}
\index{length@\ml{length}|pin}
\begin{verbatim}
   length : * list -> int
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{length}\ \ml{[}x_1\ml{;}\ldots\ml{;}x_n\ml{]} = n \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec length = fun [] . 0 | (_.l) . 1+(length l)
\end{verbatim}\end{hol}


\noindent The function \ml{append} concatenates\index{ list concatenation, in ML@{\small\verb+"@+} (list concatenation, in \ML)}
 lists; {\small\verb%@%} is an
uncurried and infixed version 
of {\small\verb%append%}\index{concatenation, of lists!in ML@in \ML}.

\begin{boxed}
\index{append@\ml{append}|pin}
\begin{verbatim}
   append : * list -> * list -> * list
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{append}\ \ml{[}x_1\ml{;}\ldots\ml{;}x_m\ml{]}\ 
\ml{[}y_1\ml{;}\ldots\ml{;}y_n\ml{]} =
\ml{[}x_1\ml{;}\ldots\ml{;}x_m\ml{;}y_1\ml{;}\ldots\ml{;}y_n\ml{]} \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec append l1 l2 = if null l1 then l2 else hd l1.append (tl l1) l2
\end{verbatim}\end{hol}


\noindent The function \ml{el} extracts a specified element from a list. It
fails if the integer argument is less than 1 or greater than the length of the
list.

\begin{boxed}
\index{el@\ml{el}|pin}
\begin{verbatim}
   el : int -> * list -> *
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{el}\ i\ \ml{[}x_1\ml{;}\ldots\ml{;}x_n\ml{]} = x_i \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec el i l =
    if null l or i < 1 then failwith `el`
    else if i = 1 then hd l
    else el (i-1) (tl l)
\end{verbatim}\end{hol}


\noindent The functions \ml{last} and \ml{butlast} compute the last element
of a list and all but the last element of a list. Both fail if the argument
list is empty.

\begin{boxed}
\index{last@\ml{last}|pin}
\index{butlast@\ml{butlast}|pin}
\begin{verbatim}
   last    : * list -> *
   butlast : * list -> * list
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{last}\ \ml{[}x_1\ml{;}\ldots\ml{;}x_n\ml{]} = x_n \]

\[ \ml{butlast}\ \ml{[}x_1\ml{;}\ldots\ml{;}x_n\ml{]} =
\ml{[}x_1\ml{;}\ldots\ml{;}x_{n-1}\ml{]} \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec last l = last (tl l) ? hd l ? failwith `last`

   letrec butlast l =
    if null (tl l) then [] else (hd l).(butlast(tl l)) ? failwith `butlast`
\end{verbatim}\end{hol}


\noindent The next function makes a list consisting of a value replicated a
specified number of times. It fails if the specified number is less than zero.

\begin{boxed}
\index{replicate@\ml{replicate}|pin}
\begin{verbatim}
   replicate : * -> int -> * list
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{replicate\ $x$\ $n$} evaluates to \ml{[}$x$\ml{;}$\ldots$\ml{;}$x$\ml{]},
a list of length $n$.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec replicate x n =
    if n < 0 then failwith `replicate`
    else if n = 0 then []
    else x . (replicate x (n-1))
\end{verbatim}\end{hol}


\section{List mapping and iterating functions}

\begin{boxed}
\index{map@\ml{map}|pin}
\begin{verbatim}
   map : (* -> **) -> * list -> ** list
\end{verbatim}\end{boxed}

\subsubsection*{Description} 

\ml{map\ $f$\ $l$} returns the list obtained by
applying $f$ to the elements of $l$ in turn.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec map f l = if null l then [] else f(hd l). map f (tl l)
\end{verbatim}\end{hol}


\noindent The following three functions are versions of `reduce'\index{reduce}.

\begin{boxed}
\index{itlist@\ml{itlist}|pin}
\index{rev_itlist@\ml{rev\_itlist}|pin}
\begin{verbatim}
   itlist     : (* -> ** -> **) -> * list -> ** -> **
   rev_itlist : (* -> ** -> **) -> * list -> ** -> **
   end_itlist : (* -> * -> *) -> * list -> *
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ 
\begin{array}{@{}ll}
\ml{itlist}\ f\ \ml{[}x_1\ml{;}x_2\ml{;}\ldots\ml{;}x_n\ml{]}\ x & =
f\ x_1\ (f\ x_2\ (\ \ldots\ (f\ x_n\ x)\ \ldots\ ))\\
 &= ((f\ x_1)\ \ml{o}\ (f\ x_2)\ \ml{o}\ \ldots\ \ml{o}\ (f\ x_n))\ x\\
 & \\
\ml{rev\_itlist}\ f\ \ml{[}x_1\ml{;}\ldots\ml{;}x_{n-1}\ml{;}x_n\ml{]}\ x& =
f\ x_n\ (f\ x_{n-1}\ (\ \ldots\ (f\ x_1\ x)\ \ldots\ ))\\
 &= ((f\ x_n)\ \ml{o}\ (f\ x_{n-1})\ \ml{o}\ \ldots\ \ml{o}\ (f\ x_1))\ x\\
 & \\
\ml{end\_itlist}\ f\ \ml{[}x_1\ml{;}x_2\ml{;}\ldots\ml{;}x_{n-1}\ml{;}x_n\ml{]}\ & =
f\ x_1\ (f\ x_2\ (\ \ldots\ (f\ x_{n-1}\ x_n)\ \ldots\ ))\\
 &= ((f\ x_1)\ \ml{o}\ (f\ x_2)\ \ml{o}\ \ldots\ \ml{o}\ (f\ x_{n-1}))\ x_n\\
\end{array} \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec itlist f l x =
    if null l then x else f (hd l) (itlist f (tl l) x)

   letrec rev_itlist f l x = 
    if null l then x else rev_itlist f (tl l) (f (hd l) x)

   let end_itlist ff l =
    if null l then failwith `end_itlist`
    else (let last.rest = rev l in
          rev_itlist ff rest last)
\end{verbatim}\end{hol}

\noindent or, equivalently:

\begin{hol}\begin{verbatim}
   letrec itlist f     = fun [] . I | (y.l) . \x. f y (itlist f l x)

   letrec rev_itlist f = fun [] . I | (y.l) . \x. rev_itlist f l (f y x)
\end{verbatim}\end{hol}


\section{List searching functions}

The functions described in this section search lists for elements with various
properties. Those functions that return elements fail if no 
such element is found;
those that return booleans never fail (\ml{false} is returned 
if the element is not found).

\begin{boxed}
\index{find@\ml{find}|pin}
\index{tryfind@\ml{tryfind}|pin}
\begin{verbatim}
   find    : (* -> bool) -> * list -> *
   tryfind : (* -> **) -> * list -> **
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{find\ $p$\ $l$} returns the first element of $l$ which 
satisfies the predicate
$p$; \ml{tryfind\ $f$\ $l$} returns the result of applying 
$f$ to the first member
of $l$ for which the application of $f$ succeeds.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec find p    = fun []    . failwith `find`
                       |  (x.l) . if p x then x else find p l


   letrec tryfind f = fun []    . failwith `tryfind`
                       |  (x.l) . (f x ? tryfind f l)
\end{verbatim}\end{hol}


\noindent The next two functions are analogous to the quantifiers $\exists$ and
$\forall$.

\begin{boxed}
\index{forall@\ml{forall}|pin}
\index{exists@\ml{exists}|pin}
\begin{verbatim}
   exists : (* -> bool) -> * list -> bool
   forall : (* -> bool) -> * list -> bool
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{exists\ $p$\ $l$} applies $p$ to the elements of $l$ in order until one is
found which satisfies $p$, or until the list is exhausted, returning \ml{true} or
\ml{false} accordingly; \ml{forall} is the dual.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let exists p l = can (find p) l

   let forall p l = not(exists ($not o p) l)
\end{verbatim}\end{hol}


\noindent The next function tests for membership of a list.

\begin{boxed}
\index{mem@\ml{mem}|pin}
\begin{verbatim}
   mem : * -> * list -> bool
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{mem\ $x$\ $l$} returns \ml{true} if some element of $l$ is equal to
$x$, otherwise it returns \ml{false}.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let mem = exists o (curry $=)
\end{verbatim}\end{hol}


\noindent The following two functions are \ML\ versions of Lisp's \ml{assoc}.

\begin{boxed}
\index{assoc@\ml{assoc}|pin}
\index{rev_assoc@\ml{rev\_assoc}|pin}
\begin{verbatim}
   assoc     : * -> (* # **) list -> (* # **)
   rev_assoc : * -> (** # *) list -> (** # *)
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{assoc\ $x$\ $l$} searches a list $l$ of pairs for one whose first component is
equal to $x$, returning the first pair found as result; similarly, 
\ml{rev\_assoc\ $y$\ $l$} searches for a pair whose second component is equal
to $y$. For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#assoc 2 [(1,4);(3,2);(2,5);(2,6)];;
(2, 5) : (int # int)

#rev_assoc 2 [(1,4);(3,2);(2,5);(2,6)];;
(3, 2) : (int # int)
\end{verbatim}\end{session}

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let assoc x     = find (\(x',y). x=x')

   let rev_assoc y = find (\(x,y'). y=y')
\end{verbatim}\end{hol}


\section{List transforming functions}

\noindent The next function reverses a list:

\begin{boxed}
\index{rev@\ml{rev}|pin}
\begin{verbatim}
   rev : * list -> * list
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{rev}\ \ml{[}x_1\ml{;}x_2\ml{;}\ldots\ml{;}x_n\ml{]} =
\ml{[}x_n\ml{;}\ldots\ml{;}x_2\ml{;}x_1\ml{]} \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let rev = rev1 []
    whererec rev1 l = fun [] . l | (x.l') . rev1 (x.l) l'
\end{verbatim}\end{hol}


\noindent The following two functions filter a list to the sublist of elements
satisfying a predicate.

\begin{boxed}
\index{filter@\ml{filter}|pin}
\index{mapfilter@\ml{mapfilter}|pin}
\begin{verbatim}
   filter    : (* -> bool) -> * list -> * list
   mapfilter : (* -> **) -> * list -> * list
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{filter\ $p$\ $l$} applies $p$ to every element of $l$, returning a list of
those that satisfy $p$; evaluating
\ml{mapfilter\ $f$\ $l$} applies $f$ to every element of $l$, returning
a list of results for those elements for which application of $f$ succeeds.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec filter p    = fun [] . []
                         |  (x.l) . if p x then (x.filter p l) else filter p l


   letrec mapfilter f = fun [] . []
                         |  (x.l) . let l' = mapfilter f l in (f x).l' ? l'
\end{verbatim}\end{hol}


\noindent The following three functions break-up lists.

\begin{boxed}
\index{remove@\ml{remove}|pin}
\index{chop_list@\ml{chop\_list}|pin}
\index{partition@\ml{partition}|pin}
\begin{verbatim}
   remove    : (* -> bool) -> * list -> (* # * list)
   partition : (* -> bool) -> * list -> (* list # * list)
   chop_list : int -> * list -> (* list # * list)
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{remove\ $p$\ $l$} separates from the rest of $l$ the first element that
satisfies the predicate $p$; it fails if no element satisfies the predicate.
\ml{partition\ $p$\ $l$} returns a pair of lists. The first list contains the
elements of $l$ which satisfy $p$. The second list contains all the other
elements of $l$.

\[ \ml{chop\_list}\ i\ \ml{[}x_1\ml{;}\ldots\ml{;}x_n\ml{]} =
\ml{([}x_1\ml{;}\ldots\ml{;}x_i\ml{],[}x_{i+1}\ml{;}\ldots\ml{;}x_n\ml{])} \]

\noindent \ml{chop\_list} fails if $i$ is negative or greater than $n$.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec remove p l =
    if p (hd l) then (hd l, tl l)
    else (I # (\r. ((hd l) . r))) (remove p (tl l))

   let partition p l =
    itlist (\a (yes,no). if p a then ((a.yes),no) else (yes,(a.no))) l ([],[])

   letrec chop_list i l =
    if i = 0 then ([],l)
    else (let l1,l2 = chop_list (i-1) (tl l) in  hd l . l1 , l2)
    ? failwith `chop_list`
\end{verbatim}\end{hol}


\noindent The next function flattens a list of lists:

\begin{boxed}
\index{flat@\ml{flat}|pin}
\begin{verbatim}
   flat : * list list -> * list
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \begin{array}{l}\ml{flat\ [[}l_{11}\ml{;}\ldots\ml{;}l_{1{m_1}}
\ml{];[}l_{21}\ml{;}\ldots\ml{;}l_{2{m_2}}\ml{];}\ \ldots\ 
\ml{;[}l_{n1}\ml{;}\ldots\ml{;}l_{n{m_n}}\ml{]]} =\\
\ \ \ml{[}l_{11}\ml{;}\ldots\ml{;}l_{1{m_1}}
\ml{;}l_{21}\ml{;}\ldots\ml{;}l_{2{m_2}}\ml{;}\ \ldots\ 
\ml{;}l_{n1}\ml{;}\ldots\ml{;}l_{n{m_n}}\ml{]}
\end{array} \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec flat = fun [] . [] | (x.l) . x@(flat l)
\end{verbatim}\end{hol}


\noindent The next two functions `zip' and `unzip' between lists of pairs
and pairs of lists.

\begin{boxed}
\index{combine@\ml{combine}|pin}
\index{split@\ml{split}|pin}
\begin{verbatim}
   combine : (* list # ** list) -> (* # **) list
   split   : (* # **) list -> (* list # ** list)
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{combine}\
\ml{([}x_1\ml{;}\ldots\ml{;}x_n\ml{],[}y_1\ml{;}\ldots\ml{;}y_n\ml{])} = 
\ml{[(}x_1\ml{,}y_1\ml{);}\ \ldots\ \ml{;(}x_n\ml{,}y_n\ml{)]} \]

\[ \ml{split}\
\ml{[(}x_1\ml{,}y_1\ml{);}\ \ldots\ \ml{;(}x_n\ml{,}y_n\ml{)]} =
\ml{([}x_1\ml{;}\ldots\ml{;}x_n\ml{],[}y_1\ml{;}\ldots\ml{;}y_n\ml{])} \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec combine = fun ([],[])         . []
                     |  ((x.lx),(y.ly)) . ((x,y).combine(lx,ly))
                     |  _               . failwith `combine`

   letrec split   = fun []        . ([],[])
                     |  ((x,y).l) . let lx,ly = split l in (x.lx,y.ly)
\end{verbatim}\end{hol}


\section{Functions for lists representing sets}

\noindent The following functions behave like the corresponding
set-theoretic operations on sets\index{sets, as ML lists@sets, as \ML\ lists}
(represented as
lists without repetitions).

\begin{boxed}
\index{intersect@\ml{intersect}|pin}
\index{subtract@\ml{subtract}|pin}
\index{union@\ml{union}|pin}
\begin{verbatim}
   intersect : * list -> * list -> * list
   subtract  : * list -> * list -> * list
   union     : * list -> * list -> * list
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \ml{intersect}\ l_1\ l_2 = l_1\cap l_2 \qquad
\ml{subtract}\ l_1\ l_2 = l_1-l_2 \qquad
\ml{union}\ l_1\ l_2 = l_1\cup l_2 \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let intersect l1 l2 = filter (\x. mem x l2) l1

   let subtract l1 l2  = filter (\x. not(mem x l2)) l1

   let union l1 l2     = l1 @ subtract l2 l1
\end{verbatim}\end{hol}


\noindent There are also functions to test if a list is a set, remove
duplicates from a list and test two lists for set equality.

\begin{boxed}
\index{distinct@\ml{distinct}|pin}
\index{setify@\ml{setify}|pin}
\index{set_equal@\ml{set\_equal}|pin}
\begin{verbatim}
   distinct  : * list -> bool
   setify    : * list -> * list
   set_equal : * list -> * list -> bool
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{distinct\ $l$} returns \ml{true} if all the elements of $l$ are distinct;
otherwise it returns \ml{false}. \ml{setify\ $l$} removes repeated elements
from $l$, leaving the last occurrence of each duplicate in the list.
\ml{set\_equal\ $l_1$\ $l_2$} returns \ml{true} if every element of $l_1$
appears in $l_2$ and every element of $l_2$ appears in $l_1$; otherwise it
returns \ml{false}.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   letrec distinct l =
    (null l) or (not (mem (hd l) (tl l)) & distinct (tl l))

   let setify l = itlist (\a s. if mem a s then s else a.s) l []

   let set_equal l1 l2 = (subtract l1 l2 = []) & (subtract l2 l1 = [])
\end{verbatim}\end{hol}


\section{Miscellaneous string processing functions}

\index{strings, in ML@strings, in \ML!processing functions for|(}
The following functions split strings into `words'; 
\ml{words2} uses a user supplied separator, while \ml{words} uses space and
carriage-return as separators.

\begin{boxed}
\index{words2@\ml{words2}|pin}
\index{words@\ml{words}|pin}
\begin{verbatim}
   words2 : string -> string -> string list
   words  : string -> string list
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\[ \begin{array}{ll}
\ml{words2\ `}c\ml{`\ `}s_1 c s_2 c \ldots c s_n\ml{`} &=
\ml{[`}s_1\ml{`;`}s_2\ml{`;}\ \ldots\ \ml{;`}s_n\ml{`]}\\
 & \\
\ml{words\ `}s_1\ s_2\ \ldots\ s_n\ml{`} &=
\ml{[`}s_1\ml{`;`}s_2\ml{`;}\ \ldots\ \ml{;`}s_n\ml{`]}\\
\end{array} \]

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let words2 sep string =
    snd (itlist (\ch (chs,tokl).
                    if ch = sep then
                       if null chs then [],tokl
                       else [], (implode chs . tokl)
                    else (ch.chs), tokl)
                (sep . explode string)
                ([],[]))
\end{verbatim}\end{hol}
\begin{hol}\begin{verbatim}
   let word_separators = [` `;`\L`]

   let words string =
    snd (itlist (\ch (chs,tokl).
                    if mem ch word_separators then
                       if null chs then [],tokl
                       else [], (implode chs . tokl)
                    else (ch.chs), tokl)
                (` ` . explode string)
                ([],[]))
\end{verbatim}\end{hol}


\noindent The next three functions (the second of which is an infixed version of
the first) are string concatenation operators.

\begin{boxed}
\index{concat@\ml{concat}|pin}
\index{concatl@\ml{concatl}|pin}
\index{ string concatenation, in ML@{\small\verb+^+} (string concatenation, in \ML)|pin}
\begin{verbatim}
   concat  : string -> string -> string
   $^      : string -> string -> string
   concatl : string list -> string
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{concat}
\index{concatenation, of ML strings@concatenation, of \ML\ strings}
concatenates two strings, {\small\verb%$^%} is an infixed version
of \ml{concat},
and \ml{concatl} concatenates all the strings in a list of strings.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let concat s1 s2 = implode(explode s1 @ explode s2)

   ml_curried_infix `^`
   let s1 ^ s2 = concat s1 s2

   let concatl sl = implode(itlist append (map explode sl) [])
\end{verbatim}\end{hol}
\index{strings, in ML@strings, in \ML!processing functions for|)}


\section{Failure handling functions}

The failure\index{failure, in ML@failure, in \ML!backtrace functions for}
 handling functions described here are useful for writing code that
fails with a backtrace\index{backtrace}.

\begin{boxed}
\index{set_fail@\ml{set\_fail}|pin}
\index{set_fail_prefix@\ml{set\_fail\_prefix}|pin}
\begin{verbatim}
   set_fail_prefix : string -> (* -> **) -> * -> **
   set_fail        : string -> (* -> **) -> * -> **
\end{verbatim}\end{boxed}

\subsubsection*{Description}

\ml{set\_fail\_prefix\ $s$\ $f$\ $x$} applies $f$ to $x$ and returns the
result of the application if it is successful; if the application fails then
the string $s$ is concatenated to the failure string and the resulting string
propagated as the new failure string.

\noindent
\ml{set\_fail\ $s$\ $f$\ $x$} applies $f$ to $x$ and returns the result of
the application if it is successful; if the application fails then the string
$s$ is propagated as the new failure string.

\subsubsection*{Definition}

\begin{hol}\begin{verbatim}
   let set_fail_prefix s f x = f x ?\s' failwith(concatl[s;`--`;s'])

   let set_fail s f x        = f x ? failwith s
\end{verbatim}\end{hol}

