changeset 27609 b23c9ad0fe7d parent 27557 151731493264 child 27705 f6277c8ab8ef
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 15 15:59:49 2008 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 15 16:02:07 2008 +0200
1.3 @@ -501,8 +501,8 @@
1.4  text {*
1.5    Before selected function theorems are turned into abstract
1.6    code, a chain of definitional transformation steps is carried
1.7 -  out: \emph{preprocessing}.  In essence, the preprocessort
1.8 -  consists of two components: a \emph{simpset} and \emph{function transformators}.
1.9 +  out: \emph{preprocessing}.  In essence, the preprocessor
1.10 +  consists of two components: a \emph{simpset} and \emph{function transformers}.
1.11
1.12    The \emph{simpset} allows to employ the full generality of the Isabelle
1.13    simplifier.  Due to the interpretation of theorems
1.14 @@ -546,22 +546,19 @@
1.15
1.16  text {*
1.17
1.18 -  \emph{Function transformators} provide a most general interface,
1.19 +  \emph{Function transformers} provide a very general interface,
1.20    transforming a list of function theorems to another
1.21    list of function theorems, provided that neither the heading
1.22    constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
1.23    pattern elimination implemented in
1.24 -  theory @{text "EfficientNat"} (\secref{eff_nat}) uses this
1.25 +  theory @{text "Efficient_Nat"} (\secref{eff_nat}) uses this
1.26    interface.
1.27
1.28    \noindent The current setup of the preprocessor may be inspected using
1.29    the @{text "\<PRINTCODESETUP>"} command.
1.30
1.31    \begin{warn}
1.32 -    Preprocessing is \emph{no} fix point process.  Keep this in mind when
1.33 -    setting up the preprocessor.
1.34 -
1.35 -    Further, the attribute \emph{code unfold}
1.36 +    The attribute \emph{code unfold}
1.37      associated with the existing code generator also applies to
1.38      the new one: \emph{code unfold} implies \emph{code inline}.
1.39    \end{warn}
1.40 @@ -1096,7 +1093,7 @@
1.41    @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\
1.42    @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
1.43    @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
1.44 -  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list)
1.45 +  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list option)
1.46      -> theory -> theory"} \\
1.47    @{index_ML Code.del_functrans: "string -> theory -> theory"} \\
1.48    @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
1.49 @@ -1120,14 +1117,16 @@
1.50    \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes
1.51       the preprocessor simpset.
1.52
1.54 -     function transformator @{text f} (named @{text name}) to executable content;
1.55 -     @{text f} is a transformation of the defining equations belonging
1.57 +     function transformer @{text f} (named @{text name}) to executable content;
1.58 +     @{text f} is a transformer of the defining equations belonging
1.59       to a certain function definition, depending on the
1.60 -     current theory context.
1.61 +     current theory context.  Returning @{text NONE} indicates that no
1.62 +     transformation took place;  otherwise, the whole process will be iterated
1.63 +     with the new defining equations.
1.64
1.65    \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes
1.66 -     function transformator named @{text name} from executable content.
1.67 +     function transformer named @{text name} from executable content.
1.68