doc-src/IsarAdvanced/Codegen/Thy/Further.thy

 theory Further
 imports Setup
 begin
 
-section {* Further topics *}
+section {* Further topics \label{sec:further} *}
 
-subsection {* Serializer options *}
+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