doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex
changeset 28447 df77ed974a78
child 28593 f087237af65d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex	Wed Oct 01 13:33:54 2008 +0200
     1.3 @@ -0,0 +1,108 @@
     1.4 +%
     1.5 +\begin{isabellebody}%
     1.6 +\def\isabellecontext{Further}%
     1.7 +%
     1.8 +\isadelimtheory
     1.9 +%
    1.10 +\endisadelimtheory
    1.11 +%
    1.12 +\isatagtheory
    1.13 +\isacommand{theory}\isamarkupfalse%
    1.14 +\ Further\isanewline
    1.15 +\isakeyword{imports}\ Setup\isanewline
    1.16 +\isakeyword{begin}%
    1.17 +\endisatagtheory
    1.18 +{\isafoldtheory}%
    1.19 +%
    1.20 +\isadelimtheory
    1.21 +%
    1.22 +\endisadelimtheory
    1.23 +%
    1.24 +\isamarkupsection{Further issues \label{sec:further}%
    1.25 +}
    1.26 +\isamarkuptrue%
    1.27 +%
    1.28 +\isamarkupsubsection{Further reading%
    1.29 +}
    1.30 +\isamarkuptrue%
    1.31 +%
    1.32 +\begin{isamarkuptext}%
    1.33 +Do dive deeper into the issue of code generation, you should visit
    1.34 +  the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
    1.35 +  constains exhaustive syntax diagrams.%
    1.36 +\end{isamarkuptext}%
    1.37 +\isamarkuptrue%
    1.38 +%
    1.39 +\isamarkupsubsection{Modules%
    1.40 +}
    1.41 +\isamarkuptrue%
    1.42 +%
    1.43 +\begin{isamarkuptext}%
    1.44 +When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave
    1.45 +  out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part;  then code is distributed over
    1.46 +  different modules, where the module name space roughly is induced
    1.47 +  by the \isa{Isabelle} theory namespace.
    1.48 +
    1.49 +  Then sometimes the awkward situation occurs that dependencies between
    1.50 +  definitions introduce cyclic dependencies between modules, which in the
    1.51 +  \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation
    1.52 +  you are using,  while for \isa{SML}/\isa{OCaml} code generation is not possible.
    1.53 +
    1.54 +  A solution is to declare module names explicitly.
    1.55 +  Let use assume the three cyclically dependent
    1.56 +  modules are named \emph{A}, \emph{B} and \emph{C}.
    1.57 +  Then, by stating%
    1.58 +\end{isamarkuptext}%
    1.59 +\isamarkuptrue%
    1.60 +\isacommand{code{\isacharunderscore}modulename}\isamarkupfalse%
    1.61 +\ SML\isanewline
    1.62 +\ \ A\ ABC\isanewline
    1.63 +\ \ B\ ABC\isanewline
    1.64 +\ \ C\ ABC%
    1.65 +\begin{isamarkuptext}%
    1.66 +we explicitly map all those modules on \emph{ABC},
    1.67 +  resulting in an ad-hoc merge of this three modules
    1.68 +  at serialisation time.%
    1.69 +\end{isamarkuptext}%
    1.70 +\isamarkuptrue%
    1.71 +%
    1.72 +\isamarkupsubsection{Evaluation oracle%
    1.73 +}
    1.74 +\isamarkuptrue%
    1.75 +%
    1.76 +\isamarkupsubsection{Code antiquotation%
    1.77 +}
    1.78 +\isamarkuptrue%
    1.79 +%
    1.80 +\isamarkupsubsection{Creating new targets%
    1.81 +}
    1.82 +\isamarkuptrue%
    1.83 +%
    1.84 +\begin{isamarkuptext}%
    1.85 +extending targets, adding targets%
    1.86 +\end{isamarkuptext}%
    1.87 +\isamarkuptrue%
    1.88 +%
    1.89 +\isamarkupsubsection{Imperative data structures%
    1.90 +}
    1.91 +\isamarkuptrue%
    1.92 +%
    1.93 +\isadelimtheory
    1.94 +%
    1.95 +\endisadelimtheory
    1.96 +%
    1.97 +\isatagtheory
    1.98 +\isacommand{end}\isamarkupfalse%
    1.99 +%
   1.100 +\endisatagtheory
   1.101 +{\isafoldtheory}%
   1.102 +%
   1.103 +\isadelimtheory
   1.104 +%
   1.105 +\endisadelimtheory
   1.106 +\isanewline
   1.107 +\end{isabellebody}%
   1.108 +%%% Local Variables:
   1.109 +%%% mode: latex
   1.110 +%%% TeX-master: "root"
   1.111 +%%% End: