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