# HG changeset patch # User haftmann # Date 1285148788 -7200 # Node ID e5448cf9a04885a3b5ab7f416b70fabf98b7e3b1 # Parent ae2c3059f8cc05ccbe98f850014c9b4814bf4112# Parent 23bdf736d84f83747693c7db0f5fec23643f55b3 merged diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/Codegen/IsaMakefile --- a/doc-src/Codegen/IsaMakefile Wed Sep 22 10:02:39 2010 +0200 +++ b/doc-src/Codegen/IsaMakefile Wed Sep 22 11:46:28 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 diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/Codegen/Thy/Evaluation.thy --- a/doc-src/Codegen/Thy/Evaluation.thy Wed Sep 22 10:02:39 2010 +0200 +++ b/doc-src/Codegen/Thy/Evaluation.thy Wed Sep 22 11:46:28 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 ae2c3059f8cc -r e5448cf9a048 doc-src/Codegen/Thy/document/Evaluation.tex --- a/doc-src/Codegen/Thy/document/Evaluation.tex Wed Sep 22 10:02:39 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex Wed Sep 22 11:46:28 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% % diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Sep 22 10:02:39 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Sep 22 11:46:28 2010 +0200 @@ -996,6 +996,7 @@ @{command_def (HOL) "code_monad"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_reflect"} & : & @{text "theory \ 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 \ theory"} \\ diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Sep 22 10:02:39 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Sep 22 11:46:28 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}} \\ diff -r ae2c3059f8cc -r e5448cf9a048 src/HOL/Imperative_HOL/Overview.thy --- a/src/HOL/Imperative_HOL/Overview.thy Wed Sep 22 10:02:39 2010 +0200 +++ b/src/HOL/Imperative_HOL/Overview.thy Wed Sep 22 11:46:28 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} *} diff -r ae2c3059f8cc -r e5448cf9a048 src/HOL/Imperative_HOL/Ref.thy --- a/src/HOL/Imperative_HOL/Ref.thy Wed Sep 22 10:02:39 2010 +0200 +++ b/src/HOL/Imperative_HOL/Ref.thy Wed Sep 22 11:46:28 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 *} diff -r ae2c3059f8cc -r e5448cf9a048 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Wed Sep 22 10:02:39 2010 +0200 +++ b/src/Tools/Code/code_preproc.ML Wed Sep 22 11:46:28 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; diff -r ae2c3059f8cc -r e5448cf9a048 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Wed Sep 22 10:02:39 2010 +0200 +++ b/src/Tools/Code/code_runtime.ML Wed Sep 22 11:46:28 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; diff -r ae2c3059f8cc -r e5448cf9a048 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Wed Sep 22 10:02:39 2010 +0200 +++ b/src/Tools/Code/code_simp.ML Wed Sep 22 11:46:28 2010 +0200 @@ -6,7 +6,6 @@ signature CODE_SIMP = sig - val no_frees_conv: conv -> conv val map_ss: (simpset -> simpset) -> theory -> theory val dynamic_eval_conv: conv val dynamic_eval_tac: theory -> int -> tactic @@ -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,8 +51,8 @@ (* evaluation with dynamic code context *) -val dynamic_eval_conv = Conv.tap_thy (fn thy => no_frees_conv (Code_Thingol.dynamic_eval_conv thy - (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program))); +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 THEN' conclude_tac thy NONE; @@ -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; diff -r ae2c3059f8cc -r e5448cf9a048 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Sep 22 10:02:39 2010 +0200 +++ b/src/Tools/nbe.ML Wed Sep 22 11:46:28 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 **)