stub for evaluation chapter

--- /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

--- a/doc-src/Codegen/Thy/Further.thy	Wed Aug 18 10:07:57 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Wed Aug 18 11:18:23 2010 +0200
@@ -126,85 +126,20 @@
 *}
 
 
-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.
-*}
-
-
-subsection {* Building evaluators *}
-
-text {*
-  FIXME
-*}
-
-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.
-*}
-
-
 subsection {* ML system interfaces \label{sec:ml} *}
 
 text {*
-  Since the code generator framework not only aims to provide
-  a nice Isar interface but also to form a base for
-  code-generation-based applications, here a short
-  description of the most important ML interfaces.
+  Since the code generator framework not only aims to provide a nice
+  Isar interface but also to form a base for code-generation-based
+  applications, here a short description of the most fundamental ML
+  interfaces.
 *}
 
 subsubsection {* Managing executable content *}
 
 text %mlref {*
   \begin{mldecls}
+  @{index_ML Code.read_const: "theory -> string -> string"} \\
   @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
   @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
   @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
@@ -221,6 +156,9 @@
 
   \begin{description}
 
+  \item @{ML Code.read_const}~@{text thy}~@{text s}
+     reads a constant as a concrete term expression @{text s}.
+
   \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
      theorem @{text "thm"} to executable content.
 
@@ -253,21 +191,6 @@
   \end{description}
 *}
 
-subsubsection {* Auxiliary *}
-
-text %mlref {*
-  \begin{mldecls}
-  @{index_ML Code.read_const: "theory -> string -> string"}
-  \end{mldecls}
-
-  \begin{description}
-
-  \item @{ML Code.read_const}~@{text thy}~@{text s}
-     reads a constant as a concrete term expression @{text s}.
-
-  \end{description}
-
-*}
 
 subsubsection {* Data depending on the theory's executable content *}
 

--- a/doc-src/Codegen/Thy/ROOT.ML	Wed Aug 18 10:07:57 2010 +0200
+++ b/doc-src/Codegen/Thy/ROOT.ML	Wed Aug 18 11:18:23 2010 +0200
@@ -5,5 +5,6 @@
 use_thy "Foundations";
 use_thy "Refinement";
 use_thy "Inductive_Predicate";
+use_thy "Evaluation";
 use_thy "Adaptation";
 use_thy "Further";

--- a/doc-src/Codegen/Thy/document/Further.tex	Wed Aug 18 10:07:57 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Wed Aug 18 11:18:23 2010 +0200
@@ -246,156 +246,15 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Evaluation oracle%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Code generation may also be used to \emph{evaluate} expressions
-  (using \isa{SML} as target language of course).
-  For instance, the \indexdef{}{command}{value}\hypertarget{command.value}{\hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}}} reduces an expression to a
-  normal form with respect to the underlying code equations:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{value}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent will display \isa{{\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}}.
-
-  The \hyperlink{method.eval}{\mbox{\isa{eval}}} method tries to reduce a goal by code generation to \isa{True}
-  and solves it in that case, but fails otherwise:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}\ {\isacharequal}\ {\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ eval%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The soundness of the \hyperlink{method.eval}{\mbox{\isa{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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Building evaluators%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Code antiquotation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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 \isa{SML}.  To facilitate interfacing of generated code
-  with system code, the code generator provides a \isa{code} antiquotation:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadelimquotett
-\ %
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\isanewline
-\ \ fun\ eval{\isacharunderscore}form\ %
-\isaantiq
-code\ T%
-\endisaantiq
-\ {\isacharequal}\ true\isanewline
-\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ %
-\isaantiq
-code\ F%
-\endisaantiq
-\ {\isacharequal}\ false\isanewline
-\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
-\isaantiq
-code\ And%
-\endisaantiq
-\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ andalso\ eval{\isacharunderscore}form\ q\isanewline
-\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
-\isaantiq
-code\ Or%
-\endisaantiq
-\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
-{\isacharverbatimclose}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent \isa{code} takes as argument the name of a constant;  after the
-  whole \isa{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
-  \isa{datatypes}.
-
-  For a less simplistic example, theory \hyperlink{theory.Ferrack}{\mbox{\isa{Ferrack}}} is
-  a good reference.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsubsection{ML system interfaces \label{sec:ml}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Since the code generator framework not only aims to provide
-  a nice Isar interface but also to form a base for
-  code-generation-based applications, here a short
-  description of the most important ML interfaces.%
+Since the code generator framework not only aims to provide a nice
+  Isar interface but also to form a base for code-generation-based
+  applications, here a short description of the most fundamental ML
+  interfaces.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -411,6 +270,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
+  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
   \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
   \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
   \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
@@ -427,6 +287,9 @@
 
   \begin{description}
 
+  \item \verb|Code.read_const|~\isa{thy}~\isa{s}
+     reads a constant as a concrete term expression \isa{s}.
+
   \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
      theorem \isa{thm} to executable content.
 
@@ -467,37 +330,6 @@
 %
 \endisadelimmlref
 %
-\isamarkupsubsubsection{Auxiliary%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
-  \end{mldecls}
-
-  \begin{description}
-
-  \item \verb|Code.read_const|~\isa{thy}~\isa{s}
-     reads a constant as a concrete term expression \isa{s}.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
 \isamarkupsubsubsection{Data depending on the theory's executable content%
 }
 \isamarkuptrue%

--- a/doc-src/Codegen/codegen.tex	Wed Aug 18 10:07:57 2010 +0200
+++ b/doc-src/Codegen/codegen.tex	Wed Aug 18 11:18:23 2010 +0200
@@ -35,6 +35,7 @@
 \input{Thy/document/Refinement.tex}
 \input{Thy/document/Inductive_Predicate.tex}
 \input{Thy/document/Adaptation.tex}
+\input{Thy/document/Evaluation.tex}
 \input{Thy/document/Further.tex}
 
 \begingroup