src/Doc/Codegen/Evaluation.thy
author wenzelm
Tue Aug 28 18:57:32 2012 +0200 (2012-08-28)
changeset 48985 5386df44a037
parent 48951 doc-src/Codegen/Evaluation.thy@b9238cbcdd41
child 51713 4fd969609b4d
permissions -rw-r--r--
renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;
     1 theory Evaluation
     2 imports Setup
     3 begin
     4 
     5 section {* Evaluation \label{sec:evaluation} *}
     6 
     7 text {*
     8   Recalling \secref{sec:principle}, code generation turns a system of
     9   equations into a program with the \emph{same} equational semantics.
    10   As a consequence, this program can be used as a \emph{rewrite
    11   engine} for terms: rewriting a term @{term "t"} using a program to a
    12   term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}.  This
    13   application of code generation in the following is referred to as
    14   \emph{evaluation}.
    15 *}
    16 
    17 
    18 subsection {* Evaluation techniques *}
    19 
    20 text {*
    21   The existing infrastructure provides a rich palette of evaluation
    22   techniques, each comprising different aspects:
    23 
    24   \begin{description}
    25 
    26     \item[Expressiveness.]  Depending on how good symbolic computation
    27       is supported, the class of terms which can be evaluated may be
    28       bigger or smaller.
    29 
    30     \item[Efficiency.]  The more machine-near the technique, the
    31       faster it is.
    32 
    33     \item[Trustability.]  Techniques which a huge (and also probably
    34       more configurable infrastructure) are more fragile and less
    35       trustable.
    36 
    37   \end{description}
    38 *}
    39 
    40 
    41 subsubsection {* The simplifier (@{text simp}) *}
    42 
    43 text {*
    44   The simplest way for evaluation is just using the simplifier with
    45   the original code equations of the underlying program.  This gives
    46   fully symbolic evaluation and highest trustablity, with the usual
    47   performance of the simplifier.  Note that for operations on abstract
    48   datatypes (cf.~\secref{sec:invariant}), the original theorems as
    49   given by the users are used, not the modified ones.
    50 *}
    51 
    52 
    53 subsubsection {* Normalization by evaluation (@{text nbe}) *}
    54 
    55 text {*
    56   Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
    57   provides a comparably fast partially symbolic evaluation which
    58   permits also normalization of functions and uninterpreted symbols;
    59   the stack of code to be trusted is considerable.
    60 *}
    61 
    62 
    63 subsubsection {* Evaluation in ML (@{text code}) *}
    64 
    65 text {*
    66   Highest performance can be achieved by evaluation in ML, at the cost
    67   of being restricted to ground results and a layered stack of code to
    68   be trusted, including code generator configurations by the user.
    69 
    70   Evaluation is carried out in a target language \emph{Eval} which
    71   inherits from \emph{SML} but for convenience uses parts of the
    72   Isabelle runtime environment.  The soundness of computation carried
    73   out there depends crucially on the correctness of the code
    74   generator setup; this is one of the reasons why you should not use
    75   adaptation (see \secref{sec:adaptation}) frivolously.
    76 *}
    77 
    78 
    79 subsection {* Aspects of evaluation *}
    80 
    81 text {*
    82   Each of the techniques can be combined with different aspects.  The
    83   most important distinction is between dynamic and static evaluation.
    84   Dynamic evaluation takes the code generator configuration \qt{as it
    85   is} at the point where evaluation is issued.  Best example is the
    86   @{command_def value} command which allows ad-hoc evaluation of
    87   terms:
    88 *}
    89 
    90 value %quote "42 / (12 :: rat)"
    91 
    92 text {*
    93   \noindent By default @{command value} tries all available evaluation
    94   techniques and prints the result of the first succeeding one.  A particular
    95   technique may be specified in square brackets, e.g.
    96 *}
    97 
    98 value %quote [nbe] "42 / (12 :: rat)"
    99 
   100 text {*
   101   To employ dynamic evaluation in the document generation, there is also
   102   a @{text value} antiquotation. By default, it also tries all available evaluation
   103   techniques and prints the result of the first succeeding one, unless a particular
   104   technique is specified in square brackets.
   105 
   106   Static evaluation freezes the code generator configuration at a
   107   certain point and uses this context whenever evaluation is issued
   108   later on.  This is particularly appropriate for proof procedures
   109   which use evaluation, since then the behaviour of evaluation is not
   110   changed or even compromised later on by actions of the user.
   111 
   112   As a technical complication, terms after evaluation in ML must be
   113   turned into Isabelle's internal term representation again.  Since
   114   this is also configurable, it is never fully trusted.  For this
   115   reason, evaluation in ML comes with further aspects:
   116 
   117   \begin{description}
   118 
   119     \item[Plain evaluation.]  A term is normalized using the provided
   120       term reconstruction from ML to Isabelle; for applications which
   121       do not need to be fully trusted.
   122 
   123     \item[Property conversion.]  Evaluates propositions; since these
   124       are monomorphic, the term reconstruction is fixed once and for all
   125       and therefore trustable.
   126 
   127     \item[Conversion.]  Evaluates an arbitrary term @{term "t"} first
   128       by plain evaluation and certifies the result @{term "t'"} by
   129       checking the equation @{term "t \<equiv> t'"} using property
   130       conversion.
   131 
   132   \end{description}
   133 
   134   \noindent The picture is further complicated by the roles of
   135   exceptions.  Here three cases have to be distinguished:
   136 
   137   \begin{itemize}
   138 
   139     \item Evaluation of @{term t} terminates with a result @{term
   140       "t'"}.
   141 
   142     \item Evaluation of @{term t} terminates which en exception
   143       indicating a pattern match failure or a non-implemented
   144       function.  As sketched in \secref{sec:partiality}, this can be
   145       interpreted as partiality.
   146      
   147     \item Evaluation raises any other kind of exception.
   148      
   149   \end{itemize}
   150 
   151   \noindent For conversions, the first case yields the equation @{term
   152   "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
   153   Exceptions of the third kind are propagated to the user.
   154 
   155   By default return values of plain evaluation are optional, yielding
   156   @{text "SOME t'"} in the first case, @{text "NONE"} in the
   157   second, and propagating the exception in the third case.  A strict
   158   variant of plain evaluation either yields @{text "t'"} or propagates
   159   any exception, a liberal variant caputures any exception in a result
   160   of type @{text "Exn.result"}.
   161   
   162   For property conversion (which coincides with conversion except for
   163   evaluation in ML), methods are provided which solve a given goal by
   164   evaluation.
   165 *}
   166 
   167 
   168 subsection {* Schematic overview *}
   169 
   170 text {*
   171   \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
   172   \fontsize{9pt}{12pt}\selectfont
   173   \begin{tabular}{ll||c|c|c}
   174     & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
   175     \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
   176       & interactive evaluation 
   177       & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
   178       \tabularnewline
   179     & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
   180     & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
   181     & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
   182     & conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
   183       & \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline
   184     \multirow{3}{1ex}{\rotatebox{90}{static}}
   185     & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
   186     & property conversion & &
   187       & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
   188     & conversion & \ttsize@{ML "Code_Simp.static_conv"}
   189       & \ttsize@{ML "Nbe.static_conv"}
   190       & \ttsize@{ML "Code_Evaluation.static_conv"}
   191   \end{tabular}
   192 *}
   193 
   194 
   195 subsection {* Intimate connection between logic and system runtime *}
   196 
   197 text {*
   198   The toolbox of static evaluation conversions forms a reasonable base
   199   to interweave generated code and system tools.  However in some
   200   situations more direct interaction is desirable.
   201 *}
   202 
   203 
   204 subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation *}
   205 
   206 text {*
   207   The @{text code} antiquotation allows to include constants from
   208   generated code directly into ML system code, as in the following toy
   209   example:
   210 *}
   211 
   212 datatype %quote form = T | F | And form form | Or form form (*<*)
   213 
   214 (*>*) ML %quotett {*
   215   fun eval_form @{code T} = true
   216     | eval_form @{code F} = false
   217     | eval_form (@{code And} (p, q)) =
   218         eval_form p andalso eval_form q
   219     | eval_form (@{code Or} (p, q)) =
   220         eval_form p orelse eval_form q;
   221 *}
   222 
   223 text {*
   224   \noindent @{text code} takes as argument the name of a constant;
   225   after the whole ML is read, the necessary code is generated
   226   transparently and the corresponding constant names are inserted.
   227   This technique also allows to use pattern matching on constructors
   228   stemming from compiled datatypes.  Note that the @{text code}
   229   antiquotation may not refer to constants which carry adaptations;
   230   here you have to refer to the corresponding adapted code directly.
   231 
   232   For a less simplistic example, theory @{text Approximation} in
   233   the @{text Decision_Procs} session is a good reference.
   234 *}
   235 
   236 
   237 subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
   238 
   239 text {*
   240   The @{text code} antiquoation is lightweight, but the generated code
   241   is only accessible while the ML section is processed.  Sometimes this
   242   is not appropriate, especially if the generated code contains datatype
   243   declarations which are shared with other parts of the system.  In these
   244   cases, @{command_def code_reflect} can be used:
   245 *}
   246 
   247 code_reflect %quote Sum_Type
   248   datatypes sum = Inl | Inr
   249   functions "Sum_Type.Projl" "Sum_Type.Projr"
   250 
   251 text {*
   252   \noindent @{command_def code_reflect} takes a structure name and
   253   references to datatypes and functions; for these code is compiled
   254   into the named ML structure and the \emph{Eval} target is modified
   255   in a way that future code generation will reference these
   256   precompiled versions of the given datatypes and functions.  This
   257   also allows to refer to the referenced datatypes and functions from
   258   arbitrary ML code as well.
   259 
   260   A typical example for @{command code_reflect} can be found in the
   261   @{theory Predicate} theory.
   262 *}
   263 
   264 
   265 subsubsection {* Separate compilation -- @{text code_reflect} *}
   266 
   267 text {*
   268   For technical reasons it is sometimes necessary to separate
   269   generation and compilation of code which is supposed to be used in
   270   the system runtime.  For this @{command code_reflect} with an
   271   optional @{text "file"} argument can be used:
   272 *}
   273 
   274 code_reflect %quote Rat
   275   datatypes rat = Frct
   276   functions Fract
   277     "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   278     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   279   file "examples/rat.ML"
   280 
   281 text {*
   282   \noindent This merely generates the referenced code to the given
   283   file which can be included into the system runtime later on.
   284 *}
   285 
   286 end
   287