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