--- a/doc-src/Codegen/Thy/Evaluation.thy Tue Sep 21 10:02:50 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy Tue Sep 21 14:36:13 2010 +0200
@@ -4,78 +4,202 @@
section {* Evaluation *}
-text {* Introduction *}
+text {*
+ 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 @{term "t"} using a program to a
+ term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}. This
+ application of code generation in the following is referred to as
+ \emph{evaluation}.
+*}
subsection {* Evaluation techniques *}
-text {* simplifier *}
+text {*
+ 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.
-text {* nbe *}
+ \item[Efficiency.] The more machine-near the technique, the
+ faster it is.
-text {* eval target: SML standalone vs. Isabelle/SML, example, soundness *}
+ \item[Trustability.] Techniques which a huge (and also probably
+ more configurable infrastructure) are more fragile and less
+ trustable.
+
+ \end{description}
+*}
-subsection {* Dynamic evaluation *}
-
-text {* value (three variants) *}
+subsubsection {* The simplifier (@{text simp}) *}
-text {* methods (three variants) *}
-
-text {* corresponding ML interfaces *}
+text {*
+ 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.
+*}
-subsection {* Static evaluation *}
+subsubsection {* Normalization by evaluation (@{text nbe}) *}
-text {* code_simp, nbe (tbd), Eval (tbd, in simple fashion) *}
-
-text {* hand-written: code antiquotation *}
+text {*
+ 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.
+*}
-subsection {* Hybrid techniques *}
+subsubsection {* Evaluation in ML (@{text code}) *}
+
+text {*
+ 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.
-text {* code reflect runtime *}
-
-text {* code reflect external *}
+ 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.
+*}
-text {* FIXME here the old sections follow *}
-
-subsection {* Evaluation oracle *}
+subsection {* Aspects of evaluation *}
text {*
- Code generation may also be used to \emph{evaluate} expressions
- (using @{text SML} as target language of course).
- For instance, the @{command_def value} reduces an expression to a
- normal form with respect to the underlying code equations:
+ 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
+ @{command_def value} command which allows ad-hoc evaluation of
+ terms:
*}
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:
+ \noindent By default @{command 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.
*}
-lemma %quote "42 / (12 :: rat) = 7 / 2"
- by %quote eval
+value %quote [nbe] "42 / (12 :: rat)"
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 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 @{term "t"} first
+ by plain evaluation and certifies the result @{term "t'"} by
+ checking the equation @{term "t \<equiv> t'"} 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 @{term t} terminates with a result @{term
+ "t'"}.
+
+ \item Evaluation of @{term 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 @{term
+ "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
+ Exceptions of the third kind are propagted to the user.
+
+ By default return values of plain evaluation are optional, yielding
+ @{text "SOME t'"} in the first case, @{text "NONE"} and in the
+ second propagating the exception in the third case. A strict
+ variant of plain evaluation either yields @{text "t'"} or propagates
+ any exception, a liberal variant caputures any exception in a result
+ of type @{text "Exn.result"}.
+
+ For property conversion (which coincides with conversion except for
+ evaluation in ML), methods are provided which solve a given goal by
+ evaluation.
*}
-subsubsection {* Code antiquotation *}
+subsection {* Schematic overview *}
+
+(*FIXME rotatebox?*)
text {*
+ \begin{tabular}{ll||c|c|c}
+ & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
+ dynamic & interactive evaluation
+ & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
+ \tabularnewline
+ & plain evaluation & & & @{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline
+ & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
+ & property conversion & & & @{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline
+ & conversion & @{ML "Code_Simp.dynamic_eval_conv"} & @{ML "Nbe.dynamic_eval_conv"}
+ & @{ML "Code_Evaluation.dynamic_eval_conv"} \tabularnewline \hline \hline
+ static & plain evaluation & & & @{ML "Code_Evaluation.static_value"} \tabularnewline \hline
+ & property conversion & &
+ & @{ML "Code_Runtime.static_holds_conv"} \tabularnewline \hline
+ & conversion & @{ML "Code_Simp.static_eval_conv"}
+ & @{ML "Nbe.static_eval_conv"}
+ & @{ML "Code_Evaluation.static_eval_conv"}
+ \end{tabular}
+*}
+
+
+subsection {* Intimate connection between logic and system runtime *}
+
+text {* FIXME *}
+
+
+subsubsection {* Static embedding of generated code into system runtime -- the code antiquotation *}
+
+text {*
+ 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 @{text SML}. To facilitate interfacing of generated code
- with system code, the code generator provides a @{text code} antiquotation:
+ 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 (*<*)
@@ -101,4 +225,12 @@
*}
+subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
+
+text {* FIXME @{command_def code_reflect} *}
+
+subsubsection {* Separate compilation -- @{text code_reflect} *}
+
+text {* FIXME *}
+
end
--- a/doc-src/Codegen/Thy/Refinement.thy Tue Sep 21 10:02:50 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Tue Sep 21 14:36:13 2010 +0200
@@ -167,7 +167,7 @@
*}
-subsection {* Datatype refinement involving invariants *}
+subsection {* Datatype refinement involving invariants \label{sec:invariant} *}
text {*
Datatype representation involving invariants require a dedicated
--- 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
--- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Sep 21 10:02:50 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Sep 21 14:36:13 2010 +0200
@@ -405,7 +405,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Datatype refinement involving invariants%
+\isamarkupsubsection{Datatype refinement involving invariants \label{sec:invariant}%
}
\isamarkuptrue%
%