diff -r 57413334669d -r d9c247f7afa3 doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Tue Sep 21 10:02:50 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Tue Sep 21 14:36:13 2010 +0200
@@ -23,7 +23,13 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Introduction%
+Recalling \secref{sec:principle}, code generation turns a system of
+  equations into a program with the \emph{same} equational semantics.
+  As a consequence, this program can be used as a \emph{rewrite
+  engine} for terms: rewriting a term \isa{t} using a program to a
+  term \isa{t{\isacharprime}} yields the theorems \isa{t\ {\isasymequiv}\ t{\isacharprime}}.  This
+  application of code generation in the following is referred to as
+  \emph{evaluation}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -32,81 +38,81 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-simplifier%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-nbe%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-eval target: SML standalone vs. Isabelle/SML, example, soundness%
+The existing infrastructure provides a rich palett of evaluation
+  techniques, each comprising different aspects:
+
+  \begin{description}
+
+    \item[Expressiveness.]  Depending on how good symbolic computation
+      is supported, the class of terms which can be evaluated may be
+      bigger or smaller.
+
+    \item[Efficiency.]  The more machine-near the technique, the
+      faster it is.
+
+    \item[Trustability.]  Techniques which a huge (and also probably
+      more configurable infrastructure) are more fragile and less
+      trustable.
+
+  \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Dynamic evaluation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-value (three variants)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-methods (three variants)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-corresponding ML interfaces%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Static evaluation%
+\isamarkupsubsubsection{The simplifier (\isa{simp})%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-code_simp, nbe (tbd), Eval (tbd, in simple fashion)%
+The simplest way for evaluation is just using the simplifier with
+  the original code equations of the underlying program.  This gives
+  fully symbolic evaluation and highest trustablity, with the usual
+  performance of the simplifier.  Note that for operations on abstract
+  datatypes (cf.~\secref{sec:invariant}), the original theorems as
+  given by the users are used, not the modified ones.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\begin{isamarkuptext}%
-hand-written: code antiquotation%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Hybrid techniques%
+\isamarkupsubsubsection{Normalization by evaluation (\isa{nbe})%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-code reflect runtime%
+Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
+  provides a comparably fast partially symbolic evaluation which
+  permits also normalization of functions and uninterpreted symbols;
+  the stack of code to be trusted is considerable.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\begin{isamarkuptext}%
-code reflect external%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME here the old sections follow%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Evaluation oracle%
+\isamarkupsubsubsection{Evaluation in ML (\isa{code})%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Code generation may also be used to \emph{evaluate} expressions
-  (using \isa{SML} as target language of course).
-  For instance, the \indexdef{}{command}{value}\hypertarget{command.value}{\hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}}} reduces an expression to a
-  normal form with respect to the underlying code equations:%
+Highest performance can be achieved by evaluation in ML, at the cost
+  of being restricted to ground results and a layered stack of code to
+  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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Aspects of evaluation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Each of the techniques can be combined with different aspects.  The
+  most important distinction is between dynamic and static evaluation.
+  Dynamic evaluation takes the code generator configuration \qt{as it
+  is} at the point where evaluation is issued.  Best example is the
+  \indexdef{}{command}{value}\hypertarget{command.value}{\hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}}} command which allows ad-hoc evaluation of
+  terms:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -125,10 +131,9 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent will display \isa{{\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}}.
-
-  The \hyperlink{method.eval}{\mbox{\isa{eval}}} method tries to reduce a goal by code generation to \isa{True}
-  and solves it in that case, but fails otherwise:%
+\noindent By default \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} tries all available evaluation
+  techniques and prints the result of the first succeeding one.  A particular
+  technique may be specified in square brackets, e.g.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -137,10 +142,8 @@
 \endisadelimquote
 %
 \isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}\ {\isacharequal}\ {\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ eval%
+\isacommand{value}\isamarkupfalse%
+\ {\isacharbrackleft}nbe{\isacharbrackright}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -149,21 +152,112 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent The soundness of the \hyperlink{method.eval}{\mbox{\isa{eval}}} method 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.%
+Static evaluation freezes the code generator configuration at a
+  certain point and uses this context whenever evaluation is issued
+  later on.  This is particularly appropriate for proof procedures
+  which use evaluation, since then the behaviour of evaluation is not
+  changed or even compromised later on by actions of the user.
+
+  As a technical complication, terms after evaluation in ML must be
+  turned into Isabelle's internal term representation again.  Since
+  this is also configurable, it is never fully trusted.  For this
+  reason, evaluation in ML comes with further aspects:
+
+  \begin{description}
+
+    \item[Plain evaluation.]  A term is normalized using the provided
+      term reconstruction from ML to Isabelle; for applications which
+      do not need to be fully trusted.
+
+    \item[Property conversion.]  Evaluates propositions; since these
+      are monomorphic, the term reconstruction is fixed once and for all
+      and therefore trustable.
+
+    \item[Conversion.]  Evaluates an arbitrary term \isa{t} first
+      by plain evaluation and certifies the result \isa{t{\isacharprime}} by
+      checking the equation \isa{t\ {\isasymequiv}\ t{\isacharprime}} using property
+      conversion.
+
+  \end{description}
+
+  \noindent The picture is further complicated by the roles of
+  exceptions.  Here three cases have to be distinguished:
+
+  \begin{itemize}
+
+    \item Evaluation of \isa{t} terminates with a result \isa{t{\isacharprime}}.
+
+    \item Evaluation of \isa{t} terminates which en exception
+      indicating a pattern match failure or a not-implemented
+      function.  As sketched in \secref{sec:partiality}, this can be
+      interpreted as partiality.
+     
+    \item Evaluation raise any other kind of exception.
+     
+  \end{itemize}
+
+  \noindent For conversions, the first case yields the equation \isa{t\ {\isacharequal}\ t{\isacharprime}}, the second defaults to reflexivity \isa{t\ {\isacharequal}\ t}.
+  Exceptions of the third kind are propagted to the user.
+
+  By default return values of plain evaluation are optional, yielding
+  \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} and in the
+  second propagating the exception in the third case.  A strict
+  variant of plain evaluation either yields \isa{t{\isacharprime}} or propagates
+  any exception, a liberal variant caputures any exception in a result
+  of type \isa{Exn{\isachardot}result}.
+  
+  For property conversion (which coincides with conversion except for
+  evaluation in ML), methods are provided which solve a given goal by
+  evaluation.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Code antiquotation%
+\isamarkupsubsection{Schematic overview%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-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:%
+\begin{tabular}{ll||c|c|c}
+    & & \isa{simp} & \isa{nbe} & \isa{code} \tabularnewline \hline \hline
+    dynamic & interactive evaluation 
+      & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}simp{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}nbe{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}code{\isacharbrackright}}
+      \tabularnewline
+    & plain evaluation & & & \verb|Code_Evaluation.dynamic_value| \tabularnewline \hline
+    & evaluation method & \hyperlink{method.code-simp}{\mbox{\isa{code{\isacharunderscore}simp}}} & \hyperlink{method.normalization}{\mbox{\isa{normalization}}} & \hyperlink{method.eval}{\mbox{\isa{eval}}} \tabularnewline
+    & property conversion & & & \verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \hline
+    & conversion & \verb|Code_Simp.dynamic_eval_conv| & \verb|Nbe.dynamic_eval_conv|
+      & \verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline
+    static & plain evaluation & & & \verb|Code_Evaluation.static_value| \tabularnewline \hline
+    & property conversion & &
+      & \verb|Code_Runtime.static_holds_conv| \tabularnewline \hline
+    & conversion & \verb|Code_Simp.static_eval_conv|
+      & \verb|Nbe.static_eval_conv|
+      & \verb|Code_Evaluation.static_eval_conv|
+  \end{tabular}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\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:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -230,6 +324,24 @@
 \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}}}}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Separate compilation -- \isa{code{\isacharunderscore}reflect}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimtheory
 %
 \endisadelimtheory