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
|
|
185 |
using the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}
|
|
186 |
(see \secref{sec:equations}) provides a convenient mechanism to
|
|
187 |
inspect the impact of a preprocessor setup on code equations.
|
|
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}%
|
|
248 |
\isatypewriter%
|
|
249 |
\noindent%
|
38437
|
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)));%
|
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 |
|
|
278 |
The first can be listed (among other data) using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command (later on in \secref{sec:refinement}
|
|
279 |
it will be shown how these code equations can be changed).
|
38406
|
280 |
|
38437
|
281 |
The code equations after preprocessing are already are blueprint of
|
|
282 |
the generated program and can be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
|
|
283 |
\end{isamarkuptext}%
|
|
284 |
\isamarkuptrue%
|
|
285 |
%
|
|
286 |
\isadelimquote
|
|
287 |
%
|
|
288 |
\endisadelimquote
|
|
289 |
%
|
|
290 |
\isatagquote
|
|
291 |
\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
|
|
292 |
\ dequeue%
|
|
293 |
\endisatagquote
|
|
294 |
{\isafoldquote}%
|
|
295 |
%
|
|
296 |
\isadelimquote
|
|
297 |
%
|
|
298 |
\endisadelimquote
|
|
299 |
%
|
|
300 |
\begin{isamarkuptext}%
|
|
301 |
\noindent This prints a table with the code equations for \isa{dequeue}, including \emph{all} code equations those equations depend
|
|
302 |
on recursively. These dependencies themselves can be visualized using
|
|
303 |
the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command.%
|
38406
|
304 |
\end{isamarkuptext}%
|
|
305 |
\isamarkuptrue%
|
|
306 |
%
|
|
307 |
\isamarkupsubsection{Equality%
|
|
308 |
}
|
|
309 |
\isamarkuptrue%
|
|
310 |
%
|
|
311 |
\begin{isamarkuptext}%
|
38437
|
312 |
Implementation of equality deserves some attention. Here an example
|
|
313 |
function involving polymorphic equality:%
|
38406
|
314 |
\end{isamarkuptext}%
|
|
315 |
\isamarkuptrue%
|
|
316 |
%
|
|
317 |
\isadelimquote
|
|
318 |
%
|
|
319 |
\endisadelimquote
|
|
320 |
%
|
|
321 |
\isatagquote
|
|
322 |
\isacommand{primrec}\isamarkupfalse%
|
|
323 |
\ 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
|
|
324 |
\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
|
38437
|
325 |
{\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
|
|
326 |
\ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
|
|
327 |
\ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
|
|
328 |
\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
|
|
329 |
\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
|
38406
|
330 |
\endisatagquote
|
|
331 |
{\isafoldquote}%
|
|
332 |
%
|
|
333 |
\isadelimquote
|
|
334 |
%
|
|
335 |
\endisadelimquote
|
|
336 |
%
|
|
337 |
\begin{isamarkuptext}%
|
|
338 |
\noindent During preprocessing, the membership test is rewritten,
|
38437
|
339 |
resulting in \isa{List{\isachardot}member}, which itself performs an explicit
|
|
340 |
equality check, as can be seen in the corresponding \isa{SML} code:%
|
38406
|
341 |
\end{isamarkuptext}%
|
|
342 |
\isamarkuptrue%
|
|
343 |
%
|
|
344 |
\isadelimquote
|
|
345 |
%
|
|
346 |
\endisadelimquote
|
|
347 |
%
|
|
348 |
\isatagquote
|
|
349 |
%
|
|
350 |
\begin{isamarkuptext}%
|
|
351 |
\isatypewriter%
|
|
352 |
\noindent%
|
|
353 |
\hspace*{0pt}structure Example :~sig\\
|
|
354 |
\hspace*{0pt} ~type 'a eq\\
|
|
355 |
\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
|
|
356 |
\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
|
|
357 |
\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
|
|
358 |
\hspace*{0pt} ~val collect{\char95}duplicates :\\
|
|
359 |
\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
|
|
360 |
\hspace*{0pt}end = struct\\
|
|
361 |
\hspace*{0pt}\\
|
|
362 |
\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
|
|
363 |
\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
|
|
364 |
\hspace*{0pt}\\
|
|
365 |
\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
|
|
366 |
\hspace*{0pt}\\
|
|
367 |
\hspace*{0pt}fun member A{\char95}~[] y = false\\
|
|
368 |
\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
|
|
369 |
\hspace*{0pt}\\
|
|
370 |
\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
|
|
371 |
\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
|
|
372 |
\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
|
|
373 |
\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
|
|
374 |
\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
|
|
375 |
\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
|
|
376 |
\hspace*{0pt}\\
|
|
377 |
\hspace*{0pt}end;~(*struct Example*)%
|
|
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
|
|
391 |
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
|
|
392 |
framework does the rest by propagating the \isa{eq} constraints
|
|
393 |
through all dependent code equations. For datatypes, instances of
|
|
394 |
\isa{eq} are implicitly derived when possible. For other types,
|
|
395 |
you may instantiate \isa{eq} 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}%
|
|
446 |
\isatypewriter%
|
|
447 |
\noindent%
|
|
448 |
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
|
|
449 |
\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
|
|
450 |
\hspace*{0pt} ~let {\char123}\\
|
|
451 |
\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
|
|
452 |
\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
|
|
453 |
\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
|
|
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
|
|
506 |
explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
|
|
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}%
|
|
537 |
\isatypewriter%
|
|
538 |
\noindent%
|
|
539 |
\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
|
|
540 |
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
|
|
541 |
\hspace*{0pt}\\
|
|
542 |
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
|
|
543 |
\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
|
|
544 |
\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
|
|
545 |
\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
|
|
546 |
\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
|
|
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:
|