1theory Evaluation 2imports Codegen_Basics.Setup 3begin (*<*) 4 5ML \<open> 6 Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples")) 7\<close> (*>*) 8 9section \<open>Evaluation \label{sec:evaluation}\<close> 10 11text \<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 22subsection \<open>Evaluation techniques\<close> 23 24text \<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 45subsubsection \<open>The simplifier (@{text simp})\<close> 46 47text \<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 57subsubsection \<open>Normalization by evaluation (@{text nbe})\<close> 58 59text \<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 67subsubsection \<open>Evaluation in ML (@{text code})\<close> 68 69text \<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 83subsection \<open>Dynamic evaluation\<close> 84 85text \<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 93value %quote "42 / (12 :: rat)" 94 95text \<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 102value %quote [nbe] "42 / (12 :: rat)" 103 104text \<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 111subsubsection \<open>Term reconstruction in ML\<close> 112 113text \<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 141subsubsection \<open>The partiality principle \label{sec:partiality_principle}\<close> 142 143text \<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 153subsubsection \<open>Schematic overview\<close> 154 155text \<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 169subsection \<open>Static evaluation\<close> 170 171text \<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 180subsubsection \<open>Static evaluation using @{text simp} and @{text nbe}\<close> 181 182text \<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 191subsubsection \<open>Intimate connection between logic and system runtime\<close> 192 193text \<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 204end 205