updated to changes in sources; tuned
authorhaftmann
Tue Jul 14 10:54:54 2009 +0200 (2009-07-14)
changeset 320006f07563dc8a9
parent 31999 cb1f26c0de5b
child 32001 fafefd0b341c
updated to changes in sources; tuned
doc-src/Codegen/Thy/Program.thy
doc-src/Codegen/Thy/document/ML.tex
doc-src/Codegen/Thy/document/Program.tex
     1.1 --- a/doc-src/Codegen/Thy/Program.thy	Tue Jul 14 10:54:21 2009 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Program.thy	Tue Jul 14 10:54:54 2009 +0200
     1.3 @@ -153,14 +153,14 @@
     1.4    out: \emph{preprocessing}.  In essence, the preprocessor
     1.5    consists of two components: a \emph{simpset} and \emph{function transformers}.
     1.6  
     1.7 -  The \emph{simpset} allows to employ the full generality of the Isabelle
     1.8 -  simplifier.  Due to the interpretation of theorems
     1.9 -  as code equations, rewrites are applied to the right
    1.10 -  hand side and the arguments of the left hand side of an
    1.11 -  equation, but never to the constant heading the left hand side.
    1.12 -  An important special case are \emph{inline theorems} which may be
    1.13 -  declared and undeclared using the
    1.14 -  \emph{code inline} or \emph{code inline del} attribute respectively.
    1.15 +  The \emph{simpset} allows to employ the full generality of the
    1.16 +  Isabelle simplifier.  Due to the interpretation of theorems as code
    1.17 +  equations, rewrites are applied to the right hand side and the
    1.18 +  arguments of the left hand side of an equation, but never to the
    1.19 +  constant heading the left hand side.  An important special case are
    1.20 +  \emph{unfold theorems} which may be declared and undeclared using
    1.21 +  the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
    1.22 +  attribute respectively.
    1.23  
    1.24    Some common applications:
    1.25  *}
    1.26 @@ -173,21 +173,21 @@
    1.27       \item replacing non-executable constructs by executable ones:
    1.28  *}     
    1.29  
    1.30 -lemma %quote [code inline]:
    1.31 +lemma %quote [code_inline]:
    1.32    "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
    1.33  
    1.34  text {*
    1.35       \item eliminating superfluous constants:
    1.36  *}
    1.37  
    1.38 -lemma %quote [code inline]:
    1.39 +lemma %quote [code_inline]:
    1.40    "1 = Suc 0" by simp
    1.41  
    1.42  text {*
    1.43       \item replacing executable but inconvenient constructs:
    1.44  *}
    1.45  
    1.46 -lemma %quote [code inline]:
    1.47 +lemma %quote [code_inline]:
    1.48    "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
    1.49  
    1.50  text_raw {*
    1.51 @@ -210,10 +210,10 @@
    1.52    on code equations.
    1.53  
    1.54    \begin{warn}
    1.55 -    The attribute \emph{code unfold}
    1.56 -    associated with the @{text "SML code generator"} also applies to
    1.57 -    the @{text "generic code generator"}:
    1.58 -    \emph{code unfold} implies \emph{code inline}.
    1.59 +
    1.60 +    Attribute @{attribute code_unfold} also applies to the
    1.61 +    preprocessor of the ancient @{text "SML code generator"}; in case
    1.62 +    this is not what you intend, use @{attribute code_inline} instead.
    1.63    \end{warn}
    1.64  *}
    1.65  
     2.1 --- a/doc-src/Codegen/Thy/document/ML.tex	Tue Jul 14 10:54:21 2009 +0200
     2.2 +++ b/doc-src/Codegen/Thy/document/ML.tex	Tue Jul 14 10:54:54 2009 +0200
     2.3 @@ -124,8 +124,7 @@
     2.4  %
     2.5  \begin{isamarkuptext}%
     2.6  \begin{mldecls}
     2.7 -  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
     2.8 -  \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
     2.9 +  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
    2.10    \end{mldecls}
    2.11  
    2.12    \begin{description}
    2.13 @@ -133,11 +132,6 @@
    2.14    \item \verb|Code.read_const|~\isa{thy}~\isa{s}
    2.15       reads a constant as a concrete term expression \isa{s}.
    2.16  
    2.17 -  \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
    2.18 -     rewrites a code equation \isa{thm} with a simpset \isa{ss};
    2.19 -     only arguments and right hand side are rewritten,
    2.20 -     not the head of the code equation.
    2.21 -
    2.22    \end{description}%
    2.23  \end{isamarkuptext}%
    2.24  \isamarkuptrue%
     3.1 --- a/doc-src/Codegen/Thy/document/Program.tex	Tue Jul 14 10:54:21 2009 +0200
     3.2 +++ b/doc-src/Codegen/Thy/document/Program.tex	Tue Jul 14 10:54:54 2009 +0200
     3.3 @@ -395,14 +395,14 @@
     3.4    out: \emph{preprocessing}.  In essence, the preprocessor
     3.5    consists of two components: a \emph{simpset} and \emph{function transformers}.
     3.6  
     3.7 -  The \emph{simpset} allows to employ the full generality of the Isabelle
     3.8 -  simplifier.  Due to the interpretation of theorems
     3.9 -  as code equations, rewrites are applied to the right
    3.10 -  hand side and the arguments of the left hand side of an
    3.11 -  equation, but never to the constant heading the left hand side.
    3.12 -  An important special case are \emph{inline theorems} which may be
    3.13 -  declared and undeclared using the
    3.14 -  \emph{code inline} or \emph{code inline del} attribute respectively.
    3.15 +  The \emph{simpset} allows to employ the full generality of the
    3.16 +  Isabelle simplifier.  Due to the interpretation of theorems as code
    3.17 +  equations, rewrites are applied to the right hand side and the
    3.18 +  arguments of the left hand side of an equation, but never to the
    3.19 +  constant heading the left hand side.  An important special case are
    3.20 +  \emph{unfold theorems} which may be declared and undeclared using
    3.21 +  the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
    3.22 +  attribute respectively.
    3.23  
    3.24    Some common applications:%
    3.25  \end{isamarkuptext}%
    3.26 @@ -421,7 +421,7 @@
    3.27  %
    3.28  \isatagquote
    3.29  \isacommand{lemma}\isamarkupfalse%
    3.30 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
    3.31 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
    3.32  \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    3.33  \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
    3.34  \endisatagquote
    3.35 @@ -442,7 +442,7 @@
    3.36  %
    3.37  \isatagquote
    3.38  \isacommand{lemma}\isamarkupfalse%
    3.39 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
    3.40 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
    3.41  \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    3.42  \ simp%
    3.43  \endisatagquote
    3.44 @@ -463,7 +463,7 @@
    3.45  %
    3.46  \isatagquote
    3.47  \isacommand{lemma}\isamarkupfalse%
    3.48 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
    3.49 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
    3.50  \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    3.51  \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
    3.52  \endisatagquote
    3.53 @@ -491,10 +491,10 @@
    3.54    on code equations.
    3.55  
    3.56    \begin{warn}
    3.57 -    The attribute \emph{code unfold}
    3.58 -    associated with the \isa{SML\ code\ generator} also applies to
    3.59 -    the \isa{generic\ code\ generator}:
    3.60 -    \emph{code unfold} implies \emph{code inline}.
    3.61 +
    3.62 +    Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
    3.63 +    preprocessor of the ancient \isa{SML\ code\ generator}; in case
    3.64 +    this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
    3.65    \end{warn}%
    3.66  \end{isamarkuptext}%
    3.67  \isamarkuptrue%