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}}}}/\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 All kinds of customisation shown in this section is \emph{safe} |
|
35 in the sense that the user does not have to worry about |
|
36 correctness -- all programs generatable that way are partially |
|
37 correct.% |
|
38 \end{isamarkuptext}% |
|
39 \isamarkuptrue% |
|
40 % |
|
41 \isamarkupsubsection{Selecting code equations% |
|
42 } |
|
43 \isamarkuptrue% |
|
44 % |
|
45 \begin{isamarkuptext}% |
|
46 Coming back to our introductory example, we |
|
47 could provide an alternative code equations for \isa{dequeue} |
|
48 explicitly:% |
|
49 \end{isamarkuptext}% |
|
50 \isamarkuptrue% |
|
51 % |
|
52 \isadelimquote |
|
53 % |
|
54 \endisadelimquote |
|
55 % |
|
56 \isatagquote |
|
57 \isacommand{lemma}\isamarkupfalse% |
|
58 \ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
59 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
60 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline |
|
61 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
62 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
63 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
64 \ \ \isacommand{by}\isamarkupfalse% |
|
65 \ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% |
|
66 \endisatagquote |
|
67 {\isafoldquote}% |
|
68 % |
|
69 \isadelimquote |
|
70 % |
|
71 \endisadelimquote |
|
72 % |
|
73 \begin{isamarkuptext}% |
|
74 \noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar} |
|
75 \isa{attribute} which states that the given theorems should be |
|
76 considered as code equations for a \isa{fun} statement -- |
|
77 the corresponding constant is determined syntactically. The resulting code:% |
|
78 \end{isamarkuptext}% |
|
79 \isamarkuptrue% |
|
80 % |
|
81 \isadelimquote |
|
82 % |
|
83 \endisadelimquote |
|
84 % |
|
85 \isatagquote |
|
86 % |
|
87 \begin{isamarkuptext}% |
|
88 \isatypewriter% |
|
89 \noindent% |
|
90 \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ |
|
91 \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ |
|
92 \hspace*{0pt}dequeue (AQueue xs []) =\\ |
|
93 \hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\ |
|
94 \hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));% |
|
95 \end{isamarkuptext}% |
|
96 \isamarkuptrue% |
|
97 % |
|
98 \endisatagquote |
|
99 {\isafoldquote}% |
|
100 % |
|
101 \isadelimquote |
|
102 % |
|
103 \endisadelimquote |
|
104 % |
|
105 \begin{isamarkuptext}% |
|
106 \noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been |
|
107 replaced by the predicate \isa{null\ xs}. This is due to the default |
|
108 setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). |
|
109 |
|
110 Changing the default constructor set of datatypes is also |
|
111 possible. See \secref{sec:datatypes} for an example. |
|
112 |
|
113 As told in \secref{sec:concept}, code generation is based |
|
114 on a structured collection of code theorems. |
|
115 For explorative purpose, this collection |
|
116 may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:% |
|
117 \end{isamarkuptext}% |
|
118 \isamarkuptrue% |
|
119 % |
|
120 \isadelimquote |
|
121 % |
|
122 \endisadelimquote |
|
123 % |
|
124 \isatagquote |
|
125 \isacommand{code{\isacharunderscore}thms}\isamarkupfalse% |
|
126 \ dequeue% |
|
127 \endisatagquote |
|
128 {\isafoldquote}% |
|
129 % |
|
130 \isadelimquote |
|
131 % |
|
132 \endisadelimquote |
|
133 % |
|
134 \begin{isamarkuptext}% |
|
135 \noindent prints a table with \emph{all} code equations |
|
136 for \isa{dequeue}, including |
|
137 \emph{all} code equations those equations depend |
|
138 on recursively. |
|
139 |
|
140 Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph |
|
141 visualising dependencies between code equations.% |
|
142 \end{isamarkuptext}% |
|
143 \isamarkuptrue% |
|
144 % |
|
145 \isamarkupsubsection{\isa{class} and \isa{instantiation}% |
|
146 } |
|
147 \isamarkuptrue% |
|
148 % |
|
149 \begin{isamarkuptext}% |
|
150 Concerning type classes and code generation, let us examine an example |
|
151 from abstract algebra:% |
|
152 \end{isamarkuptext}% |
|
153 \isamarkuptrue% |
|
154 % |
|
155 \isadelimquote |
|
156 % |
|
157 \endisadelimquote |
|
158 % |
|
159 \isatagquote |
|
160 \isacommand{class}\isamarkupfalse% |
|
161 \ semigroup\ {\isacharequal}\isanewline |
|
162 \ \ \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 |
|
163 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
164 \isanewline |
|
165 \isacommand{class}\isamarkupfalse% |
|
166 \ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline |
|
167 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
168 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
169 \ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
170 \isanewline |
|
171 \isacommand{instantiation}\isamarkupfalse% |
|
172 \ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline |
|
173 \isakeyword{begin}\isanewline |
|
174 \isanewline |
|
175 \isacommand{primrec}\isamarkupfalse% |
|
176 \ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline |
|
177 \ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
178 \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline |
|
179 \isanewline |
|
180 \isacommand{definition}\isamarkupfalse% |
|
181 \ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline |
|
182 \ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline |
|
183 \isanewline |
|
184 \isacommand{lemma}\isamarkupfalse% |
|
185 \ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline |
|
186 \ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
|
187 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline |
|
188 \ \ \isacommand{by}\isamarkupfalse% |
|
189 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline |
|
190 \isanewline |
|
191 \isacommand{instance}\isamarkupfalse% |
|
192 \ \isacommand{proof}\isamarkupfalse% |
|
193 \isanewline |
|
194 \ \ \isacommand{fix}\isamarkupfalse% |
|
195 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
|
196 \ \ \isacommand{show}\isamarkupfalse% |
|
197 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
198 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
199 \ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline |
|
200 \ \ \isacommand{show}\isamarkupfalse% |
|
201 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline |
|
202 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
203 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline |
|
204 \ \ \isacommand{show}\isamarkupfalse% |
|
205 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline |
|
206 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
207 \ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline |
|
208 \isacommand{qed}\isamarkupfalse% |
|
209 \isanewline |
|
210 \isanewline |
|
211 \isacommand{end}\isamarkupfalse% |
|
212 % |
|
213 \endisatagquote |
|
214 {\isafoldquote}% |
|
215 % |
|
216 \isadelimquote |
|
217 % |
|
218 \endisadelimquote |
|
219 % |
|
220 \begin{isamarkuptext}% |
|
221 \noindent We define the natural operation of the natural numbers |
|
222 on monoids:% |
|
223 \end{isamarkuptext}% |
|
224 \isamarkuptrue% |
|
225 % |
|
226 \isadelimquote |
|
227 % |
|
228 \endisadelimquote |
|
229 % |
|
230 \isatagquote |
|
231 \isacommand{primrec}\isamarkupfalse% |
|
232 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
233 \ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
|
234 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}% |
|
235 \endisatagquote |
|
236 {\isafoldquote}% |
|
237 % |
|
238 \isadelimquote |
|
239 % |
|
240 \endisadelimquote |
|
241 % |
|
242 \begin{isamarkuptext}% |
|
243 \noindent This we use to define the discrete exponentiation function:% |
|
244 \end{isamarkuptext}% |
|
245 \isamarkuptrue% |
|
246 % |
|
247 \isadelimquote |
|
248 % |
|
249 \endisadelimquote |
|
250 % |
|
251 \isatagquote |
|
252 \isacommand{definition}\isamarkupfalse% |
|
253 \ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
254 \ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
|
255 \endisatagquote |
|
256 {\isafoldquote}% |
|
257 % |
|
258 \isadelimquote |
|
259 % |
|
260 \endisadelimquote |
|
261 % |
|
262 \begin{isamarkuptext}% |
|
263 \noindent The corresponding code:% |
|
264 \end{isamarkuptext}% |
|
265 \isamarkuptrue% |
|
266 % |
|
267 \isadelimquote |
|
268 % |
|
269 \endisadelimquote |
|
270 % |
|
271 \isatagquote |
|
272 % |
|
273 \begin{isamarkuptext}% |
|
274 \isatypewriter% |
|
275 \noindent% |
|
276 \hspace*{0pt}module Example where {\char123}\\ |
|
277 \hspace*{0pt}\\ |
|
278 \hspace*{0pt}\\ |
|
279 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ |
|
280 \hspace*{0pt}\\ |
|
281 \hspace*{0pt}class Semigroup a where {\char123}\\ |
|
282 \hspace*{0pt} ~mult ::~a -> a -> a;\\ |
|
283 \hspace*{0pt}{\char125};\\ |
|
284 \hspace*{0pt}\\ |
|
285 \hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ |
|
286 \hspace*{0pt} ~neutral ::~a;\\ |
|
287 \hspace*{0pt}{\char125};\\ |
|
288 \hspace*{0pt}\\ |
|
289 \hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ |
|
290 \hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ |
|
291 \hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ |
|
292 \hspace*{0pt}\\ |
|
293 \hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ |
|
294 \hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ |
|
295 \hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ |
|
296 \hspace*{0pt}\\ |
|
297 \hspace*{0pt}neutral{\char95}nat ::~Nat;\\ |
|
298 \hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ |
|
299 \hspace*{0pt}\\ |
|
300 \hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ |
|
301 \hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ |
|
302 \hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
|
303 \hspace*{0pt}\\ |
|
304 \hspace*{0pt}instance Semigroup Nat where {\char123}\\ |
|
305 \hspace*{0pt} ~mult = mult{\char95}nat;\\ |
|
306 \hspace*{0pt}{\char125};\\ |
|
307 \hspace*{0pt}\\ |
|
308 \hspace*{0pt}instance Monoid Nat where {\char123}\\ |
|
309 \hspace*{0pt} ~neutral = neutral{\char95}nat;\\ |
|
310 \hspace*{0pt}{\char125};\\ |
|
311 \hspace*{0pt}\\ |
|
312 \hspace*{0pt}bexp ::~Nat -> Nat;\\ |
|
313 \hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ |
|
314 \hspace*{0pt}\\ |
|
315 \hspace*{0pt}{\char125}% |
|
316 \end{isamarkuptext}% |
|
317 \isamarkuptrue% |
|
318 % |
|
319 \endisatagquote |
|
320 {\isafoldquote}% |
|
321 % |
|
322 \isadelimquote |
|
323 % |
|
324 \endisadelimquote |
|
325 % |
|
326 \begin{isamarkuptext}% |
|
327 \noindent This is a convenient place to show how explicit dictionary construction |
|
328 manifests in generated code (here, the same example in \isa{SML}):% |
|
329 \end{isamarkuptext}% |
|
330 \isamarkuptrue% |
|
331 % |
|
332 \isadelimquote |
|
333 % |
|
334 \endisadelimquote |
|
335 % |
|
336 \isatagquote |
|
337 % |
|
338 \begin{isamarkuptext}% |
|
339 \isatypewriter% |
|
340 \noindent% |
|
341 \hspace*{0pt}structure Example = \\ |
|
342 \hspace*{0pt}struct\\ |
|
343 \hspace*{0pt}\\ |
|
344 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
|
345 \hspace*{0pt}\\ |
|
346 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ |
|
347 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\ |
|
348 \hspace*{0pt}\\ |
|
349 \hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ |
|
350 \hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\ |
|
351 \hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\ |
|
352 \hspace*{0pt}\\ |
|
353 \hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ |
|
354 \hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ |
|
355 \hspace*{0pt}\\ |
|
356 \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ |
|
357 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ |
|
358 \hspace*{0pt}\\ |
|
359 \hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\ |
|
360 \hspace*{0pt}\\ |
|
361 \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ |
|
362 \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
|
363 \hspace*{0pt}\\ |
|
364 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ |
|
365 \hspace*{0pt}\\ |
|
366 \hspace*{0pt}val monoid{\char95}nat =\\ |
|
367 \hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\ |
|
368 \hspace*{0pt} ~nat monoid;\\ |
|
369 \hspace*{0pt}\\ |
|
370 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ |
|
371 \hspace*{0pt}\\ |
|
372 \hspace*{0pt}end;~(*struct Example*)% |
|
373 \end{isamarkuptext}% |
|
374 \isamarkuptrue% |
|
375 % |
|
376 \endisatagquote |
|
377 {\isafoldquote}% |
|
378 % |
|
379 \isadelimquote |
|
380 % |
|
381 \endisadelimquote |
|
382 % |
|
383 \begin{isamarkuptext}% |
|
384 \noindent Note the parameters with trailing underscore (\verb|A_|) |
|
385 which are the dictionary parameters.% |
|
386 \end{isamarkuptext}% |
|
387 \isamarkuptrue% |
|
388 % |
|
389 \isamarkupsubsection{The preprocessor \label{sec:preproc}% |
|
390 } |
|
391 \isamarkuptrue% |
|
392 % |
|
393 \begin{isamarkuptext}% |
|
394 Before selected function theorems are turned into abstract |
|
395 code, a chain of definitional transformation steps is carried |
|
396 out: \emph{preprocessing}. In essence, the preprocessor |
|
397 consists of two components: a \emph{simpset} and \emph{function transformers}. |
|
398 |
|
399 The \emph{simpset} allows to employ the full generality of the Isabelle |
|
400 simplifier. Due to the interpretation of theorems |
|
401 as code equations, rewrites are applied to the right |
|
402 hand side and the arguments of the left hand side of an |
|
403 equation, but never to the constant heading the left hand side. |
|
404 An important special case are \emph{inline theorems} which may be |
|
405 declared and undeclared using the |
|
406 \emph{code inline} or \emph{code inline del} attribute respectively. |
|
407 |
|
408 Some common applications:% |
|
409 \end{isamarkuptext}% |
|
410 \isamarkuptrue% |
|
411 % |
|
412 \begin{itemize} |
|
413 % |
|
414 \begin{isamarkuptext}% |
|
415 \item replacing non-executable constructs by executable ones:% |
|
416 \end{isamarkuptext}% |
|
417 \isamarkuptrue% |
|
418 % |
|
419 \isadelimquote |
|
420 % |
|
421 \endisadelimquote |
|
422 % |
|
423 \isatagquote |
|
424 \isacommand{lemma}\isamarkupfalse% |
|
425 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline |
|
426 \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
427 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% |
|
428 \endisatagquote |
|
429 {\isafoldquote}% |
|
430 % |
|
431 \isadelimquote |
|
432 % |
|
433 \endisadelimquote |
|
434 % |
|
435 \begin{isamarkuptext}% |
|
436 \item eliminating superfluous constants:% |
|
437 \end{isamarkuptext}% |
|
438 \isamarkuptrue% |
|
439 % |
|
440 \isadelimquote |
|
441 % |
|
442 \endisadelimquote |
|
443 % |
|
444 \isatagquote |
|
445 \isacommand{lemma}\isamarkupfalse% |
|
446 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline |
|
447 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
448 \ simp% |
|
449 \endisatagquote |
|
450 {\isafoldquote}% |
|
451 % |
|
452 \isadelimquote |
|
453 % |
|
454 \endisadelimquote |
|
455 % |
|
456 \begin{isamarkuptext}% |
|
457 \item replacing executable but inconvenient constructs:% |
|
458 \end{isamarkuptext}% |
|
459 \isamarkuptrue% |
|
460 % |
|
461 \isadelimquote |
|
462 % |
|
463 \endisadelimquote |
|
464 % |
|
465 \isatagquote |
|
466 \isacommand{lemma}\isamarkupfalse% |
|
467 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline |
|
468 \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
469 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% |
|
470 \endisatagquote |
|
471 {\isafoldquote}% |
|
472 % |
|
473 \isadelimquote |
|
474 % |
|
475 \endisadelimquote |
|
476 % |
|
477 \end{itemize} |
|
478 % |
|
479 \begin{isamarkuptext}% |
|
480 \noindent \emph{Function transformers} provide a very general interface, |
|
481 transforming a list of function theorems to another |
|
482 list of function theorems, provided that neither the heading |
|
483 constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc} |
|
484 pattern elimination implemented in |
|
485 theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this |
|
486 interface. |
|
487 |
|
488 \noindent The current setup of the preprocessor may be inspected using |
|
489 the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. |
|
490 \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient |
|
491 mechanism to inspect the impact of a preprocessor setup |
|
492 on code equations. |
|
493 |
|
494 \begin{warn} |
|
495 The attribute \emph{code unfold} |
|
496 associated with the \isa{SML\ code\ generator} also applies to |
|
497 the \isa{generic\ code\ generator}: |
|
498 \emph{code unfold} implies \emph{code inline}. |
|
499 \end{warn}% |
|
500 \end{isamarkuptext}% |
|
501 \isamarkuptrue% |
|
502 % |
|
503 \isamarkupsubsection{Datatypes \label{sec:datatypes}% |
|
504 } |
|
505 \isamarkuptrue% |
|
506 % |
|
507 \begin{isamarkuptext}% |
|
508 Conceptually, any datatype is spanned by a set of |
|
509 \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 |
|
510 \isa{{\isasymtau}}. The HOL datatype package by default registers any new |
|
511 datatype in the table of datatypes, which may be inspected using the |
|
512 \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. |
|
513 |
|
514 In some cases, it is appropriate to alter or extend this table. As |
|
515 an example, we will develop an alternative representation of the |
|
516 queue example given in \secref{sec:intro}. The amortised |
|
517 representation is convenient for generating code but exposes its |
|
518 \qt{implementation} details, which may be cumbersome when proving |
|
519 theorems about it. Therefore, here a simple, straightforward |
|
520 representation of queues:% |
|
521 \end{isamarkuptext}% |
|
522 \isamarkuptrue% |
|
523 % |
|
524 \isadelimquote |
|
525 % |
|
526 \endisadelimquote |
|
527 % |
|
528 \isatagquote |
|
529 \isacommand{datatype}\isamarkupfalse% |
|
530 \ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline |
|
531 \isanewline |
|
532 \isacommand{definition}\isamarkupfalse% |
|
533 \ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
534 \ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
535 \isanewline |
|
536 \isacommand{primrec}\isamarkupfalse% |
|
537 \ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
538 \ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
539 \isanewline |
|
540 \isacommand{fun}\isamarkupfalse% |
|
541 \ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
542 \ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
543 \ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}% |
|
544 \endisatagquote |
|
545 {\isafoldquote}% |
|
546 % |
|
547 \isadelimquote |
|
548 % |
|
549 \endisadelimquote |
|
550 % |
|
551 \begin{isamarkuptext}% |
|
552 \noindent This we can use directly for proving; for executing, |
|
553 we provide an alternative characterisation:% |
|
554 \end{isamarkuptext}% |
|
555 \isamarkuptrue% |
|
556 % |
|
557 \isadelimquote |
|
558 % |
|
559 \endisadelimquote |
|
560 % |
|
561 \isatagquote |
|
562 \isacommand{definition}\isamarkupfalse% |
|
563 \ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
564 \ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
565 \isanewline |
|
566 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% |
|
567 \ AQueue% |
|
568 \endisatagquote |
|
569 {\isafoldquote}% |
|
570 % |
|
571 \isadelimquote |
|
572 % |
|
573 \endisadelimquote |
|
574 % |
|
575 \begin{isamarkuptext}% |
|
576 \noindent Here we define a \qt{constructor} \isa{Program{\isachardot}AQueue} which |
|
577 is defined in terms of \isa{Queue} and interprets its arguments |
|
578 according to what the \emph{content} of an amortised queue is supposed |
|
579 to be. Equipped with this, we are able to prove the following equations |
|
580 for our primitive queue operations which \qt{implement} the simple |
|
581 queues in an amortised fashion:% |
|
582 \end{isamarkuptext}% |
|
583 \isamarkuptrue% |
|
584 % |
|
585 \isadelimquote |
|
586 % |
|
587 \endisadelimquote |
|
588 % |
|
589 \isatagquote |
|
590 \isacommand{lemma}\isamarkupfalse% |
|
591 \ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
592 \ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
593 \ \ \isacommand{unfolding}\isamarkupfalse% |
|
594 \ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
595 \ simp\isanewline |
|
596 \isanewline |
|
597 \isacommand{lemma}\isamarkupfalse% |
|
598 \ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
599 \ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline |
|
600 \ \ \isacommand{unfolding}\isamarkupfalse% |
|
601 \ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
602 \ simp\isanewline |
|
603 \isanewline |
|
604 \isacommand{lemma}\isamarkupfalse% |
|
605 \ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
606 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
607 \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline |
|
608 \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
609 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
610 \ \ \isacommand{unfolding}\isamarkupfalse% |
|
611 \ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
612 \ simp{\isacharunderscore}all% |
|
613 \endisatagquote |
|
614 {\isafoldquote}% |
|
615 % |
|
616 \isadelimquote |
|
617 % |
|
618 \endisadelimquote |
|
619 % |
|
620 \begin{isamarkuptext}% |
|
621 \noindent For completeness, we provide a substitute for the |
|
622 \isa{case} combinator on queues:% |
|
623 \end{isamarkuptext}% |
|
624 \isamarkuptrue% |
|
625 % |
|
626 \isadelimquote |
|
627 % |
|
628 \endisadelimquote |
|
629 % |
|
630 \isatagquote |
|
631 \isacommand{definition}\isamarkupfalse% |
|
632 \isanewline |
|
633 \ \ aqueue{\isacharunderscore}case{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ {\isacharequal}\ queue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline |
|
634 \isanewline |
|
635 \isacommand{lemma}\isamarkupfalse% |
|
636 \ aqueue{\isacharunderscore}case\ {\isacharbrackleft}code{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\isanewline |
|
637 \ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ {\isacharequal}\ aqueue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline |
|
638 \ \ \isacommand{unfolding}\isamarkupfalse% |
|
639 \ aqueue{\isacharunderscore}case{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
640 \isanewline |
|
641 \isanewline |
|
642 \isacommand{lemma}\isamarkupfalse% |
|
643 \ case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
644 \ \ {\isachardoublequoteopen}aqueue{\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}case{\isacharunderscore}def\ 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 = \\ |
|
670 \hspace*{0pt}struct\\ |
|
671 \hspace*{0pt}\\ |
|
672 \hspace*{0pt}fun foldl f a [] = a\\ |
|
673 \hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ |
|
674 \hspace*{0pt}\\ |
|
675 \hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ |
|
676 \hspace*{0pt}\\ |
|
677 \hspace*{0pt}fun null [] = true\\ |
|
678 \hspace*{0pt} ~| null (x ::~xs) = false;\\ |
|
679 \hspace*{0pt}\\ |
|
680 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ |
|
681 \hspace*{0pt}\\ |
|
682 \hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\ |
|
683 \hspace*{0pt}\\ |
|
684 \hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ |
|
685 \hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\ |
|
686 \hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\ |
|
687 \hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\ |
|
688 \hspace*{0pt}\\ |
|
689 \hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ |
|
690 \hspace*{0pt}\\ |
|
691 \hspace*{0pt}end;~(*struct Example*)% |
|
692 \end{isamarkuptext}% |
|
693 \isamarkuptrue% |
|
694 % |
|
695 \endisatagquote |
|
696 {\isafoldquote}% |
|
697 % |
|
698 \isadelimquote |
|
699 % |
|
700 \endisadelimquote |
|
701 % |
|
702 \begin{isamarkuptext}% |
|
703 \noindent From this example, it can be glimpsed that using own |
|
704 constructor sets is a little delicate since it changes the set of |
|
705 valid patterns for values of that type. Without going into much |
|
706 detail, here some practical hints: |
|
707 |
|
708 \begin{itemize} |
|
709 |
|
710 \item When changing the constructor set for datatypes, take care |
|
711 to provide an alternative for the \isa{case} combinator |
|
712 (e.g.~by replacing it using the preprocessor). |
|
713 |
|
714 \item Values in the target language need not to be normalised -- |
|
715 different values in the target language may represent the same |
|
716 value in the logic. |
|
717 |
|
718 \item Usually, a good methodology to deal with the subtleties of |
|
719 pattern matching is to see the type as an abstract type: provide |
|
720 a set of operations which operate on the concrete representation |
|
721 of the type, and derive further operations by combinations of |
|
722 these primitive ones, without relying on a particular |
|
723 representation. |
|
724 |
|
725 \end{itemize}% |
|
726 \end{isamarkuptext}% |
|
727 \isamarkuptrue% |
|
728 % |
|
729 \isamarkupsubsection{Equality and wellsortedness% |
|
730 } |
|
731 \isamarkuptrue% |
|
732 % |
|
733 \begin{isamarkuptext}% |
|
734 Surely you have already noticed how equality is treated |
|
735 by the code generator:% |
|
736 \end{isamarkuptext}% |
|
737 \isamarkuptrue% |
|
738 % |
|
739 \isadelimquote |
|
740 % |
|
741 \endisadelimquote |
|
742 % |
|
743 \isatagquote |
|
744 \isacommand{primrec}\isamarkupfalse% |
|
745 \ 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 |
|
746 \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline |
|
747 \ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline |
|
748 \ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline |
|
749 \ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline |
|
750 \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline |
|
751 \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% |
|
752 \endisatagquote |
|
753 {\isafoldquote}% |
|
754 % |
|
755 \isadelimquote |
|
756 % |
|
757 \endisadelimquote |
|
758 % |
|
759 \begin{isamarkuptext}% |
|
760 \noindent The membership test during preprocessing is rewritten, |
|
761 resulting in \isa{op\ mem}, which itself |
|
762 performs an explicit equality check.% |
|
763 \end{isamarkuptext}% |
|
764 \isamarkuptrue% |
|
765 % |
|
766 \isadelimquote |
|
767 % |
|
768 \endisadelimquote |
|
769 % |
|
770 \isatagquote |
|
771 % |
|
772 \begin{isamarkuptext}% |
|
773 \isatypewriter% |
|
774 \noindent% |
|
775 \hspace*{0pt}structure Example = \\ |
|
776 \hspace*{0pt}struct\\ |
|
777 \hspace*{0pt}\\ |
|
778 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
|
779 \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\ |
|
780 \hspace*{0pt}\\ |
|
781 \hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\ |
|
782 \hspace*{0pt}\\ |
|
783 \hspace*{0pt}fun member A{\char95}~x [] = false\\ |
|
784 \hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqop A{\char95}~x y orelse member A{\char95}~x ys;\\ |
|
785 \hspace*{0pt}\\ |
|
786 \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ |
|
787 \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ |
|
788 \hspace*{0pt} ~~~(if member A{\char95}~z xs\\ |
|
789 \hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\ |
|
790 \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ |
|
791 \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ |
|
792 \hspace*{0pt}\\ |
|
793 \hspace*{0pt}end;~(*struct Example*)% |
|
794 \end{isamarkuptext}% |
|
795 \isamarkuptrue% |
|
796 % |
|
797 \endisatagquote |
|
798 {\isafoldquote}% |
|
799 % |
|
800 \isadelimquote |
|
801 % |
|
802 \endisadelimquote |
|
803 % |
|
804 \begin{isamarkuptext}% |
|
805 \noindent Obviously, polymorphic equality is implemented the Haskell |
|
806 way using a type class. How is this achieved? HOL introduces |
|
807 an explicit class \isa{eq} with a corresponding operation |
|
808 \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. |
|
809 The preprocessing framework does the rest by propagating the |
|
810 \isa{eq} constraints through all dependent code equations. |
|
811 For datatypes, instances of \isa{eq} are implicitly derived |
|
812 when possible. For other types, you may instantiate \isa{eq} |
|
813 manually like any other type class. |
|
814 |
|
815 Though this \isa{eq} class is designed to get rarely in |
|
816 the way, a subtlety |
|
817 enters the stage when definitions of overloaded constants |
|
818 are dependent on operational equality. For example, let |
|
819 us define a lexicographic ordering on tuples |
|
820 (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):% |
|
821 \end{isamarkuptext}% |
|
822 \isamarkuptrue% |
|
823 % |
|
824 \isadelimquote |
|
825 % |
|
826 \endisadelimquote |
|
827 % |
|
828 \isatagquote |
|
829 \isacommand{instantiation}\isamarkupfalse% |
|
830 \ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline |
|
831 \isakeyword{begin}\isanewline |
|
832 \isanewline |
|
833 \isacommand{definition}\isamarkupfalse% |
|
834 \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline |
|
835 \ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline |
|
836 \isanewline |
|
837 \isacommand{definition}\isamarkupfalse% |
|
838 \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline |
|
839 \ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline |
|
840 \isanewline |
|
841 \isacommand{instance}\isamarkupfalse% |
|
842 \ \isacommand{proof}\isamarkupfalse% |
|
843 \isanewline |
|
844 \isacommand{qed}\isamarkupfalse% |
|
845 \ {\isacharparenleft}auto\ simp{\isacharcolon}\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}prod{\isacharunderscore}def\ intro{\isacharcolon}\ order{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isanewline |
|
846 \isanewline |
|
847 \isacommand{end}\isamarkupfalse% |
|
848 \isanewline |
|
849 \isanewline |
|
850 \isacommand{lemma}\isamarkupfalse% |
|
851 \ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
852 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline |
|
853 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline |
|
854 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline |
|
855 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline |
|
856 \ \ \isacommand{by}\isamarkupfalse% |
|
857 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}% |
|
858 \endisatagquote |
|
859 {\isafoldquote}% |
|
860 % |
|
861 \isadelimquote |
|
862 % |
|
863 \endisadelimquote |
|
864 % |
|
865 \begin{isamarkuptext}% |
|
866 \noindent Then code generation will fail. Why? The definition |
|
867 of \isa{op\ {\isasymle}} depends on equality on both arguments, |
|
868 which are polymorphic and impose an additional \isa{eq} |
|
869 class constraint, which the preprocessor does not propagate |
|
870 (for technical reasons). |
|
871 |
|
872 The solution is to add \isa{eq} explicitly to the first sort arguments in the |
|
873 code theorems:% |
|
874 \end{isamarkuptext}% |
|
875 \isamarkuptrue% |
|
876 % |
|
877 \isadelimquote |
|
878 % |
|
879 \endisadelimquote |
|
880 % |
|
881 \isatagquote |
|
882 \isacommand{lemma}\isamarkupfalse% |
|
883 \ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
884 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline |
|
885 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline |
|
886 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline |
|
887 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline |
|
888 \ \ \isacommand{by}\isamarkupfalse% |
|
889 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}% |
|
890 \endisatagquote |
|
891 {\isafoldquote}% |
|
892 % |
|
893 \isadelimquote |
|
894 % |
|
895 \endisadelimquote |
|
896 % |
|
897 \begin{isamarkuptext}% |
|
898 \noindent Then code generation succeeds:% |
|
899 \end{isamarkuptext}% |
|
900 \isamarkuptrue% |
|
901 % |
|
902 \isadelimquote |
|
903 % |
|
904 \endisadelimquote |
|
905 % |
|
906 \isatagquote |
|
907 % |
|
908 \begin{isamarkuptext}% |
|
909 \isatypewriter% |
|
910 \noindent% |
|
911 \hspace*{0pt}structure Example = \\ |
|
912 \hspace*{0pt}struct\\ |
|
913 \hspace*{0pt}\\ |
|
914 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ |
|
915 \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\ |
|
916 \hspace*{0pt}\\ |
|
917 \hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool,~less :~'a -> 'a -> bool{\char125};\\ |
|
918 \hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\ |
|
919 \hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\ |
|
920 \hspace*{0pt}\\ |
|
921 \hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\ |
|
922 \hspace*{0pt}\\ |
|
923 \hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\ |
|
924 \hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\ |
|
925 \hspace*{0pt}\\ |
|
926 \hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\ |
|
927 \hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\ |
|
928 \hspace*{0pt}\\ |
|
929 \hspace*{0pt}fun less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\ |
|
930 \hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\ |
|
931 \hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\ |
|
932 \hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\ |
|
933 \hspace*{0pt} ~| less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\ |
|
934 \hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\ |
|
935 \hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\ |
|
936 \hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\ |
|
937 \hspace*{0pt}\\ |
|
938 \hspace*{0pt}end;~(*struct Example*)% |
|
939 \end{isamarkuptext}% |
|
940 \isamarkuptrue% |
|
941 % |
|
942 \endisatagquote |
|
943 {\isafoldquote}% |
|
944 % |
|
945 \isadelimquote |
|
946 % |
|
947 \endisadelimquote |
|
948 % |
|
949 \begin{isamarkuptext}% |
|
950 In some cases, the automatically derived code equations |
|
951 for equality on a particular type may not be appropriate. |
|
952 As example, watch the following datatype representing |
|
953 monomorphic parametric types (where type constructors |
|
954 are referred to by natural numbers):% |
|
955 \end{isamarkuptext}% |
|
956 \isamarkuptrue% |
|
957 % |
|
958 \isadelimquote |
|
959 % |
|
960 \endisadelimquote |
|
961 % |
|
962 \isatagquote |
|
963 \isacommand{datatype}\isamarkupfalse% |
|
964 \ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}% |
|
965 \endisatagquote |
|
966 {\isafoldquote}% |
|
967 % |
|
968 \isadelimquote |
|
969 % |
|
970 \endisadelimquote |
|
971 % |
|
972 \isadelimproof |
|
973 % |
|
974 \endisadelimproof |
|
975 % |
|
976 \isatagproof |
|
977 % |
|
978 \endisatagproof |
|
979 {\isafoldproof}% |
|
980 % |
|
981 \isadelimproof |
|
982 % |
|
983 \endisadelimproof |
|
984 % |
|
985 \begin{isamarkuptext}% |
|
986 \noindent Then code generation for SML would fail with a message |
|
987 that the generated code contains illegal mutual dependencies: |
|
988 the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the |
|
989 instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires |
|
990 \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually |
|
991 recursive \isa{instance} and \isa{function} definitions, |
|
992 but the SML serialiser does not support this. |
|
993 |
|
994 In such cases, you have to provide your own equality equations |
|
995 involving auxiliary constants. In our case, |
|
996 \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:% |
|
997 \end{isamarkuptext}% |
|
998 \isamarkuptrue% |
|
999 % |
|
1000 \isadelimquote |
|
1001 % |
|
1002 \endisadelimquote |
|
1003 % |
|
1004 \isatagquote |
|
1005 \isacommand{lemma}\isamarkupfalse% |
|
1006 \ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
1007 \ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline |
|
1008 \ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline |
|
1009 \ \ \isacommand{by}\isamarkupfalse% |
|
1010 \ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}% |
|
1011 \endisatagquote |
|
1012 {\isafoldquote}% |
|
1013 % |
|
1014 \isadelimquote |
|
1015 % |
|
1016 \endisadelimquote |
|
1017 % |
|
1018 \begin{isamarkuptext}% |
|
1019 \noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:% |
|
1020 \end{isamarkuptext}% |
|
1021 \isamarkuptrue% |
|
1022 % |
|
1023 \isadelimquote |
|
1024 % |
|
1025 \endisadelimquote |
|
1026 % |
|
1027 \isatagquote |
|
1028 % |
|
1029 \begin{isamarkuptext}% |
|
1030 \isatypewriter% |
|
1031 \noindent% |
|
1032 \hspace*{0pt}structure Example = \\ |
|
1033 \hspace*{0pt}struct\\ |
|
1034 \hspace*{0pt}\\ |
|
1035 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
|
1036 \hspace*{0pt}\\ |
|
1037 \hspace*{0pt}fun null [] = true\\ |
|
1038 \hspace*{0pt} ~| null (x ::~xs) = false;\\ |
|
1039 \hspace*{0pt}\\ |
|
1040 \hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\ |
|
1041 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\ |
|
1042 \hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\ |
|
1043 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\ |
|
1044 \hspace*{0pt}\\ |
|
1045 \hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\ |
|
1046 \hspace*{0pt}\\ |
|
1047 \hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\ |
|
1048 \hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\ |
|
1049 \hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\ |
|
1050 \hspace*{0pt}\\ |
|
1051 \hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\ |
|
1052 \hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\ |
|
1053 \hspace*{0pt}\\ |
|
1054 \hspace*{0pt}end;~(*struct Example*)% |
|
1055 \end{isamarkuptext}% |
|
1056 \isamarkuptrue% |
|
1057 % |
|
1058 \endisatagquote |
|
1059 {\isafoldquote}% |
|
1060 % |
|
1061 \isadelimquote |
|
1062 % |
|
1063 \endisadelimquote |
|
1064 % |
|
1065 \isamarkupsubsection{Explicit partiality% |
|
1066 } |
|
1067 \isamarkuptrue% |
|
1068 % |
|
1069 \begin{isamarkuptext}% |
|
1070 Partiality usually enters the game by partial patterns, as |
|
1071 in the following example, again for amortised queues:% |
|
1072 \end{isamarkuptext}% |
|
1073 \isamarkuptrue% |
|
1074 % |
|
1075 \isadelimquote |
|
1076 % |
|
1077 \endisadelimquote |
|
1078 % |
|
1079 \isatagquote |
|
1080 \isacommand{definition}\isamarkupfalse% |
|
1081 \ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
1082 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline |
|
1083 \ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
1084 \isanewline |
|
1085 \isacommand{lemma}\isamarkupfalse% |
|
1086 \ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
1087 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
1088 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
1089 \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
1090 \ \ \isacommand{by}\isamarkupfalse% |
|
1091 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% |
|
1092 \endisatagquote |
|
1093 {\isafoldquote}% |
|
1094 % |
|
1095 \isadelimquote |
|
1096 % |
|
1097 \endisadelimquote |
|
1098 % |
|
1099 \begin{isamarkuptext}% |
|
1100 \noindent In the corresponding code, there is no equation |
|
1101 for the pattern \isa{Program{\isachardot}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:% |
|
1102 \end{isamarkuptext}% |
|
1103 \isamarkuptrue% |
|
1104 % |
|
1105 \isadelimquote |
|
1106 % |
|
1107 \endisadelimquote |
|
1108 % |
|
1109 \isatagquote |
|
1110 % |
|
1111 \begin{isamarkuptext}% |
|
1112 \isatypewriter% |
|
1113 \noindent% |
|
1114 \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ |
|
1115 \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ |
|
1116 \hspace*{0pt} ~let {\char123}\\ |
|
1117 \hspace*{0pt} ~~~(y :~ys) = rev xs;\\ |
|
1118 \hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ |
|
1119 \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% |
|
1120 \end{isamarkuptext}% |
|
1121 \isamarkuptrue% |
|
1122 % |
|
1123 \endisatagquote |
|
1124 {\isafoldquote}% |
|
1125 % |
|
1126 \isadelimquote |
|
1127 % |
|
1128 \endisadelimquote |
|
1129 % |
|
1130 \begin{isamarkuptext}% |
|
1131 \noindent In some cases it is desirable to have this |
|
1132 pseudo-\qt{partiality} more explicitly, e.g.~as follows:% |
|
1133 \end{isamarkuptext}% |
|
1134 \isamarkuptrue% |
|
1135 % |
|
1136 \isadelimquote |
|
1137 % |
|
1138 \endisadelimquote |
|
1139 % |
|
1140 \isatagquote |
|
1141 \isacommand{axiomatization}\isamarkupfalse% |
|
1142 \ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline |
|
1143 \isanewline |
|
1144 \isacommand{definition}\isamarkupfalse% |
|
1145 \ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
1146 \ \ {\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 |
|
1147 \isanewline |
|
1148 \isacommand{lemma}\isamarkupfalse% |
|
1149 \ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
1150 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline |
|
1151 \ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
1152 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
1153 \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
1154 \ \ \isacommand{by}\isamarkupfalse% |
|
1155 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% |
|
1156 \endisatagquote |
|
1157 {\isafoldquote}% |
|
1158 % |
|
1159 \isadelimquote |
|
1160 % |
|
1161 \endisadelimquote |
|
1162 % |
|
1163 \begin{isamarkuptext}% |
|
1164 Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs |
|
1165 which is unspecified. |
|
1166 |
|
1167 Normally, if constants without any code equations occur in a |
|
1168 program, the code generator complains (since in most cases this is |
|
1169 not what the user expects). But such constants can also be thought |
|
1170 of as function definitions with no equations which always fail, |
|
1171 since there is never a successful pattern match on the left hand |
|
1172 side. In order to categorise a constant into that category |
|
1173 explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:% |
|
1174 \end{isamarkuptext}% |
|
1175 \isamarkuptrue% |
|
1176 % |
|
1177 \isadelimquote |
|
1178 % |
|
1179 \endisadelimquote |
|
1180 % |
|
1181 \isatagquote |
|
1182 \isacommand{code{\isacharunderscore}abort}\isamarkupfalse% |
|
1183 \ empty{\isacharunderscore}queue% |
|
1184 \endisatagquote |
|
1185 {\isafoldquote}% |
|
1186 % |
|
1187 \isadelimquote |
|
1188 % |
|
1189 \endisadelimquote |
|
1190 % |
|
1191 \begin{isamarkuptext}% |
|
1192 \noindent Then the code generator will just insert an error or |
|
1193 exception at the appropriate position:% |
|
1194 \end{isamarkuptext}% |
|
1195 \isamarkuptrue% |
|
1196 % |
|
1197 \isadelimquote |
|
1198 % |
|
1199 \endisadelimquote |
|
1200 % |
|
1201 \isatagquote |
|
1202 % |
|
1203 \begin{isamarkuptext}% |
|
1204 \isatypewriter% |
|
1205 \noindent% |
|
1206 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ |
|
1207 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ |
|
1208 \hspace*{0pt}\\ |
|
1209 \hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\ |
|
1210 \hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ |
|
1211 \hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\ |
|
1212 \hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\ |
|
1213 \hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));% |
|
1214 \end{isamarkuptext}% |
|
1215 \isamarkuptrue% |
|
1216 % |
|
1217 \endisatagquote |
|
1218 {\isafoldquote}% |
|
1219 % |
|
1220 \isadelimquote |
|
1221 % |
|
1222 \endisadelimquote |
|
1223 % |
|
1224 \begin{isamarkuptext}% |
|
1225 \noindent This feature however is rarely needed in practice. |
|
1226 Note also that the \isa{HOL} default setup already declares |
|
1227 \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most |
|
1228 likely to be used in such situations.% |
|
1229 \end{isamarkuptext}% |
|
1230 \isamarkuptrue% |
|
1231 % |
|
1232 \isadelimtheory |
|
1233 % |
|
1234 \endisadelimtheory |
|
1235 % |
|
1236 \isatagtheory |
|
1237 \isacommand{end}\isamarkupfalse% |
|
1238 % |
|
1239 \endisatagtheory |
|
1240 {\isafoldtheory}% |
|
1241 % |
|
1242 \isadelimtheory |
|
1243 % |
|
1244 \endisadelimtheory |
|
1245 \isanewline |
|
1246 \ \end{isabellebody}% |
|
1247 %%% Local Variables: |
|
1248 %%% mode: latex |
|
1249 %%% TeX-master: "root" |
|
1250 %%% End: |
|