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