doc-src/Codegen/Thy/document/Evaluation.tex

   be trusted, including code generator configurations by the user.
 
   Evaluation is carried out in a target language \emph{Eval} which
   inherits from \emph{SML} but for convenience uses parts of the
   Isabelle runtime environment.  The soundness of computation carried
-  out there crucially on the correctness of the code generator; this
-  is one of the reasons why you should not use adaptation (see
-  \secref{sec:adaptation}) frivolously.%
+  out there depends crucially on the correctness of the code
+  generator; this is one of the reasons why you should not use
+  adaptation (see \secref{sec:adaptation}) frivolously.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Aspects of evaluation%
 }

 \isamarkupsubsection{Intimate connection between logic and system runtime%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Static embedding of generated code into system runtime -- the code antiquotation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME
-
-  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 \isa{SML}.  To facilitate interfacing of
-  generated code with system code, the code generator provides a
-  \isa{code} antiquotation:%
+The toolbox of static evaluation conversions forms a reasonable base
+  to interweave generated code and system tools.  However in some
+  situations more direct interaction is desirable.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Static embedding of generated code into system runtime -- the \isa{code} antiquotation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \isa{code} antiquotation allows to include constants from
+  generated code directly into ML system code, as in the following toy
+  example:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimquote
 %

 \isadelimquotett
 %
 \endisadelimquotett
 %
 \begin{isamarkuptext}%
-\noindent \isa{code} takes as argument the name of a constant;  after the
-  whole \isa{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
-  \isa{datatypes}.
-
-  For a less simplistic example, theory \isa{Ferrack} is
-  a good reference.%
+\noindent \isa{code} takes as argument the name of a constant;
+  after the whole ML 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 \isa{datatypes}.  Note that it is not
+  possible to refer to constants which carry adaptations by means of
+  \isa{code}; here you have to refer to the adapted code directly.
+
+  For a less simplistic example, theory \isa{Approximation} in
+  the \isa{Decision{\isacharunderscore}Procs} session is a good reference.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsubsection{Static embedding of generated code into system runtime -- \isa{code{\isacharunderscore}reflect}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}}%
+The \isa{code} antiquoation is lightweight, but the generated code
+  is only accessible while the ML section is processed.  Sometimes this
+  is not appropriate, especially if the generated code contains datatype
+  declarations which are shared with other parts of the system.  In these
+  cases, \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} can be used:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}reflect}\isamarkupfalse%
+\ Sum{\isacharunderscore}Type\isanewline
+\ \ \isakeyword{datatypes}\ sum\ {\isacharequal}\ Inl\ {\isacharbar}\ Inr\isanewline
+\ \ \isakeyword{functions}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projl{\isachardoublequoteclose}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projr{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} takes a structure name and
+  references to datatypes and functions; for these code is compiled
+  into the named ML structure and the \emph{Eval} target is modified
+  in a way that future code generation will reference these
+  precompiled versions of the given datatypes and functions.  This
+  also allows to refer to the referenced datatypes and functions from
+  arbitrary ML code as well.
+
+  A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} can be found in the
+  \hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsubsection{Separate compilation -- \isa{code{\isacharunderscore}reflect}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+For technical reasons it is sometimes necessary to separate
+  generation and compilation of code which is supposed to be used in
+  the system runtime.  For this \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} with an
+  optional \isa{file} argument can be used:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}reflect}\isamarkupfalse%
+\ Rat\isanewline
+\ \ \isakeyword{datatypes}\ rat\ {\isacharequal}\ Frct\isanewline
+\ \ \isakeyword{functions}\ Fract\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}plus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}minus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}times\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}divide\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}rat{\isachardot}ML{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This just generates the references code to the specified
+  file which can be included into the system runtime later on.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimtheory
 %