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

tuned

theory Further
imports Setup
begin

section {* Further issues \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