3 \def\isabellecontext{Introduction}%
10 \isacommand{theory}\isamarkupfalse%
11 \ Introduction\isanewline
12 \isakeyword{imports}\ Setup\isanewline
21 \isamarkupsection{Introduction%
25 \begin{isamarkuptext}%
26 This tutorial introduces the code generator facilities of \isa{Isabelle{\isacharslash}HOL}. It allows to turn (a certain class of) HOL
27 specifications into corresponding executable code in the programming
28 languages \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml},
29 \isa{Haskell} \cite{haskell-revised-report} and \isa{Scala}
30 \cite{scala-overview-tech-report}.
32 To profit from this tutorial, some familiarity and experience with
33 \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.%
37 \isamarkupsubsection{Code generation principle: shallow embedding \label{sec:principle}%
41 \begin{isamarkuptext}%
42 The key concept for understanding Isabelle's code generation is
43 \emph{shallow embedding}: logical entities like constants, types and
44 classes are identified with corresponding entities in the target
45 language. In particular, the carrier of a generated program's
46 semantics are \emph{equational theorems} from the logic. If we view
47 a generated program as an implementation of a higher-order rewrite
48 system, then every rewrite step performed by the program can be
49 simulated in the logic, which guarantees partial correctness
50 \cite{Haftmann-Nipkow:2010:code}.%
54 \isamarkupsubsection{A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}%
58 \begin{isamarkuptext}%
59 In a HOL theory, the \indexdef{}{command}{datatype}\hypertarget{command.datatype}{\hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}} and \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}/\indexdef{}{command}{primrec}\hypertarget{command.primrec}{\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}}/\indexdef{}{command}{fun}\hypertarget{command.fun}{\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}} declarations
60 form the core of a functional programming language. By default
61 equational theorems stemming from those are used for generated code,
62 therefore \qt{naive} code generation can proceed without further
65 For example, here a simple \qt{implementation} of amortised queues:%
74 \isacommand{datatype}\isamarkupfalse%
75 \ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
77 \isacommand{definition}\isamarkupfalse%
78 \ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
79 \ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
81 \isacommand{primrec}\isamarkupfalse%
82 \ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
83 \ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
85 \isacommand{fun}\isamarkupfalse%
86 \ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
87 \ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
88 \ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
89 \ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
90 \ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ %
100 \endisadeliminvisible
109 \endisadeliminvisible
111 \begin{isamarkuptext}%
112 \noindent Then we can generate code e.g.~for \isa{SML} as follows:%
121 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
122 \ empty\ dequeue\ enqueue\ \isakeyword{in}\ SML\isanewline
123 \ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}example{\isachardot}ML{\isachardoublequoteclose}%
131 \begin{isamarkuptext}%
132 \noindent resulting in the following code:%
142 \begin{isamarkuptext}%
145 \hspace*{0pt}structure Example :~sig\\
146 \hspace*{0pt} ~val id :~'a -> 'a\\
147 \hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
148 \hspace*{0pt} ~val rev :~'a list -> 'a list\\
149 \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
150 \hspace*{0pt} ~val empty :~'a queue\\
151 \hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
152 \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
153 \hspace*{0pt}end = struct\\
155 \hspace*{0pt}fun id x = (fn xa => xa) x;\\
157 \hspace*{0pt}fun fold f [] = id\\
158 \hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
160 \hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
162 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
164 \hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
166 \hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
167 \hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
168 \hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\
169 \hspace*{0pt} ~~~let\\
170 \hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
171 \hspace*{0pt} ~~~in\\
172 \hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\
173 \hspace*{0pt} ~~~end;\\
175 \hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
177 \hspace*{0pt}end;~(*struct Example*)%
188 \begin{isamarkuptext}%
189 \noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
190 space-separated list of constants for which code shall be generated;
191 anything else needed for those is added implicitly. Then follows a
192 target language identifier and a freely chosen module name. A file
193 name denotes the destination to store the generated code. Note that
194 the semantics of the destination depends on the target language: for
195 \isa{SML}, \isa{OCaml} and \isa{Scala} it denotes a \emph{file},
196 for \isa{Haskell} it denotes a \emph{directory} where a file named as the
197 module name (with extension \isa{{\isachardot}hs}) is written:%
206 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
207 \ empty\ dequeue\ enqueue\ \isakeyword{in}\ Haskell\isanewline
208 \ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}%
216 \begin{isamarkuptext}%
217 \noindent This is the corresponding code:%
227 \begin{isamarkuptext}%
230 \hspace*{0pt}module Example where {\char123}\\
232 \hspace*{0pt}data Queue a = AQueue [a] [a];\\
234 \hspace*{0pt}empty ::~forall a.~Queue a;\\
235 \hspace*{0pt}empty = AQueue [] [];\\
237 \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
238 \hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
239 \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
240 \hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
241 \hspace*{0pt} ~let {\char123}\\
242 \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\
243 \hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
245 \hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
246 \hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
248 \hspace*{0pt}{\char125}%
259 \begin{isamarkuptext}%
260 \noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} see
261 \secref{sec:further}.%
265 \isamarkupsubsection{Type classes%
269 \begin{isamarkuptext}%
270 Code can also be generated from type classes in a Haskell-like
271 manner. For illustration here an example from abstract algebra:%
280 \isacommand{class}\isamarkupfalse%
281 \ semigroup\ {\isacharequal}\isanewline
282 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
283 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
285 \isacommand{class}\isamarkupfalse%
286 \ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
287 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
288 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
289 \ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
291 \isacommand{instantiation}\isamarkupfalse%
292 \ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
293 \isakeyword{begin}\isanewline
295 \isacommand{primrec}\isamarkupfalse%
296 \ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
297 \ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
298 \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
300 \isacommand{definition}\isamarkupfalse%
301 \ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
302 \ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
304 \isacommand{lemma}\isamarkupfalse%
305 \ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
306 \ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
307 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
308 \ \ \isacommand{by}\isamarkupfalse%
309 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
311 \isacommand{instance}\isamarkupfalse%
312 \ \isacommand{proof}\isamarkupfalse%
314 \ \ \isacommand{fix}\isamarkupfalse%
315 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
316 \ \ \isacommand{show}\isamarkupfalse%
317 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
318 \ \ \ \ \isacommand{by}\isamarkupfalse%
319 \ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
320 \ \ \isacommand{show}\isamarkupfalse%
321 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
322 \ \ \ \ \isacommand{by}\isamarkupfalse%
323 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
324 \ \ \isacommand{show}\isamarkupfalse%
325 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
326 \ \ \ \ \isacommand{by}\isamarkupfalse%
327 \ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
328 \isacommand{qed}\isamarkupfalse%
331 \isacommand{end}\isamarkupfalse%
340 \begin{isamarkuptext}%
341 \noindent We define the natural operation of the natural numbers
351 \isacommand{primrec}\isamarkupfalse%
352 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
353 \ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
354 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
362 \begin{isamarkuptext}%
363 \noindent This we use to define the discrete exponentiation
373 \isacommand{definition}\isamarkupfalse%
374 \ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
375 \ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
383 \begin{isamarkuptext}%
384 \noindent The corresponding code in Haskell uses that language's
395 \begin{isamarkuptext}%
398 \hspace*{0pt}module Example where {\char123}\\
400 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
402 \hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
403 \hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
404 \hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
406 \hspace*{0pt}class Semigroup a where {\char123}\\
407 \hspace*{0pt} ~mult ::~a -> a -> a;\\
408 \hspace*{0pt}{\char125};\\
410 \hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
411 \hspace*{0pt} ~neutral ::~a;\\
412 \hspace*{0pt}{\char125};\\
414 \hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
415 \hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
416 \hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
418 \hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
419 \hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
420 \hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
422 \hspace*{0pt}instance Semigroup Nat where {\char123}\\
423 \hspace*{0pt} ~mult = mult{\char95}nat;\\
424 \hspace*{0pt}{\char125};\\
426 \hspace*{0pt}neutral{\char95}nat ::~Nat;\\
427 \hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
429 \hspace*{0pt}instance Monoid Nat where {\char123}\\
430 \hspace*{0pt} ~neutral = neutral{\char95}nat;\\
431 \hspace*{0pt}{\char125};\\
433 \hspace*{0pt}bexp ::~Nat -> Nat;\\
434 \hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
436 \hspace*{0pt}{\char125}%
447 \begin{isamarkuptext}%
448 \noindent This is a convenient place to show how explicit dictionary
449 construction manifests in generated code -- the same example in
460 \begin{isamarkuptext}%
463 \hspace*{0pt}structure Example :~sig\\
464 \hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
465 \hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
466 \hspace*{0pt} ~type 'a semigroup\\
467 \hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
468 \hspace*{0pt} ~type 'a monoid\\
469 \hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
470 \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
471 \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
472 \hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
473 \hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
474 \hspace*{0pt} ~val neutral{\char95}nat :~nat\\
475 \hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
476 \hspace*{0pt} ~val bexp :~nat -> nat\\
477 \hspace*{0pt}end = struct\\
479 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
481 \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
482 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
484 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
485 \hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
487 \hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
488 \hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
489 \hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
491 \hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
492 \hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
494 \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
495 \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
497 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
499 \hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
501 \hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
502 \hspace*{0pt} ~:~nat monoid;\\
504 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
506 \hspace*{0pt}end;~(*struct Example*)%
517 \begin{isamarkuptext}%
518 \noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.%
522 \isamarkupsubsection{How to continue from here%
526 \begin{isamarkuptext}%
527 What you have seen so far should be already enough in a lot of
528 cases. If you are content with this, you can quit reading here.
530 Anyway, to understand situations where problems occur or to increase
531 the scope of code generation beyond default, it is necessary to gain
532 some understanding how the code generator actually works:
536 \item The foundations of the code generator are described in
537 \secref{sec:foundations}.
539 \item In particular \secref{sec:utterly_wrong} gives hints how to
540 debug situations where code generation does not succeed as
543 \item The scope and quality of generated code can be increased
544 dramatically by applying refinement techniques, which are
545 introduced in \secref{sec:refinement}.
547 \item Inductive predicates can be turned executable using an
548 extension of the code generator \secref{sec:inductive}.
550 \item You may want to skim over the more technical sections
551 \secref{sec:adaptation} and \secref{sec:further}.
553 \item For exhaustive syntax diagrams etc. you should visit the
554 Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
560 \begin{center}\fbox{\fbox{\begin{minipage}{8cm}
562 \begin{center}\textit{Happy proving, happy hacking!}\end{center}
564 \end{minipage}}}\end{center}
567 There is also a more ancient code generator in Isabelle by Stefan
568 Berghofer \cite{Berghofer-Nipkow:2002}. Although its
569 functionality is covered by the code generator presented here, it
570 will sometimes show up as an artifact. In case of ambiguity, we
571 will refer to the framework described here as \isa{generic\ code\ generator}, to the other as \isa{SML\ code\ generator}.
581 \isacommand{end}\isamarkupfalse%
593 %%% TeX-master: "root"