basic documentation for computations
authorhaftmann
Wed Feb 22 20:24:50 2017 +0100 (2017-02-22)
changeset 650412525e680f94f
parent 65040 5975839e8d25
child 65042 956ea00a162a
basic documentation for computations
CONTRIBUTORS
NEWS
src/Doc/Codegen/Adaptation.thy
src/Doc/Codegen/Computations.thy
src/Doc/Codegen/Evaluation.thy
src/Doc/Codegen/Further.thy
src/Doc/Codegen/document/root.tex
src/Doc/Codegen/document/style.sty
src/Doc/ROOT
     1.1 --- a/CONTRIBUTORS	Wed Feb 22 16:21:26 2017 +0000
     1.2 +++ b/CONTRIBUTORS	Wed Feb 22 20:24:50 2017 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* February 2017: Florian Haftmann, TUM
     1.8 +  Statically embedded computatations implementated by generated code.
     1.9 +
    1.10  
    1.11  Contributions to Isabelle2016-1
    1.12  -------------------------------
     2.1 --- a/NEWS	Wed Feb 22 16:21:26 2017 +0000
     2.2 +++ b/NEWS	Wed Feb 22 20:24:50 2017 +0100
     2.3 @@ -12,6 +12,17 @@
     2.4  * Document antiquotations @{prf} and @{full_prf} output proof terms
     2.5  (again) in the same way as commands 'prf' and 'full_prf'.
     2.6  
     2.7 +* Computations generated by the code generator can be embedded
     2.8 +directly into ML, alongside with @{code} antiquotations, using
     2.9 +the following antiquotations:
    2.10 +
    2.11 +  @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
    2.12 +  @{computation_conv … terms: … datatypes: …} : ('ml -> conv) -> Proof.context -> conv
    2.13 +  @{computation_check terms: … datatypes: …} : Proof.context -> conv
    2.14 +
    2.15 +See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
    2.16 +and src/HOL/Decision_Procs/Reflective_Field.thy for examples.
    2.17 +
    2.18  
    2.19  *** Prover IDE -- Isabelle/Scala/jEdit ***
    2.20  
     3.1 --- a/src/Doc/Codegen/Adaptation.thy	Wed Feb 22 16:21:26 2017 +0000
     3.2 +++ b/src/Doc/Codegen/Adaptation.thy	Wed Feb 22 20:24:50 2017 +0100
     3.3 @@ -148,7 +148,7 @@
     3.4    discretion of the user to take care for this.
     3.5  \<close>
     3.6  
     3.7 -subsection \<open>Common adaptation applications\<close>
     3.8 +subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close>
     3.9  
    3.10  text \<open>
    3.11    The @{theory HOL} @{theory Main} theory already provides a code
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Doc/Codegen/Computations.thy	Wed Feb 22 20:24:50 2017 +0100
     4.3 @@ -0,0 +1,544 @@
     4.4 +theory Computations
     4.5 +  imports Setup
     4.6 +    "~~/src/HOL/Library/Code_Target_Int"
     4.7 +    "~~/src/HOL/Library/Code_Char"
     4.8 +begin
     4.9 +
    4.10 +section \<open>Computations \label{sec:computations}\<close>
    4.11 +
    4.12 +subsection \<open>Prelude -- The @{text code} antiquotation \label{sec:code_antiq}\<close>
    4.13 +
    4.14 +text \<open>
    4.15 +  The @{ML_antiquotation_def code} antiquotation allows to include constants
    4.16 +  from
    4.17 +  generated code directly into ML system code, as in the following toy
    4.18 +  example:
    4.19 +\<close>
    4.20 +
    4.21 +datatype %quote form = T | F | And form form | Or form form (*<*)
    4.22 +
    4.23 +(*>*) ML %quotetypewriter \<open>
    4.24 +  fun eval_form @{code T} = true
    4.25 +    | eval_form @{code F} = false
    4.26 +    | eval_form (@{code And} (p, q)) =
    4.27 +        eval_form p andalso eval_form q
    4.28 +    | eval_form (@{code Or} (p, q)) =
    4.29 +        eval_form p orelse eval_form q;
    4.30 +\<close>
    4.31 +
    4.32 +text \<open>
    4.33 +  \noindent The antiquotation @{ML_antiquotation code} takes
    4.34 +  the name of a constant as argument;
    4.35 +  the required code is generated
    4.36 +  transparently and the corresponding constant names are inserted
    4.37 +  for the given antiquotations.  This technique allows to use pattern
    4.38 +  matching on constructors stemming from compiled datatypes.
    4.39 +  Note that the @{ML_antiquotation code}
    4.40 +  antiquotation may not refer to constants which carry adaptations;
    4.41 +  here you have to refer to the corresponding adapted code directly.
    4.42 +\<close>
    4.43 +
    4.44 +  
    4.45 +subsection \<open>The concept of computations\<close>
    4.46 +
    4.47 +text \<open>
    4.48 +  Computations embody the simple idea that for each
    4.49 +  monomorphic Isabelle/HOL term of type @{text \<tau>} by virtue of
    4.50 +  code generation there exists an corresponding ML type @{text T} and
    4.51 +  a morphism @{text "\<Phi> :: \<tau> \<rightarrow> T"} satisfying
    4.52 +  @{text "\<Phi> (t\<^sub>1 \<cdot> t\<^sub>2) = \<Phi> t\<^sub>1 \<cdot> \<Phi> t\<^sub>2"}, with @{text \<cdot>} denoting
    4.53 +  term application.
    4.54 +
    4.55 +  For a given Isabelle/HOL type @{text \<tau>}, parts of @{text \<Phi>} can be
    4.56 +  implemented by a corresponding ML function @{text "\<phi>\<^sub>\<tau> :: term \<rightarrow> T"}.
    4.57 +  How?
    4.58 +
    4.59 +    \<^descr> \<open>Let input be a constant C :: \<tau>.\<close> \\
    4.60 +      Then @{text "\<phi>\<^sub>\<tau> C = f\<^sub>C"} with @{text "f\<^sub>C"} being
    4.61 +      the image of @{text C} under code generation.
    4.62 +
    4.63 +    \<^descr> \<open>Let input be an application (t\<^sub>1 \<cdot> t\<^sub>2) :: \<tau>.\<close> \\
    4.64 +      Then @{text "\<phi>\<^sub>\<tau> (t\<^sub>1 \<cdot> t\<^sub>2) = \<phi>\<^sub>\<tau> t\<^sub>1 (\<phi>\<^sub>\<tau> t\<^sub>2)"}.
    4.65 +
    4.66 +  \noindent Using these trivial properties, each monomorphic constant
    4.67 +  @{text "C : \<^vec>\<tau>\<^sub>n \<rightarrow> \<tau>"} yields the following
    4.68 +  equations:
    4.69 +\<close>
    4.70 +
    4.71 +text %quote \<open>
    4.72 +  @{text "\<phi>\<^bsub>(\<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>)\<^esub> C = f\<^sub>C"} \\
    4.73 +  @{text "\<phi>\<^bsub>(\<tau>\<^sub>2 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>)\<^esub> (C \<cdot> t\<^sub>1) = f\<^sub>C (\<phi>\<^bsub>\<tau>\<^sub>1\<^esub> t\<^sub>1)"} \\
    4.74 +  @{text "\<dots>"} \\
    4.75 +  @{text "\<phi>\<^bsub>\<tau>\<^esub> (C \<cdot> t\<^sub>1 \<cdot> \<dots> \<cdot> t\<^sub>n) = f\<^sub>C (\<phi>\<^bsub>\<tau>\<^sub>1\<^esub> t\<^sub>1) \<dots> (\<phi>\<^bsub>\<tau>\<^sub>n\<^esub> t\<^sub>n)"}
    4.76 +\<close>
    4.77 +  
    4.78 +text \<open>
    4.79 +  \noindent Hence a computation is characterized as follows:
    4.80 +
    4.81 +    \<^item> Let @{text "input constants"} denote a set of monomorphic constants.
    4.82 +
    4.83 +    \<^item> Let @{text \<tau>} denote a monomorphic type and @{text "'ml"} be a schematic
    4.84 +      placeholder for its corresponding type in ML under code generation.
    4.85 +
    4.86 +    \<^item> Then the corresponding computation is an ML function of type
    4.87 +      @{ML_type "Proof.context -> term -> 'ml"}
    4.88 +      partially implementing the morphism @{text "\<Phi> :: \<tau> \<rightarrow> T"} for all
    4.89 +      \<^emph>\<open>input terms\<close> consisting only of input constants and applications.
    4.90 +
    4.91 +  \noindent The charming idea is that all required code is automatically generated
    4.92 +  by the code generator for givens input constants and types;
    4.93 +  that code is directly inserted into the Isabelle/ML runtime system
    4.94 +  by means of antiquotations.
    4.95 +\<close>
    4.96 +
    4.97 +
    4.98 +subsection \<open>The @{text computation} antiquotation\<close>
    4.99 +
   4.100 +text \<open>
   4.101 +  The following example illustrates its basic usage:
   4.102 +\<close>
   4.103 +
   4.104 +ML %quotetypewriter \<open>
   4.105 +  local
   4.106 +
   4.107 +  fun int_of_nat @{code "0 :: nat"} = 0
   4.108 +    | int_of_nat (@{code Suc} n) = int_of_nat n + 1;
   4.109 +
   4.110 +  in
   4.111 +
   4.112 +  val comp_nat = @{computation nat terms:
   4.113 +    "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   4.114 +    "sum_list :: nat list \<Rightarrow> nat" "prod_list :: nat list \<Rightarrow> nat"
   4.115 +    datatypes: nat "nat list"}
   4.116 +    (fn post => post o HOLogic.mk_nat o int_of_nat o the);
   4.117 +
   4.118 +  end
   4.119 +\<close>
   4.120 +
   4.121 +text \<open>
   4.122 +    \<^item> Antiquotations occurring in the
   4.123 +      same ML block always refer to the same transparently generated code;
   4.124 +      particularly, they share the same transparently generated datatype
   4.125 +      declarations.
   4.126 +
   4.127 +    \<^item> The type of a computation is specified as first argument.
   4.128 +
   4.129 +    \<^item> Input constants are specified the following ways:
   4.130 +
   4.131 +        \<^item> Each term following @{text "terms:"} specifies all constants
   4.132 +          it contains as input constants.
   4.133 +
   4.134 +        \<^item> Each type following @{text "datatypes:"} specifies all constructors
   4.135 +          of the corresponding code datatype as input constants.  Note that
   4.136 +          this does not increase expressiveness but succinctness for datatypes
   4.137 +          with many constructors.
   4.138 +
   4.139 +    \<^item> The code generated by a @{text computation} antiquotation takes a functional argument
   4.140 +      which describes how to conclude the computation.  What's the rationale
   4.141 +      behind this?
   4.142 +
   4.143 +        \<^item> There is no automated way to generate a reconstruction function
   4.144 +          from the resulting ML type to a Isabelle term -- this is in the
   4.145 +          responsibility of the implementor.  One possible approach
   4.146 +          for robust term reconstruction is the @{text code} antiquotation.
   4.147 +
   4.148 +        \<^item> Both statically specified input constants and dynamically provided input
   4.149 +          terms are subject to preprocessing.  Likewise the result
   4.150 +          is supposed to be subject to postprocessing; the implementor
   4.151 +          is expected this out explicitly.
   4.152 +
   4.153 +        \<^item> Computations follow the partiality principle (cf.~\secref{sec:partiality_principle}):
   4.154 +          failures due to pattern matching or unspecified functions
   4.155 +          are interpreted as partiality; therefore resulting ML values
   4.156 +          are optional. 
   4.157 +
   4.158 +      Hence the functional argument accepts the following parameters
   4.159 +
   4.160 +        \<^item> A postprocessor function @{ML_type "term -> term"}.
   4.161 +
   4.162 +        \<^item> The resulting value as optional argument.
   4.163 +
   4.164 +      The functional argument is supposed to compose the final result
   4.165 +      from these in a suitable manner.
   4.166 +
   4.167 +  \noindent A simple application:
   4.168 +\<close>
   4.169 +
   4.170 +ML_val %quotetypewriter \<open>
   4.171 +  comp_nat @{context} @{term "sum_list [Suc 0, Suc (Suc 0)] * Suc (Suc 0)"}
   4.172 +\<close>
   4.173 +
   4.174 +text \<open>
   4.175 +  \noindent A single ML block may contain an arbitrary number of computation
   4.176 +  antiquotations.  These share the \<^emph>\<open>same\<close> set of possible
   4.177 +  input constants.  In other words, it does not matter in which
   4.178 +  antiquotation constants are specified;  in the following example,
   4.179 +  \<^emph>\<open>all\<close> constants are specified by the first antiquotation once
   4.180 +  and for all:
   4.181 +\<close>
   4.182 +
   4.183 +ML %quotetypewriter \<open>
   4.184 +  local
   4.185 +
   4.186 +  fun int_of_nat @{code "0 :: nat"} = 0
   4.187 +    | int_of_nat (@{code Suc} n) = int_of_nat n + 1;
   4.188 +
   4.189 +  in
   4.190 +
   4.191 +  val comp_nat = @{computation nat terms:
   4.192 +    "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   4.193 +    "sum_list :: nat list \<Rightarrow> nat" "prod_list :: nat list \<Rightarrow> nat"
   4.194 +    "replicate :: nat \<Rightarrow> nat \<Rightarrow> nat list"
   4.195 +    datatypes: nat "nat list"}
   4.196 +    (fn post => post o HOLogic.mk_nat o int_of_nat o the);
   4.197 +
   4.198 +  val comp_nat_list = @{computation "nat list"}
   4.199 +    (fn post => post o HOLogic.mk_list @{typ nat} o
   4.200 +      map (HOLogic.mk_nat o int_of_nat) o the);
   4.201 +
   4.202 +  end
   4.203 +\<close>
   4.204 +
   4.205 +  
   4.206 +subsection \<open>Pitfalls when specifying input constants \label{sec:input_constants_pitfalls}\<close>
   4.207 +
   4.208 +text \<open>
   4.209 +    \<^descr> \<open>Complete type coverage.\<close> Specified input constants must
   4.210 +      be \<^emph>\<open>complete\<close> in the sense that for each
   4.211 +      required type @{text \<tau>} there is at least one corresponding
   4.212 +      input constant which can actually \<^emph>\<open>construct\<close> a concrete
   4.213 +      value of type @{text \<tau>}, potentially requiring more types recursively;
   4.214 +      otherwise the system of equations cannot be generated properly.
   4.215 +      Hence such incomplete input constants sets are rejected immediately.
   4.216 +
   4.217 +    \<^descr> \<open>Unsuitful right hand sides.\<close> The generated code for a computation
   4.218 +      must compile in the strict ML runtime environment.  This imposes
   4.219 +      the technical restriction that each compiled input constant
   4.220 +      @{text f\<^sub>C} on the right hand side of a generated equations
   4.221 +      must compile without throwing an exception.  That rules
   4.222 +      out pathological examples like @{term [source] "undefined :: nat"}
   4.223 +      as input constants, as well as abstract constructors (cf. \secref{sec:invariant}).
   4.224 +
   4.225 +    \<^descr> \<open>Preprocessing.\<close> For consistency, input constants are subject
   4.226 +      to preprocessing;  however, the overall approach requires
   4.227 +      to operate on constants @{text C} and their respective compiled images
   4.228 +      @{text f\<^sub>C}.\footnote{Technical restrictions of the implementation
   4.229 +      enforce this, although those could be lifted in the future.}
   4.230 +      This is a problem whenever preprocessing maps an input constant
   4.231 +      to a non-constant.
   4.232 +
   4.233 +      To circumvent these situations, the computation machinery
   4.234 +      has a dedicated preprocessor which is applied \<^emph>\<open>before\<close>
   4.235 +      the regular preprocessing, both to input constants as well as
   4.236 +      input terms.  This can be used to map problematic constants
   4.237 +      to other ones that are not subject to regular preprocessing. 
   4.238 +      Rewrite rules are added using attribute @{attribute code_computation_unfold}.
   4.239 +      There should rarely be a need to use this beyond the few default
   4.240 +      setups in HOL, which deal with literals (see also \secref{sec:literal_input}).
   4.241 +\<close>
   4.242 +
   4.243 +  
   4.244 +subsection \<open>Pitfalls concerning input terms\<close>
   4.245 +
   4.246 +text \<open>
   4.247 +    \<^descr> \<open>No polymorphims.\<close> Input terms must be monomorphic: compilation
   4.248 +      to ML requires dedicated choice of monomorphic types.
   4.249 +
   4.250 +    \<^descr> \<open>No abstractions.\<close> Only constants and applications are admissible
   4.251 +      as input; abstractions are not possible.  In theory, the
   4.252 +      compilation schema could be extended to cover abstractions also,
   4.253 +      but this would increase the trusted code base.  If abstractions
   4.254 +      are required, they can always be eliminated by a dedicated preprocessing
   4.255 +      step, e.g.~using combinatorial logic.
   4.256 +
   4.257 +    \<^descr> \<open>Potential interfering of the preprocessor.\<close> As described in \secref{sec:input_constants_pitfalls}
   4.258 +      regular preprocessing can have a disruptive effect for input constants.
   4.259 +      The same also applies to input terms; however the same measures 
   4.260 +      to circumvent that problem for input constants apply to input terms also.
   4.261 +\<close>
   4.262 +
   4.263 +  
   4.264 +subsection \<open>Computations using the @{text computation_conv} antiquotation\<close>
   4.265 +
   4.266 +text \<open>
   4.267 +  Computations are a device to implement fast proof procedures.
   4.268 +  Then results of a computation are often assumed to be trustable
   4.269 +  and thus wrapped in oracles (see \cite{isabelle-isar-ref}),
   4.270 +  as in the following example:\footnote{
   4.271 +  The technical details how numerals are dealt with are given later in
   4.272 +  \secref{sec:literal_input}.}
   4.273 +\<close>
   4.274 +
   4.275 +ML %quotetypewriter \<open>
   4.276 +  local
   4.277 +
   4.278 +  fun raw_dvd (b, ct) = Thm.mk_binop @{cterm "Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> prop"}
   4.279 +    ct (if b then @{cterm True} else @{cterm False});
   4.280 +
   4.281 +  val (_, dvd_oracle) = Context.>>> (Context.map_theory_result
   4.282 +    (Thm.add_oracle (@{binding dvd}, raw_dvd)));
   4.283 +
   4.284 +  in
   4.285 +
   4.286 +  val conv_dvd = @{computation_conv bool terms:
   4.287 +    "Rings.dvd :: int \<Rightarrow> int \<Rightarrow> bool"
   4.288 +    "plus :: int \<Rightarrow> int \<Rightarrow> int"
   4.289 +    "minus :: int \<Rightarrow> int \<Rightarrow> int"
   4.290 +    "times :: int \<Rightarrow> int \<Rightarrow> int"
   4.291 +    "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
   4.292 +  } (curry dvd_oracle)
   4.293 +
   4.294 +  end
   4.295 +\<close>
   4.296 +
   4.297 +text \<open>
   4.298 +    \<^item> Antiquotation @{ML_antiquotation computation_conv} basically yields
   4.299 +      a conversion of type @{ML_type "Proof.context -> cterm -> thm"}
   4.300 +      (see further \cite{isabelle-implementation}).
   4.301 +
   4.302 +    \<^item> The antiquotation expects one functional argument to bridge the
   4.303 +      \qt{untrusted gap};  this can be done e.g.~using an oracle.  Since that oracle
   4.304 +      will only yield \qt{valid} results in the context of that particular
   4.305 +      computation, the implementor must make sure that it does not leave
   4.306 +      the local ML scope;  in this example, this is achieved using
   4.307 +      an explicit @{text local} ML block.  The very presence of the oracle
   4.308 +      in the code acknowledges that each computation requires explicit thinking
   4.309 +      before it can be considered trustworthy!
   4.310 +
   4.311 +    \<^item> Postprocessing just operates as further conversion after normalization.
   4.312 +
   4.313 +    \<^item> Partiality makes the whole conversion fall back to reflexivity.
   4.314 +\<close> (*<*)
   4.315 +
   4.316 +(*>*) ML_val %quotetypewriter \<open>
   4.317 +  conv_dvd @{context} @{cterm "7 dvd ( 62437867527846782 :: int)"};
   4.318 +  conv_dvd @{context} @{cterm "7 dvd (-62437867527846783 :: int)"};
   4.319 +\<close>
   4.320 +
   4.321 +text \<open>
   4.322 +  \noindent An oracle is not the only way to construct a valid theorem.
   4.323 +  A computation result can be used to construct an appropriate certificate:
   4.324 +\<close>
   4.325 +
   4.326 +lemma %quote conv_div_cert:
   4.327 +  "(Code_Target_Int.positive r * Code_Target_Int.positive s)
   4.328 +     div Code_Target_Int.positive s \<equiv> (numeral r :: int)" (is "?lhs \<equiv> ?rhs")
   4.329 +proof (rule eq_reflection)
   4.330 +  have "?lhs = numeral r * numeral s div numeral s"
   4.331 +    by simp
   4.332 +  also have "numeral r * numeral s div numeral s = ?rhs"
   4.333 +    by (rule nonzero_mult_div_cancel_right) simp
   4.334 +  finally show "?lhs = ?rhs" .
   4.335 +qed
   4.336 +
   4.337 +lemma %quote positive_mult:
   4.338 +  "Code_Target_Int.positive r * Code_Target_Int.positive s = 
   4.339 +    Code_Target_Int.positive (r * s)"
   4.340 +  by simp
   4.341 +  
   4.342 +ML %quotetypewriter \<open>
   4.343 +  local
   4.344 +
   4.345 +  fun integer_of_int (@{code int_of_integer} k) = k
   4.346 +
   4.347 +  val cterm_of_int = Thm.cterm_of @{context} o HOLogic.mk_numeral o integer_of_int;
   4.348 +
   4.349 +  val divisor = Thm.dest_arg o Thm.dest_arg;
   4.350 +
   4.351 +  fun evaluate thm = 
   4.352 +    Simplifier.rewrite_rule 
   4.353 +      (Proof_Context.transfer (Thm.theory_of_thm thm) @{context})
   4.354 +      (map mk_eq @{thms arith_simps positive_mult}) thm; (*FIXME proper ctxt*)
   4.355 +
   4.356 +  fun revaluate k ct =
   4.357 +    @{thm conv_div_cert}
   4.358 +    |> Thm.instantiate' [] [SOME (cterm_of_int k), SOME (divisor ct)]
   4.359 +    |> evaluate;
   4.360 +
   4.361 +  in
   4.362 +
   4.363 +  val conv_div = @{computation_conv int terms:
   4.364 +    "divide :: int \<Rightarrow> int \<Rightarrow> int"
   4.365 +    "0 :: int" "1 :: int" "2 :: int" "3 :: int"
   4.366 +  } revaluate
   4.367 +
   4.368 +  end
   4.369 +\<close>
   4.370 +
   4.371 +ML_val %quotetypewriter \<open>
   4.372 +  conv_div @{context}
   4.373 +    @{cterm "46782454343499999992777742432342242323423425 div (7 :: int)"}
   4.374 +\<close>
   4.375 +
   4.376 +text \<open>
   4.377 +  \noindent The example is intentionally kept simple: only positive
   4.378 +  integers are covered, only remainder-free divisions are feasible,
   4.379 +  and the input term is expected to have a particular shape.
   4.380 +  This exhibits the idea more clearly:
   4.381 +  the result of the computation is used as a mere
   4.382 +  hint how to instantiate @{fact conv_div_cert}, from which the required
   4.383 +  theorem is obtained by performing multiplication using the
   4.384 +  simplifier;  hence that theorem is built of proper inferences,
   4.385 +  with no oracles involved.
   4.386 +\<close>
   4.387 +
   4.388 +
   4.389 +subsection \<open>Computations using the @{text computation_check} antiquotation\<close>
   4.390 +
   4.391 +text \<open>
   4.392 +  The @{text computation_check} antiquotation is convenient if
   4.393 +  only a positive checking of propositions is desired, because then
   4.394 +  the result type is fixed (@{typ prop}) and all the technical
   4.395 +  matter concerning postprocessing and oracles is done in the framework
   4.396 +  once and for all:
   4.397 +\<close>
   4.398 +
   4.399 +ML %quotetypewriter \<open>
   4.400 +  val check_nat = @{computation_check terms:
   4.401 +    Trueprop "less :: nat \<Rightarrow> nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" 
   4.402 +    "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   4.403 +    "0 :: nat" Suc
   4.404 +  }
   4.405 +\<close>
   4.406 +
   4.407 +text \<open>
   4.408 +  \noindent The HOL judgement @{term Trueprop} embeds an expression
   4.409 +  of type @{typ bool} into @{typ prop}.
   4.410 +\<close>
   4.411 +
   4.412 +ML_val %quotetypewriter \<open>
   4.413 +  check_nat @{context} @{cprop "less (Suc (Suc 0)) (Suc (Suc (Suc 0)))"}
   4.414 +\<close>
   4.415 +
   4.416 +text \<open>
   4.417 +  \noindent Note that such computations can only \<^emph>\<open>check\<close>
   4.418 +  for @{typ prop}s to hold but not \<^emph>\<open>decide\<close>.
   4.419 +\<close>
   4.420 +
   4.421 +
   4.422 +subsection \<open>Some practical hints\<close>  
   4.423 +
   4.424 +subsubsection \<open>Inspecting generated code\<close>
   4.425 +
   4.426 +text \<open>
   4.427 +  The antiquotations for computations attempt to produce meaningful error
   4.428 +  messages.  If these are not sufficient, it might by useful to
   4.429 +  inspect the generated code, which can be achieved using
   4.430 +\<close>
   4.431 +  
   4.432 +declare %quote [[ML_source_trace]] (*<*) declare %quote [[ML_source_trace = false]] (*>*)
   4.433 +
   4.434 +
   4.435 +subsubsection \<open>Literals as input constants \label{sec:literal_input}\<close>
   4.436 +
   4.437 +text \<open>
   4.438 +  Literals (characters, numerals) in computations cannot be processed
   4.439 +  naively: the compilation pattern for computations fails whenever
   4.440 +  target-language literals are involved; since various
   4.441 +  common code generator setups (see \secref{sec:common_adaptation})
   4.442 +  implement @{typ nat} and @{typ int} by target-language literals,
   4.443 +  this problem manifests whenever numeric types are involved.
   4.444 +  In practice, this is circumvented with a dedicated preprocessor
   4.445 +  setup for literals (see also \secref{sec:input_constants_pitfalls}).
   4.446 +
   4.447 +  The following examples illustrate the pattern
   4.448 +  how to specify input constants when literals are involved, without going into
   4.449 +  too much detail:
   4.450 +\<close>
   4.451 +
   4.452 +paragraph \<open>An example for @{typ nat}\<close>
   4.453 +
   4.454 +ML %quotetypewriter \<open>
   4.455 +  val check_nat = @{computation_check terms:
   4.456 +    Trueprop "even :: nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" 
   4.457 +    "0 :: nat" Suc "1 :: nat" "2 :: nat" "3 :: nat"
   4.458 +  }
   4.459 +\<close>
   4.460 +
   4.461 +ML_val %quotetypewriter \<open>
   4.462 +  check_nat @{context} @{cprop "even (Suc 0 + 1 + 2 + 3 + 4 + 5)"}
   4.463 +\<close>
   4.464 +  
   4.465 +paragraph \<open>An example for @{typ int}\<close>
   4.466 +
   4.467 +ML %quotetypewriter \<open>
   4.468 +  val check_int = @{computation_check terms:
   4.469 +    Trueprop "even :: int \<Rightarrow> bool" "plus :: int \<Rightarrow> int \<Rightarrow> int" 
   4.470 +    "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
   4.471 +  }
   4.472 +\<close>
   4.473 +
   4.474 +ML_val %quotetypewriter \<open>
   4.475 +  check_int @{context} @{cprop "even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)"}
   4.476 +\<close>
   4.477 +  
   4.478 +paragraph \<open>An example for @{typ char}\<close>
   4.479 +
   4.480 +definition %quote is_cap_letter :: "char \<Rightarrow> bool"
   4.481 +  where "is_cap_letter c \<longleftrightarrow> (let n = nat_of_char c in 65 \<le> n \<and> n \<le> 90)" (*<*)
   4.482 +
   4.483 +(*>*) ML %quotetypewriter \<open>
   4.484 +  val check_char = @{computation_check terms:
   4.485 +    Trueprop is_cap_letter
   4.486 +    Char datatypes: num
   4.487 +  }
   4.488 +\<close>
   4.489 +
   4.490 +ML_val %quotetypewriter \<open>
   4.491 +  check_char @{context} @{cprop "is_cap_letter (CHR ''Y'')"}
   4.492 +\<close>
   4.493 +
   4.494 +  
   4.495 +subsubsection \<open>Preprocessing HOL terms into evaluable shape\<close>
   4.496 +
   4.497 +text \<open>
   4.498 +  When integrating decision procedures developed inside HOL into HOL itself,
   4.499 +  a common approach is to use a deep embedding where operators etc.
   4.500 +  are represented by datatypes in Isabelle/HOL.  Then it is necessary
   4.501 +  to turn generic shallowly embedded statements into that particular
   4.502 +  deep embedding (\qt{reification}).
   4.503 +
   4.504 +  One option is to hardcode using code antiquotations (see \secref{sec:code_antiq}).
   4.505 +  Another option is to use pre-existing infrastructure in HOL:
   4.506 +  @{ML "Reification.conv"} and @{ML "Reification.tac"}.
   4.507 +
   4.508 +  A simplistic example:
   4.509 +\<close>
   4.510 +
   4.511 +datatype %quote form_ord = T | F | Less nat nat
   4.512 +  | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
   4.513 +
   4.514 +primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
   4.515 +where
   4.516 +  "interp T vs \<longleftrightarrow> True"
   4.517 +| "interp F vs \<longleftrightarrow> False"
   4.518 +| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
   4.519 +| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
   4.520 +| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
   4.521 +| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
   4.522 +
   4.523 +text \<open>
   4.524 +  \noindent The datatype @{type form_ord} represents formulae whose semantics is given by
   4.525 +  @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   4.526 +  whose concrete values are given in list @{term vs}.
   4.527 +\<close>
   4.528 +
   4.529 +ML %quotetypewriter (*<*) \<open>\<close>
   4.530 +lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> interp (And (Less (Suc 0) (Suc (Suc 0))) (Less (Suc 0) 0)) [z, x, y]"
   4.531 +ML_prf %quotetypewriter
   4.532 +(*>*) \<open>val thm =
   4.533 +  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
   4.534 +by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
   4.535 +(*>*) 
   4.536 +
   4.537 +text \<open>
   4.538 +  \noindent By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   4.539 +  which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   4.540 +  to @{const interp} does not contain any free variables and can thus be evaluated
   4.541 +  using evaluation.
   4.542 +
   4.543 +  A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   4.544 +  theory @{text Regexp_Method}.
   4.545 +\<close>
   4.546 +
   4.547 +end
     5.1 --- a/src/Doc/Codegen/Evaluation.thy	Wed Feb 22 16:21:26 2017 +0000
     5.2 +++ b/src/Doc/Codegen/Evaluation.thy	Wed Feb 22 20:24:50 2017 +0100
     5.3 @@ -22,14 +22,14 @@
     5.4  subsection \<open>Evaluation techniques\<close>
     5.5  
     5.6  text \<open>
     5.7 -  The existing infrastructure provides a rich palette of evaluation
     5.8 +  There is a rich palette of evaluation
     5.9    techniques, each comprising different aspects:
    5.10  
    5.11    \begin{description}
    5.12  
    5.13 -    \item[Expressiveness.]  Depending on how good symbolic computation
    5.14 -      is supported, the class of terms which can be evaluated may be
    5.15 -      bigger or smaller.
    5.16 +    \item[Expressiveness.]  Depending on the extent to which symbolic
    5.17 +      computation is possible, the class of terms which can be evaluated
    5.18 +      can be bigger or smaller.
    5.19  
    5.20      \item[Efficiency.]  The more machine-near the technique, the
    5.21        faster it is.
    5.22 @@ -67,27 +67,26 @@
    5.23  subsubsection \<open>Evaluation in ML (@{text code})\<close>
    5.24  
    5.25  text \<open>
    5.26 -  Highest performance can be achieved by evaluation in ML, at the cost
    5.27 +  Considerable performance can be achieved using evaluation in ML, at the cost
    5.28    of being restricted to ground results and a layered stack of code to
    5.29 -  be trusted, including code generator configurations by the user.
    5.30 +  be trusted, including a user's specific code generator setup.
    5.31  
    5.32    Evaluation is carried out in a target language \emph{Eval} which
    5.33    inherits from \emph{SML} but for convenience uses parts of the
    5.34 -  Isabelle runtime environment.  The soundness of computation carried
    5.35 -  out there depends crucially on the correctness of the code
    5.36 -  generator setup; this is one of the reasons why you should not use
    5.37 -  adaptation (see \secref{sec:adaptation}) frivolously.
    5.38 +  Isabelle runtime environment.  Hence soundness depends crucially
    5.39 +  on the correctness of the code generator setup; this is one of the
    5.40 +  reasons why you should not use adaptation (see \secref{sec:adaptation})
    5.41 +  frivolously.
    5.42  \<close>
    5.43  
    5.44  
    5.45 -subsection \<open>Aspects of evaluation\<close>
    5.46 +subsection \<open>Dynamic evaluation\<close>
    5.47  
    5.48  text \<open>
    5.49 -  Each of the techniques can be combined with different aspects.  The
    5.50 -  most important distinction is between dynamic and static evaluation.
    5.51    Dynamic evaluation takes the code generator configuration \qt{as it
    5.52 -  is} at the point where evaluation is issued.  Best example is the
    5.53 -  @{command_def value} command which allows ad-hoc evaluation of
    5.54 +  is} at the point where evaluation is issued and computes
    5.55 +  a corresponding result.  Best example is the
    5.56 +  @{command_def value} command for ad-hoc evaluation of
    5.57    terms:
    5.58  \<close>
    5.59  
    5.60 @@ -103,257 +102,103 @@
    5.61  value %quote [nbe] "42 / (12 :: rat)"
    5.62  
    5.63  text \<open>
    5.64 -  To employ dynamic evaluation in the document generation, there is also
    5.65 +  To employ dynamic evaluation in documents, there is also
    5.66    a @{text value} antiquotation with the same evaluation techniques 
    5.67    as @{command value}.
    5.68 +\<close>
    5.69  
    5.70 -  Static evaluation freezes the code generator configuration at a
    5.71 -  certain point and uses this context whenever evaluation is issued
    5.72 -  later on.  This is particularly appropriate for proof procedures
    5.73 -  which use evaluation, since then the behaviour of evaluation is not
    5.74 -  changed or even compromised later on by actions of the user.
    5.75 +  
    5.76 +subsubsection \<open>Term reconstruction in ML\<close>
    5.77  
    5.78 -  As a technical complication, terms after evaluation in ML must be
    5.79 +text \<open>
    5.80 +  Results from evaluation in ML must be
    5.81    turned into Isabelle's internal term representation again.  Since
    5.82 -  this is also configurable, it is never fully trusted.  For this
    5.83 -  reason, evaluation in ML comes with further aspects:
    5.84 +  that setup is highly configurable, it is never assumed to be trustable. 
    5.85 +  Hence evaluation in ML provides no full term reconstruction
    5.86 +  but distinguishes the following kinds:
    5.87  
    5.88    \begin{description}
    5.89  
    5.90 -    \item[Plain evaluation.]  A term is normalized using the provided
    5.91 -      term reconstruction from ML to Isabelle; for applications which
    5.92 -      do not need to be fully trusted.
    5.93 +    \item[Plain evaluation.]  A term is normalized using the vanilla
    5.94 +      term reconstruction from ML to Isabelle; this is a pragmatic
    5.95 +      approach for applications which do not need trustability.
    5.96  
    5.97      \item[Property conversion.]  Evaluates propositions; since these
    5.98        are monomorphic, the term reconstruction is fixed once and for all
    5.99 -      and therefore trustable.
   5.100 -
   5.101 -    \item[Conversion.]  Evaluates an arbitrary term @{term "t"} first
   5.102 -      by plain evaluation and certifies the result @{term "t'"} by
   5.103 -      checking the equation @{term "t \<equiv> t'"} using property
   5.104 -      conversion.
   5.105 +      and therefore trustable -- in the sense that only the regular
   5.106 +      code generator setup has to be trusted, without relying
   5.107 +      on term reconstruction from ML to Isabelle.
   5.108  
   5.109    \end{description}
   5.110  
   5.111 -  \noindent The picture is further complicated by the roles of
   5.112 -  exceptions.  Here three cases have to be distinguished:
   5.113 -
   5.114 -  \begin{itemize}
   5.115 -
   5.116 -    \item Evaluation of @{term t} terminates with a result @{term
   5.117 -      "t'"}.
   5.118 -
   5.119 -    \item Evaluation of @{term t} terminates which an exception
   5.120 -      indicating a pattern match failure or a non-implemented
   5.121 -      function.  As sketched in \secref{sec:partiality}, this can be
   5.122 -      interpreted as partiality.
   5.123 -     
   5.124 -    \item Evaluation raises any other kind of exception.
   5.125 -     
   5.126 -  \end{itemize}
   5.127 -
   5.128 -  \noindent For conversions, the first case yields the equation @{term
   5.129 -  "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
   5.130 -  Exceptions of the third kind are propagated to the user.
   5.131 -
   5.132 -  By default return values of plain evaluation are optional, yielding
   5.133 -  @{text "SOME t'"} in the first case, @{text "NONE"} in the
   5.134 -  second, and propagating the exception in the third case.  A strict
   5.135 -  variant of plain evaluation either yields @{text "t'"} or propagates
   5.136 -  any exception, a liberal variant captures any exception in a result
   5.137 -  of type @{text "Exn.result"}.
   5.138 -  
   5.139 -  For property conversion (which coincides with conversion except for
   5.140 -  evaluation in ML), methods are provided which solve a given goal by
   5.141 -  evaluation.
   5.142 +  \noindent The different degree of trustability is also manifest in the
   5.143 +  types of the corresponding ML functions: plain evaluation
   5.144 +  operates on uncertified terms, whereas property conversion
   5.145 +  operates on certified terms.
   5.146  \<close>
   5.147  
   5.148  
   5.149 -subsection \<open>Schematic overview\<close>
   5.150 +subsubsection \<open>The partiality principle \label{sec:partiality_principle}\<close>
   5.151 +
   5.152 +text \<open>
   5.153 +  During evaluation exceptions indicating a pattern
   5.154 +  match failure or a non-implemented function are treated specially:
   5.155 +  as sketched in \secref{sec:partiality}, such
   5.156 +  exceptions can be interpreted as partiality.  For plain evaluation,
   5.157 +  the result hence is optional; property conversion falls back
   5.158 +  to reflexivity in such cases.
   5.159 +\<close>
   5.160 +  
   5.161 +
   5.162 +subsubsection \<open>Schematic overview\<close>
   5.163  
   5.164  text \<open>
   5.165    \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
   5.166    \fontsize{9pt}{12pt}\selectfont
   5.167 -  \begin{tabular}{ll||c|c|c}
   5.168 -    & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
   5.169 -    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
   5.170 -      & interactive evaluation 
   5.171 -      & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
   5.172 -      \tabularnewline
   5.173 -    & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
   5.174 -    & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
   5.175 -    & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
   5.176 -    & conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
   5.177 -      & \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline
   5.178 -    \multirow{3}{1ex}{\rotatebox{90}{static}}
   5.179 -    & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
   5.180 -    & property conversion & &
   5.181 -      & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
   5.182 -    & conversion & \ttsize@{ML "Code_Simp.static_conv"}
   5.183 -      & \ttsize@{ML "Nbe.static_conv"}
   5.184 -      & \ttsize@{ML "Code_Evaluation.static_conv"}
   5.185 +  \begin{tabular}{l||c|c|c}
   5.186 +    & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
   5.187 +    interactive evaluation & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"} \tabularnewline
   5.188 +    plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline
   5.189 +    evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
   5.190 +    property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline
   5.191 +    conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
   5.192    \end{tabular}
   5.193  \<close>
   5.194  
   5.195 -text \<open>
   5.196 -  \noindent Note that @{ML Code_Evaluation.static_value} and
   5.197 -  @{ML Code_Evaluation.static_conv} require certain code equations to
   5.198 -  reconstruct Isabelle terms from results and certify results.  This is
   5.199 -  achieved as follows:
   5.200 -
   5.201 -  \<^enum> Identify which result types are expected.
   5.202 -
   5.203 -  \<^enum> Define an auxiliary operation which for each possible result type @{text \<tau>}
   5.204 -    contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\<tau> itself"}
   5.205 -    (for @{ML Code_Evaluation.static_value}) or
   5.206 -    a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\<tau> itself"}
   5.207 -    (for @{ML Code_Evaluation.static_conv}) respectively.
   5.208 -
   5.209 -  \<^enum> Include that auxiliary operation into the set of constants when generating
   5.210 -    the static conversion.
   5.211 -\<close>
   5.212 -
   5.213 -
   5.214 -subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
   5.215 -
   5.216 +  
   5.217 +subsection \<open>Static evaluation\<close>
   5.218 +  
   5.219  text \<open>
   5.220 -  When integrating decision procedures developed inside HOL into HOL itself,
   5.221 -  it is necessary to somehow get from the Isabelle/ML representation to
   5.222 -  the representation used by the decision procedure itself (``reification'').
   5.223 -  One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
   5.224 -  Another option is to use pre-existing infrastructure in HOL:
   5.225 -  @{ML "Reification.conv"} and @{ML "Reification.tac"}
   5.226 -
   5.227 -  A simplistic example:
   5.228 -\<close>
   5.229 -
   5.230 -datatype %quote form_ord = T | F | Less nat nat
   5.231 -  | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
   5.232 -
   5.233 -primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
   5.234 -where
   5.235 -  "interp T vs \<longleftrightarrow> True"
   5.236 -| "interp F vs \<longleftrightarrow> False"
   5.237 -| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
   5.238 -| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
   5.239 -| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
   5.240 -| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
   5.241 -
   5.242 -text \<open>
   5.243 -  The datatype @{type form_ord} represents formulae whose semantics is given by
   5.244 -  @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   5.245 -  whose concrete values are given in list @{term vs}.
   5.246 -\<close>
   5.247 -
   5.248 -ML (*<*) \<open>\<close>
   5.249 -schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
   5.250 -ML_prf 
   5.251 -(*>*) \<open>val thm =
   5.252 -  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
   5.253 -by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
   5.254 -(*>*) 
   5.255 -
   5.256 -text \<open>
   5.257 -  By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   5.258 -  which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   5.259 -  to @{const interp} does not contain any free variables and can thus be evaluated
   5.260 -  using evaluation.
   5.261 -
   5.262 -  A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   5.263 -  theory @{text Regexp_Method}.
   5.264 +  When implementing proof procedures using evaluation,
   5.265 +  in most cases the code generator setup is appropriate
   5.266 +  \qt{as it was} when the proof procedure was written in ML,
   5.267 +  not an arbitrary later potentially modified setup.  This is
   5.268 +  called static evaluation.
   5.269  \<close>
   5.270  
   5.271  
   5.272 -subsection \<open>Intimate connection between logic and system runtime\<close>
   5.273 -
   5.274 -text \<open>
   5.275 -  The toolbox of static evaluation conversions forms a reasonable base
   5.276 -  to interweave generated code and system tools.  However in some
   5.277 -  situations more direct interaction is desirable.
   5.278 -\<close>
   5.279 -
   5.280 -
   5.281 -subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close>
   5.282 -
   5.283 +subsubsection \<open>Static evaluation using @{text simp} and @{text nbe}\<close>
   5.284 +  
   5.285  text \<open>
   5.286 -  The @{text code} antiquotation allows to include constants from
   5.287 -  generated code directly into ML system code, as in the following toy
   5.288 -  example:
   5.289 -\<close>
   5.290 -
   5.291 -datatype %quote form = T | F | And form form | Or form form (*<*)
   5.292 -
   5.293 -(*>*) ML %quotett \<open>
   5.294 -  fun eval_form @{code T} = true
   5.295 -    | eval_form @{code F} = false
   5.296 -    | eval_form (@{code And} (p, q)) =
   5.297 -        eval_form p andalso eval_form q
   5.298 -    | eval_form (@{code Or} (p, q)) =
   5.299 -        eval_form p orelse eval_form q;
   5.300 -\<close>
   5.301 -
   5.302 -text \<open>
   5.303 -  \noindent @{text code} takes as argument the name of a constant;
   5.304 -  after the whole ML is read, the necessary code is generated
   5.305 -  transparently and the corresponding constant names are inserted.
   5.306 -  This technique also allows to use pattern matching on constructors
   5.307 -  stemming from compiled datatypes.  Note that the @{text code}
   5.308 -  antiquotation may not refer to constants which carry adaptations;
   5.309 -  here you have to refer to the corresponding adapted code directly.
   5.310 -
   5.311 -  For a less simplistic example, theory @{text Approximation} in
   5.312 -  the @{text Decision_Procs} session is a good reference.
   5.313 +  For @{text simp} and @{text nbe} static evaluation can be achieved using 
   5.314 +  @{ML Code_Simp.static_conv} and @{ML Nbe.static_conv}.
   5.315 +  Note that @{ML Nbe.static_conv} by its very nature
   5.316 +  requires an invocation of the ML compiler for every call,
   5.317 +  which can produce significant overhead.
   5.318  \<close>
   5.319  
   5.320  
   5.321 -subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close>
   5.322 -
   5.323 -text \<open>
   5.324 -  The @{text code} antiquoation is lightweight, but the generated code
   5.325 -  is only accessible while the ML section is processed.  Sometimes this
   5.326 -  is not appropriate, especially if the generated code contains datatype
   5.327 -  declarations which are shared with other parts of the system.  In these
   5.328 -  cases, @{command_def code_reflect} can be used:
   5.329 -\<close>
   5.330 -
   5.331 -code_reflect %quote Sum_Type
   5.332 -  datatypes sum = Inl | Inr
   5.333 -  functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
   5.334 +subsubsection \<open>Intimate connection between logic and system runtime\<close>
   5.335  
   5.336  text \<open>
   5.337 -  \noindent @{command_def code_reflect} takes a structure name and
   5.338 -  references to datatypes and functions; for these code is compiled
   5.339 -  into the named ML structure and the \emph{Eval} target is modified
   5.340 -  in a way that future code generation will reference these
   5.341 -  precompiled versions of the given datatypes and functions.  This
   5.342 -  also allows to refer to the referenced datatypes and functions from
   5.343 -  arbitrary ML code as well.
   5.344 -
   5.345 -  A typical example for @{command code_reflect} can be found in the
   5.346 -  @{theory Predicate} theory.
   5.347 +  Static evaluation for @{text eval} operates differently --
   5.348 +  the required generated code is inserted directly into an ML
   5.349 +  block using antiquotations.  The idea is that generated
   5.350 +  code performing static evaluation (called a \<^emph>\<open>computation\<close>)
   5.351 +  is compiled once and for all such that later calls do not
   5.352 +  require any invocation of the code generator or the ML
   5.353 +  compiler at all.  This topic deserved a dedicated chapter
   5.354 +  \secref{sec:computations}.
   5.355  \<close>
   5.356 -
   5.357 -
   5.358 -subsubsection \<open>Separate compilation -- @{text code_reflect}\<close>
   5.359 -
   5.360 -text \<open>
   5.361 -  For technical reasons it is sometimes necessary to separate
   5.362 -  generation and compilation of code which is supposed to be used in
   5.363 -  the system runtime.  For this @{command code_reflect} with an
   5.364 -  optional \<^theory_text>\<open>file\<close> argument can be used:
   5.365 -\<close>
   5.366 -
   5.367 -code_reflect %quote Rat
   5.368 -  datatypes rat
   5.369 -  functions Fract
   5.370 -    "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   5.371 -    "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   5.372 -  file "$ISABELLE_TMP/examples/rat.ML"
   5.373 -
   5.374 -text \<open>
   5.375 -  \noindent This merely generates the referenced code to the given
   5.376 -  file which can be included into the system runtime later on.
   5.377 -\<close>
   5.378 -
   5.379 +  
   5.380  end
   5.381 -
     6.1 --- a/src/Doc/Codegen/Further.thy	Wed Feb 22 16:21:26 2017 +0000
     6.2 +++ b/src/Doc/Codegen/Further.thy	Wed Feb 22 20:24:50 2017 +0100
     6.3 @@ -4,6 +4,57 @@
     6.4  
     6.5  section \<open>Further issues \label{sec:further}\<close>
     6.6  
     6.7 +subsection \<open>Incorporating generated code directly into the system runtime -- @{text code_reflect}\<close>
     6.8 +
     6.9 +subsubsection \<open>Static embedding of generated code into the system runtime\<close>
    6.10 +
    6.11 +text \<open>
    6.12 +  The @{ML_antiquotation code} antiquotation is lightweight, but the generated code
    6.13 +  is only accessible while the ML section is processed.  Sometimes this
    6.14 +  is not appropriate, especially if the generated code contains datatype
    6.15 +  declarations which are shared with other parts of the system.  In these
    6.16 +  cases, @{command_def code_reflect} can be used:
    6.17 +\<close>
    6.18 +
    6.19 +code_reflect %quote Sum_Type
    6.20 +  datatypes sum = Inl | Inr
    6.21 +  functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
    6.22 +
    6.23 +text \<open>
    6.24 +  \noindent @{command code_reflect} takes a structure name and
    6.25 +  references to datatypes and functions; for these code is compiled
    6.26 +  into the named ML structure and the \emph{Eval} target is modified
    6.27 +  in a way that future code generation will reference these
    6.28 +  precompiled versions of the given datatypes and functions.  This
    6.29 +  also allows to refer to the referenced datatypes and functions from
    6.30 +  arbitrary ML code as well.
    6.31 +
    6.32 +  A typical example for @{command code_reflect} can be found in the
    6.33 +  @{theory Predicate} theory.
    6.34 +\<close>
    6.35 +
    6.36 +
    6.37 +subsubsection \<open>Separate compilation\<close>
    6.38 +
    6.39 +text \<open>
    6.40 +  For technical reasons it is sometimes necessary to separate
    6.41 +  generation and compilation of code which is supposed to be used in
    6.42 +  the system runtime.  For this @{command code_reflect} with an
    6.43 +  optional \<^theory_text>\<open>file\<close> argument can be used:
    6.44 +\<close>
    6.45 +
    6.46 +code_reflect %quote Rat
    6.47 +  datatypes rat
    6.48 +  functions Fract
    6.49 +    "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
    6.50 +    "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
    6.51 +  file "$ISABELLE_TMP/examples/rat.ML"
    6.52 +
    6.53 +text \<open>
    6.54 +  \noindent This merely generates the referenced code to the given
    6.55 +  file which can be included into the system runtime later on.
    6.56 +\<close>
    6.57 +
    6.58  subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close>
    6.59  
    6.60  text \<open>
     7.1 --- a/src/Doc/Codegen/document/root.tex	Wed Feb 22 16:21:26 2017 +0000
     7.2 +++ b/src/Doc/Codegen/document/root.tex	Wed Feb 22 20:24:50 2017 +0100
     7.3 @@ -36,6 +36,7 @@
     7.4  \input{Refinement.tex}
     7.5  \input{Inductive_Predicate.tex}
     7.6  \input{Evaluation.tex}
     7.7 +\input{Computations.tex}
     7.8  \input{Adaptation.tex}
     7.9  \input{Further.tex}
    7.10  
     8.1 --- a/src/Doc/Codegen/document/style.sty	Wed Feb 22 16:21:26 2017 +0000
     8.2 +++ b/src/Doc/Codegen/document/style.sty	Wed Feb 22 20:24:50 2017 +0100
     8.3 @@ -18,6 +18,9 @@
     8.4  \newcommand{\qt}[1]{``{#1}''}
     8.5  \newcommand{\ditem}[1]{\item[\isastyletext #1]}
     8.6  
     8.7 +%% vectors
     8.8 +\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
     8.9 +
    8.10  %% quote environment
    8.11  \isakeeptag{quote}
    8.12  \renewenvironment{quote}
     9.1 --- a/src/Doc/ROOT	Wed Feb 22 16:21:26 2017 +0000
     9.2 +++ b/src/Doc/ROOT	Wed Feb 22 20:24:50 2017 +0100
     9.3 @@ -29,6 +29,7 @@
     9.4      Refinement
     9.5      Inductive_Predicate
     9.6      Evaluation
     9.7 +    Computations
     9.8      Adaptation
     9.9      Further
    9.10    document_files (in "..")