diff -r 2775062fd3a9 -r 2f4684e2ea95 doc-src/Codegen/Thy/document/Further.tex --- /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: