author | wenzelm |
Wed, 10 Jun 2009 11:28:39 +0200 | |
changeset 31544 | 19b77b1de188 |
parent 31050 | 555b56b66fcf |
child 31848 | e5ab21d14974 |
permissions | -rw-r--r-- |
28447 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Introduction}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Introduction\isanewline |
|
12 |
\isakeyword{imports}\ Setup\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupsection{Introduction and Overview% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\begin{isamarkuptext}% |
|
26 |
This tutorial introduces a generic code generator for the |
|
27 |
\isa{Isabelle} system. |
|
28 |
Generic in the sense that the |
|
29 |
\qn{target language} for which code shall ultimately be |
|
30 |
generated is not fixed but may be an arbitrary state-of-the-art |
|
31 |
functional programming language (currently, the implementation |
|
32 |
supports \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and \isa{Haskell} |
|
33 |
\cite{haskell-revised-report}). |
|
34 |
||
35 |
Conceptually the code generator framework is part |
|
36 |
of Isabelle's \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} meta logic framework; the logic |
|
37 |
\hyperlink{theory.HOL}{\mbox{\isa{HOL}}} which is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} |
|
38 |
already comes with a reasonable framework setup and thus provides |
|
39 |
a good working horse for raising code-generation-driven |
|
40 |
applications. So, we assume some familiarity and experience |
|
41 |
with the ingredients of the \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} distribution theories. |
|
42 |
(see also \cite{isa-tutorial}). |
|
43 |
||
44 |
The code generator aims to be usable with no further ado |
|
45 |
in most cases while allowing for detailed customisation. |
|
46 |
This manifests in the structure of this tutorial: after a short |
|
47 |
conceptual introduction with an example (\secref{sec:intro}), |
|
48 |
we discuss the generic customisation facilities (\secref{sec:program}). |
|
31050 | 49 |
A further section (\secref{sec:adaptation}) is dedicated to the matter of |
50 |
\qn{adaptation} to specific target language environments. After some |
|
28447 | 51 |
further issues (\secref{sec:further}) we conclude with an overview |
52 |
of some ML programming interfaces (\secref{sec:ml}). |
|
53 |
||
54 |
\begin{warn} |
|
55 |
Ultimately, the code generator which this tutorial deals with |
|
56 |
is supposed to replace the existing code generator |
|
57 |
by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. |
|
58 |
So, for the moment, there are two distinct code generators |
|
59 |
in Isabelle. In case of ambiguity, we will refer to the framework |
|
60 |
described here as \isa{generic\ code\ generator}, to the |
|
61 |
other as \isa{SML\ code\ generator}. |
|
62 |
Also note that while the framework itself is |
|
63 |
object-logic independent, only \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} provides a reasonable |
|
64 |
framework setup. |
|
65 |
\end{warn}% |
|
66 |
\end{isamarkuptext}% |
|
67 |
\isamarkuptrue% |
|
68 |
% |
|
69 |
\isamarkupsubsection{Code generation via shallow embedding \label{sec:intro}% |
|
70 |
} |
|
71 |
\isamarkuptrue% |
|
72 |
% |
|
73 |
\begin{isamarkuptext}% |
|
74 |
The key concept for understanding \isa{Isabelle}'s code generation is |
|
75 |
\emph{shallow embedding}, i.e.~logical entities like constants, types and |
|
76 |
classes are identified with corresponding concepts in the target language. |
|
77 |
||
78 |
Inside \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and |
|
79 |
\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form |
|
80 |
the core of a functional programming language. The default code generator setup |
|
81 |
allows to turn those into functional programs immediately. |
|
82 |
This means that \qt{naive} code generation can proceed without further ado. |
|
83 |
For example, here a simple \qt{implementation} of amortised queues:% |
|
84 |
\end{isamarkuptext}% |
|
85 |
\isamarkuptrue% |
|
86 |
% |
|
28564 | 87 |
\isadelimquote |
28447 | 88 |
% |
28564 | 89 |
\endisadelimquote |
28447 | 90 |
% |
28564 | 91 |
\isatagquote |
28447 | 92 |
\isacommand{datatype}\isamarkupfalse% |
29798 | 93 |
\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline |
28447 | 94 |
\isanewline |
95 |
\isacommand{definition}\isamarkupfalse% |
|
96 |
\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
29798 | 97 |
\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
28447 | 98 |
\isanewline |
99 |
\isacommand{primrec}\isamarkupfalse% |
|
100 |
\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
29798 | 101 |
\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline |
28447 | 102 |
\isanewline |
103 |
\isacommand{fun}\isamarkupfalse% |
|
104 |
\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
29798 | 105 |
\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
106 |
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
107 |
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
108 |
\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
|
28564 | 109 |
\endisatagquote |
110 |
{\isafoldquote}% |
|
28447 | 111 |
% |
28564 | 112 |
\isadelimquote |
28447 | 113 |
% |
28564 | 114 |
\endisadelimquote |
28447 | 115 |
% |
116 |
\begin{isamarkuptext}% |
|
117 |
\noindent Then we can generate code e.g.~for \isa{SML} as follows:% |
|
118 |
\end{isamarkuptext}% |
|
119 |
\isamarkuptrue% |
|
120 |
% |
|
28564 | 121 |
\isadelimquote |
28447 | 122 |
% |
28564 | 123 |
\endisadelimquote |
28447 | 124 |
% |
28564 | 125 |
\isatagquote |
28447 | 126 |
\isacommand{export{\isacharunderscore}code}\isamarkupfalse% |
127 |
\ empty\ dequeue\ enqueue\ \isakeyword{in}\ SML\isanewline |
|
128 |
\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}example{\isachardot}ML{\isachardoublequoteclose}% |
|
28564 | 129 |
\endisatagquote |
130 |
{\isafoldquote}% |
|
28447 | 131 |
% |
28564 | 132 |
\isadelimquote |
28447 | 133 |
% |
28564 | 134 |
\endisadelimquote |
28447 | 135 |
% |
136 |
\begin{isamarkuptext}% |
|
137 |
\noindent resulting in the following code:% |
|
138 |
\end{isamarkuptext}% |
|
139 |
\isamarkuptrue% |
|
140 |
% |
|
28564 | 141 |
\isadelimquote |
28447 | 142 |
% |
28564 | 143 |
\endisadelimquote |
28447 | 144 |
% |
28564 | 145 |
\isatagquote |
28447 | 146 |
% |
147 |
\begin{isamarkuptext}% |
|
28727 | 148 |
\isatypewriter% |
28447 | 149 |
\noindent% |
28714 | 150 |
\hspace*{0pt}structure Example = \\ |
151 |
\hspace*{0pt}struct\\ |
|
152 |
\hspace*{0pt}\\ |
|
153 |
\hspace*{0pt}fun foldl f a [] = a\\ |
|
154 |
\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ |
|
155 |
\hspace*{0pt}\\ |
|
156 |
\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ |
|
157 |
\hspace*{0pt}\\ |
|
158 |
\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\ |
|
159 |
\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\ |
|
160 |
\hspace*{0pt}\\ |
|
29798 | 161 |
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ |
28714 | 162 |
\hspace*{0pt}\\ |
29798 | 163 |
\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\ |
28714 | 164 |
\hspace*{0pt}\\ |
29798 | 165 |
\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\ |
166 |
\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ |
|
167 |
\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\ |
|
28714 | 168 |
\hspace*{0pt} ~~~let\\ |
169 |
\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\ |
|
170 |
\hspace*{0pt} ~~~in\\ |
|
29798 | 171 |
\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\ |
28714 | 172 |
\hspace*{0pt} ~~~end;\\ |
173 |
\hspace*{0pt}\\ |
|
29798 | 174 |
\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ |
28714 | 175 |
\hspace*{0pt}\\ |
29297 | 176 |
\hspace*{0pt}end;~(*struct Example*)% |
28447 | 177 |
\end{isamarkuptext}% |
178 |
\isamarkuptrue% |
|
179 |
% |
|
28564 | 180 |
\endisatagquote |
181 |
{\isafoldquote}% |
|
28447 | 182 |
% |
28564 | 183 |
\isadelimquote |
28447 | 184 |
% |
28564 | 185 |
\endisadelimquote |
28447 | 186 |
% |
187 |
\begin{isamarkuptext}% |
|
188 |
\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated list of |
|
189 |
constants for which code shall be generated; anything else needed for those |
|
190 |
is added implicitly. Then follows a target language identifier |
|
191 |
(\isa{SML}, \isa{OCaml} or \isa{Haskell}) and a freely chosen module name. |
|
192 |
A file name denotes the destination to store the generated code. Note that |
|
193 |
the semantics of the destination depends on the target language: for |
|
194 |
\isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} |
|
195 |
it denotes a \emph{directory} where a file named as the module name |
|
196 |
(with extension \isa{{\isachardot}hs}) is written:% |
|
197 |
\end{isamarkuptext}% |
|
198 |
\isamarkuptrue% |
|
199 |
% |
|
28564 | 200 |
\isadelimquote |
28447 | 201 |
% |
28564 | 202 |
\endisadelimquote |
28447 | 203 |
% |
28564 | 204 |
\isatagquote |
28447 | 205 |
\isacommand{export{\isacharunderscore}code}\isamarkupfalse% |
206 |
\ empty\ dequeue\ enqueue\ \isakeyword{in}\ Haskell\isanewline |
|
207 |
\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}% |
|
28564 | 208 |
\endisatagquote |
209 |
{\isafoldquote}% |
|
28447 | 210 |
% |
28564 | 211 |
\isadelimquote |
28447 | 212 |
% |
28564 | 213 |
\endisadelimquote |
28447 | 214 |
% |
215 |
\begin{isamarkuptext}% |
|
216 |
\noindent This is how the corresponding code in \isa{Haskell} looks like:% |
|
217 |
\end{isamarkuptext}% |
|
218 |
\isamarkuptrue% |
|
219 |
% |
|
28564 | 220 |
\isadelimquote |
28447 | 221 |
% |
28564 | 222 |
\endisadelimquote |
28447 | 223 |
% |
28564 | 224 |
\isatagquote |
28447 | 225 |
% |
226 |
\begin{isamarkuptext}% |
|
28727 | 227 |
\isatypewriter% |
28447 | 228 |
\noindent% |
28714 | 229 |
\hspace*{0pt}module Example where {\char123}\\ |
230 |
\hspace*{0pt}\\ |
|
231 |
\hspace*{0pt}\\ |
|
31050 | 232 |
\hspace*{0pt}foldla ::~forall a{\char95}1 b{\char95}1.~(a{\char95}1 -> b{\char95}1 -> a{\char95}1) -> a{\char95}1 -> [b{\char95}1] -> a{\char95}1;\\ |
28714 | 233 |
\hspace*{0pt}foldla f a [] = a;\\ |
234 |
\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\ |
|
235 |
\hspace*{0pt}\\ |
|
29297 | 236 |
\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\ |
28714 | 237 |
\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\ |
238 |
\hspace*{0pt}\\ |
|
29297 | 239 |
\hspace*{0pt}list{\char95}case ::~forall t a.~t -> (a -> [a] -> t) -> [a] -> t;\\ |
28714 | 240 |
\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\ |
241 |
\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\ |
|
242 |
\hspace*{0pt}\\ |
|
29798 | 243 |
\hspace*{0pt}data Queue a = AQueue [a] [a];\\ |
28714 | 244 |
\hspace*{0pt}\\ |
29297 | 245 |
\hspace*{0pt}empty ::~forall a.~Queue a;\\ |
29798 | 246 |
\hspace*{0pt}empty = AQueue [] [];\\ |
28714 | 247 |
\hspace*{0pt}\\ |
29297 | 248 |
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ |
29798 | 249 |
\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\ |
250 |
\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ |
|
251 |
\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\ |
|
31544 | 252 |
\hspace*{0pt} ~(let {\char123}\\ |
28714 | 253 |
\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\ |
31544 | 254 |
\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys) );\\ |
28714 | 255 |
\hspace*{0pt}\\ |
29297 | 256 |
\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ |
29798 | 257 |
\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\ |
28714 | 258 |
\hspace*{0pt}\\ |
259 |
\hspace*{0pt}{\char125}% |
|
28447 | 260 |
\end{isamarkuptext}% |
261 |
\isamarkuptrue% |
|
262 |
% |
|
28564 | 263 |
\endisatagquote |
264 |
{\isafoldquote}% |
|
28447 | 265 |
% |
28564 | 266 |
\isadelimquote |
28447 | 267 |
% |
28564 | 268 |
\endisadelimquote |
28447 | 269 |
% |
270 |
\begin{isamarkuptext}% |
|
271 |
\noindent This demonstrates the basic usage of the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command; |
|
272 |
for more details see \secref{sec:further}.% |
|
273 |
\end{isamarkuptext}% |
|
274 |
\isamarkuptrue% |
|
275 |
% |
|
276 |
\isamarkupsubsection{Code generator architecture \label{sec:concept}% |
|
277 |
} |
|
278 |
\isamarkuptrue% |
|
279 |
% |
|
280 |
\begin{isamarkuptext}% |
|
281 |
What you have seen so far should be already enough in a lot of cases. If you |
|
282 |
are content with this, you can quit reading here. Anyway, in order to customise |
|
283 |
and adapt the code generator, it is inevitable to gain some understanding |
|
284 |
how it works. |
|
285 |
||
286 |
\begin{figure}[h] |
|
30882
d15725e84091
moved generated eps/pdf to main directory, for proper display in dvi;
wenzelm
parents:
30880
diff
changeset
|
287 |
\includegraphics{architecture} |
28447 | 288 |
\caption{Code generator architecture} |
289 |
\label{fig:arch} |
|
290 |
\end{figure} |
|
291 |
||
292 |
The code generator employs a notion of executability |
|
293 |
for three foundational executable ingredients known |
|
294 |
from functional programming: |
|
29560 | 295 |
\emph{code equations}, \emph{datatypes}, and |
296 |
\emph{type classes}. A code equation as a first approximation |
|
28447 | 297 |
is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t} |
298 |
(an equation headed by a constant \isa{f} with arguments |
|
299 |
\isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}). |
|
29560 | 300 |
Code generation aims to turn code equations |
28447 | 301 |
into a functional program. This is achieved by three major |
302 |
components which operate sequentially, i.e. the result of one is |
|
303 |
the input |
|
30880 | 304 |
of the next in the chain, see figure \ref{fig:arch}: |
28447 | 305 |
|
306 |
\begin{itemize} |
|
307 |
||
30836 | 308 |
\item Starting point is a collection of raw code equations in a |
309 |
theory; due to proof irrelevance it is not relevant where they |
|
310 |
stem from but typically they are either descendant of specification |
|
311 |
tools or explicit proofs by the user. |
|
312 |
||
313 |
\item Before these raw code equations are continued |
|
314 |
with, they can be subjected to theorem transformations. This |
|
315 |
\qn{preprocessor} is an interface which allows to apply the full |
|
316 |
expressiveness of ML-based theorem transformations to code |
|
317 |
generation. The result of the preprocessing step is a |
|
318 |
structured collection of code equations. |
|
28447 | 319 |
|
30836 | 320 |
\item These code equations are \qn{translated} to a program in an |
321 |
abstract intermediate language. Think of it as a kind |
|
28447 | 322 |
of \qt{Mini-Haskell} with four \qn{statements}: \isa{data} |
29560 | 323 |
(for datatypes), \isa{fun} (stemming from code equations), |
28447 | 324 |
also \isa{class} and \isa{inst} (for type classes). |
325 |
||
326 |
\item Finally, the abstract program is \qn{serialised} into concrete |
|
327 |
source code of a target language. |
|
30836 | 328 |
This step only produces concrete syntax but does not change the |
329 |
program in essence; all conceptual transformations occur in the |
|
330 |
translation step. |
|
28447 | 331 |
|
332 |
\end{itemize} |
|
333 |
||
334 |
\noindent From these steps, only the two last are carried out outside the logic; by |
|
335 |
keeping this layer as thin as possible, the amount of code to trust is |
|
336 |
kept to a minimum.% |
|
337 |
\end{isamarkuptext}% |
|
338 |
\isamarkuptrue% |
|
339 |
% |
|
340 |
\isadelimtheory |
|
341 |
% |
|
342 |
\endisadelimtheory |
|
343 |
% |
|
344 |
\isatagtheory |
|
345 |
\isacommand{end}\isamarkupfalse% |
|
346 |
% |
|
347 |
\endisatagtheory |
|
348 |
{\isafoldtheory}% |
|
349 |
% |
|
350 |
\isadelimtheory |
|
351 |
% |
|
352 |
\endisadelimtheory |
|
353 |
\isanewline |
|
354 |
\end{isabellebody}% |
|
355 |
%%% Local Variables: |
|
356 |
%%% mode: latex |
|
357 |
%%% TeX-master: "root" |
|
358 |
%%% End: |