src/Doc/Codegen/Evaluation.thy
changeset 63161 2660ba498798
parent 61337 4645502c3c64
child 63175 d191892b1c23
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4      \item Evaluation of @{term t} terminates with a result @{term
     1.5        "t'"}.
     1.6  
     1.7 -    \item Evaluation of @{term t} terminates which en exception
     1.8 +    \item Evaluation of @{term t} terminates which an exception
     1.9        indicating a pattern match failure or a non-implemented
    1.10        function.  As sketched in \secref{sec:partiality}, this can be
    1.11        interpreted as partiality.
    1.12 @@ -195,18 +195,36 @@
    1.13    \end{tabular}
    1.14  \<close>
    1.15  
    1.16 +text \<open>
    1.17 +  \noindent Note that @{ML Code_Evaluation.static_value} and
    1.18 +  @{ML Code_Evaluation.static_conv} require certain code equations to
    1.19 +  reconstruct Isabelle terms from results and certify results.  This is
    1.20 +  achieved as follows:
    1.21 +
    1.22 +  \<^enum> Identify which result types are expected.
    1.23 +
    1.24 +  \<^enum> Define an auxiliary operation which for each possible result type @{text \<tau>}
    1.25 +    contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\<tau> itself"}
    1.26 +    (for @{ML Code_Evaluation.static_value}) or
    1.27 +    a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\<tau> itself"}
    1.28 +    (for @{ML Code_Evaluation.static_conv}) respectively.
    1.29 +
    1.30 +  \<^enum> Include that auxiliary operation into the set of constants when generating
    1.31 +    the static conversion.
    1.32 +\<close>
    1.33 +
    1.34  
    1.35  subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
    1.36  
    1.37  text \<open>
    1.38 -  When integration decision procedures developed inside HOL into HOL itself,
    1.39 +  When integrating decision procedures developed inside HOL into HOL itself,
    1.40    it is necessary to somehow get from the Isabelle/ML representation to
    1.41    the representation used by the decision procedure itself (``reification'').
    1.42    One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
    1.43    Another option is to use pre-existing infrastructure in HOL:
    1.44    @{ML "Reification.conv"} and @{ML "Reification.tac"}
    1.45  
    1.46 -  An simplistic example:
    1.47 +  A simplistic example:
    1.48  \<close>
    1.49  
    1.50  datatype %quote form_ord = T | F | Less nat nat