--- a/doc-src/Codegen/IsaMakefile Wed Sep 22 16:17:20 2010 +0200
+++ b/doc-src/Codegen/IsaMakefile Wed Sep 22 16:24:41 2010 +0200
@@ -26,7 +26,7 @@
$(THY): Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
@$(USEDIR) -m no_brackets -m iff HOL-Library Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
- Thy/document/pdfsetup.sty Thy/document/session.tex
+ Thy/document/pdfsetup.sty Thy/document/session.tex
## clean
--- a/doc-src/Codegen/Thy/Evaluation.thy Wed Sep 22 16:17:20 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy Wed Sep 22 16:24:41 2010 +0200
@@ -4,78 +4,202 @@
section {* Evaluation *}
-text {* Introduction *}
+text {*
+ Recalling \secref{sec:principle}, code generation turns a system of
+ equations into a program with the \emph{same} equational semantics.
+ As a consequence, this program can be used as a \emph{rewrite
+ engine} for terms: rewriting a term @{term "t"} using a program to a
+ term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}. This
+ application of code generation in the following is referred to as
+ \emph{evaluation}.
+*}
subsection {* Evaluation techniques *}
-text {* simplifier *}
+text {*
+ The existing infrastructure provides a rich palett of evaluation
+ techniques, each comprising different aspects:
+
+ \begin{description}
+
+ \item[Expressiveness.] Depending on how good symbolic computation
+ is supported, the class of terms which can be evaluated may be
+ bigger or smaller.
-text {* nbe *}
+ \item[Efficiency.] The more machine-near the technique, the
+ faster it is.
-text {* eval target: SML standalone vs. Isabelle/SML, example, soundness *}
+ \item[Trustability.] Techniques which a huge (and also probably
+ more configurable infrastructure) are more fragile and less
+ trustable.
+
+ \end{description}
+*}
-subsection {* Dynamic evaluation *}
-
-text {* value (three variants) *}
+subsubsection {* The simplifier (@{text simp}) *}
-text {* methods (three variants) *}
-
-text {* corresponding ML interfaces *}
+text {*
+ The simplest way for evaluation is just using the simplifier with
+ the original code equations of the underlying program. This gives
+ fully symbolic evaluation and highest trustablity, with the usual
+ performance of the simplifier. Note that for operations on abstract
+ datatypes (cf.~\secref{sec:invariant}), the original theorems as
+ given by the users are used, not the modified ones.
+*}
-subsection {* Static evaluation *}
+subsubsection {* Normalization by evaluation (@{text nbe}) *}
-text {* code_simp, nbe (tbd), Eval (tbd, in simple fashion) *}
-
-text {* hand-written: code antiquotation *}
+text {*
+ Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
+ provides a comparably fast partially symbolic evaluation which
+ permits also normalization of functions and uninterpreted symbols;
+ the stack of code to be trusted is considerable.
+*}
-subsection {* Hybrid techniques *}
+subsubsection {* Evaluation in ML (@{text code}) *}
+
+text {*
+ Highest performance can be achieved by evaluation in ML, at the cost
+ of being restricted to ground results and a layered stack of code to
+ be trusted, including code generator configurations by the user.
-text {* code reflect runtime *}
-
-text {* code reflect external *}
+ Evaluation is carried out in a target language \emph{Eval} which
+ inherits from \emph{SML} but for convenience uses parts of the
+ Isabelle runtime environment. The soundness of computation carried
+ out there 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.
+*}
-text {* FIXME here the old sections follow *}
-
-subsection {* Evaluation oracle *}
+subsection {* Aspects of evaluation *}
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:
+ Each of the techniques can be combined with different aspects. The
+ most important distinction is between dynamic and static evaluation.
+ Dynamic evaluation takes the code generator configuration \qt{as it
+ is} at the point where evaluation is issued. Best example is the
+ @{command_def value} command which allows ad-hoc evaluation of
+ terms:
*}
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:
+ \noindent By default @{command value} tries all available evaluation
+ techniques and prints the result of the first succeeding one. A particular
+ technique may be specified in square brackets, e.g.
*}
-lemma %quote "42 / (12 :: rat) = 7 / 2"
- by %quote eval
+value %quote [nbe] "42 / (12 :: rat)"
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.
+ Static evaluation freezes the code generator configuration at a
+ certain point and uses this context whenever evaluation is issued
+ later on. This is particularly appropriate for proof procedures
+ which use evaluation, since then the behaviour of evaluation is not
+ changed or even compromised later on by actions of the user.
+
+ As a technical complication, terms after evaluation in ML must be
+ turned into Isabelle's internal term representation again. Since
+ this is also configurable, it is never fully trusted. For this
+ reason, evaluation in ML comes with further aspects:
+
+ \begin{description}
+
+ \item[Plain evaluation.] A term is normalized using the provided
+ term reconstruction from ML to Isabelle; for applications which
+ do not need to be fully trusted.
+
+ \item[Property conversion.] Evaluates propositions; since these
+ are monomorphic, the term reconstruction is fixed once and for all
+ and therefore trustable.
+
+ \item[Conversion.] Evaluates an arbitrary term @{term "t"} first
+ by plain evaluation and certifies the result @{term "t'"} by
+ checking the equation @{term "t \<equiv> t'"} using property
+ conversion.
+
+ \end{description}
+
+ \noindent The picture is further complicated by the roles of
+ exceptions. Here three cases have to be distinguished:
+
+ \begin{itemize}
+
+ \item Evaluation of @{term t} terminates with a result @{term
+ "t'"}.
+
+ \item Evaluation of @{term t} terminates which en exception
+ indicating a pattern match failure or a not-implemented
+ function. As sketched in \secref{sec:partiality}, this can be
+ interpreted as partiality.
+
+ \item Evaluation raise any other kind of exception.
+
+ \end{itemize}
+
+ \noindent For conversions, the first case yields the equation @{term
+ "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
+ Exceptions of the third kind are propagted to the user.
+
+ By default return values of plain evaluation are optional, yielding
+ @{text "SOME t'"} in the first case, @{text "NONE"} and in the
+ second propagating the exception in the third case. A strict
+ variant of plain evaluation either yields @{text "t'"} or propagates
+ any exception, a liberal variant caputures any exception in a result
+ of type @{text "Exn.result"}.
+
+ For property conversion (which coincides with conversion except for
+ evaluation in ML), methods are provided which solve a given goal by
+ evaluation.
*}
-subsubsection {* Code antiquotation *}
+subsection {* Schematic overview *}
+
+(*FIXME rotatebox?*)
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:
+ \begin{tabular}{ll||c|c|c}
+ & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
+ dynamic & interactive evaluation
+ & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
+ \tabularnewline
+ & plain evaluation & & & @{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline
+ & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
+ & property conversion & & & @{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline
+ & conversion & @{ML "Code_Simp.dynamic_eval_conv"} & @{ML "Nbe.dynamic_eval_conv"}
+ & @{ML "Code_Evaluation.dynamic_eval_conv"} \tabularnewline \hline \hline
+ static & plain evaluation & & & @{ML "Code_Evaluation.static_value"} \tabularnewline \hline
+ & property conversion & &
+ & @{ML "Code_Runtime.static_holds_conv"} \tabularnewline \hline
+ & conversion & @{ML "Code_Simp.static_eval_conv"}
+ & @{ML "Nbe.static_eval_conv"}
+ & @{ML "Code_Evaluation.static_eval_conv"}
+ \end{tabular}
+*}
+
+
+subsection {* Intimate connection between logic and system runtime *}
+
+text {*
+ The toolbox of static evaluation conversions forms a reasonable base
+ to interweave generated code and system tools. However in some
+ situations more direct interaction is desirable.
+*}
+
+
+subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation *}
+
+text {*
+ The @{text code} antiquotation allows to include constants from
+ generated code directly into ML system code, as in the following toy
+ example:
*}
datatype %quote form = T | F | And form form | Or form form (*<*)
@@ -90,15 +214,66 @@
*}
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"}.
+ \noindent @{text code} takes as argument the name of a constant;
+ after the whole ML 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"}. Note that it is not
+ possible to refer to constants which carry adaptations by means of
+ @{text code}; here you have to refer to the adapted code directly.
- For a less simplistic example, theory @{text Ferrack} is
- a good reference.
+ For a less simplistic example, theory @{text Approximation} in
+ the @{text Decision_Procs} session is a good reference.
*}
+subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
+
+text {*
+ The @{text code} antiquoation is lightweight, but the generated code
+ is only accessible while the ML section is processed. Sometimes this
+ is not appropriate, especially if the generated code contains datatype
+ declarations which are shared with other parts of the system. In these
+ cases, @{command_def code_reflect} can be used:
+*}
+
+code_reflect %quote Sum_Type
+ datatypes sum = Inl | Inr
+ functions "Sum_Type.Projl" "Sum_Type.Projr"
+
+text {*
+ \noindent @{command_def code_reflect} takes a structure name and
+ references to datatypes and functions; for these code is compiled
+ into the named ML structure and the \emph{Eval} target is modified
+ in a way that future code generation will reference these
+ precompiled versions of the given datatypes and functions. This
+ also allows to refer to the referenced datatypes and functions from
+ arbitrary ML code as well.
+
+ A typical example for @{command code_reflect} can be found in the
+ @{theory Predicate} theory.
+*}
+
+
+subsubsection {* Separate compilation -- @{text code_reflect} *}
+
+text {*
+ For technical reasons it is sometimes necessary to separate
+ generation and compilation of code which is supposed to be used in
+ the system runtime. For this @{command code_reflect} with an
+ optional @{text "file"} argument can be used:
+*}
+
+code_reflect %quote Rat
+ datatypes rat = Frct
+ functions Fract
+ "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
+ "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
+ file "examples/rat.ML"
+
+text {*
+ \noindent This just generates the references code to the specified
+ file which can be included into the system runtime later on.
+*}
+
end
--- a/doc-src/Codegen/Thy/Refinement.thy Wed Sep 22 16:17:20 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Wed Sep 22 16:24:41 2010 +0200
@@ -167,7 +167,7 @@
*}
-subsection {* Datatype refinement involving invariants *}
+subsection {* Datatype refinement involving invariants \label{sec:invariant} *}
text {*
Datatype representation involving invariants require a dedicated
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Wed Sep 22 16:17:20 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Wed Sep 22 16:24:41 2010 +0200
@@ -23,7 +23,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Introduction%
+Recalling \secref{sec:principle}, code generation turns a system of
+ equations into a program with the \emph{same} equational semantics.
+ As a consequence, this program can be used as a \emph{rewrite
+ engine} for terms: rewriting a term \isa{t} using a program to a
+ term \isa{t{\isacharprime}} yields the theorems \isa{t\ {\isasymequiv}\ t{\isacharprime}}. This
+ application of code generation in the following is referred to as
+ \emph{evaluation}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -32,81 +38,81 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-simplifier%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-nbe%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-eval target: SML standalone vs. Isabelle/SML, example, soundness%
+The existing infrastructure provides a rich palett of evaluation
+ techniques, each comprising different aspects:
+
+ \begin{description}
+
+ \item[Expressiveness.] Depending on how good symbolic computation
+ is supported, the class of terms which can be evaluated may be
+ bigger or smaller.
+
+ \item[Efficiency.] The more machine-near the technique, the
+ faster it is.
+
+ \item[Trustability.] Techniques which a huge (and also probably
+ more configurable infrastructure) are more fragile and less
+ trustable.
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Dynamic evaluation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-value (three variants)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-methods (three variants)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-corresponding ML interfaces%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Static evaluation%
+\isamarkupsubsubsection{The simplifier (\isa{simp})%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-code_simp, nbe (tbd), Eval (tbd, in simple fashion)%
+The simplest way for evaluation is just using the simplifier with
+ the original code equations of the underlying program. This gives
+ fully symbolic evaluation and highest trustablity, with the usual
+ performance of the simplifier. Note that for operations on abstract
+ datatypes (cf.~\secref{sec:invariant}), the original theorems as
+ given by the users are used, not the modified ones.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\begin{isamarkuptext}%
-hand-written: code antiquotation%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Hybrid techniques%
+\isamarkupsubsubsection{Normalization by evaluation (\isa{nbe})%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-code reflect runtime%
+Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
+ provides a comparably fast partially symbolic evaluation which
+ permits also normalization of functions and uninterpreted symbols;
+ the stack of code to be trusted is considerable.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\begin{isamarkuptext}%
-code reflect external%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME here the old sections follow%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Evaluation oracle%
+\isamarkupsubsubsection{Evaluation in ML (\isa{code})%
}
\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:%
+Highest performance can be achieved by evaluation in ML, at the cost
+ of being restricted to ground results and a layered stack of code to
+ be trusted, including code generator configurations by the user.
+
+ Evaluation is carried out in a target language \emph{Eval} which
+ inherits from \emph{SML} but for convenience uses parts of the
+ Isabelle runtime environment. The soundness of computation carried
+ out there 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{Aspects of evaluation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Each of the techniques can be combined with different aspects. The
+ most important distinction is between dynamic and static evaluation.
+ Dynamic evaluation takes the code generator configuration \qt{as it
+ is} at the point where evaluation is issued. Best example is the
+ \indexdef{}{command}{value}\hypertarget{command.value}{\hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}}} command which allows ad-hoc evaluation of
+ terms:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -125,10 +131,9 @@
\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:%
+\noindent By default \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} tries all available evaluation
+ techniques and prints the result of the first succeeding one. A particular
+ technique may be specified in square brackets, e.g.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -137,10 +142,8 @@
\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%
+\isacommand{value}\isamarkupfalse%
+\ {\isacharbrackleft}nbe{\isacharbrackright}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
@@ -149,21 +152,110 @@
\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.%
+Static evaluation freezes the code generator configuration at a
+ certain point and uses this context whenever evaluation is issued
+ later on. This is particularly appropriate for proof procedures
+ which use evaluation, since then the behaviour of evaluation is not
+ changed or even compromised later on by actions of the user.
+
+ As a technical complication, terms after evaluation in ML must be
+ turned into Isabelle's internal term representation again. Since
+ this is also configurable, it is never fully trusted. For this
+ reason, evaluation in ML comes with further aspects:
+
+ \begin{description}
+
+ \item[Plain evaluation.] A term is normalized using the provided
+ term reconstruction from ML to Isabelle; for applications which
+ do not need to be fully trusted.
+
+ \item[Property conversion.] Evaluates propositions; since these
+ are monomorphic, the term reconstruction is fixed once and for all
+ and therefore trustable.
+
+ \item[Conversion.] Evaluates an arbitrary term \isa{t} first
+ by plain evaluation and certifies the result \isa{t{\isacharprime}} by
+ checking the equation \isa{t\ {\isasymequiv}\ t{\isacharprime}} using property
+ conversion.
+
+ \end{description}
+
+ \noindent The picture is further complicated by the roles of
+ exceptions. Here three cases have to be distinguished:
+
+ \begin{itemize}
+
+ \item Evaluation of \isa{t} terminates with a result \isa{t{\isacharprime}}.
+
+ \item Evaluation of \isa{t} terminates which en exception
+ indicating a pattern match failure or a not-implemented
+ function. As sketched in \secref{sec:partiality}, this can be
+ interpreted as partiality.
+
+ \item Evaluation raise any other kind of exception.
+
+ \end{itemize}
+
+ \noindent For conversions, the first case yields the equation \isa{t\ {\isacharequal}\ t{\isacharprime}}, the second defaults to reflexivity \isa{t\ {\isacharequal}\ t}.
+ Exceptions of the third kind are propagted to the user.
+
+ By default return values of plain evaluation are optional, yielding
+ \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} and in the
+ second propagating the exception in the third case. A strict
+ variant of plain evaluation either yields \isa{t{\isacharprime}} or propagates
+ any exception, a liberal variant caputures any exception in a result
+ of type \isa{Exn{\isachardot}result}.
+
+ For property conversion (which coincides with conversion except for
+ evaluation in ML), methods are provided which solve a given goal by
+ evaluation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Code antiquotation%
+\isamarkupsubsection{Schematic overview%
}
\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:%
+\begin{tabular}{ll||c|c|c}
+ & & \isa{simp} & \isa{nbe} & \isa{code} \tabularnewline \hline \hline
+ dynamic & interactive evaluation
+ & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}simp{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}nbe{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}code{\isacharbrackright}}
+ \tabularnewline
+ & plain evaluation & & & \verb|Code_Evaluation.dynamic_value| \tabularnewline \hline
+ & evaluation method & \hyperlink{method.code-simp}{\mbox{\isa{code{\isacharunderscore}simp}}} & \hyperlink{method.normalization}{\mbox{\isa{normalization}}} & \hyperlink{method.eval}{\mbox{\isa{eval}}} \tabularnewline
+ & property conversion & & & \verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \hline
+ & conversion & \verb|Code_Simp.dynamic_eval_conv| & \verb|Nbe.dynamic_eval_conv|
+ & \verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline
+ static & plain evaluation & & & \verb|Code_Evaluation.static_value| \tabularnewline \hline
+ & property conversion & &
+ & \verb|Code_Runtime.static_holds_conv| \tabularnewline \hline
+ & conversion & \verb|Code_Simp.static_eval_conv|
+ & \verb|Nbe.static_eval_conv|
+ & \verb|Code_Evaluation.static_eval_conv|
+ \end{tabular}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Intimate connection between logic and system runtime%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The toolbox of static evaluation conversions forms a reasonable base
+ to interweave generated code and system tools. However in some
+ situations more direct interaction is desirable.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Static embedding of generated code into system runtime -- the \isa{code} antiquotation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \isa{code} antiquotation allows to include constants from
+ generated code directly into ML system code, as in the following toy
+ example:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -219,14 +311,96 @@
\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}.
+\noindent \isa{code} takes as argument the name of a constant;
+ after the whole ML 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}. Note that it is not
+ possible to refer to constants which carry adaptations by means of
+ \isa{code}; here you have to refer to the adapted code directly.
- For a less simplistic example, theory \isa{Ferrack} is
- a good reference.%
+ For a less simplistic example, theory \isa{Approximation} in
+ the \isa{Decision{\isacharunderscore}Procs} session is a good reference.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Static embedding of generated code into system runtime -- \isa{code{\isacharunderscore}reflect}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \isa{code} antiquoation is lightweight, but the generated code
+ is only accessible while the ML section is processed. Sometimes this
+ is not appropriate, especially if the generated code contains datatype
+ declarations which are shared with other parts of the system. In these
+ cases, \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} can be used:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}reflect}\isamarkupfalse%
+\ Sum{\isacharunderscore}Type\isanewline
+\ \ \isakeyword{datatypes}\ sum\ {\isacharequal}\ Inl\ {\isacharbar}\ Inr\isanewline
+\ \ \isakeyword{functions}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projl{\isachardoublequoteclose}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projr{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} takes a structure name and
+ references to datatypes and functions; for these code is compiled
+ into the named ML structure and the \emph{Eval} target is modified
+ in a way that future code generation will reference these
+ precompiled versions of the given datatypes and functions. This
+ also allows to refer to the referenced datatypes and functions from
+ arbitrary ML code as well.
+
+ A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} can be found in the
+ \hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Separate compilation -- \isa{code{\isacharunderscore}reflect}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+For technical reasons it is sometimes necessary to separate
+ generation and compilation of code which is supposed to be used in
+ the system runtime. For this \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} with an
+ optional \isa{file} argument can be used:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}reflect}\isamarkupfalse%
+\ Rat\isanewline
+\ \ \isakeyword{datatypes}\ rat\ {\isacharequal}\ Frct\isanewline
+\ \ \isakeyword{functions}\ Fract\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}plus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}minus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}times\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}divide\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}rat{\isachardot}ML{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This just generates the references code to the specified
+ file which can be included into the system runtime later on.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Wed Sep 22 16:17:20 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Wed Sep 22 16:24:41 2010 +0200
@@ -405,7 +405,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Datatype refinement involving invariants%
+\isamarkupsubsection{Datatype refinement involving invariants \label{sec:invariant}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Sep 22 16:17:20 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Sep 22 16:24:41 2010 +0200
@@ -996,6 +996,7 @@
@{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}
\end{matharray}
\begin{rail}
@@ -1068,6 +1069,10 @@
'code\_modulename' target ( ( string string ) + )
;
+ 'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+ ( 'functions' ( string + ) ) ? ( 'file' string ) ?
+ ;
+
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
@@ -1076,8 +1081,9 @@
\begin{description}
\item @{command (HOL) "export_code"} generates code for a given list
- of constants in the specified target language(s). If no serialization
- instruction is given, only abstract code is generated internally.
+ of constants in the specified target language(s). If no
+ serialization instruction is given, only abstract code is generated
+ internally.
Constants may be specified by giving them literally, referring to
all executable contants within a certain theory by giving @{text
@@ -1089,20 +1095,20 @@
after the @{keyword "module_name"} keyword; then \emph{all} code is
placed in this module.
- For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
- single file; for \emph{Haskell}, it refers to a whole directory,
- where code is generated in multiple files reflecting the module
- hierarchy. Omitting the file specification denotes standard
+ For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
+ refers to a single file; for \emph{Haskell}, it refers to a whole
+ directory, where code is generated in multiple files reflecting the
+ module hierarchy. Omitting the file specification denotes standard
output.
Serializers take an optional list of arguments in parentheses. For
\emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
explicit module signatures.
- For \emph{Haskell} a module name prefix may be given using the ``@{text
- "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
- "deriving (Read, Show)"}'' clause to each appropriate datatype
- declaration.
+ For \emph{Haskell} a module name prefix may be given using the
+ ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
+ ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
+ datatype declaration.
\item @{attribute (HOL) code} explicitly selects (or with option
``@{text "del"}'' deselects) a code equation for code generation.
@@ -1112,8 +1118,8 @@
code equations on abstract datatype representations respectively.
\item @{command (HOL) "code_abort"} declares constants which are not
- required to have a definition by means of code equations; if
- needed these are implemented by program abort instead.
+ required to have a definition by means of code equations; if needed
+ these are implemented by program abort instead.
\item @{command (HOL) "code_datatype"} specifies a constructor set
for a logical type.
@@ -1121,17 +1127,16 @@
\item @{command (HOL) "print_codesetup"} gives an overview on
selected code equations and code generator datatypes.
- \item @{attribute (HOL) code_inline} declares (or with
- option ``@{text "del"}'' removes) inlining theorems which are
- applied as rewrite rules to any code equation during
- preprocessing.
+ \item @{attribute (HOL) code_inline} declares (or with option
+ ``@{text "del"}'' removes) inlining theorems which are applied as
+ rewrite rules to any code equation during preprocessing.
- \item @{attribute (HOL) code_post} declares (or with
- option ``@{text "del"}'' removes) theorems which are
- applied as rewrite rules to any result of an evaluation.
+ \item @{attribute (HOL) code_post} declares (or with option ``@{text
+ "del"}'' removes) theorems which are applied as rewrite rules to any
+ result of an evaluation.
- \item @{command (HOL) "print_codeproc"} prints the setup
- of the code generator preprocessor.
+ \item @{command (HOL) "print_codeproc"} prints the setup of the code
+ generator preprocessor.
\item @{command (HOL) "code_thms"} prints a list of theorems
representing the corresponding program containing all given
@@ -1173,11 +1178,21 @@
\item @{command (HOL) "code_modulename"} declares aliasings from one
module name onto another.
+ \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
+ argument compiles code into the system runtime environment and
+ modifies the code generator setup that future invocations of system
+ runtime code generation referring to one of the ``@{text
+ "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled
+ entities. With a ``@{text "file"}'' argument, the corresponding code
+ is generated into that specified file without modifying the code
+ generator setup.
+
\end{description}
- The other framework generates code from both functional and relational
- programs to SML. See \cite{isabelle-HOL} for further information
- (this actually covers the new-style theory format as well).
+ The other framework generates code from both functional and
+ relational programs to SML. See \cite{isabelle-HOL} for further
+ information (this actually covers the new-style theory format as
+ well).
\begin{matharray}{rcl}
@{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Sep 22 16:17:20 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Sep 22 16:24:41 2010 +0200
@@ -1012,6 +1012,7 @@
\indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
\end{matharray}
\begin{rail}
@@ -1084,6 +1085,10 @@
'code\_modulename' target ( ( string string ) + )
;
+ 'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+ ( 'functions' ( string + ) ) ? ( 'file' string ) ?
+ ;
+
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
@@ -1092,8 +1097,9 @@
\begin{description}
\item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list
- of constants in the specified target language(s). If no serialization
- instruction is given, only abstract code is generated internally.
+ of constants in the specified target language(s). If no
+ serialization instruction is given, only abstract code is generated
+ internally.
Constants may be specified by giving them literally, referring to
all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
@@ -1104,18 +1110,20 @@
after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
placed in this module.
- For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
- single file; for \emph{Haskell}, it refers to a whole directory,
- where code is generated in multiple files reflecting the module
- hierarchy. Omitting the file specification denotes standard
+ For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
+ refers to a single file; for \emph{Haskell}, it refers to a whole
+ directory, where code is generated in multiple files reflecting the
+ module hierarchy. Omitting the file specification denotes standard
output.
Serializers take an optional list of arguments in parentheses. For
\emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
explicit module signatures.
- For \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
- declaration.
+ For \emph{Haskell} a module name prefix may be given using the
+ ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a
+ ``\verb|deriving (Read, Show)|'' clause to each appropriate
+ datatype declaration.
\item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
@@ -1125,8 +1133,8 @@
code equations on abstract datatype representations respectively.
\item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
- required to have a definition by means of code equations; if
- needed these are implemented by program abort instead.
+ required to have a definition by means of code equations; if needed
+ these are implemented by program abort instead.
\item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
for a logical type.
@@ -1134,17 +1142,15 @@
\item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
selected code equations and code generator datatypes.
- \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
- option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
- applied as rewrite rules to any code equation during
- preprocessing.
+ \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with option
+ ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are applied as
+ rewrite rules to any code equation during preprocessing.
- \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
- option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
- applied as rewrite rules to any result of an evaluation.
+ \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are applied as rewrite rules to any
+ result of an evaluation.
- \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
- of the code generator preprocessor.
+ \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup of the code
+ generator preprocessor.
\item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
representing the corresponding program containing all given
@@ -1186,11 +1192,20 @@
\item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
module name onto another.
+ \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} without a ``\isa{{\isachardoublequote}file{\isachardoublequote}}''
+ argument compiles code into the system runtime environment and
+ modifies the code generator setup that future invocations of system
+ runtime code generation referring to one of the ``\isa{{\isachardoublequote}datatypes{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}functions{\isachardoublequote}}'' entities use these precompiled
+ entities. With a ``\isa{{\isachardoublequote}file{\isachardoublequote}}'' argument, the corresponding code
+ is generated into that specified file without modifying the code
+ generator setup.
+
\end{description}
- The other framework generates code from both functional and relational
- programs to SML. See \cite{isabelle-HOL} for further information
- (this actually covers the new-style theory format as well).
+ The other framework generates code from both functional and
+ relational programs to SML. See \cite{isabelle-HOL} for further
+ information (this actually covers the new-style theory format as
+ well).
\begin{matharray}{rcl}
\indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
--- a/doc-src/manual.bib Wed Sep 22 16:17:20 2010 +0200
+++ b/doc-src/manual.bib Wed Sep 22 16:24:41 2010 +0200
@@ -67,6 +67,19 @@
publisher = {CSLI},
year = 1988}
+@inproceedings{Aehlig-Haftmann-Nipkow:2008:nbe,
+ author = {Klaus Aehlig and Florian Haftmann and Tobias Nipkow},
+ title = {A Compiled Implementation of Normalization by Evaluation},
+ booktitle = {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics},
+ year = {2008},
+ isbn = {978-3-540-71065-3},
+ pages = {352--367},
+ publisher = Springer,
+ series = LNCS,
+ volume = {5170},
+ editor = {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar}
+}
+
@InProceedings{alf,
author = {Lena Magnusson and Bengt {Nordstr\"{o}m}},
title = {The {ALF} Proof Editor and Its Proof Engine},
--- a/src/HOL/Imperative_HOL/Overview.thy Wed Sep 22 16:17:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy Wed Sep 22 16:24:41 2010 +0200
@@ -61,7 +61,7 @@
fact collection @{text execute_simps} contains appropriate rewrites
for all fundamental operations.
- Primitive fine-granular control over heaps is avialable through rule
+ Primitive fine-granular control over heaps is available through rule
@{text Heap_cases}:
\begin{quote}
@@ -231,13 +231,13 @@
\item Whether one should prefer equational reasoning (fact
collection @{text execute_simps} or relational reasoning (fact
- collections @{text crel_intros} and @{text crel_elims}) dependes
- on the problems. For complex expressions or expressions
- involving binders, the relation style usually is superior but
- requires more proof text.
+ collections @{text crel_intros} and @{text crel_elims}) depends
+ on the problems to solve. For complex expressions or
+ expressions involving binders, the relation style usually is
+ superior but requires more proof text.
\item Note that you can extend the fact collections of Imperative
- HOL yourself.
+ HOL yourself whenever appropriate.
\end{itemize}
*}
--- a/src/HOL/Imperative_HOL/Ref.thy Wed Sep 22 16:17:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Wed Sep 22 16:24:41 2010 +0200
@@ -273,15 +273,17 @@
by (simp add: ref'_def)
-text {* SML *}
+text {* SML / Eval *}
-code_type ref (SML "_/ Unsynchronized.ref")
+code_type ref (SML "_/ ref")
+code_type ref (Eval "_/ Unsynchronized.ref")
code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
-code_const ref' (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
+code_const ref' (SML "(fn/ ()/ =>/ ref/ _)")
+code_const ref' (Eval "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
-code_reserved SML Unsynchronized
+code_reserved Eval Unsynchronized
text {* OCaml *}
--- a/src/HOL/Library/FuncSet.thy Wed Sep 22 16:17:20 2010 +0200
+++ b/src/HOL/Library/FuncSet.thy Wed Sep 22 16:24:41 2010 +0200
@@ -173,6 +173,20 @@
text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
the theorems belong here, or need at least @{term Hilbert_Choice}.*}
+lemma bij_betwI:
+assumes "f \<in> A \<rightarrow> B" and "g \<in> B \<rightarrow> A"
+ and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x" and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y"
+shows "bij_betw f A B"
+unfolding bij_betw_def
+proof
+ show "inj_on f A" by (metis g_f inj_on_def)
+next
+ have "f ` A \<subseteq> B" using `f \<in> A \<rightarrow> B` by auto
+ moreover
+ have "B \<subseteq> f ` A" by auto (metis Pi_mem `g \<in> B \<rightarrow> A` f_g image_iff)
+ ultimately show "f ` A = B" by blast
+qed
+
lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
by (auto simp add: bij_betw_def)
@@ -207,6 +221,9 @@
!!x. x\<in>A ==> f x = g x |] ==> f = g"
by (force simp add: fun_eq_iff extensional_def)
+lemma extensional_restrict: "f \<in> extensional A \<Longrightarrow> restrict f A = f"
+by(rule extensionalityI[OF restrict_extensional]) auto
+
lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
by (unfold inv_into_def) (fast intro: someI2)
--- a/src/HOL/List.thy Wed Sep 22 16:17:20 2010 +0200
+++ b/src/HOL/List.thy Wed Sep 22 16:24:41 2010 +0200
@@ -4206,6 +4206,9 @@
lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
+lemma lists_eq_set: "lists A = {xs. set xs <= A}"
+by auto
+
lemma lists_UNIV [simp]: "lists UNIV = UNIV"
by auto
--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 22 16:17:20 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 22 16:24:41 2010 +0200
@@ -215,12 +215,12 @@
>> ATerm) x
and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
-val parse_atom =
- parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
- >> (fn (u1, NONE) => AAtom u1
- | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
- | (u1, SOME (SOME _, u2)) =>
- mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))
+fun parse_atom x =
+ (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
+ >> (fn (u1, NONE) => AAtom u1
+ | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
+ | (u1, SOME (SOME _, u2)) =>
+ mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))) x
fun fo_term_head (ATerm (s, _)) = s
@@ -291,8 +291,8 @@
(* It is not clear why some literals are followed by sequences of stars and/or
pluses. We ignore them. *)
-val parse_decorated_atom =
- parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
+fun parse_decorated_atom x =
+ (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
| mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 22 16:17:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 22 16:24:41 2010 +0200
@@ -149,13 +149,9 @@
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Tactical.SOLVED'
- ((TRY o Simplifier.full_simp_tac preproc_ss)
- THEN' (REPEAT_DETERM o match_tac @{thms allI})
- THEN' (REPEAT_DETERM o ematch_tac @{thms exE})
- THEN' (TRY o Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
- (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
- ctxt)) i st0
+ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
+ (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
+ ctxt i st0
end
val metis_tac = generic_metis_tac HO
--- a/src/Tools/Code/code_preproc.ML Wed Sep 22 16:17:20 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Sep 22 16:24:41 2010 +0200
@@ -106,6 +106,22 @@
(* post- and preprocessing *)
+fun no_variables_conv conv ct =
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
+ val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
+ | t as Var _ => insert (op aconvc) (cert t)
+ | _ => I) (Thm.term_of ct) [];
+ fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
+ |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
+ in
+ ct
+ |> fold_rev Thm.cabs all_vars
+ |> conv
+ |> fold apply_beta all_vars
+ end;
+
fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
fun eqn_conv conv ct =
@@ -141,7 +157,6 @@
fun preprocess_conv thy ct =
let
val ctxt = ProofContext.init_global thy;
- val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
in
ct
@@ -149,7 +164,13 @@
|> trans_conv_rule (AxClass.unoverload_conv thy)
end;
-fun preprocess_term thy = term_of_conv thy (preprocess_conv thy);
+fun preprocess_term thy t =
+ let
+ val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
+ | t as Var _ => insert (op aconv) t
+ | _ => I) t [];
+ val resubst = curry (Term.betapplys o swap) all_vars;
+ in (resubst, term_of_conv thy (preprocess_conv thy) (fold_rev lambda all_vars t)) end;
fun postprocess_conv thy ct =
let
@@ -198,8 +219,11 @@
type code_algebra = (sort -> sort) * Sorts.algebra;
type code_graph = ((string * sort) list * Code.cert) Graph.T;
-fun cert eqngr = snd o Graph.get_node eqngr;
-fun sortargs eqngr = map snd o fst o Graph.get_node eqngr;
+fun get_node eqngr const = Graph.get_node eqngr const
+ handle Graph.UNDEF _ => error ("No such constant in code equation graph: " ^ quote const);
+
+fun cert eqngr = snd o get_node eqngr;
+fun sortargs eqngr = map snd o fst o get_node eqngr;
fun all eqngr = Graph.keys eqngr;
fun pretty thy eqngr =
@@ -433,7 +457,7 @@
fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
-fun dynamic_eval_conv thy conv ct =
+fun dynamic_eval_conv thy conv = no_variables_conv (fn ct =>
let
val thm1 = preprocess_conv thy ct;
val ct' = Thm.rhs_of thm1;
@@ -447,11 +471,11 @@
Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
error ("could not construct evaluation proof:\n"
^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
- end;
+ end);
fun dynamic_eval_value thy postproc evaluator t =
let
- val t' = preprocess_term thy t;
+ val (resubst, t') = preprocess_term thy t;
val vs' = Term.add_tfrees t' [];
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
@@ -459,7 +483,7 @@
val result = evaluator algebra' eqngr' vs' t';
in
evaluator algebra' eqngr' vs' t'
- |> postproc (postprocess_term thy)
+ |> postproc (postprocess_term thy o resubst)
end;
fun static_eval_conv thy consts conv =
@@ -467,9 +491,9 @@
val (algebra, eqngr) = obtain true thy consts [];
val conv' = conv algebra eqngr;
in
- Conv.tap_thy (fn thy => (preprocess_conv thy)
+ no_variables_conv (Conv.tap_thy (fn thy => (preprocess_conv thy)
then_conv (fn ct => uncurry (conv' thy) (dest_cterm ct) ct)
- then_conv (postprocess_conv thy))
+ then_conv (postprocess_conv thy)))
end;
fun static_eval_value thy postproc consts evaluator =
@@ -479,8 +503,9 @@
in fn t =>
t
|> preprocess_term thy
- |> (fn t => evaluator' thy (Term.add_tfrees t []) t)
- |> postproc (postprocess_term thy)
+ |-> (fn resubst => fn t => t
+ |> evaluator' thy (Term.add_tfrees t [])
+ |> postproc (postprocess_term thy o resubst))
end;
--- a/src/Tools/Code/code_runtime.ML Wed Sep 22 16:17:20 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML Wed Sep 22 16:24:41 2010 +0200
@@ -60,6 +60,11 @@
type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
+fun reject_vars thy t =
+ let
+ val ctxt = ProofContext.init_global thy;
+ in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
+
fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
(the_default target some_target) NONE "Code" [];
@@ -88,6 +93,7 @@
fun dynamic_value_exn cookie thy some_target postproc t args =
let
+ val _ = reject_vars thy t;
fun evaluator naming program ((_, vs_ty), t) deps =
base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
@@ -103,7 +109,7 @@
val serializer = obtain_serializer thy some_target;
fun evaluator naming program thy ((_, vs_ty), t) deps =
base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
- in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end;
+ in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
fun static_value_strict cookie thy some_target postproc consts t =
Exn.release (static_value_exn cookie thy some_target postproc consts t);
@@ -121,6 +127,8 @@
val put_truth = Truth_Result.put;
val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
+val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
+
fun check_holds serializer naming thy program vs_t deps ct =
let
val t = Thm.term_of ct;
@@ -143,7 +151,8 @@
raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
- (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy));
+ (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
+ o reject_vars thy);
fun static_holds_conv thy consts =
let
@@ -151,6 +160,7 @@
in
Code_Thingol.static_eval_conv thy consts
(fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
+ o reject_vars thy
end;
--- a/src/Tools/Code/code_simp.ML Wed Sep 22 16:17:20 2010 +0200
+++ b/src/Tools/Code/code_simp.ML Wed Sep 22 16:24:41 2010 +0200
@@ -6,9 +6,8 @@
signature CODE_SIMP =
sig
- val no_frees_conv: conv -> conv
val map_ss: (simpset -> simpset) -> theory -> theory
- val dynamic_eval_conv: theory -> conv
+ val dynamic_eval_conv: conv
val dynamic_eval_tac: theory -> int -> tactic
val dynamic_eval_value: theory -> term -> term
val static_eval_conv: theory -> simpset option -> string list -> conv
@@ -19,22 +18,6 @@
structure Code_Simp : CODE_SIMP =
struct
-(* avoid free variables during conversion *)
-
-fun no_frees_conv conv ct =
- let
- val frees = Thm.add_cterm_frees ct [];
- fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
- |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
- |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
- in
- ct
- |> fold_rev Thm.cabs frees
- |> conv
- |> fold apply_beta frees
- end;
-
-
(* dedicated simpset *)
structure Simpset = Theory_Data
@@ -68,12 +51,12 @@
(* evaluation with dynamic code context *)
-fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy
+val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
(fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
-fun dynamic_eval_tac thy = CONVERSION (dynamic_eval_conv thy) THEN' conclude_tac thy NONE;
+fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE;
-fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv thy o Thm.cterm_of thy;
+fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv o Thm.cterm_of thy;
val setup = Method.setup (Binding.name "code_simp")
(Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
@@ -83,9 +66,9 @@
(* evaluation with static code context *)
-fun static_eval_conv thy some_ss consts = no_frees_conv
- (Code_Thingol.static_eval_conv_simple thy consts
- (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program));
+fun static_eval_conv thy some_ss consts =
+ Code_Thingol.static_eval_conv_simple thy consts
+ (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
THEN' conclude_tac thy some_ss;
--- a/src/Tools/nbe.ML Wed Sep 22 16:17:20 2010 +0200
+++ b/src/Tools/nbe.ML Wed Sep 22 16:24:41 2010 +0200
@@ -589,28 +589,18 @@
fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
-fun no_frees_rew rew t =
- let
- val frees = map Free (Term.add_frees t []);
- in
- t
- |> fold_rev lambda frees
- |> rew
- |> curry (Term.betapplys o swap) frees
- end;
-
-val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Simp.no_frees_conv
- (lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
- (K (fn program => oracle thy program (compile false thy program))))));
+val dynamic_eval_conv = Conv.tap_thy (fn thy =>
+ lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
+ (K (fn program => oracle thy program (compile false thy program)))));
fun dynamic_eval_value thy = lift_triv_classes_rew thy
- (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
- (K (fn program => eval_term thy program (compile false thy program)))));
+ (Code_Thingol.dynamic_eval_value thy I
+ (K (fn program => eval_term thy program (compile false thy program))));
-fun static_eval_conv thy consts = Code_Simp.no_frees_conv
- (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
+fun static_eval_conv thy consts =
+ lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
(K (fn program => let val nbe_program = compile true thy program
- in fn thy => oracle thy program nbe_program end))));
+ in fn thy => oracle thy program nbe_program end)));
(** setup **)