src/Doc/Codegen/Evaluation.thy
changeset 59377 056945909f60
parent 59335 e743ce816cf6
child 59378 065f349852e6
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu Jan 15 13:39:41 2015 +0100
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Thu Jan 15 13:39:41 2015 +0100
     1.3 @@ -2,9 +2,9 @@
     1.4  imports Setup
     1.5  begin
     1.6  
     1.7 -section {* Evaluation \label{sec:evaluation} *}
     1.8 +section \<open>Evaluation \label{sec:evaluation}\<close>
     1.9  
    1.10 -text {*
    1.11 +text \<open>
    1.12    Recalling \secref{sec:principle}, code generation turns a system of
    1.13    equations into a program with the \emph{same} equational semantics.
    1.14    As a consequence, this program can be used as a \emph{rewrite
    1.15 @@ -12,12 +12,12 @@
    1.16    term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}.  This
    1.17    application of code generation in the following is referred to as
    1.18    \emph{evaluation}.
    1.19 -*}
    1.20 +\<close>
    1.21  
    1.22  
    1.23 -subsection {* Evaluation techniques *}
    1.24 +subsection \<open>Evaluation techniques\<close>
    1.25  
    1.26 -text {*
    1.27 +text \<open>
    1.28    The existing infrastructure provides a rich palette of evaluation
    1.29    techniques, each comprising different aspects:
    1.30  
    1.31 @@ -35,34 +35,34 @@
    1.32        trustable.
    1.33  
    1.34    \end{description}
    1.35 -*}
    1.36 +\<close>
    1.37  
    1.38  
    1.39 -subsubsection {* The simplifier (@{text simp}) *}
    1.40 +subsubsection \<open>The simplifier (@{text simp})\<close>
    1.41  
    1.42 -text {*
    1.43 +text \<open>
    1.44    The simplest way for evaluation is just using the simplifier with
    1.45    the original code equations of the underlying program.  This gives
    1.46    fully symbolic evaluation and highest trustablity, with the usual
    1.47    performance of the simplifier.  Note that for operations on abstract
    1.48    datatypes (cf.~\secref{sec:invariant}), the original theorems as
    1.49    given by the users are used, not the modified ones.
    1.50 -*}
    1.51 +\<close>
    1.52  
    1.53  
    1.54 -subsubsection {* Normalization by evaluation (@{text nbe}) *}
    1.55 +subsubsection \<open>Normalization by evaluation (@{text nbe})\<close>
    1.56  
    1.57 -text {*
    1.58 +text \<open>
    1.59    Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
    1.60    provides a comparably fast partially symbolic evaluation which
    1.61    permits also normalization of functions and uninterpreted symbols;
    1.62    the stack of code to be trusted is considerable.
    1.63 -*}
    1.64 +\<close>
    1.65  
    1.66  
    1.67 -subsubsection {* Evaluation in ML (@{text code}) *}
    1.68 +subsubsection \<open>Evaluation in ML (@{text code})\<close>
    1.69  
    1.70 -text {*
    1.71 +text \<open>
    1.72    Highest performance can be achieved by evaluation in ML, at the cost
    1.73    of being restricted to ground results and a layered stack of code to
    1.74    be trusted, including code generator configurations by the user.
    1.75 @@ -73,32 +73,32 @@
    1.76    out there depends crucially on the correctness of the code
    1.77    generator setup; this is one of the reasons why you should not use
    1.78    adaptation (see \secref{sec:adaptation}) frivolously.
    1.79 -*}
    1.80 +\<close>
    1.81  
    1.82  
    1.83 -subsection {* Aspects of evaluation *}
    1.84 +subsection \<open>Aspects of evaluation\<close>
    1.85  
    1.86 -text {*
    1.87 +text \<open>
    1.88    Each of the techniques can be combined with different aspects.  The
    1.89    most important distinction is between dynamic and static evaluation.
    1.90    Dynamic evaluation takes the code generator configuration \qt{as it
    1.91    is} at the point where evaluation is issued.  Best example is the
    1.92    @{command_def value} command which allows ad-hoc evaluation of
    1.93    terms:
    1.94 -*}
    1.95 +\<close>
    1.96  
    1.97  value %quote "42 / (12 :: rat)"
    1.98  
    1.99 -text {*
   1.100 +text \<open>
   1.101    \noindent @{command value} tries first to evaluate using ML, falling
   1.102    back to normalization by evaluation if this fails.
   1.103  
   1.104    A particular technique may be specified in square brackets, e.g.
   1.105 -*}
   1.106 +\<close>
   1.107  
   1.108  value %quote [nbe] "42 / (12 :: rat)"
   1.109  
   1.110 -text {*
   1.111 +text \<open>
   1.112    To employ dynamic evaluation in the document generation, there is also
   1.113    a @{text value} antiquotation with the same evaluation techniques 
   1.114    as @{command value}.
   1.115 @@ -162,12 +162,12 @@
   1.116    For property conversion (which coincides with conversion except for
   1.117    evaluation in ML), methods are provided which solve a given goal by
   1.118    evaluation.
   1.119 -*}
   1.120 +\<close>
   1.121  
   1.122  
   1.123 -subsection {* Schematic overview *}
   1.124 +subsection \<open>Schematic overview\<close>
   1.125  
   1.126 -text {*
   1.127 +text \<open>
   1.128    \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
   1.129    \fontsize{9pt}{12pt}\selectfont
   1.130    \begin{tabular}{ll||c|c|c}
   1.131 @@ -189,12 +189,12 @@
   1.132        & \ttsize@{ML "Nbe.static_conv"}
   1.133        & \ttsize@{ML "Code_Evaluation.static_conv"}
   1.134    \end{tabular}
   1.135 -*}
   1.136 +\<close>
   1.137  
   1.138  
   1.139 -subsection {* Preprocessing HOL terms into evaluable shape *}
   1.140 +subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
   1.141  
   1.142 -text {*
   1.143 +text \<open>
   1.144    When integration decision procedures developed inside HOL into HOL itself,
   1.145    it is necessary to somehow get from the Isabelle/ML representation to
   1.146    the representation used by the decision procedure itself (``reification'').
   1.147 @@ -203,7 +203,7 @@
   1.148    @{ML "Reification.conv"} and @{ML "Reification.tac"}
   1.149  
   1.150    An simplistic example:
   1.151 -*}
   1.152 +\<close>
   1.153  
   1.154  datatype %quote form_ord = T | F | Less nat nat
   1.155    | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
   1.156 @@ -217,21 +217,21 @@
   1.157  | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
   1.158  | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
   1.159  
   1.160 -text {*
   1.161 +text \<open>
   1.162    The datatype @{type form_ord} represents formulae whose semantics is given by
   1.163    @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   1.164    whose concrete values are given in list @{term vs}.
   1.165 -*}
   1.166 +\<close>
   1.167  
   1.168 -ML (*<*) {* *}
   1.169 +ML (*<*) \<open>\<close>
   1.170  schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
   1.171  ML_prf 
   1.172 -(*>*) {* val thm =
   1.173 -  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"} *} (*<*)
   1.174 -by (tactic {* ALLGOALS (rtac thm) *})
   1.175 +(*>*) \<open>val thm =
   1.176 +  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
   1.177 +by (tactic \<open>ALLGOALS (rtac thm)\<close>)
   1.178  (*>*) 
   1.179  
   1.180 -text {*
   1.181 +text \<open>
   1.182    By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   1.183    which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   1.184    to @{const interp} does not contain any free variables and can thus be evaluated
   1.185 @@ -239,38 +239,38 @@
   1.186  
   1.187    A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   1.188    theory @{text Regexp_Method}.
   1.189 -*}
   1.190 +\<close>
   1.191  
   1.192  
   1.193 -subsection {* Intimate connection between logic and system runtime *}
   1.194 +subsection \<open>Intimate connection between logic and system runtime\<close>
   1.195  
   1.196 -text {*
   1.197 +text \<open>
   1.198    The toolbox of static evaluation conversions forms a reasonable base
   1.199    to interweave generated code and system tools.  However in some
   1.200    situations more direct interaction is desirable.
   1.201 -*}
   1.202 +\<close>
   1.203  
   1.204  
   1.205 -subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq} *}
   1.206 +subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close>
   1.207  
   1.208 -text {*
   1.209 +text \<open>
   1.210    The @{text code} antiquotation allows to include constants from
   1.211    generated code directly into ML system code, as in the following toy
   1.212    example:
   1.213 -*}
   1.214 +\<close>
   1.215  
   1.216  datatype %quote form = T | F | And form form | Or form form (*<*)
   1.217  
   1.218 -(*>*) ML %quotett {*
   1.219 +(*>*) ML %quotett \<open>
   1.220    fun eval_form @{code T} = true
   1.221      | eval_form @{code F} = false
   1.222      | eval_form (@{code And} (p, q)) =
   1.223          eval_form p andalso eval_form q
   1.224      | eval_form (@{code Or} (p, q)) =
   1.225          eval_form p orelse eval_form q;
   1.226 -*}
   1.227 +\<close>
   1.228  
   1.229 -text {*
   1.230 +text \<open>
   1.231    \noindent @{text code} takes as argument the name of a constant;
   1.232    after the whole ML is read, the necessary code is generated
   1.233    transparently and the corresponding constant names are inserted.
   1.234 @@ -281,24 +281,24 @@
   1.235  
   1.236    For a less simplistic example, theory @{text Approximation} in
   1.237    the @{text Decision_Procs} session is a good reference.
   1.238 -*}
   1.239 +\<close>
   1.240  
   1.241  
   1.242 -subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
   1.243 +subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close>
   1.244  
   1.245 -text {*
   1.246 +text \<open>
   1.247    The @{text code} antiquoation is lightweight, but the generated code
   1.248    is only accessible while the ML section is processed.  Sometimes this
   1.249    is not appropriate, especially if the generated code contains datatype
   1.250    declarations which are shared with other parts of the system.  In these
   1.251    cases, @{command_def code_reflect} can be used:
   1.252 -*}
   1.253 +\<close>
   1.254  
   1.255  code_reflect %quote Sum_Type
   1.256    datatypes sum = Inl | Inr
   1.257    functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
   1.258  
   1.259 -text {*
   1.260 +text \<open>
   1.261    \noindent @{command_def code_reflect} takes a structure name and
   1.262    references to datatypes and functions; for these code is compiled
   1.263    into the named ML structure and the \emph{Eval} target is modified
   1.264 @@ -309,17 +309,17 @@
   1.265  
   1.266    A typical example for @{command code_reflect} can be found in the
   1.267    @{theory Predicate} theory.
   1.268 -*}
   1.269 +\<close>
   1.270  
   1.271  
   1.272 -subsubsection {* Separate compilation -- @{text code_reflect} *}
   1.273 +subsubsection \<open>Separate compilation -- @{text code_reflect}\<close>
   1.274  
   1.275 -text {*
   1.276 +text \<open>
   1.277    For technical reasons it is sometimes necessary to separate
   1.278    generation and compilation of code which is supposed to be used in
   1.279    the system runtime.  For this @{command code_reflect} with an
   1.280    optional @{text "file"} argument can be used:
   1.281 -*}
   1.282 +\<close>
   1.283  
   1.284  code_reflect %quote Rat
   1.285    datatypes rat = Frct
   1.286 @@ -328,10 +328,10 @@
   1.287      "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   1.288    file "$ISABELLE_TMP/examples/rat.ML"
   1.289  
   1.290 -text {*
   1.291 +text \<open>
   1.292    \noindent This merely generates the referenced code to the given
   1.293    file which can be included into the system runtime later on.
   1.294 -*}
   1.295 +\<close>
   1.296  
   1.297  end
   1.298