doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
author haftmann
Mon Nov 03 14:15:25 2008 +0100 (2008-11-03)
changeset 28714 1992553cccfe
parent 28636 d5342d4c7360
child 28727 185110a4b97a
permissions -rw-r--r--
improved verbatim mechanism
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@28447
    97
\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\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@28447
   101
\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\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@28447
   105
\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ Queue\ {\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@28447
   109
\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28447
   110
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28447
   111
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
haftmann@28447
   112
\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ {\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@28447
   152
\isaverbatim%
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@28714
   165
\hspace*{0pt}datatype 'a queue = Queue of 'a list * 'a list;\\
haftmann@28714
   166
\hspace*{0pt}\\
haftmann@28714
   167
\hspace*{0pt}val empty :~'a queue = Queue ([], []);\\
haftmann@28714
   168
\hspace*{0pt}\\
haftmann@28714
   169
\hspace*{0pt}fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))\\
haftmann@28714
   170
\hspace*{0pt} ~| dequeue (Queue (xs, y ::~ys)) = (SOME y, Queue (xs, ys))\\
haftmann@28714
   171
\hspace*{0pt} ~| dequeue (Queue (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@28714
   175
\hspace*{0pt} ~~~~~(SOME y, Queue ([], ys))\\
haftmann@28714
   176
\hspace*{0pt} ~~~end;\\
haftmann@28714
   177
\hspace*{0pt}\\
haftmann@28714
   178
\hspace*{0pt}fun enqueue x (Queue (xs, ys)) = Queue (x ::~xs, ys);\\
haftmann@28714
   179
\hspace*{0pt}\\
haftmann@28714
   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@28447
   231
\isaverbatim%
haftmann@28447
   232
\noindent%
haftmann@28714
   233
\hspace*{0pt}module Example where {\char123}\\
haftmann@28714
   234
\hspace*{0pt}\\
haftmann@28714
   235
\hspace*{0pt}\\
haftmann@28714
   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}\\
haftmann@28714
   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}\\
haftmann@28714
   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@28714
   247
\hspace*{0pt}data Queue a = Queue [a] [a];\\
haftmann@28714
   248
\hspace*{0pt}\\
haftmann@28714
   249
\hspace*{0pt}empty ::~forall a. Queue a;\\
haftmann@28714
   250
\hspace*{0pt}empty = Queue [] [];\\
haftmann@28714
   251
\hspace*{0pt}\\
haftmann@28714
   252
\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
haftmann@28714
   253
\hspace*{0pt}dequeue (Queue [] []) = (Nothing, Queue [] []);\\
haftmann@28714
   254
\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
haftmann@28714
   255
\hspace*{0pt}dequeue (Queue (v :~va) []) =\\
haftmann@28714
   256
\hspace*{0pt} ~let {\char123}\\
haftmann@28714
   257
\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
haftmann@28714
   258
\hspace*{0pt} ~{\char125}~in (Just y, Queue [] ys);\\
haftmann@28714
   259
\hspace*{0pt}\\
haftmann@28714
   260
\hspace*{0pt}enqueue ::~forall a. a -> Queue a -> Queue a;\\
haftmann@28714
   261
\hspace*{0pt}enqueue x (Queue xs ys) = Queue (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@28635
   296
      \node (eqn) at (2, 2) [style=entity] {defining 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@28447
   321
  \emph{defining equations}, \emph{datatypes}, and
haftmann@28447
   322
  \emph{type classes}.  A defining 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@28447
   326
  Code generation aims to turn defining 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@28447
   336
      defining 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@28447
   345
    \item Before the selected defining 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@28447
   353
      of defining equations.
haftmann@28447
   354
haftmann@28447
   355
    \item These defining 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@28447
   358
      (for datatypes), \isa{fun} (stemming from defining 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: