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