172 \item[Property conversion.] Evaluates propositions; since these |
172 \item[Property conversion.] Evaluates propositions; since these |
173 are monomorphic, the term reconstruction is fixed once and for all |
173 are monomorphic, the term reconstruction is fixed once and for all |
174 and therefore trustable. |
174 and therefore trustable. |
175 |
175 |
176 \item[Conversion.] Evaluates an arbitrary term \isa{t} first |
176 \item[Conversion.] Evaluates an arbitrary term \isa{t} first |
177 by plain evaluation and certifies the result \isa{t{\isacharprime}} by |
177 by plain evaluation and certifies the result \isa{t{\isaliteral{27}{\isacharprime}}} by |
178 checking the equation \isa{t\ {\isasymequiv}\ t{\isacharprime}} using property |
178 checking the equation \isa{t\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{27}{\isacharprime}}} using property |
179 conversion. |
179 conversion. |
180 |
180 |
181 \end{description} |
181 \end{description} |
182 |
182 |
183 \noindent The picture is further complicated by the roles of |
183 \noindent The picture is further complicated by the roles of |
184 exceptions. Here three cases have to be distinguished: |
184 exceptions. Here three cases have to be distinguished: |
185 |
185 |
186 \begin{itemize} |
186 \begin{itemize} |
187 |
187 |
188 \item Evaluation of \isa{t} terminates with a result \isa{t{\isacharprime}}. |
188 \item Evaluation of \isa{t} terminates with a result \isa{t{\isaliteral{27}{\isacharprime}}}. |
189 |
189 |
190 \item Evaluation of \isa{t} terminates which en exception |
190 \item Evaluation of \isa{t} terminates which en exception |
191 indicating a pattern match failure or a non-implemented |
191 indicating a pattern match failure or a non-implemented |
192 function. As sketched in \secref{sec:partiality}, this can be |
192 function. As sketched in \secref{sec:partiality}, this can be |
193 interpreted as partiality. |
193 interpreted as partiality. |
194 |
194 |
195 \item Evaluation raises any other kind of exception. |
195 \item Evaluation raises any other kind of exception. |
196 |
196 |
197 \end{itemize} |
197 \end{itemize} |
198 |
198 |
199 \noindent For conversions, the first case yields the equation \isa{t\ {\isacharequal}\ t{\isacharprime}}, the second defaults to reflexivity \isa{t\ {\isacharequal}\ t}. |
199 \noindent For conversions, the first case yields the equation \isa{t\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{27}{\isacharprime}}}, the second defaults to reflexivity \isa{t\ {\isaliteral{3D}{\isacharequal}}\ t}. |
200 Exceptions of the third kind are propagated to the user. |
200 Exceptions of the third kind are propagated to the user. |
201 |
201 |
202 By default return values of plain evaluation are optional, yielding |
202 By default return values of plain evaluation are optional, yielding |
203 \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} in the |
203 \isa{SOME\ t{\isaliteral{27}{\isacharprime}}} in the first case, \isa{NONE} in the |
204 second, and propagating the exception in the third case. A strict |
204 second, and propagating the exception in the third case. A strict |
205 variant of plain evaluation either yields \isa{t{\isacharprime}} or propagates |
205 variant of plain evaluation either yields \isa{t{\isaliteral{27}{\isacharprime}}} or propagates |
206 any exception, a liberal variant caputures any exception in a result |
206 any exception, a liberal variant caputures any exception in a result |
207 of type \isa{Exn{\isachardot}result}. |
207 of type \isa{Exn{\isaliteral{2E}{\isachardot}}result}. |
208 |
208 |
209 For property conversion (which coincides with conversion except for |
209 For property conversion (which coincides with conversion except for |
210 evaluation in ML), methods are provided which solve a given goal by |
210 evaluation in ML), methods are provided which solve a given goal by |
211 evaluation.% |
211 evaluation.% |
212 \end{isamarkuptext}% |
212 \end{isamarkuptext}% |
221 \fontsize{9pt}{12pt}\selectfont |
221 \fontsize{9pt}{12pt}\selectfont |
222 \begin{tabular}{ll||c|c|c} |
222 \begin{tabular}{ll||c|c|c} |
223 & & \isa{simp} & \isa{nbe} & \isa{code} \tabularnewline \hline \hline |
223 & & \isa{simp} & \isa{nbe} & \isa{code} \tabularnewline \hline \hline |
224 \multirow{5}{1ex}{\rotatebox{90}{dynamic}} |
224 \multirow{5}{1ex}{\rotatebox{90}{dynamic}} |
225 & interactive evaluation |
225 & interactive evaluation |
226 & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}simp{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}nbe{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}code{\isacharbrackright}} |
226 & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isaliteral{5B}{\isacharbrackleft}}nbe{\isaliteral{5D}{\isacharbrackright}}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}} |
227 \tabularnewline |
227 \tabularnewline |
228 & plain evaluation & & & \ttsize\verb|Code_Evaluation.dynamic_value| \tabularnewline \cline{2-5} |
228 & plain evaluation & & & \ttsize\verb|Code_Evaluation.dynamic_value| \tabularnewline \cline{2-5} |
229 & evaluation method & \hyperlink{method.code-simp}{\mbox{\isa{code{\isacharunderscore}simp}}} & \hyperlink{method.normalization}{\mbox{\isa{normalization}}} & \hyperlink{method.eval}{\mbox{\isa{eval}}} \tabularnewline |
229 & evaluation method & \hyperlink{method.code-simp}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}simp}}} & \hyperlink{method.normalization}{\mbox{\isa{normalization}}} & \hyperlink{method.eval}{\mbox{\isa{eval}}} \tabularnewline |
230 & property conversion & & & \ttsize\verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \cline{2-5} |
230 & property conversion & & & \ttsize\verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \cline{2-5} |
231 & conversion & \ttsize\verb|Code_Simp.dynamic_eval_conv| & \ttsize\verb|Nbe.dynamic_eval_conv| |
231 & conversion & \ttsize\verb|Code_Simp.dynamic_eval_conv| & \ttsize\verb|Nbe.dynamic_eval_conv| |
232 & \ttsize\verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline |
232 & \ttsize\verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline |
233 \multirow{3}{1ex}{\rotatebox{90}{static}} |
233 \multirow{3}{1ex}{\rotatebox{90}{static}} |
234 & plain evaluation & & & \ttsize\verb|Code_Evaluation.static_value| \tabularnewline \cline{2-5} |
234 & plain evaluation & & & \ttsize\verb|Code_Evaluation.static_value| \tabularnewline \cline{2-5} |
281 \ % |
281 \ % |
282 \endisadelimquotett |
282 \endisadelimquotett |
283 % |
283 % |
284 \isatagquotett |
284 \isatagquotett |
285 \isacommand{ML}\isamarkupfalse% |
285 \isacommand{ML}\isamarkupfalse% |
286 \ {\isacharverbatimopen}\isanewline |
286 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
287 \ \ fun\ eval{\isacharunderscore}form\ % |
287 \ \ fun\ eval{\isaliteral{5F}{\isacharunderscore}}form\ % |
288 \isaantiq |
288 \isaantiq |
289 code\ T% |
289 code\ T{}% |
290 \endisaantiq |
290 \endisaantiq |
291 \ {\isacharequal}\ true\isanewline |
291 \ {\isaliteral{3D}{\isacharequal}}\ true\isanewline |
292 \ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ % |
292 \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}form\ % |
293 \isaantiq |
293 \isaantiq |
294 code\ F% |
294 code\ F{}% |
295 \endisaantiq |
295 \endisaantiq |
296 \ {\isacharequal}\ false\isanewline |
296 \ {\isaliteral{3D}{\isacharequal}}\ false\isanewline |
297 \ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}% |
297 \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}form\ {\isaliteral{28}{\isacharparenleft}}% |
298 \isaantiq |
298 \isaantiq |
299 code\ And% |
299 code\ And{}% |
300 \endisaantiq |
300 \endisaantiq |
301 \ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
301 \ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}\ q{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
302 \ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ andalso\ eval{\isacharunderscore}form\ q\isanewline |
302 \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}form\ p\ andalso\ eval{\isaliteral{5F}{\isacharunderscore}}form\ q\isanewline |
303 \ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}% |
303 \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}form\ {\isaliteral{28}{\isacharparenleft}}% |
304 \isaantiq |
304 \isaantiq |
305 code\ Or% |
305 code\ Or{}% |
306 \endisaantiq |
306 \endisaantiq |
307 \ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
307 \ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}\ q{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
308 \ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline |
308 \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}form\ p\ orelse\ eval{\isaliteral{5F}{\isacharunderscore}}form\ q{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
309 {\isacharverbatimclose}% |
309 {\isaliteral{2A7D}{\isacharverbatimclose}}% |
310 \endisatagquotett |
310 \endisatagquotett |
311 {\isafoldquotett}% |
311 {\isafoldquotett}% |
312 % |
312 % |
313 \isadelimquotett |
313 \isadelimquotett |
314 % |
314 % |
322 stemming from compiled datatypes. Note that the \isa{code} |
322 stemming from compiled datatypes. Note that the \isa{code} |
323 antiquotation may not refer to constants which carry adaptations; |
323 antiquotation may not refer to constants which carry adaptations; |
324 here you have to refer to the corresponding adapted code directly. |
324 here you have to refer to the corresponding adapted code directly. |
325 |
325 |
326 For a less simplistic example, theory \isa{Approximation} in |
326 For a less simplistic example, theory \isa{Approximation} in |
327 the \isa{Decision{\isacharunderscore}Procs} session is a good reference.% |
327 the \isa{Decision{\isaliteral{5F}{\isacharunderscore}}Procs} session is a good reference.% |
328 \end{isamarkuptext}% |
328 \end{isamarkuptext}% |
329 \isamarkuptrue% |
329 \isamarkuptrue% |
330 % |
330 % |
331 \isamarkupsubsubsection{Static embedding of generated code into system runtime -- \isa{code{\isacharunderscore}reflect}% |
331 \isamarkupsubsubsection{Static embedding of generated code into system runtime -- \isa{code{\isaliteral{5F}{\isacharunderscore}}reflect}% |
332 } |
332 } |
333 \isamarkuptrue% |
333 \isamarkuptrue% |
334 % |
334 % |
335 \begin{isamarkuptext}% |
335 \begin{isamarkuptext}% |
336 The \isa{code} antiquoation is lightweight, but the generated code |
336 The \isa{code} antiquoation is lightweight, but the generated code |
337 is only accessible while the ML section is processed. Sometimes this |
337 is only accessible while the ML section is processed. Sometimes this |
338 is not appropriate, especially if the generated code contains datatype |
338 is not appropriate, especially if the generated code contains datatype |
339 declarations which are shared with other parts of the system. In these |
339 declarations which are shared with other parts of the system. In these |
340 cases, \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} can be used:% |
340 cases, \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}} can be used:% |
341 \end{isamarkuptext}% |
341 \end{isamarkuptext}% |
342 \isamarkuptrue% |
342 \isamarkuptrue% |
343 % |
343 % |
344 \isadelimquote |
344 \isadelimquote |
345 % |
345 % |
346 \endisadelimquote |
346 \endisadelimquote |
347 % |
347 % |
348 \isatagquote |
348 \isatagquote |
349 \isacommand{code{\isacharunderscore}reflect}\isamarkupfalse% |
349 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}\isamarkupfalse% |
350 \ Sum{\isacharunderscore}Type\isanewline |
350 \ Sum{\isaliteral{5F}{\isacharunderscore}}Type\isanewline |
351 \ \ \isakeyword{datatypes}\ sum\ {\isacharequal}\ Inl\ {\isacharbar}\ Inr\isanewline |
351 \ \ \isakeyword{datatypes}\ sum\ {\isaliteral{3D}{\isacharequal}}\ Inl\ {\isaliteral{7C}{\isacharbar}}\ Inr\isanewline |
352 \ \ \isakeyword{functions}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projl{\isachardoublequoteclose}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projr{\isachardoublequoteclose}% |
352 \ \ \isakeyword{functions}\ {\isaliteral{22}{\isachardoublequoteopen}}Sum{\isaliteral{5F}{\isacharunderscore}}Type{\isaliteral{2E}{\isachardot}}Projl{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}Sum{\isaliteral{5F}{\isacharunderscore}}Type{\isaliteral{2E}{\isachardot}}Projr{\isaliteral{22}{\isachardoublequoteclose}}% |
353 \endisatagquote |
353 \endisatagquote |
354 {\isafoldquote}% |
354 {\isafoldquote}% |
355 % |
355 % |
356 \isadelimquote |
356 \isadelimquote |
357 % |
357 % |
358 \endisadelimquote |
358 \endisadelimquote |
359 % |
359 % |
360 \begin{isamarkuptext}% |
360 \begin{isamarkuptext}% |
361 \noindent \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} takes a structure name and |
361 \noindent \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}} takes a structure name and |
362 references to datatypes and functions; for these code is compiled |
362 references to datatypes and functions; for these code is compiled |
363 into the named ML structure and the \emph{Eval} target is modified |
363 into the named ML structure and the \emph{Eval} target is modified |
364 in a way that future code generation will reference these |
364 in a way that future code generation will reference these |
365 precompiled versions of the given datatypes and functions. This |
365 precompiled versions of the given datatypes and functions. This |
366 also allows to refer to the referenced datatypes and functions from |
366 also allows to refer to the referenced datatypes and functions from |
367 arbitrary ML code as well. |
367 arbitrary ML code as well. |
368 |
368 |
369 A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} can be found in the |
369 A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} can be found in the |
370 \hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.% |
370 \hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.% |
371 \end{isamarkuptext}% |
371 \end{isamarkuptext}% |
372 \isamarkuptrue% |
372 \isamarkuptrue% |
373 % |
373 % |
374 \isamarkupsubsubsection{Separate compilation -- \isa{code{\isacharunderscore}reflect}% |
374 \isamarkupsubsubsection{Separate compilation -- \isa{code{\isaliteral{5F}{\isacharunderscore}}reflect}% |
375 } |
375 } |
376 \isamarkuptrue% |
376 \isamarkuptrue% |
377 % |
377 % |
378 \begin{isamarkuptext}% |
378 \begin{isamarkuptext}% |
379 For technical reasons it is sometimes necessary to separate |
379 For technical reasons it is sometimes necessary to separate |
380 generation and compilation of code which is supposed to be used in |
380 generation and compilation of code which is supposed to be used in |
381 the system runtime. For this \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} with an |
381 the system runtime. For this \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} with an |
382 optional \isa{file} argument can be used:% |
382 optional \isa{file} argument can be used:% |
383 \end{isamarkuptext}% |
383 \end{isamarkuptext}% |
384 \isamarkuptrue% |
384 \isamarkuptrue% |
385 % |
385 % |
386 \isadelimquote |
386 \isadelimquote |
387 % |
387 % |
388 \endisadelimquote |
388 \endisadelimquote |
389 % |
389 % |
390 \isatagquote |
390 \isatagquote |
391 \isacommand{code{\isacharunderscore}reflect}\isamarkupfalse% |
391 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}\isamarkupfalse% |
392 \ Rat\isanewline |
392 \ Rat\isanewline |
393 \ \ \isakeyword{datatypes}\ rat\ {\isacharequal}\ Frct\isanewline |
393 \ \ \isakeyword{datatypes}\ rat\ {\isaliteral{3D}{\isacharequal}}\ Frct\isanewline |
394 \ \ \isakeyword{functions}\ Fract\isanewline |
394 \ \ \isakeyword{functions}\ Fract\isanewline |
395 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}plus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}minus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
395 \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}plus\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ rat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ rat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ rat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}minus\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ rat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ rat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ rat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
396 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}times\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}divide\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
396 \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}times\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ rat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ rat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ rat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}divide\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ rat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ rat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ rat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
397 \ \ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}rat{\isachardot}ML{\isachardoublequoteclose}% |
397 \ \ \isakeyword{file}\ {\isaliteral{22}{\isachardoublequoteopen}}examples{\isaliteral{2F}{\isacharslash}}rat{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}% |
398 \endisatagquote |
398 \endisatagquote |
399 {\isafoldquote}% |
399 {\isafoldquote}% |
400 % |
400 % |
401 \isadelimquote |
401 \isadelimquote |
402 % |
402 % |