6 Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
9 section \<open>Introduction\<close>
12 This tutorial introduces the code generator facilities of @{text
13 "Isabelle/HOL"}. It allows to turn (a certain class of) HOL
14 specifications into corresponding executable code in the programming
15 languages @{text SML} @{cite SML}, @{text OCaml} @{cite OCaml},
16 @{text Haskell} @{cite "haskell-revised-report"} and @{text Scala}
17 @{cite "scala-overview-tech-report"}.
19 To profit from this tutorial, some familiarity and experience with
20 @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed.
24 subsection \<open>Code generation principle: shallow embedding \label{sec:principle}\<close>
27 The key concept for understanding Isabelle's code generation is
28 \emph{shallow embedding}: logical entities like constants, types and
29 classes are identified with corresponding entities in the target
30 language. In particular, the carrier of a generated program's
31 semantics are \emph{equational theorems} from the logic. If we view
32 a generated program as an implementation of a higher-order rewrite
33 system, then every rewrite step performed by the program can be
34 simulated in the logic, which guarantees partial correctness
35 @{cite "Haftmann-Nipkow:2010:code"}.
39 subsection \<open>A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}\<close>
42 In a HOL theory, the @{command_def datatype} and @{command_def
43 definition}/@{command_def primrec}/@{command_def fun} declarations
44 form the core of a functional programming language. By default
45 equational theorems stemming from those are used for generated code,
46 therefore \qt{naive} code generation can proceed without further
49 For example, here a simple \qt{implementation} of amortised queues:
52 datatype %quote 'a queue = AQueue "'a list" "'a list"
54 definition %quote empty :: "'a queue" where
55 "empty = AQueue [] []"
57 primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
58 "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
60 fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
61 "dequeue (AQueue [] []) = (None, AQueue [] [])"
62 | "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
63 | "dequeue (AQueue xs []) =
64 (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))" (*<*)
66 lemma %invisible dequeue_nonempty_Nil [simp]:
67 "xs \<noteq> [] \<Longrightarrow> dequeue (AQueue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
68 by (cases xs) (simp_all split: list.splits) (*>*)
70 text \<open>\noindent Then we can generate code e.g.~for @{text SML} as follows:\<close>
72 export_code %quote empty dequeue enqueue in SML
73 module_name Example file "$ISABELLE_TMP/examples/example.ML"
75 text \<open>\noindent resulting in the following code:\<close>
77 text %quotetypewriter \<open>
78 @{code_stmts empty enqueue dequeue (SML)}
82 \noindent The @{command_def export_code} command takes a
83 space-separated list of constants for which code shall be generated;
84 anything else needed for those is added implicitly. Then follows a
85 target language identifier and a freely chosen module name. A file
86 name denotes the destination to store the generated code. Note that
87 the semantics of the destination depends on the target language: for
88 @{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
89 for @{text Haskell} it denotes a \emph{directory} where a file named as the
90 module name (with extension @{text ".hs"}) is written:
93 export_code %quote empty dequeue enqueue in Haskell
94 module_name Example file "$ISABELLE_TMP/examples/"
97 \noindent This is the corresponding code:
100 text %quotetypewriter \<open>
101 @{code_stmts empty enqueue dequeue (Haskell)}
105 \noindent For more details about @{command export_code} see
106 \secref{sec:further}.
110 subsection \<open>Type classes\<close>
113 Code can also be generated from type classes in a Haskell-like
114 manner. For illustration here an example from abstract algebra:
117 class %quote semigroup =
118 fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
119 assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
121 class %quote monoid = semigroup +
122 fixes neutral :: 'a ("\<one>")
123 assumes neutl: "\<one> \<otimes> x = x"
124 and neutr: "x \<otimes> \<one> = x"
126 instantiation %quote nat :: monoid
129 primrec %quote mult_nat where
130 "0 \<otimes> n = (0::nat)"
131 | "Suc m \<otimes> n = n + m \<otimes> n"
133 definition %quote neutral_nat where
136 lemma %quote add_mult_distrib:
138 shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
139 by (induct n) simp_all
141 instance %quote proof
143 show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
144 by (induct m) (simp_all add: add_mult_distrib)
145 show "\<one> \<otimes> n = n"
146 by (simp add: neutral_nat_def)
147 show "m \<otimes> \<one> = m"
148 by (induct m) (simp_all add: neutral_nat_def)
154 \noindent We define the natural operation of the natural numbers
158 primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
160 | "pow (Suc n) a = a \<otimes> pow n a"
163 \noindent This we use to define the discrete exponentiation
167 definition %quote bexp :: "nat \<Rightarrow> nat" where
168 "bexp n = pow n (Suc (Suc 0))"
171 \noindent The corresponding code in Haskell uses that language's
175 text %quotetypewriter \<open>
176 @{code_stmts bexp (Haskell)}
180 \noindent This is a convenient place to show how explicit dictionary
181 construction manifests in generated code -- the same example in
185 text %quotetypewriter \<open>
186 @{code_stmts bexp (SML)}
190 \noindent Note the parameters with trailing underscore (@{verbatim
191 "A_"}), which are the dictionary parameters.
195 subsection \<open>How to continue from here\<close>
198 What you have seen so far should be already enough in a lot of
199 cases. If you are content with this, you can quit reading here.
201 Anyway, to understand situations where problems occur or to increase
202 the scope of code generation beyond default, it is necessary to gain
203 some understanding how the code generator actually works:
207 \item The foundations of the code generator are described in
208 \secref{sec:foundations}.
210 \item In particular \secref{sec:utterly_wrong} gives hints how to
211 debug situations where code generation does not succeed as
214 \item The scope and quality of generated code can be increased
215 dramatically by applying refinement techniques, which are
216 introduced in \secref{sec:refinement}.
218 \item Inductive predicates can be turned executable using an
219 extension of the code generator \secref{sec:inductive}.
221 \item If you want to utilize code generation to obtain fast
222 evaluators e.g.~for decision procedures, have a look at
223 \secref{sec:evaluation}.
225 \item You may want to skim over the more technical sections
226 \secref{sec:adaptation} and \secref{sec:further}.
228 \item The target language Scala @{cite "scala-overview-tech-report"}
229 comes with some specialities discussed in \secref{sec:scala}.
231 \item For exhaustive syntax diagrams etc. you should visit the
232 Isabelle/Isar Reference Manual @{cite "isabelle-isar-ref"}.
238 \begin{center}\fbox{\fbox{\begin{minipage}{8cm}
240 \begin{center}\textit{Happy proving, happy hacking!}\end{center}
242 \end{minipage}}}\end{center}