src/Doc/Codegen/Evaluation.thy
author haftmann
Mon Feb 06 20:56:34 2017 +0100 (2017-02-06)
changeset 64990 c6a7de505796
parent 63670 8e0148e1f5f4
child 65041 2525e680f94f
permissions -rw-r--r--
more explicit errors in pathological cases
haftmann@38510
     1
theory Evaluation
haftmann@38510
     2
imports Setup
haftmann@59378
     3
begin (*<*)
haftmann@59378
     4
haftmann@59378
     5
ML \<open>
haftmann@59378
     6
  Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
haftmann@59378
     7
\<close> (*>*)
haftmann@38510
     8
haftmann@59377
     9
section \<open>Evaluation \label{sec:evaluation}\<close>
haftmann@38510
    10
haftmann@59377
    11
text \<open>
haftmann@39599
    12
  Recalling \secref{sec:principle}, code generation turns a system of
haftmann@39599
    13
  equations into a program with the \emph{same} equational semantics.
haftmann@39599
    14
  As a consequence, this program can be used as a \emph{rewrite
haftmann@39599
    15
  engine} for terms: rewriting a term @{term "t"} using a program to a
haftmann@39599
    16
  term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}.  This
haftmann@39599
    17
  application of code generation in the following is referred to as
haftmann@39599
    18
  \emph{evaluation}.
haftmann@59377
    19
\<close>
haftmann@38510
    20
haftmann@38510
    21
haftmann@59377
    22
subsection \<open>Evaluation techniques\<close>
haftmann@38510
    23
haftmann@59377
    24
text \<open>
haftmann@40350
    25
  The existing infrastructure provides a rich palette of evaluation
haftmann@39599
    26
  techniques, each comprising different aspects:
haftmann@39599
    27
haftmann@39599
    28
  \begin{description}
haftmann@39599
    29
haftmann@39599
    30
    \item[Expressiveness.]  Depending on how good symbolic computation
haftmann@39599
    31
      is supported, the class of terms which can be evaluated may be
haftmann@39599
    32
      bigger or smaller.
haftmann@38510
    33
haftmann@39599
    34
    \item[Efficiency.]  The more machine-near the technique, the
haftmann@39599
    35
      faster it is.
haftmann@38510
    36
haftmann@39599
    37
    \item[Trustability.]  Techniques which a huge (and also probably
haftmann@39599
    38
      more configurable infrastructure) are more fragile and less
haftmann@39599
    39
      trustable.
haftmann@39599
    40
haftmann@39599
    41
  \end{description}
haftmann@59377
    42
\<close>
haftmann@38510
    43
haftmann@38510
    44
haftmann@59377
    45
subsubsection \<open>The simplifier (@{text simp})\<close>
haftmann@38510
    46
haftmann@59377
    47
text \<open>
haftmann@39599
    48
  The simplest way for evaluation is just using the simplifier with
haftmann@39599
    49
  the original code equations of the underlying program.  This gives
haftmann@39599
    50
  fully symbolic evaluation and highest trustablity, with the usual
haftmann@39599
    51
  performance of the simplifier.  Note that for operations on abstract
haftmann@39599
    52
  datatypes (cf.~\secref{sec:invariant}), the original theorems as
haftmann@39599
    53
  given by the users are used, not the modified ones.
haftmann@59377
    54
\<close>
haftmann@38510
    55
haftmann@38510
    56
haftmann@59377
    57
subsubsection \<open>Normalization by evaluation (@{text nbe})\<close>
haftmann@38510
    58
haftmann@59377
    59
text \<open>
wenzelm@58620
    60
  Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
haftmann@39599
    61
  provides a comparably fast partially symbolic evaluation which
haftmann@39599
    62
  permits also normalization of functions and uninterpreted symbols;
haftmann@39599
    63
  the stack of code to be trusted is considerable.
haftmann@59377
    64
\<close>
haftmann@38510
    65
haftmann@38510
    66
haftmann@59377
    67
subsubsection \<open>Evaluation in ML (@{text code})\<close>
haftmann@39599
    68
haftmann@59377
    69
text \<open>
haftmann@39599
    70
  Highest performance can be achieved by evaluation in ML, at the cost
