--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/document/Further.tex Tue Mar 03 11:00:51 2009 +0100
@@ -0,0 +1,234 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Further}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Further\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Further issues \label{sec:further}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Further reading%
+}
+\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
+ contains exhaustive syntax diagrams.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Modules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave
+ out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over
+ different modules, where the module name space roughly is induced
+ by the \isa{Isabelle} theory name space.
+
+ Then sometimes the awkward situation occurs that dependencies between
+ definitions introduce cyclic dependencies between modules, which in the
+ \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation
+ you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
+
+ A solution is to declare module names explicitly.
+ Let use assume the three cyclically dependent
+ modules are named \emph{A}, \emph{B} and \emph{C}.
+ 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
+ at serialisation time.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Evaluation oracle%
+}
+\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%
+%
+\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}%
+\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.Ferrack}{\mbox{\isa{Ferrack}}} is
+ a good reference.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Imperative data structures%
+}
+\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
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: