33 \item[Trustability.] Techniques which a huge (and also probably |
33 \item[Trustability.] Techniques which a huge (and also probably |
34 more configurable infrastructure) are more fragile and less |
34 more configurable infrastructure) are more fragile and less |
35 trustable. |
35 trustable. |
36 |
36 |
37 \end{description} |
37 \end{description} |
38 *} |
38 \<close> |
39 |
39 |
40 |
40 |
41 subsubsection {* The simplifier (@{text simp}) *} |
41 subsubsection \<open>The simplifier (@{text simp})\<close> |
42 |
42 |
43 text {* |
43 text \<open> |
44 The simplest way for evaluation is just using the simplifier with |
44 The simplest way for evaluation is just using the simplifier with |
45 the original code equations of the underlying program. This gives |
45 the original code equations of the underlying program. This gives |
46 fully symbolic evaluation and highest trustablity, with the usual |
46 fully symbolic evaluation and highest trustablity, with the usual |
47 performance of the simplifier. Note that for operations on abstract |
47 performance of the simplifier. Note that for operations on abstract |
48 datatypes (cf.~\secref{sec:invariant}), the original theorems as |
48 datatypes (cf.~\secref{sec:invariant}), the original theorems as |
49 given by the users are used, not the modified ones. |
49 given by the users are used, not the modified ones. |
50 *} |
50 \<close> |
51 |
51 |
52 |
52 |
53 subsubsection {* Normalization by evaluation (@{text nbe}) *} |
53 subsubsection \<open>Normalization by evaluation (@{text nbe})\<close> |
54 |
54 |
55 text {* |
55 text \<open> |
56 Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"} |
56 Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"} |
57 provides a comparably fast partially symbolic evaluation which |
57 provides a comparably fast partially symbolic evaluation which |
58 permits also normalization of functions and uninterpreted symbols; |
58 permits also normalization of functions and uninterpreted symbols; |
59 the stack of code to be trusted is considerable. |
59 the stack of code to be trusted is considerable. |
60 *} |
60 \<close> |
61 |
61 |
62 |
62 |
63 subsubsection {* Evaluation in ML (@{text code}) *} |
63 subsubsection \<open>Evaluation in ML (@{text code})\<close> |
64 |
64 |
65 text {* |
65 text \<open> |
66 Highest performance can be achieved by evaluation in ML, at the cost |
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 |
67 of being restricted to ground results and a layered stack of code to |
68 be trusted, including code generator configurations by the user. |
68 be trusted, including code generator configurations by the user. |
69 |
69 |
70 Evaluation is carried out in a target language \emph{Eval} which |
70 Evaluation is carried out in a target language \emph{Eval} which |
71 inherits from \emph{SML} but for convenience uses parts of the |
71 inherits from \emph{SML} but for convenience uses parts of the |
72 Isabelle runtime environment. The soundness of computation carried |
72 Isabelle runtime environment. The soundness of computation carried |
73 out there depends crucially on the correctness of the code |
73 out there depends crucially on the correctness of the code |
74 generator setup; this is one of the reasons why you should not use |
74 generator setup; this is one of the reasons why you should not use |
75 adaptation (see \secref{sec:adaptation}) frivolously. |
75 adaptation (see \secref{sec:adaptation}) frivolously. |
76 *} |
76 \<close> |
77 |
77 |
78 |
78 |
79 subsection {* Aspects of evaluation *} |
79 subsection \<open>Aspects of evaluation\<close> |
80 |
80 |
81 text {* |
81 text \<open> |
82 Each of the techniques can be combined with different aspects. The |
82 Each of the techniques can be combined with different aspects. The |
83 most important distinction is between dynamic and static evaluation. |
83 most important distinction is between dynamic and static evaluation. |
84 Dynamic evaluation takes the code generator configuration \qt{as it |
84 Dynamic evaluation takes the code generator configuration \qt{as it |
85 is} at the point where evaluation is issued. Best example is the |
85 is} at the point where evaluation is issued. Best example is the |
86 @{command_def value} command which allows ad-hoc evaluation of |
86 @{command_def value} command which allows ad-hoc evaluation of |
87 terms: |
87 terms: |
88 *} |
88 \<close> |
89 |
89 |
90 value %quote "42 / (12 :: rat)" |
90 value %quote "42 / (12 :: rat)" |
91 |
91 |
92 text {* |
92 text \<open> |
93 \noindent @{command value} tries first to evaluate using ML, falling |
93 \noindent @{command value} tries first to evaluate using ML, falling |
94 back to normalization by evaluation if this fails. |
94 back to normalization by evaluation if this fails. |
95 |
95 |
96 A particular technique may be specified in square brackets, e.g. |
96 A particular technique may be specified in square brackets, e.g. |
97 *} |
97 \<close> |
98 |
98 |
99 value %quote [nbe] "42 / (12 :: rat)" |
99 value %quote [nbe] "42 / (12 :: rat)" |
100 |
100 |
101 text {* |
101 text \<open> |
102 To employ dynamic evaluation in the document generation, there is also |
102 To employ dynamic evaluation in the document generation, there is also |
103 a @{text value} antiquotation with the same evaluation techniques |
103 a @{text value} antiquotation with the same evaluation techniques |
104 as @{command value}. |
104 as @{command value}. |
105 |
105 |
106 Static evaluation freezes the code generator configuration at a |
106 Static evaluation freezes the code generator configuration at a |
187 & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5} |
187 & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5} |
188 & conversion & \ttsize@{ML "Code_Simp.static_conv"} |
188 & conversion & \ttsize@{ML "Code_Simp.static_conv"} |
189 & \ttsize@{ML "Nbe.static_conv"} |
189 & \ttsize@{ML "Nbe.static_conv"} |
190 & \ttsize@{ML "Code_Evaluation.static_conv"} |
190 & \ttsize@{ML "Code_Evaluation.static_conv"} |
191 \end{tabular} |
191 \end{tabular} |
192 *} |
192 \<close> |
193 |
193 |
194 |
194 |
195 subsection {* Preprocessing HOL terms into evaluable shape *} |
195 subsection \<open>Preprocessing HOL terms into evaluable shape\<close> |
196 |
196 |
197 text {* |
197 text \<open> |
198 When integration decision procedures developed inside HOL into HOL itself, |
198 When integration decision procedures developed inside HOL into HOL itself, |
199 it is necessary to somehow get from the Isabelle/ML representation to |
199 it is necessary to somehow get from the Isabelle/ML representation to |
200 the representation used by the decision procedure itself (``reification''). |
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}). |
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: |
202 Another option is to use pre-existing infrastructure in HOL: |
203 @{ML "Reification.conv"} and @{ML "Reification.tac"} |
203 @{ML "Reification.conv"} and @{ML "Reification.tac"} |
204 |
204 |
205 An simplistic example: |
205 An simplistic example: |
206 *} |
206 \<close> |
207 |
207 |
208 datatype %quote form_ord = T | F | Less nat nat |
208 datatype %quote form_ord = T | F | Less nat nat |
209 | And form_ord form_ord | Or form_ord form_ord | Neg form_ord |
209 | And form_ord form_ord | Or form_ord form_ord | Neg form_ord |
210 |
210 |
211 primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool" |
211 primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool" |
215 | "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j" |
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" |
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" |
217 | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs" |
218 | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs" |
218 | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs" |
219 |
219 |
220 text {* |
220 text \<open> |
221 The datatype @{type form_ord} represents formulae whose semantics is given by |
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}) |
222 @{const interp}. Note that values are represented by variable indices (@{typ nat}) |
223 whose concrete values are given in list @{term vs}. |
223 whose concrete values are given in list @{term vs}. |
224 *} |
224 \<close> |
225 |
225 |
226 ML (*<*) {* *} |
226 ML (*<*) \<open>\<close> |
227 schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P" |
227 schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P" |
228 ML_prf |
228 ML_prf |
229 (*>*) {* val thm = |
229 (*>*) \<open>val thm = |
230 Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"} *} (*<*) |
230 Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*) |
231 by (tactic {* ALLGOALS (rtac thm) *}) |
231 by (tactic \<open>ALLGOALS (rtac thm)\<close>) |
232 (*>*) |
232 (*>*) |
233 |
233 |
234 text {* |
234 text \<open> |
235 By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion |
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 |
236 which, for this concrete example, yields @{thm thm [no_vars]}. Note that the argument |
237 to @{const interp} does not contain any free variables and can thus be evaluated |
237 to @{const interp} does not contain any free variables and can thus be evaluated |
238 using evaluation. |
238 using evaluation. |
239 |
239 |
240 A less meager example can be found in the AFP, session @{text "Regular-Sets"}, |
240 A less meager example can be found in the AFP, session @{text "Regular-Sets"}, |
241 theory @{text Regexp_Method}. |
241 theory @{text Regexp_Method}. |
242 *} |
242 \<close> |
243 |
243 |
244 |
244 |
245 subsection {* Intimate connection between logic and system runtime *} |
245 subsection \<open>Intimate connection between logic and system runtime\<close> |
246 |
246 |
247 text {* |
247 text \<open> |
248 The toolbox of static evaluation conversions forms a reasonable base |
248 The toolbox of static evaluation conversions forms a reasonable base |
249 to interweave generated code and system tools. However in some |
249 to interweave generated code and system tools. However in some |
250 situations more direct interaction is desirable. |
250 situations more direct interaction is desirable. |
251 *} |
251 \<close> |
252 |
252 |
253 |
253 |
254 subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq} *} |
254 subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close> |
255 |
255 |
256 text {* |
256 text \<open> |
257 The @{text code} antiquotation allows to include constants from |
257 The @{text code} antiquotation allows to include constants from |
258 generated code directly into ML system code, as in the following toy |
258 generated code directly into ML system code, as in the following toy |
259 example: |
259 example: |
260 *} |
260 \<close> |
261 |
261 |
262 datatype %quote form = T | F | And form form | Or form form (*<*) |
262 datatype %quote form = T | F | And form form | Or form form (*<*) |
263 |
263 |
264 (*>*) ML %quotett {* |
264 (*>*) ML %quotett \<open> |
265 fun eval_form @{code T} = true |
265 fun eval_form @{code T} = true |
266 | eval_form @{code F} = false |
266 | eval_form @{code F} = false |
267 | eval_form (@{code And} (p, q)) = |
267 | eval_form (@{code And} (p, q)) = |
268 eval_form p andalso eval_form q |
268 eval_form p andalso eval_form q |
269 | eval_form (@{code Or} (p, q)) = |
269 | eval_form (@{code Or} (p, q)) = |
270 eval_form p orelse eval_form q; |
270 eval_form p orelse eval_form q; |
271 *} |
271 \<close> |
272 |
272 |
273 text {* |
273 text \<open> |
274 \noindent @{text code} takes as argument the name of a constant; |
274 \noindent @{text code} takes as argument the name of a constant; |
275 after the whole ML is read, the necessary code is generated |
275 after the whole ML is read, the necessary code is generated |
276 transparently and the corresponding constant names are inserted. |
276 transparently and the corresponding constant names are inserted. |
277 This technique also allows to use pattern matching on constructors |
277 This technique also allows to use pattern matching on constructors |
278 stemming from compiled datatypes. Note that the @{text code} |
278 stemming from compiled datatypes. Note that the @{text code} |
279 antiquotation may not refer to constants which carry adaptations; |
279 antiquotation may not refer to constants which carry adaptations; |
280 here you have to refer to the corresponding adapted code directly. |
280 here you have to refer to the corresponding adapted code directly. |
281 |
281 |
282 For a less simplistic example, theory @{text Approximation} in |
282 For a less simplistic example, theory @{text Approximation} in |
283 the @{text Decision_Procs} session is a good reference. |
283 the @{text Decision_Procs} session is a good reference. |
284 *} |
284 \<close> |
285 |
285 |
286 |
286 |
287 subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *} |
287 subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close> |
288 |
288 |
289 text {* |
289 text \<open> |
290 The @{text code} antiquoation is lightweight, but the generated code |
290 The @{text code} antiquoation is lightweight, but the generated code |
291 is only accessible while the ML section is processed. Sometimes this |
291 is only accessible while the ML section is processed. Sometimes this |
292 is not appropriate, especially if the generated code contains datatype |
292 is not appropriate, especially if the generated code contains datatype |
293 declarations which are shared with other parts of the system. In these |
293 declarations which are shared with other parts of the system. In these |
294 cases, @{command_def code_reflect} can be used: |
294 cases, @{command_def code_reflect} can be used: |
295 *} |
295 \<close> |
296 |
296 |
297 code_reflect %quote Sum_Type |
297 code_reflect %quote Sum_Type |
298 datatypes sum = Inl | Inr |
298 datatypes sum = Inl | Inr |
299 functions "Sum_Type.sum.projl" "Sum_Type.sum.projr" |
299 functions "Sum_Type.sum.projl" "Sum_Type.sum.projr" |
300 |
300 |
301 text {* |
301 text \<open> |
302 \noindent @{command_def code_reflect} takes a structure name and |
302 \noindent @{command_def code_reflect} takes a structure name and |
303 references to datatypes and functions; for these code is compiled |
303 references to datatypes and functions; for these code is compiled |
304 into the named ML structure and the \emph{Eval} target is modified |
304 into the named ML structure and the \emph{Eval} target is modified |
305 in a way that future code generation will reference these |
305 in a way that future code generation will reference these |
306 precompiled versions of the given datatypes and functions. This |
306 precompiled versions of the given datatypes and functions. This |
307 also allows to refer to the referenced datatypes and functions from |
307 also allows to refer to the referenced datatypes and functions from |
308 arbitrary ML code as well. |
308 arbitrary ML code as well. |
309 |
309 |
310 A typical example for @{command code_reflect} can be found in the |
310 A typical example for @{command code_reflect} can be found in the |
311 @{theory Predicate} theory. |
311 @{theory Predicate} theory. |
312 *} |
312 \<close> |
313 |
313 |
314 |
314 |
315 subsubsection {* Separate compilation -- @{text code_reflect} *} |
315 subsubsection \<open>Separate compilation -- @{text code_reflect}\<close> |
316 |
316 |
317 text {* |
317 text \<open> |
318 For technical reasons it is sometimes necessary to separate |
318 For technical reasons it is sometimes necessary to separate |
319 generation and compilation of code which is supposed to be used in |
319 generation and compilation of code which is supposed to be used in |
320 the system runtime. For this @{command code_reflect} with an |
320 the system runtime. For this @{command code_reflect} with an |
321 optional @{text "file"} argument can be used: |
321 optional @{text "file"} argument can be used: |
322 *} |
322 \<close> |
323 |
323 |
324 code_reflect %quote Rat |
324 code_reflect %quote Rat |
325 datatypes rat = Frct |
325 datatypes rat = Frct |
326 functions Fract |
326 functions Fract |
327 "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
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)" |
328 "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
329 file "$ISABELLE_TMP/examples/rat.ML" |
329 file "$ISABELLE_TMP/examples/rat.ML" |
330 |
330 |
331 text {* |
331 text \<open> |
332 \noindent This merely generates the referenced code to the given |
332 \noindent This merely generates the referenced code to the given |
333 file which can be included into the system runtime later on. |
333 file which can be included into the system runtime later on. |
334 *} |
334 \<close> |
335 |
335 |
336 end |
336 end |
337 |
337 |