--- a/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Mon Mar 02 16:58:39 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-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
- contains 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 name space.
-
- 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 %quote 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 *}
-
-text {*
- Code generation may also be used to \emph{evaluate} expressions
- (using @{text SML} as target language of course).
- For instance, the @{command value} allows to reduce an expression to a
- normal form with respect to the underlying code equations:
-*}
-
-value %quote "42 / (12 :: rat)"
-
-text {*
- \noindent will display @{term "7 / (2 :: rat)"}.
-
- The @{method eval} method tries to reduce a goal by code generation to @{term True}
- and solves it in that case, but fails otherwise:
-*}
-
-lemma %quote "42 / (12 :: rat) = 7 / 2"
- by %quote eval
-
-text {*
- \noindent The soundness of the @{method eval} method depends crucially
- on the correctness of the code generator; this is one of the reasons
- why you should not use adaption (see \secref{sec:adaption}) frivolously.
-*}
-
-subsection {* Code antiquotation *}
-
-text {*
- In scenarios involving techniques like reflection it is quite common
- that code generated from a theory forms the basis for implementing
- a proof procedure in @{text SML}. To facilitate interfacing of generated code
- with system code, the code generator provides a @{text code} antiquotation:
-*}
-
-datatype %quote form = T | F | And form form | Or form form
-
-ML %quote {*
- fun eval_form @{code T} = true
- | eval_form @{code F} = false
- | eval_form (@{code And} (p, q)) =
- eval_form p andalso eval_form q
- | eval_form (@{code Or} (p, q)) =
- eval_form p orelse eval_form q;
-*}
-
-text {*
- \noindent @{text code} takes as argument the name of a constant; after the
- whole @{text SML} is read, the necessary code is generated transparently
- and the corresponding constant names are inserted. This technique also
- allows to use pattern matching on constructors stemming from compiled
- @{text datatypes}.
-
- For a less simplistic example, theory @{theory Ferrack} is
- a good reference.
-*}
-
-subsection {* Imperative data structures *}
-
-text {*
- If you consider imperative data structures as inevitable for a specific
- application, you should consider
- \emph{Imperative Functional Programming with Isabelle/HOL}
- (\cite{bulwahn-et-al:2008:imperative});
- the framework described there is available in theory @{theory Imperative_HOL}.
-*}
-
-end