%
\begin{isabellebody}%
\def\isabellecontext{Foundations}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Foundations\isanewline
\isakeyword{imports}\ Introduction\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsection{Code generation foundations \label{sec:foundations}%
}
\isamarkuptrue%
%
\isamarkupsubsection{Code generator architecture \label{sec:architecture}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The code generator is actually a framework consisting of different
components which can be customised individually.
Conceptually all components operate on Isabelle's logic framework
\hyperlink{theory.Pure}{\mbox{\isa{Pure}}}. Practically, the object logic \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}
provides the necessary facilities to make use of the code generator,
mainly since it is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}.
The constellation of the different components is visualized in the
following picture.
\begin{figure}[h]
\includegraphics{architecture}
\caption{Code generator architecture}
\label{fig:arch}
\end{figure}
\noindent Central to code generation is the notion of \emph{code
equations}. A code equation as a first approximation is a theorem
of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t} (an equation headed by a
constant \isa{f} with arguments \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right
hand side \isa{t}).
\begin{itemize}
\item Starting point of code generation is a collection of (raw)
code equations in a theory. It is not relevant where they stem
from, but typically they were either produced by specification
tools or proved explicitly by the user.
\item These raw code equations can be subjected to theorem
transformations. This \qn{preprocessor} (see
\secref{sec:preproc}) can apply the full expressiveness of
ML-based theorem transformations to code generation. The result
of preprocessing is a structured collection of code equations.
\item These code equations are \qn{translated} to a program in an
abstract intermediate language. Think of it as a kind of
\qt{Mini-Haskell} with four \qn{statements}: \isa{data} (for
datatypes), \isa{fun} (stemming from code equations), also
\isa{class} and \isa{inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into
concrete source code of a target language. This step only
produces concrete syntax but does not change the program in
essence; all conceptual transformations occur in the translation
step.
\end{itemize}
\noindent From these steps, only the last two are carried out
outside the logic; by keeping this layer as thin as possible, the
amount of code to trust is kept to a minimum.%
\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}. The preprocessor consists of two
components: a \emph{simpset} and \emph{function transformers}.
The \emph{simpset} can apply 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{unfold theorems}, which may be declared and removed using the
\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} 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{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\item replacing executable but inconvenient constructs:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\item eliminating disturbing expressions:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
\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 \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}} (see
\secref{eff_nat}) uses this interface.
\noindent The current setup of the preprocessor may be inspected
using the \indexdef{}{command}{print\_codeproc}\hypertarget{command.print-codeproc}{\hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}} command. \indexdef{}{command}{code\_thms}\hypertarget{command.code-thms}{\hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}} (see \secref{sec:equations}) provides a convenient
mechanism to inspect the impact of a preprocessor setup on code
equations.
\begin{warn}
Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
preprocessor of the ancient \isa{SML\ code\ generator}; in case
this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Understanding code equations \label{sec:equations}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
As told in \secref{sec:principle}, the notion of code equations is
vital to code generation. Indeed most problems which occur in
practice can be resolved by an inspection of the underlying code
equations.
It is possible to exchange the default code equations for constants
by explicitly proving alternative ones:%
\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{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.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
\hspace*{0pt}dequeue (Example.AQueue xs []) =\\
\hspace*{0pt} ~(if null xs then (Nothing,~Example.AQueue [] [])\\
\hspace*{0pt} ~~~else Example.dequeue (Example.AQueue [] (reverse 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{List{\isachardot}null\ xs}. This is due
to the default setup of the \qn{preprocessor}.
This possibility to select arbitrary code equations is the key
technique for program and datatype refinement (see
\secref{sec:refinement}.
Due to the preprocessor, there is the distinction of raw code
equations (before preprocessing) and code equations (after
preprocessing).
The first can be listed (among other data) using the \indexdef{}{command}{print\_codesetup}\hypertarget{command.print-codesetup}{\hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}} command.
The code equations after preprocessing are already are blueprint of
the generated program and can 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 This prints a table with the code equations for \isa{dequeue}, including \emph{all} code equations those equations depend
on recursively. These dependencies themselves can be visualized using
the \indexdef{}{command}{code\_deps}\hypertarget{command.code-deps}{\hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}} command.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Equality%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Implementation of equality deserves some attention. Here an example
function involving polymorphic equality:%
\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 During preprocessing, the membership test is rewritten,
resulting in \isa{List{\isachardot}member}, which itself performs an explicit
equality check, as can be seen in the corresponding \isa{SML} code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
%
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
\hspace*{0pt} ~type 'a equal\\
\hspace*{0pt} ~val equal :~'a equal -> 'a -> 'a -> bool\\
\hspace*{0pt} ~val eq :~'a equal -> 'a -> 'a -> bool\\
\hspace*{0pt} ~val member :~'a equal -> 'a list -> 'a -> bool\\
\hspace*{0pt} ~val collect{\char95}duplicates :\\
\hspace*{0pt} ~~~'a equal -> 'a list -> 'a list -> 'a list -> 'a list\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a equal = {\char123}equal :~'a -> 'a -> bool{\char125};\\
\hspace*{0pt}val equal = {\char35}equal :~'a equal -> 'a -> 'a -> bool;\\
\hspace*{0pt}\\
\hspace*{0pt}fun eq A{\char95}~a b = equal A{\char95}~a b;\\
\hspace*{0pt}\\
\hspace*{0pt}fun member A{\char95}~[] y = false\\
\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eq A{\char95}~x y orelse member A{\char95}~xs y;\\
\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}~xs z\\
\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z 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{equal} with a corresponding operation \isa{equal{\isacharunderscore}class{\isachardot}equal} such that \isa{equal{\isacharunderscore}class{\isachardot}equal\ {\isacharequal}\ op\ {\isacharequal}}. The preprocessing
framework does the rest by propagating the \isa{equal} constraints
through all dependent code equations. For datatypes, instances of
\isa{equal} are implicitly derived when possible. For other types,
you may instantiate \isa{equal} manually like any other type class.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Explicit partiality \label{sec: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{\isacharparenright}\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ list{\isachardot}split{\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.~Example.Queue a -> (a,~Example.Queue a);\\
\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
\hspace*{0pt} ~let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
\hspace*{0pt} ~{\char125}~in (y,~Example.AQueue [] ys);\\
\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.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
\isacommand{axiomatization}\isamarkupfalse%
\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
Normally, if constants without any code equations occur in a
program, the code generator complains (since in most cases this is
indeed an error). But such constants can also be thought
of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
explicitly, use \indexdef{}{command}{code\_abort}\hypertarget{command.code-abort}{\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
\ empty{\isacharunderscore}queue%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Then the code generator will just insert an error or
exception at the appropriate position:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
%
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
\hspace*{0pt}\\
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);\\
\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
\hspace*{0pt} ~(if null xs then Example.empty{\char95}queue\\
\hspace*{0pt} ~~~else Example.strict{\char95}dequeue (Example.AQueue [] (reverse xs)));%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This feature however is rarely needed in practice. Note
also that the HOL default setup already declares \isa{undefined}
as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most likely to be used in such
situations.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{If something goes utterly wrong \label{sec:utterly_wrong}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Under certain circumstances, the code generator fails to produce
code entirely. To debug these, the following hints may prove
helpful:
\begin{description}
\ditem{\emph{Check with a different target language}.} Sometimes
the situation gets more clear if you switch to another target
language; the code generated there might give some hints what
prevents the code generator to produce code for the desired
language.
\ditem{\emph{Inspect code equations}.} Code equations are the central
carrier of code generation. Most problems occuring while generation
code can be traced to single equations which are printed as part of
the error message. A closer inspection of those may offer the key
for solving issues (cf.~\secref{sec:equations}).
\ditem{\emph{Inspect preprocessor setup}.} The preprocessor might
transform code equations unexpectedly; to understand an
inspection of its setup is necessary (cf.~\secref{sec:preproc}).
\ditem{\emph{Generate exceptions}.} If the code generator
complains about missing code equations, in can be helpful to
implement the offending constants as exceptions
(cf.~\secref{sec:partiality}); this allows at least for a formal
generation of code, whose inspection may then give clues what is
wrong.
\ditem{\emph{Remove offending code equations}.} If code
generation is prevented by just a single equation, this can be
removed (cf.~\secref{sec:equations}) to allow formal code
generation, whose result in turn can be used to trace the
problem. The most prominent case here are mismatches in type
class signatures (\qt{wellsortedness error}).
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: