doc-src/Codegen/Thy/Evaluation.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/Evaluation.thy	Wed Aug 18 11:18:23 2010 +0200
@@ -0,0 +1,104 @@
+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