author | haftmann |
Wed, 01 Oct 2008 13:33:54 +0200 | |
changeset 28447 | df77ed974a78 |
parent 28419 | f65e8b318581 |
child 28593 | f087237af65d |
permissions | -rw-r--r-- |
haftmann@28213 | 1 |
theory Further |
haftmann@28213 | 2 |
imports Setup |
haftmann@28213 | 3 |
begin |
haftmann@28213 | 4 |
|
haftmann@28447 | 5 |
section {* Further issues \label{sec:further} *} |
haftmann@28213 | 6 |
|
haftmann@28419 | 7 |
subsection {* Further reading *} |
haftmann@28419 | 8 |
|
haftmann@28419 | 9 |
text {* |
haftmann@28419 | 10 |
Do dive deeper into the issue of code generation, you should visit |
haftmann@28419 | 11 |
the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which |
haftmann@28419 | 12 |
constains exhaustive syntax diagrams. |
haftmann@28419 | 13 |
*} |
haftmann@28419 | 14 |
|
haftmann@28419 | 15 |
subsection {* Modules *} |
haftmann@28419 | 16 |
|
haftmann@28419 | 17 |
text {* |
haftmann@28419 | 18 |
When invoking the @{command export_code} command it is possible to leave |
haftmann@28419 | 19 |
out the @{keyword "module_name"} part; then code is distributed over |
haftmann@28419 | 20 |
different modules, where the module name space roughly is induced |
haftmann@28419 | 21 |
by the @{text Isabelle} theory namespace. |
haftmann@28419 | 22 |
|
haftmann@28419 | 23 |
Then sometimes the awkward situation occurs that dependencies between |
haftmann@28419 | 24 |
definitions introduce cyclic dependencies between modules, which in the |
haftmann@28419 | 25 |
@{text Haskell} world leaves you to the mercy of the @{text Haskell} implementation |
haftmann@28419 | 26 |
you are using, while for @{text SML}/@{text OCaml} code generation is not possible. |
haftmann@28419 | 27 |
|
haftmann@28419 | 28 |
A solution is to declare module names explicitly. |
haftmann@28419 | 29 |
Let use assume the three cyclically dependent |
haftmann@28419 | 30 |
modules are named \emph{A}, \emph{B} and \emph{C}. |
haftmann@28419 | 31 |
Then, by stating |
haftmann@28419 | 32 |
*} |
haftmann@28419 | 33 |
|
haftmann@28419 | 34 |
code_modulename SML |
haftmann@28419 | 35 |
A ABC |
haftmann@28419 | 36 |
B ABC |
haftmann@28419 | 37 |
C ABC |
haftmann@28419 | 38 |
|
haftmann@28419 | 39 |
text {* |
haftmann@28419 | 40 |
we explicitly map all those modules on \emph{ABC}, |
haftmann@28419 | 41 |
resulting in an ad-hoc merge of this three modules |
haftmann@28419 | 42 |
at serialisation time. |
haftmann@28419 | 43 |
*} |
haftmann@28213 | 44 |
|
haftmann@28213 | 45 |
subsection {* Evaluation oracle *} |
haftmann@28213 | 46 |
|
haftmann@28213 | 47 |
subsection {* Code antiquotation *} |
haftmann@28213 | 48 |
|
haftmann@28213 | 49 |
subsection {* Creating new targets *} |
haftmann@28213 | 50 |
|
haftmann@28213 | 51 |
text {* extending targets, adding targets *} |
haftmann@28213 | 52 |
|
haftmann@28419 | 53 |
subsection {* Imperative data structures *} |
haftmann@28419 | 54 |
|
haftmann@28213 | 55 |
end |