src/Doc/Codegen/Evaluation.thy
changeset 65041 2525e680f94f
parent 63670 8e0148e1f5f4
child 66453 cc19f7ca2ed6
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Wed Feb 22 16:21:26 2017 +0000
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Wed Feb 22 20:24:50 2017 +0100
     1.3 @@ -22,14 +22,14 @@
     1.4  subsection \<open>Evaluation techniques\<close>
     1.5  
     1.6  text \<open>
     1.7 -  The existing infrastructure provides a rich palette of evaluation
     1.8 +  There is a rich palette of evaluation
     1.9    techniques, each comprising different aspects:
    1.10  
    1.11    \begin{description}
    1.12  
    1.13 -    \item[Expressiveness.]  Depending on how good symbolic computation
    1.14 -      is supported, the class of terms which can be evaluated may be
    1.15 -      bigger or smaller.
    1.16 +    \item[Expressiveness.]  Depending on the extent to which symbolic
    1.17 +      computation is possible, the class of terms which can be evaluated
    1.18 +      can be bigger or smaller.
    1.19  
    1.20      \item[Efficiency.]  The more machine-near the technique, the
    1.21        faster it is.
    1.22 @@ -67,27 +67,26 @@
    1.23  subsubsection \<open>Evaluation in ML (@{text code})\<close>
    1.24  
    1.25  text \<open>
    1.26 -  Highest performance can be achieved by evaluation in ML, at the cost
    1.27 +  Considerable performance can be achieved using evaluation in ML, at the cost
    1.28    of being restricted to ground results and a layered stack of code to
    1.29 -  be trusted, including code generator configurations by the user.
    1.30 +  be trusted, including a user's specific code generator setup.
    1.31  
    1.32    Evaluation is carried out in a target language \emph{Eval} which
    1.33    inherits from \emph{SML} but for convenience uses parts of the
    1.34 -  Isabelle runtime environment.  The soundness of computation carried
    1.35 -  out there depends crucially on the correctness of the code
    1.36 -  generator setup; this is one of the reasons why you should not use
    1.37 -  adaptation (see \secref{sec:adaptation}) frivolously.
    1.38 +  Isabelle runtime environment.  Hence soundness depends crucially
    1.39 +  on the correctness of the code generator setup; this is one of the
    1.40 +  reasons why you should not use adaptation (see \secref{sec:adaptation})
    1.41 +  frivolously.
    1.42  \<close>
    1.43  
    1.44  
    1.45 -subsection \<open>Aspects of evaluation\<close>
    1.46 +subsection \<open>Dynamic evaluation\<close>
    1.47  
    1.48  text \<open>
    1.49 -  Each of the techniques can be combined with different aspects.  The
    1.50 -  most important distinction is between dynamic and static evaluation.
    1.51    Dynamic evaluation takes the code generator configuration \qt{as it
    1.52 -  is} at the point where evaluation is issued.  Best example is the
    1.53 -  @{command_def value} command which allows ad-hoc evaluation of
    1.54 +  is} at the point where evaluation is issued and computes
    1.55 +  a corresponding result.  Best example is the
    1.56 +  @{command_def value} command for ad-hoc evaluation of
    1.57    terms:
    1.58  \<close>
    1.59  
    1.60 @@ -103,257 +102,103 @@
    1.61  value %quote [nbe] "42 / (12 :: rat)"
    1.62  
    1.63  text \<open>
    1.64 -  To employ dynamic evaluation in the document generation, there is also
    1.65 +  To employ dynamic evaluation in documents, there is also
    1.66    a @{text value} antiquotation with the same evaluation techniques 
    1.67    as @{command value}.
    1.68 +\<close>
    1.69  
    1.70 -  Static evaluation freezes the code generator configuration at a
    1.71 -  certain point and uses this context whenever evaluation is issued
    1.72 -  later on.  This is particularly appropriate for proof procedures
    1.73 -  which use evaluation, since then the behaviour of evaluation is not
    1.74 -  changed or even compromised later on by actions of the user.
    1.75 +  
    1.76 +subsubsection \<open>Term reconstruction in ML\<close>
    1.77  
    1.78 -  As a technical complication, terms after evaluation in ML must be
    1.79 +text \<open>
    1.80 +  Results from evaluation in ML must be
    1.81    turned into Isabelle's internal term representation again.  Since
    1.82 -  this is also configurable, it is never fully trusted.  For this
    1.83 -  reason, evaluation in ML comes with further aspects:
    1.84 +  that setup is highly configurable, it is never assumed to be trustable. 
    1.85 +  Hence evaluation in ML provides no full term reconstruction
    1.86 +  but distinguishes the following kinds:
    1.87  
    1.88    \begin{description}
    1.89  
    1.90 -    \item[Plain evaluation.]  A term is normalized using the provided
    1.91 -      term reconstruction from ML to Isabelle; for applications which
    1.92 -      do not need to be fully trusted.
    1.93 +    \item[Plain evaluation.]  A term is normalized using the vanilla
    1.94 +      term reconstruction from ML to Isabelle; this is a pragmatic
    1.95 +      approach for applications which do not need trustability.
    1.96  
    1.97      \item[Property conversion.]  Evaluates propositions; since these
    1.98        are monomorphic, the term reconstruction is fixed once and for all
    1.99 -      and therefore trustable.
   1.100 -
   1.101 -    \item[Conversion.]  Evaluates an arbitrary term @{term "t"} first
   1.102 -      by plain evaluation and certifies the result @{term "t'"} by
   1.103 -      checking the equation @{term "t \<equiv> t'"} using property
   1.104 -      conversion.
   1.105 +      and therefore trustable -- in the sense that only the regular
   1.106 +      code generator setup has to be trusted, without relying
   1.107 +      on term reconstruction from ML to Isabelle.
   1.108  
   1.109    \end{description}
   1.110  
   1.111 -  \noindent The picture is further complicated by the roles of
   1.112 -  exceptions.  Here three cases have to be distinguished:
   1.113 -
   1.114 -  \begin{itemize}
   1.115 -
   1.116 -    \item Evaluation of @{term t} terminates with a result @{term
   1.117 -      "t'"}.
   1.118 -
   1.119 -    \item Evaluation of @{term t} terminates which an exception
   1.120 -      indicating a pattern match failure or a non-implemented
   1.121 -      function.  As sketched in \secref{sec:partiality}, this can be
   1.122 -      interpreted as partiality.
   1.123 -     
   1.124 -    \item Evaluation raises any other kind of exception.
   1.125 -     
   1.126 -  \end{itemize}
   1.127 -
   1.128 -  \noindent For conversions, the first case yields the equation @{term
   1.129 -  "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
   1.130 -  Exceptions of the third kind are propagated to the user.
   1.131 -
   1.132 -  By default return values of plain evaluation are optional, yielding
   1.133 -  @{text "SOME t'"} in the first case, @{text "NONE"} in the
   1.134 -  second, and propagating the exception in the third case.  A strict
   1.135 -  variant of plain evaluation either yields @{text "t'"} or propagates
   1.136 -  any exception, a liberal variant captures any exception in a result
   1.137 -  of type @{text "Exn.result"}.
   1.138 -  
   1.139 -  For property conversion (which coincides with conversion except for
   1.140 -  evaluation in ML), methods are provided which solve a given goal by
   1.141 -  evaluation.
   1.142 +  \noindent The different degree of trustability is also manifest in the
   1.143 +  types of the corresponding ML functions: plain evaluation
   1.144 +  operates on uncertified terms, whereas property conversion
   1.145 +  operates on certified terms.
   1.146  \<close>
   1.147  
   1.148  
   1.149 -subsection \<open>Schematic overview\<close>
   1.150 +subsubsection \<open>The partiality principle \label{sec:partiality_principle}\<close>
   1.151 +
   1.152 +text \<open>
   1.153 +  During evaluation exceptions indicating a pattern
   1.154 +  match failure or a non-implemented function are treated specially:
   1.155 +  as sketched in \secref{sec:partiality}, such
   1.156 +  exceptions can be interpreted as partiality.  For plain evaluation,
   1.157 +  the result hence is optional; property conversion falls back
   1.158 +  to reflexivity in such cases.
   1.159 +\<close>
   1.160 +  
   1.161 +
   1.162 +subsubsection \<open>Schematic overview\<close>
   1.163  
   1.164  text \<open>
   1.165    \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
   1.166    \fontsize{9pt}{12pt}\selectfont
   1.167 -  \begin{tabular}{ll||c|c|c}
   1.168 -    & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
   1.169 -    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
   1.170 -      & interactive evaluation 
   1.171 -      & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
   1.172 -      \tabularnewline
   1.173 -    & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
   1.174 -    & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
   1.175 -    & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
   1.176 -    & conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
   1.177 -      & \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline
   1.178 -    \multirow{3}{1ex}{\rotatebox{90}{static}}
   1.179 -    & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
   1.180 -    & property conversion & &
   1.181 -      & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
   1.182 -    & conversion & \ttsize@{ML "Code_Simp.static_conv"}
   1.183 -      & \ttsize@{ML "Nbe.static_conv"}
   1.184 -      & \ttsize@{ML "Code_Evaluation.static_conv"}
   1.185 +  \begin{tabular}{l||c|c|c}
   1.186 +    & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
   1.187 +    interactive evaluation & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"} \tabularnewline
   1.188 +    plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline
   1.189 +    evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
   1.190 +    property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline
   1.191 +    conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
   1.192    \end{tabular}
   1.193  \<close>
   1.194  
   1.195 -text \<open>
   1.196 -  \noindent Note that @{ML Code_Evaluation.static_value} and
   1.197 -  @{ML Code_Evaluation.static_conv} require certain code equations to
   1.198 -  reconstruct Isabelle terms from results and certify results.  This is
   1.199 -  achieved as follows:
   1.200 -
   1.201 -  \<^enum> Identify which result types are expected.
   1.202 -
   1.203 -  \<^enum> Define an auxiliary operation which for each possible result type @{text \<tau>}
   1.204 -    contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\<tau> itself"}
   1.205 -    (for @{ML Code_Evaluation.static_value}) or
   1.206 -    a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\<tau> itself"}
   1.207 -    (for @{ML Code_Evaluation.static_conv}) respectively.
   1.208 -
   1.209 -  \<^enum> Include that auxiliary operation into the set of constants when generating
   1.210 -    the static conversion.
   1.211 -\<close>
   1.212 -
   1.213 -
   1.214 -subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
   1.215 -
   1.216 +  
   1.217 +subsection \<open>Static evaluation\<close>
   1.218 +  
   1.219  text \<open>
   1.220 -  When integrating decision procedures developed inside HOL into HOL itself,
   1.221 -  it is necessary to somehow get from the Isabelle/ML representation to
   1.222 -  the representation used by the decision procedure itself (``reification'').
   1.223 -  One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
   1.224 -  Another option is to use pre-existing infrastructure in HOL:
   1.225 -  @{ML "Reification.conv"} and @{ML "Reification.tac"}
   1.226 -
   1.227 -  A simplistic example:
   1.228 -\<close>
   1.229 -
   1.230 -datatype %quote form_ord = T | F | Less nat nat
   1.231 -  | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
   1.232 -
   1.233 -primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
   1.234 -where
   1.235 -  "interp T vs \<longleftrightarrow> True"
   1.236 -| "interp F vs \<longleftrightarrow> False"
   1.237 -| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
   1.238 -| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
   1.239 -| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
   1.240 -| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
   1.241 -
   1.242 -text \<open>
   1.243 -  The datatype @{type form_ord} represents formulae whose semantics is given by
   1.244 -  @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   1.245 -  whose concrete values are given in list @{term vs}.
   1.246 -\<close>
   1.247 -
   1.248 -ML (*<*) \<open>\<close>
   1.249 -schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
   1.250 -ML_prf 
   1.251 -(*>*) \<open>val thm =
   1.252 -  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
   1.253 -by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
   1.254 -(*>*) 
   1.255 -
   1.256 -text \<open>
   1.257 -  By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   1.258 -  which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   1.259 -  to @{const interp} does not contain any free variables and can thus be evaluated
   1.260 -  using evaluation.
   1.261 -
   1.262 -  A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   1.263 -  theory @{text Regexp_Method}.
   1.264 +  When implementing proof procedures using evaluation,
   1.265 +  in most cases the code generator setup is appropriate
   1.266 +  \qt{as it was} when the proof procedure was written in ML,
   1.267 +  not an arbitrary later potentially modified setup.  This is
   1.268 +  called static evaluation.
   1.269  \<close>
   1.270  
   1.271  
   1.272 -subsection \<open>Intimate connection between logic and system runtime\<close>
   1.273 -
   1.274 -text \<open>
   1.275 -  The toolbox of static evaluation conversions forms a reasonable base
   1.276 -  to interweave generated code and system tools.  However in some
   1.277 -  situations more direct interaction is desirable.
   1.278 -\<close>
   1.279 -
   1.280 -
   1.281 -subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close>
   1.282 -
   1.283 +subsubsection \<open>Static evaluation using @{text simp} and @{text nbe}\<close>
   1.284 +  
   1.285  text \<open>
   1.286 -  The @{text code} antiquotation allows to include constants from
   1.287 -  generated code directly into ML system code, as in the following toy
   1.288 -  example:
   1.289 -\<close>
   1.290 -
   1.291 -datatype %quote form = T | F | And form form | Or form form (*<*)
   1.292 -
   1.293 -(*>*) ML %quotett \<open>
   1.294 -  fun eval_form @{code T} = true
   1.295 -    | eval_form @{code F} = false
   1.296 -    | eval_form (@{code And} (p, q)) =
   1.297 -        eval_form p andalso eval_form q
   1.298 -    | eval_form (@{code Or} (p, q)) =
   1.299 -        eval_form p orelse eval_form q;
   1.300 -\<close>
   1.301 -
   1.302 -text \<open>
   1.303 -  \noindent @{text code} takes as argument the name of a constant;
   1.304 -  after the whole ML is read, the necessary code is generated
   1.305 -  transparently and the corresponding constant names are inserted.
   1.306 -  This technique also allows to use pattern matching on constructors
   1.307 -  stemming from compiled datatypes.  Note that the @{text code}
   1.308 -  antiquotation may not refer to constants which carry adaptations;
   1.309 -  here you have to refer to the corresponding adapted code directly.
   1.310 -
   1.311 -  For a less simplistic example, theory @{text Approximation} in
   1.312 -  the @{text Decision_Procs} session is a good reference.
   1.313 +  For @{text simp} and @{text nbe} static evaluation can be achieved using 
   1.314 +  @{ML Code_Simp.static_conv} and @{ML Nbe.static_conv}.
   1.315 +  Note that @{ML Nbe.static_conv} by its very nature
   1.316 +  requires an invocation of the ML compiler for every call,
   1.317 +  which can produce significant overhead.
   1.318  \<close>
   1.319  
   1.320  
   1.321 -subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close>
   1.322 -
   1.323 -text \<open>
   1.324 -  The @{text code} antiquoation is lightweight, but the generated code
   1.325 -  is only accessible while the ML section is processed.  Sometimes this
   1.326 -  is not appropriate, especially if the generated code contains datatype
   1.327 -  declarations which are shared with other parts of the system.  In these
   1.328 -  cases, @{command_def code_reflect} can be used:
   1.329 -\<close>
   1.330 -
   1.331 -code_reflect %quote Sum_Type
   1.332 -  datatypes sum = Inl | Inr
   1.333 -  functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
   1.334 +subsubsection \<open>Intimate connection between logic and system runtime\<close>
   1.335  
   1.336  text \<open>
   1.337 -  \noindent @{command_def code_reflect} takes a structure name and
   1.338 -  references to datatypes and functions; for these code is compiled
   1.339 -  into the named ML structure and the \emph{Eval} target is modified
   1.340 -  in a way that future code generation will reference these
   1.341 -  precompiled versions of the given datatypes and functions.  This
   1.342 -  also allows to refer to the referenced datatypes and functions from
   1.343 -  arbitrary ML code as well.
   1.344 -
   1.345 -  A typical example for @{command code_reflect} can be found in the
   1.346 -  @{theory Predicate} theory.
   1.347 +  Static evaluation for @{text eval} operates differently --
   1.348 +  the required generated code is inserted directly into an ML
   1.349 +  block using antiquotations.  The idea is that generated
   1.350 +  code performing static evaluation (called a \<^emph>\<open>computation\<close>)
   1.351 +  is compiled once and for all such that later calls do not
   1.352 +  require any invocation of the code generator or the ML
   1.353 +  compiler at all.  This topic deserved a dedicated chapter
   1.354 +  \secref{sec:computations}.
   1.355  \<close>
   1.356 -
   1.357 -
   1.358 -subsubsection \<open>Separate compilation -- @{text code_reflect}\<close>
   1.359 -
   1.360 -text \<open>
   1.361 -  For technical reasons it is sometimes necessary to separate
   1.362 -  generation and compilation of code which is supposed to be used in
   1.363 -  the system runtime.  For this @{command code_reflect} with an
   1.364 -  optional \<^theory_text>\<open>file\<close> argument can be used:
   1.365 -\<close>
   1.366 -
   1.367 -code_reflect %quote Rat
   1.368 -  datatypes rat
   1.369 -  functions Fract
   1.370 -    "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   1.371 -    "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   1.372 -  file "$ISABELLE_TMP/examples/rat.ML"
   1.373 -
   1.374 -text \<open>
   1.375 -  \noindent This merely generates the referenced code to the given
   1.376 -  file which can be included into the system runtime later on.
   1.377 -\<close>
   1.378 -
   1.379 +  
   1.380  end
   1.381 -