src/Doc/Codegen/Evaluation.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 66453 cc19f7ca2ed6
child 69422 472af2d7835d
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 theory Evaluation
     2 imports Codegen_Basics.Setup
     3 begin (*<*)
     4 
     5 ML \<open>
     6   Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
     7 \<close> (*>*)
     8 
     9 section \<open>Evaluation \label{sec:evaluation}\<close>
    10 
    11 text \<open>
    12   Recalling \secref{sec:principle}, code generation turns a system of
    13   equations into a program with the \emph{same} equational semantics.
    14   As a consequence, this program can be used as a \emph{rewrite
    15   engine} for terms: rewriting a term @{term "t"} using a program to a
    16   term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}.  This
    17   application of code generation in the following is referred to as
    18   \emph{evaluation}.
    19 \<close>
    20 
    21 
    22 subsection \<open>Evaluation techniques\<close>
    23 
    24 text \<open>
    25   There is a rich palette of evaluation
    26   techniques, each comprising different aspects:
    27 
    28   \begin{description}
    29 
    30     \item[Expressiveness.]  Depending on the extent to which symbolic
    31       computation is possible, the class of terms which can be evaluated
    32       can be bigger or smaller.
    33 
    34     \item[Efficiency.]  The more machine-near the technique, the
    35       faster it is.
    36 
    37     \item[Trustability.]  Techniques which a huge (and also probably
    38       more configurable infrastructure) are more fragile and less
    39       trustable.
    40 
    41   \end{description}
    42 \<close>
    43 
    44 
    45 subsubsection \<open>The simplifier (@{text simp})\<close>
    46 
    47 text \<open>
    48   The simplest way for evaluation is just using the simplifier with
    49   the original code equations of the underlying program.  This gives
    50   fully symbolic evaluation and highest trustablity, with the usual
    51   performance of the simplifier.  Note that for operations on abstract
    52   datatypes (cf.~\secref{sec:invariant}), the original theorems as
    53   given by the users are used, not the modified ones.
    54 \<close>
    55 
    56 
    57 subsubsection \<open>Normalization by evaluation (@{text nbe})\<close>
    58 
    59 text \<open>
    60   Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
    61   provides a comparably fast partially symbolic evaluation which
    62   permits also normalization of functions and uninterpreted symbols;
    63   the stack of code to be trusted is considerable.
    64 \<close>
    65 
    66 
    67 subsubsection \<open>Evaluation in ML (@{text code})\<close>
    68 
    69 text \<open>
    70   Considerable performance can be achieved using evaluation in ML, at the cost
    71   of being restricted to ground results and a layered stack of code to
    72   be trusted, including a user's specific code generator setup.
    73 
    74   Evaluation is carried out in a target language \emph{Eval} which
    75   inherits from \emph{SML} but for convenience uses parts of the
    76   Isabelle runtime environment.  Hence soundness depends crucially
    77   on the correctness of the code generator setup; this is one of the
    78   reasons why you should not use adaptation (see \secref{sec:adaptation})
    79   frivolously.
    80 \<close>
    81 
    82 
    83 subsection \<open>Dynamic evaluation\<close>
    84 
    85 text \<open>
    86   Dynamic evaluation takes the code generator configuration \qt{as it
    87   is} at the point where evaluation is issued and computes
    88   a corresponding result.  Best example is the
    89   @{command_def value} command for ad-hoc evaluation of
    90   terms:
    91 \<close>
    92 
    93 value %quote "42 / (12 :: rat)"
    94 
    95 text \<open>
    96   \noindent @{command value} tries first to evaluate using ML, falling
    97   back to normalization by evaluation if this fails.
    98 
    99   A particular technique may be specified in square brackets, e.g.
   100 \<close>
   101 
   102 value %quote [nbe] "42 / (12 :: rat)"
   103 
   104 text \<open>
   105   To employ dynamic evaluation in documents, there is also
   106   a @{text value} antiquotation with the same evaluation techniques 
   107   as @{command value}.
   108 \<close>
   109 
   110   
   111 subsubsection \<open>Term reconstruction in ML\<close>
   112 
   113 text \<open>
   114   Results from evaluation in ML must be
   115   turned into Isabelle's internal term representation again.  Since
   116   that setup is highly configurable, it is never assumed to be trustable. 
   117   Hence evaluation in ML provides no full term reconstruction
   118   but distinguishes the following kinds:
   119 
   120   \begin{description}
   121 
   122     \item[Plain evaluation.]  A term is normalized using the vanilla
   123       term reconstruction from ML to Isabelle; this is a pragmatic
   124       approach for applications which do not need trustability.
   125 
   126     \item[Property conversion.]  Evaluates propositions; since these
   127       are monomorphic, the term reconstruction is fixed once and for all
   128       and therefore trustable -- in the sense that only the regular
   129       code generator setup has to be trusted, without relying
   130       on term reconstruction from ML to Isabelle.
   131 
   132   \end{description}
   133 
   134   \noindent The different degree of trustability is also manifest in the
   135   types of the corresponding ML functions: plain evaluation
   136   operates on uncertified terms, whereas property conversion
   137   operates on certified terms.
   138 \<close>
   139 
   140 
   141 subsubsection \<open>The partiality principle \label{sec:partiality_principle}\<close>
   142 
   143 text \<open>
   144   During evaluation exceptions indicating a pattern
   145   match failure or a non-implemented function are treated specially:
   146   as sketched in \secref{sec:partiality}, such
   147   exceptions can be interpreted as partiality.  For plain evaluation,
   148   the result hence is optional; property conversion falls back
   149   to reflexivity in such cases.
   150 \<close>
   151   
   152 
   153 subsubsection \<open>Schematic overview\<close>
   154 
   155 text \<open>
   156   \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
   157   \fontsize{9pt}{12pt}\selectfont
   158   \begin{tabular}{l||c|c|c}
   159     & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
   160     interactive evaluation & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"} \tabularnewline
   161     plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline
   162     evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
   163     property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline
   164     conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
   165   \end{tabular}
   166 \<close>
   167 
   168   
   169 subsection \<open>Static evaluation\<close>
   170   
   171 text \<open>
   172   When implementing proof procedures using evaluation,
   173   in most cases the code generator setup is appropriate
   174   \qt{as it was} when the proof procedure was written in ML,
   175   not an arbitrary later potentially modified setup.  This is
   176   called static evaluation.
   177 \<close>
   178 
   179 
   180 subsubsection \<open>Static evaluation using @{text simp} and @{text nbe}\<close>
   181   
   182 text \<open>
   183   For @{text simp} and @{text nbe} static evaluation can be achieved using 
   184   @{ML Code_Simp.static_conv} and @{ML Nbe.static_conv}.
   185   Note that @{ML Nbe.static_conv} by its very nature
   186   requires an invocation of the ML compiler for every call,
   187   which can produce significant overhead.
   188 \<close>
   189 
   190 
   191 subsubsection \<open>Intimate connection between logic and system runtime\<close>
   192 
   193 text \<open>
   194   Static evaluation for @{text eval} operates differently --
   195   the required generated code is inserted directly into an ML
   196   block using antiquotations.  The idea is that generated
   197   code performing static evaluation (called a \<^emph>\<open>computation\<close>)
   198   is compiled once and for all such that later calls do not
   199   require any invocation of the code generator or the ML
   200   compiler at all.  This topic deserved a dedicated chapter
   201   \secref{sec:computations}.
   202 \<close>
   203   
   204 end