use command_def vs. command more consciously
--- a/doc-src/Codegen/Thy/Adaptation.thy Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed Aug 18 09:55:00 2010 +0200
@@ -194,12 +194,12 @@
(SML "true" and "false" and "_ andalso _")
text {*
- \noindent The @{command code_type} command takes a type constructor
+ \noindent The @{command_def code_type} command takes a type constructor
as arguments together with a list of custom serialisations. Each
custom serialisation starts with a target language identifier
followed by an expression, which during code serialisation is
inserted whenever the type constructor would occur. For constants,
- @{command code_const} implements the corresponding mechanism. Each
+ @{command_def code_const} implements the corresponding mechanism. Each
``@{verbatim "_"}'' in a serialisation expression is treated as a
placeholder for the type constructor's (the constant's) arguments.
*}
@@ -226,7 +226,7 @@
avoided to be used for new declarations. Initially, this table
typically contains the keywords of the target language. It can be
extended manually, thus avoiding accidental overwrites, using the
- @{command "code_reserved"} command:
+ @{command_def "code_reserved"} command:
*}
code_reserved %quote "\<SML>" bool true false andalso
@@ -274,7 +274,7 @@
For convenience, the default @{text HOL} setup for @{text Haskell}
maps the @{class eq} class to its counterpart in @{text Haskell},
giving custom serialisations for the class @{class eq} (by command
- @{command code_class}) and its operation @{const HOL.eq}
+ @{command_def code_class}) and its operation @{const HOL.eq}
*}
code_class %quotett eq
@@ -318,7 +318,7 @@
text {*
In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the @{command
+ target language; this is accomplished using the @{command_def
"code_include"} command:
*}
--- a/doc-src/Codegen/Thy/Foundations.thy Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Wed Aug 18 09:55:00 2010 +0200
@@ -121,9 +121,10 @@
\secref{eff_nat}) uses this interface.
\noindent The current setup of the preprocessor may be inspected
- using the @{command print_codeproc} command. @{command code_thms}
- (see \secref{sec:equations}) provides a convenient mechanism to
- inspect the impact of a preprocessor setup on code equations.
+ using the @{command_def print_codeproc} command. @{command_def
+ code_thms} (see \secref{sec:equations}) provides a convenient
+ mechanism to inspect the impact of a preprocessor setup on code
+ equations.
\begin{warn}
Attribute @{attribute code_unfold} also applies to the
@@ -175,9 +176,8 @@
equations (before preprocessing) and code equations (after
preprocessing).
- The first can be listed (among other data) using the @{command
- print_codesetup} command (later on in \secref{sec:refinement}
- it will be shown how these code equations can be changed).
+ The first can be listed (among other data) using the @{command_def
+ print_codesetup} command.
The code equations after preprocessing are already are blueprint of
the generated program and can be inspected using the @{command
@@ -190,7 +190,7 @@
\noindent This prints a table with the code equations for @{const
dequeue}, including \emph{all} code equations those equations depend
on recursively. These dependencies themselves can be visualized using
- the @{command code_deps} command.
+ the @{command_def code_deps} command.
*}
@@ -280,7 +280,7 @@
of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
- explicitly, use @{command "code_abort"}:
+ explicitly, use @{command_def "code_abort"}:
*}
code_abort %quote empty_queue
--- a/doc-src/Codegen/Thy/Further.thy Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Wed Aug 18 09:55:00 2010 +0200
@@ -75,7 +75,7 @@
end %quote
text {*
- After an interpretation of this locale (say, @{command
+ After an interpretation of this locale (say, @{command_def
interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
"fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
@@ -131,7 +131,7 @@
text {*
Code generation may also be used to \emph{evaluate} expressions
(using @{text SML} as target language of course).
- For instance, the @{command value} reduces an expression to a
+ For instance, the @{command_def value} reduces an expression to a
normal form with respect to the underlying code equations:
*}
--- a/doc-src/Codegen/Thy/Introduction.thy Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed Aug 18 09:55:00 2010 +0200
@@ -34,11 +34,12 @@
subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
text {*
- In a HOL theory, the @{command datatype} and @{command
- definition}/@{command primrec}/@{command fun} declarations form the
- core of a functional programming language. By default equational
- theorems stemming from those are used for generated code, therefore
- \qt{naive} code generation can proceed without further ado.
+ In a HOL theory, the @{command_def datatype} and @{command_def
+ definition}/@{command_def primrec}/@{command_def fun} declarations
+ form the core of a functional programming language. By default
+ equational theorems stemming from those are used for generated code,
+ therefore \qt{naive} code generation can proceed without further
+ ado.
For example, here a simple \qt{implementation} of amortised queues:
*}
@@ -71,12 +72,12 @@
text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
text {*
- \noindent The @{command export_code} command takes a space-separated
- list of constants for which code shall be generated; anything else
- needed for those is added implicitly. Then follows a target
- language identifier and a freely chosen module name. A file name
- denotes the destination to store the generated code. Note that the
- semantics of the destination depends on the target language: for
+ \noindent The @{command_def export_code} command takes a
+ space-separated list of constants for which code shall be generated;
+ anything else needed for those is added implicitly. Then follows a
+ target language identifier and a freely chosen module name. A file
+ name denotes the destination to store the generated code. Note that
+ the semantics of the destination depends on the target language: for
@{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text
Haskell} it denotes a \emph{directory} where a file named as the
module name (with extension @{text ".hs"}) is written:
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Aug 18 09:55:00 2010 +0200
@@ -302,12 +302,12 @@
\endisadelimquotett
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
+\noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} command takes a type constructor
as arguments together with a list of custom serialisations. Each
custom serialisation starts with a target language identifier
followed by an expression, which during code serialisation is
inserted whenever the type constructor would occur. For constants,
- \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements the corresponding mechanism. Each
+ \indexdef{}{command}{code\_const}\hypertarget{command.code-const}{\hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} implements the corresponding mechanism. Each
``\verb|_|'' in a serialisation expression is treated as a
placeholder for the type constructor's (the constant's) arguments.%
\end{isamarkuptext}%
@@ -416,7 +416,7 @@
avoided to be used for new declarations. Initially, this table
typically contains the keywords of the target language. It can be
extended manually, thus avoiding accidental overwrites, using the
- \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
+ \indexdef{}{command}{code\_reserved}\hypertarget{command.code-reserved}{\hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -501,7 +501,7 @@
For convenience, the default \isa{HOL} setup for \isa{Haskell}
maps the \isa{eq} class to its counterpart in \isa{Haskell},
giving custom serialisations for the class \isa{eq} (by command
- \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation \isa{eq{\isacharunderscore}class{\isachardot}eq}%
+ \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{eq{\isacharunderscore}class{\isachardot}eq}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -602,7 +602,7 @@
%
\begin{isamarkuptext}%
In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} command:%
+ target language; this is accomplished using the \indexdef{}{command}{code\_include}\hypertarget{command.code-include}{\hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Foundations.tex Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Wed Aug 18 09:55:00 2010 +0200
@@ -182,9 +182,9 @@
\secref{eff_nat}) uses this interface.
\noindent The current setup of the preprocessor may be inspected
- using the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}
- (see \secref{sec:equations}) provides a convenient mechanism to
- inspect the impact of a preprocessor setup on code equations.
+ using the \indexdef{}{command}{print\_codeproc}\hypertarget{command.print-codeproc}{\hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}} command. \indexdef{}{command}{code\_thms}\hypertarget{command.code-thms}{\hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}} (see \secref{sec:equations}) provides a convenient
+ mechanism to inspect the impact of a preprocessor setup on code
+ equations.
\begin{warn}
Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
@@ -275,8 +275,7 @@
equations (before preprocessing) and code equations (after
preprocessing).
- The first can be listed (among other data) using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command (later on in \secref{sec:refinement}
- it will be shown how these code equations can be changed).
+ The first can be listed (among other data) using the \indexdef{}{command}{print\_codesetup}\hypertarget{command.print-codesetup}{\hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}} command.
The code equations after preprocessing are already are blueprint of
the generated program and can be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
@@ -300,7 +299,7 @@
\begin{isamarkuptext}%
\noindent This prints a table with the code equations for \isa{dequeue}, including \emph{all} code equations those equations depend
on recursively. These dependencies themselves can be visualized using
- the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command.%
+ the \indexdef{}{command}{code\_deps}\hypertarget{command.code-deps}{\hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}} command.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -503,7 +502,7 @@
of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
- explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
+ explicitly, use \indexdef{}{command}{code\_abort}\hypertarget{command.code-abort}{\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Further.tex Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed Aug 18 09:55:00 2010 +0200
@@ -145,7 +145,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-After an interpretation of this locale (say, \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} \isa{fun{\isacharunderscore}power{\isacharcolon}} \isa{{\isachardoublequote}power\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}), one would expect to have a constant \isa{fun{\isacharunderscore}power{\isachardot}powers\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} for which code
+After an interpretation of this locale (say, \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} \isa{fun{\isacharunderscore}power{\isacharcolon}} \isa{{\isachardoublequote}power\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}), one would expect to have a constant \isa{fun{\isacharunderscore}power{\isachardot}powers\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} for which code
can be generated. But this not the case: internally, the term
\isa{fun{\isacharunderscore}power{\isachardot}powers} is an abbreviation for the foundational
term \isa{{\isachardoublequote}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}
@@ -253,7 +253,7 @@
\begin{isamarkuptext}%
Code generation may also be used to \emph{evaluate} expressions
(using \isa{SML} as target language of course).
- For instance, the \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} reduces an expression to a
+ For instance, the \indexdef{}{command}{value}\hypertarget{command.value}{\hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}}} reduces an expression to a
normal form with respect to the underlying code equations:%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Aug 18 09:55:00 2010 +0200
@@ -55,10 +55,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-In a HOL theory, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form the
- core of a functional programming language. By default equational
- theorems stemming from those are used for generated code, therefore
- \qt{naive} code generation can proceed without further ado.
+In a HOL theory, the \indexdef{}{command}{datatype}\hypertarget{command.datatype}{\hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}} and \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}/\indexdef{}{command}{primrec}\hypertarget{command.primrec}{\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}}/\indexdef{}{command}{fun}\hypertarget{command.fun}{\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}} declarations
+ form the core of a functional programming language. By default
+ equational theorems stemming from those are used for generated code,
+ therefore \qt{naive} code generation can proceed without further
+ ado.
For example, here a simple \qt{implementation} of amortised queues:%
\end{isamarkuptext}%
@@ -184,12 +185,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated
- list of constants for which code shall be generated; anything else
- needed for those is added implicitly. Then follows a target
- language identifier and a freely chosen module name. A file name
- denotes the destination to store the generated code. Note that the
- semantics of the destination depends on the target language: for
+\noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
+ space-separated list of constants for which code shall be generated;
+ anything else needed for those is added implicitly. Then follows a
+ target language identifier and a freely chosen module name. A file
+ name denotes the destination to store the generated code. Note that
+ the semantics of the destination depends on the target language: for
\isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} it denotes a \emph{directory} where a file named as the
module name (with extension \isa{{\isachardot}hs}) is written:%
\end{isamarkuptext}%