src/Doc/Codegen/Evaluation.thy
author blanchet
Wed Feb 12 08:37:28 2014 +0100 (2014-02-12)
changeset 55418 9f25e0cca254
parent 52287 7e54c4d964e7
child 56927 4044a7d1720f
permissions -rw-r--r--
adapted to renaming of 'Projl' and 'Projr'
     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 captures 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 {* Preprocessing HOL terms into evaluable shape *}
   196 
   197 text {*
   198   When integration decision procedures developed inside HOL into HOL itself,
   199   it is necessary to somehow get from the Isabelle/ML representation to
   200   the representation used by the decision procedure itself (``reification'').
   201   One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
   202   Another option is to use pre-existing infrastructure in HOL:
   203   @{ML "Reification.conv"} and @{ML "Reification.tac"}
   204 
   205   An simplistic example:
   206 *}
   207 
   208 datatype %quote form_ord = T | F | Less nat nat
   209   | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
   210 
   211 primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
   212 where
   213   "interp T vs \<longleftrightarrow> True"
   214 | "interp F vs \<longleftrightarrow> False"
   215 | "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
   216 | "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
   217 | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
   218 | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
   219 
   220 text {*
   221   The datatype @{type form_ord} represents formulae whose semantics is given by
   222   @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   223   whose concrete values are given in list @{term vs}.
   224 *}
   225 
   226 ML (*<*) {* *}
   227 schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
   228 ML_prf 
   229 (*>*) {* val thm =
   230   Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"} *} (*<*)
   231 by (tactic {* ALLGOALS (rtac thm) *})
   232 (*>*) 
   233 
   234 text {*
   235   By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   236   which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   237   to @{const interp} does not contain any free variables and can this be evaluated
   238   using evaluation.
   239 
   240   A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   241   theory @{text Regexp_Method}.
   242 *}
   243 
   244 
   245 subsection {* Intimate connection between logic and system runtime *}
   246 
   247 text {*
   248   The toolbox of static evaluation conversions forms a reasonable base
   249   to interweave generated code and system tools.  However in some
   250   situations more direct interaction is desirable.
   251 *}
   252 
   253 
   254 subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq} *}
   255 
   256 text {*
   257   The @{text code} antiquotation allows to include constants from
   258   generated code directly into ML system code, as in the following toy
   259   example:
   260 *}
   261 
   262 datatype %quote form = T | F | And form form | Or form form (*<*)
   263 
   264 (*>*) ML %quotett {*
   265   fun eval_form @{code T} = true
   266     | eval_form @{code F} = false
   267     | eval_form (@{code And} (p, q)) =
   268         eval_form p andalso eval_form q
   269     | eval_form (@{code Or} (p, q)) =
   270         eval_form p orelse eval_form q;
   271 *}
   272 
   273 text {*
   274   \noindent @{text code} takes as argument the name of a constant;
   275   after the whole ML is read, the necessary code is generated
   276   transparently and the corresponding constant names are inserted.
   277   This technique also allows to use pattern matching on constructors
   278   stemming from compiled datatypes.  Note that the @{text code}
   279   antiquotation may not refer to constants which carry adaptations;
   280   here you have to refer to the corresponding adapted code directly.
   281 
   282   For a less simplistic example, theory @{text Approximation} in
   283   the @{text Decision_Procs} session is a good reference.
   284 *}
   285 
   286 
   287 subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
   288 
   289 text {*
   290   The @{text code} antiquoation is lightweight, but the generated code
   291   is only accessible while the ML section is processed.  Sometimes this
   292   is not appropriate, especially if the generated code contains datatype
   293   declarations which are shared with other parts of the system.  In these
   294   cases, @{command_def code_reflect} can be used:
   295 *}
   296 
   297 code_reflect %quote Sum_Type
   298   datatypes sum = Inl | Inr
   299   functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
   300 
   301 text {*
   302   \noindent @{command_def code_reflect} takes a structure name and
   303   references to datatypes and functions; for these code is compiled
   304   into the named ML structure and the \emph{Eval} target is modified
   305   in a way that future code generation will reference these
   306   precompiled versions of the given datatypes and functions.  This
   307   also allows to refer to the referenced datatypes and functions from
   308   arbitrary ML code as well.
   309 
   310   A typical example for @{command code_reflect} can be found in the
   311   @{theory Predicate} theory.
   312 *}
   313 
   314 
   315 subsubsection {* Separate compilation -- @{text code_reflect} *}
   316 
   317 text {*
   318   For technical reasons it is sometimes necessary to separate
   319   generation and compilation of code which is supposed to be used in
   320   the system runtime.  For this @{command code_reflect} with an
   321   optional @{text "file"} argument can be used:
   322 *}
   323 
   324 code_reflect %quote Rat
   325   datatypes rat = Frct
   326   functions Fract
   327     "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   328     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   329   file "examples/rat.ML"
   330 
   331 text {*
   332   \noindent This merely generates the referenced code to the given
   333   file which can be included into the system runtime later on.
   334 *}
   335 
   336 end
   337