theory Further
imports Setup
begin
section {* Further topics \label{sec:further} *}
subsection {* Further reading *}
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.
*}
subsection {* Modules *}
text {*
When invoking the @{command export_code} command it is possible to leave
out the @{keyword "module_name"} part; then code is distributed over
different modules, where the module name space roughly is induced
by the @{text Isabelle} theory namespace.
Then sometimes the awkward situation occurs that dependencies between
definitions introduce cyclic dependencies between modules, which in the
@{text Haskell} world leaves you to the mercy of the @{text Haskell} implementation
you are using, while for @{text SML}/@{text 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
*}
code_modulename SML
A ABC
B ABC
C ABC
text {*
we explicitly map all those modules on \emph{ABC},
resulting in an ad-hoc merge of this three modules
at serialisation time.
*}
subsection {* Evaluation oracle *}
subsection {* Code antiquotation *}
subsection {* Creating new targets *}
text {* extending targets, adding targets *}
subsection {* Imperative data structures *}
end