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