doc-src/Codegen/Thy/Evaluation.thy

set depth to 1

theory Evaluation
imports Setup
begin

section {* Evaluation *}

text {* Introduction *}


subsection {* Evaluation techniques *}

text {* simplifier *}

text {* nbe *}

text {* eval target: SML standalone vs. Isabelle/SML, example, soundness *}


subsection {* Dynamic evaluation *}

text {* value (three variants) *}

text {* methods (three variants) *}

text {* corresponding ML interfaces *}


subsection {* Static evaluation *}

text {* code_simp, nbe (tbd), Eval (tbd, in simple fashion) *}

text {* hand-written: code antiquotation *}


subsection {* Hybrid techniques *}

text {* code reflect runtime *}

text {* code reflect external *}


text {* FIXME here the old sections follow *}

subsection {* Evaluation oracle *}

text {*
  Code generation may also be used to \emph{evaluate} expressions
  (using @{text SML} as target language of course).
  For instance, the @{command_def value} reduces an expression to a
  normal form with respect to the underlying code equations:
*}

value %quote "42 / (12 :: rat)"

text {*
  \noindent will display @{term "7 / (2 :: rat)"}.

  The @{method eval} method tries to reduce a goal by code generation to @{term True}
  and solves it in that case, but fails otherwise:
*}

lemma %quote "42 / (12 :: rat) = 7 / 2"
  by %quote eval

text {*
  \noindent The soundness of the @{method eval} method depends crucially 
  on the correctness of the code generator;  this is one of the reasons
  why you should not use adaptation (see \secref{sec:adaptation}) frivolously.
*}


subsubsection {* Code antiquotation *}

text {*
  In scenarios involving techniques like reflection it is quite common
  that code generated from a theory forms the basis for implementing
  a proof procedure in @{text SML}.  To facilitate interfacing of generated code
  with system code, the code generator provides a @{text code} antiquotation:
*}

datatype %quote form = T | F | And form form | Or form form (*<*)

(*>*) ML %quotett {*
  fun eval_form @{code T} = true
    | eval_form @{code F} = false
    | eval_form (@{code And} (p, q)) =
        eval_form p andalso eval_form q
    | eval_form (@{code Or} (p, q)) =
        eval_form p orelse eval_form q;
*}

text {*
  \noindent @{text code} takes as argument the name of a constant;  after the
  whole @{text SML} is read, the necessary code is generated transparently
  and the corresponding constant names are inserted.  This technique also
  allows to use pattern matching on constructors stemming from compiled
  @{text "datatypes"}.

  For a less simplistic example, theory @{theory Ferrack} is
  a good reference.
*}


end