author | haftmann |
Thu, 15 Jan 2015 13:39:41 +0100 | |
changeset 59377 | 056945909f60 |
parent 59335 | e743ce816cf6 |
child 59378 | 065f349852e6 |
permissions | -rw-r--r-- |
38510 | 1 |
theory Evaluation |
2 |
imports Setup |
|
3 |
begin |
|
4 |
||
59377 | 5 |
section \<open>Evaluation \label{sec:evaluation}\<close> |
38510 | 6 |
|
59377 | 7 |
text \<open> |
39599 | 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}. |
|
59377 | 15 |
\<close> |
38510 | 16 |
|
17 |
||
59377 | 18 |
subsection \<open>Evaluation techniques\<close> |
38510 | 19 |
|
59377 | 20 |
text \<open> |
40350 | 21 |
The existing infrastructure provides a rich palette of evaluation |
39599 | 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} |
|
59377 | 38 |
\<close> |
38510 | 39 |
|
40 |
||
59377 | 41 |
subsubsection \<open>The simplifier (@{text simp})\<close> |
38510 | 42 |
|
59377 | 43 |
text \<open> |
39599 | 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. |
|
59377 | 50 |
\<close> |
38510 | 51 |
|
52 |
||
59377 | 53 |
subsubsection \<open>Normalization by evaluation (@{text nbe})\<close> |
38510 | 54 |
|
59377 | 55 |
text \<open> |
58620 | 56 |
Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"} |
39599 | 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. |
|
59377 | 60 |
\<close> |
38510 | 61 |
|
62 |
||
59377 | 63 |
subsubsection \<open>Evaluation in ML (@{text code})\<close> |
39599 | 64 |
|
59377 | 65 |
text \<open> |
39599 | 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 |
|
39609 | 73 |
out there depends crucially on the correctness of the code |
39643 | 74 |
generator setup; this is one of the reasons why you should not use |
39609 | 75 |
adaptation (see \secref{sec:adaptation}) frivolously. |
59377 | 76 |
\<close> |
38510 | 77 |
|
78 |
||
59377 | 79 |
subsection \<open>Aspects of evaluation\<close> |
38510 | 80 |
|
59377 | 81 |
text \<open> |
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: |
|
59377 | 88 |
\<close> |
38510 | 89 |
|
90 |
value %quote "42 / (12 :: rat)" |
|
91 |
||
59377 | 92 |
text \<open> |
56927 | 93 |
\noindent @{command value} tries first to evaluate using ML, falling |
94 |
back to normalization by evaluation if this fails. |
|
38510 | 95 |
|
58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
96 |
A particular technique may be specified in square brackets, e.g. |
59377 | 97 |
\<close> |
58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
98 |
|
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
99 |
value %quote [nbe] "42 / (12 :: rat)" |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
100 |
|
59377 | 101 |
text \<open> |
43656
9ece73262746
adding documentation of the value antiquotation to the code generation manual
bulwahn
parents:
41184
diff
changeset
|
102 |
To employ dynamic evaluation in the document generation, there is also |
56927 | 103 |
a @{text value} antiquotation with the same evaluation techniques |
104 |
as @{command value}. |
|
43656
9ece73262746
adding documentation of the value antiquotation to the code generation manual
bulwahn
parents:
41184
diff
changeset
|
105 |
|
39599 | 106 |
Static evaluation freezes the code generator configuration at a |
107 |
certain point and uses this context whenever evaluation is issued |
|
108 |
later on. This is particularly appropriate for proof procedures |
|
109 |
which use evaluation, since then the behaviour of evaluation is not |
|
110 |
changed or even compromised later on by actions of the user. |
|
111 |
||
112 |
As a technical complication, terms after evaluation in ML must be |
|
113 |
turned into Isabelle's internal term representation again. Since |
|
114 |
this is also configurable, it is never fully trusted. For this |
|
115 |
reason, evaluation in ML comes with further aspects: |
|
116 |
||
117 |
\begin{description} |
|
118 |
||
119 |
\item[Plain evaluation.] A term is normalized using the provided |
|
120 |
term reconstruction from ML to Isabelle; for applications which |
|
121 |
do not need to be fully trusted. |
|
122 |
||
123 |
\item[Property conversion.] Evaluates propositions; since these |
|
124 |
are monomorphic, the term reconstruction is fixed once and for all |
|
125 |
and therefore trustable. |
|
126 |
||
127 |
\item[Conversion.] Evaluates an arbitrary term @{term "t"} first |
|
128 |
by plain evaluation and certifies the result @{term "t'"} by |
|
129 |
checking the equation @{term "t \<equiv> t'"} using property |
|
130 |
conversion. |
|
131 |
||
132 |
\end{description} |
|
133 |
||
134 |
\noindent The picture is further complicated by the roles of |
|
135 |
exceptions. Here three cases have to be distinguished: |
|
136 |
||
137 |
\begin{itemize} |
|
138 |
||
139 |
\item Evaluation of @{term t} terminates with a result @{term |
|
140 |
"t'"}. |
|
141 |
||
142 |
\item Evaluation of @{term t} terminates which en exception |
|
40350 | 143 |
indicating a pattern match failure or a non-implemented |
39599 | 144 |
function. As sketched in \secref{sec:partiality}, this can be |
145 |
interpreted as partiality. |
|
146 |
||
39643 | 147 |
\item Evaluation raises any other kind of exception. |
39599 | 148 |
|
149 |
\end{itemize} |
|
150 |
||
151 |
\noindent For conversions, the first case yields the equation @{term |
|
152 |
"t = t'"}, the second defaults to reflexivity @{term "t = t"}. |
|
39643 | 153 |
Exceptions of the third kind are propagated to the user. |
39599 | 154 |
|
155 |
By default return values of plain evaluation are optional, yielding |
|
40350 | 156 |
@{text "SOME t'"} in the first case, @{text "NONE"} in the |
157 |
second, and propagating the exception in the third case. A strict |
|
39599 | 158 |
variant of plain evaluation either yields @{text "t'"} or propagates |
51713 | 159 |
any exception, a liberal variant captures any exception in a result |
39599 | 160 |
of type @{text "Exn.result"}. |
161 |
||
162 |
For property conversion (which coincides with conversion except for |
|
163 |
evaluation in ML), methods are provided which solve a given goal by |
|
164 |
evaluation. |
|
59377 | 165 |
\<close> |
38510 | 166 |
|
167 |
||
59377 | 168 |
subsection \<open>Schematic overview\<close> |
39599 | 169 |
|
59377 | 170 |
text \<open> |
39693 | 171 |
\newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont} |
172 |
\fontsize{9pt}{12pt}\selectfont |
|
39599 | 173 |
\begin{tabular}{ll||c|c|c} |
174 |
& & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline |
|
58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
175 |
\multirow{5}{1ex}{\rotatebox{90}{dynamic}} |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
176 |
& interactive evaluation |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
177 |
& @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"} |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
178 |
\tabularnewline |
39693 | 179 |
& plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5} |
39599 | 180 |
& evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline |
39693 | 181 |
& property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5} |
41184 | 182 |
& conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"} |
183 |
& \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline |
|
39693 | 184 |
\multirow{3}{1ex}{\rotatebox{90}{static}} |
41184 | 185 |
& plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5} |
39599 | 186 |
& property conversion & & |
39693 | 187 |
& \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5} |
41184 | 188 |
& conversion & \ttsize@{ML "Code_Simp.static_conv"} |
189 |
& \ttsize@{ML "Nbe.static_conv"} |
|
190 |
& \ttsize@{ML "Code_Evaluation.static_conv"} |
|
39599 | 191 |
\end{tabular} |
59377 | 192 |
\<close> |
39599 | 193 |
|
194 |
||
59377 | 195 |
subsection \<open>Preprocessing HOL terms into evaluable shape\<close> |
52287 | 196 |
|
59377 | 197 |
text \<open> |
52287 | 198 |
When integration decision procedures developed inside HOL into HOL itself, |
199 |
it is necessary to somehow get from the Isabelle/ML representation to |
|
200 |
the representation used by the decision procedure itself (``reification''). |
|
201 |
One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}). |
|
202 |
Another option is to use pre-existing infrastructure in HOL: |
|
203 |
@{ML "Reification.conv"} and @{ML "Reification.tac"} |
|
204 |
||
205 |
An simplistic example: |
|
59377 | 206 |
\<close> |
52287 | 207 |
|
58310 | 208 |
datatype %quote form_ord = T | F | Less nat nat |
52287 | 209 |
| And form_ord form_ord | Or form_ord form_ord | Neg form_ord |
210 |
||
211 |
primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool" |
|
212 |
where |
|
213 |
"interp T vs \<longleftrightarrow> True" |
|
214 |
| "interp F vs \<longleftrightarrow> False" |
|
215 |
| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j" |
|
216 |
| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs" |
|
217 |
| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs" |
|
218 |
| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs" |
|
219 |
||
59377 | 220 |
text \<open> |
52287 | 221 |
The datatype @{type form_ord} represents formulae whose semantics is given by |
222 |
@{const interp}. Note that values are represented by variable indices (@{typ nat}) |
|
223 |
whose concrete values are given in list @{term vs}. |
|
59377 | 224 |
\<close> |
52287 | 225 |
|
59377 | 226 |
ML (*<*) \<open>\<close> |
52287 | 227 |
schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P" |
228 |
ML_prf |
|
59377 | 229 |
(*>*) \<open>val thm = |
230 |
Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*) |
|
231 |
by (tactic \<open>ALLGOALS (rtac thm)\<close>) |
|
52287 | 232 |
(*>*) |
233 |
||
59377 | 234 |
text \<open> |
52287 | 235 |
By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion |
236 |
which, for this concrete example, yields @{thm thm [no_vars]}. Note that the argument |
|
59335 | 237 |
to @{const interp} does not contain any free variables and can thus be evaluated |
52287 | 238 |
using evaluation. |
239 |
||
240 |
A less meager example can be found in the AFP, session @{text "Regular-Sets"}, |
|
241 |
theory @{text Regexp_Method}. |
|
59377 | 242 |
\<close> |
52287 | 243 |
|
244 |
||
59377 | 245 |
subsection \<open>Intimate connection between logic and system runtime\<close> |
39599 | 246 |
|
59377 | 247 |
text \<open> |
39609 | 248 |
The toolbox of static evaluation conversions forms a reasonable base |
249 |
to interweave generated code and system tools. However in some |
|
250 |
situations more direct interaction is desirable. |
|
59377 | 251 |
\<close> |
39599 | 252 |
|
253 |
||
59377 | 254 |
subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close> |
39599 | 255 |
|
59377 | 256 |
text \<open> |
39609 | 257 |
The @{text code} antiquotation allows to include constants from |
258 |
generated code directly into ML system code, as in the following toy |
|
259 |
example: |
|
59377 | 260 |
\<close> |
38510 | 261 |
|
58310 | 262 |
datatype %quote form = T | F | And form form | Or form form (*<*) |
38510 | 263 |
|
59377 | 264 |
(*>*) ML %quotett \<open> |
38510 | 265 |
fun eval_form @{code T} = true |
266 |
| eval_form @{code F} = false |
|
267 |
| eval_form (@{code And} (p, q)) = |
|
268 |
eval_form p andalso eval_form q |
|
269 |
| eval_form (@{code Or} (p, q)) = |
|
270 |
eval_form p orelse eval_form q; |
|
59377 | 271 |
\<close> |
38510 | 272 |
|
59377 | 273 |
text \<open> |
39609 | 274 |
\noindent @{text code} takes as argument the name of a constant; |
275 |
after the whole ML is read, the necessary code is generated |
|
276 |
transparently and the corresponding constant names are inserted. |
|
277 |
This technique also allows to use pattern matching on constructors |
|
39643 | 278 |
stemming from compiled datatypes. Note that the @{text code} |
279 |
antiquotation may not refer to constants which carry adaptations; |
|
280 |
here you have to refer to the corresponding adapted code directly. |
|
38510 | 281 |
|
39609 | 282 |
For a less simplistic example, theory @{text Approximation} in |
283 |
the @{text Decision_Procs} session is a good reference. |
|
59377 | 284 |
\<close> |
38510 | 285 |
|
286 |
||
59377 | 287 |
subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close> |
39599 | 288 |
|
59377 | 289 |
text \<open> |
39609 | 290 |
The @{text code} antiquoation is lightweight, but the generated code |
291 |
is only accessible while the ML section is processed. Sometimes this |
|
292 |
is not appropriate, especially if the generated code contains datatype |
|
293 |
declarations which are shared with other parts of the system. In these |
|
294 |
cases, @{command_def code_reflect} can be used: |
|
59377 | 295 |
\<close> |
39609 | 296 |
|
297 |
code_reflect %quote Sum_Type |
|
298 |
datatypes sum = Inl | Inr |
|
55418 | 299 |
functions "Sum_Type.sum.projl" "Sum_Type.sum.projr" |
39609 | 300 |
|
59377 | 301 |
text \<open> |
39609 | 302 |
\noindent @{command_def code_reflect} takes a structure name and |
303 |
references to datatypes and functions; for these code is compiled |
|
304 |
into the named ML structure and the \emph{Eval} target is modified |
|
305 |
in a way that future code generation will reference these |
|
306 |
precompiled versions of the given datatypes and functions. This |
|
307 |
also allows to refer to the referenced datatypes and functions from |
|
308 |
arbitrary ML code as well. |
|
309 |
||
310 |
A typical example for @{command code_reflect} can be found in the |
|
311 |
@{theory Predicate} theory. |
|
59377 | 312 |
\<close> |
39609 | 313 |
|
39599 | 314 |
|
59377 | 315 |
subsubsection \<open>Separate compilation -- @{text code_reflect}\<close> |
39599 | 316 |
|
59377 | 317 |
text \<open> |
39609 | 318 |
For technical reasons it is sometimes necessary to separate |
319 |
generation and compilation of code which is supposed to be used in |
|
320 |
the system runtime. For this @{command code_reflect} with an |
|
321 |
optional @{text "file"} argument can be used: |
|
59377 | 322 |
\<close> |
39609 | 323 |
|
324 |
code_reflect %quote Rat |
|
325 |
datatypes rat = Frct |
|
326 |
functions Fract |
|
327 |
"(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
|
328 |
"(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
|
59334 | 329 |
file "$ISABELLE_TMP/examples/rat.ML" |
39609 | 330 |
|
59377 | 331 |
text \<open> |
39643 | 332 |
\noindent This merely generates the referenced code to the given |
39609 | 333 |
file which can be included into the system runtime later on. |
59377 | 334 |
\<close> |
39599 | 335 |
|
38510 | 336 |
end |
46522 | 337 |