--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Wed Oct 01 12:18:18 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Wed Oct 01 13:33:54 2008 +0200
@@ -28,19 +28,21 @@
The code generator aims to be usable with no further ado
in most cases while allowing for detailed customisation.
This manifests in the structure of this tutorial: after a short
- conceptual introduction with an example \secref{sec:intro},
- we discuss the generic customisation facilities \secref{sec:program}.
- A further section \secref{sec:adaption} is dedicated to the matter of
+ conceptual introduction with an example (\secref{sec:intro}),
+ we discuss the generic customisation facilities (\secref{sec:program}).
+ A further section (\secref{sec:adaption}) is dedicated to the matter of
\qn{adaption} to specific target language environments. After some
- further issues \secref{sec:further} we conclude with an overview
- of some ML programming interfaces \secref{sec:ml}.
+ further issues (\secref{sec:further}) we conclude with an overview
+ of some ML programming interfaces (\secref{sec:ml}).
\begin{warn}
Ultimately, the code generator which this tutorial deals with
- is supposed to replace the already established code generator
+ is supposed to replace the existing code generator
by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
So, for the moment, there are two distinct code generators
- in Isabelle.
+ in Isabelle. In case of ambiguity, we will refer to the framework
+ described here as @{text "generic code generator"}, to the
+ other as @{text "SML code generator"}.
Also note that while the framework itself is
object-logic independent, only @{theory HOL} provides a reasonable
framework setup.
@@ -59,7 +61,6 @@
@{command definition}/@{command primrec}/@{command fun} declarations form
the core of a functional programming language. The default code generator setup
allows to turn those into functional programs immediately.
-
This means that \qt{naive} code generation can proceed without further ado.
For example, here a simple \qt{implementation} of amortised queues:
*}
@@ -75,11 +76,13 @@
fun %quoteme dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
"dequeue (Queue [] []) = (None, Queue [] [])"
| "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)"
- | "dequeue (Queue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, Queue [] ys))"
+ | "dequeue (Queue xs []) =
+ (case rev xs of y # ys \<Rightarrow> (Some y, Queue [] ys))"
text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
-export_code %quoteme empty dequeue enqueue in SML module_name Example file "examples/example.ML"
+export_code %quoteme empty dequeue enqueue in SML
+ module_name Example file "examples/example.ML"
text {* \noindent resulting in the following code: *}
@@ -88,7 +91,7 @@
text {*
\noindent The @{command export_code} command takes a space-separated list of
constants for which code shall be generated; anything else needed for those
- is added implicitly. Then follows by a target language identifier
+ is added implicitly. Then follows a target language identifier
(@{text SML}, @{text OCaml} or @{text Haskell}) and a freely chosen module name.
A file name denotes the destination to store the generated code. Note that
the semantics of the destination depends on the target language: for
@@ -97,7 +100,8 @@
(with extension @{text ".hs"}) is written:
*}
-export_code %quoteme empty dequeue enqueue in Haskell module_name Example file "examples/"
+export_code %quoteme empty dequeue enqueue in Haskell
+ module_name Example file "examples/"
text {*
\noindent This is how the corresponding code in @{text Haskell} looks like:
@@ -107,10 +111,10 @@
text {*
\noindent This demonstrates the basic usage of the @{command export_code} command;
- for more details see \secref{sec:serializer}.
+ for more details see \secref{sec:further}.
*}
-subsection {* Code generator architecture *}
+subsection {* Code generator architecture \label{sec:concept} *}
text {*
What you have seen so far should be already enough in a lot of cases. If you
@@ -125,10 +129,6 @@
\label{fig:arch}
\end{figure}
- The code generator itself consists of three major components
- which operate sequentially, i.e. the result of one is the input
- of the next in the chain, see diagram \ref{fig:arch}:
-
The code generator employs a notion of executability
for three foundational executable ingredients known
from functional programming:
@@ -138,8 +138,10 @@
(an equation headed by a constant @{text f} with arguments
@{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}).
Code generation aims to turn defining equations
- into a functional program by running through the following
- process:
+ into a functional program. This is achieved by three major
+ components which operate sequentially, i.e. the result of one is
+ the input
+ of the next in the chain, see diagram \ref{fig:arch}:
\begin{itemize}
@@ -165,7 +167,10 @@
of defining equations.
\item These defining equations are \qn{translated} to a program
- in an abstract intermediate language.
+ in an abstract intermediate language. Think of it as a kind
+ of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
+ (for datatypes), @{text fun} (stemming from defining equations),
+ also @{text class} and @{text inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into concrete
source code of a target language.