1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Program}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Program\isanewline |
|
12 \isakeyword{imports}\ Introduction\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupsection{Turning Theories into Programs \label{sec:program}% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup% |
|
26 } |
|
27 \isamarkuptrue% |
|
28 % |
|
29 \begin{isamarkuptext}% |
|
30 We have already seen how by default equations stemming from |
|
31 \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} |
|
32 statements are used for code generation. This default behaviour |
|
33 can be changed, e.g.\ by providing different code equations. |
|
34 The customisations shown in this section are \emph{safe} |
|
35 as regards correctness: all programs that can be generated are partially |
|
36 correct.% |
|
37 \end{isamarkuptext}% |
|
38 \isamarkuptrue% |
|
39 % |
|
40 \isamarkupsubsection{Selecting code equations% |
|
41 } |
|
42 \isamarkuptrue% |
|
43 % |
|
44 \begin{isamarkuptext}% |
|
45 Coming back to our introductory example, we |
|
46 could provide an alternative code equations for \isa{dequeue} |
|
47 explicitly:% |
|
48 \end{isamarkuptext}% |
|
49 \isamarkuptrue% |
|
50 % |
|
51 \isadelimquote |
|
52 % |
|
53 \endisadelimquote |
|
54 % |
|
55 \isatagquote |
|
56 \isacommand{lemma}\isamarkupfalse% |
|
57 \ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
58 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
59 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline |
|
60 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
61 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
62 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
63 \ \ \isacommand{by}\isamarkupfalse% |
|
64 \ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% |
|
65 \endisatagquote |
|
66 {\isafoldquote}% |
|
67 % |
|
68 \isadelimquote |
|
69 % |
|
70 \endisadelimquote |
|
71 % |
|
72 \begin{isamarkuptext}% |
|
73 \noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar} |
|
74 \isa{attribute} which states that the given theorems should be |
|
75 considered as code equations for a \isa{fun} statement -- |
|
76 the corresponding constant is determined syntactically. The resulting code:% |
|
77 \end{isamarkuptext}% |
|
78 \isamarkuptrue% |
|
79 % |
|
80 \isadelimquote |
|
81 % |
|
82 \endisadelimquote |
|
83 % |
|
84 \isatagquote |
|
85 % |
|
86 \begin{isamarkuptext}% |
|
87 \isatypewriter% |
|
88 \noindent% |
|
89 \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ |
|
90 \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ |
|
91 \hspace*{0pt}dequeue (AQueue xs []) =\\ |
|
92 \hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ |
|
93 \hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% |
|
94 \end{isamarkuptext}% |
|
95 \isamarkuptrue% |
|
96 % |
|
97 \endisatagquote |
|
98 {\isafoldquote}% |
|
99 % |
|
100 \isadelimquote |
|
101 % |
|
102 \endisadelimquote |
|
103 % |
|
104 \begin{isamarkuptext}% |
|
105 \noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been |
|
106 replaced by the predicate \isa{null\ xs}. This is due to the default |
|
107 setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). |
|
108 |
|
109 Changing the default constructor set of datatypes is also |
|
110 possible. See \secref{sec:datatypes} for an example. |
|
111 |
|
112 As told in \secref{sec:concept}, code generation is based |
|
113 on a structured collection of code theorems. |
|
114 This collection |
|
115 may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:% |
|
116 \end{isamarkuptext}% |
|
117 \isamarkuptrue% |
|
118 % |
|
119 \isadelimquote |
|
120 % |
|
121 \endisadelimquote |
|
122 % |
|
123 \isatagquote |
|
124 \isacommand{code{\isacharunderscore}thms}\isamarkupfalse% |
|
125 \ dequeue% |
|
126 \endisatagquote |
|
127 {\isafoldquote}% |
|
128 % |
|
129 \isadelimquote |
|
130 % |
|
131 \endisadelimquote |
|
132 % |
|
133 \begin{isamarkuptext}% |
|
134 \noindent prints a table with \emph{all} code equations |
|
135 for \isa{dequeue}, including |
|
136 \emph{all} code equations those equations depend |
|
137 on recursively. |
|
138 |
|
139 Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph |
|
140 visualising dependencies between code equations.% |
|
141 \end{isamarkuptext}% |
|
142 \isamarkuptrue% |
|
143 % |
|
144 \isamarkupsubsection{\isa{class} and \isa{instantiation}% |
|
145 } |
|
146 \isamarkuptrue% |
|
147 % |
|
148 \begin{isamarkuptext}% |
|
149 Concerning type classes and code generation, let us examine an example |
|
150 from abstract algebra:% |
|
151 \end{isamarkuptext}% |
|
152 \isamarkuptrue% |
|
153 % |
|
154 \isadelimquote |
|
155 % |
|
156 \endisadelimquote |
|
157 % |
|
158 \isatagquote |
|
159 \isacommand{class}\isamarkupfalse% |
|
160 \ semigroup\ {\isacharequal}\isanewline |
|
161 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
162 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
163 \isanewline |
|
164 \isacommand{class}\isamarkupfalse% |
|
165 \ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline |
|
166 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
167 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
168 \ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
169 \isanewline |
|
170 \isacommand{instantiation}\isamarkupfalse% |
|
171 \ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline |
|
172 \isakeyword{begin}\isanewline |
|
173 \isanewline |
|
174 \isacommand{primrec}\isamarkupfalse% |
|
175 \ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline |
|
176 \ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
177 \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline |
|
178 \isanewline |
|
179 \isacommand{definition}\isamarkupfalse% |
|
180 \ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline |
|
181 \ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline |
|
182 \isanewline |
|
183 \isacommand{lemma}\isamarkupfalse% |
|
184 \ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline |
|
185 \ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
|
186 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline |
|
187 \ \ \isacommand{by}\isamarkupfalse% |
|
188 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline |
|
189 \isanewline |
|
190 \isacommand{instance}\isamarkupfalse% |
|
191 \ \isacommand{proof}\isamarkupfalse% |
|
192 \isanewline |
|
193 \ \ \isacommand{fix}\isamarkupfalse% |
|
194 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
|
195 \ \ \isacommand{show}\isamarkupfalse% |
|
196 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
197 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
198 \ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline |
|
199 \ \ \isacommand{show}\isamarkupfalse% |
|
200 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline |
|
201 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
202 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline |
|
203 \ \ \isacommand{show}\isamarkupfalse% |
|
204 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline |
|
205 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
206 \ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline |
|
207 \isacommand{qed}\isamarkupfalse% |
|
208 \isanewline |
|
209 \isanewline |
|
210 \isacommand{end}\isamarkupfalse% |
|
211 % |
|
212 \endisatagquote |
|
213 {\isafoldquote}% |
|
214 % |
|
215 \isadelimquote |
|
216 % |
|
217 \endisadelimquote |
|
218 % |
|
219 \begin{isamarkuptext}% |
|
220 \noindent We define the natural operation of the natural numbers |
|
221 on monoids:% |
|
222 \end{isamarkuptext}% |
|
223 \isamarkuptrue% |
|
224 % |
|
225 \isadelimquote |
|
226 % |
|
227 \endisadelimquote |
|
228 % |
|
229 \isatagquote |
|
230 \isacommand{primrec}\isamarkupfalse% |
|
231 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
232 \ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
|
233 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}% |
|
234 \endisatagquote |
|
235 {\isafoldquote}% |
|
236 % |
|
237 \isadelimquote |
|
238 % |
|
239 \endisadelimquote |
|
240 % |
|
241 \begin{isamarkuptext}% |
|
242 \noindent This we use to define the discrete exponentiation function:% |
|
243 \end{isamarkuptext}% |
|
244 \isamarkuptrue% |
|
245 % |
|
246 \isadelimquote |
|
247 % |
|
248 \endisadelimquote |
|
249 % |
|
250 \isatagquote |
|
251 \isacommand{definition}\isamarkupfalse% |
|
252 \ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
253 \ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
|
254 \endisatagquote |
|
255 {\isafoldquote}% |
|
256 % |
|
257 \isadelimquote |
|
258 % |
|
259 \endisadelimquote |
|
260 % |
|
261 \begin{isamarkuptext}% |
|
262 \noindent The corresponding code in Haskell uses that language's native classes:% |
|
263 \end{isamarkuptext}% |
|
264 \isamarkuptrue% |
|
265 % |
|
266 \isadelimquote |
|
267 % |
|
268 \endisadelimquote |
|
269 % |
|
270 \isatagquote |
|
271 % |
|
272 \begin{isamarkuptext}% |
|
273 \isatypewriter% |
|
274 \noindent% |
|
275 \hspace*{0pt}module Example where {\char123}\\ |
|
276 \hspace*{0pt}\\ |
|
277 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ |
|
278 \hspace*{0pt}\\ |
|
279 \hspace*{0pt}class Semigroup a where {\char123}\\ |
|
280 \hspace*{0pt} ~mult ::~a -> a -> a;\\ |
|
281 \hspace*{0pt}{\char125};\\ |
|
282 \hspace*{0pt}\\ |
|
283 \hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ |
|
284 \hspace*{0pt} ~neutral ::~a;\\ |
|
285 \hspace*{0pt}{\char125};\\ |
|
286 \hspace*{0pt}\\ |
|
287 \hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ |
|
288 \hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ |
|
289 \hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ |
|
290 \hspace*{0pt}\\ |
|
291 \hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ |
|
292 \hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ |
|
293 \hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ |
|
294 \hspace*{0pt}\\ |
|
295 \hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ |
|
296 \hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ |
|
297 \hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
|
298 \hspace*{0pt}\\ |
|
299 \hspace*{0pt}neutral{\char95}nat ::~Nat;\\ |
|
300 \hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ |
|
301 \hspace*{0pt}\\ |
|
302 \hspace*{0pt}instance Semigroup Nat where {\char123}\\ |
|
303 \hspace*{0pt} ~mult = mult{\char95}nat;\\ |
|
304 \hspace*{0pt}{\char125};\\ |
|
305 \hspace*{0pt}\\ |
|
306 \hspace*{0pt}instance Monoid Nat where {\char123}\\ |
|
307 \hspace*{0pt} ~neutral = neutral{\char95}nat;\\ |
|
308 \hspace*{0pt}{\char125};\\ |
|
309 \hspace*{0pt}\\ |
|
310 \hspace*{0pt}bexp ::~Nat -> Nat;\\ |
|
311 \hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ |
|
312 \hspace*{0pt}\\ |
|
313 \hspace*{0pt}{\char125}% |
|
314 \end{isamarkuptext}% |
|
315 \isamarkuptrue% |
|
316 % |
|
317 \endisatagquote |
|
318 {\isafoldquote}% |
|
319 % |
|
320 \isadelimquote |
|
321 % |
|
322 \endisadelimquote |
|
323 % |
|
324 \begin{isamarkuptext}% |
|
325 \noindent This is a convenient place to show how explicit dictionary construction |
|
326 manifests in generated code (here, the same example in \isa{SML}) |
|
327 \cite{Haftmann-Nipkow:2010:code}:% |
|
328 \end{isamarkuptext}% |
|
329 \isamarkuptrue% |
|
330 % |
|
331 \isadelimquote |
|
332 % |
|
333 \endisadelimquote |
|
334 % |
|
335 \isatagquote |
|
336 % |
|
337 \begin{isamarkuptext}% |
|
338 \isatypewriter% |
|
339 \noindent% |
|
340 \hspace*{0pt}structure Example :~sig\\ |
|
341 \hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\ |
|
342 \hspace*{0pt} ~type 'a semigroup\\ |
|
343 \hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\ |
|
344 \hspace*{0pt} ~type 'a monoid\\ |
|
345 \hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\ |
|
346 \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ |
|
347 \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ |
|
348 \hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\ |
|
349 \hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ |
|
350 \hspace*{0pt} ~val neutral{\char95}nat :~nat\\ |
|
351 \hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ |
|
352 \hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ |
|
353 \hspace*{0pt} ~val bexp :~nat -> nat\\ |
|
354 \hspace*{0pt}end = struct\\ |
|
355 \hspace*{0pt}\\ |
|
356 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
|
357 \hspace*{0pt}\\ |
|
358 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ |
|
359 \hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\ |
|
360 \hspace*{0pt}\\ |
|
361 \hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ |
|
362 \hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\ |
|
363 \hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\ |
|
364 \hspace*{0pt}\\ |
|
365 \hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ |
|
366 \hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ |
|
367 \hspace*{0pt}\\ |
|
368 \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ |
|
369 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ |
|
370 \hspace*{0pt}\\ |
|
371 \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ |
|
372 \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
|
373 \hspace*{0pt}\\ |
|
374 \hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ |
|
375 \hspace*{0pt}\\ |
|
376 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ |
|
377 \hspace*{0pt}\\ |
|
378 \hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ |
|
379 \hspace*{0pt} ~:~nat monoid;\\ |
|
380 \hspace*{0pt}\\ |
|
381 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ |
|
382 \hspace*{0pt}\\ |
|
383 \hspace*{0pt}end;~(*struct Example*)% |
|
384 \end{isamarkuptext}% |
|
385 \isamarkuptrue% |
|
386 % |
|
387 \endisatagquote |
|
388 {\isafoldquote}% |
|
389 % |
|
390 \isadelimquote |
|
391 % |
|
392 \endisadelimquote |
|
393 % |
|
394 \begin{isamarkuptext}% |
|
395 \noindent Note the parameters with trailing underscore (\verb|A_|), |
|
396 which are the dictionary parameters.% |
|
397 \end{isamarkuptext}% |
|
398 \isamarkuptrue% |
|
399 % |
|
400 \isamarkupsubsection{The preprocessor \label{sec:preproc}% |
|
401 } |
|
402 \isamarkuptrue% |
|
403 % |
|
404 \begin{isamarkuptext}% |
|
405 Before selected function theorems are turned into abstract |
|
406 code, a chain of definitional transformation steps is carried |
|
407 out: \emph{preprocessing}. In essence, the preprocessor |
|
408 consists of two components: a \emph{simpset} and \emph{function transformers}. |
|
409 |
|
410 The \emph{simpset} can apply the full generality of the |
|
411 Isabelle simplifier. Due to the interpretation of theorems as code |
|
412 equations, rewrites are applied to the right hand side and the |
|
413 arguments of the left hand side of an equation, but never to the |
|
414 constant heading the left hand side. An important special case are |
|
415 \emph{unfold theorems}, which may be declared and removed using |
|
416 the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del} |
|
417 attribute, respectively. |
|
418 |
|
419 Some common applications:% |
|
420 \end{isamarkuptext}% |
|
421 \isamarkuptrue% |
|
422 % |
|
423 \begin{itemize} |
|
424 % |
|
425 \begin{isamarkuptext}% |
|
426 \item replacing non-executable constructs by executable ones:% |
|
427 \end{isamarkuptext}% |
|
428 \isamarkuptrue% |
|
429 % |
|
430 \isadelimquote |
|
431 % |
|
432 \endisadelimquote |
|
433 % |
|
434 \isatagquote |
|
435 \isacommand{lemma}\isamarkupfalse% |
|
436 \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline |
|
437 \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
438 \ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}% |
|
439 \endisatagquote |
|
440 {\isafoldquote}% |
|
441 % |
|
442 \isadelimquote |
|
443 % |
|
444 \endisadelimquote |
|
445 % |
|
446 \begin{isamarkuptext}% |
|
447 \item eliminating superfluous constants:% |
|
448 \end{isamarkuptext}% |
|
449 \isamarkuptrue% |
|
450 % |
|
451 \isadelimquote |
|
452 % |
|
453 \endisadelimquote |
|
454 % |
|
455 \isatagquote |
|
456 \isacommand{lemma}\isamarkupfalse% |
|
457 \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline |
|
458 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
459 \ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}% |
|
460 \endisatagquote |
|
461 {\isafoldquote}% |
|
462 % |
|
463 \isadelimquote |
|
464 % |
|
465 \endisadelimquote |
|
466 % |
|
467 \begin{isamarkuptext}% |
|
468 \item replacing executable but inconvenient constructs:% |
|
469 \end{isamarkuptext}% |
|
470 \isamarkuptrue% |
|
471 % |
|
472 \isadelimquote |
|
473 % |
|
474 \endisadelimquote |
|
475 % |
|
476 \isatagquote |
|
477 \isacommand{lemma}\isamarkupfalse% |
|
478 \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline |
|
479 \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
480 \ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}% |
|
481 \endisatagquote |
|
482 {\isafoldquote}% |
|
483 % |
|
484 \isadelimquote |
|
485 % |
|
486 \endisadelimquote |
|
487 % |
|
488 \end{itemize} |
|
489 % |
|
490 \begin{isamarkuptext}% |
|
491 \noindent \emph{Function transformers} provide a very general interface, |
|
492 transforming a list of function theorems to another |
|
493 list of function theorems, provided that neither the heading |
|
494 constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc} |
|
495 pattern elimination implemented in |
|
496 theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this |
|
497 interface. |
|
498 |
|
499 \noindent The current setup of the preprocessor may be inspected using |
|
500 the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. |
|
501 \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient |
|
502 mechanism to inspect the impact of a preprocessor setup |
|
503 on code equations. |
|
504 |
|
505 \begin{warn} |
|
506 |
|
507 Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the |
|
508 preprocessor of the ancient \isa{SML\ code\ generator}; in case |
|
509 this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead. |
|
510 \end{warn}% |
|
511 \end{isamarkuptext}% |
|
512 \isamarkuptrue% |
|
513 % |
|
514 \isamarkupsubsection{Datatypes \label{sec:datatypes}% |
|
515 } |
|
516 \isamarkuptrue% |
|
517 % |
|
518 \begin{isamarkuptext}% |
|
519 Conceptually, any datatype is spanned by a set of |
|
520 \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in |
|
521 \isa{{\isasymtau}}. The HOL datatype package by default registers any new |
|
522 datatype in the table of datatypes, which may be inspected using the |
|
523 \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. |
|
524 |
|
525 In some cases, it is appropriate to alter or extend this table. As |
|
526 an example, we will develop an alternative representation of the |
|
527 queue example given in \secref{sec:intro}. The amortised |
|
528 representation is convenient for generating code but exposes its |
|
529 \qt{implementation} details, which may be cumbersome when proving |
|
530 theorems about it. Therefore, here is a simple, straightforward |
|
531 representation of queues:% |
|
532 \end{isamarkuptext}% |
|
533 \isamarkuptrue% |
|
534 % |
|
535 \isadelimquote |
|
536 % |
|
537 \endisadelimquote |
|
538 % |
|
539 \isatagquote |
|
540 \isacommand{datatype}\isamarkupfalse% |
|
541 \ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline |
|
542 \isanewline |
|
543 \isacommand{definition}\isamarkupfalse% |
|
544 \ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
545 \ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
546 \isanewline |
|
547 \isacommand{primrec}\isamarkupfalse% |
|
548 \ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
549 \ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
550 \isanewline |
|
551 \isacommand{fun}\isamarkupfalse% |
|
552 \ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
553 \ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
554 \ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}% |
|
555 \endisatagquote |
|
556 {\isafoldquote}% |
|
557 % |
|
558 \isadelimquote |
|
559 % |
|
560 \endisadelimquote |
|
561 % |
|
562 \begin{isamarkuptext}% |
|
563 \noindent This we can use directly for proving; for executing, |
|
564 we provide an alternative characterisation:% |
|
565 \end{isamarkuptext}% |
|
566 \isamarkuptrue% |
|
567 % |
|
568 \isadelimquote |
|
569 % |
|
570 \endisadelimquote |
|
571 % |
|
572 \isatagquote |
|
573 \isacommand{definition}\isamarkupfalse% |
|
574 \ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
575 \ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
576 \isanewline |
|
577 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% |
|
578 \ AQueue% |
|
579 \endisatagquote |
|
580 {\isafoldquote}% |
|
581 % |
|
582 \isadelimquote |
|
583 % |
|
584 \endisadelimquote |
|
585 % |
|
586 \begin{isamarkuptext}% |
|
587 \noindent Here we define a \qt{constructor} \isa{AQueue} which |
|
588 is defined in terms of \isa{Queue} and interprets its arguments |
|
589 according to what the \emph{content} of an amortised queue is supposed |
|
590 to be. Equipped with this, we are able to prove the following equations |
|
591 for our primitive queue operations which \qt{implement} the simple |
|
592 queues in an amortised fashion:% |
|
593 \end{isamarkuptext}% |
|
594 \isamarkuptrue% |
|
595 % |
|
596 \isadelimquote |
|
597 % |
|
598 \endisadelimquote |
|
599 % |
|
600 \isatagquote |
|
601 \isacommand{lemma}\isamarkupfalse% |
|
602 \ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
603 \ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
604 \ \ \isacommand{unfolding}\isamarkupfalse% |
|
605 \ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
606 \ simp\isanewline |
|
607 \isanewline |
|
608 \isacommand{lemma}\isamarkupfalse% |
|
609 \ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
610 \ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline |
|
611 \ \ \isacommand{unfolding}\isamarkupfalse% |
|
612 \ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
613 \ simp\isanewline |
|
614 \isanewline |
|
615 \isacommand{lemma}\isamarkupfalse% |
|
616 \ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
617 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
618 \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline |
|
619 \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
620 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
621 \ \ \isacommand{unfolding}\isamarkupfalse% |
|
622 \ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
623 \ simp{\isacharunderscore}all% |
|
624 \endisatagquote |
|
625 {\isafoldquote}% |
|
626 % |
|
627 \isadelimquote |
|
628 % |
|
629 \endisadelimquote |
|
630 % |
|
631 \begin{isamarkuptext}% |
|
632 \noindent For completeness, we provide a substitute for the |
|
633 \isa{case} combinator on queues:% |
|
634 \end{isamarkuptext}% |
|
635 \isamarkuptrue% |
|
636 % |
|
637 \isadelimquote |
|
638 % |
|
639 \endisadelimquote |
|
640 % |
|
641 \isatagquote |
|
642 \isacommand{lemma}\isamarkupfalse% |
|
643 \ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
644 \ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
645 \ \ \isacommand{unfolding}\isamarkupfalse% |
|
646 \ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
647 \ simp% |
|
648 \endisatagquote |
|
649 {\isafoldquote}% |
|
650 % |
|
651 \isadelimquote |
|
652 % |
|
653 \endisadelimquote |
|
654 % |
|
655 \begin{isamarkuptext}% |
|
656 \noindent The resulting code looks as expected:% |
|
657 \end{isamarkuptext}% |
|
658 \isamarkuptrue% |
|
659 % |
|
660 \isadelimquote |
|
661 % |
|
662 \endisadelimquote |
|
663 % |
|
664 \isatagquote |
|
665 % |
|
666 \begin{isamarkuptext}% |
|
667 \isatypewriter% |
|
668 \noindent% |
|
669 \hspace*{0pt}structure Example :~sig\\ |
|
670 \hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\ |
|
671 \hspace*{0pt} ~val rev :~'a list -> 'a list\\ |
|
672 \hspace*{0pt} ~val null :~'a list -> bool\\ |
|
673 \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ |
|
674 \hspace*{0pt} ~val empty :~'a queue\\ |
|
675 \hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\ |
|
676 \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\ |
|
677 \hspace*{0pt}end = struct\\ |
|
678 \hspace*{0pt}\\ |
|
679 \hspace*{0pt}fun foldl f a [] = a\\ |
|
680 \hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ |
|
681 \hspace*{0pt}\\ |
|
682 \hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ |
|
683 \hspace*{0pt}\\ |
|
684 \hspace*{0pt}fun null [] = true\\ |
|
685 \hspace*{0pt} ~| null (x ::~xs) = false;\\ |
|
686 \hspace*{0pt}\\ |
|
687 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ |
|
688 \hspace*{0pt}\\ |
|
689 \hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ |
|
690 \hspace*{0pt}\\ |
|
691 \hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ |
|
692 \hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\ |
|
693 \hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\ |
|
694 \hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\ |
|
695 \hspace*{0pt}\\ |
|
696 \hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ |
|
697 \hspace*{0pt}\\ |
|
698 \hspace*{0pt}end;~(*struct Example*)% |
|
699 \end{isamarkuptext}% |
|
700 \isamarkuptrue% |
|
701 % |
|
702 \endisatagquote |
|
703 {\isafoldquote}% |
|
704 % |
|
705 \isadelimquote |
|
706 % |
|
707 \endisadelimquote |
|
708 % |
|
709 \begin{isamarkuptext}% |
|
710 \noindent From this example, it can be glimpsed that using own |
|
711 constructor sets is a little delicate since it changes the set of |
|
712 valid patterns for values of that type. Without going into much |
|
713 detail, here some practical hints: |
|
714 |
|
715 \begin{itemize} |
|
716 |
|
717 \item When changing the constructor set for datatypes, take care |
|
718 to provide alternative equations for the \isa{case} combinator. |
|
719 |
|
720 \item Values in the target language need not to be normalised -- |
|
721 different values in the target language may represent the same |
|
722 value in the logic. |
|
723 |
|
724 \item Usually, a good methodology to deal with the subtleties of |
|
725 pattern matching is to see the type as an abstract type: provide |
|
726 a set of operations which operate on the concrete representation |
|
727 of the type, and derive further operations by combinations of |
|
728 these primitive ones, without relying on a particular |
|
729 representation. |
|
730 |
|
731 \end{itemize}% |
|
732 \end{isamarkuptext}% |
|
733 \isamarkuptrue% |
|
734 % |
|
735 \isamarkupsubsection{Equality% |
|
736 } |
|
737 \isamarkuptrue% |
|
738 % |
|
739 \begin{isamarkuptext}% |
|
740 Surely you have already noticed how equality is treated |
|
741 by the code generator:% |
|
742 \end{isamarkuptext}% |
|
743 \isamarkuptrue% |
|
744 % |
|
745 \isadelimquote |
|
746 % |
|
747 \endisadelimquote |
|
748 % |
|
749 \isatagquote |
|
750 \isacommand{primrec}\isamarkupfalse% |
|
751 \ 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 |
|
752 \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline |
|
753 \ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline |
|
754 \ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline |
|
755 \ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline |
|
756 \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline |
|
757 \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% |
|
758 \endisatagquote |
|
759 {\isafoldquote}% |
|
760 % |
|
761 \isadelimquote |
|
762 % |
|
763 \endisadelimquote |
|
764 % |
|
765 \begin{isamarkuptext}% |
|
766 \noindent During preprocessing, the membership test is rewritten, |
|
767 resulting in \isa{List{\isachardot}member}, which itself |
|
768 performs an explicit equality check.% |
|
769 \end{isamarkuptext}% |
|
770 \isamarkuptrue% |
|
771 % |
|
772 \isadelimquote |
|
773 % |
|
774 \endisadelimquote |
|
775 % |
|
776 \isatagquote |
|
777 % |
|
778 \begin{isamarkuptext}% |
|
779 \isatypewriter% |
|
780 \noindent% |
|
781 \hspace*{0pt}structure Example :~sig\\ |
|
782 \hspace*{0pt} ~type 'a eq\\ |
|
783 \hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\ |
|
784 \hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\ |
|
785 \hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\ |
|
786 \hspace*{0pt} ~val collect{\char95}duplicates :\\ |
|
787 \hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\ |
|
788 \hspace*{0pt}end = struct\\ |
|
789 \hspace*{0pt}\\ |
|
790 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
|
791 \hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\ |
|
792 \hspace*{0pt}\\ |
|
793 \hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\ |
|
794 \hspace*{0pt}\\ |
|
795 \hspace*{0pt}fun member A{\char95}~[] y = false\\ |
|
796 \hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\ |
|
797 \hspace*{0pt}\\ |
|
798 \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ |
|
799 \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ |
|
800 \hspace*{0pt} ~~~(if member A{\char95}~xs z\\ |
|
801 \hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\ |
|
802 \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ |
|
803 \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ |
|
804 \hspace*{0pt}\\ |
|
805 \hspace*{0pt}end;~(*struct Example*)% |
|
806 \end{isamarkuptext}% |
|
807 \isamarkuptrue% |
|
808 % |
|
809 \endisatagquote |
|
810 {\isafoldquote}% |
|
811 % |
|
812 \isadelimquote |
|
813 % |
|
814 \endisadelimquote |
|
815 % |
|
816 \begin{isamarkuptext}% |
|
817 \noindent Obviously, polymorphic equality is implemented the Haskell |
|
818 way using a type class. How is this achieved? HOL introduces |
|
819 an explicit class \isa{eq} with a corresponding operation |
|
820 \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. |
|
821 The preprocessing framework does the rest by propagating the |
|
822 \isa{eq} constraints through all dependent code equations. |
|
823 For datatypes, instances of \isa{eq} are implicitly derived |
|
824 when possible. For other types, you may instantiate \isa{eq} |
|
825 manually like any other type class.% |
|
826 \end{isamarkuptext}% |
|
827 \isamarkuptrue% |
|
828 % |
|
829 \isamarkupsubsection{Explicit partiality% |
|
830 } |
|
831 \isamarkuptrue% |
|
832 % |
|
833 \begin{isamarkuptext}% |
|
834 Partiality usually enters the game by partial patterns, as |
|
835 in the following example, again for amortised queues:% |
|
836 \end{isamarkuptext}% |
|
837 \isamarkuptrue% |
|
838 % |
|
839 \isadelimquote |
|
840 % |
|
841 \endisadelimquote |
|
842 % |
|
843 \isatagquote |
|
844 \isacommand{definition}\isamarkupfalse% |
|
845 \ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
846 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline |
|
847 \ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
848 \isanewline |
|
849 \isacommand{lemma}\isamarkupfalse% |
|
850 \ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
851 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
852 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
853 \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
854 \ \ \isacommand{by}\isamarkupfalse% |
|
855 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% |
|
856 \endisatagquote |
|
857 {\isafoldquote}% |
|
858 % |
|
859 \isadelimquote |
|
860 % |
|
861 \endisadelimquote |
|
862 % |
|
863 \begin{isamarkuptext}% |
|
864 \noindent In the corresponding code, there is no equation |
|
865 for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:% |
|
866 \end{isamarkuptext}% |
|
867 \isamarkuptrue% |
|
868 % |
|
869 \isadelimquote |
|
870 % |
|
871 \endisadelimquote |
|
872 % |
|
873 \isatagquote |
|
874 % |
|
875 \begin{isamarkuptext}% |
|
876 \isatypewriter% |
|
877 \noindent% |
|
878 \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ |
|
879 \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ |
|
880 \hspace*{0pt} ~let {\char123}\\ |
|
881 \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ |
|
882 \hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ |
|
883 \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% |
|
884 \end{isamarkuptext}% |
|
885 \isamarkuptrue% |
|
886 % |
|
887 \endisatagquote |
|
888 {\isafoldquote}% |
|
889 % |
|
890 \isadelimquote |
|
891 % |
|
892 \endisadelimquote |
|
893 % |
|
894 \begin{isamarkuptext}% |
|
895 \noindent In some cases it is desirable to have this |
|
896 pseudo-\qt{partiality} more explicitly, e.g.~as follows:% |
|
897 \end{isamarkuptext}% |
|
898 \isamarkuptrue% |
|
899 % |
|
900 \isadelimquote |
|
901 % |
|
902 \endisadelimquote |
|
903 % |
|
904 \isatagquote |
|
905 \isacommand{axiomatization}\isamarkupfalse% |
|
906 \ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline |
|
907 \isanewline |
|
908 \isacommand{definition}\isamarkupfalse% |
|
909 \ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
910 \ \ {\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 |
|
911 \isanewline |
|
912 \isacommand{lemma}\isamarkupfalse% |
|
913 \ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
914 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline |
|
915 \ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
916 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
917 \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
918 \ \ \isacommand{by}\isamarkupfalse% |
|
919 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% |
|
920 \endisatagquote |
|
921 {\isafoldquote}% |
|
922 % |
|
923 \isadelimquote |
|
924 % |
|
925 \endisadelimquote |
|
926 % |
|
927 \begin{isamarkuptext}% |
|
928 Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs. |
|
929 |
|
930 Normally, if constants without any code equations occur in a |
|
931 program, the code generator complains (since in most cases this is |
|
932 indeed an error). But such constants can also be thought |
|
933 of as function definitions which always fail, |
|
934 since there is never a successful pattern match on the left hand |
|
935 side. In order to categorise a constant into that category |
|
936 explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:% |
|
937 \end{isamarkuptext}% |
|
938 \isamarkuptrue% |
|
939 % |
|
940 \isadelimquote |
|
941 % |
|
942 \endisadelimquote |
|
943 % |
|
944 \isatagquote |
|
945 \isacommand{code{\isacharunderscore}abort}\isamarkupfalse% |
|
946 \ empty{\isacharunderscore}queue% |
|
947 \endisatagquote |
|
948 {\isafoldquote}% |
|
949 % |
|
950 \isadelimquote |
|
951 % |
|
952 \endisadelimquote |
|
953 % |
|
954 \begin{isamarkuptext}% |
|
955 \noindent Then the code generator will just insert an error or |
|
956 exception at the appropriate position:% |
|
957 \end{isamarkuptext}% |
|
958 \isamarkuptrue% |
|
959 % |
|
960 \isadelimquote |
|
961 % |
|
962 \endisadelimquote |
|
963 % |
|
964 \isatagquote |
|
965 % |
|
966 \begin{isamarkuptext}% |
|
967 \isatypewriter% |
|
968 \noindent% |
|
969 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ |
|
970 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ |
|
971 \hspace*{0pt}\\ |
|
972 \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ |
|
973 \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ |
|
974 \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ |
|
975 \hspace*{0pt} ~(if null xs then empty{\char95}queue\\ |
|
976 \hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% |
|
977 \end{isamarkuptext}% |
|
978 \isamarkuptrue% |
|
979 % |
|
980 \endisatagquote |
|
981 {\isafoldquote}% |
|
982 % |
|
983 \isadelimquote |
|
984 % |
|
985 \endisadelimquote |
|
986 % |
|
987 \begin{isamarkuptext}% |
|
988 \noindent This feature however is rarely needed in practice. |
|
989 Note also that the \isa{HOL} default setup already declares |
|
990 \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most |
|
991 likely to be used in such situations.% |
|
992 \end{isamarkuptext}% |
|
993 \isamarkuptrue% |
|
994 % |
|
995 \isadelimtheory |
|
996 % |
|
997 \endisadelimtheory |
|
998 % |
|
999 \isatagtheory |
|
1000 \isacommand{end}\isamarkupfalse% |
|
1001 % |
|
1002 \endisatagtheory |
|
1003 {\isafoldtheory}% |
|
1004 % |
|
1005 \isadelimtheory |
|
1006 % |
|
1007 \endisadelimtheory |
|
1008 \isanewline |
|
1009 \end{isabellebody}% |
|
1010 %%% Local Variables: |
|
1011 %%% mode: latex |
|
1012 %%% TeX-master: "root" |
|
1013 %%% End: |
|