26 (see also \cite{isa-tutorial}). |
26 (see also \cite{isa-tutorial}). |
27 |
27 |
28 The code generator aims to be usable with no further ado |
28 The code generator aims to be usable with no further ado |
29 in most cases while allowing for detailed customisation. |
29 in most cases while allowing for detailed customisation. |
30 This manifests in the structure of this tutorial: after a short |
30 This manifests in the structure of this tutorial: after a short |
31 conceptual introduction with an example \secref{sec:intro}, |
31 conceptual introduction with an example (\secref{sec:intro}), |
32 we discuss the generic customisation facilities \secref{sec:program}. |
32 we discuss the generic customisation facilities (\secref{sec:program}). |
33 A further section \secref{sec:adaption} is dedicated to the matter of |
33 A further section (\secref{sec:adaption}) is dedicated to the matter of |
34 \qn{adaption} to specific target language environments. After some |
34 \qn{adaption} to specific target language environments. After some |
35 further issues \secref{sec:further} we conclude with an overview |
35 further issues (\secref{sec:further}) we conclude with an overview |
36 of some ML programming interfaces \secref{sec:ml}. |
36 of some ML programming interfaces (\secref{sec:ml}). |
37 |
37 |
38 \begin{warn} |
38 \begin{warn} |
39 Ultimately, the code generator which this tutorial deals with |
39 Ultimately, the code generator which this tutorial deals with |
40 is supposed to replace the already established code generator |
40 is supposed to replace the existing code generator |
41 by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. |
41 by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. |
42 So, for the moment, there are two distinct code generators |
42 So, for the moment, there are two distinct code generators |
43 in Isabelle. |
43 in Isabelle. In case of ambiguity, we will refer to the framework |
|
44 described here as @{text "generic code generator"}, to the |
|
45 other as @{text "SML code generator"}. |
44 Also note that while the framework itself is |
46 Also note that while the framework itself is |
45 object-logic independent, only @{theory HOL} provides a reasonable |
47 object-logic independent, only @{theory HOL} provides a reasonable |
46 framework setup. |
48 framework setup. |
47 \end{warn} |
49 \end{warn} |
48 |
50 |
57 |
59 |
58 Inside @{theory HOL}, the @{command datatype} and |
60 Inside @{theory HOL}, the @{command datatype} and |
59 @{command definition}/@{command primrec}/@{command fun} declarations form |
61 @{command definition}/@{command primrec}/@{command fun} declarations form |
60 the core of a functional programming language. The default code generator setup |
62 the core of a functional programming language. The default code generator setup |
61 allows to turn those into functional programs immediately. |
63 allows to turn those into functional programs immediately. |
62 |
|
63 This means that \qt{naive} code generation can proceed without further ado. |
64 This means that \qt{naive} code generation can proceed without further ado. |
64 For example, here a simple \qt{implementation} of amortised queues: |
65 For example, here a simple \qt{implementation} of amortised queues: |
65 *} |
66 *} |
66 |
67 |
67 datatype %quoteme 'a queue = Queue "'a list" "'a list" |
68 datatype %quoteme 'a queue = Queue "'a list" "'a list" |
73 "enqueue x (Queue xs ys) = Queue (x # xs) ys" |
74 "enqueue x (Queue xs ys) = Queue (x # xs) ys" |
74 |
75 |
75 fun %quoteme dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where |
76 fun %quoteme dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where |
76 "dequeue (Queue [] []) = (None, Queue [] [])" |
77 "dequeue (Queue [] []) = (None, Queue [] [])" |
77 | "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)" |
78 | "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)" |
78 | "dequeue (Queue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, Queue [] ys))" |
79 | "dequeue (Queue xs []) = |
|
80 (case rev xs of y # ys \<Rightarrow> (Some y, Queue [] ys))" |
79 |
81 |
80 text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *} |
82 text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *} |
81 |
83 |
82 export_code %quoteme empty dequeue enqueue in SML module_name Example file "examples/example.ML" |
84 export_code %quoteme empty dequeue enqueue in SML |
|
85 module_name Example file "examples/example.ML" |
83 |
86 |
84 text {* \noindent resulting in the following code: *} |
87 text {* \noindent resulting in the following code: *} |
85 |
88 |
86 text %quoteme {*@{code_stmts empty enqueue dequeue (SML)}*} |
89 text %quoteme {*@{code_stmts empty enqueue dequeue (SML)}*} |
87 |
90 |
88 text {* |
91 text {* |
89 \noindent The @{command export_code} command takes a space-separated list of |
92 \noindent The @{command export_code} command takes a space-separated list of |
90 constants for which code shall be generated; anything else needed for those |
93 constants for which code shall be generated; anything else needed for those |
91 is added implicitly. Then follows by a target language identifier |
94 is added implicitly. Then follows a target language identifier |
92 (@{text SML}, @{text OCaml} or @{text Haskell}) and a freely chosen module name. |
95 (@{text SML}, @{text OCaml} or @{text Haskell}) and a freely chosen module name. |
93 A file name denotes the destination to store the generated code. Note that |
96 A file name denotes the destination to store the generated code. Note that |
94 the semantics of the destination depends on the target language: for |
97 the semantics of the destination depends on the target language: for |
95 @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text Haskell} |
98 @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text Haskell} |
96 it denotes a \emph{directory} where a file named as the module name |
99 it denotes a \emph{directory} where a file named as the module name |
97 (with extension @{text ".hs"}) is written: |
100 (with extension @{text ".hs"}) is written: |
98 *} |
101 *} |
99 |
102 |
100 export_code %quoteme empty dequeue enqueue in Haskell module_name Example file "examples/" |
103 export_code %quoteme empty dequeue enqueue in Haskell |
|
104 module_name Example file "examples/" |
101 |
105 |
102 text {* |
106 text {* |
103 \noindent This is how the corresponding code in @{text Haskell} looks like: |
107 \noindent This is how the corresponding code in @{text Haskell} looks like: |
104 *} |
108 *} |
105 |
109 |
106 text %quoteme {*@{code_stmts empty enqueue dequeue (Haskell)}*} |
110 text %quoteme {*@{code_stmts empty enqueue dequeue (Haskell)}*} |
107 |
111 |
108 text {* |
112 text {* |
109 \noindent This demonstrates the basic usage of the @{command export_code} command; |
113 \noindent This demonstrates the basic usage of the @{command export_code} command; |
110 for more details see \secref{sec:serializer}. |
114 for more details see \secref{sec:further}. |
111 *} |
115 *} |
112 |
116 |
113 subsection {* Code generator architecture *} |
117 subsection {* Code generator architecture \label{sec:concept} *} |
114 |
118 |
115 text {* |
119 text {* |
116 What you have seen so far should be already enough in a lot of cases. If you |
120 What you have seen so far should be already enough in a lot of cases. If you |
117 are content with this, you can quit reading here. Anyway, in order to customise |
121 are content with this, you can quit reading here. Anyway, in order to customise |
118 and adapt the code generator, it is inevitable to gain some understanding |
122 and adapt the code generator, it is inevitable to gain some understanding |
123 \includegraphics[width=0.7\textwidth]{codegen_process} |
127 \includegraphics[width=0.7\textwidth]{codegen_process} |
124 \caption{Code generator architecture} |
128 \caption{Code generator architecture} |
125 \label{fig:arch} |
129 \label{fig:arch} |
126 \end{figure} |
130 \end{figure} |
127 |
131 |
128 The code generator itself consists of three major components |
|
129 which operate sequentially, i.e. the result of one is the input |
|
130 of the next in the chain, see diagram \ref{fig:arch}: |
|
131 |
|
132 The code generator employs a notion of executability |
132 The code generator employs a notion of executability |
133 for three foundational executable ingredients known |
133 for three foundational executable ingredients known |
134 from functional programming: |
134 from functional programming: |
135 \emph{defining equations}, \emph{datatypes}, and |
135 \emph{defining equations}, \emph{datatypes}, and |
136 \emph{type classes}. A defining equation as a first approximation |
136 \emph{type classes}. A defining equation as a first approximation |
137 is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"} |
137 is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"} |
138 (an equation headed by a constant @{text f} with arguments |
138 (an equation headed by a constant @{text f} with arguments |
139 @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}). |
139 @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}). |
140 Code generation aims to turn defining equations |
140 Code generation aims to turn defining equations |
141 into a functional program by running through the following |
141 into a functional program. This is achieved by three major |
142 process: |
142 components which operate sequentially, i.e. the result of one is |
|
143 the input |
|
144 of the next in the chain, see diagram \ref{fig:arch}: |
143 |
145 |
144 \begin{itemize} |
146 \begin{itemize} |
145 |
147 |
146 \item Out of the vast collection of theorems proven in a |
148 \item Out of the vast collection of theorems proven in a |
147 \qn{theory}, a reasonable subset modelling |
149 \qn{theory}, a reasonable subset modelling |
163 \secref{sec:preproc}. |
165 \secref{sec:preproc}. |
164 The result of the preprocessing step is a structured collection |
166 The result of the preprocessing step is a structured collection |
165 of defining equations. |
167 of defining equations. |
166 |
168 |
167 \item These defining equations are \qn{translated} to a program |
169 \item These defining equations are \qn{translated} to a program |
168 in an abstract intermediate language. |
170 in an abstract intermediate language. Think of it as a kind |
|
171 of \qt{Mini-Haskell} with four \qn{statements}: @{text data} |
|
172 (for datatypes), @{text fun} (stemming from defining equations), |
|
173 also @{text class} and @{text inst} (for type classes). |
169 |
174 |
170 \item Finally, the abstract program is \qn{serialised} into concrete |
175 \item Finally, the abstract program is \qn{serialised} into concrete |
171 source code of a target language. |
176 source code of a target language. |
172 |
177 |
173 \end{itemize} |
178 \end{itemize} |