# HG changeset patch # User haftmann # Date 1282118100 -7200 # Node ID 2f8699695cf676025c2963dca97563b5a1e33bd9 # Parent 76965c356d2aed872e3a2af999adf666dcab61b8 use command_def vs. command more consciously diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/Adaptation.thy --- 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 "\" 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: *} diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/Foundations.thy --- 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 diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/Further.thy --- 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 (\n (f :: 'a \ 'a). f ^^ n)"}), one would expect to have a constant @{text "fun_power.powers :: nat list \ ('a \ 'a) \ 'a \ '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: *} diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/Introduction.thy --- 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: diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/document/Adaptation.tex --- 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% % diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/document/Foundations.tex --- 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% % diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/document/Further.tex --- 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% diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/document/Introduction.tex --- 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}%