38510
|
1 |
theory Evaluation
|
|
2 |
imports Setup
|
|
3 |
begin
|
|
4 |
|
|
5 |
section {* Evaluation *}
|
|
6 |
|
|
7 |
text {* Introduction *}
|
|
8 |
|
|
9 |
|
|
10 |
subsection {* Evaluation techniques *}
|
|
11 |
|
|
12 |
text {* simplifier *}
|
|
13 |
|
|
14 |
text {* nbe *}
|
|
15 |
|
|
16 |
text {* eval target: SML standalone vs. Isabelle/SML, example, soundness *}
|
|
17 |
|
|
18 |
|
|
19 |
subsection {* Dynamic evaluation *}
|
|
20 |
|
|
21 |
text {* value (three variants) *}
|
|
22 |
|
|
23 |
text {* methods (three variants) *}
|
|
24 |
|
|
25 |
text {* corresponding ML interfaces *}
|
|
26 |
|
|
27 |
|
|
28 |
subsection {* Static evaluation *}
|
|
29 |
|
|
30 |
text {* code_simp, nbe (tbd), Eval (tbd, in simple fashion) *}
|
|
31 |
|
|
32 |
text {* hand-written: code antiquotation *}
|
|
33 |
|
|
34 |
|
|
35 |
subsection {* Hybrid techniques *}
|
|
36 |
|
|
37 |
text {* code reflect runtime *}
|
|
38 |
|
|
39 |
text {* code reflect external *}
|
|
40 |
|
|
41 |
|
|
42 |
text {* FIXME here the old sections follow *}
|
|
43 |
|
|
44 |
subsection {* Evaluation oracle *}
|
|
45 |
|
|
46 |
text {*
|
|
47 |
Code generation may also be used to \emph{evaluate} expressions
|
|
48 |
(using @{text SML} as target language of course).
|
|
49 |
For instance, the @{command_def value} reduces an expression to a
|
|
50 |
normal form with respect to the underlying code equations:
|
|
51 |
*}
|
|
52 |
|
|
53 |
value %quote "42 / (12 :: rat)"
|
|
54 |
|
|
55 |
text {*
|
|
56 |
\noindent will display @{term "7 / (2 :: rat)"}.
|
|
57 |
|
|
58 |
The @{method eval} method tries to reduce a goal by code generation to @{term True}
|
|
59 |
and solves it in that case, but fails otherwise:
|
|
60 |
*}
|
|
61 |
|
|
62 |
lemma %quote "42 / (12 :: rat) = 7 / 2"
|
|
63 |
by %quote eval
|
|
64 |
|
|
65 |
text {*
|
|
66 |
\noindent The soundness of the @{method eval} method depends crucially
|
|
67 |
on the correctness of the code generator; this is one of the reasons
|
|
68 |
why you should not use adaptation (see \secref{sec:adaptation}) frivolously.
|
|
69 |
*}
|
|
70 |
|
|
71 |
|
|
72 |
subsubsection {* Code antiquotation *}
|
|
73 |
|
|
74 |
text {*
|
|
75 |
In scenarios involving techniques like reflection it is quite common
|
|
76 |
that code generated from a theory forms the basis for implementing
|
|
77 |
a proof procedure in @{text SML}. To facilitate interfacing of generated code
|
|
78 |
with system code, the code generator provides a @{text code} antiquotation:
|
|
79 |
*}
|
|
80 |
|
|
81 |
datatype %quote form = T | F | And form form | Or form form (*<*)
|
|
82 |
|
|
83 |
(*>*) ML %quotett {*
|
|
84 |
fun eval_form @{code T} = true
|
|
85 |
| eval_form @{code F} = false
|
|
86 |
| eval_form (@{code And} (p, q)) =
|
|
87 |
eval_form p andalso eval_form q
|
|
88 |
| eval_form (@{code Or} (p, q)) =
|
|
89 |
eval_form p orelse eval_form q;
|
|
90 |
*}
|
|
91 |
|
|
92 |
text {*
|
|
93 |
\noindent @{text code} takes as argument the name of a constant; after the
|
|
94 |
whole @{text SML} is read, the necessary code is generated transparently
|
|
95 |
and the corresponding constant names are inserted. This technique also
|
|
96 |
allows to use pattern matching on constructors stemming from compiled
|
|
97 |
@{text "datatypes"}.
|
|
98 |
|
39067
|
99 |
For a less simplistic example, theory @{text Ferrack} is
|
38510
|
100 |
a good reference.
|
|
101 |
*}
|
|
102 |
|
|
103 |
|
|
104 |
end
|