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