author | wenzelm |
Mon, 05 Oct 2020 21:15:58 +0200 | |
changeset 72375 | e48d93811ed7 |
parent 70011 | 9dde788b0128 |
child 76649 | 9a6cb5ecc183 |
permissions | -rw-r--r-- |
28213 | 1 |
theory Introduction |
69422
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
wenzelm
parents:
68484
diff
changeset
|
2 |
imports Setup |
59378
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
3 |
begin (*<*) |
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
4 |
|
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
5 |
ML \<open> |
72375 | 6 |
Isabelle_System.make_directory (File.tmp_path (Path.basic "examples")) |
59378
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
7 |
\<close> (*>*) |
28213 | 8 |
|
59377 | 9 |
section \<open>Introduction\<close> |
38405 | 10 |
|
59377 | 11 |
text \<open> |
69505 | 12 |
This tutorial introduces the code generator facilities of \<open>Isabelle/HOL\<close>. It allows to turn (a certain class of) HOL |
38437 | 13 |
specifications into corresponding executable code in the programming |
69505 | 14 |
languages \<open>SML\<close> @{cite SML}, \<open>OCaml\<close> @{cite OCaml}, |
15 |
\<open>Haskell\<close> @{cite "haskell-revised-report"} and \<open>Scala\<close> |
|
58620 | 16 |
@{cite "scala-overview-tech-report"}. |
38405 | 17 |
|
38437 | 18 |
To profit from this tutorial, some familiarity and experience with |
68484 | 19 |
Isabelle/HOL @{cite "isa-tutorial"} and its basic theories is assumed. |
59377 | 20 |
\<close> |
38405 | 21 |
|
22 |
||
59377 | 23 |
subsection \<open>Code generation principle: shallow embedding \label{sec:principle}\<close> |
28213 | 24 |
|
59377 | 25 |
text \<open> |
38437 | 26 |
The key concept for understanding Isabelle's code generation is |
27 |
\emph{shallow embedding}: logical entities like constants, types and |
|
28 |
classes are identified with corresponding entities in the target |
|
29 |
language. In particular, the carrier of a generated program's |
|
30 |
semantics are \emph{equational theorems} from the logic. If we view |
|
31 |
a generated program as an implementation of a higher-order rewrite |
|
32 |
system, then every rewrite step performed by the program can be |
|
33 |
simulated in the logic, which guarantees partial correctness |
|
58620 | 34 |
@{cite "Haftmann-Nipkow:2010:code"}. |
59377 | 35 |
\<close> |
28213 | 36 |
|
38437 | 37 |
|
59377 | 38 |
subsection \<open>A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}\<close> |
28419 | 39 |
|
59377 | 40 |
text \<open> |
58310 | 41 |
In a HOL theory, the @{command_def datatype} and @{command_def |
38505 | 42 |
definition}/@{command_def primrec}/@{command_def fun} declarations |
43 |
form the core of a functional programming language. By default |
|
44 |
equational theorems stemming from those are used for generated code, |
|
45 |
therefore \qt{naive} code generation can proceed without further |
|
46 |
ado. |
|
28419 | 47 |
|
48 |
For example, here a simple \qt{implementation} of amortised queues: |
|
59377 | 49 |
\<close> |
28419 | 50 |
|
58310 | 51 |
datatype %quote 'a queue = AQueue "'a list" "'a list" |
28419 | 52 |
|
28564 | 53 |
definition %quote empty :: "'a queue" where |
29798 | 54 |
"empty = AQueue [] []" |
28419 | 55 |
|
28564 | 56 |
primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where |
29798 | 57 |
"enqueue x (AQueue xs ys) = AQueue (x # xs) ys" |
28419 | 58 |
|
28564 | 59 |
fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where |
29798 | 60 |
"dequeue (AQueue [] []) = (None, AQueue [] [])" |
61 |
| "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)" |
|
62 |
| "dequeue (AQueue xs []) = |
|
38437 | 63 |
(case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))" (*<*) |
64 |
||
65 |
lemma %invisible dequeue_nonempty_Nil [simp]: |
|
66 |
"xs \<noteq> [] \<Longrightarrow> dequeue (AQueue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))" |
|
67 |
by (cases xs) (simp_all split: list.splits) (*>*) |
|
28419 | 68 |
|
69505 | 69 |
text \<open>\noindent Then we can generate code e.g.~for \<open>SML\<close> as follows:\<close> |
28213 | 70 |
|
70011 | 71 |
export_code %quote empty dequeue enqueue in SML module_name Example |
28419 | 72 |
|
59377 | 73 |
text \<open>\noindent resulting in the following code:\<close> |
28419 | 74 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69605
diff
changeset
|
75 |
text %quote \<open> |
39683 | 76 |
@{code_stmts empty enqueue dequeue (SML)} |
59377 | 77 |
\<close> |
28419 | 78 |
|
59377 | 79 |
text \<open> |
70011 | 80 |
\noindent The @{command_def export_code} command takes multiple constants |
81 |
for which code shall be generated; anything else needed for those is |
|
82 |
added implicitly. Then follows a target language identifier and a freely |
|
83 |
chosen \<^theory_text>\<open>module_name\<close>. |
|
70009
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69660
diff
changeset
|
84 |
|
70011 | 85 |
Output is written to a logical file-system within the theory context, |
86 |
with the theory name and ``\<^verbatim>\<open>code\<close>'' as overall prefix. There is also a |
|
87 |
formal session export using the same name: the result may be explored in |
|
88 |
the Isabelle/jEdit Prover IDE using the file-browser on the URL |
|
89 |
``\<^verbatim>\<open>isabelle-export:\<close>''. |
|
90 |
||
91 |
The file name is determined by the target language together with an |
|
92 |
optional \<^theory_text>\<open>file_prefix\<close> (the default is ``\<^verbatim>\<open>export\<close>'' with a consecutive |
|
93 |
number within the current theory). For \<open>SML\<close>, \<open>OCaml\<close> and \<open>Scala\<close>, the |
|
94 |
file prefix becomes a plain file with extension (e.g.\ ``\<^verbatim>\<open>.ML\<close>'' for |
|
95 |
SML). For \<open>Haskell\<close> the file prefix becomes a directory that is populated |
|
96 |
with a separate file for each module (with extension ``\<^verbatim>\<open>.hs\<close>''). |
|
97 |
||
98 |
Consider the following example: |
|
59377 | 99 |
\<close> |
28419 | 100 |
|
28564 | 101 |
export_code %quote empty dequeue enqueue in Haskell |
70011 | 102 |
module_name Example file_prefix example |
28419 | 103 |
|
59377 | 104 |
text \<open> |
38437 | 105 |
\noindent This is the corresponding code: |
59377 | 106 |
\<close> |
28419 | 107 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69605
diff
changeset
|
108 |
text %quote \<open> |
39683 | 109 |
@{code_stmts empty enqueue dequeue (Haskell)} |
59377 | 110 |
\<close> |
28419 | 111 |
|
59377 | 112 |
text \<open> |
38437 | 113 |
\noindent For more details about @{command export_code} see |
114 |
\secref{sec:further}. |
|
59377 | 115 |
\<close> |
28213 | 116 |
|
38437 | 117 |
|
59377 | 118 |
subsection \<open>Type classes\<close> |
38402 | 119 |
|
59377 | 120 |
text \<open> |
38437 | 121 |
Code can also be generated from type classes in a Haskell-like |
122 |
manner. For illustration here an example from abstract algebra: |
|
59377 | 123 |
\<close> |
38402 | 124 |
|
38437 | 125 |
class %quote semigroup = |
126 |
fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70) |
|
127 |
assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
|
128 |
||
129 |
class %quote monoid = semigroup + |
|
130 |
fixes neutral :: 'a ("\<one>") |
|
131 |
assumes neutl: "\<one> \<otimes> x = x" |
|
132 |
and neutr: "x \<otimes> \<one> = x" |
|
133 |
||
134 |
instantiation %quote nat :: monoid |
|
135 |
begin |
|
136 |
||
137 |
primrec %quote mult_nat where |
|
61076 | 138 |
"0 \<otimes> n = (0::nat)" |
38437 | 139 |
| "Suc m \<otimes> n = n + m \<otimes> n" |
140 |
||
141 |
definition %quote neutral_nat where |
|
142 |
"\<one> = Suc 0" |
|
143 |
||
144 |
lemma %quote add_mult_distrib: |
|
145 |
fixes n m q :: nat |
|
146 |
shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q" |
|
147 |
by (induct n) simp_all |
|
148 |
||
149 |
instance %quote proof |
|
150 |
fix m n q :: nat |
|
151 |
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" |
|
152 |
by (induct m) (simp_all add: add_mult_distrib) |
|
153 |
show "\<one> \<otimes> n = n" |
|
154 |
by (simp add: neutral_nat_def) |
|
155 |
show "m \<otimes> \<one> = m" |
|
156 |
by (induct m) (simp_all add: neutral_nat_def) |
|
157 |
qed |
|
158 |
||
159 |
end %quote |
|
28213 | 160 |
|
59377 | 161 |
text \<open> |
38437 | 162 |
\noindent We define the natural operation of the natural numbers |
163 |
on monoids: |
|
59377 | 164 |
\<close> |
38437 | 165 |
|
166 |
primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
167 |
"pow 0 a = \<one>" |
|
168 |
| "pow (Suc n) a = a \<otimes> pow n a" |
|
28419 | 169 |
|
59377 | 170 |
text \<open> |
38437 | 171 |
\noindent This we use to define the discrete exponentiation |
172 |
function: |
|
59377 | 173 |
\<close> |
38437 | 174 |
|
175 |
definition %quote bexp :: "nat \<Rightarrow> nat" where |
|
176 |
"bexp n = pow n (Suc (Suc 0))" |
|
177 |
||
59377 | 178 |
text \<open> |
38437 | 179 |
\noindent The corresponding code in Haskell uses that language's |
180 |
native classes: |
|
59377 | 181 |
\<close> |
38437 | 182 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69605
diff
changeset
|
183 |
text %quote \<open> |
39683 | 184 |
@{code_stmts bexp (Haskell)} |
59377 | 185 |
\<close> |
28419 | 186 |
|
59377 | 187 |
text \<open> |
38437 | 188 |
\noindent This is a convenient place to show how explicit dictionary |
189 |
construction manifests in generated code -- the same example in |
|
69505 | 190 |
\<open>SML\<close>: |
59377 | 191 |
\<close> |
38437 | 192 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69605
diff
changeset
|
193 |
text %quote \<open> |
39683 | 194 |
@{code_stmts bexp (SML)} |
59377 | 195 |
\<close> |
38437 | 196 |
|
59377 | 197 |
text \<open> |
69597 | 198 |
\noindent Note the parameters with trailing underscore (\<^verbatim>\<open>A_\<close>), which are the dictionary parameters. |
59377 | 199 |
\<close> |
38437 | 200 |
|
201 |
||
59377 | 202 |
subsection \<open>How to continue from here\<close> |
38437 | 203 |
|
59377 | 204 |
text \<open> |
38437 | 205 |
What you have seen so far should be already enough in a lot of |
206 |
cases. If you are content with this, you can quit reading here. |
|
207 |
||
208 |
Anyway, to understand situations where problems occur or to increase |
|
209 |
the scope of code generation beyond default, it is necessary to gain |
|
210 |
some understanding how the code generator actually works: |
|
28419 | 211 |
|
212 |
\begin{itemize} |
|
213 |
||
38437 | 214 |
\item The foundations of the code generator are described in |
215 |
\secref{sec:foundations}. |
|
216 |
||
217 |
\item In particular \secref{sec:utterly_wrong} gives hints how to |
|
218 |
debug situations where code generation does not succeed as |
|
219 |
expected. |
|
28419 | 220 |
|
38437 | 221 |
\item The scope and quality of generated code can be increased |
222 |
dramatically by applying refinement techniques, which are |
|
223 |
introduced in \secref{sec:refinement}. |
|
28419 | 224 |
|
38437 | 225 |
\item Inductive predicates can be turned executable using an |
226 |
extension of the code generator \secref{sec:inductive}. |
|
227 |
||
40753 | 228 |
\item If you want to utilize code generation to obtain fast |
229 |
evaluators e.g.~for decision procedures, have a look at |
|
230 |
\secref{sec:evaluation}. |
|
231 |
||
38437 | 232 |
\item You may want to skim over the more technical sections |
233 |
\secref{sec:adaptation} and \secref{sec:further}. |
|
234 |
||
58620 | 235 |
\item The target language Scala @{cite "scala-overview-tech-report"} |
42096 | 236 |
comes with some specialities discussed in \secref{sec:scala}. |
237 |
||
38437 | 238 |
\item For exhaustive syntax diagrams etc. you should visit the |
58620 | 239 |
Isabelle/Isar Reference Manual @{cite "isabelle-isar-ref"}. |
28419 | 240 |
|
241 |
\end{itemize} |
|
242 |
||
38437 | 243 |
\bigskip |
244 |
||
245 |
\begin{center}\fbox{\fbox{\begin{minipage}{8cm} |
|
246 |
||
247 |
\begin{center}\textit{Happy proving, happy hacking!}\end{center} |
|
248 |
||
249 |
\end{minipage}}}\end{center} |
|
59377 | 250 |
\<close> |
28213 | 251 |
|
252 |
end |
|
46522 | 253 |