# HG changeset patch # User haftmann # Date 1285143770 -7200 # Node ID 0af12dea761f261b33b73e4611e20904bdb9af27 # Parent 76bc7e4999f87a24dd13bceeb8eeceb866125911 sections on @{code} and code_reflect diff -r 76bc7e4999f8 -r 0af12dea761f doc-src/Codegen/Thy/Evaluation.thy --- a/doc-src/Codegen/Thy/Evaluation.thy Wed Sep 22 10:04:17 2010 +0200 +++ b/doc-src/Codegen/Thy/Evaluation.thy Wed Sep 22 10:22:50 2010 +0200 @@ -70,9 +70,9 @@ 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 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. + 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. *} @@ -187,19 +187,19 @@ subsection {* Intimate connection between logic and system runtime *} -text {* FIXME *} +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 code antiquotation *} +subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation *} text {* - FIXME - - 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: + 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 (*<*) @@ -214,23 +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 {* FIXME @{command_def 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 {* FIXME *} +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 \ rat \ rat)" "(minus :: rat \ rat \ rat)" + "(times :: rat \ rat \ rat)" "(divide :: rat \ rat \ 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 diff -r 76bc7e4999f8 -r 0af12dea761f doc-src/Codegen/Thy/document/Evaluation.tex --- a/doc-src/Codegen/Thy/document/Evaluation.tex Wed Sep 22 10:04:17 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex Wed Sep 22 10:22:50 2010 +0200 @@ -96,9 +96,9 @@ 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 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.% + 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% % @@ -242,22 +242,20 @@ \isamarkuptrue% % \begin{isamarkuptext}% -FIXME% +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 code antiquotation% +\isamarkupsubsubsection{Static embedding of generated code into system runtime -- the \isa{code} antiquotation% } \isamarkuptrue% % \begin{isamarkuptext}% -FIXME - - 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:% +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% % @@ -313,14 +311,16 @@ \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% % @@ -329,7 +329,41 @@ \isamarkuptrue% % \begin{isamarkuptext}% -FIXME \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}}% +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% % @@ -338,7 +372,35 @@ \isamarkuptrue% % \begin{isamarkuptext}% -FIXME% +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% %