%

\begin{isabellebody}%

\def\isabellecontext{Program}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

\isacommand{theory}\isamarkupfalse%

\ Program\isanewline

\isakeyword{imports}\ Introduction\isanewline

\isakeyword{begin}%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isamarkupsection{Turning Theories into Programs \label{sec:program}%

}

\isamarkuptrue%

%

\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

We have already seen how by default equations stemming from

  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}

  statements are used for code generation.  This default behaviour

  can be changed, e.g. by providing different code equations.

  All kinds of customisation shown in this section is \emph{safe}

  in the sense that the user does not have to worry about

  correctness -- all programs generatable that way are partially

  correct.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Selecting code equations%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Coming back to our introductory example, we

  could provide an alternative code equations for \isa{dequeue}

  explicitly:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{lemma}\isamarkupfalse%

\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline

\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline

\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline

\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}

  \isa{attribute} which states that the given theorems should be

  considered as code equations for a \isa{fun} statement --

  the corresponding constant is determined syntactically.  The resulting code:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\

\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\

\hspace*{0pt}dequeue (AQueue xs []) =\\

\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\

\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been

  replaced by the predicate \isa{null\ xs}.  This is due to the default

  setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).

  Changing the default constructor set of datatypes is also

  possible.  See \secref{sec:datatypes} for an example.

  As told in \secref{sec:concept}, code generation is based

  on a structured collection of code theorems.

  For explorative purpose, this collection

  may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%

\ dequeue%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent prints a table with \emph{all} code equations

  for \isa{dequeue}, including

  \emph{all} code equations those equations depend

  on recursively.

  Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph

  visualising dependencies between code equations.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{\isa{class} and \isa{instantiation}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Concerning type classes and code generation, let us examine an example

  from abstract algebra:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{class}\isamarkupfalse%

\ semigroup\ {\isacharequal}\isanewline

\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline

\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{class}\isamarkupfalse%

\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline

\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline

\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline

\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{instantiation}\isamarkupfalse%

\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline

\isakeyword{begin}\isanewline

\isanewline

\isacommand{primrec}\isamarkupfalse%

\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline

\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{lemma}\isamarkupfalse%

\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline

\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline

\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline

\ \ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline

\isanewline

\isacommand{instance}\isamarkupfalse%

\ \isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \isacommand{fix}\isamarkupfalse%

\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline

\ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ \ \ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline

\ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline

\ \ \ \ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline

\ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline

\ \ \ \ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline

\isacommand{qed}\isamarkupfalse%

\isanewline

\isanewline

\isacommand{end}\isamarkupfalse%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent We define the natural operation of the natural numbers

  on monoids:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{primrec}\isamarkupfalse%

\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline

\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent This we use to define the discrete exponentiation function:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{definition}\isamarkupfalse%

\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent The corresponding code:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}module Example where {\char123}\\

\hspace*{0pt}\\

\hspace*{0pt}\\

\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\

\hspace*{0pt}\\

\hspace*{0pt}class Semigroup a where {\char123}\\

\hspace*{0pt} ~mult ::~a -> a -> a;\\

\hspace*{0pt}{\char125};\\

\hspace*{0pt}\\

\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\

\hspace*{0pt} ~neutral ::~a;\\

\hspace*{0pt}{\char125};\\

\hspace*{0pt}\\

\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\

\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\

\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\

\hspace*{0pt}\\

\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\

\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\

\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\

\hspace*{0pt}\\

\hspace*{0pt}neutral{\char95}nat ::~Nat;\\

\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\

\hspace*{0pt}\\

\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\

\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\

\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\

\hspace*{0pt}\\

\hspace*{0pt}instance Semigroup Nat where {\char123}\\

\hspace*{0pt} ~mult = mult{\char95}nat;\\

\hspace*{0pt}{\char125};\\

\hspace*{0pt}\\

\hspace*{0pt}instance Monoid Nat where {\char123}\\

\hspace*{0pt} ~neutral = neutral{\char95}nat;\\

\hspace*{0pt}{\char125};\\

\hspace*{0pt}\\

\hspace*{0pt}bexp ::~Nat -> Nat;\\

\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\

\hspace*{0pt}\\

\hspace*{0pt}{\char125}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent This is a convenient place to show how explicit dictionary construction

  manifests in generated code (here, the same example in \isa{SML}):%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}structure Example = \\

\hspace*{0pt}struct\\

\hspace*{0pt}\\

\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\

\hspace*{0pt}\\

\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\

\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\

