author | haftmann |
Fri, 30 Mar 2007 16:18:59 +0200 | |
changeset 22550 | c5039bee2602 |
parent 22479 | de15ea8fb348 |
child 22751 | 1bfd75c1f232 |
permissions | -rw-r--r-- |
20948 | 1 |
(* $Id$ *) |
2 |
||
21147 | 3 |
(*<*) |
20948 | 4 |
theory Codegen |
5 |
imports Main |
|
21452 | 6 |
uses "../../../antiquote_setup.ML" |
20948 | 7 |
begin |
8 |
||
21147 | 9 |
ML {* |
22015 | 10 |
CodegenSerializer.code_width := 74; |
21147 | 11 |
*} |
12 |
||
13 |
(*>*) |
|
14 |
||
20948 | 15 |
chapter {* Code generation from Isabelle theories *} |
16 |
||
17 |
section {* Introduction *} |
|
18 |
||
21058 | 19 |
subsection {* Motivation *} |
20 |
||
20948 | 21 |
text {* |
21058 | 22 |
Executing formal specifications as programs is a well-established |
23 |
topic in the theorem proving community. With increasing |
|
24 |
application of theorem proving systems in the area of |
|
25 |
software development and verification, its relevance manifests |
|
26 |
for running test cases and rapid prototyping. In logical |
|
27 |
calculi like constructive type theory, |
|
28 |
a notion of executability is implicit due to the nature |
|
22550 | 29 |
of the calculus. In contrast, specifications in Isabelle |
21058 | 30 |
can be highly non-executable. In order to bridge |
31 |
the gap between logic and executable specifications, |
|
32 |
an explicit non-trivial transformation has to be applied: |
|
33 |
code generation. |
|
34 |
||
35 |
This tutorial introduces a generic code generator for the |
|
36 |
Isabelle system \cite{isa-tutorial}. |
|
37 |
Generic in the sense that the |
|
38 |
\qn{target language} for which code shall ultimately be |
|
39 |
generated is not fixed but may be an arbitrary state-of-the-art |
|
40 |
functional programming language (currently, the implementation |
|
22550 | 41 |
supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell |
42 |
\cite{haskell-revised-report}). |
|
21058 | 43 |
We aim to provide a |
44 |
versatile environment |
|
45 |
suitable for software development and verification, |
|
46 |
structuring the process |
|
47 |
of code generation into a small set of orthogonal principles |
|
48 |
while achieving a big coverage of application areas |
|
49 |
with maximum flexibility. |
|
21189 | 50 |
|
22550 | 51 |
Conceptually the code generator framework is part |
52 |
of Isabelle's @{text Pure} meta logic; the object logic |
|
53 |
@{text HOL} which is an extension of @{text Pure} |
|
54 |
already comes with a reasonable framework setup and thus provides |
|
55 |
a good working horse for raising code-generation-driven |
|
56 |
applications. So, we assume some familiarity and experience |
|
57 |
with the ingredients of the @{text HOL} \emph{Main} theory |
|
58 |
(see also \cite{isa-tutorial}). |
|
21058 | 59 |
*} |
60 |
||
61 |
||
62 |
subsection {* Overview *} |
|
63 |
||
64 |
text {* |
|
65 |
The code generator aims to be usable with no further ado |
|
66 |
in most cases while allowing for detailed customization. |
|
22550 | 67 |
This manifests in the structure of this tutorial: |
68 |
we start with a generic example \secref{sec:example} |
|
69 |
and introduce code generation concepts \secref{sec:concept}. |
|
70 |
Section |
|
21178 | 71 |
\secref{sec:basics} explains how to use the framework naively, |
21058 | 72 |
presuming a reasonable default setup. Then, section |
73 |
\secref{sec:advanced} deals with advanced topics, |
|
74 |
introducing further aspects of the code generator framework |
|
75 |
in a motivation-driven manner. Last, section \secref{sec:ml} |
|
76 |
introduces the framework's internal programming interfaces. |
|
20948 | 77 |
|
21058 | 78 |
\begin{warn} |
79 |
Ultimately, the code generator which this tutorial deals with |
|
80 |
is supposed to replace the already established code generator |
|
81 |
by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. |
|
21147 | 82 |
So, for the moment, there are two distinct code generators |
21058 | 83 |
in Isabelle. |
84 |
Also note that while the framework itself is largely |
|
22550 | 85 |
object-logic independent, only @{text HOL} provides a reasonable |
21058 | 86 |
framework setup. |
87 |
\end{warn} |
|
88 |
*} |
|
89 |
||
90 |
||
22550 | 91 |
section {* An example: a simple theory of search trees \label{sec:example} *} |
92 |
||
93 |
text {* |
|
94 |
When writing executable specifications, it is convenient to use |
|
95 |
three existing packages: the datatype package for defining |
|
96 |
datatypes, the function package for (recursive) functions, |
|
97 |
and the class package for overloaded definitions. |
|
98 |
||
99 |
We develope a small theory of search trees; trees are represented |
|
100 |
as a datatype with key type @{typ "'a"} and value type @{typ "'b"}: |
|
101 |
*} |
|
22479 | 102 |
|
103 |
datatype ('a, 'b) searchtree = Leaf "'a\<Colon>linorder" 'b |
|
104 |
| Branch "('a, 'b) searchtree" "'a" "('a, 'b) searchtree" |
|
105 |
||
22550 | 106 |
text {* |
107 |
\noindent Note that we have constrained the type of keys |
|
108 |
to the class of total orders, @{text linorder}. |
|
109 |
||
110 |
We define @{text find} and @{text update} functions: |
|
111 |
*} |
|
112 |
||
22479 | 113 |
fun |
114 |
find :: "('a\<Colon>linorder, 'b) searchtree \<Rightarrow> 'a \<Rightarrow> 'b option" where |
|
115 |
"find (Leaf key val) it = (if it = key then Some val else None)" |
|
116 |
| "find (Branch t1 key t2) it = (if it \<le> key then find t1 it else find t2 it)" |
|
117 |
||
118 |
fun |
|
119 |
update :: "'a\<Colon>linorder \<times> 'b \<Rightarrow> ('a, 'b) searchtree \<Rightarrow> ('a, 'b) searchtree" where |
|
120 |
"update (it, entry) (Leaf key val) = ( |
|
121 |
if it = key then Leaf key entry |
|
122 |
else if it \<le> key |
|
123 |
then Branch (Leaf it entry) it (Leaf key val) |
|
124 |
else Branch (Leaf key val) it (Leaf it entry) |
|
125 |
)" |
|
126 |
| "update (it, entry) (Branch t1 key t2) = ( |
|
127 |
if it \<le> key |
|
128 |
then (Branch (update (it, entry) t1) key t2) |
|
129 |
else (Branch t1 key (update (it, entry) t2)) |
|
130 |
)" |
|
131 |
||
22550 | 132 |
text {* |
133 |
\noindent For testing purpose, we define a small example |
|
134 |
using natural numbers @{typ nat} (which are a @{text linorder}) |
|
135 |
as keys and strings values: |
|
136 |
*} |
|
137 |
||
22479 | 138 |
fun |
139 |
example :: "nat \<Rightarrow> (nat, string) searchtree" where |
|
140 |
"example n = update (n, ''bar'') (Leaf 0 ''foo'')" |
|
141 |
||
22550 | 142 |
text {* |
143 |
\noindent Then we generate code |
|
144 |
*} |
|
145 |
||
22479 | 146 |
code_gen example (*<*)(SML #)(*>*)(SML "examples/tree.ML") |
147 |
||
148 |
text {* |
|
22550 | 149 |
\noindent which looks like: |
22479 | 150 |
\lstsml{Thy/examples/tree.ML} |
151 |
*} |
|
152 |
||
22550 | 153 |
|
154 |
section {* Code generation concepts and process \label{sec:concept} *} |
|
21058 | 155 |
|
156 |
text {* |
|
21189 | 157 |
\begin{figure}[h] |
158 |
\centering |
|
159 |
\includegraphics[width=0.7\textwidth]{codegen_process} |
|
160 |
\caption{code generator -- processing overview} |
|
161 |
\label{fig:process} |
|
162 |
\end{figure} |
|
163 |
||
21058 | 164 |
The code generator employs a notion of executability |
165 |
for three foundational executable ingredients known |
|
166 |
from functional programming: |
|
22060 | 167 |
\emph{defining equations}, \emph{datatypes}, and |
168 |
\emph{type classes}. A defining equation as a first approximation |
|
21058 | 169 |
is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"} |
170 |
(an equation headed by a constant @{text f} with arguments |
|
171 |
@{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}. |
|
22060 | 172 |
Code generation aims to turn defining equations |
21058 | 173 |
into a functional program by running through |
174 |
a process (see figure \ref{fig:process}): |
|
175 |
||
176 |
\begin{itemize} |
|
177 |
||
178 |
\item Out of the vast collection of theorems proven in a |
|
179 |
\qn{theory}, a reasonable subset modeling |
|
22060 | 180 |
defining equations is \qn{selected}. |
21058 | 181 |
|
182 |
\item On those selected theorems, certain |
|
183 |
transformations are carried out |
|
184 |
(\qn{preprocessing}). Their purpose is to turn theorems |
|
185 |
representing non- or badly executable |
|
186 |
specifications into equivalent but executable counterparts. |
|
187 |
The result is a structured collection of \qn{code theorems}. |
|
188 |
||
22479 | 189 |
\item These \qn{code theorems} then are \qn{translated} |
21058 | 190 |
into an Haskell-like intermediate |
191 |
language. |
|
192 |
||
193 |
\item Finally, out of the intermediate language the final |
|
194 |
code in the desired \qn{target language} is \qn{serialized}. |
|
195 |
||
196 |
\end{itemize} |
|
197 |
||
198 |
From these steps, only the two last are carried out |
|
199 |
outside the logic; by keeping this layer as |
|
200 |
thin as possible, the amount of code to trust is |
|
201 |
kept to a minimum. |
|
202 |
*} |
|
203 |
||
204 |
||
205 |
||
206 |
section {* Basics \label{sec:basics} *} |
|
20948 | 207 |
|
208 |
subsection {* Invoking the code generator *} |
|
209 |
||
21058 | 210 |
text {* |
211 |
Thanks to a reasonable setup of the HOL theories, in |
|
212 |
most cases code generation proceeds without further ado: |
|
213 |
*} |
|
214 |
||
22473 | 215 |
fun |
216 |
fac :: "nat \<Rightarrow> nat" where |
|
217 |
"fac 0 = 1" |
|
218 |
| "fac (Suc n) = Suc n * fac n" |
|
21058 | 219 |
|
220 |
text {* |
|
22550 | 221 |
\noindent This executable specification is now turned to SML code: |
21058 | 222 |
*} |
223 |
||
21545 | 224 |
code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML") |
21058 | 225 |
|
226 |
text {* |
|
22550 | 227 |
\noindent The @{text "\<CODEGEN>"} command takes a space-separated list of |
21058 | 228 |
constants together with \qn{serialization directives} |
229 |
in parentheses. These start with a \qn{target language} |
|
21178 | 230 |
identifier, followed by arguments, their semantics |
21058 | 231 |
depending on the target. In the SML case, a filename |
232 |
is given where to write the generated code to. |
|
233 |
||
22060 | 234 |
Internally, the defining equations for all selected |
21178 | 235 |
constants are taken, including any transitively required |
21058 | 236 |
constants, datatypes and classes, resulting in the following |
237 |
code: |
|
238 |
||
239 |
\lstsml{Thy/examples/fac.ML} |
|
240 |
||
241 |
The code generator will complain when a required |
|
22550 | 242 |
ingredient does not provide a executable counterpart, |
243 |
e.g.~generating code |
|
21058 | 244 |
for constants not yielding |
22550 | 245 |
a defining equation (e.g.~the Hilbert choice |
246 |
operation @{text "SOME"}): |
|
21058 | 247 |
*} |
248 |
||
249 |
(*<*) |
|
250 |
setup {* Sign.add_path "foo" *} |
|
251 |
(*>*) |
|
252 |
||
253 |
definition |
|
21993 | 254 |
pick_some :: "'a list \<Rightarrow> 'a" where |
21058 | 255 |
"pick_some xs = (SOME x. x \<in> set xs)" |
256 |
||
257 |
(*<*) |
|
258 |
hide const pick_some |
|
259 |
||
260 |
setup {* Sign.parent_path *} |
|
261 |
||
262 |
definition |
|
21993 | 263 |
pick_some :: "'a list \<Rightarrow> 'a" where |
21058 | 264 |
"pick_some = hd" |
265 |
(*>*) |
|
266 |
||
267 |
code_gen pick_some (SML "examples/fail_const.ML") |
|
268 |
||
22550 | 269 |
text {* \noindent will fail. *} |
270 |
||
20948 | 271 |
subsection {* Theorem selection *} |
272 |
||
21058 | 273 |
text {* |
22060 | 274 |
The list of all defining equations in a theory may be inspected |
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
275 |
using the @{text "\<PRINTCODESETUP>"} command: |
21058 | 276 |
*} |
277 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
278 |
print_codesetup |
21058 | 279 |
|
280 |
text {* |
|
281 |
\noindent which displays a table of constant with corresponding |
|
22060 | 282 |
defining equations (the additional stuff displayed |
21058 | 283 |
shall not bother us for the moment). If this table does |
22550 | 284 |
not provide at least one defining |
285 |
equation for a particular constant, the table of primitive |
|
286 |
definitions is searched |
|
21058 | 287 |
whether it provides one. |
288 |
||
289 |
The typical HOL tools are already set up in a way that |
|
21323 | 290 |
function definitions introduced by @{text "\<FUN>"}, |
291 |
@{text "\<FUNCTION>"}, @{text "\<PRIMREC>"} |
|
292 |
@{text "\<RECDEF>"} are implicitly propagated |
|
22060 | 293 |
to this defining equation table. Specific theorems may be |
21058 | 294 |
selected using an attribute: \emph{code func}. As example, |
295 |
a weight selector function: |
|
296 |
*} |
|
297 |
||
298 |
consts |
|
299 |
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a" |
|
300 |
||
301 |
primrec |
|
302 |
"pick (x#xs) n = (let (k, v) = x in |
|
303 |
if n < k then v else pick xs (n - k))" |
|
304 |
||
305 |
text {* |
|
306 |
We want to eliminate the explicit destruction |
|
307 |
of @{term x} to @{term "(k, v)"}: |
|
308 |
*} |
|
309 |
||
310 |
lemma [code func]: |
|
311 |
"pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" |
|
312 |
by simp |
|
313 |
||
21545 | 314 |
code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML") |
21058 | 315 |
|
316 |
text {* |
|
22060 | 317 |
This theorem is now added to the defining equation table: |
21058 | 318 |
|
319 |
\lstsml{Thy/examples/pick1.ML} |
|
320 |
||
321 |
It might be convenient to remove the pointless original |
|
322 |
equation, using the \emph{nofunc} attribute: |
|
323 |
*} |
|
324 |
||
325 |
lemmas [code nofunc] = pick.simps |
|
326 |
||
21545 | 327 |
code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick2.ML") |
21058 | 328 |
|
329 |
text {* |
|
330 |
\lstsml{Thy/examples/pick2.ML} |
|
331 |
||
332 |
Syntactic redundancies are implicitly dropped. For example, |
|
333 |
using a modified version of the @{const fac} function |
|
22060 | 334 |
as defining equation, the then redundant (since |
335 |
syntactically subsumed) original defining equations |
|
21058 | 336 |
are dropped, resulting in a warning: |
337 |
*} |
|
338 |
||
339 |
lemma [code func]: |
|
340 |
"fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)" |
|
341 |
by (cases n) simp_all |
|
342 |
||
21545 | 343 |
code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac_case.ML") |
21058 | 344 |
|
345 |
text {* |
|
346 |
\lstsml{Thy/examples/fac_case.ML} |
|
347 |
||
348 |
\begin{warn} |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
349 |
The attributes \emph{code} and \emph{code del} |
21058 | 350 |
associated with the existing code generator also apply to |
351 |
the new one: \emph{code} implies \emph{code func}, |
|
352 |
and \emph{code del} implies \emph{code nofunc}. |
|
353 |
\end{warn} |
|
354 |
*} |
|
20948 | 355 |
|
356 |
subsection {* Type classes *} |
|
357 |
||
21058 | 358 |
text {* |
359 |
Type classes enter the game via the Isar class package. |
|
21075 | 360 |
For a short introduction how to use it, see \cite{isabelle-classes}; |
21147 | 361 |
here we just illustrate its impact on code generation. |
21058 | 362 |
|
363 |
In a target language, type classes may be represented |
|
21178 | 364 |
natively (as in the case of Haskell). For languages |
21058 | 365 |
like SML, they are implemented using \emph{dictionaries}. |
21178 | 366 |
Our following example specifies a class \qt{null}, |
21058 | 367 |
assigning to each of its inhabitants a \qt{null} value: |
368 |
*} |
|
369 |
||
22473 | 370 |
class null = type + |
21058 | 371 |
fixes null :: 'a |
372 |
||
373 |
consts |
|
374 |
head :: "'a\<Colon>null list \<Rightarrow> 'a" |
|
375 |
||
376 |
primrec |
|
377 |
"head [] = null" |
|
378 |
"head (x#xs) = x" |
|
379 |
||
380 |
text {* |
|
381 |
We provide some instances for our @{text null}: |
|
382 |
*} |
|
383 |
||
384 |
instance option :: (type) null |
|
385 |
"null \<equiv> None" .. |
|
386 |
||
387 |
instance list :: (type) null |
|
388 |
"null \<equiv> []" .. |
|
389 |
||
390 |
text {* |
|
391 |
Constructing a dummy example: |
|
392 |
*} |
|
393 |
||
394 |
definition |
|
395 |
"dummy = head [Some (Suc 0), None]" |
|
396 |
||
397 |
text {* |
|
21178 | 398 |
Type classes offer a suitable occasion to introduce |
21058 | 399 |
the Haskell serializer. Its usage is almost the same |
21075 | 400 |
as SML, but, in accordance with conventions |
401 |
some Haskell systems enforce, each module ends |
|
402 |
up in a single file. The module hierarchy is reflected in |
|
403 |
the file system, with root given by the user. |
|
21058 | 404 |
*} |
405 |
||
21075 | 406 |
code_gen dummy (Haskell "examples/") |
21147 | 407 |
(* NOTE: you may use Haskell only once in this document, otherwise |
408 |
you have to work in distinct subdirectories *) |
|
21058 | 409 |
|
410 |
text {* |
|
411 |
\lsthaskell{Thy/examples/Codegen.hs} |
|
412 |
||
413 |
(we have left out all other modules). |
|
414 |
||
415 |
The whole code in SML with explicit dictionary passing: |
|
416 |
*} |
|
417 |
||
21545 | 418 |
code_gen dummy (*<*)(SML #)(*>*)(SML "examples/class.ML") |
21058 | 419 |
|
420 |
text {* |
|
421 |
\lstsml{Thy/examples/class.ML} |
|
422 |
*} |
|
423 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
424 |
text {* |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
425 |
or in OCaml: |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
426 |
*} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
427 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
428 |
code_gen dummy (OCaml "examples/class.ocaml") |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
429 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
430 |
text {* |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
431 |
\lstsml{Thy/examples/class.ocaml} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
432 |
*} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
433 |
|
21058 | 434 |
subsection {* Incremental code generation *} |
435 |
||
21075 | 436 |
text {* |
437 |
Code generation is \emph{incremental}: theorems |
|
438 |
and abstract intermediate code are cached and extended on demand. |
|
439 |
The cache may be partially or fully dropped if the underlying |
|
440 |
executable content of the theory changes. |
|
441 |
Implementation of caching is supposed to transparently |
|
442 |
hid away the details from the user. Anyway, caching |
|
443 |
reaches the surface by using a slightly more general form |
|
21323 | 444 |
of the @{text "\<CODEGEN>"}: either the list of constants or the |
21075 | 445 |
list of serialization expressions may be dropped. If no |
446 |
serialization expressions are given, only abstract code |
|
447 |
is generated and cached; if no constants are given, the |
|
448 |
current cache is serialized. |
|
449 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
450 |
For explorative purpose, the |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
451 |
@{text "\<CODETHMS>"} command may prove useful: |
21075 | 452 |
*} |
453 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
454 |
code_thms |
21075 | 455 |
|
456 |
text {* |
|
22060 | 457 |
\noindent print all cached defining equations (i.e.~\emph{after} |
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
458 |
any applied transformation). A |
21075 | 459 |
list of constants may be given; their function |
21178 | 460 |
equations are added to the cache if not already present. |
22550 | 461 |
|
462 |
Similarly, the @{text "\<CODEDEPS>"} command shows a graph |
|
463 |
visualizing dependencies between defining equations. |
|
21075 | 464 |
*} |
465 |
||
21058 | 466 |
|
22550 | 467 |
|
21058 | 468 |
section {* Recipes and advanced topics \label{sec:advanced} *} |
469 |
||
21089 | 470 |
text {* |
471 |
In this tutorial, we do not attempt to give an exhaustive |
|
472 |
description of the code generator framework; instead, |
|
473 |
we cast a light on advanced topics by introducing |
|
474 |
them together with practically motivated examples. Concerning |
|
475 |
further reading, see |
|
476 |
||
477 |
\begin{itemize} |
|
478 |
||
479 |
\item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} |
|
480 |
for exhaustive syntax diagrams. |
|
21222 | 481 |
\item or \fixme[ref] which deals with foundational issues |
21089 | 482 |
of the code generator framework. |
483 |
||
484 |
\end{itemize} |
|
485 |
*} |
|
21058 | 486 |
|
487 |
subsection {* Library theories *} |
|
488 |
||
21089 | 489 |
text {* |
490 |
The HOL \emph{Main} theory already provides a code generator setup |
|
491 |
which should be suitable for most applications. Common extensions |
|
492 |
and modifications are available by certain theories of the HOL |
|
493 |
library; beside being useful in applications, they may serve |
|
21178 | 494 |
as a tutorial for customizing the code generator setup. |
21089 | 495 |
|
496 |
\begin{description} |
|
497 |
||
21452 | 498 |
\item[@{text "ExecutableSet"}] allows to generate code |
21089 | 499 |
for finite sets using lists. |
21452 | 500 |
\item[@{text "ExecutableRat"}] \label{exec_rat} implements rational |
21089 | 501 |
numbers as triples @{text "(sign, enumerator, denominator)"}. |
21452 | 502 |
\item[@{text "EfficientNat"}] \label{eff_nat} implements natural numbers by integers, |
21178 | 503 |
which in general will result in higher efficency; pattern |
21089 | 504 |
matching with @{const "0\<Colon>nat"} / @{const "Suc"} |
21189 | 505 |
is eliminated. |
21452 | 506 |
\item[@{text "MLString"}] provides an additional datatype @{text "mlstring"}; |
21089 | 507 |
in the HOL default setup, strings in HOL are mapped to list |
508 |
of chars in SML; values of type @{text "mlstring"} are |
|
509 |
mapped to strings in SML. |
|
510 |
||
511 |
\end{description} |
|
512 |
*} |
|
513 |
||
20948 | 514 |
subsection {* Preprocessing *} |
515 |
||
21089 | 516 |
text {* |
21147 | 517 |
Before selected function theorems are turned into abstract |
518 |
code, a chain of definitional transformation steps is carried |
|
21178 | 519 |
out: \emph{preprocessing}. There are three possibilities |
21147 | 520 |
to customize preprocessing: \emph{inline theorems}, |
521 |
\emph{inline procedures} and \emph{generic preprocessors}. |
|
522 |
||
523 |
\emph{Inline theorems} are rewriting rules applied to each |
|
22060 | 524 |
defining equation. Due to the interpretation of theorems |
525 |
of defining equations, rewrites are applied to the right |
|
21147 | 526 |
hand side and the arguments of the left hand side of an |
527 |
equation, but never to the constant heading the left hand side. |
|
528 |
Inline theorems may be declared an undeclared using the |
|
21178 | 529 |
\emph{code inline} or \emph{code noinline} attribute respectively. |
21147 | 530 |
|
531 |
Some common applications: |
|
532 |
*} |
|
533 |
||
534 |
text_raw {* |
|
535 |
\begin{itemize} |
|
536 |
\item replacing non-executable constructs by executable ones: \\ |
|
537 |
*} |
|
538 |
||
539 |
lemma [code inline]: |
|
540 |
"x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all |
|
541 |
||
542 |
text_raw {* |
|
543 |
\item eliminating superfluous constants: \\ |
|
544 |
*} |
|
545 |
||
546 |
lemma [code inline]: |
|
547 |
"1 = Suc 0" by simp |
|
548 |
||
549 |
text_raw {* |
|
550 |
\item replacing executable but inconvenient constructs: \\ |
|
21089 | 551 |
*} |
552 |
||
21147 | 553 |
lemma [code inline]: |
554 |
"xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all |
|
555 |
||
556 |
text_raw {* |
|
557 |
\end{itemize} |
|
558 |
*} |
|
559 |
||
560 |
text {* |
|
561 |
The current set of inline theorems may be inspected using |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
562 |
the @{text "\<PRINTCODESETUP>"} command. |
21147 | 563 |
|
564 |
\emph{Inline procedures} are a generalized version of inline |
|
565 |
theorems written in ML -- rewrite rules are generated dependent |
|
566 |
on the function theorems for a certain function. One |
|
567 |
application is the implicit expanding of @{typ nat} numerals |
|
568 |
to @{const "0\<Colon>nat"} / @{const Suc} representation. See further |
|
569 |
\secref{sec:ml} |
|
570 |
||
571 |
\emph{Generic preprocessors} provide a most general interface, |
|
572 |
transforming a list of function theorems to another |
|
573 |
list of function theorems, provided that neither the heading |
|
574 |
constant nor its type change. The @{const "0\<Colon>nat"} / @{const Suc} |
|
21323 | 575 |
pattern elimination implemented in |
21452 | 576 |
theory @{text "EfficientNat"} (\secref{eff_nat}) uses this |
21147 | 577 |
interface. |
578 |
||
579 |
\begin{warn} |
|
580 |
The order in which single preprocessing steps are carried |
|
581 |
out currently is not specified; in particular, preprocessing |
|
21178 | 582 |
is \emph{no} fix point process. Keep this in mind when |
21147 | 583 |
setting up the preprocessor. |
584 |
||
585 |
Further, the attribute \emph{code unfold} |
|
586 |
associated with the existing code generator also applies to |
|
587 |
the new one: \emph{code unfold} implies \emph{code inline}. |
|
588 |
\end{warn} |
|
589 |
*} |
|
20948 | 590 |
|
21058 | 591 |
subsection {* Customizing serialization *} |
20948 | 592 |
|
21147 | 593 |
text {* |
594 |
Consider the following function and its corresponding |
|
595 |
SML code: |
|
596 |
*} |
|
597 |
||
598 |
fun |
|
599 |
in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
600 |
"in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l" |
|
601 |
||
602 |
(*<*) |
|
21323 | 603 |
code_type %tt bool |
21147 | 604 |
(SML) |
21323 | 605 |
code_const %tt True and False and "op \<and>" and Not |
21147 | 606 |
(SML and and and) |
607 |
(*>*) |
|
608 |
||
21545 | 609 |
code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML") |
21147 | 610 |
|
611 |
text {* |
|
21323 | 612 |
\lstsml{Thy/examples/bool_literal.ML} |
21147 | 613 |
|
614 |
Though this is correct code, it is a little bit unsatisfactory: |
|
615 |
boolean values and operators are materialized as distinguished |
|
616 |
entities with have nothing to do with the SML-builtin notion |
|
617 |
of \qt{bool}. This results in less readable code; |
|
618 |
additionally, eager evaluation may cause programs to |
|
619 |
loop or break which would perfectly terminate when |
|
620 |
the existing SML \qt{bool} would be used. To map |
|
621 |
the HOL \qt{bool} on SML \qt{bool}, we may use |
|
622 |
\qn{custom serializations}: |
|
623 |
*} |
|
624 |
||
21323 | 625 |
code_type %tt bool |
21147 | 626 |
(SML "bool") |
21323 | 627 |
code_const %tt True and False and "op \<and>" |
21147 | 628 |
(SML "true" and "false" and "_ andalso _") |
629 |
||
630 |
text {* |
|
21323 | 631 |
The @{text "\<CODETYPE>"} commad takes a type constructor |
21147 | 632 |
as arguments together with a list of custom serializations. |
633 |
Each custom serialization starts with a target language |
|
634 |
identifier followed by an expression, which during |
|
635 |
code serialization is inserted whenever the type constructor |
|
21323 | 636 |
would occur. For constants, @{text "\<CODECONST>"} implements |
637 |
the corresponding mechanism. Each ``@{verbatim "_"}'' in |
|
21147 | 638 |
a serialization expression is treated as a placeholder |
639 |
for the type constructor's (the constant's) arguments. |
|
640 |
*} |
|
641 |
||
642 |
code_reserved SML |
|
643 |
bool true false |
|
644 |
||
645 |
text {* |
|
646 |
To assert that the existing \qt{bool}, \qt{true} and \qt{false} |
|
21323 | 647 |
is not used for generated code, we use @{text "\<CODERESERVED>"}. |
21147 | 648 |
|
649 |
After this setup, code looks quite more readable: |
|
650 |
*} |
|
651 |
||
21545 | 652 |
code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_mlbool.ML") |
21147 | 653 |
|
654 |
text {* |
|
21323 | 655 |
\lstsml{Thy/examples/bool_mlbool.ML} |
21147 | 656 |
|
657 |
This still is not perfect: the parentheses |
|
21323 | 658 |
around the \qt{andalso} expression are superfluous. |
659 |
Though the serializer |
|
21147 | 660 |
by no means attempts to imitate the rich Isabelle syntax |
661 |
framework, it provides some common idioms, notably |
|
662 |
associative infixes with precedences which may be used here: |
|
663 |
*} |
|
664 |
||
21323 | 665 |
code_const %tt "op \<and>" |
21147 | 666 |
(SML infixl 1 "andalso") |
667 |
||
21545 | 668 |
code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_infix.ML") |
21147 | 669 |
|
670 |
text {* |
|
21323 | 671 |
\lstsml{Thy/examples/bool_infix.ML} |
21147 | 672 |
|
673 |
Next, we try to map HOL pairs to SML pairs, using the |
|
21323 | 674 |
infix ``@{verbatim "*"}'' type constructor and parentheses: |
21147 | 675 |
*} |
676 |
||
677 |
(*<*) |
|
678 |
code_type * |
|
679 |
(SML) |
|
680 |
code_const Pair |
|
681 |
(SML) |
|
682 |
(*>*) |
|
683 |
||
21323 | 684 |
code_type %tt * |
21147 | 685 |
(SML infix 2 "*") |
686 |
||
21323 | 687 |
code_const %tt Pair |
21147 | 688 |
(SML "!((_),/ (_))") |
689 |
||
690 |
text {* |
|
21323 | 691 |
The initial bang ``@{verbatim "!"}'' tells the serializer to never put |
21147 | 692 |
parentheses around the whole expression (they are already present), |
693 |
while the parentheses around argument place holders |
|
694 |
tell not to put parentheses around the arguments. |
|
21323 | 695 |
The slash ``@{verbatim "/"}'' (followed by arbitrary white space) |
21147 | 696 |
inserts a space which may be used as a break if necessary |
697 |
during pretty printing. |
|
698 |
||
21178 | 699 |
So far, we did only provide more idiomatic serializations for |
700 |
constructs which would be executable on their own. Target-specific |
|
701 |
serializations may also be used to \emph{implement} constructs |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
702 |
which have no explicit notion of executability. For example, |
21178 | 703 |
take the HOL integers: |
704 |
*} |
|
705 |
||
706 |
definition |
|
21993 | 707 |
double_inc :: "int \<Rightarrow> int" where |
21178 | 708 |
"double_inc k = 2 * k + 1" |
709 |
||
710 |
code_gen double_inc (SML "examples/integers.ML") |
|
711 |
||
712 |
text {* |
|
713 |
will fail: @{typ int} in HOL is implemented using a quotient |
|
714 |
type, which does not provide any notion of executability. |
|
715 |
\footnote{Eventually, we also want to provide executability |
|
716 |
for quotients.}. However, we could use the SML builtin |
|
717 |
integers: |
|
21147 | 718 |
*} |
719 |
||
21323 | 720 |
code_type %tt int |
21147 | 721 |
(SML "IntInf.int") |
722 |
||
21323 | 723 |
code_const %tt "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
21147 | 724 |
and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
21178 | 725 |
(SML "IntInf.+ (_, _)" and "IntInf.* (_, _)") |
726 |
||
21545 | 727 |
code_gen double_inc (*<*)(SML #)(*>*)(SML "examples/integers.ML") |
21147 | 728 |
|
21178 | 729 |
text {* |
730 |
resulting in: |
|
21147 | 731 |
|
21178 | 732 |
\lstsml{Thy/examples/integers.ML} |
733 |
*} |
|
21147 | 734 |
|
21178 | 735 |
text {* |
736 |
These examples give a glimpse what powerful mechanisms |
|
737 |
custom serializations provide; however their usage |
|
738 |
requires careful thinking in order not to introduce |
|
739 |
inconsistencies -- or, in other words: |
|
740 |
custom serializations are completely axiomatic. |
|
21147 | 741 |
|
21178 | 742 |
A further noteworthy details is that any special |
743 |
character in a custom serialization may be quoted |
|
21323 | 744 |
using ``@{verbatim "'"}''; thus, in |
745 |
``@{verbatim "fn '_ => _"}'' the first |
|
746 |
``@{verbatim "_"}'' is a proper underscore while the |
|
747 |
second ``@{verbatim "_"}'' is a placeholder. |
|
21147 | 748 |
|
21178 | 749 |
The HOL theories provide further |
750 |
examples for custom serializations and form |
|
751 |
a recommended tutorial on how to use them properly. |
|
752 |
*} |
|
21147 | 753 |
|
754 |
subsection {* Concerning operational equality *} |
|
755 |
||
756 |
text {* |
|
757 |
Surely you have already noticed how equality is treated |
|
758 |
by the code generator: |
|
759 |
*} |
|
760 |
||
761 |
fun |
|
762 |
collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
22473 | 763 |
"collect_duplicates xs ys [] = xs" |
764 |
| "collect_duplicates xs ys (z#zs) = (if z \<in> set xs |
|
765 |
then if z \<in> set ys |
|
766 |
then collect_duplicates xs ys zs |
|
767 |
else collect_duplicates xs (z#ys) zs |
|
768 |
else collect_duplicates (z#xs) (z#ys) zs)" |
|
21147 | 769 |
|
770 |
text {* |
|
21217 | 771 |
The membership test during preprocessing is rewritten, |
21147 | 772 |
resulting in @{const List.memberl}, which itself |
773 |
performs an explicit equality check. |
|
774 |
*} |
|
775 |
||
21545 | 776 |
code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML") |
21147 | 777 |
|
778 |
text {* |
|
779 |
\lstsml{Thy/examples/collect_duplicates.ML} |
|
780 |
*} |
|
781 |
||
782 |
text {* |
|
783 |
Obviously, polymorphic equality is implemented the Haskell |
|
784 |
way using a type class. How is this achieved? By an |
|
785 |
almost trivial definition in the HOL setup: |
|
786 |
*} |
|
787 |
||
788 |
(*<*) |
|
789 |
setup {* Sign.add_path "foo" *} |
|
21452 | 790 |
consts "op =" :: "'a" |
21147 | 791 |
(*>*) |
792 |
||
22473 | 793 |
class eq (attach "op =") = type |
21147 | 794 |
|
795 |
text {* |
|
796 |
This merely introduces a class @{text eq} with corresponding |
|
21993 | 797 |
operation @{text "op ="}; |
21452 | 798 |
the preprocessing framework does the rest. |
21147 | 799 |
*} |
800 |
||
801 |
(*<*) |
|
802 |
hide (open) "class" eq |
|
21452 | 803 |
hide (open) const "op =" |
21147 | 804 |
setup {* Sign.parent_path *} |
805 |
(*>*) |
|
806 |
||
807 |
text {* |
|
808 |
For datatypes, instances of @{text eq} are implicitly derived |
|
809 |
when possible. |
|
810 |
||
811 |
Though this class is designed to get rarely in the way, there |
|
812 |
are some cases when it suddenly comes to surface: |
|
813 |
*} |
|
814 |
||
21223 | 815 |
subsubsection {* typedecls interpreted by customary serializations *} |
21178 | 816 |
|
817 |
text {* |
|
818 |
A common idiom is to use unspecified types for formalizations |
|
819 |
and interpret them for a specific target language: |
|
21147 | 820 |
*} |
821 |
||
822 |
typedecl key |
|
823 |
||
824 |
fun |
|
825 |
lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where |
|
22473 | 826 |
"lookup [] l = None" |
827 |
| "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)" |
|
21147 | 828 |
|
21323 | 829 |
code_type %tt key |
21147 | 830 |
(SML "string") |
831 |
||
21178 | 832 |
text {* |
833 |
This, though, is not sufficient: @{typ key} is no instance |
|
21147 | 834 |
of @{text eq} since @{typ key} is no datatype; the instance |
835 |
has to be declared manually, including a serialization |
|
21452 | 836 |
for the particular instance of @{const "op ="}: |
21147 | 837 |
*} |
838 |
||
839 |
instance key :: eq .. |
|
840 |
||
21452 | 841 |
code_const %tt "op = \<Colon> key \<Rightarrow> key \<Rightarrow> bool" |
842 |
(SML "!((_ : string) = _)") |
|
21147 | 843 |
|
21178 | 844 |
text {* |
845 |
Then everything goes fine: |
|
21147 | 846 |
*} |
847 |
||
21545 | 848 |
code_gen lookup (*<*)(SML #)(*>*)(SML "examples/lookup.ML") |
21147 | 849 |
|
850 |
text {* |
|
851 |
\lstsml{Thy/examples/lookup.ML} |
|
852 |
*} |
|
853 |
||
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
854 |
subsubsection {* lexicographic orderings *} |
21178 | 855 |
|
856 |
text {* |
|
857 |
Another subtlety |
|
21147 | 858 |
enters the stage when definitions of overloaded constants |
859 |
are dependent on operational equality. For example, let |
|
21189 | 860 |
us define a lexicographic ordering on tuples: |
21147 | 861 |
*} |
862 |
||
21178 | 863 |
instance * :: (ord, ord) ord |
864 |
"p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in |
|
21147 | 865 |
x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)" |
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
866 |
"p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
867 |
x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" .. |
21147 | 868 |
|
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
869 |
lemma ord_prod [code func]: |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
870 |
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)" |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
871 |
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
872 |
unfolding "less_eq_*_def" "less_*_def" by simp_all |
21147 | 873 |
|
21178 | 874 |
text {* |
875 |
Then code generation will fail. Why? The definition |
|
21147 | 876 |
of @{const "op \<le>"} depends on equality on both arguments, |
21178 | 877 |
which are polymorphic and impose an additional @{text eq} |
21147 | 878 |
class constraint, thus violating the type discipline |
879 |
for class operations. |
|
880 |
||
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
881 |
The solution is to add @{text eq} explicitly to the first sort arguments in the |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
882 |
code theorems: |
21147 | 883 |
*} |
884 |
||
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
885 |
(*<*) |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
886 |
declare ord_prod [code del] |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
887 |
(*>*) |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
888 |
|
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
889 |
lemma ord_prod_code [code func]: |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
890 |
"(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)" |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
891 |
"(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
892 |
unfolding ord_prod by rule+ |
21147 | 893 |
|
21178 | 894 |
text {* |
895 |
Then code generation succeeds: |
|
21147 | 896 |
*} |
897 |
||
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
898 |
code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
21545 | 899 |
(*<*)(SML #)(*>*)(SML "examples/lexicographic.ML") |
21147 | 900 |
|
901 |
text {* |
|
902 |
\lstsml{Thy/examples/lexicographic.ML} |
|
903 |
*} |
|
904 |
||
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
905 |
text {* |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
906 |
In general, code theorems for overloaded constants may have more |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
907 |
restrictive sort constraints than the underlying instance relation |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
908 |
between class and type constructor as long as the whole system of |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
909 |
constraints is coregular; code theorems violating coregularity |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
910 |
are rejected immediately. |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
911 |
*} |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
912 |
|
21178 | 913 |
subsubsection {* Haskell serialization *} |
914 |
||
915 |
text {* |
|
916 |
For convenience, the default |
|
917 |
HOL setup for Haskell maps the @{text eq} class to |
|
918 |
its counterpart in Haskell, giving custom serializations |
|
21323 | 919 |
for the class (@{text "\<CODECLASS>"}) and its operation: |
21178 | 920 |
*} |
921 |
||
922 |
(*<*) |
|
923 |
setup {* Sign.add_path "bar" *} |
|
22473 | 924 |
class eq = type + fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
21178 | 925 |
(*>*) |
926 |
||
21323 | 927 |
code_class %tt eq |
21178 | 928 |
(Haskell "Eq" where eq \<equiv> "(==)") |
929 |
||
21323 | 930 |
code_const %tt eq |
21178 | 931 |
(Haskell infixl 4 "==") |
932 |
||
933 |
(*<*) |
|
934 |
hide "class" eq |
|
935 |
hide const eq |
|
936 |
setup {* Sign.parent_path *} |
|
937 |
(*>*) |
|
938 |
||
939 |
text {* |
|
940 |
A problem now occurs whenever a type which |
|
941 |
is an instance of @{text eq} in HOL is mapped |
|
942 |
on a Haskell-builtin type which is also an instance |
|
943 |
of Haskell @{text Eq}: |
|
21147 | 944 |
*} |
945 |
||
21178 | 946 |
typedecl bar |
947 |
||
948 |
instance bar :: eq .. |
|
949 |
||
21323 | 950 |
code_type %tt bar |
21178 | 951 |
(Haskell "Integer") |
952 |
||
953 |
text {* |
|
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
954 |
The code generator would produce |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
955 |
an additional instance, which of course is rejected. |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
956 |
To suppress this additional instance, use |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
957 |
@{text "\<CODEINSTANCE>"}: |
21147 | 958 |
*} |
959 |
||
21323 | 960 |
code_instance %tt bar :: eq |
21178 | 961 |
(Haskell -) |
962 |
||
963 |
subsection {* Types matter *} |
|
964 |
||
965 |
text {* |
|
966 |
Imagine the following quick-and-dirty setup for implementing |
|
21189 | 967 |
some kind of sets as lists in SML: |
21178 | 968 |
*} |
969 |
||
21323 | 970 |
code_type %tt set |
21178 | 971 |
(SML "_ list") |
972 |
||
21323 | 973 |
code_const %tt "{}" and insert |
21178 | 974 |
(SML "![]" and infixl 7 "::") |
975 |
||
976 |
definition |
|
21993 | 977 |
dummy_set :: "(nat \<Rightarrow> nat) set" where |
21189 | 978 |
"dummy_set = {Suc}" |
979 |
||
980 |
text {* |
|
981 |
Then code generation for @{const dummy_set} will fail. |
|
22060 | 982 |
Why? A glimpse at the defining equations will offer: |
21189 | 983 |
*} |
984 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
985 |
code_thms insert |
21189 | 986 |
|
987 |
text {* |
|
22060 | 988 |
This reveals the defining equation @{thm insert_def} |
21223 | 989 |
for @{const insert}, which is operationally meaningless |
21189 | 990 |
but forces an equality constraint on the set members |
21223 | 991 |
(which is not satisfiable if the set members are functions). |
21189 | 992 |
Even when using set of natural numbers (which are an instance |
993 |
of \emph{eq}), we run into a problem: |
|
994 |
*} |
|
995 |
||
996 |
definition |
|
21993 | 997 |
foobar_set :: "nat set" where |
21189 | 998 |
"foobar_set = {0, 1, 2}" |
999 |
||
1000 |
text {* |
|
1001 |
In this case the serializer would complain that @{const insert} |
|
1002 |
expects dictionaries (namely an \emph{eq} dictionary) but |
|
1003 |
has also been given a customary serialization. |
|
1004 |
||
1005 |
The solution to this dilemma: |
|
1006 |
*} |
|
1007 |
||
1008 |
lemma [code func]: |
|
1009 |
"insert = insert" .. |
|
1010 |
||
21545 | 1011 |
code_gen dummy_set foobar_set (*<*)(SML #)(*>*)(SML "examples/dirty_set.ML") |
21189 | 1012 |
|
1013 |
text {* |
|
1014 |
\lstsml{Thy/examples/dirty_set.ML} |
|
21178 | 1015 |
|
22060 | 1016 |
Reflexive defining equations by convention are dropped. |
21189 | 1017 |
But their presence prevents primitive definitions to be |
22060 | 1018 |
used as defining equations: |
21189 | 1019 |
*} |
1020 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1021 |
code_thms insert |
21189 | 1022 |
|
1023 |
text {* |
|
22060 | 1024 |
will show \emph{no} defining equations for insert. |
21178 | 1025 |
|
21189 | 1026 |
Note that the sort constraints of reflexive equations |
1027 |
are considered; so |
|
1028 |
*} |
|
1029 |
||
1030 |
lemma [code func]: |
|
1031 |
"(insert \<Colon> 'a\<Colon>eq \<Rightarrow> 'a set \<Rightarrow> 'a set) = insert" .. |
|
1032 |
||
1033 |
text {* |
|
1034 |
would mean nothing else than to introduce the evil |
|
1035 |
sort constraint by hand. |
|
1036 |
*} |
|
1037 |
||
22550 | 1038 |
|
1039 |
subsection {* Constructor sets for datatypes *} |
|
1040 |
||
1041 |
text {* |
|
1042 |
\fixme |
|
1043 |
*} |
|
1044 |
||
1045 |
||
21189 | 1046 |
subsection {* Cyclic module dependencies *} |
21178 | 1047 |
|
21189 | 1048 |
text {* |
1049 |
Sometimes the awkward situation occurs that dependencies |
|
1050 |
between definitions introduce cyclic dependencies |
|
1051 |
between modules, which in the Haskell world leaves |
|
1052 |
you to the mercy of the Haskell implementation you are using, |
|
1053 |
while for SML code generation is not possible. |
|
21178 | 1054 |
|
21189 | 1055 |
A solution is to declare module names explicitly. |
1056 |
Let use assume the three cyclically dependent |
|
1057 |
modules are named \emph{A}, \emph{B} and \emph{C}. |
|
1058 |
Then, by stating |
|
1059 |
*} |
|
1060 |
||
1061 |
code_modulename SML |
|
1062 |
A ABC |
|
1063 |
B ABC |
|
1064 |
C ABC |
|
1065 |
||
1066 |
text {* |
|
1067 |
we explicitly map all those modules on \emph{ABC}, |
|
1068 |
resulting in an ad-hoc merge of this three modules |
|
1069 |
at serialization time. |
|
1070 |
*} |
|
21147 | 1071 |
|
1072 |
subsection {* Axiomatic extensions *} |
|
1073 |
||
1074 |
text {* |
|
1075 |
\begin{warn} |
|
1076 |
The extensions introduced in this section, though working |
|
21189 | 1077 |
in practice, are not the cream of the crop, as you |
1078 |
will notice during reading. They will |
|
21147 | 1079 |
eventually be replaced by more mature approaches. |
1080 |
\end{warn} |
|
21189 | 1081 |
|
1082 |
Sometimes equalities are taken for granted which are |
|
1083 |
not derivable inside the HOL logic but are silently assumed |
|
1084 |
to hold for executable code. For example, we may want |
|
1085 |
to identify the famous HOL constant @{const arbitrary} |
|
1086 |
of type @{typ "'a option"} with @{const None}. |
|
1087 |
By brute force: |
|
1088 |
*} |
|
1089 |
||
21323 | 1090 |
axiomatization where |
1091 |
"arbitrary = None" |
|
21189 | 1092 |
|
1093 |
text {* |
|
1094 |
However this has to be considered harmful since this axiom, |
|
1095 |
though probably justifiable for generated code, could |
|
1096 |
introduce serious inconsistencies into the logic. |
|
1097 |
||
1098 |
So, there is a distinguished construct for stating axiomatic |
|
1099 |
equalities of constants which apply only for code generation. |
|
1100 |
Before introducing this, here is a convenient place to describe |
|
1101 |
shortly how to deal with some restrictions the type discipline |
|
1102 |
imposes. |
|
1103 |
||
1104 |
By itself, the constant @{const arbitrary} is a non-overloaded |
|
1105 |
polymorphic constant. So, there is no way to distinguish |
|
1106 |
different versions of @{const arbitrary} for different types |
|
1107 |
inside the code generator framework. However, inlining |
|
1108 |
theorems together with auxiliary constants provide a solution: |
|
21147 | 1109 |
*} |
1110 |
||
21189 | 1111 |
definition |
21993 | 1112 |
arbitrary_option :: "'a option" where |
21189 | 1113 |
[symmetric, code inline]: "arbitrary_option = arbitrary" |
1114 |
||
1115 |
text {* |
|
1116 |
By that, we replace any @{const arbitrary} with option type |
|
22060 | 1117 |
by @{const arbitrary_option} in defining equations. |
21189 | 1118 |
|
1119 |
For technical reasons, we further have to provide a |
|
1120 |
synonym for @{const None} which in code generator view |
|
22175 | 1121 |
is a function rather than a term constructor: |
21189 | 1122 |
*} |
1123 |
||
1124 |
definition |
|
1125 |
"None' = None" |
|
1126 |
||
1127 |
text {* |
|
21323 | 1128 |
Then finally we are enabled to use @{text "\<CODEAXIOMS>"}: |
21189 | 1129 |
*} |
1130 |
||
1131 |
code_axioms |
|
1132 |
arbitrary_option \<equiv> None' |
|
1133 |
||
1134 |
text {* |
|
1135 |
A dummy example: |
|
1136 |
*} |
|
1137 |
||
1138 |
fun |
|
1139 |
dummy_option :: "'a list \<Rightarrow> 'a option" where |
|
22473 | 1140 |
"dummy_option (x#xs) = Some x" |
1141 |
| "dummy_option [] = arbitrary" |
|
21189 | 1142 |
|
21545 | 1143 |
code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML") |
21189 | 1144 |
|
1145 |
text {* |
|
1146 |
\lstsml{Thy/examples/arbitrary.ML} |
|
1147 |
||
1148 |
Another axiomatic extension is code generation |
|
1149 |
for abstracted types. For this, the |
|
21452 | 1150 |
@{text "ExecutableRat"} (see \secref{exec_rat}) |
21189 | 1151 |
forms a good example. |
1152 |
*} |
|
1153 |
||
20948 | 1154 |
|
21058 | 1155 |
section {* ML interfaces \label{sec:ml} *} |
20948 | 1156 |
|
21189 | 1157 |
text {* |
1158 |
Since the code generator framework not only aims to provide |
|
1159 |
a nice Isar interface but also to form a base for |
|
1160 |
code-generation-based applications, here a short |
|
1161 |
description of the most important ML interfaces. |
|
1162 |
*} |
|
1163 |
||
21147 | 1164 |
subsection {* Constants with type discipline: codegen\_consts.ML *} |
1165 |
||
21189 | 1166 |
text {* |
1167 |
This Pure module manages identification of (probably overloaded) |
|
1168 |
constants by unique identifiers. |
|
1169 |
*} |
|
1170 |
||
21147 | 1171 |
text %mlref {* |
1172 |
\begin{mldecls} |
|
22550 | 1173 |
@{index_ML_type CodegenConsts.const: "string * string option"} \\ |
1174 |
@{index_ML CodegenConsts.const_of_cexpr: "theory -> string * typ -> CodegenConsts.const"} \\ |
|
21189 | 1175 |
\end{mldecls} |
1176 |
||
1177 |
\begin{description} |
|
1178 |
||
1179 |
\item @{ML_type CodegenConsts.const} is the identifier type: |
|
1180 |
the product of a \emph{string} with a list of \emph{typs}. |
|
1181 |
The \emph{string} is the constant name as represented inside Isabelle; |
|
22550 | 1182 |
for overloaded constants, the attached \emph{string option} |
1183 |
is either @{text SOME} type constructor denoting an instance, |
|
1184 |
or @{text NONE} for the polymorphic constant. |
|
21189 | 1185 |
|
22550 | 1186 |
\item @{ML CodegenConsts.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"} |
1187 |
maps a constant expression @{text "(constname, typ)"} |
|
1188 |
to its canonical identifier. |
|
21189 | 1189 |
|
1190 |
\end{description} |
|
21147 | 1191 |
*} |
1192 |
||
1193 |
subsection {* Executable theory content: codegen\_data.ML *} |
|
1194 |
||
1195 |
text {* |
|
1196 |
This Pure module implements the core notions of |
|
1197 |
executable content of a theory. |
|
1198 |
*} |
|
1199 |
||
1200 |
subsubsection {* Suspended theorems *} |
|
1201 |
||
1202 |
text %mlref {* |
|
1203 |
\begin{mldecls} |
|
21341 | 1204 |
@{index_ML CodegenData.lazy: "(unit -> thm list) -> thm list Susp.T"} |
21147 | 1205 |
\end{mldecls} |
21189 | 1206 |
|
1207 |
\begin{description} |
|
1208 |
||
1209 |
\item @{ML CodegenData.lazy}~@{text f} turns an abstract |
|
21323 | 1210 |
theorem computation @{text f} into a suspension of theorems. |
21189 | 1211 |
|
1212 |
\end{description} |
|
21147 | 1213 |
*} |
1214 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1215 |
subsubsection {* Managing executable content *} |
20948 | 1216 |
|
21147 | 1217 |
text %mlref {* |
1218 |
\begin{mldecls} |
|
22550 | 1219 |
@{index_ML CodegenData.add_func: "bool -> thm -> theory -> theory"} \\ |
21147 | 1220 |
@{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\ |
21341 | 1221 |
@{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\ |
21147 | 1222 |
@{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\ |
1223 |
@{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\ |
|
22046 | 1224 |
@{index_ML CodegenData.add_inline_proc: "string * (theory -> cterm list -> thm list) |
21189 | 1225 |
-> theory -> theory"} \\ |
22046 | 1226 |
@{index_ML CodegenData.del_inline_proc: "string -> theory -> theory"} \\ |
1227 |
@{index_ML CodegenData.add_preproc: "string * (theory -> thm list -> thm list) |
|
21189 | 1228 |
-> theory -> theory"} \\ |
22046 | 1229 |
@{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\ |
22423 | 1230 |
@{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list) |
1231 |
-> theory -> theory"} \\ |
|
21189 | 1232 |
@{index_ML CodegenData.get_datatype: "theory -> string |
22479 | 1233 |
-> (string * sort) list * (string * typ list) list"} \\ |
21147 | 1234 |
@{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"} |
1235 |
\end{mldecls} |
|
1236 |
||
1237 |
\begin{description} |
|
1238 |
||
21189 | 1239 |
\item @{ML CodegenData.add_func}~@{text "thm"}~@{text "thy"} adds function |
1240 |
theorem @{text "thm"} to executable content. |
|
1241 |
||
1242 |
\item @{ML CodegenData.del_func}~@{text "thm"}~@{text "thy"} removes function |
|
1243 |
theorem @{text "thm"} from executable content, if present. |
|
1244 |
||
1245 |
\item @{ML CodegenData.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds |
|
22060 | 1246 |
suspended defining equations @{text lthms} for constant |
21189 | 1247 |
@{text const} to executable content. |
1248 |
||
1249 |
\item @{ML CodegenData.add_inline}~@{text "thm"}~@{text "thy"} adds |
|
21223 | 1250 |
inlining theorem @{text thm} to executable content. |
21189 | 1251 |
|
1252 |
\item @{ML CodegenData.del_inline}~@{text "thm"}~@{text "thy"} remove |
|
1253 |
inlining theorem @{text thm} from executable content, if present. |
|
1254 |
||
22046 | 1255 |
\item @{ML CodegenData.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds |
1256 |
inline procedure @{text f} (named @{text name}) to executable content; |
|
21189 | 1257 |
@{text f} is a computation of rewrite rules dependent on |
1258 |
the current theory context and the list of all arguments |
|
22060 | 1259 |
and right hand sides of the defining equations belonging |
21189 | 1260 |
to a certain function definition. |
1261 |
||
22046 | 1262 |
\item @{ML CodegenData.del_inline_proc}~@{text "name"}~@{text "thy"} removes |
1263 |
inline procedure named @{text name} from executable content. |
|
1264 |
||
1265 |
\item @{ML CodegenData.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds |
|
1266 |
generic preprocessor @{text f} (named @{text name}) to executable content; |
|
22060 | 1267 |
@{text f} is a transformation of the defining equations belonging |
21189 | 1268 |
to a certain function definition, depending on the |
1269 |
current theory context. |
|
1270 |
||
22060 | 1271 |
\item @{ML CodegenData.del_preproc}~@{text "name"}~@{text "thy"} removes |
22046 | 1272 |
generic preprcoessor named @{text name} from executable content. |
1273 |
||
22423 | 1274 |
\item @{ML CodegenData.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds |
21189 | 1275 |
a datatype to executable content, with type constructor |
1276 |
@{text name} and specification @{text spec}; @{text spec} is |
|
1277 |
a pair consisting of a list of type variable with sort |
|
21223 | 1278 |
constraints and a list of constructors with name |
22423 | 1279 |
and types of arguments. |
21189 | 1280 |
|
1281 |
\item @{ML CodegenData.get_datatype_of_constr}~@{text "thy"}~@{text "const"} |
|
1282 |
returns type constructor corresponding to |
|
1283 |
constructor @{text const}; returns @{text NONE} |
|
1284 |
if @{text const} is no constructor. |
|
21147 | 1285 |
|
1286 |
\end{description} |
|
1287 |
*} |
|
1288 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1289 |
subsection {* Auxiliary *} |
21147 | 1290 |
|
1291 |
text %mlref {* |
|
1292 |
\begin{mldecls} |
|
1293 |
@{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\ |
|
1294 |
@{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\ |
|
1295 |
@{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\ |
|
1296 |
@{index_ML_structure CodegenConsts.Consttab} \\ |
|
22060 | 1297 |
@{index_ML CodegenFunc.typ_func: "thm -> typ"} \\ |
1298 |
@{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\ |
|
21147 | 1299 |
\end{mldecls} |
21217 | 1300 |
|
1301 |
\begin{description} |
|
1302 |
||
1303 |
\item @{ML CodegenConsts.const_ord},~@{ML CodegenConsts.eq_const} |
|
1304 |
provide order and equality on constant identifiers. |
|
1305 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1306 |
\item @{ML_struct CodegenConsts.Consttab} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1307 |
provides table structures with constant identifiers as keys. |
21217 | 1308 |
|
1309 |
\item @{ML CodegenConsts.read_const}~@{text thy}~@{text s} |
|
1310 |
reads a constant as a concrete term expression @{text s}. |
|
1311 |
||
22060 | 1312 |
\item @{ML CodegenFunc.typ_func}~@{text thm} |
1313 |
extracts the type of a constant in a defining equation @{text thm}. |
|
21217 | 1314 |
|
22060 | 1315 |
\item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm} |
1316 |
rewrites a defining equation @{text thm} with a set of rewrite |
|
21217 | 1317 |
rules @{text rews}; only arguments and right hand side are rewritten, |
22060 | 1318 |
not the head of the defining equation. |
21217 | 1319 |
|
1320 |
\end{description} |
|
1321 |
||
21147 | 1322 |
*} |
20948 | 1323 |
|
1324 |
subsection {* Implementing code generator applications *} |
|
1325 |
||
21147 | 1326 |
text {* |
21217 | 1327 |
Implementing code generator applications on top |
1328 |
of the framework set out so far usually not only |
|
1329 |
involves using those primitive interfaces |
|
1330 |
but also storing code-dependent data and various |
|
1331 |
other things. |
|
1332 |
||
21147 | 1333 |
\begin{warn} |
1334 |
Some interfaces discussed here have not reached |
|
1335 |
a final state yet. |
|
1336 |
Changes likely to occur in future. |
|
1337 |
\end{warn} |
|
1338 |
*} |
|
1339 |
||
1340 |
subsubsection {* Data depending on the theory's executable content *} |
|
1341 |
||
21217 | 1342 |
text {* |
21452 | 1343 |
Due to incrementality of code generation, changes in the |
1344 |
theory's executable content have to be propagated in a |
|
1345 |
certain fashion. Additionally, such changes may occur |
|
1346 |
not only during theory extension but also during theory |
|
1347 |
merge, which is a little bit nasty from an implementation |
|
1348 |
point of view. The framework provides a solution |
|
1349 |
to this technical challenge by providing a functorial |
|
1350 |
data slot @{ML_functor CodeDataFun}; on instantiation |
|
1351 |
of this functor, the following types and operations |
|
1352 |
are required: |
|
1353 |
||
21217 | 1354 |
\medskip |
1355 |
\begin{tabular}{l} |
|
1356 |
@{text "val name: string"} \\ |
|
1357 |
@{text "type T"} \\ |
|
1358 |
@{text "val empty: T"} \\ |
|
1359 |
@{text "val merge: Pretty.pp \<rightarrow> T * T \<rightarrow> T"} \\ |
|
1360 |
@{text "val purge: theory option \<rightarrow> CodegenConsts.const list option \<rightarrow> T \<rightarrow> T"} |
|
1361 |
\end{tabular} |
|
1362 |
||
21452 | 1363 |
\begin{description} |
1364 |
||
1365 |
\item @{text name} is a system-wide unique name identifying the data. |
|
1366 |
||
1367 |
\item @{text T} the type of data to store. |
|
1368 |
||
1369 |
\item @{text empty} initial (empty) data. |
|
1370 |
||
1371 |
\item @{text merge} merging two data slots. |
|
1372 |
||
1373 |
\item @{text purge}~@{text thy}~@{text cs} propagates changes in executable content; |
|
1374 |
if possible, the current theory context is handed over |
|
1375 |
as argument @{text thy} (if there is no current theory context (e.g.~during |
|
1376 |
theory merge, @{ML NONE}); @{text cs} indicates the kind |
|
1377 |
of change: @{ML NONE} stands for a fundamental change |
|
1378 |
which invalidates any existing code, @{text "SOME cs"} |
|
1379 |
hints that executable content for constants @{text cs} |
|
1380 |
has changed. |
|
1381 |
||
1382 |
\end{description} |
|
1383 |
||
1384 |
An instance of @{ML_functor CodeDataFun} provides the following |
|
1385 |
interface: |
|
1386 |
||
21217 | 1387 |
\medskip |
1388 |
\begin{tabular}{l} |
|
1389 |
@{text "init: theory \<rightarrow> theory"} \\ |
|
1390 |
@{text "get: theory \<rightarrow> T"} \\ |
|
1391 |
@{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\ |
|
1392 |
@{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"} |
|
1393 |
\end{tabular} |
|
1394 |
||
1395 |
\begin{description} |
|
1396 |
||
21452 | 1397 |
\item @{text init} initialization during theory setup. |
1398 |
||
1399 |
\item @{text get} retrieval of the current data. |
|
1400 |
||
1401 |
\item @{text change} update of current data (cached!) |
|
1402 |
by giving a continuation. |
|
1403 |
||
1404 |
\item @{text change_yield} update with side result. |
|
21217 | 1405 |
|
1406 |
\end{description} |
|
1407 |
*} |
|
1408 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1409 |
(* subsubsection {* Building implementable systems fo defining equations *} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1410 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1411 |
text {* |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1412 |
Out of the executable content of a theory, a normalized |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1413 |
defining equation systems may be constructed containing |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1414 |
function definitions for constants. The system is cached |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1415 |
until its underlying executable content changes. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1416 |
*} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1417 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1418 |
text %mlref {* |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1419 |
\begin{mldecls} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1420 |
@{index_ML_type CodegenFuncgr.T} \\ |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1421 |
@{index_ML CodegenFuncgr.make: "theory -> CodegenConsts.const list -> CodegenFuncgr.T"} \\ |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1422 |
@{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\ |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1423 |
@{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\ |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1424 |
@{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1425 |
-> CodegenConsts.const list -> CodegenConsts.const list list"} \\ |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1426 |
@{index_ML CodegenFuncgr.all: "CodegenFuncgr.T -> CodegenConsts.const list"} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1427 |
\end{mldecls} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1428 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1429 |
\begin{description} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1430 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1431 |
\item @{ML_type CodegenFuncgr.T} represents |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1432 |
a normalized defining equation system. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1433 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1434 |
\item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1435 |
returns a normalized defining equation system, |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1436 |
with the assertion that it contains any function |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1437 |
definition for constants @{text cs} (if existing). |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1438 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1439 |
\item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text c} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1440 |
retrieves function definition for constant @{text c}. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1441 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1442 |
\item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text c} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1443 |
retrieves function type for constant @{text c}. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1444 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1445 |
\item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text cs} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1446 |
returns the transitive closure of dependencies for |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1447 |
constants @{text cs} as a partitioning where each partition |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1448 |
corresponds to a strongly connected component of |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1449 |
dependencies and any partition does \emph{not} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1450 |
depend on partitions further left. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1451 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1452 |
\item @{ML CodegenFuncgr.all}~@{text funcgr} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1453 |
returns all currently represented constants. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1454 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1455 |
\end{description} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1456 |
*} *) |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1457 |
|
21147 | 1458 |
subsubsection {* Datatype hooks *} |
1459 |
||
21452 | 1460 |
text {* |
1461 |
Isabelle/HOL's datatype package provides a mechanism to |
|
1462 |
extend theories depending on datatype declarations: |
|
1463 |
\emph{datatype hooks}. For example, when declaring a new |
|
22060 | 1464 |
datatype, a hook proves defining equations for equality on |
21452 | 1465 |
that datatype (if possible). |
1466 |
*} |
|
1467 |
||
21217 | 1468 |
text %mlref {* |
1469 |
\begin{mldecls} |
|
21323 | 1470 |
@{index_ML_type DatatypeHooks.hook: "string list -> theory -> theory"} \\ |
21217 | 1471 |
@{index_ML DatatypeHooks.add: "DatatypeHooks.hook -> theory -> theory"} |
1472 |
\end{mldecls} |
|
21452 | 1473 |
|
1474 |
\begin{description} |
|
1475 |
||
1476 |
\item @{ML_type DatatypeHooks.hook} specifies the interface |
|
1477 |
of \emph{datatype hooks}: a theory update |
|
1478 |
depending on the list of newly introduced |
|
1479 |
datatype names. |
|
1480 |
||
1481 |
\item @{ML DatatypeHooks.add} adds a hook to the |
|
1482 |
chain of all hooks. |
|
1483 |
||
1484 |
\end{description} |
|
1485 |
*} |
|
1486 |
||
1487 |
subsubsection {* Trivial typedefs -- type copies *} |
|
1488 |
||
1489 |
text {* |
|
1490 |
Sometimes packages will introduce new types |
|
1491 |
as \emph{marked type copies} similar to Haskell's |
|
1492 |
@{text newtype} declaration (e.g. the HOL record package) |
|
1493 |
\emph{without} tinkering with the overhead of datatypes. |
|
1494 |
Technically, these type copies are trivial forms of typedefs. |
|
1495 |
Since these type copies in code generation view are nothing |
|
1496 |
else than datatypes, they have been given a own package |
|
1497 |
in order to faciliate code generation: |
|
21147 | 1498 |
*} |
21058 | 1499 |
|
21217 | 1500 |
text %mlref {* |
1501 |
\begin{mldecls} |
|
21452 | 1502 |
@{index_ML_type TypecopyPackage.info} \\ |
21217 | 1503 |
@{index_ML TypecopyPackage.add_typecopy: " |
1504 |
bstring * string list -> typ -> (bstring * bstring) option |
|
1505 |
-> theory -> (string * TypecopyPackage.info) * theory"} \\ |
|
1506 |
@{index_ML TypecopyPackage.get_typecopy_info: "theory |
|
1507 |
-> string -> TypecopyPackage.info option"} \\ |
|
1508 |
@{index_ML TypecopyPackage.get_spec: "theory -> string |
|
21452 | 1509 |
-> (string * sort) list * (string * typ list) list"} \\ |
1510 |
@{index_ML_type TypecopyPackage.hook: "string * TypecopyPackage.info -> theory -> theory"} \\ |
|
1511 |
@{index_ML TypecopyPackage.add_hook: |
|
1512 |
"TypecopyPackage.hook -> theory -> theory"} \\ |
|
21217 | 1513 |
\end{mldecls} |
21452 | 1514 |
|
1515 |
\begin{description} |
|
1516 |
||
1517 |
\item @{ML_type TypecopyPackage.info} a record containing |
|
1518 |
the specification and further data of a type copy. |
|
1519 |
||
1520 |
\item @{ML TypecopyPackage.add_typecopy} defines a new |
|
1521 |
type copy. |
|
1522 |
||
1523 |
\item @{ML TypecopyPackage.get_typecopy_info} retrieves |
|
1524 |
data of an existing type copy. |
|
1525 |
||
1526 |
\item @{ML TypecopyPackage.get_spec} retrieves datatype-like |
|
1527 |
specification of a type copy. |
|
1528 |
||
1529 |
\item @{ML_type TypecopyPackage.hook},~@{ML TypecopyPackage.add_hook} |
|
1530 |
provide a hook mechanism corresponding to the hook mechanism |
|
1531 |
on datatypes. |
|
1532 |
||
1533 |
\end{description} |
|
1534 |
*} |
|
1535 |
||
1536 |
subsubsection {* Unifying type copies and datatypes *} |
|
1537 |
||
1538 |
text {* |
|
1539 |
Since datatypes and type copies are mapped to the same concept (datatypes) |
|
1540 |
by code generation, the view on both is unified \qt{code types}: |
|
21217 | 1541 |
*} |
1542 |
||
1543 |
text %mlref {* |
|
1544 |
\begin{mldecls} |
|
21452 | 1545 |
@{index_ML_type DatatypeCodegen.hook: "(string * (bool * ((string * sort) list |
1546 |
* (string * typ list) list))) list |
|
21323 | 1547 |
-> theory -> theory"} \\ |
21217 | 1548 |
@{index_ML DatatypeCodegen.add_codetypes_hook_bootstrap: " |
1549 |
DatatypeCodegen.hook -> theory -> theory"} |
|
1550 |
\end{mldecls} |
|
1551 |
*} |
|
1552 |
||
21222 | 1553 |
text {* |
21452 | 1554 |
\begin{description} |
1555 |
||
1556 |
\item @{ML_type DatatypeCodegen.hook} specifies the code type hook |
|
1557 |
interface: a theory transformation depending on a list of |
|
1558 |
mutual recursive code types; each entry in the list |
|
1559 |
has the structure @{text "(name, (is_data, (vars, cons)))"} |
|
1560 |
where @{text name} is the name of the code type, @{text is_data} |
|
1561 |
is true iff @{text name} is a datatype rather then a type copy, |
|
1562 |
and @{text "(vars, cons)"} is the specification of the code type. |
|
1563 |
||
1564 |
\item @{ML DatatypeCodegen.add_codetypes_hook_bootstrap} adds a code |
|
1565 |
type hook; the hook is immediately processed for all already |
|
1566 |
existing datatypes, in blocks of mutual recursive datatypes, |
|
1567 |
where all datatypes a block depends on are processed before |
|
1568 |
the block. |
|
1569 |
||
1570 |
\end{description} |
|
1571 |
||
1572 |
\emph{Happy proving, happy hacking!} |
|
21222 | 1573 |
*} |
21217 | 1574 |
|
20948 | 1575 |
end |