3 \def\isabellecontext{Foundations}%
10 \isacommand{theory}\isamarkupfalse%
11 \ Foundations\isanewline
12 \isakeyword{imports}\ Introduction\isanewline
21 \isamarkupsection{Code generation foundations \label{sec:foundations}%
25 \isamarkupsubsection{Code generator architecture \label{sec:architecture}%
29 \begin{isamarkuptext}%
30 The code generator is actually a framework consisting of different
31 components which can be customised individually.
33 Conceptually all components operate on Isabelle's logic framework
34 \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}. Practically, the object logic \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}
35 provides the necessary facilities to make use of the code generator,
36 mainly since it is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}.
38 The constellation of the different components is visualized in the
42 \includegraphics{architecture}
43 \caption{Code generator architecture}
47 \noindent Central to code generation is the notion of \emph{code
48 equations}. A code equation as a first approximation is a theorem
49 of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t} (an equation headed by a
50 constant \isa{f} with arguments \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right
55 \item Starting point of code generation is a collection of (raw)
56 code equations in a theory. It is not relevant where they stem
57 from, but typically they were either produced by specification
58 tools or proved explicitly by the user.
60 \item These raw code equations can be subjected to theorem
61 transformations. This \qn{preprocessor} (see
62 \secref{sec:preproc}) can apply the full expressiveness of
63 ML-based theorem transformations to code generation. The result
64 of preprocessing is a structured collection of code equations.
66 \item These code equations are \qn{translated} to a program in an
67 abstract intermediate language. Think of it as a kind of
68 \qt{Mini-Haskell} with four \qn{statements}: \isa{data} (for
69 datatypes), \isa{fun} (stemming from code equations), also
70 \isa{class} and \isa{inst} (for type classes).
72 \item Finally, the abstract program is \qn{serialised} into
73 concrete source code of a target language. This step only
74 produces concrete syntax but does not change the program in
75 essence; all conceptual transformations occur in the translation
80 \noindent From these steps, only the last two are carried out
81 outside the logic; by keeping this layer as thin as possible, the
82 amount of code to trust is kept to a minimum.%
86 \isamarkupsubsection{The preprocessor \label{sec:preproc}%
90 \begin{isamarkuptext}%
91 Before selected function theorems are turned into abstract code, a
92 chain of definitional transformation steps is carried out:
93 \emph{preprocessing}. The preprocessor consists of two
94 components: a \emph{simpset} and \emph{function transformers}.
96 The \emph{simpset} can apply the full generality of the Isabelle
97 simplifier. Due to the interpretation of theorems as code
98 equations, rewrites are applied to the right hand side and the
99 arguments of the left hand side of an equation, but never to the
100 constant heading the left hand side. An important special case are
101 \emph{unfold theorems}, which may be declared and removed using the
102 \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
103 attribute, respectively.
105 Some common applications:%
111 \begin{isamarkuptext}%
112 \item replacing non-executable constructs by executable ones:%
121 \isacommand{lemma}\isamarkupfalse%
122 \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
123 \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
124 \ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}%
132 \begin{isamarkuptext}%
133 \item replacing executable but inconvenient constructs:%
142 \isacommand{lemma}\isamarkupfalse%
143 \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
144 \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
145 \ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}%
153 \begin{isamarkuptext}%
154 \item eliminating disturbing expressions:%
163 \isacommand{lemma}\isamarkupfalse%
164 \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
165 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
166 \ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
176 \begin{isamarkuptext}%
177 \noindent \emph{Function transformers} provide a very general
178 interface, transforming a list of function theorems to another list
179 of function theorems, provided that neither the heading constant nor
180 its type change. The \isa{{\isadigit{0}}} / \isa{Suc} pattern
181 elimination implemented in theory \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}} (see
182 \secref{eff_nat}) uses this interface.
184 \noindent The current setup of the preprocessor may be inspected
185 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
186 mechanism to inspect the impact of a preprocessor setup on code
190 Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
191 preprocessor of the ancient \isa{SML\ code\ generator}; in case
192 this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
197 \isamarkupsubsection{Understanding code equations \label{sec:equations}%
201 \begin{isamarkuptext}%
202 As told in \secref{sec:principle}, the notion of code equations is
203 vital to code generation. Indeed most problems which occur in
204 practice can be resolved by an inspection of the underlying code
207 It is possible to exchange the default code equations for constants
208 by explicitly proving alternative ones:%
217 \isacommand{lemma}\isamarkupfalse%
218 \ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
219 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
220 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
221 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
222 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
223 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
224 \ \ \isacommand{by}\isamarkupfalse%
225 \ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
233 \begin{isamarkuptext}%
234 \noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{attribute}
235 which states that the given theorems should be considered as code
236 equations for a \isa{fun} statement -- the corresponding constant
237 is determined syntactically. The resulting code:%
247 \begin{isamarkuptext}%
250 \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
251 \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
252 \hspace*{0pt}dequeue (AQueue xs []) =\\
253 \hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
254 \hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
265 \begin{isamarkuptext}%
266 \noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has
267 been replaced by the predicate \isa{List{\isachardot}null\ xs}. This is due
268 to the default setup of the \qn{preprocessor}.
270 This possibility to select arbitrary code equations is the key
271 technique for program and datatype refinement (see
272 \secref{sec:refinement}.
274 Due to the preprocessor, there is the distinction of raw code
275 equations (before preprocessing) and code equations (after
278 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.
280 The code equations after preprocessing are already are blueprint of
281 the generated program and can be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
290 \isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
299 \begin{isamarkuptext}%
300 \noindent This prints a table with the code equations for \isa{dequeue}, including \emph{all} code equations those equations depend
301 on recursively. These dependencies themselves can be visualized using
302 the \indexdef{}{command}{code\_deps}\hypertarget{command.code-deps}{\hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}} command.%
306 \isamarkupsubsection{Equality%
310 \begin{isamarkuptext}%
311 Implementation of equality deserves some attention. Here an example
312 function involving polymorphic equality:%
321 \isacommand{primrec}\isamarkupfalse%
322 \ 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
323 \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
324 {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
325 \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
326 \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
327 \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
328 \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
336 \begin{isamarkuptext}%
337 \noindent During preprocessing, the membership test is rewritten,
338 resulting in \isa{List{\isachardot}member}, which itself performs an explicit
339 equality check, as can be seen in the corresponding \isa{SML} code:%
349 \begin{isamarkuptext}%
352 \hspace*{0pt}structure Example :~sig\\
353 \hspace*{0pt} ~type 'a equal\\
354 \hspace*{0pt} ~val equal :~'a equal -> 'a -> 'a -> bool\\
355 \hspace*{0pt} ~val eq :~'a equal -> 'a -> 'a -> bool\\
356 \hspace*{0pt} ~val member :~'a equal -> 'a list -> 'a -> bool\\
357 \hspace*{0pt} ~val collect{\char95}duplicates :\\
358 \hspace*{0pt} ~~~'a equal -> 'a list -> 'a list -> 'a list -> 'a list\\
359 \hspace*{0pt}end = struct\\
361 \hspace*{0pt}type 'a equal = {\char123}equal :~'a -> 'a -> bool{\char125};\\
362 \hspace*{0pt}val equal = {\char35}equal :~'a equal -> 'a -> 'a -> bool;\\
364 \hspace*{0pt}fun eq A{\char95}~a b = equal A{\char95}~a b;\\
366 \hspace*{0pt}fun member A{\char95}~[] y = false\\
367 \hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eq A{\char95}~x y orelse member A{\char95}~xs y;\\
369 \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
370 \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
371 \hspace*{0pt} ~~~(if member A{\char95}~xs z\\
372 \hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
373 \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
374 \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
376 \hspace*{0pt}end;~(*struct Example*)%
387 \begin{isamarkuptext}%
388 \noindent Obviously, polymorphic equality is implemented the Haskell
389 way using a type class. How is this achieved? HOL introduces an
390 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
391 framework does the rest by propagating the \isa{equal} constraints
392 through all dependent code equations. For datatypes, instances of
393 \isa{equal} are implicitly derived when possible. For other types,
394 you may instantiate \isa{equal} manually like any other type class.%
398 \isamarkupsubsection{Explicit partiality \label{sec:partiality}%
402 \begin{isamarkuptext}%
403 Partiality usually enters the game by partial patterns, as
404 in the following example, again for amortised queues:%
413 \isacommand{definition}\isamarkupfalse%
414 \ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
415 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
416 \ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
418 \isacommand{lemma}\isamarkupfalse%
419 \ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
420 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
421 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
422 \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
423 \ \ \isacommand{by}\isamarkupfalse%
424 \ {\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}%
432 \begin{isamarkuptext}%
433 \noindent In the corresponding code, there is no equation
434 for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
444 \begin{isamarkuptext}%
447 \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
448 \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
449 \hspace*{0pt} ~let {\char123}\\
450 \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
451 \hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
452 \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
463 \begin{isamarkuptext}%
464 \noindent In some cases it is desirable to have this
465 pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
474 \isacommand{axiomatization}\isamarkupfalse%
475 \ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
477 \isacommand{definition}\isamarkupfalse%
478 \ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
479 \ \ {\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
481 \isacommand{lemma}\isamarkupfalse%
482 \ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
483 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
484 \ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
485 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
486 \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
487 \ \ \isacommand{by}\isamarkupfalse%
488 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
496 \begin{isamarkuptext}%
497 Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
499 Normally, if constants without any code equations occur in a
500 program, the code generator complains (since in most cases this is
501 indeed an error). But such constants can also be thought
502 of as function definitions which always fail,
503 since there is never a successful pattern match on the left hand
504 side. In order to categorise a constant into that category
505 explicitly, use \indexdef{}{command}{code\_abort}\hypertarget{command.code-abort}{\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}}:%
514 \isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
515 \ empty{\isacharunderscore}queue%
523 \begin{isamarkuptext}%
524 \noindent Then the code generator will just insert an error or
525 exception at the appropriate position:%
535 \begin{isamarkuptext}%
538 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
539 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
541 \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
542 \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
543 \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
544 \hspace*{0pt} ~(if null xs then empty{\char95}queue\\
545 \hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
556 \begin{isamarkuptext}%
557 \noindent This feature however is rarely needed in practice. Note
558 also that the HOL default setup already declares \isa{undefined}
559 as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most likely to be used in such
564 \isamarkupsubsection{If something goes utterly wrong \label{sec:utterly_wrong}%
568 \begin{isamarkuptext}%
569 Under certain circumstances, the code generator fails to produce
570 code entirely. To debug these, the following hints may prove
575 \ditem{\emph{Check with a different target language}.} Sometimes
576 the situation gets more clear if you switch to another target
577 language; the code generated there might give some hints what
578 prevents the code generator to produce code for the desired
581 \ditem{\emph{Inspect code equations}.} Code equations are the central
582 carrier of code generation. Most problems occuring while generation
583 code can be traced to single equations which are printed as part of
584 the error message. A closer inspection of those may offer the key
585 for solving issues (cf.~\secref{sec:equations}).
587 \ditem{\emph{Inspect preprocessor setup}.} The preprocessor might
588 transform code equations unexpectedly; to understand an
589 inspection of its setup is necessary (cf.~\secref{sec:preproc}).
591 \ditem{\emph{Generate exceptions}.} If the code generator
592 complains about missing code equations, in can be helpful to
593 implement the offending constants as exceptions
594 (cf.~\secref{sec:partiality}); this allows at least for a formal
595 generation of code, whose inspection may then give clues what is
598 \ditem{\emph{Remove offending code equations}.} If code
599 generation is prevented by just a single equation, this can be
600 removed (cf.~\secref{sec:equations}) to allow formal code
601 generation, whose result in turn can be used to trace the
602 problem. The most prominent case here are mismatches in type
603 class signatures (\qt{wellsortedness error}).
614 \isacommand{end}\isamarkupfalse%
626 %%% TeX-master: "root"