\hspace*{0pt}\\

\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\

\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\

\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\

\hspace*{0pt}\\

\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\

\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\

\hspace*{0pt}\\

\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\

\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\

\hspace*{0pt}\\

\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\

\hspace*{0pt}\\

\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\

\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\

\hspace*{0pt}\\

\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\

\hspace*{0pt}\\

\hspace*{0pt}val monoid{\char95}nat =\\

\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\

\hspace*{0pt} ~nat monoid;\\

\hspace*{0pt}\\

\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\

\hspace*{0pt}\\

\hspace*{0pt}end;~(*struct Example*)%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent Note the parameters with trailing underscore (\verb|A_|)

    which are the dictionary parameters.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{The preprocessor \label{sec:preproc}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Before selected function theorems are turned into abstract

  code, a chain of definitional transformation steps is carried

  out: \emph{preprocessing}.  In essence, the preprocessor

  consists of two components: a \emph{simpset} and \emph{function transformers}.

  The \emph{simpset} allows to employ the full generality of the Isabelle

  simplifier.  Due to the interpretation of theorems

  as code equations, rewrites are applied to the right

  hand side and the arguments of the left hand side of an

  equation, but never to the constant heading the left hand side.

  An important special case are \emph{inline theorems} which may be

  declared and undeclared using the

  \emph{code inline} or \emph{code inline del} attribute respectively.

  Some common applications:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\begin{itemize}

%

\begin{isamarkuptext}%

\item replacing non-executable constructs by executable ones:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{lemma}\isamarkupfalse%

\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\item eliminating superfluous constants:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{lemma}\isamarkupfalse%

\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

\ simp%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\item replacing executable but inconvenient constructs:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{lemma}\isamarkupfalse%

\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\end{itemize}

%

\begin{isamarkuptext}%

\noindent \emph{Function transformers} provide a very general interface,

  transforming a list of function theorems to another

  list of function theorems, provided that neither the heading

  constant nor its type change.  The \isa{{\isadigit{0}}} / \isa{Suc}

  pattern elimination implemented in

  theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this

  interface.

  \noindent The current setup of the preprocessor may be inspected using

  the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.

  \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient

  mechanism to inspect the impact of a preprocessor setup

  on code equations.

  \begin{warn}

    The attribute \emph{code unfold}

    associated with the \isa{SML\ code\ generator} also applies to

    the \isa{generic\ code\ generator}:

    \emph{code unfold} implies \emph{code inline}.

  \end{warn}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Datatypes \label{sec:datatypes}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Conceptually, any datatype is spanned by a set of

  \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in

  \isa{{\isasymtau}}.  The HOL datatype package by default registers any new

  datatype in the table of datatypes, which may be inspected using the

  \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.

  In some cases, it is appropriate to alter or extend this table.  As

  an example, we will develop an alternative representation of the

  queue example given in \secref{sec:intro}.  The amortised

  representation is convenient for generating code but exposes its

  \qt{implementation} details, which may be cumbersome when proving

  theorems about it.  Therefore, here a simple, straightforward

  representation of queues:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{datatype}\isamarkupfalse%

\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{primrec}\isamarkupfalse%

\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{fun}\isamarkupfalse%

\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent This we can use directly for proving;  for executing,

  we provide an alternative characterisation:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{definition}\isamarkupfalse%

\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%

\ AQueue%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent Here we define a \qt{constructor} \isa{AQueue} which

  is defined in terms of \isa{Queue} and interprets its arguments

  according to what the \emph{content} of an amortised queue is supposed

  to be.  Equipped with this, we are able to prove the following equations

  for our primitive queue operations which \qt{implement} the simple

  queues in an amortised fashion:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{lemma}\isamarkupfalse%

\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline

\ \ \isacommand{unfolding}\isamarkupfalse%

\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\isanewline

\isacommand{lemma}\isamarkupfalse%

\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline

\ \ \isacommand{unfolding}\isamarkupfalse%

\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\isanewline

\isacommand{lemma}\isamarkupfalse%

\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline

\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline

\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ \isacommand{unfolding}\isamarkupfalse%

\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp{\isacharunderscore}all%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent For completeness, we provide a substitute for the

  \isa{case} combinator on queues:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{lemma}\isamarkupfalse%

\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ \isacommand{unfolding}\isamarkupfalse%

\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent The resulting code looks as expected:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}structure Example = \\

\hspace*{0pt}struct\\

\hspace*{0pt}\\

\hspace*{0pt}fun foldl f a [] = a\\

\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\

\hspace*{0pt}\\

\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\

\hspace*{0pt}\\

\hspace*{0pt}fun null [] = true\\

\hspace*{0pt} ~| null (x ::~xs) = false;\\

\hspace*{0pt}\\

\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\

\hspace*{0pt}\\

\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\

\hspace*{0pt}\\

\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\

\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\

\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\

\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\

\hspace*{0pt}\\

\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\

\hspace*{0pt}\\

\hspace*{0pt}end;~(*struct Example*)%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent From this example, it can be glimpsed that using own

  constructor sets is a little delicate since it changes the set of

  valid patterns for values of that type.  Without going into much

  detail, here some practical hints:

  \begin{itemize}

    \item When changing the constructor set for datatypes, take care

      to provide alternative equations for the \isa{case} combinator.

    \item Values in the target language need not to be normalised --

      different values in the target language may represent the same

      value in the logic.

    \item Usually, a good methodology to deal with the subtleties of

      pattern matching is to see the type as an abstract type: provide

      a set of operations which operate on the concrete representation

      of the type, and derive further operations by combinations of

      these primitive ones, without relying on a particular

      representation.

  \end{itemize}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Equality%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Surely you have already noticed how equality is treated

  by the code generator:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{primrec}\isamarkupfalse%

\ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline

\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline

\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline

\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline

\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline

\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent The membership test during preprocessing is rewritten,

  resulting in \isa{op\ mem}, which itself

  performs an explicit equality check.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}structure Example = \\

\hspace*{0pt}struct\\

\hspace*{0pt}\\

\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\

\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\

\hspace*{0pt}\\

\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\

\hspace*{0pt}\\

\hspace*{0pt}fun member A{\char95}~x [] = false\\

\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\

\hspace*{0pt}\\

\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\

\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\

\hspace*{0pt} ~~~(if member A{\char95}~z xs\\

\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\

\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\

\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\

\hspace*{0pt}\\

\hspace*{0pt}end;~(*struct Example*)%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent Obviously, polymorphic equality is implemented the Haskell

  way using a type class.  How is this achieved?  HOL introduces

  an explicit class \isa{eq} with a corresponding operation

  \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.

  The preprocessing framework does the rest by propagating the

  \isa{eq} constraints through all dependent code equations.

  For datatypes, instances of \isa{eq} are implicitly derived

  when possible.  For other types, you may instantiate \isa{eq}

  manually like any other type class.

  Though this \isa{eq} class is designed to get rarely in

  the way, in some cases the automatically derived code equations

  for equality on a particular type may not be appropriate.

  As example, watch the following datatype representing

  monomorphic parametric types (where type constructors

  are referred to by natural numbers):%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{datatype}\isamarkupfalse%

\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Then code generation for SML would fail with a message

  that the generated code contains illegal mutual dependencies:

  the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the

  instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires

  \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}};  Haskell has no problem with mutually

  recursive \isa{instance} and \isa{function} definitions,

  but the SML serialiser does not support this.

  In such cases, you have to provide your own equality equations

  involving auxiliary constants.  In our case,

  \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{lemma}\isamarkupfalse%

\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline

\ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline

\ \ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}structure Example = \\

\hspace*{0pt}struct\\

\hspace*{0pt}\\

\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\

\hspace*{0pt}\\

\hspace*{0pt}fun null [] = true\\

\hspace*{0pt} ~| null (x ::~xs) = false;\\

\hspace*{0pt}\\

\hspace*{0pt}fun eq{\char95}nat (Suc nat') Zero{\char95}nat = false\\

\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc nat') = false\\

\hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\

\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\

\hspace*{0pt}\\

\hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\

\hspace*{0pt}\\

\hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\

\hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\

\hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\

\hspace*{0pt}\\

\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\

\hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\

\hspace*{0pt}\\

\hspace*{0pt}end;~(*struct Example*)%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\isamarkupsubsection{Explicit partiality%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Partiality usually enters the game by partial patterns, as

  in the following example, again for amortised queues:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{definition}\isamarkupfalse%

\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline

\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{lemma}\isamarkupfalse%

\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline

\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ \isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent In the corresponding code, there is no equation

  for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\

\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\

\hspace*{0pt} ~let {\char123}\\

\hspace*{0pt} ~~~(y :~ys) = rev xs;\\

\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\

\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent In some cases it is desirable to have this

  pseudo-\qt{partiality} more explicitly, e.g.~as follows:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote