28213
|
1 |
theory Introduction
|
|
2 |
imports Setup
|
|
3 |
begin
|
|
4 |
|
38405
|
5 |
section {* Introduction *}
|
|
6 |
|
38437
|
7 |
text {*
|
|
8 |
This tutorial introduces the code generator facilities of @{text
|
|
9 |
"Isabelle/HOL"}. It allows to turn (a certain class of) HOL
|
|
10 |
specifications into corresponding executable code in the programming
|
38814
|
11 |
languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml},
|
|
12 |
@{text Haskell} \cite{haskell-revised-report} and @{text Scala}
|
|
13 |
\cite{scala-overview-tech-report}.
|
38405
|
14 |
|
38437
|
15 |
To profit from this tutorial, some familiarity and experience with
|
|
16 |
@{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
|
|
17 |
*}
|
38405
|
18 |
|
|
19 |
|
38437
|
20 |
subsection {* Code generation principle: shallow embedding \label{sec:principle} *}
|
28213
|
21 |
|
|
22 |
text {*
|
38437
|
23 |
The key concept for understanding Isabelle's code generation is
|
|
24 |
\emph{shallow embedding}: logical entities like constants, types and
|
|
25 |
classes are identified with corresponding entities in the target
|
|
26 |
language. In particular, the carrier of a generated program's
|
|
27 |
semantics are \emph{equational theorems} from the logic. If we view
|
|
28 |
a generated program as an implementation of a higher-order rewrite
|
|
29 |
system, then every rewrite step performed by the program can be
|
|
30 |
simulated in the logic, which guarantees partial correctness
|
|
31 |
\cite{Haftmann-Nipkow:2010:code}.
|
28213
|
32 |
*}
|
|
33 |
|
38437
|
34 |
|
|
35 |
subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
|
28419
|
36 |
|
|
37 |
text {*
|
38505
|
38 |
In a HOL theory, the @{command_def datatype} and @{command_def
|
|
39 |
definition}/@{command_def primrec}/@{command_def fun} declarations
|
|
40 |
form the core of a functional programming language. By default
|
|
41 |
equational theorems stemming from those are used for generated code,
|
|
42 |
therefore \qt{naive} code generation can proceed without further
|
|
43 |
ado.
|
28419
|
44 |
|
|
45 |
For example, here a simple \qt{implementation} of amortised queues:
|
|
46 |
*}
|
|
47 |
|
29798
|
48 |
datatype %quote 'a queue = AQueue "'a list" "'a list"
|
28419
|
49 |
|
28564
|
50 |
definition %quote empty :: "'a queue" where
|
29798
|
51 |
"empty = AQueue [] []"
|
28419
|
52 |
|
28564
|
53 |
primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
|
29798
|
54 |
"enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
|
28419
|
55 |
|
28564
|
56 |
fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
|
29798
|
57 |
"dequeue (AQueue [] []) = (None, AQueue [] [])"
|
|
58 |
| "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
|
|
59 |
| "dequeue (AQueue xs []) =
|
38437
|
60 |
(case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))" (*<*)
|
|
61 |
|
|
62 |
lemma %invisible dequeue_nonempty_Nil [simp]:
|
|
63 |
"xs \<noteq> [] \<Longrightarrow> dequeue (AQueue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
|
|
64 |
by (cases xs) (simp_all split: list.splits) (*>*)
|
28419
|
65 |
|
|
66 |
text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
|
28213
|
67 |
|
28564
|
68 |
export_code %quote empty dequeue enqueue in SML
|
28447
|
69 |
module_name Example file "examples/example.ML"
|
28419
|
70 |
|
|
71 |
text {* \noindent resulting in the following code: *}
|
|
72 |
|
28564
|
73 |
text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
|
28419
|
74 |
|
|
75 |
text {*
|
38505
|
76 |
\noindent The @{command_def export_code} command takes a
|
|
77 |
space-separated list of constants for which code shall be generated;
|
|
78 |
anything else needed for those is added implicitly. Then follows a
|
|
79 |
target language identifier and a freely chosen module name. A file
|
|
80 |
name denotes the destination to store the generated code. Note that
|
|
81 |
the semantics of the destination depends on the target language: for
|
38814
|
82 |
@{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
|
|
83 |
for @{text Haskell} it denotes a \emph{directory} where a file named as the
|
38437
|
84 |
module name (with extension @{text ".hs"}) is written:
|
28419
|
85 |
*}
|
|
86 |
|
28564
|
87 |
export_code %quote empty dequeue enqueue in Haskell
|
28447
|
88 |
module_name Example file "examples/"
|
28419
|
89 |
|
|
90 |
text {*
|
38437
|
91 |
\noindent This is the corresponding code:
|
28419
|
92 |
*}
|
|
93 |
|
28564
|
94 |
text %quote {*@{code_stmts empty enqueue dequeue (Haskell)}*}
|
28419
|
95 |
|
|
96 |
text {*
|
38437
|
97 |
\noindent For more details about @{command export_code} see
|
|
98 |
\secref{sec:further}.
|
28419
|
99 |
*}
|
28213
|
100 |
|
38437
|
101 |
|
|
102 |
subsection {* Type classes *}
|
38402
|
103 |
|
|
104 |
text {*
|
38437
|
105 |
Code can also be generated from type classes in a Haskell-like
|
|
106 |
manner. For illustration here an example from abstract algebra:
|
38402
|
107 |
*}
|
|
108 |
|
38437
|
109 |
class %quote semigroup =
|
|
110 |
fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
|
|
111 |
assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
|
|
112 |
|
|
113 |
class %quote monoid = semigroup +
|
|
114 |
fixes neutral :: 'a ("\<one>")
|
|
115 |
assumes neutl: "\<one> \<otimes> x = x"
|
|
116 |
and neutr: "x \<otimes> \<one> = x"
|
|
117 |
|
|
118 |
instantiation %quote nat :: monoid
|
|
119 |
begin
|
|
120 |
|
|
121 |
primrec %quote mult_nat where
|
|
122 |
"0 \<otimes> n = (0\<Colon>nat)"
|
|
123 |
| "Suc m \<otimes> n = n + m \<otimes> n"
|
|
124 |
|
|
125 |
definition %quote neutral_nat where
|
|
126 |
"\<one> = Suc 0"
|
|
127 |
|
|
128 |
lemma %quote add_mult_distrib:
|
|
129 |
fixes n m q :: nat
|
|
130 |
shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
|
|
131 |
by (induct n) simp_all
|
|
132 |
|
|
133 |
instance %quote proof
|
|
134 |
fix m n q :: nat
|
|
135 |
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
|
|
136 |
by (induct m) (simp_all add: add_mult_distrib)
|
|
137 |
show "\<one> \<otimes> n = n"
|
|
138 |
by (simp add: neutral_nat_def)
|
|
139 |
show "m \<otimes> \<one> = m"
|
|
140 |
by (induct m) (simp_all add: neutral_nat_def)
|
|
141 |
qed
|
|
142 |
|
|
143 |
end %quote
|
28213
|
144 |
|
28419
|
145 |
text {*
|
38437
|
146 |
\noindent We define the natural operation of the natural numbers
|
|
147 |
on monoids:
|
|
148 |
*}
|
|
149 |
|
|
150 |
primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
|
|
151 |
"pow 0 a = \<one>"
|
|
152 |
| "pow (Suc n) a = a \<otimes> pow n a"
|
28419
|
153 |
|
38437
|
154 |
text {*
|
|
155 |
\noindent This we use to define the discrete exponentiation
|
|
156 |
function:
|
|
157 |
*}
|
|
158 |
|
|
159 |
definition %quote bexp :: "nat \<Rightarrow> nat" where
|
|
160 |
"bexp n = pow n (Suc (Suc 0))"
|
|
161 |
|
|
162 |
text {*
|
|
163 |
\noindent The corresponding code in Haskell uses that language's
|
|
164 |
native classes:
|
|
165 |
*}
|
|
166 |
|
|
167 |
text %quote {*@{code_stmts bexp (Haskell)}*}
|
28419
|
168 |
|
38437
|
169 |
text {*
|
|
170 |
\noindent This is a convenient place to show how explicit dictionary
|
|
171 |
construction manifests in generated code -- the same example in
|
|
172 |
@{text SML}:
|
|
173 |
*}
|
|
174 |
|
|
175 |
text %quote {*@{code_stmts bexp (SML)}*}
|
|
176 |
|
|
177 |
text {*
|
|
178 |
\noindent Note the parameters with trailing underscore (@{verbatim
|
|
179 |
"A_"}), which are the dictionary parameters.
|
|
180 |
*}
|
|
181 |
|
|
182 |
|
|
183 |
subsection {* How to continue from here *}
|
|
184 |
|
|
185 |
text {*
|
|
186 |
What you have seen so far should be already enough in a lot of
|
|
187 |
cases. If you are content with this, you can quit reading here.
|
|
188 |
|
|
189 |
Anyway, to understand situations where problems occur or to increase
|
|
190 |
the scope of code generation beyond default, it is necessary to gain
|
|
191 |
some understanding how the code generator actually works:
|
28419
|
192 |
|
|
193 |
\begin{itemize}
|
|
194 |
|
38437
|
195 |
\item The foundations of the code generator are described in
|
|
196 |
\secref{sec:foundations}.
|
|
197 |
|
|
198 |
\item In particular \secref{sec:utterly_wrong} gives hints how to
|
|
199 |
debug situations where code generation does not succeed as
|
|
200 |
expected.
|
28419
|
201 |
|
38437
|
202 |
\item The scope and quality of generated code can be increased
|
|
203 |
dramatically by applying refinement techniques, which are
|
|
204 |
introduced in \secref{sec:refinement}.
|
28419
|
205 |
|
38437
|
206 |
\item Inductive predicates can be turned executable using an
|
|
207 |
extension of the code generator \secref{sec:inductive}.
|
|
208 |
|
|
209 |
\item You may want to skim over the more technical sections
|
|
210 |
\secref{sec:adaptation} and \secref{sec:further}.
|
|
211 |
|
|
212 |
\item For exhaustive syntax diagrams etc. you should visit the
|
|
213 |
Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
|
28419
|
214 |
|
|
215 |
\end{itemize}
|
|
216 |
|
38437
|
217 |
\bigskip
|
|
218 |
|
|
219 |
\begin{center}\fbox{\fbox{\begin{minipage}{8cm}
|
|
220 |
|
|
221 |
\begin{center}\textit{Happy proving, happy hacking!}\end{center}
|
|
222 |
|
|
223 |
\end{minipage}}}\end{center}
|
|
224 |
|
|
225 |
\begin{warn}
|
|
226 |
There is also a more ancient code generator in Isabelle by Stefan
|
|
227 |
Berghofer \cite{Berghofer-Nipkow:2002}. Although its
|
|
228 |
functionality is covered by the code generator presented here, it
|
|
229 |
will sometimes show up as an artifact. In case of ambiguity, we
|
|
230 |
will refer to the framework described here as @{text "generic code
|
|
231 |
generator"}, to the other as @{text "SML code generator"}.
|
|
232 |
\end{warn}
|
28419
|
233 |
*}
|
28213
|
234 |
|
|
235 |
end
|