author | wenzelm |
Fri, 05 Apr 2019 17:05:32 +0200 | |
changeset 70067 | 9b34dbeb1103 |
parent 69658 | 7357a4f79f60 |
child 72375 | e48d93811ed7 |
permissions | -rw-r--r-- |
38510 | 1 |
theory Evaluation |
69422
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
wenzelm
parents:
66453
diff
changeset
|
2 |
imports Setup |
59378
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
3 |
begin (*<*) |
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
4 |
|
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
5 |
ML \<open> |
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
6 |
Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples")) |
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
7 |
\<close> (*>*) |
38510 | 8 |
|
59377 | 9 |
section \<open>Evaluation \label{sec:evaluation}\<close> |
38510 | 10 |
|
59377 | 11 |
text \<open> |
39599 | 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 |
|
69597 | 15 |
engine} for terms: rewriting a term \<^term>\<open>t\<close> using a program to a |
16 |
term \<^term>\<open>t'\<close> yields the theorems \<^prop>\<open>t \<equiv> t'\<close>. This |
|
39599 | 17 |
application of code generation in the following is referred to as |
18 |
\emph{evaluation}. |
|
59377 | 19 |
\<close> |
38510 | 20 |
|
21 |
||
59377 | 22 |
subsection \<open>Evaluation techniques\<close> |
38510 | 23 |
|
59377 | 24 |
text \<open> |
65041 | 25 |
There is a rich palette of evaluation |
39599 | 26 |
techniques, each comprising different aspects: |
27 |
||
28 |
\begin{description} |
|
29 |
||
65041 | 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. |
|
38510 | 33 |
|
39599 | 34 |
\item[Efficiency.] The more machine-near the technique, the |
35 |
faster it is. |
|
38510 | 36 |
|
39599 | 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} |
|
59377 | 42 |
\<close> |
38510 | 43 |
|
44 |
||
69505 | 45 |
subsubsection \<open>The simplifier (\<open>simp\<close>)\<close> |
38510 | 46 |
|
59377 | 47 |
text \<open> |
39599 | 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. |
|
59377 | 54 |
\<close> |
38510 | 55 |
|
56 |
||
69505 | 57 |
subsubsection \<open>Normalization by evaluation (\<open>nbe\<close>)\<close> |
38510 | 58 |
|
59377 | 59 |
text \<open> |
58620 | 60 |
Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"} |
39599 | 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. |
|
59377 | 64 |
\<close> |
38510 | 65 |
|
66 |
||
69505 | 67 |
subsubsection \<open>Evaluation in ML (\<open>code\<close>)\<close> |
39599 | 68 |
|
59377 | 69 |
text \<open> |
65041 | 70 |
Considerable performance can be achieved using evaluation in ML, at the cost |
39599 | 71 |
of being restricted to ground results and a layered stack of code to |
65041 | 72 |
be trusted, including a user's specific code generator setup. |
38510 | 73 |
|
39599 | 74 |
Evaluation is carried out in a target language \emph{Eval} which |
75 |
inherits from \emph{SML} but for convenience uses parts of the |
|
65041 | 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. |
|
59377 | 80 |
\<close> |
38510 | 81 |
|
82 |
||
65041 | 83 |
subsection \<open>Dynamic evaluation\<close> |
38510 | 84 |
|
59377 | 85 |
text \<open> |
39599 | 86 |
Dynamic evaluation takes the code generator configuration \qt{as it |
65041 | 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 |
|
39599 | 90 |
terms: |
59377 | 91 |
\<close> |
38510 | 92 |
|
93 |
value %quote "42 / (12 :: rat)" |
|
94 |
||
59377 | 95 |
text \<open> |
56927 | 96 |
\noindent @{command value} tries first to evaluate using ML, falling |
97 |
back to normalization by evaluation if this fails. |
|
38510 | 98 |
|
58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
99 |
A particular technique may be specified in square brackets, e.g. |
59377 | 100 |
\<close> |
58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
101 |
|
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
102 |
value %quote [nbe] "42 / (12 :: rat)" |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
103 |
|
59377 | 104 |
text \<open> |
65041 | 105 |
To employ dynamic evaluation in documents, there is also |
69505 | 106 |
a \<open>value\<close> antiquotation with the same evaluation techniques |
56927 | 107 |
as @{command value}. |
65041 | 108 |
\<close> |
43656
9ece73262746
adding documentation of the value antiquotation to the code generation manual
bulwahn
parents:
41184
diff
changeset
|
109 |
|
65041 | 110 |
|
111 |
subsubsection \<open>Term reconstruction in ML\<close> |
|
39599 | 112 |
|
65041 | 113 |
text \<open> |
114 |
Results from evaluation in ML must be |
|
39599 | 115 |
turned into Isabelle's internal term representation again. Since |
65041 | 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: |
|
39599 | 119 |
|
120 |
\begin{description} |
|
121 |
||
65041 | 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. |
|
39599 | 125 |
|
126 |
\item[Property conversion.] Evaluates propositions; since these |
|
127 |
are monomorphic, the term reconstruction is fixed once and for all |
|
65041 | 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. |
|
39599 | 131 |
|
132 |
\end{description} |
|
133 |
||
65041 | 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. |
|
59377 | 138 |
\<close> |
38510 | 139 |
|
140 |
||
65041 | 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> |
|
39599 | 154 |
|
59377 | 155 |
text \<open> |
39693 | 156 |
\newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont} |
157 |
\fontsize{9pt}{12pt}\selectfont |
|
65041 | 158 |
\begin{tabular}{l||c|c|c} |
69505 | 159 |
& \<open>simp\<close> & \<open>nbe\<close> & \<open>code\<close> \tabularnewline \hline \hline |
160 |
interactive evaluation & @{command value} \<open>[simp]\<close> & @{command value} \<open>[nbe]\<close> & @{command value} \<open>[code]\<close> \tabularnewline |
|
69597 | 161 |
plain evaluation & & & \ttsize\<^ML>\<open>Code_Evaluation.dynamic_value\<close> \tabularnewline \hline |
65041 | 162 |
evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline |
69597 | 163 |
property conversion & & & \ttsize\<^ML>\<open>Code_Runtime.dynamic_holds_conv\<close> \tabularnewline \hline |
164 |
conversion & \ttsize\<^ML>\<open>Code_Simp.dynamic_conv\<close> & \ttsize\<^ML>\<open>Nbe.dynamic_conv\<close> |
|
39599 | 165 |
\end{tabular} |
59377 | 166 |
\<close> |
39599 | 167 |
|
65041 | 168 |
|
169 |
subsection \<open>Static evaluation\<close> |
|
170 |
||
59377 | 171 |
text \<open> |
65041 | 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. |
|
59377 | 177 |
\<close> |
52287 | 178 |
|
179 |
||
69505 | 180 |
subsubsection \<open>Static evaluation using \<open>simp\<close> and \<open>nbe\<close>\<close> |
65041 | 181 |
|
59377 | 182 |
text \<open> |
69505 | 183 |
For \<open>simp\<close> and \<open>nbe\<close> static evaluation can be achieved using |
69597 | 184 |
\<^ML>\<open>Code_Simp.static_conv\<close> and \<^ML>\<open>Nbe.static_conv\<close>. |
185 |
Note that \<^ML>\<open>Nbe.static_conv\<close> by its very nature |
|
65041 | 186 |
requires an invocation of the ML compiler for every call, |
187 |
which can produce significant overhead. |
|
59377 | 188 |
\<close> |
38510 | 189 |
|
190 |
||
65041 | 191 |
subsubsection \<open>Intimate connection between logic and system runtime\<close> |
39609 | 192 |
|
59377 | 193 |
text \<open> |
69505 | 194 |
Static evaluation for \<open>eval\<close> operates differently -- |
65041 | 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 |
|
69658 | 200 |
compiler at all. This topic deserves a dedicated chapter |
65041 | 201 |
\secref{sec:computations}. |
59377 | 202 |
\<close> |
65041 | 203 |
|
38510 | 204 |
end |