--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Tue Oct 14 16:01:36 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Tue Oct 14 16:32:26 2008 +0200
@@ -23,11 +23,11 @@
\noindent In this section we will introduce means to \emph{adapt} the serialiser
to a specific target language, i.e.~to print program fragments
- in a way which accomodates \qt{already existing} ingredients of
+ in a way which accommodates \qt{already existing} ingredients of
a target language environment, for three reasons:
\begin{itemize}
- \item improving readability and aethetics of generated code
+ \item improving readability and aesthetics of generated code
\item gaining efficiency
\item interface with language parts which have no direct counterpart
in @{text "HOL"} (say, imperative data structures)
@@ -40,8 +40,8 @@
\item The safe configuration methods act uniformly on every target language,
whereas for adaption you have to treat each target language separate.
\item Application is extremely tedious since there is no abstraction
- which would allow for a static check, makeing it easy to produce garbage.
- \item More or less subtle erros can be introduced unconsciously.
+ which would allow for a static check, making it easy to produce garbage.
+ \item More or less subtle errors can be introduced unconsciously.
\end{itemize}
\noindent However, even if you ought refrain from setting up adaption
@@ -69,7 +69,7 @@
text {*
The @{theory HOL} @{theory Main} theory already provides a code
generator setup
- which should be suitable for most applications. Common extensions
+ which should be suitable for most applications. Common extensions
and modifications are available by certain theories of the @{text HOL}
library; beside being useful in applications, they may serve
as a tutorial for customising the code generator setup (see below
@@ -160,7 +160,7 @@
text {*
\noindent This still is not perfect: the parentheses
around the \qt{andalso} expression are superfluous.
- Though the serializer
+ Though the serialiser
by no means attempts to imitate the rich Isabelle syntax
framework, it provides some common idioms, notably
associative infixes with precedences which may be used here:
@@ -198,7 +198,7 @@
(SML "!((_),/ (_))")
text {*
- \noindent The initial bang ``@{verbatim "!"}'' tells the serializer
+ \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
never to put
parentheses around the whole expression (they are already present),
while the parentheses around argument place holders
@@ -261,7 +261,7 @@
text {*
\noindent The code generator would produce
- an additional instance, which of course is rejectedby the @{text Haskell}
+ an additional instance, which of course is rejected by the @{text Haskell}
compiler.
To suppress this additional instance, use
@{text "code_instance"}:
@@ -274,7 +274,7 @@
subsection {* Enhancing the target language context *}
text {*
- In rare cases it is neccessary to \emph{enrich} the context of a
+ In rare cases it is necessary to \emph{enrich} the context of a
target language; this is accomplished using the @{command "code_include"}
command:
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Tue Oct 14 16:01:36 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Tue Oct 14 16:32:26 2008 +0200
@@ -9,7 +9,7 @@
text {*
Do dive deeper into the issue of code generation, you should visit
the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
- constains exhaustive syntax diagrams.
+ contains exhaustive syntax diagrams.
*}
subsection {* Modules *}
@@ -31,7 +31,7 @@
Then, by stating
*}
-code_modulename SML
+code_modulename %quote SML
A ABC
B ABC
C ABC
@@ -44,12 +44,70 @@
subsection {* Evaluation oracle *}
+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
+ normal form with respect to the underlying code equations:
+*}
+
+value %quote "42 / (12 :: rat)"
+
+text {*
+ \noindent will display @{term "7 / (2 :: rat)"}.
+
+ The @{method eval} method tries to reduce a goal by code generation to @{term True}
+ and solves it in that case, but fails otherwise:
+*}
+
+lemma %quote "42 / (12 :: rat) = 7 / 2"
+ by %quote eval
+
+text {*
+ \noindent The soundness of the @{method eval} method depends crucially
+ on the correctness of the code generator; this is one of the reasons
+ why you should not use adaption (see \secref{sec:adaption}) frivolously.
+*}
+
subsection {* Code antiquotation *}
-subsection {* Creating new targets *}
+text {*
+ In scenarios involving techniques like reflection it is quite common
+ that code generated from a theory forms the basis for implementing
+ a proof procedure in @{text SML}. To facilitate interfacing of generated code
+ with system code, the code generator provides a @{text code} antiquotation:
+*}
+
+datatype %quote form = T | F | And form form | Or form form
-text {* extending targets, adding targets *}
+ML %quote {*
+ fun eval_form @{code T} = true
+ | eval_form @{code F} = false
+ | eval_form (@{code And} (p, q)) =
+ eval_form p andalso eval_form q
+ | eval_form (@{code Or} (p, q)) =
+ eval_form p orelse eval_form q;
+*}
+
+text {*
+ \noindent @{text code} takes as argument the name of a constant; after the
+ whole @{text SML} is read, the necessary code is generated transparently
+ and the corresponding constant names are inserted. This technique also
+ allows to use pattern matching on constructors stemming from compiled
+ @{text datatypes}.
+
+ For a less simplistic example, theory @{theory ReflectedFerrack} is
+ a good reference.
+*}
subsection {* Imperative data structures *}
+text {*
+ 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});
+ the framework described there is available in theory @{theory Imperative_HOL}.
+*}
+
end
--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Oct 14 16:01:36 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Oct 14 16:32:26 2008 +0200
@@ -11,7 +11,7 @@
@{command definition}/@{command primrec}/@{command fun}
statements are used for code generation. This default behaviour
can be changed, e.g. by providing different defining equations.
- All kinds of customization shown in this section is \emph{safe}
+ 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
correct.
@@ -222,7 +222,7 @@
text {*
Conceptually, any datatype is spanned by a set of
\emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"}
- where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is excactly the set of \emph{all}
+ where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all}
type variables in @{text "\<tau>"}. The HOL datatype package
by default registers any new datatype in the table
of datatypes, which may be inspected using
@@ -431,7 +431,7 @@
instance @{text "monotype \<Colon> eq"}, which itself requires
@{thm monotype_eq [no_vars]}; Haskell has no problem with mutually
recursive @{text instance} and @{text function} definitions,
- but the SML serializer does not support this.
+ but the SML serialiser does not support this.
In such cases, you have to provide your own equality equations
involving auxiliary constants. In our case,
@@ -498,7 +498,7 @@
this is not what the user expects). But such constants can also
be thought of as function definitions with no equations which
always fail, since there is never a successful pattern match
- on the left hand side. In order to categorize a constant into
+ on the left hand side. In order to categorise a constant into
that category explicitly, use @{command "code_abort"}:
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Oct 14 16:01:36 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Oct 14 16:32:26 2008 +0200
@@ -4,7 +4,8 @@
begin
ML {* no_document use_thys
- ["Efficient_Nat", "Code_Char_chr", "Product_ord"] *}
+ ["Efficient_Nat", "Code_Char_chr", "Product_ord", "Imperative_HOL",
+ "~~/src/HOL/Complex/ex/ReflectedFerrack"] *}
ML_val {* Code_Target.code_width := 74 *}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Tue Oct 14 16:01:36 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Tue Oct 14 16:32:26 2008 +0200
@@ -57,11 +57,11 @@
\noindent In this section we will introduce means to \emph{adapt} the serialiser
to a specific target language, i.e.~to print program fragments
- in a way which accomodates \qt{already existing} ingredients of
+ in a way which accommodates \qt{already existing} ingredients of
a target language environment, for three reasons:
\begin{itemize}
- \item improving readability and aethetics of generated code
+ \item improving readability and aesthetics of generated code
\item gaining efficiency
\item interface with language parts which have no direct counterpart
in \isa{HOL} (say, imperative data structures)
@@ -74,8 +74,8 @@
\item The safe configuration methods act uniformly on every target language,
whereas for adaption you have to treat each target language separate.
\item Application is extremely tedious since there is no abstraction
- which would allow for a static check, makeing it easy to produce garbage.
- \item More or less subtle erros can be introduced unconsciously.
+ which would allow for a static check, making it easy to produce garbage.
+ \item More or less subtle errors can be introduced unconsciously.
\end{itemize}
\noindent However, even if you ought refrain from setting up adaption
@@ -109,7 +109,7 @@
\begin{isamarkuptext}%
The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
generator setup
- which should be suitable for most applications. Common extensions
+ which should be suitable for most applications. Common extensions
and modifications are available by certain theories of the \isa{HOL}
library; beside being useful in applications, they may serve
as a tutorial for customising the code generator setup (see below
@@ -305,7 +305,7 @@
\begin{isamarkuptext}%
\noindent This still is not perfect: the parentheses
around the \qt{andalso} expression are superfluous.
- Though the serializer
+ Though the serialiser
by no means attempts to imitate the rich Isabelle syntax
framework, it provides some common idioms, notably
associative infixes with precedences which may be used here:%
@@ -421,7 +421,7 @@
\endisadelimquotett
%
\begin{isamarkuptext}%
-\noindent The initial bang ``\verb|!|'' tells the serializer
+\noindent The initial bang ``\verb|!|'' tells the serialiser
never to put
parentheses around the whole expression (they are already present),
while the parentheses around argument place holders
@@ -532,7 +532,7 @@
%
\begin{isamarkuptext}%
\noindent The code generator would produce
- an additional instance, which of course is rejectedby the \isa{Haskell}
+ an additional instance, which of course is rejected by the \isa{Haskell}
compiler.
To suppress this additional instance, use
\isa{code{\isacharunderscore}instance}:%
@@ -559,7 +559,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-In rare cases it is neccessary to \emph{enrich} the context of a
+In rare cases it is necessary to \emph{enrich} the context of a
target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
command:%
\end{isamarkuptext}%
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex Tue Oct 14 16:01:36 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex Tue Oct 14 16:32:26 2008 +0200
@@ -29,7 +29,7 @@
\begin{isamarkuptext}%
Do dive deeper into the issue of code generation, you should visit
the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
- constains exhaustive syntax diagrams.%
+ contains exhaustive syntax diagrams.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -54,11 +54,24 @@
Then, by stating%
\end{isamarkuptext}%
\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
\isacommand{code{\isacharunderscore}modulename}\isamarkupfalse%
\ SML\isanewline
\ \ A\ ABC\isanewline
\ \ B\ ABC\isanewline
\ \ C\ ABC%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\begin{isamarkuptext}%
we explicitly map all those modules on \emph{ABC},
resulting in an ad-hoc merge of this three modules
@@ -70,16 +83,120 @@
}
\isamarkuptrue%
%
+\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
+ normal form with respect to the underlying code equations:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{value}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent will display \isa{{\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}}.
+
+ The \hyperlink{method.eval}{\mbox{\isa{eval}}} method tries to reduce a goal by code generation to \isa{True}
+ and solves it in that case, but fails otherwise:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}\ {\isacharequal}\ {\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ eval%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The soundness of the \hyperlink{method.eval}{\mbox{\isa{eval}}} method depends crucially
+ on the correctness of the code generator; this is one of the reasons
+ why you should not use adaption (see \secref{sec:adaption}) frivolously.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Code antiquotation%
}
\isamarkuptrue%
%
-\isamarkupsubsection{Creating new targets%
-}
+\begin{isamarkuptext}%
+In scenarios involving techniques like reflection it is quite common
+ that code generated from a theory forms the basis for implementing
+ a proof procedure in \isa{SML}. To facilitate interfacing of generated code
+ with system code, the code generator provides a \isa{code} antiquotation:%
+\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{datatype}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\isanewline
+\isanewline
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ fun\ eval{\isacharunderscore}form\ %
+\isaantiq
+code\ T%
+\endisaantiq
+\ {\isacharequal}\ true\isanewline
+\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ %
+\isaantiq
+code\ F%
+\endisaantiq
+\ {\isacharequal}\ false\isanewline
+\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
+\isaantiq
+code\ And%
+\endisaantiq
+\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ andalso\ eval{\isacharunderscore}form\ q\isanewline
+\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
+\isaantiq
+code\ Or%
+\endisaantiq
+\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\begin{isamarkuptext}%
-extending targets, adding targets%
+\noindent \isa{code} takes as argument the name of a constant; after the
+ whole \isa{SML} is read, the necessary code is generated transparently
+ and the corresponding constant names are inserted. This technique also
+ allows to use pattern matching on constructors stemming from compiled
+ \isa{datatypes}.
+
+ For a less simplistic example, theory \hyperlink{theory.ReflectedFerrack}{\mbox{\isa{ReflectedFerrack}}} is
+ a good reference.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -87,6 +204,15 @@
}
\isamarkuptrue%
%
+\begin{isamarkuptext}%
+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});
+ the framework described there is available in theory \hyperlink{theory.Imperative-HOL}{\mbox{\isa{Imperative{\isacharunderscore}HOL}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Tue Oct 14 16:01:36 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Tue Oct 14 16:32:26 2008 +0200
@@ -31,7 +31,7 @@
\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
statements are used for code generation. This default behaviour
can be changed, e.g. by providing different defining equations.
- All kinds of customization shown in this section is \emph{safe}
+ 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
correct.%
@@ -507,7 +507,7 @@
\begin{isamarkuptext}%
Conceptually, any datatype is spanned by a set of
\emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
- where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all}
+ where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all}
type variables in \isa{{\isasymtau}}. The HOL datatype package
by default registers any new datatype in the table
of datatypes, which may be inspected using
@@ -993,7 +993,7 @@
instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
\isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually
recursive \isa{instance} and \isa{function} definitions,
- but the SML serializer does not support this.
+ but the SML serialiser does not support this.
In such cases, you have to provide your own equality equations
involving auxiliary constants. In our case,
@@ -1170,7 +1170,7 @@
this is not what the user expects). But such constants can also
be thought of as function definitions with no equations which
always fail, since there is never a successful pattern match
- on the left hand side. In order to categorize a constant into
+ 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}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/manual.bib Tue Oct 14 16:01:36 2008 +0200
+++ b/doc-src/manual.bib Tue Oct 14 16:32:26 2008 +0200
@@ -232,6 +232,13 @@
pages = {38--53}
}
+@InProceedings{bulwahn-et-al:2008:imperative,
+ author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
+ title = {Imperative Functional Programming with {Isabelle/HOL}},
+ crossref = {tphols2008},
+}
+% pages = {38--53}
+
@Article{ban89,
author = {M. Burrows and M. Abadi and R. M. Needham},
title = {A Logic of Authentication},
@@ -1595,6 +1602,15 @@
volume = 4732,
year = 2007}
+@Proceedings{tphols2008,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
+ publisher = Springer,
+ series = LNCS,
+ year = 2008}
+% editor =
+% volume = 4732,
+
@unpublished{classes_modules,
title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
author = {Stefan Wehr et. al.}