# HG changeset patch # User haftmann # Date 1282123103 -7200 # Node ID ec0408c7328b4befc62049f7b718bc9367748f2d # Parent 9cea8a0e925a4571afc99139e7b6acfb340a05bd stub for evaluation chapter diff -r 9cea8a0e925a -r ec0408c7328b 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 diff -r 9cea8a0e925a -r ec0408c7328b doc-src/Codegen/Thy/Further.thy --- 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 *} diff -r 9cea8a0e925a -r ec0408c7328b doc-src/Codegen/Thy/ROOT.ML --- 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"; diff -r 9cea8a0e925a -r ec0408c7328b doc-src/Codegen/Thy/document/Further.tex --- 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% diff -r 9cea8a0e925a -r ec0408c7328b doc-src/Codegen/codegen.tex --- 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