author | haftmann |
Fri, 30 May 2008 09:17:44 +0200 | |
changeset 27025 | c1f9fb015ea5 |
parent 26999 | 284c871d3acb |
child 27103 | d8549f4d900b |
permissions | -rw-r--r-- |
26513 | 1 |
|
20948 | 2 |
(* $Id$ *) |
3 |
||
21147 | 4 |
(*<*) |
20948 | 5 |
theory Codegen |
6 |
imports Main |
|
21452 | 7 |
uses "../../../antiquote_setup.ML" |
20948 | 8 |
begin |
9 |
||
21147 | 10 |
ML {* |
27025 | 11 |
CodeTarget.target_code_width := 74; |
21147 | 12 |
*} |
13 |
||
14 |
(*>*) |
|
15 |
||
20948 | 16 |
chapter {* Code generation from Isabelle theories *} |
17 |
||
18 |
section {* Introduction *} |
|
19 |
||
21058 | 20 |
subsection {* Motivation *} |
21 |
||
20948 | 22 |
text {* |
21058 | 23 |
Executing formal specifications as programs is a well-established |
24 |
topic in the theorem proving community. With increasing |
|
25 |
application of theorem proving systems in the area of |
|
26 |
software development and verification, its relevance manifests |
|
27 |
for running test cases and rapid prototyping. In logical |
|
28 |
calculi like constructive type theory, |
|
29 |
a notion of executability is implicit due to the nature |
|
22550 | 30 |
of the calculus. In contrast, specifications in Isabelle |
21058 | 31 |
can be highly non-executable. In order to bridge |
32 |
the gap between logic and executable specifications, |
|
33 |
an explicit non-trivial transformation has to be applied: |
|
34 |
code generation. |
|
35 |
||
36 |
This tutorial introduces a generic code generator for the |
|
37 |
Isabelle system \cite{isa-tutorial}. |
|
38 |
Generic in the sense that the |
|
39 |
\qn{target language} for which code shall ultimately be |
|
40 |
generated is not fixed but may be an arbitrary state-of-the-art |
|
41 |
functional programming language (currently, the implementation |
|
22550 | 42 |
supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell |
43 |
\cite{haskell-revised-report}). |
|
21058 | 44 |
We aim to provide a |
45 |
versatile environment |
|
46 |
suitable for software development and verification, |
|
47 |
structuring the process |
|
48 |
of code generation into a small set of orthogonal principles |
|
49 |
while achieving a big coverage of application areas |
|
50 |
with maximum flexibility. |
|
21189 | 51 |
|
22550 | 52 |
Conceptually the code generator framework is part |
53 |
of Isabelle's @{text Pure} meta logic; the object logic |
|
54 |
@{text HOL} which is an extension of @{text Pure} |
|
55 |
already comes with a reasonable framework setup and thus provides |
|
56 |
a good working horse for raising code-generation-driven |
|
57 |
applications. So, we assume some familiarity and experience |
|
58 |
with the ingredients of the @{text HOL} \emph{Main} theory |
|
59 |
(see also \cite{isa-tutorial}). |
|
21058 | 60 |
*} |
61 |
||
62 |
||
63 |
subsection {* Overview *} |
|
64 |
||
65 |
text {* |
|
66 |
The code generator aims to be usable with no further ado |
|
67 |
in most cases while allowing for detailed customization. |
|
22550 | 68 |
This manifests in the structure of this tutorial: |
69 |
we start with a generic example \secref{sec:example} |
|
70 |
and introduce code generation concepts \secref{sec:concept}. |
|
71 |
Section |
|
21178 | 72 |
\secref{sec:basics} explains how to use the framework naively, |
21058 | 73 |
presuming a reasonable default setup. Then, section |
74 |
\secref{sec:advanced} deals with advanced topics, |
|
75 |
introducing further aspects of the code generator framework |
|
76 |
in a motivation-driven manner. Last, section \secref{sec:ml} |
|
77 |
introduces the framework's internal programming interfaces. |
|
20948 | 78 |
|
21058 | 79 |
\begin{warn} |
80 |
Ultimately, the code generator which this tutorial deals with |
|
81 |
is supposed to replace the already established code generator |
|
82 |
by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. |
|
21147 | 83 |
So, for the moment, there are two distinct code generators |
21058 | 84 |
in Isabelle. |
22916 | 85 |
Also note that while the framework itself is |
22550 | 86 |
object-logic independent, only @{text HOL} provides a reasonable |
21058 | 87 |
framework setup. |
88 |
\end{warn} |
|
89 |
*} |
|
90 |
||
91 |
||
22550 | 92 |
section {* An example: a simple theory of search trees \label{sec:example} *} |
93 |
||
94 |
text {* |
|
22916 | 95 |
When writing executable specifications using @{text HOL}, |
96 |
it is convenient to use |
|
22550 | 97 |
three existing packages: the datatype package for defining |
98 |
datatypes, the function package for (recursive) functions, |
|
99 |
and the class package for overloaded definitions. |
|
100 |
||
101 |
We develope a small theory of search trees; trees are represented |
|
102 |
as a datatype with key type @{typ "'a"} and value type @{typ "'b"}: |
|
103 |
*} |
|
22479 | 104 |
|
105 |
datatype ('a, 'b) searchtree = Leaf "'a\<Colon>linorder" 'b |
|
106 |
| Branch "('a, 'b) searchtree" "'a" "('a, 'b) searchtree" |
|
107 |
||
22550 | 108 |
text {* |
109 |
\noindent Note that we have constrained the type of keys |
|
110 |
to the class of total orders, @{text linorder}. |
|
111 |
||
112 |
We define @{text find} and @{text update} functions: |
|
113 |
*} |
|
114 |
||
25870 | 115 |
primrec |
22479 | 116 |
find :: "('a\<Colon>linorder, 'b) searchtree \<Rightarrow> 'a \<Rightarrow> 'b option" where |
117 |
"find (Leaf key val) it = (if it = key then Some val else None)" |
|
118 |
| "find (Branch t1 key t2) it = (if it \<le> key then find t1 it else find t2 it)" |
|
119 |
||
120 |
fun |
|
121 |
update :: "'a\<Colon>linorder \<times> 'b \<Rightarrow> ('a, 'b) searchtree \<Rightarrow> ('a, 'b) searchtree" where |
|
122 |
"update (it, entry) (Leaf key val) = ( |
|
123 |
if it = key then Leaf key entry |
|
124 |
else if it \<le> key |
|
125 |
then Branch (Leaf it entry) it (Leaf key val) |
|
126 |
else Branch (Leaf key val) it (Leaf it entry) |
|
127 |
)" |
|
128 |
| "update (it, entry) (Branch t1 key t2) = ( |
|
129 |
if it \<le> key |
|
130 |
then (Branch (update (it, entry) t1) key t2) |
|
131 |
else (Branch t1 key (update (it, entry) t2)) |
|
132 |
)" |
|
133 |
||
22550 | 134 |
text {* |
135 |
\noindent For testing purpose, we define a small example |
|
136 |
using natural numbers @{typ nat} (which are a @{text linorder}) |
|
23130 | 137 |
as keys and list of nats as values: |
22550 | 138 |
*} |
139 |
||
23130 | 140 |
definition |
141 |
example :: "(nat, nat list) searchtree" |
|
142 |
where |
|
143 |
"example = update (Suc (Suc (Suc (Suc 0))), [Suc (Suc 0), Suc (Suc 0)]) (update (Suc (Suc (Suc 0)), [Suc (Suc (Suc 0))]) |
|
144 |
(update (Suc (Suc 0), [Suc (Suc 0)]) (Leaf (Suc 0) [])))" |
|
22479 | 145 |
|
22550 | 146 |
text {* |
147 |
\noindent Then we generate code |
|
148 |
*} |
|
149 |
||
26999 | 150 |
export_code example (*<*)in SML (*>*)in SML file "examples/tree.ML" |
22479 | 151 |
|
152 |
text {* |
|
22550 | 153 |
\noindent which looks like: |
22479 | 154 |
\lstsml{Thy/examples/tree.ML} |
155 |
*} |
|
156 |
||
22550 | 157 |
|
158 |
section {* Code generation concepts and process \label{sec:concept} *} |
|
21058 | 159 |
|
160 |
text {* |
|
21189 | 161 |
\begin{figure}[h] |
162 |
\centering |
|
163 |
\includegraphics[width=0.7\textwidth]{codegen_process} |
|
164 |
\caption{code generator -- processing overview} |
|
165 |
\label{fig:process} |
|
166 |
\end{figure} |
|
167 |
||
21058 | 168 |
The code generator employs a notion of executability |
169 |
for three foundational executable ingredients known |
|
170 |
from functional programming: |
|
22060 | 171 |
\emph{defining equations}, \emph{datatypes}, and |
172 |
\emph{type classes}. A defining equation as a first approximation |
|
21058 | 173 |
is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"} |
174 |
(an equation headed by a constant @{text f} with arguments |
|
22798 | 175 |
@{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}). |
22060 | 176 |
Code generation aims to turn defining equations |
21058 | 177 |
into a functional program by running through |
178 |
a process (see figure \ref{fig:process}): |
|
179 |
||
180 |
\begin{itemize} |
|
181 |
||
182 |
\item Out of the vast collection of theorems proven in a |
|
183 |
\qn{theory}, a reasonable subset modeling |
|
22060 | 184 |
defining equations is \qn{selected}. |
21058 | 185 |
|
186 |
\item On those selected theorems, certain |
|
187 |
transformations are carried out |
|
188 |
(\qn{preprocessing}). Their purpose is to turn theorems |
|
189 |
representing non- or badly executable |
|
190 |
specifications into equivalent but executable counterparts. |
|
191 |
The result is a structured collection of \qn{code theorems}. |
|
192 |
||
22479 | 193 |
\item These \qn{code theorems} then are \qn{translated} |
21058 | 194 |
into an Haskell-like intermediate |
195 |
language. |
|
196 |
||
197 |
\item Finally, out of the intermediate language the final |
|
198 |
code in the desired \qn{target language} is \qn{serialized}. |
|
199 |
||
200 |
\end{itemize} |
|
201 |
||
202 |
From these steps, only the two last are carried out |
|
203 |
outside the logic; by keeping this layer as |
|
204 |
thin as possible, the amount of code to trust is |
|
205 |
kept to a minimum. |
|
206 |
*} |
|
207 |
||
208 |
||
209 |
||
210 |
section {* Basics \label{sec:basics} *} |
|
20948 | 211 |
|
212 |
subsection {* Invoking the code generator *} |
|
213 |
||
21058 | 214 |
text {* |
22916 | 215 |
Thanks to a reasonable setup of the @{text HOL} theories, in |
21058 | 216 |
most cases code generation proceeds without further ado: |
217 |
*} |
|
218 |
||
25870 | 219 |
primrec |
22473 | 220 |
fac :: "nat \<Rightarrow> nat" where |
221 |
"fac 0 = 1" |
|
222 |
| "fac (Suc n) = Suc n * fac n" |
|
21058 | 223 |
|
224 |
text {* |
|
22550 | 225 |
\noindent This executable specification is now turned to SML code: |
21058 | 226 |
*} |
227 |
||
24348 | 228 |
export_code fac (*<*)in SML(*>*)in SML file "examples/fac.ML" |
21058 | 229 |
|
230 |
text {* |
|
24348 | 231 |
\noindent The @{text "\<EXPORTCODE>"} command takes a space-separated list of |
21058 | 232 |
constants together with \qn{serialization directives} |
22845 | 233 |
These start with a \qn{target language} |
234 |
identifier, followed by a file specification |
|
235 |
where to write the generated code to. |
|
21058 | 236 |
|
22060 | 237 |
Internally, the defining equations for all selected |
21178 | 238 |
constants are taken, including any transitively required |
21058 | 239 |
constants, datatypes and classes, resulting in the following |
240 |
code: |
|
241 |
||
242 |
\lstsml{Thy/examples/fac.ML} |
|
243 |
||
244 |
The code generator will complain when a required |
|
22550 | 245 |
ingredient does not provide a executable counterpart, |
246 |
e.g.~generating code |
|
21058 | 247 |
for constants not yielding |
22550 | 248 |
a defining equation (e.g.~the Hilbert choice |
249 |
operation @{text "SOME"}): |
|
21058 | 250 |
*} |
251 |
(*<*) |
|
252 |
setup {* Sign.add_path "foo" *} |
|
253 |
(*>*) |
|
254 |
definition |
|
21993 | 255 |
pick_some :: "'a list \<Rightarrow> 'a" where |
21058 | 256 |
"pick_some xs = (SOME x. x \<in> set xs)" |
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 |
(*>*) |
|
25870 | 266 |
|
24348 | 267 |
export_code pick_some in SML file "examples/fail_const.ML" |
21058 | 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 |
22751 | 283 |
shall not bother us for the moment). |
21058 | 284 |
|
22916 | 285 |
The typical @{text HOL} tools are already set up in a way that |
22751 | 286 |
function definitions introduced by @{text "\<DEFINITION>"}, |
25870 | 287 |
@{text "\<PRIMREC>"}, @{text "\<FUN>"}, |
288 |
@{text "\<FUNCTION>"}, @{text "\<CONSTDEFS>"}, |
|
21323 | 289 |
@{text "\<RECDEF>"} are implicitly propagated |
22060 | 290 |
to this defining equation table. Specific theorems may be |
21058 | 291 |
selected using an attribute: \emph{code func}. As example, |
292 |
a weight selector function: |
|
293 |
*} |
|
294 |
||
295 |
primrec |
|
25870 | 296 |
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a" where |
21058 | 297 |
"pick (x#xs) n = (let (k, v) = x in |
298 |
if n < k then v else pick xs (n - k))" |
|
299 |
||
300 |
text {* |
|
22798 | 301 |
\noindent We want to eliminate the explicit destruction |
21058 | 302 |
of @{term x} to @{term "(k, v)"}: |
303 |
*} |
|
304 |
||
305 |
lemma [code func]: |
|
306 |
"pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" |
|
307 |
by simp |
|
308 |
||
24348 | 309 |
export_code pick (*<*)in SML(*>*) in SML file "examples/pick1.ML" |
21058 | 310 |
|
311 |
text {* |
|
22798 | 312 |
\noindent This theorem now is used for generating code: |
21058 | 313 |
|
314 |
\lstsml{Thy/examples/pick1.ML} |
|
315 |
||
22798 | 316 |
\noindent It might be convenient to remove the pointless original |
22845 | 317 |
equation, using the \emph{func del} attribute: |
21058 | 318 |
*} |
319 |
||
22845 | 320 |
lemmas [code func del] = pick.simps |
21058 | 321 |
|
24348 | 322 |
export_code pick (*<*)in SML(*>*) in SML file "examples/pick2.ML" |
21058 | 323 |
|
324 |
text {* |
|
325 |
\lstsml{Thy/examples/pick2.ML} |
|
326 |
||
22798 | 327 |
\noindent Syntactic redundancies are implicitly dropped. For example, |
21058 | 328 |
using a modified version of the @{const fac} function |
22060 | 329 |
as defining equation, the then redundant (since |
330 |
syntactically subsumed) original defining equations |
|
21058 | 331 |
are dropped, resulting in a warning: |
332 |
*} |
|
333 |
||
334 |
lemma [code func]: |
|
335 |
"fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)" |
|
336 |
by (cases n) simp_all |
|
337 |
||
24348 | 338 |
export_code fac (*<*)in SML(*>*)in SML file "examples/fac_case.ML" |
21058 | 339 |
|
340 |
text {* |
|
341 |
\lstsml{Thy/examples/fac_case.ML} |
|
342 |
||
343 |
\begin{warn} |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
344 |
The attributes \emph{code} and \emph{code del} |
21058 | 345 |
associated with the existing code generator also apply to |
346 |
the new one: \emph{code} implies \emph{code func}, |
|
22845 | 347 |
and \emph{code del} implies \emph{code func del}. |
21058 | 348 |
\end{warn} |
349 |
*} |
|
20948 | 350 |
|
351 |
subsection {* Type classes *} |
|
352 |
||
21058 | 353 |
text {* |
354 |
Type classes enter the game via the Isar class package. |
|
21075 | 355 |
For a short introduction how to use it, see \cite{isabelle-classes}; |
21147 | 356 |
here we just illustrate its impact on code generation. |
21058 | 357 |
|
358 |
In a target language, type classes may be represented |
|
22798 | 359 |
natively (as in the case of Haskell). For languages |
21058 | 360 |
like SML, they are implemented using \emph{dictionaries}. |
21178 | 361 |
Our following example specifies a class \qt{null}, |
21058 | 362 |
assigning to each of its inhabitants a \qt{null} value: |
363 |
*} |
|
364 |
||
22473 | 365 |
class null = type + |
21058 | 366 |
fixes null :: 'a |
367 |
||
25870 | 368 |
primrec |
369 |
head :: "'a\<Colon>null list \<Rightarrow> 'a" where |
|
21058 | 370 |
"head [] = null" |
22798 | 371 |
| "head (x#xs) = x" |
21058 | 372 |
|
373 |
text {* |
|
25533 | 374 |
\noindent We provide some instances for our @{text null}: |
21058 | 375 |
*} |
376 |
||
25533 | 377 |
instantiation option and list :: (type) null |
378 |
begin |
|
379 |
||
380 |
definition |
|
381 |
"null = None" |
|
21058 | 382 |
|
25533 | 383 |
definition |
384 |
"null = []" |
|
385 |
||
386 |
instance .. |
|
387 |
||
388 |
end |
|
21058 | 389 |
|
390 |
text {* |
|
25533 | 391 |
\noindent Constructing a dummy example: |
21058 | 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 |
|
22845 | 403 |
the file system, with root directory given as file specification. |
21058 | 404 |
*} |
405 |
||
24348 | 406 |
export_code dummy in Haskell file "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} |
|
22798 | 412 |
\noindent (we have left out all other modules). |
21058 | 413 |
|
22798 | 414 |
\medskip |
21058 | 415 |
|
416 |
The whole code in SML with explicit dictionary passing: |
|
417 |
*} |
|
418 |
||
24348 | 419 |
export_code dummy (*<*)in SML(*>*)in SML file "examples/class.ML" |
21058 | 420 |
|
421 |
text {* |
|
422 |
\lstsml{Thy/examples/class.ML} |
|
423 |
||
22798 | 424 |
\medskip |
425 |
||
426 |
\noindent or in OCaml: |
|
22292
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 |
|
24348 | 429 |
export_code dummy in OCaml file "examples/class.ocaml" |
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
430 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
431 |
text {* |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
432 |
\lstsml{Thy/examples/class.ocaml} |
22798 | 433 |
|
434 |
\medskip The explicit association of constants |
|
435 |
to classes can be inspected using the @{text "\<PRINTCLASSES>"} |
|
22845 | 436 |
command. |
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
437 |
*} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
438 |
|
22550 | 439 |
|
21058 | 440 |
section {* Recipes and advanced topics \label{sec:advanced} *} |
441 |
||
21089 | 442 |
text {* |
443 |
In this tutorial, we do not attempt to give an exhaustive |
|
444 |
description of the code generator framework; instead, |
|
445 |
we cast a light on advanced topics by introducing |
|
446 |
them together with practically motivated examples. Concerning |
|
447 |
further reading, see |
|
448 |
||
449 |
\begin{itemize} |
|
450 |
||
451 |
\item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} |
|
452 |
for exhaustive syntax diagrams. |
|
24193 | 453 |
\item or \cite{Haftmann-Nipkow:2007:codegen} which deals with foundational issues |
21089 | 454 |
of the code generator framework. |
455 |
||
456 |
\end{itemize} |
|
457 |
*} |
|
21058 | 458 |
|
22798 | 459 |
subsection {* Library theories \label{sec:library} *} |
21058 | 460 |
|
21089 | 461 |
text {* |
22916 | 462 |
The @{text HOL} @{text Main} theory already provides a code |
463 |
generator setup |
|
21089 | 464 |
which should be suitable for most applications. Common extensions |
22916 | 465 |
and modifications are available by certain theories of the @{text HOL} |
21089 | 466 |
library; beside being useful in applications, they may serve |
21178 | 467 |
as a tutorial for customizing the code generator setup. |
21089 | 468 |
|
469 |
\begin{description} |
|
470 |
||
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
471 |
\item[@{text "Code_Integer"}] represents @{text HOL} integers by big |
22798 | 472 |
integer literals in target languages. |
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
473 |
\item[@{text "Code_Char"}] represents @{text HOL} characters by |
22798 | 474 |
character literals in target languages. |
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
475 |
\item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, |
22798 | 476 |
but also offers treatment of character codes; includes |
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
477 |
@{text "Code_Integer"}. |
23850 | 478 |
\item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers, |
21178 | 479 |
which in general will result in higher efficency; pattern |
25369
5200374fda5d
replaced @{const} (allows name only) by proper @{term};
wenzelm
parents:
24994
diff
changeset
|
480 |
matching with @{term "0\<Colon>nat"} / @{const "Suc"} |
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
481 |
is eliminated; includes @{text "Code_Integer"}. |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
482 |
\item[@{text "Code_Index"}] provides an additional datatype |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
483 |
@{text index} which is mapped to target-language built-in integers. |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
484 |
Useful for code setups which involve e.g. indexing of |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
485 |
target-language arrays. |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
486 |
\item[@{text "Code_Message"}] provides an additional datatype |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
487 |
@{text message_string} which is isomorphic to strings; |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
488 |
@{text message_string}s are mapped to target-language strings. |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24628
diff
changeset
|
489 |
Useful for code setups which involve e.g. printing (error) messages. |
21089 | 490 |
|
491 |
\end{description} |
|
22916 | 492 |
|
493 |
\begin{warn} |
|
494 |
When importing any of these theories, they should form the last |
|
495 |
items in an import list. Since these theories adapt the |
|
496 |
code generator setup in a non-conservative fashion, |
|
497 |
strange effects may occur otherwise. |
|
498 |
\end{warn} |
|
21089 | 499 |
*} |
500 |
||
20948 | 501 |
subsection {* Preprocessing *} |
502 |
||
21089 | 503 |
text {* |
21147 | 504 |
Before selected function theorems are turned into abstract |
505 |
code, a chain of definitional transformation steps is carried |
|
21178 | 506 |
out: \emph{preprocessing}. There are three possibilities |
21147 | 507 |
to customize preprocessing: \emph{inline theorems}, |
508 |
\emph{inline procedures} and \emph{generic preprocessors}. |
|
509 |
||
510 |
\emph{Inline theorems} are rewriting rules applied to each |
|
22060 | 511 |
defining equation. Due to the interpretation of theorems |
512 |
of defining equations, rewrites are applied to the right |
|
21147 | 513 |
hand side and the arguments of the left hand side of an |
514 |
equation, but never to the constant heading the left hand side. |
|
515 |
Inline theorems may be declared an undeclared using the |
|
22845 | 516 |
\emph{code inline} or \emph{code inline del} attribute respectively. |
21147 | 517 |
Some common applications: |
518 |
*} |
|
519 |
||
520 |
text_raw {* |
|
521 |
\begin{itemize} |
|
522 |
*} |
|
523 |
||
22845 | 524 |
text {* |
525 |
\item replacing non-executable constructs by executable ones: |
|
526 |
*} |
|
21147 | 527 |
|
22845 | 528 |
lemma [code inline]: |
529 |
"x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all |
|
530 |
||
531 |
text {* |
|
532 |
\item eliminating superfluous constants: |
|
21089 | 533 |
*} |
534 |
||
22845 | 535 |
lemma [code inline]: |
536 |
"1 = Suc 0" by simp |
|
537 |
||
538 |
text {* |
|
539 |
\item replacing executable but inconvenient constructs: |
|
540 |
*} |
|
541 |
||
542 |
lemma [code inline]: |
|
543 |
"xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all |
|
21147 | 544 |
|
545 |
text_raw {* |
|
546 |
\end{itemize} |
|
547 |
*} |
|
548 |
||
549 |
text {* |
|
22845 | 550 |
\noindent 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
|
551 |
the @{text "\<PRINTCODESETUP>"} command. |
21147 | 552 |
|
553 |
\emph{Inline procedures} are a generalized version of inline |
|
554 |
theorems written in ML -- rewrite rules are generated dependent |
|
555 |
on the function theorems for a certain function. One |
|
556 |
application is the implicit expanding of @{typ nat} numerals |
|
25369
5200374fda5d
replaced @{const} (allows name only) by proper @{term};
wenzelm
parents:
24994
diff
changeset
|
557 |
to @{term "0\<Colon>nat"} / @{const Suc} representation. See further |
21147 | 558 |
\secref{sec:ml} |
559 |
||
560 |
\emph{Generic preprocessors} provide a most general interface, |
|
561 |
transforming a list of function theorems to another |
|
562 |
list of function theorems, provided that neither the heading |
|
25369
5200374fda5d
replaced @{const} (allows name only) by proper @{term};
wenzelm
parents:
24994
diff
changeset
|
563 |
constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc} |
21323 | 564 |
pattern elimination implemented in |
21452 | 565 |
theory @{text "EfficientNat"} (\secref{eff_nat}) uses this |
21147 | 566 |
interface. |
567 |
||
568 |
\begin{warn} |
|
569 |
The order in which single preprocessing steps are carried |
|
570 |
out currently is not specified; in particular, preprocessing |
|
21178 | 571 |
is \emph{no} fix point process. Keep this in mind when |
21147 | 572 |
setting up the preprocessor. |
573 |
||
574 |
Further, the attribute \emph{code unfold} |
|
575 |
associated with the existing code generator also applies to |
|
576 |
the new one: \emph{code unfold} implies \emph{code inline}. |
|
577 |
\end{warn} |
|
578 |
*} |
|
20948 | 579 |
|
22798 | 580 |
|
581 |
subsection {* Concerning operational equality *} |
|
582 |
||
583 |
text {* |
|
584 |
Surely you have already noticed how equality is treated |
|
585 |
by the code generator: |
|
586 |
*} |
|
587 |
||
25870 | 588 |
primrec |
22798 | 589 |
collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
590 |
"collect_duplicates xs ys [] = xs" |
|
591 |
| "collect_duplicates xs ys (z#zs) = (if z \<in> set xs |
|
592 |
then if z \<in> set ys |
|
593 |
then collect_duplicates xs ys zs |
|
594 |
else collect_duplicates xs (z#ys) zs |
|
595 |
else collect_duplicates (z#xs) (z#ys) zs)" |
|
596 |
||
597 |
text {* |
|
598 |
The membership test during preprocessing is rewritten, |
|
23850 | 599 |
resulting in @{const List.member}, which itself |
22798 | 600 |
performs an explicit equality check. |
601 |
*} |
|
602 |
||
24348 | 603 |
export_code collect_duplicates (*<*)in SML(*>*)in SML file "examples/collect_duplicates.ML" |
22798 | 604 |
|
605 |
text {* |
|
606 |
\lstsml{Thy/examples/collect_duplicates.ML} |
|
607 |
*} |
|
608 |
||
609 |
text {* |
|
610 |
Obviously, polymorphic equality is implemented the Haskell |
|
26513 | 611 |
way using a type class. How is this achieved? HOL introduces |
612 |
an explicit class @{text eq} with a corresponding operation |
|
26732 | 613 |
@{const eq_class.eq} such that @{thm eq [no_vars]}. |
26513 | 614 |
The preprocessing framework does the rest. |
22798 | 615 |
For datatypes, instances of @{text eq} are implicitly derived |
26513 | 616 |
when possible. For other types, you may instantiate @{text eq} |
617 |
manually like any other type class. |
|
22798 | 618 |
|
619 |
Though this @{text eq} class is designed to get rarely in |
|
620 |
the way, a subtlety |
|
621 |
enters the stage when definitions of overloaded constants |
|
622 |
are dependent on operational equality. For example, let |
|
623 |
us define a lexicographic ordering on tuples: |
|
624 |
*} |
|
26513 | 625 |
|
25870 | 626 |
instantiation * :: (ord, ord) ord |
627 |
begin |
|
628 |
||
629 |
definition |
|
630 |
[code func del]: "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in |
|
631 |
x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))" |
|
22798 | 632 |
|
25870 | 633 |
definition |
634 |
[code func del]: "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in |
|
635 |
x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))" |
|
636 |
||
637 |
instance .. |
|
638 |
||
639 |
end |
|
22798 | 640 |
|
22845 | 641 |
lemma ord_prod [code func(*<*), code func del(*>*)]: |
22798 | 642 |
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)" |
643 |
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" |
|
644 |
unfolding less_prod_def less_eq_prod_def by simp_all |
|
645 |
||
646 |
text {* |
|
647 |
Then code generation will fail. Why? The definition |
|
25369
5200374fda5d
replaced @{const} (allows name only) by proper @{term};
wenzelm
parents:
24994
diff
changeset
|
648 |
of @{term "op \<le>"} depends on equality on both arguments, |
22798 | 649 |
which are polymorphic and impose an additional @{text eq} |
650 |
class constraint, thus violating the type discipline |
|
651 |
for class operations. |
|
652 |
||
653 |
The solution is to add @{text eq} explicitly to the first sort arguments in the |
|
654 |
code theorems: |
|
655 |
*} |
|
656 |
||
657 |
lemma ord_prod_code [code func]: |
|
658 |
"(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> |
|
659 |
x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)" |
|
660 |
"(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> |
|
661 |
x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" |
|
662 |
unfolding ord_prod by rule+ |
|
663 |
||
664 |
text {* |
|
665 |
\noindent Then code generation succeeds: |
|
666 |
*} |
|
667 |
||
24348 | 668 |
export_code "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
22845 | 669 |
(*<*)in SML(*>*)in SML file "examples/lexicographic.ML" |
22798 | 670 |
|
671 |
text {* |
|
672 |
\lstsml{Thy/examples/lexicographic.ML} |
|
673 |
*} |
|
674 |
||
675 |
text {* |
|
676 |
In general, code theorems for overloaded constants may have more |
|
677 |
restrictive sort constraints than the underlying instance relation |
|
678 |
between class and type constructor as long as the whole system of |
|
679 |
constraints is coregular; code theorems violating coregularity |
|
680 |
are rejected immediately. Consequently, it might be necessary |
|
681 |
to delete disturbing theorems in the code theorem table, |
|
682 |
as we have done here with the original definitions @{text less_prod_def} |
|
683 |
and @{text less_eq_prod_def}. |
|
22885 | 684 |
|
685 |
In some cases, the automatically derived defining equations |
|
686 |
for equality on a particular type may not be appropriate. |
|
687 |
As example, watch the following datatype representing |
|
23130 | 688 |
monomorphic parametric types (where type constructors |
689 |
are referred to by natural numbers): |
|
22798 | 690 |
*} |
691 |
||
23130 | 692 |
datatype monotype = Mono nat "monotype list" |
22885 | 693 |
(*<*) |
694 |
lemma monotype_eq: |
|
695 |
"Mono tyco1 typargs1 = Mono tyco2 typargs2 \<equiv> |
|
696 |
tyco1 = tyco2 \<and> typargs1 = typargs2" by simp |
|
697 |
(*>*) |
|
698 |
||
699 |
text {* |
|
700 |
Then code generation for SML would fail with a message |
|
701 |
that the generated code conains illegal mutual dependencies: |
|
23130 | 702 |
the theorem @{thm monotype_eq [no_vars]} already requires the |
22885 | 703 |
instance @{text "monotype \<Colon> eq"}, which itself requires |
23130 | 704 |
@{thm monotype_eq [no_vars]}; Haskell has no problem with mutually |
22885 | 705 |
recursive @{text instance} and @{text function} definitions, |
706 |
but the SML serializer does not support this. |
|
707 |
||
708 |
In such cases, you have to provide you own equality equations |
|
709 |
involving auxiliary constants. In our case, |
|
710 |
@{const [show_types] list_all2} can do the job: |
|
711 |
*} |
|
712 |
||
713 |
lemma monotype_eq_list_all2 [code func]: |
|
714 |
"Mono tyco1 typargs1 = Mono tyco2 typargs2 \<longleftrightarrow> |
|
715 |
tyco1 = tyco2 \<and> list_all2 (op =) typargs1 typargs2" |
|
716 |
by (simp add: list_all2_eq [symmetric]) |
|
717 |
||
718 |
text {* |
|
719 |
does not depend on instance @{text "monotype \<Colon> eq"}: |
|
720 |
*} |
|
721 |
||
24348 | 722 |
export_code "op = :: monotype \<Rightarrow> monotype \<Rightarrow> bool" |
22885 | 723 |
(*<*)in SML(*>*)in SML file "examples/monotype.ML" |
724 |
||
725 |
text {* |
|
726 |
\lstsml{Thy/examples/monotype.ML} |
|
727 |
*} |
|
22798 | 728 |
|
729 |
subsection {* Programs as sets of theorems *} |
|
730 |
||
731 |
text {* |
|
732 |
As told in \secref{sec:concept}, code generation is based |
|
733 |
on a structured collection of code theorems. |
|
734 |
For explorative purpose, this collection |
|
735 |
may be inspected using the @{text "\<CODETHMS>"} command: |
|
736 |
*} |
|
737 |
||
738 |
code_thms "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat" |
|
739 |
||
740 |
text {* |
|
741 |
\noindent prints a table with \emph{all} defining equations |
|
25369
5200374fda5d
replaced @{const} (allows name only) by proper @{term};
wenzelm
parents:
24994
diff
changeset
|
742 |
for @{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}, including |
22798 | 743 |
\emph{all} defining equations those equations depend |
744 |
on recursivly. @{text "\<CODETHMS>"} provides a convenient |
|
745 |
mechanism to inspect the impact of a preprocessor setup |
|
746 |
on defining equations. |
|
747 |
||
748 |
Similarly, the @{text "\<CODEDEPS>"} command shows a graph |
|
749 |
visualizing dependencies between defining equations. |
|
750 |
*} |
|
751 |
||
752 |
||
25411 | 753 |
subsection {* Constructor sets for datatypes *} |
754 |
||
755 |
text {* |
|
756 |
Conceptually, any datatype is spanned by a set of |
|
757 |
\emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} |
|
758 |
where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is excactly the set of \emph{all} |
|
759 |
type variables in @{text "\<tau>"}. The HOL datatype package |
|
760 |
by default registers any new datatype in the table |
|
761 |
of datatypes, which may be inspected using |
|
762 |
the @{text "\<PRINTCODESETUP>"} command. |
|
763 |
||
764 |
In some cases, it may be convenient to alter or |
|
26999 | 765 |
extend this table; as an example, we will develope an alternative |
766 |
representation of natural numbers as binary digits, whose |
|
767 |
size does increase logarithmically with its value, not linear |
|
768 |
\footnote{Indeed, the @{text "Efficient_Nat"} theory \ref{eff_nat} |
|
769 |
does something similar}. First, the digit representation: |
|
770 |
*} |
|
771 |
||
772 |
definition Dig0 :: "nat \<Rightarrow> nat" where |
|
773 |
"Dig0 n = 2 * n" |
|
774 |
||
775 |
definition Dig1 :: "nat \<Rightarrow> nat" where |
|
776 |
"Dig1 n = Suc (2 * n)" |
|
777 |
||
778 |
text {* |
|
779 |
\noindent We will use these two ">digits"< to represent natural numbers |
|
780 |
in binary digits, e.g.: |
|
781 |
*} |
|
782 |
||
783 |
lemma 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))" |
|
784 |
by (simp add: Dig0_def Dig1_def) |
|
785 |
||
786 |
text {* |
|
787 |
\noindent Of course we also have to provide proper code equations for |
|
788 |
the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}: |
|
26973 | 789 |
*} |
25411 | 790 |
|
26999 | 791 |
lemma plus_Dig [code func]: |
792 |
"0 + n = n" |
|
793 |
"m + 0 = m" |
|
794 |
"1 + Dig0 n = Dig1 n" |
|
795 |
"Dig0 m + 1 = Dig1 m" |
|
796 |
"1 + Dig1 n = Dig0 (n + 1)" |
|
797 |
"Dig1 m + 1 = Dig0 (m + 1)" |
|
798 |
"Dig0 m + Dig0 n = Dig0 (m + n)" |
|
799 |
"Dig0 m + Dig1 n = Dig1 (m + n)" |
|
800 |
"Dig1 m + Dig0 n = Dig1 (m + n)" |
|
801 |
"Dig1 m + Dig1 n = Dig0 (m + n + 1)" |
|
802 |
by (simp_all add: Dig0_def Dig1_def) |
|
803 |
||
804 |
text {* |
|
805 |
\noindent We then instruct the code generator to view @{term "0\<Colon>nat"}, |
|
806 |
@{term "1\<Colon>nat"}, @{term Dig0} and @{term Dig1} as |
|
807 |
datatype constructors: |
|
808 |
*} |
|
809 |
||
810 |
code_datatype "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1 |
|
25411 | 811 |
|
26999 | 812 |
text {* |
813 |
\noindent For the former constructor @{term Suc}, we provide a code |
|
814 |
equation and remove some parts of the default code generator setup |
|
815 |
which are an obstacle here: |
|
816 |
*} |
|
817 |
||
818 |
lemma Suc_Dig [code func]: |
|
819 |
"Suc n = n + 1" |
|
820 |
by simp |
|
25411 | 821 |
|
26999 | 822 |
declare One_nat_def [code inline del] |
823 |
declare add_Suc_shift [code func del] |
|
824 |
||
825 |
text {* |
|
826 |
\noindent This yields the following code: |
|
827 |
*} |
|
828 |
||
829 |
export_code "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (*<*)in SML(*>*) in SML file "examples/nat_binary.ML" |
|
830 |
||
831 |
text {* \lstsml{Thy/examples/nat_binary.ML} *} |
|
25411 | 832 |
|
833 |
text {* |
|
834 |
\medskip |
|
835 |
||
26999 | 836 |
From this example, it can be easily glimpsed that using own constructor sets |
837 |
is a little delicate since it changes the set of valid patterns for values |
|
838 |
of that type. Without going into much detail, here some practical hints: |
|
839 |
||
840 |
\begin{itemize} |
|
841 |
\item When changing the constuctor set for datatypes, take care to |
|
842 |
provide an alternative for the @{text case} combinator (e.g. by replacing |
|
843 |
it using the preprocessor). |
|
844 |
\item Values in the target language need not to be normalized -- different |
|
845 |
values in the target language may represent the same value in the |
|
846 |
logic (e.g. @{text "Dig1 0 = 1"}). |
|
847 |
\item Usually, a good methodology to deal with the subleties of pattern |
|
848 |
matching is to see the type as an abstract type: provide a set |
|
849 |
of operations which operate on the concrete representation of the type, |
|
850 |
and derive further operations by combinations of these primitive ones, |
|
851 |
without relying on a particular representation. |
|
852 |
\end{itemize} |
|
25411 | 853 |
*} |
854 |
||
26999 | 855 |
code_datatype %invisible "0::nat" Suc |
856 |
declare %invisible plus_Dig [code func del] |
|
857 |
declare %invisible One_nat_def [code inline] |
|
858 |
declare %invisible add_Suc_shift [code func] |
|
859 |
lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp |
|
860 |
||
25411 | 861 |
|
21058 | 862 |
subsection {* Customizing serialization *} |
20948 | 863 |
|
22798 | 864 |
subsubsection {* Basics *} |
865 |
||
21147 | 866 |
text {* |
867 |
Consider the following function and its corresponding |
|
868 |
SML code: |
|
869 |
*} |
|
870 |
||
25870 | 871 |
primrec |
21147 | 872 |
in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where |
873 |
"in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l" |
|
874 |
(*<*) |
|
21323 | 875 |
code_type %tt bool |
21147 | 876 |
(SML) |
21323 | 877 |
code_const %tt True and False and "op \<and>" and Not |
21147 | 878 |
(SML and and and) |
879 |
(*>*) |
|
24348 | 880 |
export_code in_interval (*<*)in SML(*>*)in SML file "examples/bool_literal.ML" |
21147 | 881 |
|
882 |
text {* |
|
21323 | 883 |
\lstsml{Thy/examples/bool_literal.ML} |
21147 | 884 |
|
22798 | 885 |
\noindent Though this is correct code, it is a little bit unsatisfactory: |
21147 | 886 |
boolean values and operators are materialized as distinguished |
887 |
entities with have nothing to do with the SML-builtin notion |
|
888 |
of \qt{bool}. This results in less readable code; |
|
889 |
additionally, eager evaluation may cause programs to |
|
890 |
loop or break which would perfectly terminate when |
|
891 |
the existing SML \qt{bool} would be used. To map |
|
892 |
the HOL \qt{bool} on SML \qt{bool}, we may use |
|
893 |
\qn{custom serializations}: |
|
894 |
*} |
|
895 |
||
21323 | 896 |
code_type %tt bool |
21147 | 897 |
(SML "bool") |
21323 | 898 |
code_const %tt True and False and "op \<and>" |
21147 | 899 |
(SML "true" and "false" and "_ andalso _") |
900 |
||
901 |
text {* |
|
21323 | 902 |
The @{text "\<CODETYPE>"} commad takes a type constructor |
21147 | 903 |
as arguments together with a list of custom serializations. |
904 |
Each custom serialization starts with a target language |
|
905 |
identifier followed by an expression, which during |
|
906 |
code serialization is inserted whenever the type constructor |
|
21323 | 907 |
would occur. For constants, @{text "\<CODECONST>"} implements |
908 |
the corresponding mechanism. Each ``@{verbatim "_"}'' in |
|
21147 | 909 |
a serialization expression is treated as a placeholder |
910 |
for the type constructor's (the constant's) arguments. |
|
911 |
*} |
|
912 |
||
24348 | 913 |
export_code in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML" |
21147 | 914 |
|
915 |
text {* |
|
21323 | 916 |
\lstsml{Thy/examples/bool_mlbool.ML} |
21147 | 917 |
|
22798 | 918 |
\noindent This still is not perfect: the parentheses |
21323 | 919 |
around the \qt{andalso} expression are superfluous. |
920 |
Though the serializer |
|
21147 | 921 |
by no means attempts to imitate the rich Isabelle syntax |
922 |
framework, it provides some common idioms, notably |
|
923 |
associative infixes with precedences which may be used here: |
|
924 |
*} |
|
925 |
||
21323 | 926 |
code_const %tt "op \<and>" |
21147 | 927 |
(SML infixl 1 "andalso") |
928 |
||
24348 | 929 |
export_code in_interval (*<*)in SML(*>*) in SML file "examples/bool_infix.ML" |
21147 | 930 |
|
931 |
text {* |
|
21323 | 932 |
\lstsml{Thy/examples/bool_infix.ML} |
21147 | 933 |
|
22798 | 934 |
\medskip |
935 |
||
21147 | 936 |
Next, we try to map HOL pairs to SML pairs, using the |
21323 | 937 |
infix ``@{verbatim "*"}'' type constructor and parentheses: |
21147 | 938 |
*} |
939 |
(*<*) |
|
940 |
code_type * |
|
941 |
(SML) |
|
942 |
code_const Pair |
|
943 |
(SML) |
|
944 |
(*>*) |
|
21323 | 945 |
code_type %tt * |
21147 | 946 |
(SML infix 2 "*") |
21323 | 947 |
code_const %tt Pair |
21147 | 948 |
(SML "!((_),/ (_))") |
949 |
||
950 |
text {* |
|
21323 | 951 |
The initial bang ``@{verbatim "!"}'' tells the serializer to never put |
21147 | 952 |
parentheses around the whole expression (they are already present), |
953 |
while the parentheses around argument place holders |
|
954 |
tell not to put parentheses around the arguments. |
|
21323 | 955 |
The slash ``@{verbatim "/"}'' (followed by arbitrary white space) |
21147 | 956 |
inserts a space which may be used as a break if necessary |
957 |
during pretty printing. |
|
958 |
||
22798 | 959 |
These examples give a glimpse what mechanisms |
21178 | 960 |
custom serializations provide; however their usage |
961 |
requires careful thinking in order not to introduce |
|
962 |
inconsistencies -- or, in other words: |
|
963 |
custom serializations are completely axiomatic. |
|
21147 | 964 |
|
21178 | 965 |
A further noteworthy details is that any special |
966 |
character in a custom serialization may be quoted |
|
21323 | 967 |
using ``@{verbatim "'"}''; thus, in |
968 |
``@{verbatim "fn '_ => _"}'' the first |
|
969 |
``@{verbatim "_"}'' is a proper underscore while the |
|
970 |
second ``@{verbatim "_"}'' is a placeholder. |
|
21147 | 971 |
|
21178 | 972 |
The HOL theories provide further |
25411 | 973 |
examples for custom serializations. |
21178 | 974 |
*} |
21147 | 975 |
|
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
976 |
|
21178 | 977 |
subsubsection {* Haskell serialization *} |
978 |
||
979 |
text {* |
|
980 |
For convenience, the default |
|
981 |
HOL setup for Haskell maps the @{text eq} class to |
|
982 |
its counterpart in Haskell, giving custom serializations |
|
21323 | 983 |
for the class (@{text "\<CODECLASS>"}) and its operation: |
21178 | 984 |
*} |
985 |
||
21323 | 986 |
code_class %tt eq |
22798 | 987 |
(Haskell "Eq" where "op =" \<equiv> "(==)") |
21178 | 988 |
|
22798 | 989 |
code_const %tt "op =" |
21178 | 990 |
(Haskell infixl 4 "==") |
991 |
||
992 |
text {* |
|
993 |
A problem now occurs whenever a type which |
|
994 |
is an instance of @{text eq} in HOL is mapped |
|
995 |
on a Haskell-builtin type which is also an instance |
|
996 |
of Haskell @{text Eq}: |
|
21147 | 997 |
*} |
998 |
||
21178 | 999 |
typedecl bar |
1000 |
||
26513 | 1001 |
instantiation bar :: eq |
1002 |
begin |
|
1003 |
||
26732 | 1004 |
definition "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y" |
26513 | 1005 |
|
1006 |
instance by default (simp add: eq_bar_def) |
|
1007 |
||
1008 |
end |
|
21178 | 1009 |
|
21323 | 1010 |
code_type %tt bar |
21178 | 1011 |
(Haskell "Integer") |
1012 |
||
1013 |
text {* |
|
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
1014 |
The code generator would produce |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
1015 |
an additional instance, which of course is rejected. |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
1016 |
To suppress this additional instance, use |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
1017 |
@{text "\<CODEINSTANCE>"}: |
21147 | 1018 |
*} |
1019 |
||
21323 | 1020 |
code_instance %tt bar :: eq |
21178 | 1021 |
(Haskell -) |
1022 |
||
1023 |
||
22798 | 1024 |
subsubsection {* Pretty printing *} |
21189 | 1025 |
|
1026 |
text {* |
|
22798 | 1027 |
The serializer provides ML interfaces to set up |
1028 |
pretty serializations for expressions like lists, numerals |
|
1029 |
and characters; these are |
|
1030 |
monolithic stubs and should only be used with the |
|
1031 |
theories introduces in \secref{sec:library}. |
|
21189 | 1032 |
*} |
1033 |
||
22550 | 1034 |
|
21189 | 1035 |
subsection {* Cyclic module dependencies *} |
21178 | 1036 |
|
21189 | 1037 |
text {* |
1038 |
Sometimes the awkward situation occurs that dependencies |
|
1039 |
between definitions introduce cyclic dependencies |
|
1040 |
between modules, which in the Haskell world leaves |
|
1041 |
you to the mercy of the Haskell implementation you are using, |
|
1042 |
while for SML code generation is not possible. |
|
21178 | 1043 |
|
21189 | 1044 |
A solution is to declare module names explicitly. |
1045 |
Let use assume the three cyclically dependent |
|
1046 |
modules are named \emph{A}, \emph{B} and \emph{C}. |
|
1047 |
Then, by stating |
|
1048 |
*} |
|
1049 |
||
1050 |
code_modulename SML |
|
1051 |
A ABC |
|
1052 |
B ABC |
|
1053 |
C ABC |
|
1054 |
||
1055 |
text {* |
|
1056 |
we explicitly map all those modules on \emph{ABC}, |
|
1057 |
resulting in an ad-hoc merge of this three modules |
|
1058 |
at serialization time. |
|
1059 |
*} |
|
21147 | 1060 |
|
22798 | 1061 |
subsection {* Incremental code generation *} |
1062 |
||
1063 |
text {* |
|
1064 |
Code generation is \emph{incremental}: theorems |
|
1065 |
and abstract intermediate code are cached and extended on demand. |
|
1066 |
The cache may be partially or fully dropped if the underlying |
|
1067 |
executable content of the theory changes. |
|
1068 |
Implementation of caching is supposed to transparently |
|
1069 |
hid away the details from the user. Anyway, caching |
|
1070 |
reaches the surface by using a slightly more general form |
|
1071 |
of the @{text "\<CODETHMS>"}, @{text "\<CODEDEPS>"} |
|
24348 | 1072 |
and @{text "\<EXPORTCODE>"} commands: the list of constants |
22798 | 1073 |
may be omitted. Then, all constants with code theorems |
1074 |
in the current cache are referred to. |
|
1075 |
*} |
|
1076 |
||
25411 | 1077 |
(*subsection {* Code generation and proof extraction *} |
21189 | 1078 |
|
1079 |
text {* |
|
24217 | 1080 |
\fixme |
25411 | 1081 |
*}*) |
21189 | 1082 |
|
20948 | 1083 |
|
21058 | 1084 |
section {* ML interfaces \label{sec:ml} *} |
20948 | 1085 |
|
21189 | 1086 |
text {* |
1087 |
Since the code generator framework not only aims to provide |
|
1088 |
a nice Isar interface but also to form a base for |
|
1089 |
code-generation-based applications, here a short |
|
1090 |
description of the most important ML interfaces. |
|
1091 |
*} |
|
1092 |
||
24217 | 1093 |
subsection {* Executable theory content: @{text Code} *} |
21147 | 1094 |
|
1095 |
text {* |
|
1096 |
This Pure module implements the core notions of |
|
1097 |
executable content of a theory. |
|
1098 |
*} |
|
1099 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1100 |
subsubsection {* Managing executable content *} |
20948 | 1101 |
|
21147 | 1102 |
text %mlref {* |
1103 |
\begin{mldecls} |
|
25369
5200374fda5d
replaced @{const} (allows name only) by proper @{term};
wenzelm
parents:
24994
diff
changeset
|
1104 |
@{index_ML Code.add_func: "thm -> theory -> theory"} \\ |
24217 | 1105 |
@{index_ML Code.del_func: "thm -> theory -> theory"} \\ |
24421 | 1106 |
@{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\ |
24217 | 1107 |
@{index_ML Code.add_inline: "thm -> theory -> theory"} \\ |
1108 |
@{index_ML Code.del_inline: "thm -> theory -> theory"} \\ |
|
1109 |
@{index_ML Code.add_inline_proc: "string * (theory -> cterm list -> thm list) |
|
21189 | 1110 |
-> theory -> theory"} \\ |
24217 | 1111 |
@{index_ML Code.del_inline_proc: "string -> theory -> theory"} \\ |
1112 |
@{index_ML Code.add_preproc: "string * (theory -> thm list -> thm list) |
|
21189 | 1113 |
-> theory -> theory"} \\ |
24217 | 1114 |
@{index_ML Code.del_preproc: "string -> theory -> theory"} \\ |
24421 | 1115 |
@{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ |
24217 | 1116 |
@{index_ML Code.get_datatype: "theory -> string |
22479 | 1117 |
-> (string * sort) list * (string * typ list) list"} \\ |
24421 | 1118 |
@{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"} |
21147 | 1119 |
\end{mldecls} |
1120 |
||
1121 |
\begin{description} |
|
1122 |
||
24217 | 1123 |
\item @{ML Code.add_func}~@{text "thm"}~@{text "thy"} adds function |
21189 | 1124 |
theorem @{text "thm"} to executable content. |
1125 |
||
24217 | 1126 |
\item @{ML Code.del_func}~@{text "thm"}~@{text "thy"} removes function |
21189 | 1127 |
theorem @{text "thm"} from executable content, if present. |
1128 |
||
24217 | 1129 |
\item @{ML Code.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds |
22060 | 1130 |
suspended defining equations @{text lthms} for constant |
21189 | 1131 |
@{text const} to executable content. |
1132 |
||
24217 | 1133 |
\item @{ML Code.add_inline}~@{text "thm"}~@{text "thy"} adds |
21223 | 1134 |
inlining theorem @{text thm} to executable content. |
21189 | 1135 |
|
24217 | 1136 |
\item @{ML Code.del_inline}~@{text "thm"}~@{text "thy"} remove |
21189 | 1137 |
inlining theorem @{text thm} from executable content, if present. |
1138 |
||
24217 | 1139 |
\item @{ML Code.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds |
22046 | 1140 |
inline procedure @{text f} (named @{text name}) to executable content; |
21189 | 1141 |
@{text f} is a computation of rewrite rules dependent on |
1142 |
the current theory context and the list of all arguments |
|
22060 | 1143 |
and right hand sides of the defining equations belonging |
21189 | 1144 |
to a certain function definition. |
1145 |
||
24217 | 1146 |
\item @{ML Code.del_inline_proc}~@{text "name"}~@{text "thy"} removes |
22046 | 1147 |
inline procedure named @{text name} from executable content. |
1148 |
||
24217 | 1149 |
\item @{ML Code.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds |
22046 | 1150 |
generic preprocessor @{text f} (named @{text name}) to executable content; |
22060 | 1151 |
@{text f} is a transformation of the defining equations belonging |
21189 | 1152 |
to a certain function definition, depending on the |
1153 |
current theory context. |
|
1154 |
||
24217 | 1155 |
\item @{ML Code.del_preproc}~@{text "name"}~@{text "thy"} removes |
22046 | 1156 |
generic preprcoessor named @{text name} from executable content. |
1157 |
||
24421 | 1158 |
\item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds |
1159 |
a datatype to executable content, with generation |
|
1160 |
set @{text cs}. |
|
21189 | 1161 |
|
24217 | 1162 |
\item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"} |
21189 | 1163 |
returns type constructor corresponding to |
1164 |
constructor @{text const}; returns @{text NONE} |
|
1165 |
if @{text const} is no constructor. |
|
21147 | 1166 |
|
1167 |
\end{description} |
|
1168 |
*} |
|
1169 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1170 |
subsection {* Auxiliary *} |
21147 | 1171 |
|
1172 |
text %mlref {* |
|
1173 |
\begin{mldecls} |
|
24421 | 1174 |
@{index_ML CodeUnit.read_const: "theory -> string -> string"} \\ |
26973 | 1175 |
@{index_ML CodeUnit.head_func: "thm -> string * ((string * sort) list * typ)"} \\ |
24217 | 1176 |
@{index_ML CodeUnit.rewrite_func: "thm list -> thm -> thm"} \\ |
21147 | 1177 |
\end{mldecls} |
21217 | 1178 |
|
1179 |
\begin{description} |
|
1180 |
||
24217 | 1181 |
\item @{ML CodeUnit.read_const}~@{text thy}~@{text s} |
21217 | 1182 |
reads a constant as a concrete term expression @{text s}. |
1183 |
||
24217 | 1184 |
\item @{ML CodeUnit.head_func}~@{text thm} |
22751 | 1185 |
extracts the constant and its type from a defining equation @{text thm}. |
21217 | 1186 |
|
24217 | 1187 |
\item @{ML CodeUnit.rewrite_func}~@{text rews}~@{text thm} |
22060 | 1188 |
rewrites a defining equation @{text thm} with a set of rewrite |
21217 | 1189 |
rules @{text rews}; only arguments and right hand side are rewritten, |
22060 | 1190 |
not the head of the defining equation. |
21217 | 1191 |
|
1192 |
\end{description} |
|
1193 |
||
21147 | 1194 |
*} |
20948 | 1195 |
|
1196 |
subsection {* Implementing code generator applications *} |
|
1197 |
||
21147 | 1198 |
text {* |
21217 | 1199 |
Implementing code generator applications on top |
1200 |
of the framework set out so far usually not only |
|
1201 |
involves using those primitive interfaces |
|
1202 |
but also storing code-dependent data and various |
|
1203 |
other things. |
|
1204 |
||
21147 | 1205 |
\begin{warn} |
1206 |
Some interfaces discussed here have not reached |
|
1207 |
a final state yet. |
|
1208 |
Changes likely to occur in future. |
|
1209 |
\end{warn} |
|
1210 |
*} |
|
1211 |
||
1212 |
subsubsection {* Data depending on the theory's executable content *} |
|
1213 |
||
21217 | 1214 |
text {* |
21452 | 1215 |
Due to incrementality of code generation, changes in the |
1216 |
theory's executable content have to be propagated in a |
|
1217 |
certain fashion. Additionally, such changes may occur |
|
1218 |
not only during theory extension but also during theory |
|
1219 |
merge, which is a little bit nasty from an implementation |
|
1220 |
point of view. The framework provides a solution |
|
1221 |
to this technical challenge by providing a functorial |
|
1222 |
data slot @{ML_functor CodeDataFun}; on instantiation |
|
1223 |
of this functor, the following types and operations |
|
1224 |
are required: |
|
1225 |
||
21217 | 1226 |
\medskip |
1227 |
\begin{tabular}{l} |
|
1228 |
@{text "type T"} \\ |
|
1229 |
@{text "val empty: T"} \\ |
|
1230 |
@{text "val merge: Pretty.pp \<rightarrow> T * T \<rightarrow> T"} \\ |
|
24217 | 1231 |
@{text "val purge: theory option \<rightarrow> CodeUnit.const list option \<rightarrow> T \<rightarrow> T"} |
21217 | 1232 |
\end{tabular} |
1233 |
||
21452 | 1234 |
\begin{description} |
1235 |
||
1236 |
\item @{text T} the type of data to store. |
|
1237 |
||
1238 |
\item @{text empty} initial (empty) data. |
|
1239 |
||
1240 |
\item @{text merge} merging two data slots. |
|
1241 |
||
22798 | 1242 |
\item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content; |
21452 | 1243 |
if possible, the current theory context is handed over |
1244 |
as argument @{text thy} (if there is no current theory context (e.g.~during |
|
22798 | 1245 |
theory merge, @{ML NONE}); @{text consts} indicates the kind |
21452 | 1246 |
of change: @{ML NONE} stands for a fundamental change |
22798 | 1247 |
which invalidates any existing code, @{text "SOME consts"} |
1248 |
hints that executable content for constants @{text consts} |
|
21452 | 1249 |
has changed. |
1250 |
||
1251 |
\end{description} |
|
1252 |
||
1253 |
An instance of @{ML_functor CodeDataFun} provides the following |
|
1254 |
interface: |
|
1255 |
||
21217 | 1256 |
\medskip |
1257 |
\begin{tabular}{l} |
|
1258 |
@{text "get: theory \<rightarrow> T"} \\ |
|
1259 |
@{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\ |
|
1260 |
@{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"} |
|
1261 |
\end{tabular} |
|
1262 |
||
1263 |
\begin{description} |
|
1264 |
||
21452 | 1265 |
\item @{text get} retrieval of the current data. |
1266 |
||
1267 |
\item @{text change} update of current data (cached!) |
|
1268 |
by giving a continuation. |
|
1269 |
||
1270 |
\item @{text change_yield} update with side result. |
|
21217 | 1271 |
|
1272 |
\end{description} |
|
1273 |
*} |
|
1274 |
||
24628 | 1275 |
(*subsubsection {* Datatype hooks *} |
21147 | 1276 |
|
21452 | 1277 |
text {* |
1278 |
Isabelle/HOL's datatype package provides a mechanism to |
|
1279 |
extend theories depending on datatype declarations: |
|
1280 |
\emph{datatype hooks}. For example, when declaring a new |
|
22060 | 1281 |
datatype, a hook proves defining equations for equality on |
21452 | 1282 |
that datatype (if possible). |
1283 |
*} |
|
1284 |
||
21217 | 1285 |
text %mlref {* |
1286 |
\begin{mldecls} |
|
21323 | 1287 |
@{index_ML_type DatatypeHooks.hook: "string list -> theory -> theory"} \\ |
21217 | 1288 |
@{index_ML DatatypeHooks.add: "DatatypeHooks.hook -> theory -> theory"} |
1289 |
\end{mldecls} |
|
21452 | 1290 |
|
1291 |
\begin{description} |
|
1292 |
||
1293 |
\item @{ML_type DatatypeHooks.hook} specifies the interface |
|
1294 |
of \emph{datatype hooks}: a theory update |
|
1295 |
depending on the list of newly introduced |
|
1296 |
datatype names. |
|
1297 |
||
1298 |
\item @{ML DatatypeHooks.add} adds a hook to the |
|
1299 |
chain of all hooks. |
|
1300 |
||
1301 |
\end{description} |
|
1302 |
*} |
|
1303 |
||
1304 |
subsubsection {* Trivial typedefs -- type copies *} |
|
1305 |
||
1306 |
text {* |
|
1307 |
Sometimes packages will introduce new types |
|
1308 |
as \emph{marked type copies} similar to Haskell's |
|
1309 |
@{text newtype} declaration (e.g. the HOL record package) |
|
1310 |
\emph{without} tinkering with the overhead of datatypes. |
|
1311 |
Technically, these type copies are trivial forms of typedefs. |
|
1312 |
Since these type copies in code generation view are nothing |
|
1313 |
else than datatypes, they have been given a own package |
|
1314 |
in order to faciliate code generation: |
|
21147 | 1315 |
*} |
21058 | 1316 |
|
21217 | 1317 |
text %mlref {* |
1318 |
\begin{mldecls} |
|
21452 | 1319 |
@{index_ML_type TypecopyPackage.info} \\ |
21217 | 1320 |
@{index_ML TypecopyPackage.add_typecopy: " |
1321 |
bstring * string list -> typ -> (bstring * bstring) option |
|
1322 |
-> theory -> (string * TypecopyPackage.info) * theory"} \\ |
|
1323 |
@{index_ML TypecopyPackage.get_typecopy_info: "theory |
|
1324 |
-> string -> TypecopyPackage.info option"} \\ |
|
1325 |
@{index_ML TypecopyPackage.get_spec: "theory -> string |
|
21452 | 1326 |
-> (string * sort) list * (string * typ list) list"} \\ |
1327 |
@{index_ML_type TypecopyPackage.hook: "string * TypecopyPackage.info -> theory -> theory"} \\ |
|
1328 |
@{index_ML TypecopyPackage.add_hook: |
|
1329 |
"TypecopyPackage.hook -> theory -> theory"} \\ |
|
21217 | 1330 |
\end{mldecls} |
21452 | 1331 |
|
1332 |
\begin{description} |
|
1333 |
||
1334 |
\item @{ML_type TypecopyPackage.info} a record containing |
|
1335 |
the specification and further data of a type copy. |
|
1336 |
||
1337 |
\item @{ML TypecopyPackage.add_typecopy} defines a new |
|
1338 |
type copy. |
|
1339 |
||
1340 |
\item @{ML TypecopyPackage.get_typecopy_info} retrieves |
|
1341 |
data of an existing type copy. |
|
1342 |
||
1343 |
\item @{ML TypecopyPackage.get_spec} retrieves datatype-like |
|
1344 |
specification of a type copy. |
|
1345 |
||
1346 |
\item @{ML_type TypecopyPackage.hook},~@{ML TypecopyPackage.add_hook} |
|
1347 |
provide a hook mechanism corresponding to the hook mechanism |
|
1348 |
on datatypes. |
|
1349 |
||
1350 |
\end{description} |
|
1351 |
*} |
|
1352 |
||
1353 |
subsubsection {* Unifying type copies and datatypes *} |
|
1354 |
||
1355 |
text {* |
|
1356 |
Since datatypes and type copies are mapped to the same concept (datatypes) |
|
1357 |
by code generation, the view on both is unified \qt{code types}: |
|
21217 | 1358 |
*} |
1359 |
||
1360 |
text %mlref {* |
|
1361 |
\begin{mldecls} |
|
21452 | 1362 |
@{index_ML_type DatatypeCodegen.hook: "(string * (bool * ((string * sort) list |
1363 |
* (string * typ list) list))) list |
|
21323 | 1364 |
-> theory -> theory"} \\ |
21217 | 1365 |
@{index_ML DatatypeCodegen.add_codetypes_hook_bootstrap: " |
1366 |
DatatypeCodegen.hook -> theory -> theory"} |
|
1367 |
\end{mldecls} |
|
1368 |
*} |
|
1369 |
||
21222 | 1370 |
text {* |
21452 | 1371 |
\begin{description} |
1372 |
||
1373 |
\item @{ML_type DatatypeCodegen.hook} specifies the code type hook |
|
1374 |
interface: a theory transformation depending on a list of |
|
1375 |
mutual recursive code types; each entry in the list |
|
1376 |
has the structure @{text "(name, (is_data, (vars, cons)))"} |
|
1377 |
where @{text name} is the name of the code type, @{text is_data} |
|
1378 |
is true iff @{text name} is a datatype rather then a type copy, |
|
1379 |
and @{text "(vars, cons)"} is the specification of the code type. |
|
1380 |
||
1381 |
\item @{ML DatatypeCodegen.add_codetypes_hook_bootstrap} adds a code |
|
1382 |
type hook; the hook is immediately processed for all already |
|
1383 |
existing datatypes, in blocks of mutual recursive datatypes, |
|
1384 |
where all datatypes a block depends on are processed before |
|
1385 |
the block. |
|
1386 |
||
1387 |
\end{description} |
|
24628 | 1388 |
*}*) |
21452 | 1389 |
|
24628 | 1390 |
text {* |
21452 | 1391 |
\emph{Happy proving, happy hacking!} |
21222 | 1392 |
*} |
21217 | 1393 |
|
20948 | 1394 |
end |