--- 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
--- 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 \<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/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%
%
--- 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 \<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 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}} \\
--- 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}
*}
--- 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 *}
--- 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;
--- 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;
--- 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;
--- 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 **)