src/Doc/Codegen/Evaluation.thy
author haftmann
Fri May 09 08:13:37 2014 +0200 (2014-05-09)
changeset 56927 4044a7d1720f
parent 55418 9f25e0cca254
child 58100 f54a8a4134d3
permissions -rw-r--r--
hardcoded nbe and sml into value command
     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 @{command value} tries first to evaluate using ML, falling
    94   back to normalization by evaluation if this fails.
    95 
    96   To employ dynamic evaluation in the document generation, there is also
    97   a @{text value} antiquotation with the same evaluation techniques 
    98   as @{command value}.
    99 
   100   Static evaluation freezes the code generator configuration at a
   101   certain point and uses this context whenever evaluation is issued
   102   later on.  This is particularly appropriate for proof procedures
   103   which use evaluation, since then the behaviour of evaluation is not
   104   changed or even compromised later on by actions of the user.
   105 
   106   As a technical complication, terms after evaluation in ML must be
   107   turned into Isabelle's internal term representation again.  Since
   108   this is also configurable, it is never fully trusted.  For this
   109   reason, evaluation in ML comes with further aspects:
   110 
   111   \begin{description}
   112 
   113     \item[Plain evaluation.]  A term is normalized using the provided
   114       term reconstruction from ML to Isabelle; for applications which
   115       do not need to be fully trusted.
   116 
   117     \item[Property conversion.]  Evaluates propositions; since these
   118       are monomorphic, the term reconstruction is fixed once and for all
   119       and therefore trustable.
   120 
   121     \item[Conversion.]  Evaluates an arbitrary term @{term "t"} first
   122       by plain evaluation and certifies the result @{term "t'"} by
   123       checking the equation @{term "t \<equiv> t'"} using property
   124       conversion.
   125 
   126   \end{description}
   127 
   128   \noindent The picture is further complicated by the roles of
   129   exceptions.  Here three cases have to be distinguished:
   130 
   131   \begin{itemize}
   132 
   133     \item Evaluation of @{term t} terminates with a result @{term
   134       "t'"}.
   135 
   136     \item Evaluation of @{term t} terminates which en exception
   137       indicating a pattern match failure or a non-implemented
   138       function.  As sketched in \secref{sec:partiality}, this can be
   139       interpreted as partiality.
   140      
   141     \item Evaluation raises any other kind of exception.
   142      
   143   \end{itemize}
   144 
   145   \noindent For conversions, the first case yields the equation @{term
   146   "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
   147   Exceptions of the third kind are propagated to the user.
   148 
   149   By default return values of plain evaluation are optional, yielding
   150   @{text "SOME t'"} in the first case, @{text "NONE"} in the
   151   second, and propagating the exception in the third case.  A strict
   152   variant of plain evaluation either yields @{text "t'"} or propagates
   153   any exception, a liberal variant captures any exception in a result
   154   of type @{text "Exn.result"}.
   155   
   156   For property conversion (which coincides with conversion except for
   157   evaluation in ML), methods are provided which solve a given goal by
   158   evaluation.
   159 *}
   160 
   161 
   162 subsection {* Schematic overview *}
   163 
   164 text {*
   165   \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
   166   \fontsize{9pt}{12pt}\selectfont
   167   \begin{tabular}{ll||c|c|c}
   168     & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
   169     \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
   170     & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
   171     & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
   172     & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
   173     & conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
   174       & \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline
   175     \multirow{3}{1ex}{\rotatebox{90}{static}}
   176     & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
   177     & property conversion & &
   178       & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
   179     & conversion & \ttsize@{ML "Code_Simp.static_conv"}
   180       & \ttsize@{ML "Nbe.static_conv"}
   181       & \ttsize@{ML "Code_Evaluation.static_conv"}
   182   \end{tabular}
   183 *}
   184 
   185 
   186 subsection {* Preprocessing HOL terms into evaluable shape *}
   187 
   188 text {*
   189   When integration decision procedures developed inside HOL into HOL itself,
   190   it is necessary to somehow get from the Isabelle/ML representation to
   191   the representation used by the decision procedure itself (``reification'').
   192   One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
   193   Another option is to use pre-existing infrastructure in HOL:
   194   @{ML "Reification.conv"} and @{ML "Reification.tac"}
   195 
   196   An simplistic example:
   197 *}
   198 
   199 datatype %quote form_ord = T | F | Less nat nat
   200   | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
   201 
   202 primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
   203 where
   204   "interp T vs \<longleftrightarrow> True"
   205 | "interp F vs \<longleftrightarrow> False"
   206 | "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
   207 | "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
   208 | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
   209 | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
   210 
   211 text {*
   212   The datatype @{type form_ord} represents formulae whose semantics is given by
   213   @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   214   whose concrete values are given in list @{term vs}.
   215 *}
   216 
   217 ML (*<*) {* *}
   218 schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
   219 ML_prf 
   220 (*>*) {* val thm =
   221   Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"} *} (*<*)
   222 by (tactic {* ALLGOALS (rtac thm) *})
   223 (*>*) 
   224 
   225 text {*
   226   By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   227   which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   228   to @{const interp} does not contain any free variables and can this be evaluated
   229   using evaluation.
   230 
   231   A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   232   theory @{text Regexp_Method}.
   233 *}
   234 
   235 
   236 subsection {* Intimate connection between logic and system runtime *}
   237 
   238 text {*
   239   The toolbox of static evaluation conversions forms a reasonable base
   240   to interweave generated code and system tools.  However in some
   241   situations more direct interaction is desirable.
   242 *}
   243 
   244 
   245 subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq} *}
   246 
   247 text {*
   248   The @{text code} antiquotation allows to include constants from
   249   generated code directly into ML system code, as in the following toy
   250   example:
   251 *}
   252 
   253 datatype %quote form = T | F | And form form | Or form form (*<*)
   254 
   255 (*>*) ML %quotett {*
   256   fun eval_form @{code T} = true
   257     | eval_form @{code F} = false
   258     | eval_form (@{code And} (p, q)) =
   259         eval_form p andalso eval_form q
   260     | eval_form (@{code Or} (p, q)) =
   261         eval_form p orelse eval_form q;
   262 *}
   263 
   264 text {*
   265   \noindent @{text code} takes as argument the name of a constant;
   266   after the whole ML is read, the necessary code is generated
   267   transparently and the corresponding constant names are inserted.
   268   This technique also allows to use pattern matching on constructors
   269   stemming from compiled datatypes.  Note that the @{text code}
   270   antiquotation may not refer to constants which carry adaptations;
   271   here you have to refer to the corresponding adapted code directly.
   272 
   273   For a less simplistic example, theory @{text Approximation} in
   274   the @{text Decision_Procs} session is a good reference.
   275 *}
   276 
   277 
   278 subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
   279 
   280 text {*
   281   The @{text code} antiquoation is lightweight, but the generated code
   282   is only accessible while the ML section is processed.  Sometimes this
   283   is not appropriate, especially if the generated code contains datatype
   284   declarations which are shared with other parts of the system.  In these
   285   cases, @{command_def code_reflect} can be used:
   286 *}
   287 
   288 code_reflect %quote Sum_Type
   289   datatypes sum = Inl | Inr
   290   functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
   291 
   292 text {*
   293   \noindent @{command_def code_reflect} takes a structure name and
   294   references to datatypes and functions; for these code is compiled
   295   into the named ML structure and the \emph{Eval} target is modified
   296   in a way that future code generation will reference these
   297   precompiled versions of the given datatypes and functions.  This
   298   also allows to refer to the referenced datatypes and functions from
   299   arbitrary ML code as well.
   300 
   301   A typical example for @{command code_reflect} can be found in the
   302   @{theory Predicate} theory.
   303 *}
   304 
   305 
   306 subsubsection {* Separate compilation -- @{text code_reflect} *}
   307 
   308 text {*
   309   For technical reasons it is sometimes necessary to separate
   310   generation and compilation of code which is supposed to be used in
   311   the system runtime.  For this @{command code_reflect} with an
   312   optional @{text "file"} argument can be used:
   313 *}
   314 
   315 code_reflect %quote Rat
   316   datatypes rat = Frct
   317   functions Fract
   318     "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   319     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   320   file "examples/rat.ML"
   321 
   322 text {*
   323   \noindent This merely generates the referenced code to the given
   324   file which can be included into the system runtime later on.
   325 *}
   326 
   327 end
   328