diff -r 3a1aef73b2b2 -r aea5d7fa7ef5 doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex Wed Mar 04 11:05:02 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,234 +0,0 @@ -% -\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: