author | haftmann |
Thu, 26 Apr 2007 13:32:55 +0200 | |
changeset 22798 | e3962371f568 |
parent 22751 | 1bfd75c1f232 |
child 22845 | 5f9138bcb3d7 |
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 |
|
22798 | 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 |
setup {* Sign.add_path "foo" *} |
|
250 |
(*>*) |
|
251 |
definition |
|
21993 | 252 |
pick_some :: "'a list \<Rightarrow> 'a" where |
21058 | 253 |
"pick_some xs = (SOME x. x \<in> set xs)" |
254 |
(*<*) |
|
255 |
hide const pick_some |
|
256 |
||
257 |
setup {* Sign.parent_path *} |
|
258 |
||
259 |
definition |
|
21993 | 260 |
pick_some :: "'a list \<Rightarrow> 'a" where |
21058 | 261 |
"pick_some = hd" |
262 |
(*>*) |
|
263 |
code_gen pick_some (SML "examples/fail_const.ML") |
|
264 |
||
22550 | 265 |
text {* \noindent will fail. *} |
266 |
||
20948 | 267 |
subsection {* Theorem selection *} |
268 |
||
21058 | 269 |
text {* |
22060 | 270 |
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
|
271 |
using the @{text "\<PRINTCODESETUP>"} command: |
21058 | 272 |
*} |
273 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
274 |
print_codesetup |
21058 | 275 |
|
276 |
text {* |
|
277 |
\noindent which displays a table of constant with corresponding |
|
22060 | 278 |
defining equations (the additional stuff displayed |
22751 | 279 |
shall not bother us for the moment). |
21058 | 280 |
|
281 |
The typical HOL tools are already set up in a way that |
|
22751 | 282 |
function definitions introduced by @{text "\<DEFINITION>"}, |
283 |
@{text "\<FUN>"}, |
|
22798 | 284 |
@{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}, |
21323 | 285 |
@{text "\<RECDEF>"} are implicitly propagated |
22060 | 286 |
to this defining equation table. Specific theorems may be |
21058 | 287 |
selected using an attribute: \emph{code func}. As example, |
288 |
a weight selector function: |
|
289 |
*} |
|
290 |
||
291 |
consts |
|
292 |
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a" |
|
293 |
||
294 |
primrec |
|
295 |
"pick (x#xs) n = (let (k, v) = x in |
|
296 |
if n < k then v else pick xs (n - k))" |
|
297 |
||
298 |
text {* |
|
22798 | 299 |
\noindent We want to eliminate the explicit destruction |
21058 | 300 |
of @{term x} to @{term "(k, v)"}: |
301 |
*} |
|
302 |
||
303 |
lemma [code func]: |
|
304 |
"pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" |
|
305 |
by simp |
|
306 |
||
21545 | 307 |
code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML") |
21058 | 308 |
|
309 |
text {* |
|
22798 | 310 |
\noindent This theorem now is used for generating code: |
21058 | 311 |
|
312 |
\lstsml{Thy/examples/pick1.ML} |
|
313 |
||
22798 | 314 |
\noindent It might be convenient to remove the pointless original |
21058 | 315 |
equation, using the \emph{nofunc} attribute: |
316 |
*} |
|
317 |
||
318 |
lemmas [code nofunc] = pick.simps |
|
319 |
||
21545 | 320 |
code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick2.ML") |
21058 | 321 |
|
322 |
text {* |
|
323 |
\lstsml{Thy/examples/pick2.ML} |
|
324 |
||
22798 | 325 |
\noindent Syntactic redundancies are implicitly dropped. For example, |
21058 | 326 |
using a modified version of the @{const fac} function |
22060 | 327 |
as defining equation, the then redundant (since |
328 |
syntactically subsumed) original defining equations |
|
21058 | 329 |
are dropped, resulting in a warning: |
330 |
*} |
|
331 |
||
332 |
lemma [code func]: |
|
333 |
"fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)" |
|
334 |
by (cases n) simp_all |
|
335 |
||
21545 | 336 |
code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac_case.ML") |
21058 | 337 |
|
338 |
text {* |
|
339 |
\lstsml{Thy/examples/fac_case.ML} |
|
340 |
||
341 |
\begin{warn} |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
342 |
The attributes \emph{code} and \emph{code del} |
21058 | 343 |
associated with the existing code generator also apply to |
344 |
the new one: \emph{code} implies \emph{code func}, |
|
345 |
and \emph{code del} implies \emph{code nofunc}. |
|
346 |
\end{warn} |
|
347 |
*} |
|
20948 | 348 |
|
349 |
subsection {* Type classes *} |
|
350 |
||
21058 | 351 |
text {* |
352 |
Type classes enter the game via the Isar class package. |
|
21075 | 353 |
For a short introduction how to use it, see \cite{isabelle-classes}; |
21147 | 354 |
here we just illustrate its impact on code generation. |
21058 | 355 |
|
356 |
In a target language, type classes may be represented |
|
22798 | 357 |
natively (as in the case of Haskell). For languages |
21058 | 358 |
like SML, they are implemented using \emph{dictionaries}. |
21178 | 359 |
Our following example specifies a class \qt{null}, |
21058 | 360 |
assigning to each of its inhabitants a \qt{null} value: |
361 |
*} |
|
362 |
||
22473 | 363 |
class null = type + |
21058 | 364 |
fixes null :: 'a |
365 |
||
22798 | 366 |
fun |
21058 | 367 |
head :: "'a\<Colon>null list \<Rightarrow> 'a" |
22798 | 368 |
where |
21058 | 369 |
"head [] = null" |
22798 | 370 |
| "head (x#xs) = x" |
21058 | 371 |
|
372 |
text {* |
|
373 |
We provide some instances for our @{text null}: |
|
374 |
*} |
|
375 |
||
376 |
instance option :: (type) null |
|
377 |
"null \<equiv> None" .. |
|
378 |
||
379 |
instance list :: (type) null |
|
380 |
"null \<equiv> []" .. |
|
381 |
||
382 |
text {* |
|
383 |
Constructing a dummy example: |
|
384 |
*} |
|
385 |
||
386 |
definition |
|
387 |
"dummy = head [Some (Suc 0), None]" |
|
388 |
||
389 |
text {* |
|
21178 | 390 |
Type classes offer a suitable occasion to introduce |
21058 | 391 |
the Haskell serializer. Its usage is almost the same |
21075 | 392 |
as SML, but, in accordance with conventions |
393 |
some Haskell systems enforce, each module ends |
|
394 |
up in a single file. The module hierarchy is reflected in |
|
395 |
the file system, with root given by the user. |
|
21058 | 396 |
*} |
397 |
||
21075 | 398 |
code_gen dummy (Haskell "examples/") |
21147 | 399 |
(* NOTE: you may use Haskell only once in this document, otherwise |
400 |
you have to work in distinct subdirectories *) |
|
21058 | 401 |
|
402 |
text {* |
|
403 |
\lsthaskell{Thy/examples/Codegen.hs} |
|
22798 | 404 |
\noindent (we have left out all other modules). |
21058 | 405 |
|
22798 | 406 |
\medskip |
21058 | 407 |
|
408 |
The whole code in SML with explicit dictionary passing: |
|
409 |
*} |
|
410 |
||
21545 | 411 |
code_gen dummy (*<*)(SML #)(*>*)(SML "examples/class.ML") |
21058 | 412 |
|
413 |
text {* |
|
414 |
\lstsml{Thy/examples/class.ML} |
|
415 |
||
22798 | 416 |
\medskip |
417 |
||
418 |
\noindent or in OCaml: |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
419 |
*} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
420 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
421 |
code_gen dummy (OCaml "examples/class.ocaml") |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
422 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
423 |
text {* |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
424 |
\lstsml{Thy/examples/class.ocaml} |
22798 | 425 |
|
426 |
\medskip The explicit association of constants |
|
427 |
to classes can be inspected using the @{text "\<PRINTCLASSES>"} |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
428 |
*} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
429 |
|
22550 | 430 |
|
21058 | 431 |
section {* Recipes and advanced topics \label{sec:advanced} *} |
432 |
||
21089 | 433 |
text {* |
434 |
In this tutorial, we do not attempt to give an exhaustive |
|
435 |
description of the code generator framework; instead, |
|
436 |
we cast a light on advanced topics by introducing |
|
437 |
them together with practically motivated examples. Concerning |
|
438 |
further reading, see |
|
439 |
||
440 |
\begin{itemize} |
|
441 |
||
442 |
\item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} |
|
443 |
for exhaustive syntax diagrams. |
|
21222 | 444 |
\item or \fixme[ref] which deals with foundational issues |
21089 | 445 |
of the code generator framework. |
446 |
||
447 |
\end{itemize} |
|
448 |
*} |
|
21058 | 449 |
|
22798 | 450 |
subsection {* Library theories \label{sec:library} *} |
21058 | 451 |
|
21089 | 452 |
text {* |
453 |
The HOL \emph{Main} theory already provides a code generator setup |
|
454 |
which should be suitable for most applications. Common extensions |
|
455 |
and modifications are available by certain theories of the HOL |
|
456 |
library; beside being useful in applications, they may serve |
|
21178 | 457 |
as a tutorial for customizing the code generator setup. |
21089 | 458 |
|
459 |
\begin{description} |
|
460 |
||
22798 | 461 |
\item[@{text "Pretty_Int"}] represents HOL integers by big |
462 |
integer literals in target languages. |
|
463 |
\item[@{text "Pretty_Char"}] represents HOL characters by |
|
464 |
character literals in target languages. |
|
465 |
\item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char_chr"}, |
|
466 |
but also offers treatment of character codes; includes |
|
467 |
@{text "Pretty_Int"}. |
|
21452 | 468 |
\item[@{text "ExecutableSet"}] allows to generate code |
21089 | 469 |
for finite sets using lists. |
21452 | 470 |
\item[@{text "ExecutableRat"}] \label{exec_rat} implements rational |
21089 | 471 |
numbers as triples @{text "(sign, enumerator, denominator)"}. |
21452 | 472 |
\item[@{text "EfficientNat"}] \label{eff_nat} implements natural numbers by integers, |
21178 | 473 |
which in general will result in higher efficency; pattern |
21089 | 474 |
matching with @{const "0\<Colon>nat"} / @{const "Suc"} |
22798 | 475 |
is eliminated; includes @{text "Pretty_Int"}. |
21452 | 476 |
\item[@{text "MLString"}] provides an additional datatype @{text "mlstring"}; |
21089 | 477 |
in the HOL default setup, strings in HOL are mapped to list |
22798 | 478 |
of HOL characters in SML; values of type @{text "mlstring"} are |
21089 | 479 |
mapped to strings in SML. |
480 |
||
481 |
\end{description} |
|
482 |
*} |
|
483 |
||
20948 | 484 |
subsection {* Preprocessing *} |
485 |
||
21089 | 486 |
text {* |
21147 | 487 |
Before selected function theorems are turned into abstract |
488 |
code, a chain of definitional transformation steps is carried |
|
21178 | 489 |
out: \emph{preprocessing}. There are three possibilities |
21147 | 490 |
to customize preprocessing: \emph{inline theorems}, |
491 |
\emph{inline procedures} and \emph{generic preprocessors}. |
|
492 |
||
493 |
\emph{Inline theorems} are rewriting rules applied to each |
|
22060 | 494 |
defining equation. Due to the interpretation of theorems |
495 |
of defining equations, rewrites are applied to the right |
|
21147 | 496 |
hand side and the arguments of the left hand side of an |
497 |
equation, but never to the constant heading the left hand side. |
|
498 |
Inline theorems may be declared an undeclared using the |
|
21178 | 499 |
\emph{code inline} or \emph{code noinline} attribute respectively. |
21147 | 500 |
Some common applications: |
501 |
*} |
|
502 |
||
503 |
text_raw {* |
|
504 |
\begin{itemize} |
|
505 |
\item replacing non-executable constructs by executable ones: \\ |
|
506 |
*} |
|
507 |
||
508 |
lemma [code inline]: |
|
509 |
"x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all |
|
510 |
||
511 |
text_raw {* |
|
512 |
\item eliminating superfluous constants: \\ |
|
513 |
*} |
|
514 |
||
515 |
lemma [code inline]: |
|
516 |
"1 = Suc 0" by simp |
|
517 |
||
518 |
text_raw {* |
|
519 |
\item replacing executable but inconvenient constructs: \\ |
|
21089 | 520 |
*} |
521 |
||
21147 | 522 |
lemma [code inline]: |
523 |
"xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all |
|
524 |
||
525 |
text_raw {* |
|
526 |
\end{itemize} |
|
527 |
*} |
|
528 |
||
529 |
text {* |
|
530 |
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
|
531 |
the @{text "\<PRINTCODESETUP>"} command. |
21147 | 532 |
|
533 |
\emph{Inline procedures} are a generalized version of inline |
|
534 |
theorems written in ML -- rewrite rules are generated dependent |
|
535 |
on the function theorems for a certain function. One |
|
536 |
application is the implicit expanding of @{typ nat} numerals |
|
537 |
to @{const "0\<Colon>nat"} / @{const Suc} representation. See further |
|
538 |
\secref{sec:ml} |
|
539 |
||
540 |
\emph{Generic preprocessors} provide a most general interface, |
|
541 |
transforming a list of function theorems to another |
|
542 |
list of function theorems, provided that neither the heading |
|
543 |
constant nor its type change. The @{const "0\<Colon>nat"} / @{const Suc} |
|
21323 | 544 |
pattern elimination implemented in |
21452 | 545 |
theory @{text "EfficientNat"} (\secref{eff_nat}) uses this |
21147 | 546 |
interface. |
547 |
||
548 |
\begin{warn} |
|
549 |
The order in which single preprocessing steps are carried |
|
550 |
out currently is not specified; in particular, preprocessing |
|
21178 | 551 |
is \emph{no} fix point process. Keep this in mind when |
21147 | 552 |
setting up the preprocessor. |
553 |
||
554 |
Further, the attribute \emph{code unfold} |
|
555 |
associated with the existing code generator also applies to |
|
556 |
the new one: \emph{code unfold} implies \emph{code inline}. |
|
557 |
\end{warn} |
|
558 |
*} |
|
20948 | 559 |
|
22798 | 560 |
|
561 |
subsection {* Concerning operational equality *} |
|
562 |
||
563 |
text {* |
|
564 |
Surely you have already noticed how equality is treated |
|
565 |
by the code generator: |
|
566 |
*} |
|
567 |
||
568 |
fun |
|
569 |
collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
570 |
"collect_duplicates xs ys [] = xs" |
|
571 |
| "collect_duplicates xs ys (z#zs) = (if z \<in> set xs |
|
572 |
then if z \<in> set ys |
|
573 |
then collect_duplicates xs ys zs |
|
574 |
else collect_duplicates xs (z#ys) zs |
|
575 |
else collect_duplicates (z#xs) (z#ys) zs)" |
|
576 |
||
577 |
text {* |
|
578 |
The membership test during preprocessing is rewritten, |
|
579 |
resulting in @{const List.memberl}, which itself |
|
580 |
performs an explicit equality check. |
|
581 |
*} |
|
582 |
||
583 |
code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML") |
|
584 |
||
585 |
text {* |
|
586 |
\lstsml{Thy/examples/collect_duplicates.ML} |
|
587 |
*} |
|
588 |
||
589 |
text {* |
|
590 |
Obviously, polymorphic equality is implemented the Haskell |
|
591 |
way using a type class. How is this achieved? By an |
|
592 |
almost trivial definition in the HOL setup: |
|
593 |
*} |
|
594 |
(*<*) |
|
595 |
setup {* Sign.add_path "foo" *} |
|
596 |
consts "op =" :: "'a" |
|
597 |
(*>*) |
|
598 |
class eq (attach "op =") = type |
|
599 |
||
600 |
text {* |
|
601 |
This merely introduces a class @{text eq} with corresponding |
|
602 |
operation @{text "op ="}; |
|
603 |
the preprocessing framework does the rest. |
|
604 |
For datatypes, instances of @{text eq} are implicitly derived |
|
605 |
when possible. |
|
606 |
||
607 |
Though this @{text eq} class is designed to get rarely in |
|
608 |
the way, a subtlety |
|
609 |
enters the stage when definitions of overloaded constants |
|
610 |
are dependent on operational equality. For example, let |
|
611 |
us define a lexicographic ordering on tuples: |
|
612 |
*} |
|
613 |
(*<*) |
|
614 |
hide (open) "class" eq |
|
615 |
hide (open) const "op =" |
|
616 |
setup {* Sign.parent_path *} |
|
617 |
(*>*) |
|
618 |
instance * :: (ord, ord) ord |
|
619 |
less_prod_def: |
|
620 |
"p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in |
|
621 |
x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)" |
|
622 |
less_eq_prod_def: |
|
623 |
"p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in |
|
624 |
x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" .. |
|
625 |
||
626 |
lemmas [code nofunc] = less_prod_def less_eq_prod_def |
|
627 |
||
628 |
lemma ord_prod [code func(*<*), code nofunc(*>*)]: |
|
629 |
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)" |
|
630 |
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" |
|
631 |
unfolding less_prod_def less_eq_prod_def by simp_all |
|
632 |
||
633 |
text {* |
|
634 |
Then code generation will fail. Why? The definition |
|
635 |
of @{const "op \<le>"} depends on equality on both arguments, |
|
636 |
which are polymorphic and impose an additional @{text eq} |
|
637 |
class constraint, thus violating the type discipline |
|
638 |
for class operations. |
|
639 |
||
640 |
The solution is to add @{text eq} explicitly to the first sort arguments in the |
|
641 |
code theorems: |
|
642 |
*} |
|
643 |
||
644 |
lemma ord_prod_code [code func]: |
|
645 |
"(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> |
|
646 |
x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)" |
|
647 |
"(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> |
|
648 |
x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" |
|
649 |
unfolding ord_prod by rule+ |
|
650 |
||
651 |
text {* |
|
652 |
\noindent Then code generation succeeds: |
|
653 |
*} |
|
654 |
||
655 |
code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
|
656 |
(*<*)(SML #)(*>*)(SML "examples/lexicographic.ML") |
|
657 |
||
658 |
text {* |
|
659 |
\lstsml{Thy/examples/lexicographic.ML} |
|
660 |
*} |
|
661 |
||
662 |
text {* |
|
663 |
In general, code theorems for overloaded constants may have more |
|
664 |
restrictive sort constraints than the underlying instance relation |
|
665 |
between class and type constructor as long as the whole system of |
|
666 |
constraints is coregular; code theorems violating coregularity |
|
667 |
are rejected immediately. Consequently, it might be necessary |
|
668 |
to delete disturbing theorems in the code theorem table, |
|
669 |
as we have done here with the original definitions @{text less_prod_def} |
|
670 |
and @{text less_eq_prod_def}. |
|
671 |
*} |
|
672 |
||
673 |
||
674 |
subsection {* Programs as sets of theorems *} |
|
675 |
||
676 |
text {* |
|
677 |
As told in \secref{sec:concept}, code generation is based |
|
678 |
on a structured collection of code theorems. |
|
679 |
For explorative purpose, this collection |
|
680 |
may be inspected using the @{text "\<CODETHMS>"} command: |
|
681 |
*} |
|
682 |
||
683 |
code_thms "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat" |
|
684 |
||
685 |
text {* |
|
686 |
\noindent prints a table with \emph{all} defining equations |
|
687 |
for @{const "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}, including |
|
688 |
\emph{all} defining equations those equations depend |
|
689 |
on recursivly. @{text "\<CODETHMS>"} provides a convenient |
|
690 |
mechanism to inspect the impact of a preprocessor setup |
|
691 |
on defining equations. |
|
692 |
||
693 |
Similarly, the @{text "\<CODEDEPS>"} command shows a graph |
|
694 |
visualizing dependencies between defining equations. |
|
695 |
*} |
|
696 |
||
697 |
||
21058 | 698 |
subsection {* Customizing serialization *} |
20948 | 699 |
|
22798 | 700 |
subsubsection {* Basics *} |
701 |
||
21147 | 702 |
text {* |
703 |
Consider the following function and its corresponding |
|
704 |
SML code: |
|
705 |
*} |
|
706 |
||
707 |
fun |
|
708 |
in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
709 |
"in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l" |
|
710 |
(*<*) |
|
21323 | 711 |
code_type %tt bool |
21147 | 712 |
(SML) |
21323 | 713 |
code_const %tt True and False and "op \<and>" and Not |
21147 | 714 |
(SML and and and) |
715 |
(*>*) |
|
21545 | 716 |
code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML") |
21147 | 717 |
|
718 |
text {* |
|
21323 | 719 |
\lstsml{Thy/examples/bool_literal.ML} |
21147 | 720 |
|
22798 | 721 |
\noindent Though this is correct code, it is a little bit unsatisfactory: |
21147 | 722 |
boolean values and operators are materialized as distinguished |
723 |
entities with have nothing to do with the SML-builtin notion |
|
724 |
of \qt{bool}. This results in less readable code; |
|
725 |
additionally, eager evaluation may cause programs to |
|
726 |
loop or break which would perfectly terminate when |
|
727 |
the existing SML \qt{bool} would be used. To map |
|
728 |
the HOL \qt{bool} on SML \qt{bool}, we may use |
|
729 |
\qn{custom serializations}: |
|
730 |
*} |
|
731 |
||
21323 | 732 |
code_type %tt bool |
21147 | 733 |
(SML "bool") |
21323 | 734 |
code_const %tt True and False and "op \<and>" |
21147 | 735 |
(SML "true" and "false" and "_ andalso _") |
736 |
||
737 |
text {* |
|
21323 | 738 |
The @{text "\<CODETYPE>"} commad takes a type constructor |
21147 | 739 |
as arguments together with a list of custom serializations. |
740 |
Each custom serialization starts with a target language |
|
741 |
identifier followed by an expression, which during |
|
742 |
code serialization is inserted whenever the type constructor |
|
21323 | 743 |
would occur. For constants, @{text "\<CODECONST>"} implements |
744 |
the corresponding mechanism. Each ``@{verbatim "_"}'' in |
|
21147 | 745 |
a serialization expression is treated as a placeholder |
746 |
for the type constructor's (the constant's) arguments. |
|
747 |
*} |
|
748 |
||
749 |
code_reserved SML |
|
750 |
bool true false |
|
751 |
||
752 |
text {* |
|
753 |
To assert that the existing \qt{bool}, \qt{true} and \qt{false} |
|
21323 | 754 |
is not used for generated code, we use @{text "\<CODERESERVED>"}. |
21147 | 755 |
|
756 |
After this setup, code looks quite more readable: |
|
757 |
*} |
|
758 |
||
21545 | 759 |
code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_mlbool.ML") |
21147 | 760 |
|
761 |
text {* |
|
21323 | 762 |
\lstsml{Thy/examples/bool_mlbool.ML} |
21147 | 763 |
|
22798 | 764 |
\noindent This still is not perfect: the parentheses |
21323 | 765 |
around the \qt{andalso} expression are superfluous. |
766 |
Though the serializer |
|
21147 | 767 |
by no means attempts to imitate the rich Isabelle syntax |
768 |
framework, it provides some common idioms, notably |
|
769 |
associative infixes with precedences which may be used here: |
|
770 |
*} |
|
771 |
||
21323 | 772 |
code_const %tt "op \<and>" |
21147 | 773 |
(SML infixl 1 "andalso") |
774 |
||
21545 | 775 |
code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_infix.ML") |
21147 | 776 |
|
777 |
text {* |
|
21323 | 778 |
\lstsml{Thy/examples/bool_infix.ML} |
21147 | 779 |
|
22798 | 780 |
\medskip |
781 |
||
21147 | 782 |
Next, we try to map HOL pairs to SML pairs, using the |
21323 | 783 |
infix ``@{verbatim "*"}'' type constructor and parentheses: |
21147 | 784 |
*} |
785 |
(*<*) |
|
786 |
code_type * |
|
787 |
(SML) |
|
788 |
code_const Pair |
|
789 |
(SML) |
|
790 |
(*>*) |
|
21323 | 791 |
code_type %tt * |
21147 | 792 |
(SML infix 2 "*") |
21323 | 793 |
code_const %tt Pair |
21147 | 794 |
(SML "!((_),/ (_))") |
795 |
||
796 |
text {* |
|
21323 | 797 |
The initial bang ``@{verbatim "!"}'' tells the serializer to never put |
21147 | 798 |
parentheses around the whole expression (they are already present), |
799 |
while the parentheses around argument place holders |
|
800 |
tell not to put parentheses around the arguments. |
|
21323 | 801 |
The slash ``@{verbatim "/"}'' (followed by arbitrary white space) |
21147 | 802 |
inserts a space which may be used as a break if necessary |
803 |
during pretty printing. |
|
804 |
||
22798 | 805 |
These examples give a glimpse what mechanisms |
21178 | 806 |
custom serializations provide; however their usage |
807 |
requires careful thinking in order not to introduce |
|
808 |
inconsistencies -- or, in other words: |
|
809 |
custom serializations are completely axiomatic. |
|
21147 | 810 |
|
21178 | 811 |
A further noteworthy details is that any special |
812 |
character in a custom serialization may be quoted |
|
21323 | 813 |
using ``@{verbatim "'"}''; thus, in |
814 |
``@{verbatim "fn '_ => _"}'' the first |
|
815 |
``@{verbatim "_"}'' is a proper underscore while the |
|
816 |
second ``@{verbatim "_"}'' is a placeholder. |
|
21147 | 817 |
|
21178 | 818 |
The HOL theories provide further |
819 |
examples for custom serializations and form |
|
820 |
a recommended tutorial on how to use them properly. |
|
821 |
*} |
|
21147 | 822 |
|
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
823 |
|
21178 | 824 |
subsubsection {* Haskell serialization *} |
825 |
||
826 |
text {* |
|
827 |
For convenience, the default |
|
828 |
HOL setup for Haskell maps the @{text eq} class to |
|
829 |
its counterpart in Haskell, giving custom serializations |
|
21323 | 830 |
for the class (@{text "\<CODECLASS>"}) and its operation: |
21178 | 831 |
*} |
832 |
||
21323 | 833 |
code_class %tt eq |
22798 | 834 |
(Haskell "Eq" where "op =" \<equiv> "(==)") |
21178 | 835 |
|
22798 | 836 |
code_const %tt "op =" |
21178 | 837 |
(Haskell infixl 4 "==") |
838 |
||
839 |
text {* |
|
840 |
A problem now occurs whenever a type which |
|
841 |
is an instance of @{text eq} in HOL is mapped |
|
842 |
on a Haskell-builtin type which is also an instance |
|
843 |
of Haskell @{text Eq}: |
|
21147 | 844 |
*} |
845 |
||
21178 | 846 |
typedecl bar |
847 |
||
848 |
instance bar :: eq .. |
|
849 |
||
21323 | 850 |
code_type %tt bar |
21178 | 851 |
(Haskell "Integer") |
852 |
||
853 |
text {* |
|
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
854 |
The code generator would produce |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
855 |
an additional instance, which of course is rejected. |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
856 |
To suppress this additional instance, use |
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22175
diff
changeset
|
857 |
@{text "\<CODEINSTANCE>"}: |
21147 | 858 |
*} |
859 |
||
21323 | 860 |
code_instance %tt bar :: eq |
21178 | 861 |
(Haskell -) |
862 |
||
863 |
||
22798 | 864 |
subsubsection {* Pretty printing *} |
21189 | 865 |
|
866 |
text {* |
|
22798 | 867 |
The serializer provides ML interfaces to set up |
868 |
pretty serializations for expressions like lists, numerals |
|
869 |
and characters; these are |
|
870 |
monolithic stubs and should only be used with the |
|
871 |
theories introduces in \secref{sec:library}. |
|
21189 | 872 |
*} |
873 |
||
22550 | 874 |
subsection {* Constructor sets for datatypes *} |
875 |
||
876 |
text {* |
|
22798 | 877 |
Conceptually, any datatype is spanned by a set of |
878 |
\emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} |
|
879 |
where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is excactly the set of \emph{all} |
|
880 |
type variables in @{text "\<tau>"}. The HOL datatype package |
|
881 |
by default registers any new datatype in the table |
|
882 |
of datatypes, which may be inspected using |
|
883 |
the @{text "\<PRINTCODESETUP>"} command. |
|
884 |
||
885 |
In some cases, it may be convenient to alter or |
|
886 |
extend this table; as an example, we show |
|
887 |
how to implement finite sets by lists |
|
888 |
using the conversion @{term [source] "set \<Colon> 'a list \<Rightarrow> 'a set"} |
|
889 |
as constructor: |
|
22550 | 890 |
*} |
891 |
||
22798 | 892 |
code_datatype set |
893 |
||
894 |
lemma [code func]: "{} = set []" by simp |
|
895 |
||
896 |
lemma [code func]: "insert x (set xs) = set (x#xs)" by simp |
|
897 |
||
898 |
lemma [code func]: "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all |
|
899 |
||
900 |
lemma [code func]: "xs \<union> set ys = foldr insert ys xs" by (induct ys) simp_all |
|
901 |
||
902 |
lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all |
|
903 |
||
904 |
code_gen "{}" insert "op \<in>" "op \<union>" "Union" (*<*)(SML #)(*>*)(SML "examples/set_list.ML") |
|
905 |
||
906 |
text {* |
|
907 |
\lstsml{Thy/examples/set_list.ML} |
|
908 |
||
909 |
\medskip |
|
910 |
||
911 |
Changing the representation of existing datatypes requires |
|
912 |
some care with respect to pattern matching and such. |
|
913 |
*} |
|
22550 | 914 |
|
21189 | 915 |
subsection {* Cyclic module dependencies *} |
21178 | 916 |
|
21189 | 917 |
text {* |
918 |
Sometimes the awkward situation occurs that dependencies |
|
919 |
between definitions introduce cyclic dependencies |
|
920 |
between modules, which in the Haskell world leaves |
|
921 |
you to the mercy of the Haskell implementation you are using, |
|
922 |
while for SML code generation is not possible. |
|
21178 | 923 |
|
21189 | 924 |
A solution is to declare module names explicitly. |
925 |
Let use assume the three cyclically dependent |
|
926 |
modules are named \emph{A}, \emph{B} and \emph{C}. |
|
927 |
Then, by stating |
|
928 |
*} |
|
929 |
||
930 |
code_modulename SML |
|
931 |
A ABC |
|
932 |
B ABC |
|
933 |
C ABC |
|
934 |
||
935 |
text {* |
|
936 |
we explicitly map all those modules on \emph{ABC}, |
|
937 |
resulting in an ad-hoc merge of this three modules |
|
938 |
at serialization time. |
|
939 |
*} |
|
21147 | 940 |
|
22798 | 941 |
subsection {* Incremental code generation *} |
942 |
||
943 |
text {* |
|
944 |
Code generation is \emph{incremental}: theorems |
|
945 |
and abstract intermediate code are cached and extended on demand. |
|
946 |
The cache may be partially or fully dropped if the underlying |
|
947 |
executable content of the theory changes. |
|
948 |
Implementation of caching is supposed to transparently |
|
949 |
hid away the details from the user. Anyway, caching |
|
950 |
reaches the surface by using a slightly more general form |
|
951 |
of the @{text "\<CODETHMS>"}, @{text "\<CODEDEPS>"} |
|
952 |
and @{text "\<CODEGEN>"} commands: the list of constants |
|
953 |
may be omitted. Then, all constants with code theorems |
|
954 |
in the current cache are referred to. |
|
955 |
*} |
|
956 |
||
21147 | 957 |
subsection {* Axiomatic extensions *} |
958 |
||
959 |
text {* |
|
960 |
\begin{warn} |
|
961 |
The extensions introduced in this section, though working |
|
21189 | 962 |
in practice, are not the cream of the crop, as you |
963 |
will notice during reading. They will |
|
21147 | 964 |
eventually be replaced by more mature approaches. |
965 |
\end{warn} |
|
21189 | 966 |
|
967 |
Sometimes equalities are taken for granted which are |
|
968 |
not derivable inside the HOL logic but are silently assumed |
|
969 |
to hold for executable code. For example, we may want |
|
970 |
to identify the famous HOL constant @{const arbitrary} |
|
971 |
of type @{typ "'a option"} with @{const None}. |
|
972 |
By brute force: |
|
973 |
*} |
|
974 |
||
21323 | 975 |
axiomatization where |
976 |
"arbitrary = None" |
|
21189 | 977 |
|
978 |
text {* |
|
979 |
However this has to be considered harmful since this axiom, |
|
980 |
though probably justifiable for generated code, could |
|
981 |
introduce serious inconsistencies into the logic. |
|
982 |
||
983 |
So, there is a distinguished construct for stating axiomatic |
|
984 |
equalities of constants which apply only for code generation. |
|
985 |
Before introducing this, here is a convenient place to describe |
|
986 |
shortly how to deal with some restrictions the type discipline |
|
987 |
imposes. |
|
988 |
||
989 |
By itself, the constant @{const arbitrary} is a non-overloaded |
|
990 |
polymorphic constant. So, there is no way to distinguish |
|
991 |
different versions of @{const arbitrary} for different types |
|
992 |
inside the code generator framework. However, inlining |
|
993 |
theorems together with auxiliary constants provide a solution: |
|
21147 | 994 |
*} |
995 |
||
21189 | 996 |
definition |
21993 | 997 |
arbitrary_option :: "'a option" where |
21189 | 998 |
[symmetric, code inline]: "arbitrary_option = arbitrary" |
999 |
||
1000 |
text {* |
|
1001 |
By that, we replace any @{const arbitrary} with option type |
|
22060 | 1002 |
by @{const arbitrary_option} in defining equations. |
21189 | 1003 |
|
1004 |
For technical reasons, we further have to provide a |
|
1005 |
synonym for @{const None} which in code generator view |
|
22175 | 1006 |
is a function rather than a term constructor: |
21189 | 1007 |
*} |
1008 |
||
1009 |
definition |
|
1010 |
"None' = None" |
|
1011 |
||
1012 |
text {* |
|
21323 | 1013 |
Then finally we are enabled to use @{text "\<CODEAXIOMS>"}: |
21189 | 1014 |
*} |
1015 |
||
1016 |
code_axioms |
|
1017 |
arbitrary_option \<equiv> None' |
|
1018 |
||
1019 |
text {* |
|
1020 |
A dummy example: |
|
1021 |
*} |
|
1022 |
||
1023 |
fun |
|
1024 |
dummy_option :: "'a list \<Rightarrow> 'a option" where |
|
22473 | 1025 |
"dummy_option (x#xs) = Some x" |
1026 |
| "dummy_option [] = arbitrary" |
|
21189 | 1027 |
|
21545 | 1028 |
code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML") |
21189 | 1029 |
|
1030 |
text {* |
|
1031 |
\lstsml{Thy/examples/arbitrary.ML} |
|
1032 |
||
22798 | 1033 |
\medskip |
1034 |
||
21189 | 1035 |
Another axiomatic extension is code generation |
1036 |
for abstracted types. For this, the |
|
21452 | 1037 |
@{text "ExecutableRat"} (see \secref{exec_rat}) |
21189 | 1038 |
forms a good example. |
1039 |
*} |
|
1040 |
||
20948 | 1041 |
|
21058 | 1042 |
section {* ML interfaces \label{sec:ml} *} |
20948 | 1043 |
|
21189 | 1044 |
text {* |
1045 |
Since the code generator framework not only aims to provide |
|
1046 |
a nice Isar interface but also to form a base for |
|
1047 |
code-generation-based applications, here a short |
|
1048 |
description of the most important ML interfaces. |
|
1049 |
*} |
|
1050 |
||
21147 | 1051 |
subsection {* Constants with type discipline: codegen\_consts.ML *} |
1052 |
||
21189 | 1053 |
text {* |
1054 |
This Pure module manages identification of (probably overloaded) |
|
1055 |
constants by unique identifiers. |
|
1056 |
*} |
|
1057 |
||
21147 | 1058 |
text %mlref {* |
1059 |
\begin{mldecls} |
|
22550 | 1060 |
@{index_ML_type CodegenConsts.const: "string * string option"} \\ |
1061 |
@{index_ML CodegenConsts.const_of_cexpr: "theory -> string * typ -> CodegenConsts.const"} \\ |
|
21189 | 1062 |
\end{mldecls} |
1063 |
||
1064 |
\begin{description} |
|
1065 |
||
1066 |
\item @{ML_type CodegenConsts.const} is the identifier type: |
|
1067 |
the product of a \emph{string} with a list of \emph{typs}. |
|
1068 |
The \emph{string} is the constant name as represented inside Isabelle; |
|
22550 | 1069 |
for overloaded constants, the attached \emph{string option} |
1070 |
is either @{text SOME} type constructor denoting an instance, |
|
1071 |
or @{text NONE} for the polymorphic constant. |
|
21189 | 1072 |
|
22550 | 1073 |
\item @{ML CodegenConsts.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"} |
1074 |
maps a constant expression @{text "(constname, typ)"} |
|
1075 |
to its canonical identifier. |
|
21189 | 1076 |
|
1077 |
\end{description} |
|
21147 | 1078 |
*} |
1079 |
||
1080 |
subsection {* Executable theory content: codegen\_data.ML *} |
|
1081 |
||
1082 |
text {* |
|
1083 |
This Pure module implements the core notions of |
|
1084 |
executable content of a theory. |
|
1085 |
*} |
|
1086 |
||
1087 |
subsubsection {* Suspended theorems *} |
|
1088 |
||
1089 |
text %mlref {* |
|
1090 |
\begin{mldecls} |
|
22751 | 1091 |
@{index_ML CodegenData.lazy_thms: "(unit -> thm list) -> thm list Susp.T"} |
21147 | 1092 |
\end{mldecls} |
21189 | 1093 |
|
1094 |
\begin{description} |
|
1095 |
||
22751 | 1096 |
\item @{ML CodegenData.lazy_thms}~@{text f} turns an abstract |
21323 | 1097 |
theorem computation @{text f} into a suspension of theorems. |
21189 | 1098 |
|
1099 |
\end{description} |
|
21147 | 1100 |
*} |
1101 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1102 |
subsubsection {* Managing executable content *} |
20948 | 1103 |
|
21147 | 1104 |
text %mlref {* |
1105 |
\begin{mldecls} |
|
22550 | 1106 |
@{index_ML CodegenData.add_func: "bool -> thm -> theory -> theory"} \\ |
21147 | 1107 |
@{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\ |
21341 | 1108 |
@{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\ |
21147 | 1109 |
@{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\ |
1110 |
@{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\ |
|
22046 | 1111 |
@{index_ML CodegenData.add_inline_proc: "string * (theory -> cterm list -> thm list) |
21189 | 1112 |
-> theory -> theory"} \\ |
22046 | 1113 |
@{index_ML CodegenData.del_inline_proc: "string -> theory -> theory"} \\ |
1114 |
@{index_ML CodegenData.add_preproc: "string * (theory -> thm list -> thm list) |
|
21189 | 1115 |
-> theory -> theory"} \\ |
22046 | 1116 |
@{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\ |
22423 | 1117 |
@{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list) |
1118 |
-> theory -> theory"} \\ |
|
21189 | 1119 |
@{index_ML CodegenData.get_datatype: "theory -> string |
22479 | 1120 |
-> (string * sort) list * (string * typ list) list"} \\ |
21147 | 1121 |
@{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"} |
1122 |
\end{mldecls} |
|
1123 |
||
1124 |
\begin{description} |
|
1125 |
||
21189 | 1126 |
\item @{ML CodegenData.add_func}~@{text "thm"}~@{text "thy"} adds function |
1127 |
theorem @{text "thm"} to executable content. |
|
1128 |
||
1129 |
\item @{ML CodegenData.del_func}~@{text "thm"}~@{text "thy"} removes function |
|
1130 |
theorem @{text "thm"} from executable content, if present. |
|
1131 |
||
1132 |
\item @{ML CodegenData.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds |
|
22060 | 1133 |
suspended defining equations @{text lthms} for constant |
21189 | 1134 |
@{text const} to executable content. |
1135 |
||
1136 |
\item @{ML CodegenData.add_inline}~@{text "thm"}~@{text "thy"} adds |
|
21223 | 1137 |
inlining theorem @{text thm} to executable content. |
21189 | 1138 |
|
1139 |
\item @{ML CodegenData.del_inline}~@{text "thm"}~@{text "thy"} remove |
|
1140 |
inlining theorem @{text thm} from executable content, if present. |
|
1141 |
||
22046 | 1142 |
\item @{ML CodegenData.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds |
1143 |
inline procedure @{text f} (named @{text name}) to executable content; |
|
21189 | 1144 |
@{text f} is a computation of rewrite rules dependent on |
1145 |
the current theory context and the list of all arguments |
|
22060 | 1146 |
and right hand sides of the defining equations belonging |
21189 | 1147 |
to a certain function definition. |
1148 |
||
22046 | 1149 |
\item @{ML CodegenData.del_inline_proc}~@{text "name"}~@{text "thy"} removes |
1150 |
inline procedure named @{text name} from executable content. |
|
1151 |
||
1152 |
\item @{ML CodegenData.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds |
|
1153 |
generic preprocessor @{text f} (named @{text name}) to executable content; |
|
22060 | 1154 |
@{text f} is a transformation of the defining equations belonging |
21189 | 1155 |
to a certain function definition, depending on the |
1156 |
current theory context. |
|
1157 |
||
22060 | 1158 |
\item @{ML CodegenData.del_preproc}~@{text "name"}~@{text "thy"} removes |
22046 | 1159 |
generic preprcoessor named @{text name} from executable content. |
1160 |
||
22423 | 1161 |
\item @{ML CodegenData.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds |
21189 | 1162 |
a datatype to executable content, with type constructor |
1163 |
@{text name} and specification @{text spec}; @{text spec} is |
|
1164 |
a pair consisting of a list of type variable with sort |
|
21223 | 1165 |
constraints and a list of constructors with name |
22423 | 1166 |
and types of arguments. |
21189 | 1167 |
|
1168 |
\item @{ML CodegenData.get_datatype_of_constr}~@{text "thy"}~@{text "const"} |
|
1169 |
returns type constructor corresponding to |
|
1170 |
constructor @{text const}; returns @{text NONE} |
|
1171 |
if @{text const} is no constructor. |
|
21147 | 1172 |
|
1173 |
\end{description} |
|
1174 |
*} |
|
1175 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1176 |
subsection {* Auxiliary *} |
21147 | 1177 |
|
1178 |
text %mlref {* |
|
1179 |
\begin{mldecls} |
|
1180 |
@{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\ |
|
1181 |
@{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\ |
|
1182 |
@{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\ |
|
1183 |
@{index_ML_structure CodegenConsts.Consttab} \\ |
|
22751 | 1184 |
@{index_ML CodegenFunc.head_func: "thm -> CodegenConsts.const * typ"} \\ |
22060 | 1185 |
@{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\ |
21147 | 1186 |
\end{mldecls} |
21217 | 1187 |
|
1188 |
\begin{description} |
|
1189 |
||
1190 |
\item @{ML CodegenConsts.const_ord},~@{ML CodegenConsts.eq_const} |
|
1191 |
provide order and equality on constant identifiers. |
|
1192 |
||
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1193 |
\item @{ML_struct CodegenConsts.Consttab} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1194 |
provides table structures with constant identifiers as keys. |
21217 | 1195 |
|
1196 |
\item @{ML CodegenConsts.read_const}~@{text thy}~@{text s} |
|
1197 |
reads a constant as a concrete term expression @{text s}. |
|
1198 |
||
22751 | 1199 |
\item @{ML CodegenFunc.head_func}~@{text thm} |
1200 |
extracts the constant and its type from a defining equation @{text thm}. |
|
21217 | 1201 |
|
22060 | 1202 |
\item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm} |
1203 |
rewrites a defining equation @{text thm} with a set of rewrite |
|
21217 | 1204 |
rules @{text rews}; only arguments and right hand side are rewritten, |
22060 | 1205 |
not the head of the defining equation. |
21217 | 1206 |
|
1207 |
\end{description} |
|
1208 |
||
21147 | 1209 |
*} |
20948 | 1210 |
|
1211 |
subsection {* Implementing code generator applications *} |
|
1212 |
||
21147 | 1213 |
text {* |
21217 | 1214 |
Implementing code generator applications on top |
1215 |
of the framework set out so far usually not only |
|
1216 |
involves using those primitive interfaces |
|
1217 |
but also storing code-dependent data and various |
|
1218 |
other things. |
|
1219 |
||
21147 | 1220 |
\begin{warn} |
1221 |
Some interfaces discussed here have not reached |
|
1222 |
a final state yet. |
|
1223 |
Changes likely to occur in future. |
|
1224 |
\end{warn} |
|
1225 |
*} |
|
1226 |
||
1227 |
subsubsection {* Data depending on the theory's executable content *} |
|
1228 |
||
21217 | 1229 |
text {* |
21452 | 1230 |
Due to incrementality of code generation, changes in the |
1231 |
theory's executable content have to be propagated in a |
|
1232 |
certain fashion. Additionally, such changes may occur |
|
1233 |
not only during theory extension but also during theory |
|
1234 |
merge, which is a little bit nasty from an implementation |
|
1235 |
point of view. The framework provides a solution |
|
1236 |
to this technical challenge by providing a functorial |
|
1237 |
data slot @{ML_functor CodeDataFun}; on instantiation |
|
1238 |
of this functor, the following types and operations |
|
1239 |
are required: |
|
1240 |
||
21217 | 1241 |
\medskip |
1242 |
\begin{tabular}{l} |
|
1243 |
@{text "val name: string"} \\ |
|
1244 |
@{text "type T"} \\ |
|
1245 |
@{text "val empty: T"} \\ |
|
1246 |
@{text "val merge: Pretty.pp \<rightarrow> T * T \<rightarrow> T"} \\ |
|
1247 |
@{text "val purge: theory option \<rightarrow> CodegenConsts.const list option \<rightarrow> T \<rightarrow> T"} |
|
1248 |
\end{tabular} |
|
1249 |
||
21452 | 1250 |
\begin{description} |
1251 |
||
1252 |
\item @{text name} is a system-wide unique name identifying the data. |
|
1253 |
||
1254 |
\item @{text T} the type of data to store. |
|
1255 |
||
1256 |
\item @{text empty} initial (empty) data. |
|
1257 |
||
1258 |
\item @{text merge} merging two data slots. |
|
1259 |
||
22798 | 1260 |
\item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content; |
21452 | 1261 |
if possible, the current theory context is handed over |
1262 |
as argument @{text thy} (if there is no current theory context (e.g.~during |
|
22798 | 1263 |
theory merge, @{ML NONE}); @{text consts} indicates the kind |
21452 | 1264 |
of change: @{ML NONE} stands for a fundamental change |
22798 | 1265 |
which invalidates any existing code, @{text "SOME consts"} |
1266 |
hints that executable content for constants @{text consts} |
|
21452 | 1267 |
has changed. |
1268 |
||
1269 |
\end{description} |
|
1270 |
||
1271 |
An instance of @{ML_functor CodeDataFun} provides the following |
|
1272 |
interface: |
|
1273 |
||
21217 | 1274 |
\medskip |
1275 |
\begin{tabular}{l} |
|
1276 |
@{text "init: theory \<rightarrow> theory"} \\ |
|
1277 |
@{text "get: theory \<rightarrow> T"} \\ |
|
1278 |
@{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\ |
|
1279 |
@{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"} |
|
1280 |
\end{tabular} |
|
1281 |
||
1282 |
\begin{description} |
|
1283 |
||
21452 | 1284 |
\item @{text init} initialization during theory setup. |
1285 |
||
1286 |
\item @{text get} retrieval of the current data. |
|
1287 |
||
1288 |
\item @{text change} update of current data (cached!) |
|
1289 |
by giving a continuation. |
|
1290 |
||
1291 |
\item @{text change_yield} update with side result. |
|
21217 | 1292 |
|
1293 |
\end{description} |
|
1294 |
*} |
|
1295 |
||
22798 | 1296 |
subsubsection {* Building implementable systems fo defining equations *} |
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1297 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1298 |
text {* |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1299 |
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
|
1300 |
defining equation systems may be constructed containing |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1301 |
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
|
1302 |
until its underlying executable content changes. |
22798 | 1303 |
|
1304 |
Defining equations are retrieved by instantiation |
|
1305 |
of the functor @{ML_functor CodegenFuncgrRetrieval} |
|
1306 |
which takes two arguments: |
|
1307 |
||
1308 |
\medskip |
|
1309 |
\begin{tabular}{l} |
|
1310 |
@{text "val name: string"} \\ |
|
1311 |
@{text "val rewrites: theory \<rightarrow> thm list"} |
|
1312 |
\end{tabular} |
|
1313 |
||
1314 |
\begin{description} |
|
1315 |
||
1316 |
\item @{text name} is a system-wide unique name identifying |
|
1317 |
this particular system of defining equations. |
|
1318 |
||
1319 |
\item @{text rewrites} specifies a set of theory-dependent |
|
1320 |
rewrite rules which are added to the preprocessor setup; |
|
1321 |
if no additional preprocessing is required, pass |
|
1322 |
a function returning an empty list. |
|
1323 |
||
1324 |
\end{description} |
|
1325 |
||
1326 |
An instance of @{ML_functor CodegenFuncgrRetrieval} in essence |
|
1327 |
provides the following interface: |
|
1328 |
||
1329 |
\medskip |
|
1330 |
\begin{tabular}{l} |
|
1331 |
@{text "make: theory \<rightarrow> CodegenConsts.const list \<rightarrow> CodegenFuncgr.T"} \\ |
|
1332 |
\end{tabular} |
|
1333 |
||
1334 |
\begin{description} |
|
1335 |
||
1336 |
\item @{text make}~@{text thy}~@{text consts} returns |
|
1337 |
a system of defining equations which is guaranteed |
|
1338 |
to contain all defining equations for constants @{text consts} |
|
1339 |
including all defining equations any defining equation |
|
1340 |
for any constant in @{text consts} depends on. |
|
1341 |
||
1342 |
\end{description} |
|
1343 |
||
1344 |
Systems of defining equations are graphs accesible by the |
|
1345 |
following operations: |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1346 |
*} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1347 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1348 |
text %mlref {* |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1349 |
\begin{mldecls} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1350 |
@{index_ML_type CodegenFuncgr.T} \\ |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1351 |
@{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
|
1352 |
@{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
|
1353 |
@{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1354 |
-> CodegenConsts.const list -> CodegenConsts.const list list"} \\ |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1355 |
@{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
|
1356 |
\end{mldecls} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1357 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1358 |
\begin{description} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1359 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1360 |
\item @{ML_type CodegenFuncgr.T} represents |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1361 |
a normalized defining equation system. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1362 |
|
22798 | 1363 |
\item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text const} |
1364 |
retrieves defining equiations for constant @{text const}. |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1365 |
|
22798 | 1366 |
\item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text const} |
1367 |
retrieves function type for constant @{text const}. |
|
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1368 |
|
22798 | 1369 |
\item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text consts} |
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1370 |
returns the transitive closure of dependencies for |
22798 | 1371 |
constants @{text consts} as a partitioning where each partition |
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1372 |
corresponds to a strongly connected component of |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1373 |
dependencies and any partition does \emph{not} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1374 |
depend on partitions further left. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1375 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1376 |
\item @{ML CodegenFuncgr.all}~@{text funcgr} |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1377 |
returns all currently represented constants. |
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1378 |
|
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1379 |
\end{description} |
22798 | 1380 |
*} |
22292
3b118010ec08
adjusted to new code generator Isar commands and changes in implementation
haftmann
parents:
22188
diff
changeset
|
1381 |
|
21147 | 1382 |
subsubsection {* Datatype hooks *} |
1383 |
||
21452 | 1384 |
text {* |
1385 |
Isabelle/HOL's datatype package provides a mechanism to |
|
1386 |
extend theories depending on datatype declarations: |
|
1387 |
\emph{datatype hooks}. For example, when declaring a new |
|
22060 | 1388 |
datatype, a hook proves defining equations for equality on |
21452 | 1389 |
that datatype (if possible). |
1390 |
*} |
|
1391 |
||
21217 | 1392 |
text %mlref {* |
1393 |
\begin{mldecls} |
|
21323 | 1394 |
@{index_ML_type DatatypeHooks.hook: "string list -> theory -> theory"} \\ |
21217 | 1395 |
@{index_ML DatatypeHooks.add: "DatatypeHooks.hook -> theory -> theory"} |
1396 |
\end{mldecls} |
|
21452 | 1397 |
|
1398 |
\begin{description} |
|
1399 |
||
1400 |
\item @{ML_type DatatypeHooks.hook} specifies the interface |
|
1401 |
of \emph{datatype hooks}: a theory update |
|
1402 |
depending on the list of newly introduced |
|
1403 |
datatype names. |
|
1404 |
||
1405 |
\item @{ML DatatypeHooks.add} adds a hook to the |
|
1406 |
chain of all hooks. |
|
1407 |
||
1408 |
\end{description} |
|
1409 |
*} |
|
1410 |
||
1411 |
subsubsection {* Trivial typedefs -- type copies *} |
|
1412 |
||
1413 |
text {* |
|
1414 |
Sometimes packages will introduce new types |
|
1415 |
as \emph{marked type copies} similar to Haskell's |
|
1416 |
@{text newtype} declaration (e.g. the HOL record package) |
|
1417 |
\emph{without} tinkering with the overhead of datatypes. |
|
1418 |
Technically, these type copies are trivial forms of typedefs. |
|
1419 |
Since these type copies in code generation view are nothing |
|
1420 |
else than datatypes, they have been given a own package |
|
1421 |
in order to faciliate code generation: |
|
21147 | 1422 |
*} |
21058 | 1423 |
|
21217 | 1424 |
text %mlref {* |
1425 |
\begin{mldecls} |
|
21452 | 1426 |
@{index_ML_type TypecopyPackage.info} \\ |
21217 | 1427 |
@{index_ML TypecopyPackage.add_typecopy: " |
1428 |
bstring * string list -> typ -> (bstring * bstring) option |
|
1429 |
-> theory -> (string * TypecopyPackage.info) * theory"} \\ |
|
1430 |
@{index_ML TypecopyPackage.get_typecopy_info: "theory |
|
1431 |
-> string -> TypecopyPackage.info option"} \\ |
|
1432 |
@{index_ML TypecopyPackage.get_spec: "theory -> string |
|
21452 | 1433 |
-> (string * sort) list * (string * typ list) list"} \\ |
1434 |
@{index_ML_type TypecopyPackage.hook: "string * TypecopyPackage.info -> theory -> theory"} \\ |
|
1435 |
@{index_ML TypecopyPackage.add_hook: |
|
1436 |
"TypecopyPackage.hook -> theory -> theory"} \\ |
|
21217 | 1437 |
\end{mldecls} |
21452 | 1438 |
|
1439 |
\begin{description} |
|
1440 |
||
1441 |
\item @{ML_type TypecopyPackage.info} a record containing |
|
1442 |
the specification and further data of a type copy. |
|
1443 |
||
1444 |
\item @{ML TypecopyPackage.add_typecopy} defines a new |
|
1445 |
type copy. |
|
1446 |
||
1447 |
\item @{ML TypecopyPackage.get_typecopy_info} retrieves |
|
1448 |
data of an existing type copy. |
|
1449 |
||
1450 |
\item @{ML TypecopyPackage.get_spec} retrieves datatype-like |
|
1451 |
specification of a type copy. |
|
1452 |
||
1453 |
\item @{ML_type TypecopyPackage.hook},~@{ML TypecopyPackage.add_hook} |
|
1454 |
provide a hook mechanism corresponding to the hook mechanism |
|
1455 |
on datatypes. |
|
1456 |
||
1457 |
\end{description} |
|
1458 |
*} |
|
1459 |
||
1460 |
subsubsection {* Unifying type copies and datatypes *} |
|
1461 |
||
1462 |
text {* |
|
1463 |
Since datatypes and type copies are mapped to the same concept (datatypes) |
|
1464 |
by code generation, the view on both is unified \qt{code types}: |
|
21217 | 1465 |
*} |
1466 |
||
1467 |
text %mlref {* |
|
1468 |
\begin{mldecls} |
|
21452 | 1469 |
@{index_ML_type DatatypeCodegen.hook: "(string * (bool * ((string * sort) list |
1470 |
* (string * typ list) list))) list |
|
21323 | 1471 |
-> theory -> theory"} \\ |
21217 | 1472 |
@{index_ML DatatypeCodegen.add_codetypes_hook_bootstrap: " |
1473 |
DatatypeCodegen.hook -> theory -> theory"} |
|
1474 |
\end{mldecls} |
|
1475 |
*} |
|
1476 |
||
21222 | 1477 |
text {* |
21452 | 1478 |
\begin{description} |
1479 |
||
1480 |
\item @{ML_type DatatypeCodegen.hook} specifies the code type hook |
|
1481 |
interface: a theory transformation depending on a list of |
|
1482 |
mutual recursive code types; each entry in the list |
|
1483 |
has the structure @{text "(name, (is_data, (vars, cons)))"} |
|
1484 |
where @{text name} is the name of the code type, @{text is_data} |
|
1485 |
is true iff @{text name} is a datatype rather then a type copy, |
|
1486 |
and @{text "(vars, cons)"} is the specification of the code type. |
|
1487 |
||
1488 |
\item @{ML DatatypeCodegen.add_codetypes_hook_bootstrap} adds a code |
|
1489 |
type hook; the hook is immediately processed for all already |
|
1490 |
existing datatypes, in blocks of mutual recursive datatypes, |
|
1491 |
where all datatypes a block depends on are processed before |
|
1492 |
the block. |
|
1493 |
||
1494 |
\end{description} |
|
1495 |
||
1496 |
\emph{Happy proving, happy hacking!} |
|
21222 | 1497 |
*} |
21217 | 1498 |
|
20948 | 1499 |
end |