1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Codegen/Thy/Further.thy	Tue Mar 03 11:00:51 2009 +0100
     1.3 @@ -0,0 +1,113 @@
     1.4 +theory Further
     1.5 +imports Setup
     1.6 +begin
     1.7 +
     1.8 +section {* Further issues \label{sec:further} *}
     1.9 +
    1.10 +subsection {* Further reading *}
    1.11 +
    1.12 +text {*
    1.13 +  Do dive deeper into the issue of code generation, you should visit
    1.14 +  the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
    1.15 +  contains exhaustive syntax diagrams.
    1.16 +*}
    1.17 +
    1.18 +subsection {* Modules *}
    1.19 +
    1.20 +text {*
    1.21 +  When invoking the @{command export_code} command it is possible to leave
    1.22 +  out the @{keyword "module_name"} part;  then code is distributed over
    1.23 +  different modules, where the module name space roughly is induced
    1.24 +  by the @{text Isabelle} theory name space.
    1.25 +
    1.26 +  Then sometimes the awkward situation occurs that dependencies between
    1.27 +  definitions introduce cyclic dependencies between modules, which in the
    1.28 +  @{text Haskell} world leaves you to the mercy of the @{text Haskell} implementation
    1.29 +  you are using,  while for @{text SML}/@{text OCaml} code generation is not possible.
    1.30 +
    1.31 +  A solution is to declare module names explicitly.
    1.32 +  Let use assume the three cyclically dependent
    1.33 +  modules are named \emph{A}, \emph{B} and \emph{C}.
    1.34 +  Then, by stating
    1.35 +*}
    1.36 +
    1.37 +code_modulename %quote SML
    1.38 +  A ABC
    1.39 +  B ABC
    1.40 +  C ABC
    1.41 +
    1.42 +text {*
    1.43 +  we explicitly map all those modules on \emph{ABC},
    1.44 +  resulting in an ad-hoc merge of this three modules
    1.45 +  at serialisation time.
    1.46 +*}
    1.47 +
    1.48 +subsection {* Evaluation oracle *}
    1.49 +
    1.50 +text {*
    1.51 +  Code generation may also be used to \emph{evaluate} expressions
    1.52 +  (using @{text SML} as target language of course).
    1.53 +  For instance, the @{command value} allows to reduce an expression to a
    1.54 +  normal form with respect to the underlying code equations:
    1.55 +*}
    1.56 +
    1.57 +value %quote "42 / (12 :: rat)"
    1.58 +
    1.59 +text {*
    1.60 +  \noindent will display @{term "7 / (2 :: rat)"}.
    1.61 +
    1.62 +  The @{method eval} method tries to reduce a goal by code generation to @{term True}
    1.63 +  and solves it in that case, but fails otherwise:
    1.64 +*}
    1.65 +
    1.66 +lemma %quote "42 / (12 :: rat) = 7 / 2"
    1.67 +  by %quote eval
    1.68 +
    1.69 +text {*
    1.70 +  \noindent The soundness of the @{method eval} method depends crucially 
    1.71 +  on the correctness of the code generator;  this is one of the reasons
    1.72 +  why you should not use adaption (see \secref{sec:adaption}) frivolously.
    1.73 +*}
    1.74 +
    1.75 +subsection {* Code antiquotation *}
    1.76 +
    1.77 +text {*
    1.78 +  In scenarios involving techniques like reflection it is quite common
    1.79 +  that code generated from a theory forms the basis for implementing
    1.80 +  a proof procedure in @{text SML}.  To facilitate interfacing of generated code
    1.81 +  with system code, the code generator provides a @{text code} antiquotation:
    1.82 +*}
    1.83 +
    1.84 +datatype %quote form = T | F | And form form | Or form form
    1.85 +
    1.86 +ML %quote {*
    1.87 +  fun eval_form @{code T} = true
    1.88 +    | eval_form @{code F} = false
    1.89 +    | eval_form (@{code And} (p, q)) =
    1.90 +        eval_form p andalso eval_form q
    1.91 +    | eval_form (@{code Or} (p, q)) =
    1.92 +        eval_form p orelse eval_form q;
    1.93 +*}
    1.94 +
    1.95 +text {*
    1.96 +  \noindent @{text code} takes as argument the name of a constant;  after the
    1.97 +  whole @{text SML} is read, the necessary code is generated transparently
    1.98 +  and the corresponding constant names are inserted.  This technique also
    1.99 +  allows to use pattern matching on constructors stemming from compiled
   1.100 +  @{text datatypes}.
   1.101 +
   1.102 +  For a less simplistic example, theory @{theory Ferrack} is
   1.103 +  a good reference.
   1.104 +*}
   1.105 +
   1.106 +subsection {* Imperative data structures *}
   1.107 +
   1.108 +text {*
   1.109 +  If you consider imperative data structures as inevitable for a specific
   1.110 +  application, you should consider
   1.111 +  \emph{Imperative Functional Programming with Isabelle/HOL}
   1.112 +  (\cite{bulwahn-et-al:2008:imperative});
   1.113 +  the framework described there is available in theory @{theory Imperative_HOL}.
   1.114 +*}
   1.115 +
   1.116 +end