diff -r 57413334669d -r d9c247f7afa3 doc-src/Codegen/Thy/Evaluation.thy --- 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 \ 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 \ 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