author | wenzelm |
Wed, 15 Jun 2011 22:01:27 +0200 | |
changeset 43409 | 868a748b162a |
parent 40406 | 313a24b66a8d |
child 43561 | 2bb6fd55e195 |
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 |
|
40406 | 49 |
of the form \isa{f\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} (an equation headed by a |
50 |
constant \isa{f} with arguments \isa{t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub n} and right |
|
38437 | 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 |
40406 | 102 |
\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\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% |
|
40406 | 122 |
\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
123 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ xs\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ List{\isaliteral{2E}{\isachardot}}member\ xs\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
124 |
\ {\isaliteral{28}{\isacharparenleft}}fact\ in{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}member{\isaliteral{29}{\isacharparenright}}% |
|
38406 | 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% |
|
40406 | 143 |
\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
144 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ List{\isaliteral{2E}{\isachardot}}null\ xs{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
145 |
\ {\isaliteral{28}{\isacharparenleft}}fact\ eq{\isaliteral{5F}{\isacharunderscore}}Nil{\isaliteral{5F}{\isacharunderscore}}null{\isaliteral{29}{\isacharparenright}}% |
|
38406 | 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% |
|
40406 | 164 |
\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
165 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
166 |
\ {\isaliteral{28}{\isacharparenleft}}fact\ One{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\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 |
|
40406 | 181 |
elimination implemented in theory \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat}}} (see |
38437 | 182 |
\secref{eff_nat}) uses this interface. |
183 |
||
184 |
\noindent The current setup of the preprocessor may be inspected |
|
40406 | 185 |
using the \indexdef{}{command}{print\_codeproc}\hypertarget{command.print-codeproc}{\hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}}} command. \indexdef{}{command}{code\_thms}\hypertarget{command.code-thms}{\hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}} (see \secref{sec:equations}) provides a convenient |
38505 | 186 |
mechanism to inspect the impact of a preprocessor setup on code |
187 |
equations. |
|
38437 | 188 |
|
189 |
\begin{warn} |
|
40406 | 190 |
Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}} also applies to the |
38437 | 191 |
preprocessor of the ancient \isa{SML\ code\ generator}; in case |
40406 | 192 |
this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} instead. |
38437 | 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% |
|
40406 | 218 |
\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
219 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
220 |
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ then\ {\isaliteral{28}{\isacharparenleft}}None{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
221 |
\ \ \ \ \ \ \ else\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
222 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
223 |
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Some\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 224 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 225 |
\ {\isaliteral{28}{\isacharparenleft}}cases\ xs{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}cases\ {\isaliteral{22}{\isachardoublequoteopen}}rev\ xs{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}% |
38406 | 226 |
\endisatagquote |
227 |
{\isafoldquote}% |
|
228 |
% |
|
229 |
\isadelimquote |
|
230 |
% |
|
231 |
\endisadelimquote |
|
232 |
% |
|
233 |
\begin{isamarkuptext}% |
|
40406 | 234 |
\noindent The annotation \isa{{\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}} is an \isa{attribute} |
38437 | 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 |
% |
|
39745 | 241 |
\isadelimquotetypewriter |
38406 | 242 |
% |
39745 | 243 |
\endisadelimquotetypewriter |
38406 | 244 |
% |
39745 | 245 |
\isatagquotetypewriter |
38406 | 246 |
% |
247 |
\begin{isamarkuptext}% |
|
40406 | 248 |
dequeue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Queue\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}Maybe\ a{\isaliteral{2C}{\isacharcomma}}\ Queue\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
249 |
dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Just\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
250 |
dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
251 |
\ \ {\isaliteral{28}{\isacharparenleft}}if\ null\ xs\ then\ {\isaliteral{28}{\isacharparenleft}}Nothing{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
252 |
\ \ \ \ else\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}reverse\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline% |
|
38406 | 253 |
\end{isamarkuptext}% |
254 |
\isamarkuptrue% |
|
255 |
% |
|
39745 | 256 |
\endisatagquotetypewriter |
257 |
{\isafoldquotetypewriter}% |
|
38406 | 258 |
% |
39745 | 259 |
\isadelimquotetypewriter |
38406 | 260 |
% |
39745 | 261 |
\endisadelimquotetypewriter |
38406 | 262 |
% |
263 |
\begin{isamarkuptext}% |
|
40406 | 264 |
\noindent You may note that the equality test \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} has |
265 |
been replaced by the predicate \isa{List{\isaliteral{2E}{\isachardot}}null\ xs}. This is due |
|
38437 | 266 |
to the default setup of the \qn{preprocessor}. |
38406 | 267 |
|
38437 | 268 |
This possibility to select arbitrary code equations is the key |
269 |
technique for program and datatype refinement (see |
|
39683 | 270 |
\secref{sec:refinement}). |
38406 | 271 |
|
38437 | 272 |
Due to the preprocessor, there is the distinction of raw code |
273 |
equations (before preprocessing) and code equations (after |
|
274 |
preprocessing). |
|
275 |
||
40406 | 276 |
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{\isaliteral{5F}{\isacharunderscore}}codesetup}}}}} command. |
38406 | 277 |
|
38437 | 278 |
The code equations after preprocessing are already are blueprint of |
40406 | 279 |
the generated program and can be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}} command:% |
38437 | 280 |
\end{isamarkuptext}% |
281 |
\isamarkuptrue% |
|
282 |
% |
|
283 |
\isadelimquote |
|
284 |
% |
|
285 |
\endisadelimquote |
|
286 |
% |
|
287 |
\isatagquote |
|
40406 | 288 |
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}\isamarkupfalse% |
38437 | 289 |
\ dequeue% |
290 |
\endisatagquote |
|
291 |
{\isafoldquote}% |
|
292 |
% |
|
293 |
\isadelimquote |
|
294 |
% |
|
295 |
\endisadelimquote |
|
296 |
% |
|
297 |
\begin{isamarkuptext}% |
|
298 |
\noindent This prints a table with the code equations for \isa{dequeue}, including \emph{all} code equations those equations depend |
|
299 |
on recursively. These dependencies themselves can be visualized using |
|
40406 | 300 |
the \indexdef{}{command}{code\_deps}\hypertarget{command.code-deps}{\hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}} command.% |
38406 | 301 |
\end{isamarkuptext}% |
302 |
\isamarkuptrue% |
|
303 |
% |
|
304 |
\isamarkupsubsection{Equality% |
|
305 |
} |
|
306 |
\isamarkuptrue% |
|
307 |
% |
|
308 |
\begin{isamarkuptext}% |
|
38437 | 309 |
Implementation of equality deserves some attention. Here an example |
310 |
function involving polymorphic equality:% |
|
38406 | 311 |
\end{isamarkuptext}% |
312 |
\isamarkuptrue% |
|
313 |
% |
|
314 |
\isadelimquote |
|
315 |
% |
|
316 |
\endisadelimquote |
|
317 |
% |
|
318 |
\isatagquote |
|
319 |
\isacommand{primrec}\isamarkupfalse% |
|
40406 | 320 |
\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
321 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ xs\ ys\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
322 |
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ xs\ ys\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ z\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ xs\isanewline |
|
323 |
\ \ \ \ then\ if\ z\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ ys\isanewline |
|
324 |
\ \ \ \ \ \ then\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ xs\ ys\ zs\isanewline |
|
325 |
\ \ \ \ \ \ else\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ xs\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{23}{\isacharhash}}ys{\isaliteral{29}{\isacharparenright}}\ zs\isanewline |
|
326 |
\ \ \ \ else\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{23}{\isacharhash}}xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{23}{\isacharhash}}ys{\isaliteral{29}{\isacharparenright}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
38406 | 327 |
\endisatagquote |
328 |
{\isafoldquote}% |
|
329 |
% |
|
330 |
\isadelimquote |
|
331 |
% |
|
332 |
\endisadelimquote |
|
333 |
% |
|
334 |
\begin{isamarkuptext}% |
|
335 |
\noindent During preprocessing, the membership test is rewritten, |
|
40406 | 336 |
resulting in \isa{List{\isaliteral{2E}{\isachardot}}member}, which itself performs an explicit |
38437 | 337 |
equality check, as can be seen in the corresponding \isa{SML} code:% |
38406 | 338 |
\end{isamarkuptext}% |
339 |
\isamarkuptrue% |
|
340 |
% |
|
39745 | 341 |
\isadelimquotetypewriter |
38406 | 342 |
% |
39745 | 343 |
\endisadelimquotetypewriter |
38406 | 344 |
% |
39745 | 345 |
\isatagquotetypewriter |
38406 | 346 |
% |
347 |
\begin{isamarkuptext}% |
|
40406 | 348 |
structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline |
349 |
\ \ type\ {\isaliteral{27}{\isacharprime}}a\ equal\isanewline |
|
350 |
\ \ val\ equal\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ equal\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline |
|
351 |
\ \ val\ eq\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ equal\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline |
|
352 |
\ \ val\ member\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ equal\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline |
|
353 |
\ \ val\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ {\isaliteral{3A}{\isacharcolon}}\isanewline |
|
354 |
\ \ \ \ {\isaliteral{27}{\isacharprime}}a\ equal\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\isanewline |
|
355 |
end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
356 |
\isanewline |
40406 | 357 |
type\ {\isaliteral{27}{\isacharprime}}a\ equal\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}equal\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
358 |
val\ equal\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}equal\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ equal\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
359 |
\isanewline |
40406 | 360 |
fun\ eq\ A{\isaliteral{5F}{\isacharunderscore}}\ a\ b\ {\isaliteral{3D}{\isacharequal}}\ equal\ A{\isaliteral{5F}{\isacharunderscore}}\ a\ b{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
361 |
\isanewline |
40406 | 362 |
fun\ member\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ false\isanewline |
363 |
\ \ {\isaliteral{7C}{\isacharbar}}\ member\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ eq\ A{\isaliteral{5F}{\isacharunderscore}}\ x\ y\ orelse\ member\ A{\isaliteral{5F}{\isacharunderscore}}\ xs\ y{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
364 |
\isanewline |
40406 | 365 |
fun\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ A{\isaliteral{5F}{\isacharunderscore}}\ xs\ ys\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ xs\isanewline |
366 |
\ \ {\isaliteral{7C}{\isacharbar}}\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ A{\isaliteral{5F}{\isacharunderscore}}\ xs\ ys\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
367 |
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ member\ A{\isaliteral{5F}{\isacharunderscore}}\ xs\ z\isanewline |
|
368 |
\ \ \ \ \ \ then\ {\isaliteral{28}{\isacharparenleft}}if\ member\ A{\isaliteral{5F}{\isacharunderscore}}\ ys\ z\ then\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ A{\isaliteral{5F}{\isacharunderscore}}\ xs\ ys\ zs\isanewline |
|
369 |
\ \ \ \ \ \ \ \ \ \ \ \ \ else\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ A{\isaliteral{5F}{\isacharunderscore}}\ xs\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}\ zs{\isaliteral{29}{\isacharparenright}}\isanewline |
|
370 |
\ \ \ \ \ \ else\ collect{\isaliteral{5F}{\isacharunderscore}}duplicates\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
371 |
\isanewline |
40406 | 372 |
end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline% |
38406 | 373 |
\end{isamarkuptext}% |
374 |
\isamarkuptrue% |
|
375 |
% |
|
39745 | 376 |
\endisatagquotetypewriter |
377 |
{\isafoldquotetypewriter}% |
|
38406 | 378 |
% |
39745 | 379 |
\isadelimquotetypewriter |
38406 | 380 |
% |
39745 | 381 |
\endisadelimquotetypewriter |
38406 | 382 |
% |
383 |
\begin{isamarkuptext}% |
|
384 |
\noindent Obviously, polymorphic equality is implemented the Haskell |
|
38437 | 385 |
way using a type class. How is this achieved? HOL introduces an |
40406 | 386 |
explicit class \isa{equal} with a corresponding operation \isa{equal{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}equal} such that \isa{equal{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}equal\ {\isaliteral{3D}{\isacharequal}}\ op\ {\isaliteral{3D}{\isacharequal}}}. The preprocessing |
39070 | 387 |
framework does the rest by propagating the \isa{equal} constraints |
38437 | 388 |
through all dependent code equations. For datatypes, instances of |
39070 | 389 |
\isa{equal} are implicitly derived when possible. For other types, |
390 |
you may instantiate \isa{equal} manually like any other type class.% |
|
38406 | 391 |
\end{isamarkuptext}% |
392 |
\isamarkuptrue% |
|
393 |
% |
|
38440 | 394 |
\isamarkupsubsection{Explicit partiality \label{sec:partiality}% |
38406 | 395 |
} |
396 |
\isamarkuptrue% |
|
397 |
% |
|
398 |
\begin{isamarkuptext}% |
|
399 |
Partiality usually enters the game by partial patterns, as |
|
400 |
in the following example, again for amortised queues:% |
|
401 |
\end{isamarkuptext}% |
|
402 |
\isamarkuptrue% |
|
403 |
% |
|
404 |
\isadelimquote |
|
405 |
% |
|
406 |
\endisadelimquote |
|
407 |
% |
|
408 |
\isatagquote |
|
409 |
\isacommand{definition}\isamarkupfalse% |
|
40406 | 410 |
\ strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
411 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ q\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}case\ dequeue\ q\isanewline |
|
412 |
\ \ \ \ of\ {\isaliteral{28}{\isacharparenleft}}Some\ x{\isaliteral{2C}{\isacharcomma}}\ q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38406 | 413 |
\isanewline |
414 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 415 |
\ strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
416 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
417 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
418 |
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}case\ rev\ xs\ of\ y\ {\isaliteral{23}{\isacharhash}}\ ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38406 | 419 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 420 |
\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}cases\ xs{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\ split{\isaliteral{3A}{\isacharcolon}}\ list{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}% |
38406 | 421 |
\endisatagquote |
422 |
{\isafoldquote}% |
|
423 |
% |
|
424 |
\isadelimquote |
|
425 |
% |
|
426 |
\endisadelimquote |
|
427 |
% |
|
428 |
\begin{isamarkuptext}% |
|
429 |
\noindent In the corresponding code, there is no equation |
|
40406 | 430 |
for the pattern \isa{AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}:% |
38406 | 431 |
\end{isamarkuptext}% |
432 |
\isamarkuptrue% |
|
433 |
% |
|
39745 | 434 |
\isadelimquotetypewriter |
38406 | 435 |
% |
39745 | 436 |
\endisadelimquotetypewriter |
38406 | 437 |
% |
39745 | 438 |
\isatagquotetypewriter |
38406 | 439 |
% |
440 |
\begin{isamarkuptext}% |
|
40406 | 441 |
strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Queue\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ Queue\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
442 |
strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
443 |
\ \ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
444 |
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ reverse\ xs{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
445 |
\ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
446 |
strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline% |
|
38406 | 447 |
\end{isamarkuptext}% |
448 |
\isamarkuptrue% |
|
449 |
% |
|
39745 | 450 |
\endisatagquotetypewriter |
451 |
{\isafoldquotetypewriter}% |
|
38406 | 452 |
% |
39745 | 453 |
\isadelimquotetypewriter |
38406 | 454 |
% |
39745 | 455 |
\endisadelimquotetypewriter |
38406 | 456 |
% |
457 |
\begin{isamarkuptext}% |
|
458 |
\noindent In some cases it is desirable to have this |
|
459 |
pseudo-\qt{partiality} more explicitly, e.g.~as follows:% |
|
460 |
\end{isamarkuptext}% |
|
461 |
\isamarkuptrue% |
|
462 |
% |
|
463 |
\isadelimquote |
|
464 |
% |
|
465 |
\endisadelimquote |
|
466 |
% |
|
467 |
\isatagquote |
|
468 |
\isacommand{axiomatization}\isamarkupfalse% |
|
40406 | 469 |
\ empty{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
38406 | 470 |
\isanewline |
471 |
\isacommand{definition}\isamarkupfalse% |
|
40406 | 472 |
\ strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
473 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{27}{\isacharprime}}\ q\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}case\ dequeue\ q\ of\ {\isaliteral{28}{\isacharparenleft}}Some\ x{\isaliteral{2C}{\isacharcomma}}\ q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ empty{\isaliteral{5F}{\isacharunderscore}}queue{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38406 | 474 |
\isanewline |
475 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 476 |
\ strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
477 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ then\ empty{\isaliteral{5F}{\isacharunderscore}}queue\isanewline |
|
478 |
\ \ \ \ \ else\ strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
479 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
480 |
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38406 | 481 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 482 |
\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}def\ split{\isaliteral{3A}{\isacharcolon}}\ list{\isaliteral{2E}{\isachardot}}splits{\isaliteral{29}{\isacharparenright}}% |
38406 | 483 |
\endisatagquote |
484 |
{\isafoldquote}% |
|
485 |
% |
|
486 |
\isadelimquote |
|
487 |
% |
|
488 |
\endisadelimquote |
|
489 |
% |
|
490 |
\begin{isamarkuptext}% |
|
40406 | 491 |
Observe that on the right hand side of the definition of \isa{strict{\isaliteral{5F}{\isacharunderscore}}dequeue{\isaliteral{27}{\isacharprime}}}, the unspecified constant \isa{empty{\isaliteral{5F}{\isacharunderscore}}queue} occurs. |
38406 | 492 |
|
493 |
Normally, if constants without any code equations occur in a |
|
494 |
program, the code generator complains (since in most cases this is |
|
495 |
indeed an error). But such constants can also be thought |
|
496 |
of as function definitions which always fail, |
|
497 |
since there is never a successful pattern match on the left hand |
|
498 |
side. In order to categorise a constant into that category |
|
40406 | 499 |
explicitly, use \indexdef{}{command}{code\_abort}\hypertarget{command.code-abort}{\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}:% |
38406 | 500 |
\end{isamarkuptext}% |
501 |
\isamarkuptrue% |
|
502 |
% |
|
503 |
\isadelimquote |
|
504 |
% |
|
505 |
\endisadelimquote |
|
506 |
% |
|
507 |
\isatagquote |
|
40406 | 508 |
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}\isamarkupfalse% |
509 |
\ empty{\isaliteral{5F}{\isacharunderscore}}queue% |
|
38406 | 510 |
\endisatagquote |
511 |
{\isafoldquote}% |
|
512 |
% |
|
513 |
\isadelimquote |
|
514 |
% |
|
515 |
\endisadelimquote |
|
516 |
% |
|
517 |
\begin{isamarkuptext}% |
|
518 |
\noindent Then the code generator will just insert an error or |
|
519 |
exception at the appropriate position:% |
|
520 |
\end{isamarkuptext}% |
|
521 |
\isamarkuptrue% |
|
522 |
% |
|
39745 | 523 |
\isadelimquotetypewriter |
38406 | 524 |
% |
39745 | 525 |
\endisadelimquotetypewriter |
38406 | 526 |
% |
39745 | 527 |
\isatagquotetypewriter |
38406 | 528 |
% |
529 |
\begin{isamarkuptext}% |
|
40406 | 530 |
empty{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
531 |
empty{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3D}{\isacharequal}}\ error\ {\isaliteral{22}{\isachardoublequote}}empty{\isaliteral{5F}{\isacharunderscore}}queue{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
532 |
\isanewline |
40406 | 533 |
strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Queue\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ Queue\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
534 |
strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
535 |
strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
536 |
\ \ {\isaliteral{28}{\isacharparenleft}}if\ null\ xs\ then\ empty{\isaliteral{5F}{\isacharunderscore}}queue\isanewline |
|
537 |
\ \ \ \ else\ strict{\isaliteral{5F}{\isacharunderscore}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}reverse\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline% |
|
38406 | 538 |
\end{isamarkuptext}% |
539 |
\isamarkuptrue% |
|
540 |
% |
|
39745 | 541 |
\endisatagquotetypewriter |
542 |
{\isafoldquotetypewriter}% |
|
38406 | 543 |
% |
39745 | 544 |
\isadelimquotetypewriter |
38406 | 545 |
% |
39745 | 546 |
\endisadelimquotetypewriter |
38406 | 547 |
% |
548 |
\begin{isamarkuptext}% |
|
38437 | 549 |
\noindent This feature however is rarely needed in practice. Note |
550 |
also that the HOL default setup already declares \isa{undefined} |
|
40406 | 551 |
as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}, which is most likely to be used in such |
38437 | 552 |
situations.% |
553 |
\end{isamarkuptext}% |
|
554 |
\isamarkuptrue% |
|
555 |
% |
|
556 |
\isamarkupsubsection{If something goes utterly wrong \label{sec:utterly_wrong}% |
|
557 |
} |
|
558 |
\isamarkuptrue% |
|
559 |
% |
|
560 |
\begin{isamarkuptext}% |
|
561 |
Under certain circumstances, the code generator fails to produce |
|
38440 | 562 |
code entirely. To debug these, the following hints may prove |
563 |
helpful: |
|
38437 | 564 |
|
565 |
\begin{description} |
|
566 |
||
38440 | 567 |
\ditem{\emph{Check with a different target language}.} Sometimes |
568 |
the situation gets more clear if you switch to another target |
|
569 |
language; the code generated there might give some hints what |
|
570 |
prevents the code generator to produce code for the desired |
|
571 |
language. |
|
38437 | 572 |
|
38440 | 573 |
\ditem{\emph{Inspect code equations}.} Code equations are the central |
43409 | 574 |
carrier of code generation. Most problems occuring while generating |
38440 | 575 |
code can be traced to single equations which are printed as part of |
576 |
the error message. A closer inspection of those may offer the key |
|
577 |
for solving issues (cf.~\secref{sec:equations}). |
|
38437 | 578 |
|
38440 | 579 |
\ditem{\emph{Inspect preprocessor setup}.} The preprocessor might |
580 |
transform code equations unexpectedly; to understand an |
|
581 |
inspection of its setup is necessary (cf.~\secref{sec:preproc}). |
|
38437 | 582 |
|
38440 | 583 |
\ditem{\emph{Generate exceptions}.} If the code generator |
584 |
complains about missing code equations, in can be helpful to |
|
585 |
implement the offending constants as exceptions |
|
586 |
(cf.~\secref{sec:partiality}); this allows at least for a formal |
|
587 |
generation of code, whose inspection may then give clues what is |
|
588 |
wrong. |
|
38437 | 589 |
|
38440 | 590 |
\ditem{\emph{Remove offending code equations}.} If code |
591 |
generation is prevented by just a single equation, this can be |
|
592 |
removed (cf.~\secref{sec:equations}) to allow formal code |
|
593 |
generation, whose result in turn can be used to trace the |
|
594 |
problem. The most prominent case here are mismatches in type |
|
595 |
class signatures (\qt{wellsortedness error}). |
|
38437 | 596 |
|
597 |
\end{description}% |
|
38406 | 598 |
\end{isamarkuptext}% |
599 |
\isamarkuptrue% |
|
600 |
% |
|
601 |
\isadelimtheory |
|
602 |
% |
|
603 |
\endisadelimtheory |
|
604 |
% |
|
605 |
\isatagtheory |
|
606 |
\isacommand{end}\isamarkupfalse% |
|
607 |
% |
|
608 |
\endisatagtheory |
|
609 |
{\isafoldtheory}% |
|
610 |
% |
|
611 |
\isadelimtheory |
|
612 |
% |
|
613 |
\endisadelimtheory |
|
614 |
\isanewline |
|
615 |
\end{isabellebody}% |
|
616 |
%%% Local Variables: |
|
617 |
%%% mode: latex |
|
618 |
%%% TeX-master: "root" |
|
619 |
%%% End: |