38510
|
1 |
theory Evaluation
|
|
2 |
imports Setup
|
|
3 |
begin
|
|
4 |
|
|
5 |
section {* Evaluation *}
|
|
6 |
|
39599
|
7 |
text {*
|
|
8 |
Recalling \secref{sec:principle}, code generation turns a system of
|
|
9 |
equations into a program with the \emph{same} equational semantics.
|
|
10 |
As a consequence, this program can be used as a \emph{rewrite
|
|
11 |
engine} for terms: rewriting a term @{term "t"} using a program to a
|
|
12 |
term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}. This
|
|
13 |
application of code generation in the following is referred to as
|
|
14 |
\emph{evaluation}.
|
|
15 |
*}
|
38510
|
16 |
|
|
17 |
|
|
18 |
subsection {* Evaluation techniques *}
|
|
19 |
|
39599
|
20 |
text {*
|
|
21 |
The existing infrastructure provides a rich palett of evaluation
|
|
22 |
techniques, each comprising different aspects:
|
|
23 |
|
|
24 |
\begin{description}
|
|
25 |
|
|
26 |
\item[Expressiveness.] Depending on how good symbolic computation
|
|
27 |
is supported, the class of terms which can be evaluated may be
|
|
28 |
bigger or smaller.
|
38510
|
29 |
|
39599
|
30 |
\item[Efficiency.] The more machine-near the technique, the
|
|
31 |
faster it is.
|
38510
|
32 |
|
39599
|
33 |
\item[Trustability.] Techniques which a huge (and also probably
|
|
34 |
more configurable infrastructure) are more fragile and less
|
|
35 |
trustable.
|
|
36 |
|
|
37 |
\end{description}
|
|
38 |
*}
|
38510
|
39 |
|
|
40 |
|
39599
|
41 |
subsubsection {* The simplifier (@{text simp}) *}
|
38510
|
42 |
|
39599
|
43 |
text {*
|
|
44 |
The simplest way for evaluation is just using the simplifier with
|
|
45 |
the original code equations of the underlying program. This gives
|
|
46 |
fully symbolic evaluation and highest trustablity, with the usual
|
|
47 |
performance of the simplifier. Note that for operations on abstract
|
|
48 |
datatypes (cf.~\secref{sec:invariant}), the original theorems as
|
|
49 |
given by the users are used, not the modified ones.
|
|
50 |
*}
|
38510
|
51 |
|
|
52 |
|
39599
|
53 |
subsubsection {* Normalization by evaluation (@{text nbe}) *}
|
38510
|
54 |
|
39599
|
55 |
text {*
|
|
56 |
Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
|
|
57 |
provides a comparably fast partially symbolic evaluation which
|
|
58 |
permits also normalization of functions and uninterpreted symbols;
|
|
59 |
the stack of code to be trusted is considerable.
|
|
60 |
*}
|
38510
|
61 |
|
|
62 |
|
39599
|
63 |
subsubsection {* Evaluation in ML (@{text code}) *}
|
|
64 |
|
|
65 |
text {*
|
|
66 |
Highest performance can be achieved by evaluation in ML, at the cost
|
|
67 |
of being restricted to ground results and a layered stack of code to
|
|
68 |
be trusted, including code generator configurations by the user.
|
38510
|
69 |
|
39599
|
70 |
Evaluation is carried out in a target language \emph{Eval} which
|
|
71 |
inherits from \emph{SML} but for convenience uses parts of the
|
|
72 |
Isabelle runtime environment. The soundness of computation carried
|
|
73 |
out there crucially on the correctness of the code generator; this
|
|
74 |
is one of the reasons why you should not use adaptation (see
|
|
75 |
\secref{sec:adaptation}) frivolously.
|
|
76 |
*}
|
38510
|
77 |
|
|
78 |
|
39599
|
79 |
subsection {* Aspects of evaluation *}
|
38510
|
80 |
|
|
81 |
text {*
|
39599
|
82 |
Each of the techniques can be combined with different aspects. The
|
|
83 |
most important distinction is between dynamic and static evaluation.
|
|
84 |
Dynamic evaluation takes the code generator configuration \qt{as it
|
|
85 |
is} at the point where evaluation is issued. Best example is the
|
|
86 |
@{command_def value} command which allows ad-hoc evaluation of
|
|
87 |
terms:
|
38510
|
88 |
*}
|
|
89 |
|
|
90 |
value %quote "42 / (12 :: rat)"
|
|
91 |
|
|
92 |
text {*
|
39599
|
93 |
\noindent By default @{command value} tries all available evaluation
|
|
94 |
techniques and prints the result of the first succeeding one. A particular
|
|
95 |
technique may be specified in square brackets, e.g.
|
38510
|
96 |
*}
|
|
97 |
|
39599
|
98 |
value %quote [nbe] "42 / (12 :: rat)"
|
38510
|
99 |
|
|
100 |
text {*
|
39599
|
101 |
Static evaluation freezes the code generator configuration at a
|
|
102 |
certain point and uses this context whenever evaluation is issued
|
|
103 |
later on. This is particularly appropriate for proof procedures
|
|
104 |
which use evaluation, since then the behaviour of evaluation is not
|
|
105 |
changed or even compromised later on by actions of the user.
|
|
106 |
|
|
107 |
As a technical complication, terms after evaluation in ML must be
|
|
108 |
turned into Isabelle's internal term representation again. Since
|
|
109 |
this is also configurable, it is never fully trusted. For this
|
|
110 |
reason, evaluation in ML comes with further aspects:
|
|
111 |
|
|
112 |
\begin{description}
|
|
113 |
|
|
114 |
\item[Plain evaluation.] A term is normalized using the provided
|
|
115 |
term reconstruction from ML to Isabelle; for applications which
|
|
116 |
do not need to be fully trusted.
|
|
117 |
|
|
118 |
\item[Property conversion.] Evaluates propositions; since these
|
|
119 |
are monomorphic, the term reconstruction is fixed once and for all
|
|
120 |
and therefore trustable.
|
|
121 |
|
|
122 |
\item[Conversion.] Evaluates an arbitrary term @{term "t"} first
|
|
123 |
by plain evaluation and certifies the result @{term "t'"} by
|
|
124 |
checking the equation @{term "t \<equiv> t'"} using property
|
|
125 |
conversion.
|
|
126 |
|
|
127 |
\end{description}
|
|
128 |
|
|
129 |
\noindent The picture is further complicated by the roles of
|
|
130 |
exceptions. Here three cases have to be distinguished:
|
|
131 |
|
|
132 |
\begin{itemize}
|
|
133 |
|
|
134 |
\item Evaluation of @{term t} terminates with a result @{term
|
|
135 |
"t'"}.
|
|
136 |
|
|
137 |
\item Evaluation of @{term t} terminates which en exception
|
|
138 |
indicating a pattern match failure or a not-implemented
|
|
139 |
function. As sketched in \secref{sec:partiality}, this can be
|
|
140 |
interpreted as partiality.
|
|
141 |
|
|
142 |
\item Evaluation raise any other kind of exception.
|
|
143 |
|
|
144 |
\end{itemize}
|
|
145 |
|
|
146 |
\noindent For conversions, the first case yields the equation @{term
|
|
147 |
"t = t'"}, the second defaults to reflexivity @{term "t = t"}.
|
|
148 |
Exceptions of the third kind are propagted to the user.
|
|
149 |
|
|
150 |
By default return values of plain evaluation are optional, yielding
|
|
151 |
@{text "SOME t'"} in the first case, @{text "NONE"} and in the
|
|
152 |
second propagating the exception in the third case. A strict
|
|
153 |
variant of plain evaluation either yields @{text "t'"} or propagates
|
|
154 |
any exception, a liberal variant caputures any exception in a result
|
|
155 |
of type @{text "Exn.result"}.
|
|
156 |
|
|
157 |
For property conversion (which coincides with conversion except for
|
|
158 |
evaluation in ML), methods are provided which solve a given goal by
|
|
159 |
evaluation.
|
38510
|
160 |
*}
|
|
161 |
|
|
162 |
|
39599
|
163 |
subsection {* Schematic overview *}
|
|
164 |
|
|
165 |
(*FIXME rotatebox?*)
|
38510
|
166 |
|
|
167 |
text {*
|
39599
|
168 |
\begin{tabular}{ll||c|c|c}
|
|
169 |
& & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
|
|
170 |
dynamic & interactive evaluation
|
|
171 |
& @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
|
|
172 |
\tabularnewline
|
|
173 |
& plain evaluation & & & @{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline
|
|
174 |
& evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
|
|
175 |
& property conversion & & & @{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline
|
|
176 |
& conversion & @{ML "Code_Simp.dynamic_eval_conv"} & @{ML "Nbe.dynamic_eval_conv"}
|
|
177 |
& @{ML "Code_Evaluation.dynamic_eval_conv"} \tabularnewline \hline \hline
|
|
178 |
static & plain evaluation & & & @{ML "Code_Evaluation.static_value"} \tabularnewline \hline
|
|
179 |
& property conversion & &
|
|
180 |
& @{ML "Code_Runtime.static_holds_conv"} \tabularnewline \hline
|
|
181 |
& conversion & @{ML "Code_Simp.static_eval_conv"}
|
|
182 |
& @{ML "Nbe.static_eval_conv"}
|
|
183 |
& @{ML "Code_Evaluation.static_eval_conv"}
|
|
184 |
\end{tabular}
|
|
185 |
*}
|
|
186 |
|
|
187 |
|
|
188 |
subsection {* Intimate connection between logic and system runtime *}
|
|
189 |
|
|
190 |
text {* FIXME *}
|
|
191 |
|
|
192 |
|
|
193 |
subsubsection {* Static embedding of generated code into system runtime -- the code antiquotation *}
|
|
194 |
|
|
195 |
text {*
|
|
196 |
FIXME
|
|
197 |
|
38510
|
198 |
In scenarios involving techniques like reflection it is quite common
|
39599
|
199 |
that code generated from a theory forms the basis for implementing a
|
|
200 |
proof procedure in @{text SML}. To facilitate interfacing of
|
|
201 |
generated code with system code, the code generator provides a
|
|
202 |
@{text code} antiquotation:
|
38510
|
203 |
*}
|
|
204 |
|
|
205 |
datatype %quote form = T | F | And form form | Or form form (*<*)
|
|
206 |
|
|
207 |
(*>*) ML %quotett {*
|
|
208 |
fun eval_form @{code T} = true
|
|
209 |
| eval_form @{code F} = false
|
|
210 |
| eval_form (@{code And} (p, q)) =
|
|
211 |
eval_form p andalso eval_form q
|
|
212 |
| eval_form (@{code Or} (p, q)) =
|
|
213 |
eval_form p orelse eval_form q;
|
|
214 |
*}
|
|
215 |
|
|
216 |
text {*
|
|
217 |
\noindent @{text code} takes as argument the name of a constant; after the
|
|
218 |
whole @{text SML} is read, the necessary code is generated transparently
|
|
219 |
and the corresponding constant names are inserted. This technique also
|
|
220 |
allows to use pattern matching on constructors stemming from compiled
|
|
221 |
@{text "datatypes"}.
|
|
222 |
|
39067
|
223 |
For a less simplistic example, theory @{text Ferrack} is
|
38510
|
224 |
a good reference.
|
|
225 |
*}
|
|
226 |
|
|
227 |
|
39599
|
228 |
subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
|
|
229 |
|
|
230 |
text {* FIXME @{command_def code_reflect} *}
|
|
231 |
|
|
232 |
subsubsection {* Separate compilation -- @{text code_reflect} *}
|
|
233 |
|
|
234 |
text {* FIXME *}
|
|
235 |
|
38510
|
236 |
end
|