author | haftmann |
Thu, 23 Sep 2010 15:46:17 +0200 | |
changeset 39664 | 0afaf89ab591 |
parent 39210 | 985b13c5a61d |
child 39683 | f75a01ee6c41 |
permissions | -rw-r--r-- |
38406 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Foundations}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Foundations\isanewline |
|
12 |
\isakeyword{imports}\ Introduction\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
38437 | 21 |
\isamarkupsection{Code generation foundations \label{sec:foundations}% |
38406 | 22 |
} |
23 |
\isamarkuptrue% |
|
24 |
% |
|
38437 | 25 |
\isamarkupsubsection{Code generator architecture \label{sec:architecture}% |
38406 | 26 |
} |
27 |
\isamarkuptrue% |
|
28 |
% |
|
29 |
\begin{isamarkuptext}% |
|
38437 | 30 |
The code generator is actually a framework consisting of different |
31 |
components which can be customised individually. |
|
32 |
||
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}}}. |
|
37 |
||
38 |
The constellation of the different components is visualized in the |
|
39 |
following picture. |
|
40 |
||
41 |
\begin{figure}[h] |
|
42 |
\includegraphics{architecture} |
|
43 |
\caption{Code generator architecture} |
|
44 |
\label{fig:arch} |
|
45 |
\end{figure} |
|
46 |
||
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 |
|
51 |
hand side \isa{t}). |
|
52 |
||
53 |
\begin{itemize} |
|
54 |
||
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. |
|
59 |
||
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. |
|
65 |
||
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). |
|
71 |
||
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 |
|
76 |
step. |
|
77 |
||
78 |
\end{itemize} |
|
79 |
||
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.% |
|
38406 | 83 |
\end{isamarkuptext}% |
84 |
\isamarkuptrue% |
|
85 |
% |
|
86 |
\isamarkupsubsection{The preprocessor \label{sec:preproc}% |
|
87 |
} |
|
88 |
\isamarkuptrue% |
|
89 |
% |
|
90 |
\begin{isamarkuptext}% |
|
38437 | 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}. |
|
38406 | 95 |
|
38437 | 96 |
The \emph{simpset} can apply the full generality of the Isabelle |
97 |
simplifier. Due to the interpretation of theorems as code |
|
38406 | 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 |
|
38437 | 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} |
|
38406 | 103 |
attribute, respectively. |
104 |
||
105 |
Some common applications:% |
|
106 |
\end{isamarkuptext}% |
|
107 |
\isamarkuptrue% |
|
108 |
% |
|
109 |
\begin{itemize} |
|
110 |
% |
|
111 |
\begin{isamarkuptext}% |
|
112 |
\item replacing non-executable constructs by executable ones:% |
|
113 |
\end{isamarkuptext}% |
|
114 |
\isamarkuptrue% |
|
115 |
% |
|
116 |
\isadelimquote |
|
117 |
% |
|
118 |
\endisadelimquote |
|
119 |
% |
|
120 |
\isatagquote |
|
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}% |
|
125 |
\endisatagquote |
|
126 |
{\isafoldquote}% |
|
127 |
% |
|
128 |
\isadelimquote |
|
129 |
% |
|
130 |
\endisadelimquote |
|
131 |
% |
|
132 |
\begin{isamarkuptext}% |
|
133 |
\item replacing executable but inconvenient constructs:% |
|
134 |
\end{isamarkuptext}% |
|
135 |
\isamarkuptrue% |
|
136 |
% |
|
137 |
\isadelimquote |
|
138 |
% |
|
139 |
\endisadelimquote |
|
140 |
% |
|
141 |
\isatagquote |
|
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}% |
|
146 |
\endisatagquote |
|
147 |
{\isafoldquote}% |
|
148 |
% |
|
149 |
\isadelimquote |
|
150 |
% |
|
151 |
\endisadelimquote |
|
152 |
% |
|
153 |
\begin{isamarkuptext}% |
|
38437 | 154 |
\item eliminating disturbing expressions:% |
38406 | 155 |
\end{isamarkuptext}% |
156 |
\isamarkuptrue% |
|
157 |
% |
|
158 |
\isadelimquote |
|
159 |
% |
|
160 |
\endisadelimquote |
|
161 |
% |
|
162 |
\isatagquote |
|
163 |
\isacommand{lemma}\isamarkupfalse% |
|
38437 | 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}% |
|
38406 | 167 |
\endisatagquote |
168 |
{\isafoldquote}% |
|
169 |
% |
|
170 |
\isadelimquote |
|
171 |
% |
|
172 |
\endisadelimquote |
|
173 |
% |
|
38437 | 174 |
\end{itemize} |
175 |
% |
|
38406 | 176 |
\begin{isamarkuptext}% |
38437 | 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. |
|
183 |
||
184 |
\noindent The current setup of the preprocessor may be inspected |
|
38505 | 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 |
|
187 |
equations. |
|
38437 | 188 |
|
189 |
\begin{warn} |
|
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. |
|
193 |
\end{warn}% |
|
194 |
\end{isamarkuptext}% |
|
195 |
\isamarkuptrue% |
|
196 |
% |
|
197 |
\isamarkupsubsection{Understanding code equations \label{sec:equations}% |
|
198 |
} |
|
199 |
\isamarkuptrue% |
|
200 |
% |
|
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 |
|
205 |
equations. |
|
206 |
||
207 |
It is possible to exchange the default code equations for constants |
|
208 |
by explicitly proving alternative ones:% |
|
38406 | 209 |
\end{isamarkuptext}% |
210 |
\isamarkuptrue% |
|
211 |
% |
|
212 |
\isadelimquote |
|
213 |
% |
|
214 |
\endisadelimquote |
|
215 |
% |
|
216 |
\isatagquote |
|
217 |
\isacommand{lemma}\isamarkupfalse% |
|
38437 | 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}% |
|
38406 | 226 |
\endisatagquote |
227 |
{\isafoldquote}% |
|
228 |
% |
|
229 |
\isadelimquote |
|
230 |
% |
|
231 |
\endisadelimquote |
|
232 |
% |
|
233 |
\begin{isamarkuptext}% |
|
38437 | 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:% |
|
38406 | 238 |
\end{isamarkuptext}% |
239 |
\isamarkuptrue% |
|
240 |
% |
|
241 |
\isadelimquote |
|
242 |
% |
|
243 |
\endisadelimquote |
|
244 |
% |
|
245 |
\isatagquote |
|
246 |
% |
|
247 |
\begin{isamarkuptext}% |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
248 |
\begin{typewriter} |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
249 |
dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
250 |
dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
251 |
dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
252 |
\ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
253 |
\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon} |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
254 |
\end{typewriter}% |
38406 | 255 |
\end{isamarkuptext}% |
256 |
\isamarkuptrue% |
|
257 |
% |
|
258 |
\endisatagquote |
|
259 |
{\isafoldquote}% |
|
260 |
% |
|
261 |
\isadelimquote |
|
262 |
% |
|
263 |
\endisadelimquote |
|
264 |
% |
|
265 |
\begin{isamarkuptext}% |
|
38437 | 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}. |
|
38406 | 269 |
|
38437 | 270 |
This possibility to select arbitrary code equations is the key |
271 |
technique for program and datatype refinement (see |
|
272 |
\secref{sec:refinement}. |
|
38406 | 273 |
|
38437 | 274 |
Due to the preprocessor, there is the distinction of raw code |
275 |
equations (before preprocessing) and code equations (after |
|
276 |
preprocessing). |
|
277 |
||
38505 | 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. |
38406 | 279 |
|
38437 | 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:% |
|
282 |
\end{isamarkuptext}% |
|
283 |
\isamarkuptrue% |
|
284 |
% |
|
285 |
\isadelimquote |
|
286 |
% |
|
287 |
\endisadelimquote |
|
288 |
% |
|
289 |
\isatagquote |
|
290 |
\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% |
|
291 |
\ dequeue% |
|
292 |
\endisatagquote |
|
293 |
{\isafoldquote}% |
|
294 |
% |
|
295 |
\isadelimquote |
|
296 |
% |
|
297 |
\endisadelimquote |
|
298 |
% |
|
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 |
|
38505 | 302 |
the \indexdef{}{command}{code\_deps}\hypertarget{command.code-deps}{\hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}} command.% |
38406 | 303 |
\end{isamarkuptext}% |
304 |
\isamarkuptrue% |
|
305 |
% |
|
306 |
\isamarkupsubsection{Equality% |
|
307 |
} |
|
308 |
\isamarkuptrue% |
|
309 |
% |
|
310 |
\begin{isamarkuptext}% |
|
38437 | 311 |
Implementation of equality deserves some attention. Here an example |
312 |
function involving polymorphic equality:% |
|
38406 | 313 |
\end{isamarkuptext}% |
314 |
\isamarkuptrue% |
|
315 |
% |
|
316 |
\isadelimquote |
|
317 |
% |
|
318 |
\endisadelimquote |
|
319 |
% |
|
320 |
\isatagquote |
|
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 |
|
38437 | 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}% |
|
38406 | 329 |
\endisatagquote |
330 |
{\isafoldquote}% |
|
331 |
% |
|
332 |
\isadelimquote |
|
333 |
% |
|
334 |
\endisadelimquote |
|
335 |
% |
|
336 |
\begin{isamarkuptext}% |
|
337 |
\noindent During preprocessing, the membership test is rewritten, |
|
38437 | 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:% |
|
38406 | 340 |
\end{isamarkuptext}% |
341 |
\isamarkuptrue% |
|
342 |
% |
|
343 |
\isadelimquote |
|
344 |
% |
|
345 |
\endisadelimquote |
|
346 |
% |
|
347 |
\isatagquote |
|
348 |
% |
|
349 |
\begin{isamarkuptext}% |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
350 |
\begin{typewriter} |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
351 |
structure\ Example\ {\isacharcolon}\ sig\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
352 |
\ \ type\ {\isacharprime}a\ equal\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
353 |
\ \ val\ equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
354 |
\ \ val\ eq\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
355 |
\ \ val\ member\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
356 |
\ \ val\ collect{\isacharunderscore}duplicates\ {\isacharcolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
357 |
\ \ \ \ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
358 |
end\ {\isacharequal}\ struct\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
359 |
\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
360 |
type\ {\isacharprime}a\ equal\ {\isacharequal}\ {\isacharbraceleft}equal\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool{\isacharbraceright}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
361 |
val\ equal\ {\isacharequal}\ {\isacharhash}equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
362 |
\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
363 |
fun\ eq\ A{\isacharunderscore}\ a\ b\ {\isacharequal}\ equal\ A{\isacharunderscore}\ a\ b{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
364 |
\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
365 |
fun\ member\ A{\isacharunderscore}\ {\isacharbrackleft}{\isacharbrackright}\ y\ {\isacharequal}\ false\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
366 |
\ \ {\isacharbar}\ member\ A{\isacharunderscore}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ y\ {\isacharequal}\ eq\ A{\isacharunderscore}\ x\ y\ orelse\ member\ A{\isacharunderscore}\ xs\ y{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
367 |
\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
368 |
fun\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
369 |
\ \ {\isacharbar}\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ zs{\isacharparenright}\ {\isacharequal}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
370 |
\ \ \ \ {\isacharparenleft}if\ member\ A{\isacharunderscore}\ xs\ z\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
371 |
\ \ \ \ \ \ then\ {\isacharparenleft}if\ member\ A{\isacharunderscore}\ ys\ z\ then\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ zs\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
372 |
\ \ \ \ \ \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
373 |
\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
374 |
\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
375 |
end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
376 |
|
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
377 |
\end{typewriter}% |
38406 | 378 |
\end{isamarkuptext}% |
379 |
\isamarkuptrue% |
|
380 |
% |
|
381 |
\endisatagquote |
|
382 |
{\isafoldquote}% |
|
383 |
% |
|
384 |
\isadelimquote |
|
385 |
% |
|
386 |
\endisadelimquote |
|
387 |
% |
|
388 |
\begin{isamarkuptext}% |
|
389 |
\noindent Obviously, polymorphic equality is implemented the Haskell |
|
38437 | 390 |
way using a type class. How is this achieved? HOL introduces an |
39070 | 391 |
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 |
392 |
framework does the rest by propagating the \isa{equal} constraints |
|
38437 | 393 |
through all dependent code equations. For datatypes, instances of |
39070 | 394 |
\isa{equal} are implicitly derived when possible. For other types, |
395 |
you may instantiate \isa{equal} manually like any other type class.% |
|
38406 | 396 |
\end{isamarkuptext}% |
397 |
\isamarkuptrue% |
|
398 |
% |
|
38440 | 399 |
\isamarkupsubsection{Explicit partiality \label{sec:partiality}% |
38406 | 400 |
} |
401 |
\isamarkuptrue% |
|
402 |
% |
|
403 |
\begin{isamarkuptext}% |
|
404 |
Partiality usually enters the game by partial patterns, as |
|
405 |
in the following example, again for amortised queues:% |
|
406 |
\end{isamarkuptext}% |
|
407 |
\isamarkuptrue% |
|
408 |
% |
|
409 |
\isadelimquote |
|
410 |
% |
|
411 |
\endisadelimquote |
|
412 |
% |
|
413 |
\isatagquote |
|
414 |
\isacommand{definition}\isamarkupfalse% |
|
415 |
\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
416 |
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline |
|
417 |
\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
418 |
\isanewline |
|
419 |
\isacommand{lemma}\isamarkupfalse% |
|
420 |
\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
421 |
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
422 |
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
423 |
\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
424 |
\ \ \isacommand{by}\isamarkupfalse% |
|
38437 | 425 |
\ {\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}% |
38406 | 426 |
\endisatagquote |
427 |
{\isafoldquote}% |
|
428 |
% |
|
429 |
\isadelimquote |
|
430 |
% |
|
431 |
\endisadelimquote |
|
432 |
% |
|
433 |
\begin{isamarkuptext}% |
|
434 |
\noindent In the corresponding code, there is no equation |
|
435 |
for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:% |
|
436 |
\end{isamarkuptext}% |
|
437 |
\isamarkuptrue% |
|
438 |
% |
|
439 |
\isadelimquote |
|
440 |
% |
|
441 |
\endisadelimquote |
|
442 |
% |
|
443 |
\isatagquote |
|
444 |
% |
|
445 |
\begin{isamarkuptext}% |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
446 |
\begin{typewriter} |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
447 |
strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
448 |
strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
449 |
\ \ let\ {\isacharbraceleft}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
450 |
\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ xs{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
451 |
\ \ {\isacharbraceright}\ in\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
452 |
strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon} |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
453 |
\end{typewriter}% |
38406 | 454 |
\end{isamarkuptext}% |
455 |
\isamarkuptrue% |
|
456 |
% |
|
457 |
\endisatagquote |
|
458 |
{\isafoldquote}% |
|
459 |
% |
|
460 |
\isadelimquote |
|
461 |
% |
|
462 |
\endisadelimquote |
|
463 |
% |
|
464 |
\begin{isamarkuptext}% |
|
465 |
\noindent In some cases it is desirable to have this |
|
466 |
pseudo-\qt{partiality} more explicitly, e.g.~as follows:% |
|
467 |
\end{isamarkuptext}% |
|
468 |
\isamarkuptrue% |
|
469 |
% |
|
470 |
\isadelimquote |
|
471 |
% |
|
472 |
\endisadelimquote |
|
473 |
% |
|
474 |
\isatagquote |
|
475 |
\isacommand{axiomatization}\isamarkupfalse% |
|
476 |
\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline |
|
477 |
\isanewline |
|
478 |
\isacommand{definition}\isamarkupfalse% |
|
479 |
\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
480 |
\ \ {\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 |
\isanewline |
|
482 |
\isacommand{lemma}\isamarkupfalse% |
|
483 |
\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
484 |
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline |
|
485 |
\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
486 |
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
487 |
\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
488 |
\ \ \isacommand{by}\isamarkupfalse% |
|
38437 | 489 |
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% |
38406 | 490 |
\endisatagquote |
491 |
{\isafoldquote}% |
|
492 |
% |
|
493 |
\isadelimquote |
|
494 |
% |
|
495 |
\endisadelimquote |
|
496 |
% |
|
497 |
\begin{isamarkuptext}% |
|
498 |
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 |
||
500 |
Normally, if constants without any code equations occur in a |
|
501 |
program, the code generator complains (since in most cases this is |
|
502 |
indeed an error). But such constants can also be thought |
|
503 |
of as function definitions which always fail, |
|
504 |
since there is never a successful pattern match on the left hand |
|
505 |
side. In order to categorise a constant into that category |
|
38505 | 506 |
explicitly, use \indexdef{}{command}{code\_abort}\hypertarget{command.code-abort}{\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}}:% |
38406 | 507 |
\end{isamarkuptext}% |
508 |
\isamarkuptrue% |
|
509 |
% |
|
510 |
\isadelimquote |
|
511 |
% |
|
512 |
\endisadelimquote |
|
513 |
% |
|
514 |
\isatagquote |
|
515 |
\isacommand{code{\isacharunderscore}abort}\isamarkupfalse% |
|
516 |
\ empty{\isacharunderscore}queue% |
|
517 |
\endisatagquote |
|
518 |
{\isafoldquote}% |
|
519 |
% |
|
520 |
\isadelimquote |
|
521 |
% |
|
522 |
\endisadelimquote |
|
523 |
% |
|
524 |
\begin{isamarkuptext}% |
|
525 |
\noindent Then the code generator will just insert an error or |
|
526 |
exception at the appropriate position:% |
|
527 |
\end{isamarkuptext}% |
|
528 |
\isamarkuptrue% |
|
529 |
% |
|
530 |
\isadelimquote |
|
531 |
% |
|
532 |
\endisadelimquote |
|
533 |
% |
|
534 |
\isatagquote |
|
535 |
% |
|
536 |
\begin{isamarkuptext}% |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
537 |
\begin{typewriter} |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
538 |
empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
539 |
empty{\isacharunderscore}queue\ {\isacharequal}\ error\ {\isachardoublequote}empty{\isacharunderscore}queue{\isachardoublequote}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
540 |
\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
541 |
strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
542 |
strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
543 |
strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
544 |
\ \ {\isacharparenleft}if\ null\ xs\ then\ empty{\isacharunderscore}queue\isanewline |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
545 |
\ \ \ \ else\ strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon} |
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
546 |
\end{typewriter}% |
38406 | 547 |
\end{isamarkuptext}% |
548 |
\isamarkuptrue% |
|
549 |
% |
|
550 |
\endisatagquote |
|
551 |
{\isafoldquote}% |
|
552 |
% |
|
553 |
\isadelimquote |
|
554 |
% |
|
555 |
\endisadelimquote |
|
556 |
% |
|
557 |
\begin{isamarkuptext}% |
|
38437 | 558 |
\noindent This feature however is rarely needed in practice. Note |
559 |
also that the HOL default setup already declares \isa{undefined} |
|
560 |
as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most likely to be used in such |
|
561 |
situations.% |
|
562 |
\end{isamarkuptext}% |
|
563 |
\isamarkuptrue% |
|
564 |
% |
|
565 |
\isamarkupsubsection{If something goes utterly wrong \label{sec:utterly_wrong}% |
|
566 |
} |
|
567 |
\isamarkuptrue% |
|
568 |
% |
|
569 |
\begin{isamarkuptext}% |
|
570 |
Under certain circumstances, the code generator fails to produce |
|
38440 | 571 |
code entirely. To debug these, the following hints may prove |
572 |
helpful: |
|
38437 | 573 |
|
574 |
\begin{description} |
|
575 |
||
38440 | 576 |
\ditem{\emph{Check with a different target language}.} Sometimes |
577 |
the situation gets more clear if you switch to another target |
|
578 |
language; the code generated there might give some hints what |
|
579 |
prevents the code generator to produce code for the desired |
|
580 |
language. |
|
38437 | 581 |
|
38440 | 582 |
\ditem{\emph{Inspect code equations}.} Code equations are the central |
583 |
carrier of code generation. Most problems occuring while generation |
|
584 |
code can be traced to single equations which are printed as part of |
|
585 |
the error message. A closer inspection of those may offer the key |
|
586 |
for solving issues (cf.~\secref{sec:equations}). |
|
38437 | 587 |
|
38440 | 588 |
\ditem{\emph{Inspect preprocessor setup}.} The preprocessor might |
589 |
transform code equations unexpectedly; to understand an |
|
590 |
inspection of its setup is necessary (cf.~\secref{sec:preproc}). |
|
38437 | 591 |
|
38440 | 592 |
\ditem{\emph{Generate exceptions}.} If the code generator |
593 |
complains about missing code equations, in can be helpful to |
|
594 |
implement the offending constants as exceptions |
|
595 |
(cf.~\secref{sec:partiality}); this allows at least for a formal |
|
596 |
generation of code, whose inspection may then give clues what is |
|
597 |
wrong. |
|
38437 | 598 |
|
38440 | 599 |
\ditem{\emph{Remove offending code equations}.} If code |
600 |
generation is prevented by just a single equation, this can be |
|
601 |
removed (cf.~\secref{sec:equations}) to allow formal code |
|
602 |
generation, whose result in turn can be used to trace the |
|
603 |
problem. The most prominent case here are mismatches in type |
|
604 |
class signatures (\qt{wellsortedness error}). |
|
38437 | 605 |
|
606 |
\end{description}% |
|
38406 | 607 |
\end{isamarkuptext}% |
608 |
\isamarkuptrue% |
|
609 |
% |
|
610 |
\isadelimtheory |
|
611 |
% |
|
612 |
\endisadelimtheory |
|
613 |
% |
|
614 |
\isatagtheory |
|
615 |
\isacommand{end}\isamarkupfalse% |
|
616 |
% |
|
617 |
\endisatagtheory |
|
618 |
{\isafoldtheory}% |
|
619 |
% |
|
620 |
\isadelimtheory |
|
621 |
% |
|
622 |
\endisadelimtheory |
|
623 |
\isanewline |
|
624 |
\end{isabellebody}% |
|
625 |
%%% Local Variables: |
|
626 |
%%% mode: latex |
|
627 |
%%% TeX-master: "root" |
|
628 |
%%% End: |