haftmann@39599
    71
  of being restricted to ground results and a layered stack of code to
haftmann@39599
    72
  be trusted, including code generator configurations by the user.
haftmann@38510
    73
haftmann@39599
    74
  Evaluation is carried out in a target language \emph{Eval} which
haftmann@39599
    75
  inherits from \emph{SML} but for convenience uses parts of the
haftmann@39599
    76
  Isabelle runtime environment.  The soundness of computation carried
haftmann@39609
    77
  out there depends crucially on the correctness of the code
haftmann@39643
    78
  generator setup; this is one of the reasons why you should not use
haftmann@39609
    79
  adaptation (see \secref{sec:adaptation}) frivolously.
haftmann@59377
    80
\<close>
haftmann@38510
    81
haftmann@38510
    82
haftmann@59377
    83
subsection \<open>Aspects of evaluation\<close>
haftmann@38510
    84
haftmann@59377
    85
text \<open>
haftmann@39599
    86
  Each of the techniques can be combined with different aspects.  The
haftmann@39599
    87
  most important distinction is between dynamic and static evaluation.
haftmann@39599
    88
  Dynamic evaluation takes the code generator configuration \qt{as it
haftmann@39599
    89
  is} at the point where evaluation is issued.  Best example is the
haftmann@39599
    90
  @{command_def value} command which allows ad-hoc evaluation of
haftmann@39599
    91
  terms:
haftmann@59377
    92
\<close>
haftmann@38510
    93
haftmann@38510
    94
value %quote "42 / (12 :: rat)"
haftmann@38510
    95
haftmann@59377
    96
text \<open>
haftmann@56927
    97
  \noindent @{command value} tries first to evaluate using ML, falling
haftmann@56927
    98
  back to normalization by evaluation if this fails.
haftmann@38510
    99
haftmann@58100
   100
  A particular technique may be specified in square brackets, e.g.
haftmann@59377
   101
\<close>
haftmann@58100
   102
haftmann@58100
   103
value %quote [nbe] "42 / (12 :: rat)"
haftmann@58100
   104
haftmann@59377
   105
text \<open>
bulwahn@43656
   106
  To employ dynamic evaluation in the document generation, there is also
haftmann@56927
   107
  a @{text value} antiquotation with the same evaluation techniques 
haftmann@56927
   108
  as @{command value}.
bulwahn@43656
   109
haftmann@39599
   110
  Static evaluation freezes the code generator configuration at a
haftmann@39599
   111
  certain point and uses this context whenever evaluation is issued
haftmann@39599
   112
  later on.  This is particularly appropriate for proof procedures
haftmann@39599
   113
  which use evaluation, since then the behaviour of evaluation is not
haftmann@39599
   114
  changed or even compromised later on by actions of the user.
haftmann@39599
   115
haftmann@39599
   116
  As a technical complication, terms after evaluation in ML must be
haftmann@39599
   117
  turned into Isabelle's internal term representation again.  Since
haftmann@39599
   118
  this is also configurable, it is never fully trusted.  For this
haftmann@39599
   119
  reason, evaluation in ML comes with further aspects:
haftmann@39599
   120
haftmann@39599
   121
  \begin{description}
haftmann@39599
   122
haftmann@39599
   123
    \item[Plain evaluation.]  A term is normalized using the provided
haftmann@39599
   124
      term reconstruction from ML to Isabelle; for applications which
haftmann@39599
   125
      do not need to be fully trusted.
haftmann@39599
   126
haftmann@39599
   127
    \item[Property conversion.]  Evaluates propositions; since these
haftmann@39599
   128
      are monomorphic, the term reconstruction is fixed once and for all
haftmann@39599
   129
      and therefore trustable.
haftmann@39599
   130
haftmann@39599
   131
    \item[Conversion.]  Evaluates an arbitrary term @{term "t"} first
haftmann@39599
   132
      by plain evaluation and certifies the result @{term "t'"} by
haftmann@39599
   133
      checking the equation @{term "t \<equiv> t'"} using property
haftmann@39599
   134
      conversion.
haftmann@39599
   135
haftmann@39599
   136
  \end{description}
haftmann@39599
   137
haftmann@39599
   138
  \noindent The picture is further complicated by the roles of
haftmann@39599
   139
  exceptions.  Here three cases have to be distinguished:
haftmann@39599
   140
haftmann@39599
   141
  \begin{itemize}
haftmann@39599
   142
haftmann@39599
   143
    \item Evaluation of @{term t} terminates with a result @{term
haftmann@39599
   144
      "t'"}.
haftmann@39599
   145
haftmann@63161
   146
    \item Evaluation of @{term t} terminates which an exception
haftmann@40350
   147
      indicating a pattern match failure or a non-implemented
haftmann@39599
   148
      function.  As sketched in \secref{sec:partiality}, this can be
haftmann@39599
   149
      interpreted as partiality.
haftmann@39599
   150
     
haftmann@39643
   151
    \item Evaluation raises any other kind of exception.
haftmann@39599
   152
     
haftmann@39599
   153
  \end{itemize}
haftmann@39599
   154
haftmann@39599
   155
  \noindent For conversions, the first case yields the equation @{term
haftmann@39599
   156
  "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
haftmann@39643
   157
  Exceptions of the third kind are propagated to the user.
haftmann@39599
   158
haftmann@39599
   159
  By default return values of plain evaluation are optional, yielding
haftmann@40350
   160
  @{text "SOME t'"} in the first case, @{text "NONE"} in the
haftmann@40350
   161
  second, and propagating the exception in the third case.  A strict
haftmann@39599
   162
  variant of plain evaluation either yields @{text "t'"} or propagates
haftmann@51713
   163
  any exception, a liberal variant captures any exception in a result
haftmann@39599
   164
  of type @{text "Exn.result"}.
haftmann@39599
   165
  
haftmann@39599
   166
  For property conversion (which coincides with conversion except for
haftmann@39599
   167
  evaluation in ML), methods are provided which solve a given goal by
haftmann@39599
   168
  evaluation.
haftmann@59377
   169
\<close>
haftmann@38510
   170
haftmann@38510
   171
haftmann@59377
   172
subsection \<open>Schematic overview\<close>
haftmann@39599
   173
haftmann@59377
   174
text \<open>
haftmann@39693
   175
  \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
haftmann@39693
   176
  \fontsize{9pt}{12pt}\selectfont
haftmann@39599
   177
  \begin{tabular}{ll||c|c|c}
haftmann@39599
   178
    & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
haftmann@58100
   179
    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
haftmann@58100
   180
      & interactive evaluation 
haftmann@58100
   181
      & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
haftmann@58100
   182
      \tabularnewline
haftmann@39693
   183
    & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
haftmann@39599
   184
    & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
haftmann@39693
   185
    & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
haftmann@41184
   186
    & conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
haftmann@41184
   187
      & \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline
haftmann@39693
   188
    \multirow{3}{1ex}{\rotatebox{90}{static}}
haftmann@41184
   189
    & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
haftmann@39599
   190
    & property conversion & &
haftmann@39693
   191
      & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
haftmann@41184
   192
    & conversion & \ttsize@{ML "Code_Simp.static_conv"}
haftmann@41184
   193
      & \ttsize@{ML "Nbe.static_conv"}
haftmann@41184
   194
      & \ttsize@{ML "Code_Evaluation.static_conv"}
haftmann@39599
   195
  \end{tabular}
haftmann@59377
   196
\<close>
haftmann@39599
   197
haftmann@63161
   198
text \<open>
haftmann@63161
   199
  \noindent Note that @{ML Code_Evaluation.static_value} and
haftmann@63161
   200
  @{ML Code_Evaluation.static_conv} require certain code equations to
haftmann@63161
   201
  reconstruct Isabelle terms from results and certify results.  This is
haftmann@63161
   202
  achieved as follows:
haftmann@63161
   203
haftmann@63161
   204
  \<^enum> Identify which result types are expected.
haftmann@63161
   205
haftmann@63161
   206
  \<^enum> Define an auxiliary operation which for each possible result type @{text \<tau>}
haftmann@63161
   207
    contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\<tau> itself"}
haftmann@63161
   208
    (for @{ML Code_Evaluation.static_value}) or
haftmann@63161
   209
    a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\<tau> itself"}
haftmann@63161
   210
    (for @{ML Code_Evaluation.static_conv}) respectively.
haftmann@63161
   211
haftmann@63161
   212
  \<^enum> Include that auxiliary operation into the set of constants when generating
haftmann@63161
   213
    the static conversion.
haftmann@63161
   214
\<close>
haftmann@63161
   215
haftmann@39599
   216
haftmann@59377
   217
subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
haftmann@52287
   218
haftmann@59377
   219
text \<open>
haftmann@63161
   220
  When integrating decision procedures developed inside HOL into HOL itself,
haftmann@52287
   221
  it is necessary to somehow get from the Isabelle/ML representation to
haftmann@52287
   222
  the representation used by the decision procedure itself (``reification'').
haftmann@52287
   223
  One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
haftmann@52287
   224
  Another option is to use pre-existing infrastructure in HOL:
haftmann@52287
   225
  @{ML "Reification.conv"} and @{ML "Reification.tac"}
haftmann@52287
   226
haftmann@63161
   227
  A simplistic example:
haftmann@59377
   228
\<close>
haftmann@52287
   229
blanchet@58310
   230
datatype %quote form_ord = T | F | Less nat nat
haftmann@52287
   231
  | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
haftmann@52287
   232
haftmann@52287
   233
primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
haftmann@52287
   234
where
haftmann@52287
   235
  "interp T vs \<longleftrightarrow> True"
haftmann@52287
   236
| "interp F vs \<longleftrightarrow> False"
haftmann@52287
   237
| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
haftmann@52287
   238
| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
haftmann@52287
   239
| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
haftmann@52287
   240
| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
haftmann@52287
   241
haftmann@59377
   242
text \<open>
haftmann@52287
   243
  The datatype @{type form_ord} represents formulae whose semantics is given by
haftmann@52287
   244
  @{const interp}.  Note that values are represented by variable indices (@{typ nat})
haftmann@52287
   245
  whose concrete values are given in list @{term vs}.
haftmann@59377
   246
\<close>
haftmann@52287
   247
haftmann@59377
   248
ML (*<*) \<open>\<close>
wenzelm@61337
   249
schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
haftmann@52287
   250
ML_prf 
haftmann@59377
   251
(*>*) \<open>val thm =
haftmann@59377
   252
  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
wenzelm@60754
   253
by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
haftmann@52287
   254
(*>*) 
haftmann@52287
   255
haftmann@59377
   256
text \<open>
haftmann@52287
   257
  By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
haftmann@52287
   258
  which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
haftmann@59335
   259
  to @{const interp} does not contain any free variables and can thus be evaluated
haftmann@52287
   260
  using evaluation.
haftmann@52287
   261
haftmann@52287
   262
  A less meager example can be found in the AFP, session @{text "Regular-Sets"},
haftmann@52287
   263
  theory @{text Regexp_Method}.
haftmann@59377
   264
\<close>
haftmann@52287
   265
haftmann@52287
   266
haftmann@59377
   267
subsection \<open>Intimate connection between logic and system runtime\<close>
haftmann@39599
   268
haftmann@59377
   269
text \<open>
haftmann@39609
   270
  The toolbox of static evaluation conversions forms a reasonable base
haftmann@39609
   271
  to interweave generated code and system tools.  However in some
haftmann@39609
   272
  situations more direct interaction is desirable.
haftmann@59377
   273
\<close>
haftmann@39599
   274
haftmann@39599
   275
haftmann@59377
   276
subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close>
haftmann@39599
   277
haftmann@59377
   278
text \<open>
haftmann@39609
   279
  The @{text code} antiquotation allows to include constants from
haftmann@39609
   280
  generated code directly into ML system code, as in the following toy
haftmann@39609
   281
  example:
haftmann@59377
   282
\<close>
haftmann@38510
   283
blanchet@58310
   284
datatype %quote form = T | F | And form form | Or form form (*<*)
haftmann@38510
   285
haftmann@59377
   286
(*>*) ML %quotett \<open>
haftmann@38510
   287
  fun eval_form @{code T} = true
haftmann@38510
   288
    | eval_form @{code F} = false
haftmann@38510
   289
    | eval_form (@{code And} (p, q)) =
haftmann@38510
   290
        eval_form p andalso eval_form q
haftmann@38510
   291
    | eval_form (@{code Or} (p, q)) =
haftmann@38510
   292
        eval_form p orelse eval_form q;
haftmann@59377
   293
\<close>
haftmann@38510
   294
haftmann@59377
   295
text \<open>
haftmann@39609
   296
  \noindent @{text code} takes as argument the name of a constant;
haftmann@39609
   297
  after the whole ML is read, the necessary code is generated
haftmann@39609
   298
  transparently and the corresponding constant names are inserted.
haftmann@39609
   299
  This technique also allows to use pattern matching on constructors
haftmann@39643
   300
  stemming from compiled datatypes.  Note that the @{text code}
haftmann@39643
   301
  antiquotation may not refer to constants which carry adaptations;
haftmann@39643
   302
  here you have to refer to the corresponding adapted code directly.
haftmann@38510
   303
haftmann@39609
   304
  For a less simplistic example, theory @{text Approximation} in
haftmann@39609
   305
  the @{text Decision_Procs} session is a good reference.
haftmann@59377
   306
\<close>
haftmann@38510
   307
haftmann@38510
   308
haftmann@59377
   309
subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close>
haftmann@39599
   310
haftmann@59377
   311
text \<open>
haftmann@39609
   312
  The @{text code} antiquoation is lightweight, but the generated code
haftmann@39609
   313
  is only accessible while the ML section is processed.  Sometimes this
haftmann@39609
   314
  is not appropriate, especially if the generated code contains datatype
haftmann@39609
   315
  declarations which are shared with other parts of the system.  In these
haftmann@39609
   316
  cases, @{command_def code_reflect} can be used:
haftmann@59377
   317
\<close>
haftmann@39609
   318
haftmann@39609
   319
code_reflect %quote Sum_Type
haftmann@39609
   320
  datatypes sum = Inl | Inr
blanchet@55418
   321
  functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
haftmann@39609
   322
haftmann@59377
   323
text \<open>
haftmann@39609
   324
  \noindent @{command_def code_reflect} takes a structure name and
haftmann@39609
   325
  references to datatypes and functions; for these code is compiled
haftmann@39609
   326
  into the named ML structure and the \emph{Eval} target is modified
haftmann@39609
   327
  in a way that future code generation will reference these
haftmann@39609
   328
  precompiled versions of the given datatypes and functions.  This
haftmann@39609
   329
  also allows to refer to the referenced datatypes and functions from
haftmann@39609
   330
  arbitrary ML code as well.
haftmann@39609
   331
haftmann@39609
   332
  A typical example for @{command code_reflect} can be found in the
haftmann@39609
   333
  @{theory Predicate} theory.
haftmann@59377
   334
\<close>
haftmann@39609
   335
haftmann@39599
   336
haftmann@59377
   337
subsubsection \<open>Separate compilation -- @{text code_reflect}\<close>
haftmann@39599
   338
haftmann@59377
   339
text \<open>
haftmann@39609
   340
  For technical reasons it is sometimes necessary to separate
haftmann@39609
   341
  generation and compilation of code which is supposed to be used in
haftmann@39609
   342
  the system runtime.  For this @{command code_reflect} with an
wenzelm@63670
   343
  optional \<^theory_text>\<open>file\<close> argument can be used:
haftmann@59377
   344
\<close>
haftmann@39609
   345
haftmann@39609
   346
code_reflect %quote Rat
haftmann@63175
   347
  datatypes rat
haftmann@39609
   348
  functions Fract
haftmann@39609
   349
    "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
haftmann@39609
   350
    "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
haftmann@59334
   351
  file "$ISABELLE_TMP/examples/rat.ML"
haftmann@39609
   352
haftmann@59377
   353
text \<open>
haftmann@39643
   354
  \noindent This merely generates the referenced code to the given
haftmann@39609
   355
  file which can be included into the system runtime later on.
haftmann@59377
   356
\<close>
haftmann@39599
   357
haftmann@38510
   358
end
haftmann@46522
   359