--- a/doc-src/Codegen/Thy/Adaptation.thy Mon Dec 21 10:40:14 2009 +0100
+++ b/doc-src/Codegen/Thy/Adaptation.thy Mon Dec 21 16:49:04 2009 +0000
@@ -38,10 +38,10 @@
\begin{itemize}
\item The safe configuration methods act uniformly on every target language,
- whereas for adaptation you have to treat each target language separate.
+ whereas for adaptation you have to treat each target language separately.
\item Application is extremely tedious since there is no abstraction
which would allow for a static check, making it easy to produce garbage.
- \item More or less subtle errors can be introduced unconsciously.
+ \item Subtle errors can be introduced unconsciously.
\end{itemize}
\noindent However, even if you ought refrain from setting up adaptation
--- a/doc-src/Codegen/Thy/Further.thy Mon Dec 21 10:40:14 2009 +0100
+++ b/doc-src/Codegen/Thy/Further.thy Mon Dec 21 16:49:04 2009 +0000
@@ -7,8 +7,8 @@
subsection {* Further reading *}
text {*
- Do dive deeper into the issue of code generation, you should visit
- the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
+ To dive deeper into the issue of code generation, you should visit
+ the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}, which
contains exhaustive syntax diagrams.
*}
@@ -36,7 +36,7 @@
B ABC
C ABC
-text {*
+text {*\noindent
we explicitly map all those modules on \emph{ABC},
resulting in an ad-hoc merge of this three modules
at serialisation time.
@@ -47,7 +47,7 @@
text {*
Code generation may also be used to \emph{evaluate} expressions
(using @{text SML} as target language of course).
- For instance, the @{command value} allows to reduce an expression to a
+ For instance, the @{command value} reduces an expression to a
normal form with respect to the underlying code equations:
*}
@@ -106,7 +106,7 @@
If you consider imperative data structures as inevitable for a specific
application, you should consider
\emph{Imperative Functional Programming with Isabelle/HOL}
- (\cite{bulwahn-et-al:2008:imperative});
+ \cite{bulwahn-et-al:2008:imperative};
the framework described there is available in theory @{theory Imperative_HOL}.
*}
--- a/doc-src/Codegen/Thy/Introduction.thy Mon Dec 21 10:40:14 2009 +0100
+++ b/doc-src/Codegen/Thy/Introduction.thy Mon Dec 21 16:49:04 2009 +0000
@@ -7,25 +7,24 @@
text {*
This tutorial introduces a generic code generator for the
@{text Isabelle} system.
- Generic in the sense that the
- \qn{target language} for which code shall ultimately be
- generated is not fixed but may be an arbitrary state-of-the-art
- functional programming language (currently, the implementation
+ The
+ \qn{target language} for which code is
+ generated is not fixed, but may be one of several
+ functional programming languages (currently, the implementation
supports @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml} and @{text Haskell}
\cite{haskell-revised-report}).
Conceptually the code generator framework is part
of Isabelle's @{theory Pure} meta logic framework; the logic
- @{theory HOL} which is an extension of @{theory Pure}
+ @{theory HOL} \cite{isa-tutorial}, which is an extension of @{theory Pure},
already comes with a reasonable framework setup and thus provides
- a good working horse for raising code-generation-driven
+ a good basis for creating code-generation-driven
applications. So, we assume some familiarity and experience
with the ingredients of the @{theory HOL} distribution theories.
- (see also \cite{isa-tutorial}).
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
+ in most cases, while allowing for detailed customisation.
+ This can be seen 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:adaptation}) is dedicated to the matter of
@@ -58,7 +57,7 @@
Inside @{theory HOL}, the @{command datatype} and
@{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.
+ transforms 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:
*}
@@ -102,7 +101,7 @@
module_name Example file "examples/"
text {*
- \noindent This is how the corresponding code in @{text Haskell} looks like:
+ \noindent This is the corresponding code in @{text Haskell}:
*}
text %quote {*@{code_stmts empty enqueue dequeue (Haskell)}*}
@@ -117,7 +116,7 @@
text {*
What you have seen so far should be already enough in a lot of cases. If you
are content with this, you can quit reading here. Anyway, in order to customise
- and adapt the code generator, it is inevitable to gain some understanding
+ and adapt the code generator, it is necessary to gain some understanding
how it works.
\begin{figure}[h]
@@ -142,16 +141,15 @@
\begin{itemize}
- \item Starting point is a collection of raw code equations in a
- theory; due to proof irrelevance it is not relevant where they
- stem from but typically they are either descendant of specification
- tools or explicit proofs by the user.
+ \item The starting point is a collection of raw code equations in a
+ theory. It is not relevant where they
+ stem from, but typically they were either produced by specification
+ tools or proved explicitly by the user.
- \item Before these raw code equations are continued
- with, they can be subjected to theorem transformations. This
- \qn{preprocessor} is an interface which allows to apply the full
+ \item These raw code equations can be subjected to theorem transformations. This
+ \qn{preprocessor} can apply the full
expressiveness of ML-based theorem transformations to code
- generation. The result of the preprocessing step is a
+ generation. The result of preprocessing is a
structured collection of code equations.
\item These code equations are \qn{translated} to a program in an
--- a/doc-src/Codegen/Thy/Program.thy Mon Dec 21 10:40:14 2009 +0100
+++ b/doc-src/Codegen/Thy/Program.thy Mon Dec 21 16:49:04 2009 +0000
@@ -8,12 +8,11 @@
text {*
We have already seen how by default equations stemming from
- @{command definition}/@{command primrec}/@{command fun}
+ @{command definition}, @{command primrec} and @{command fun}
statements are used for code generation. This default behaviour
- can be changed, e.g. by providing different code equations.
- All kinds of customisation shown in this section is \emph{safe}
- in the sense that the user does not have to worry about
- correctness -- all programs generatable that way are partially
+ can be changed, e.g.\ by providing different code equations.
+ The customisations shown in this section are \emph{safe}
+ as regards correctness: all programs that can be generated are partially
correct.
*}
@@ -52,7 +51,7 @@
As told in \secref{sec:concept}, code generation is based
on a structured collection of code theorems.
- For explorative purpose, this collection
+ This collection
may be inspected using the @{command code_thms} command:
*}
@@ -128,7 +127,7 @@
"bexp n = pow n (Suc (Suc 0))"
text {*
- \noindent The corresponding code:
+ \noindent The corresponding code in Haskell uses that language's native classes:
*}
text %quote {*@{code_stmts bexp (Haskell)}*}
@@ -141,7 +140,7 @@
text %quote {*@{code_stmts bexp (SML)}*}
text {*
- \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
+ \noindent Note the parameters with trailing underscore (@{verbatim "A_"}),
which are the dictionary parameters.
*}
@@ -153,14 +152,14 @@
out: \emph{preprocessing}. In essence, the preprocessor
consists of two components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} allows to employ the full generality of the
+ The \emph{simpset} can apply the full generality of the
Isabelle simplifier. Due to the interpretation of theorems as code
equations, rewrites are applied to the right hand side and the
arguments of the left hand side of an equation, but never to the
constant heading the left hand side. An important special case are
- \emph{unfold theorems} which may be declared and undeclared using
+ \emph{unfold theorems}, which may be declared and removed using
the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
- attribute respectively.
+ attribute, respectively.
Some common applications:
*}
@@ -232,7 +231,7 @@
queue example given in \secref{sec:intro}. The amortised
representation is convenient for generating code but exposes its
\qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here a simple, straightforward
+ theorems about it. Therefore, here is a simple, straightforward
representation of queues:
*}
@@ -402,13 +401,12 @@
text {*
Observe that on the right hand side of the definition of @{const
- "strict_dequeue'"} the constant @{const empty_queue} occurs
- which is unspecified.
+ "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
Normally, if constants without any code equations occur in a
program, the code generator complains (since in most cases this is
- not what the user expects). But such constants can also be thought
- of as function definitions with no equations which always fail,
+ indeed an error). But such constants can also be thought
+ of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
explicitly, use @{command "code_abort"}:
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Mon Dec 21 10:40:14 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Mon Dec 21 16:49:04 2009 +0000
@@ -72,10 +72,10 @@
\begin{itemize}
\item The safe configuration methods act uniformly on every target language,
- whereas for adaptation you have to treat each target language separate.
+ whereas for adaptation you have to treat each target language separately.
\item Application is extremely tedious since there is no abstraction
which would allow for a static check, making it easy to produce garbage.
- \item More or less subtle errors can be introduced unconsciously.
+ \item Subtle errors can be introduced unconsciously.
\end{itemize}
\noindent However, even if you ought refrain from setting up adaptation
@@ -229,24 +229,30 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~datatype boola = True | False\\
+\hspace*{0pt} ~val anda :~boola -> boola -> boola\\
+\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\
+\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> boola\\
+\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> boola\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
\hspace*{0pt}datatype boola = True | False;\\
\hspace*{0pt}\\
\hspace*{0pt}fun anda p True = p\\
-\hspace*{0pt} ~| anda p False = False\\
-\hspace*{0pt} ~| anda True p = p\\
-\hspace*{0pt} ~| anda False p = False;\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda p False = False\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda True p = p\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda False p = False;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
+\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = False\\
+\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = True;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = anda {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat k n{\char123}{\char92}isacharparenright{\char125}~{\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat n l{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -312,17 +318,21 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
+\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
+\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = true;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat k n{\char123}{\char92}isacharparenright{\char125}~andalso {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat n l{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -369,17 +379,21 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
+\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
+\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = true;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
+\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
--- a/doc-src/Codegen/Thy/document/Further.tex Mon Dec 21 10:40:14 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Mon Dec 21 16:49:04 2009 +0000
@@ -27,8 +27,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Do dive deeper into the issue of code generation, you should visit
- the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
+To dive deeper into the issue of code generation, you should visit
+ the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}, which
contains exhaustive syntax diagrams.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -73,7 +73,8 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-we explicitly map all those modules on \emph{ABC},
+\noindent
+ we explicitly map all those modules on \emph{ABC},
resulting in an ad-hoc merge of this three modules
at serialisation time.%
\end{isamarkuptext}%
@@ -86,7 +87,7 @@
\begin{isamarkuptext}%
Code generation may also be used to \emph{evaluate} expressions
(using \isa{SML} as target language of course).
- For instance, the \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} allows to reduce an expression to a
+ For instance, the \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} reduces an expression to a
normal form with respect to the underlying code equations:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -219,7 +220,7 @@
If you consider imperative data structures as inevitable for a specific
application, you should consider
\emph{Imperative Functional Programming with Isabelle/HOL}
- (\cite{bulwahn-et-al:2008:imperative});
+ \cite{bulwahn-et-al:2008:imperative};
the framework described there is available in theory \hyperlink{theory.Imperative-HOL}{\mbox{\isa{Imperative{\isacharunderscore}HOL}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Dec 21 10:40:14 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Mon Dec 21 16:49:04 2009 +0000
@@ -25,25 +25,24 @@
\begin{isamarkuptext}%
This tutorial introduces a generic code generator for the
\isa{Isabelle} system.
- Generic in the sense that the
- \qn{target language} for which code shall ultimately be
- generated is not fixed but may be an arbitrary state-of-the-art
- functional programming language (currently, the implementation
+ The
+ \qn{target language} for which code is
+ generated is not fixed, but may be one of several
+ functional programming languages (currently, the implementation
supports \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and \isa{Haskell}
\cite{haskell-revised-report}).
Conceptually the code generator framework is part
of Isabelle's \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} meta logic framework; the logic
- \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} which is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}
+ \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial}, which is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}},
already comes with a reasonable framework setup and thus provides
- a good working horse for raising code-generation-driven
+ a good basis for creating code-generation-driven
applications. So, we assume some familiarity and experience
with the ingredients of the \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} distribution theories.
- (see also \cite{isa-tutorial}).
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
+ in most cases, while allowing for detailed customisation.
+ This can be seen 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:adaptation}) is dedicated to the matter of
@@ -78,7 +77,7 @@
Inside \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and
\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form
the core of a functional programming language. The default code generator setup
- allows to turn those into functional programs immediately.
+ transforms 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:%
\end{isamarkuptext}%
@@ -147,31 +146,38 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~val foldl :~{\char123}{\char92}isacharparenleft{\char125}'a -> 'b -> 'a{\char123}{\char92}isacharparenright{\char125}~-> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val rev :~'a list -> 'a list\\
+\hspace*{0pt} ~val list{\char95}case :~'a -> {\char123}{\char92}isacharparenleft{\char125}'b -> 'b list -> 'a{\char123}{\char92}isacharparenright{\char125}~-> 'b list -> 'a\\
+\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list\\
+\hspace*{0pt} ~val empty :~'a queue\\
+\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
+\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~foldl f a {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= foldl f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun rev xs = foldl {\char123}{\char92}isacharparenleft{\char125}fn xsa => fn x => x ::~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\
-\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\
+\hspace*{0pt}fun list{\char123}{\char92}isacharunderscore{\char125}case f1 f2 {\char123}{\char92}isacharparenleft{\char125}a ::~lista{\char123}{\char92}isacharparenright{\char125}~= f2 a lista\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~list{\char123}{\char92}isacharunderscore{\char125}case f1 f2 [] = f1;\\
\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
+\hspace*{0pt}val empty :~'a queue = AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
-\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\
+\hspace*{0pt}fun dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (NONE,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~y ::~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}v ::~va{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~~~let\\
-\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
+\hspace*{0pt} ~~~~~val y ::~ys = rev {\char123}{\char92}isacharparenleft{\char125}v ::~va{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt} ~~~in\\
-\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\
+\hspace*{0pt} ~~~~~(SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
\hspace*{0pt} ~~~end;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
+\hspace*{0pt}fun enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -213,7 +219,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This is how the corresponding code in \isa{Haskell} looks like:%
+\noindent This is the corresponding code in \isa{Haskell}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -228,16 +234,15 @@
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}\\
-\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\
+\hspace*{0pt}foldla ::~forall a b.~{\char123}{\char92}isacharparenleft{\char125}a -> b -> a{\char123}{\char92}isacharparenright{\char125}~-> a -> [b] -> a;\\
\hspace*{0pt}foldla f a [] = a;\\
-\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
+\hspace*{0pt}foldla f a {\char123}{\char92}isacharparenleft{\char125}x :~xs{\char123}{\char92}isacharparenright{\char125}~= foldla f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
\hspace*{0pt}\\
\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\
-\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
+\hspace*{0pt}rev xs = foldla {\char123}{\char92}isacharparenleft{\char125}{\char92}~xsa x -> x :~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\
-\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
+\hspace*{0pt}list{\char95}case ::~forall a b.~a -> {\char123}{\char92}isacharparenleft{\char125}b -> [b] -> a{\char123}{\char92}isacharparenright{\char125}~-> [b] -> a;\\
+\hspace*{0pt}list{\char95}case f1 f2 {\char123}{\char92}isacharparenleft{\char125}a :~list{\char123}{\char92}isacharparenright{\char125}~= f2 a list;\\
\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
\hspace*{0pt}\\
\hspace*{0pt}data Queue a = AQueue [a] [a];\\
@@ -246,15 +251,15 @@
\hspace*{0pt}empty = AQueue [] [];\\
\hspace*{0pt}\\
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
-\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue [] []{\char123}{\char92}isacharparenright{\char125}~= (Nothing,~AQueue [] []);\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}v :~va{\char123}{\char92}isacharparenright{\char125}~[]{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
+\hspace*{0pt} ~~~{\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}~= rev {\char123}{\char92}isacharparenleft{\char125}v :~va{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
\hspace*{0pt}\\
\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
-\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
+\hspace*{0pt}enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue xs ys{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x :~xs{\char123}{\char92}isacharparenright{\char125}~ys;\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
@@ -280,7 +285,7 @@
\begin{isamarkuptext}%
What you have seen so far should be already enough in a lot of cases. If you
are content with this, you can quit reading here. Anyway, in order to customise
- and adapt the code generator, it is inevitable to gain some understanding
+ and adapt the code generator, it is necessary to gain some understanding
how it works.
\begin{figure}[h]
@@ -305,16 +310,15 @@
\begin{itemize}
- \item Starting point is a collection of raw code equations in a
- theory; due to proof irrelevance it is not relevant where they
- stem from but typically they are either descendant of specification
- tools or explicit proofs by the user.
+ \item The starting point is a collection of raw code equations in a
+ theory. It is not relevant where they
+ stem from, but typically they were either produced by specification
+ tools or proved explicitly by the user.
- \item Before these raw code equations are continued
- with, they can be subjected to theorem transformations. This
- \qn{preprocessor} is an interface which allows to apply the full
+ \item These raw code equations can be subjected to theorem transformations. This
+ \qn{preprocessor} can apply the full
expressiveness of ML-based theorem transformations to code
- generation. The result of the preprocessing step is a
+ generation. The result of preprocessing is a
structured collection of code equations.
\item These code equations are \qn{translated} to a program in an
--- a/doc-src/Codegen/Thy/document/Program.tex Mon Dec 21 10:40:14 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex Mon Dec 21 16:49:04 2009 +0000
@@ -28,12 +28,11 @@
%
\begin{isamarkuptext}%
We have already seen how by default equations stemming from
- \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
+ \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
statements are used for code generation. This default behaviour
- can be changed, e.g. by providing different code equations.
- All kinds of customisation shown in this section is \emph{safe}
- in the sense that the user does not have to worry about
- correctness -- all programs generatable that way are partially
+ can be changed, e.g.\ by providing different code equations.
+ The customisations shown in this section are \emph{safe}
+ as regards correctness: all programs that can be generated are partially
correct.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -88,10 +87,10 @@
\isatypewriter%
\noindent%
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue (AQueue xs []) =\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\
-\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%
+\hspace*{0pt} ~~~else dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue [] {\char123}{\char92}isacharparenleft{\char125}rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -112,7 +111,7 @@
As told in \secref{sec:concept}, code generation is based
on a structured collection of code theorems.
- For explorative purpose, this collection
+ This collection
may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -260,7 +259,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The corresponding code:%
+\noindent The corresponding code in Haskell uses that language's native classes:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -275,23 +274,22 @@
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}\\
\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
\hspace*{0pt}\\
\hspace*{0pt}class Semigroup a where {\char123}\\
\hspace*{0pt} ~mult ::~a -> a -> a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
+\hspace*{0pt}class {\char123}{\char92}isacharparenleft{\char125}Semigroup a{\char123}{\char92}isacharparenright{\char125}~=> Monoid a where {\char123}\\
\hspace*{0pt} ~neutral ::~a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
+\hspace*{0pt}pow ::~forall a.~{\char123}{\char92}isacharparenleft{\char125}Monoid a{\char123}{\char92}isacharparenright{\char125}~=> Nat -> a -> a;\\
\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
-\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
+\hspace*{0pt}pow {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~a = mult a {\char123}{\char92}isacharparenleft{\char125}pow n a{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
-\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
+\hspace*{0pt}plus{\char95}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
\hspace*{0pt}\\
\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
@@ -299,7 +297,7 @@
\hspace*{0pt}\\
\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
-\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
+\hspace*{0pt}mult{\char95}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}mult{\char95}nat m n{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}instance Semigroup Nat where {\char123}\\
\hspace*{0pt} ~mult = mult{\char95}nat;\\
@@ -310,7 +308,7 @@
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}bexp ::~Nat -> Nat;\\
-\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}bexp n = pow n {\char123}{\char92}isacharparenleft{\char125}Suc {\char123}{\char92}isacharparenleft{\char125}Suc Zero{\char95}nat{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
@@ -338,35 +336,48 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~type 'a semigroup\\
+\hspace*{0pt} ~val mult :~'a semigroup{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> 'a\\
+\hspace*{0pt} ~type 'a monoid\\
+\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a semigroup\\
+\hspace*{0pt} ~val neutral :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a\\
+\hspace*{0pt} ~val pow :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~nat -> 'a -> 'a\\
+\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
+\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
+\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
+\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
+\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
+\hspace*{0pt} ~val bexp :~nat -> nat\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
-\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
+\hspace*{0pt}type 'a semigroup = {\char123}{\char92}isacharbraceleft{\char125}mult :~'a -> 'a -> 'a{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
+\hspace*{0pt}val mult = {\char35}mult :~'a semigroup{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> 'a;\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}semigroup{\char95}monoid A{\char95};\\
-\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
+\hspace*{0pt}type 'a monoid = {\char123}{\char92}isacharbraceleft{\char125}semigroup{\char95}monoid :~'a semigroup{\char123}{\char92}isacharcomma{\char125}~neutral :~'a{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
+\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a semigroup;\\
+\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
-\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~pow A{\char95}~{\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~a = mult {\char123}{\char92}isacharparenleft{\char125}semigroup{\char95}monoid A{\char95}{\char123}{\char92}isacharparenright{\char125}~a {\char123}{\char92}isacharparenleft{\char125}pow A{\char95}~n a{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
-\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}fun plus{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~plus{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = n;\\
\hspace*{0pt}\\
\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
-\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
+\hspace*{0pt}fun mult{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = Zero{\char95}nat\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~mult{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}mult{\char95}nat m n{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
+\hspace*{0pt}val semigroup{\char95}nat = {\char123}{\char92}isacharbraceleft{\char125}mult = mult{\char95}nat{\char123}{\char92}isacharbraceright{\char125}~:~nat semigroup;\\
\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
+\hspace*{0pt}val monoid{\char95}nat = {\char123}{\char92}isacharbraceleft{\char125}semigroup{\char95}monoid = semigroup{\char95}nat{\char123}{\char92}isacharcomma{\char125}~neutral = neutral{\char95}nat{\char123}{\char92}isacharbraceright{\char125}\\
\hspace*{0pt} ~:~nat monoid;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}Suc {\char123}{\char92}isacharparenleft{\char125}Suc Zero{\char95}nat{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -380,7 +391,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Note the parameters with trailing underscore (\verb|A_|)
+\noindent Note the parameters with trailing underscore (\verb|A_|),
which are the dictionary parameters.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -395,14 +406,14 @@
out: \emph{preprocessing}. In essence, the preprocessor
consists of two components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} allows to employ the full generality of the
+ The \emph{simpset} can apply the full generality of the
Isabelle simplifier. Due to the interpretation of theorems as code
equations, rewrites are applied to the right hand side and the
arguments of the left hand side of an equation, but never to the
constant heading the left hand side. An important special case are
- \emph{unfold theorems} which may be declared and undeclared using
+ \emph{unfold theorems}, which may be declared and removed using
the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
- attribute respectively.
+ attribute, respectively.
Some common applications:%
\end{isamarkuptext}%
@@ -515,7 +526,7 @@
queue example given in \secref{sec:intro}. The amortised
representation is convenient for generating code but exposes its
\qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here a simple, straightforward
+ theorems about it. Therefore, here is a simple, straightforward
representation of queues:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -654,27 +665,34 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~val foldl :~{\char123}{\char92}isacharparenleft{\char125}'a -> 'b -> 'a{\char123}{\char92}isacharparenright{\char125}~-> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val rev :~'a list -> 'a list\\
+\hspace*{0pt} ~val null :~'a list -> bool\\
+\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list\\
+\hspace*{0pt} ~val empty :~'a queue\\
+\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
+\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~foldl f a {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= foldl f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun rev xs = foldl {\char123}{\char92}isacharparenleft{\char125}fn xsa => fn x => x ::~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
\hspace*{0pt}\\
\hspace*{0pt}fun null [] = true\\
-\hspace*{0pt} ~| null (x ::~xs) = false;\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~null {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= false;\\
\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
+\hspace*{0pt}val empty :~'a queue = AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
-\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
-\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
+\hspace*{0pt}fun dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~y ::~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~=\\
+\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~~~~~else dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});\\
\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
+\hspace*{0pt}fun enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -759,23 +777,29 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~type 'a eq\\
+\hspace*{0pt} ~val eq :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool\\
+\hspace*{0pt} ~val eqa :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool\\
+\hspace*{0pt} ~val member :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a list -> bool\\
+\hspace*{0pt} ~val collect{\char95}duplicates :\\
+\hspace*{0pt} ~~~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a list -> 'a list -> 'a list -> 'a list\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
-\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
+\hspace*{0pt}type 'a eq = {\char123}{\char92}isacharbraceleft{\char125}eq :~'a -> 'a -> bool{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
+\hspace*{0pt}val eq = {\char35}eq :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool;\\
\hspace*{0pt}\\
\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
\hspace*{0pt}\\
\hspace*{0pt}fun member A{\char95}~x [] = false\\
-\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~member A{\char95}~x {\char123}{\char92}isacharparenleft{\char125}y ::~ys{\char123}{\char92}isacharparenright{\char125}~= eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
-\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
+\hspace*{0pt}fun collect{\char123}{\char92}isacharunderscore{\char125}duplicates A{\char95}~xs ys [] = xs\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~collect{\char123}{\char92}isacharunderscore{\char125}duplicates A{\char95}~xs ys {\char123}{\char92}isacharparenleft{\char125}z ::~zs{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
-\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
-\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
+\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs {\char123}{\char92}isacharparenleft{\char125}z ::~ys{\char123}{\char92}isacharparenright{\char125}~zs)\\
+\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~{\char123}{\char92}isacharparenleft{\char125}z ::~xs{\char123}{\char92}isacharparenright{\char125}~{\char123}{\char92}isacharparenleft{\char125}z ::~ys{\char123}{\char92}isacharparenright{\char125}~zs);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -851,11 +875,11 @@
\isatypewriter%
\noindent%
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
+\hspace*{0pt} ~~~{\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}~= rev xs;\\
\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
+\hspace*{0pt}strict{\char95}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (y,~AQueue xs ys);%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -900,13 +924,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs
- which is unspecified.
+Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
Normally, if constants without any code equations occur in a
program, the code generator complains (since in most cases this is
- not what the user expects). But such constants can also be thought
- of as function definitions with no equations which always fail,
+ indeed an error). But such constants can also be thought
+ of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
@@ -946,10 +969,10 @@
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
\hspace*{0pt}\\
\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
+\hspace*{0pt} ~~~else strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue [] {\char123}{\char92}isacharparenleft{\char125}rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});%
\end{isamarkuptext}%
\isamarkuptrue%
%