# HG changeset patch
# User haftmann
# Date 1163453483 -3600
# Node ID 74c1da5d44be58986c127fc69fe1b4c32d15004b
# Parent  fccc48e844f5c0ce2fbfa3c7fa2601ec4d173a88
upd

diff -r fccc48e844f5 -r 74c1da5d44be doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Mon Nov 13 22:21:09 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Mon Nov 13 22:31:23 2006 +0100
@@ -69,7 +69,11 @@
   structuring the process
   of code generation into a small set of orthogonal principles
   while achieving a big coverage of application areas
-  with maximum flexibility.%
+  with maximum flexibility.
+
+  For readers, some familiarity and experience
+  with the the ingredients
+  of the HOL \emph{Main} theory is assumed.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -107,7 +111,14 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The code generator employs a notion of executability
+\begin{figure}[h]
+  \centering
+  \includegraphics[width=0.7\textwidth]{codegen_process}
+  \caption{code generator -- processing overview}
+  \label{fig:process}
+  \end{figure}
+
+  The code generator employs a notion of executability
   for three foundational executable ingredients known
   from functional programming:
   \emph{function equations}, \emph{datatypes}, and
@@ -141,13 +152,6 @@
 
   \end{itemize}
 
-  \begin{figure}[h]
-  \centering
-  \includegraphics[width=0.3\textwidth]{codegen_process}
-  \caption{code generator -- processing overview}
-  \label{fig:process}
-  \end{figure}
-
   From these steps, only the two last are carried out
   outside the logic; by keeping this layer as
   thin as possible, the amount of code to trust is
@@ -183,7 +187,7 @@
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
 \ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
-The \isasymCODEGEN command takes a space-separated list of
+The \isa{{\isasymCODEGEN}} command takes a space-separated list of
   constants together with \qn{serialization directives}
   in parentheses. These start with a \qn{target language}
   identifier, followed by arguments, their semantics
@@ -286,7 +290,7 @@
 %
 \begin{isamarkuptext}%
 The list of all function equations in a theory may be inspected
-  using the \isasymPRINTCODETHMS command:%
+  using the \isa{{\isasymPRINTCODETHMS}} command:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
@@ -300,8 +304,9 @@
   whether it provides one.
 
   The typical HOL tools are already set up in a way that
-  function definitions introduced by \isasymFUN, \isasymFUNCTION,
-  \isasymPRIMREC, \isasymRECDEF are implicitly propagated
+  function definitions introduced by \isa{{\isasymFUN}},
+  \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}
+  \isa{{\isasymRECDEF}} are implicitly propagated
   to this function equation table. Specific theorems may be
   selected using an attribute: \emph{code func}. As example,
   a weight selector function:%
@@ -514,14 +519,14 @@
   Implementation of caching is supposed to transparently
   hid away the details from the user.  Anyway, caching
   reaches the surface by using a slightly more general form
-  of the \isasymCODEGEN: either the list of constants or the
+  of the \isa{{\isasymCODEGEN}}: either the list of constants or the
   list of serialization expressions may be dropped.  If no
   serialization expressions are given, only abstract code
   is generated and cached; if no constants are given, the
   current cache is serialized.
 
-  For explorative reasons, an extended version of the
-  \isasymCODEGEN command may prove useful:%
+  For explorative purpose, an extended version of the
+  \isa{{\isasymCODEGEN}} command may prove useful:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
@@ -549,7 +554,7 @@
 
   \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
     for exhaustive syntax diagrams.
-  \item or \fixme{ref} which deals with foundational issues
+  \item or \fixme[ref] which deals with foundational issues
     of the code generator framework.
 
   \end{itemize}%
@@ -571,12 +576,12 @@
 
     \item[ExecutableSet] allows to generate code
        for finite sets using lists.
-    \item[ExecutableRat] implements rational
+    \item[ExecutableRat] \label{exec_rat} implements rational
        numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
-    \item[EfficientNat] implements natural numbers by integers,
+    \item[EfficientNat] \label{eff_nat} implements natural numbers by integers,
        which in general will result in higher efficency; pattern
        matching with \isa{{\isadigit{0}}} / \isa{Suc}
-       is eliminated. \label{eff_nat}
+       is eliminated.
     \item[MLString] provides an additional datatype \isa{mlstring};
        in the HOL default setup, strings in HOL are mapped to list
        of chars in SML; values of type \isa{mlstring} are
@@ -668,7 +673,7 @@
 %
 \begin{isamarkuptext}%
 The current set of inline theorems may be inspected using
-  the \isasymPRINTCODETHMS command.
+  the \isa{{\isasymPRINTCODETHMS}} command.
 
   \emph{Inline procedures} are a generalized version of inline
   theorems written in ML -- rewrite rules are generated dependent
@@ -681,7 +686,8 @@
   transforming a list of function theorems to another
   list of function theorems, provided that neither the heading
   constant nor its type change.  The \isa{{\isadigit{0}}} / \isa{Suc}
-  pattern elimination implemented in \secref{eff_nat} uses this
+  pattern elimination implemented in
+  theory EfficientNat (\secref{eff_nat}) uses this
   interface.
 
   \begin{warn}
@@ -709,27 +715,24 @@
 \isacommand{fun}\isamarkupfalse%
 \isanewline
 \ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}\isanewline
-\isacommand{termination}\isamarkupfalse%
+\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
+\isadelimtt
 %
-\isadelimproof
-\ %
-\endisadelimproof
+\endisadelimtt
+%
+\isatagtt
 %
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+\isanewline
 %
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
+\endisadelimtt
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
-\lstsml{Thy/examples/bool1.ML}
+\lstsml{Thy/examples/bool_literal.ML}
 
   Though this is correct code, it is a little bit unsatisfactory:
   boolean values and operators are materialized as distinguished
@@ -742,20 +745,33 @@
   \qn{custom serializations}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ bool\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
 \begin{isamarkuptext}%
-The \isasymCODETYPE commad takes a type constructor
+The \isa{{\isasymCODETYPE}} commad takes a type constructor
   as arguments together with a list of custom serializations.
   Each custom serialization starts with a target language
   identifier followed by an expression, which during
   code serialization is inserted whenever the type constructor
-  would occur.  For constants, \isasymCODECONST implements
-  the corresponding mechanism.  Each \qt{\_} in
+  would occur.  For constants, \isa{{\isasymCODECONST}} implements
+  the corresponding mechanism.  Each ``\verb|_|'' in
   a serialization expression is treated as a placeholder
   for the type constructor's (the constant's) arguments.%
 \end{isamarkuptext}%
@@ -765,37 +781,57 @@
 \ \ bool\ true\ false%
 \begin{isamarkuptext}%
 To assert that the existing \qt{bool}, \qt{true} and \qt{false}
-  is not used for generated code, we use \isasymCODERESERVED.
+  is not used for generated code, we use \isa{{\isasymCODERESERVED}}.
 
   After this setup, code looks quite more readable:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
-\lstsml{Thy/examples/bool2.ML}
+\lstsml{Thy/examples/bool_mlbool.ML}
 
   This still is not perfect: the parentheses
-  around \qt{andalso} are superfluous.  Though the serializer
+  around the \qt{andalso} expression are superfluous.
+  Though the serializer
   by no means attempts to imitate the rich Isabelle syntax
   framework, it provides some common idioms, notably
   associative infixes with precedences which may be used here:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{3}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
-\lstsml{Thy/examples/bool3.ML}
+\lstsml{Thy/examples/bool_infix.ML}
 
   Next, we try to map HOL pairs to SML pairs, using the
-  infix \qt{ * } type constructor and parentheses:%
+  infix ``\verb|*|'' type constructor and parentheses:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isanewline
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ {\isacharasterisk}\isanewline
 \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -803,12 +839,19 @@
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ Pair\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
 \begin{isamarkuptext}%
-The initial bang \qt{!} tells the serializer to never put
+The initial bang ``\verb|!|'' tells the serializer to never put
   parentheses around the whole expression (they are already present),
   while the parentheses around argument place holders
   tell not to put parentheses around the arguments.
-  The slash \qt{/} (followed by arbitrary white space)
+  The slash ``\verb|/|'' (followed by arbitrary white space)
   inserts a space which may be used as a break if necessary
   during pretty printing.
 
@@ -834,6 +877,12 @@
   integers:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ int\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}int{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -841,7 +890,14 @@
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharasterisk}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
 \ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
@@ -861,9 +917,10 @@
 
   A further noteworthy details is that any special
   character in a custom serialization may be quoted
-  using \qt{'}; thus, in \qt{fn '\_ => \_} the first
-  \qt{'\_} is a proper underscore while the
-  second \qt{\_} is a placeholder.
+  using ``\verb|'|''; thus, in
+  ``\verb|fn '_ => _|'' the first
+  ``\verb|_|'' is a proper underscore while the
+  second ``\verb|_|'' is a placeholder.
 
   The HOL theories provide further
   examples for custom serializations and form
@@ -888,25 +945,9 @@
 \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
 \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
 \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
-\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isacommand{termination}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}length\ o\ snd\ o\ snd{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
+\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-The membership test during preprocessing is rewriting,
+The membership test during preprocessing is rewritten,
   resulting in \isa{op\ mem}, which itself
   performs an explicit equality check.%
 \end{isamarkuptext}%
@@ -982,9 +1023,22 @@
 Examine the following:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
 \begin{isamarkuptext}%
 What is wrong here? Since \isa{op\ {\isacharequal}} is nothing else then
   a plain constant, this customary serialization will refer
@@ -993,10 +1047,23 @@
   by using the overloaded constant \isa{Code{\isacharunderscore}Generator{\isachardot}eq}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\isamarkupsubsubsection{typedecls interpretated by customary serializations%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isamarkupsubsubsection{typedecls interpreted by customary serializations%
 }
 \isamarkuptrue%
 %
@@ -1013,25 +1080,22 @@
 \ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}key\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isacommand{termination}\isamarkupfalse%
 %
-\isadelimproof
-\ %
-\endisadelimproof
+\isadelimtt
 %
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}length\ o\ fst{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
+\endisadelimtt
 %
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ key\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}string{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
 \begin{isamarkuptext}%
 This, though, is not sufficient: \isa{key} is no instance
   of \isa{eq} since \isa{key} is no datatype; the instance
@@ -1055,10 +1119,23 @@
 %
 \endisadelimproof
 \isanewline
+%
+\isadelimtt
 \isanewline
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
 \begin{isamarkuptext}%
 Then everything goes fine:%
 \end{isamarkuptext}%
@@ -1078,7 +1155,7 @@
 Another subtlety
   enters the stage when definitions of overloaded constants
   are dependent on operational equality.  For example, let
-  us define a lexicographic ordering on tuples: \\%
+  us define a lexicographic ordering on tuples:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1177,7 +1254,7 @@
 For convenience, the default
   HOL setup for Haskell maps the \isa{eq} class to
   its counterpart in Haskell, giving custom serializations
-  for the class (\isasymCODECLASS) and its operation:%
+  for the class (\isa{{\isasymCODECLASS}}) and its operation:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1194,6 +1271,12 @@
 %
 \endisadelimML
 \isanewline
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
 \ eq\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ eq\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -1202,6 +1285,13 @@
 \ eq\isanewline
 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\isanewline
 %
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
 \isadelimML
 %
 \endisadelimML
@@ -1241,41 +1331,197 @@
 %
 \endisadelimproof
 \isanewline
+%
+\isadelimtt
 \isanewline
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ bar\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
 \begin{isamarkuptext}%
 The code generator would produce
     an additional instance, which of course is rejected.
     To suppress this additional instance, use
-    \isasymCODEINSTANCE:%
+    \isa{{\isasymCODEINSTANCE}}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
 \isamarkupsubsection{Types matter%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Imagine the following quick-and-dirty setup for implementing
-  some sets as lists:%
+  some kind of sets as lists in SML:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ set\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharunderscore}\ list{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ insert\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharcolon}{\isacharcolon}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharcolon}{\isacharcolon}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+\isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbraceright}{\isachardoublequoteclose}%
+\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+Then code generation for \isa{dummy{\isacharunderscore}set} will fail.
+  Why? A glimpse at the function equations will offer:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
+\ {\isacharparenleft}insert{\isacharparenright}%
+\begin{isamarkuptext}%
+This reveals the function equation \isa{insert\ {\isacharquery}a\ {\isacharquery}B\ {\isasymequiv}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}a{\isacharbraceright}\ {\isasymunion}\ {\isacharquery}B}
+  for \isa{insert}, which is operationally meaningless
+  but forces an equality constraint on the set members
+  (which is not satisfiable if the set members are functions).
+  Even when using set of natural numbers (which are an instance
+  of \emph{eq}), we run into a problem:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}foobar{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+In this case the serializer would complain that \isa{insert}
+  expects dictionaries (namely an \emph{eq} dictionary) but
+  has also been given a customary serialization.
+
+  The solution to this dilemma:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}insert\ {\isacharequal}\ insert{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ dummy{\isacharunderscore}set\ foobar{\isacharunderscore}set\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}dirty{\isacharunderscore}set{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/dirty_set.ML}
+
+  Reflexive function equations by convention are dropped.
+  But their presence prevents primitive definitions to be
+  used as function equations:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
+\ {\isacharparenleft}insert{\isacharparenright}%
+\begin{isamarkuptext}%
+will show \emph{no} function equations for insert.
+
+  Note that the sort constraints of reflexive equations
+  are considered; so%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}insert\ {\isasymColon}\ {\isacharprime}a{\isasymColon}eq\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}\ {\isacharequal}\ insert{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+would mean nothing else than to introduce the evil
+  sort constraint by hand.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Cyclic module dependencies%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Sometimes the awkward situation occurs that dependencies
+  between definitions introduce cyclic dependencies
+  between modules, which in the Haskell world leaves
+  you to the mercy of the Haskell implementation you are using,
+  while for SML code generation is not possible.
+
+  A solution is to declare module names explicitly.
+  Let use assume the three cyclically dependent
+  modules are named \emph{A}, \emph{B} and \emph{C}.
+  Then, by stating%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}modulename}\isamarkupfalse%
+\ SML\isanewline
+\ \ A\ ABC\isanewline
+\ \ B\ ABC\isanewline
+\ \ C\ ABC%
+\begin{isamarkuptext}%
+we explicitly map all those modules on \emph{ABC},
+  resulting in an ad-hoc merge of this three modules
+  at serialization time.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Axiomatic extensions%
 }
 \isamarkuptrue%
@@ -1283,9 +1529,81 @@
 \begin{isamarkuptext}%
 \begin{warn}
     The extensions introduced in this section, though working
-    in practice, are not the cream of the crop.  They will
+    in practice, are not the cream of the crop, as you
+    will notice during reading.  They will
     eventually be replaced by more mature approaches.
-  \end{warn}%
+  \end{warn}
+
+  Sometimes equalities are taken for granted which are
+  not derivable inside the HOL logic but are silently assumed
+  to hold for executable code.  For example, we may want
+  to identify the famous HOL constant \isa{arbitrary}
+  of type \isa{{\isacharprime}a\ option} with \isa{None}.
+  By brute force:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{axiomatization}\isamarkupfalse%
+\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}arbitrary\ {\isacharequal}\ None{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+However this has to be considered harmful since this axiom,
+  though probably justifiable for generated code, could
+  introduce serious inconsistencies into the logic.
+
+  So, there is a distinguished construct for stating axiomatic
+  equalities of constants which apply only for code generation.
+  Before introducing this, here is a convenient place to describe
+  shortly how to deal with some restrictions the type discipline
+  imposes.
+
+  By itself, the constant \isa{arbitrary} is a non-overloaded
+  polymorphic constant.  So, there is no way to distinguish
+  different versions of \isa{arbitrary} for different types
+  inside the code generator framework.  However, inlining
+  theorems together with auxiliary constants provide a solution:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ arbitrary{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ option{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbrackleft}symmetric{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}arbitrary{\isacharunderscore}option\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+By that, we replace any \isa{arbitrary} with option type
+  by \isa{arbitrary{\isacharunderscore}option} in function equations.
+
+  For technical reasons, we further have to provide a
+  synonym for \isa{None} which in code generator view
+  is a function rather than a datatype constructor%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ {\isachardoublequoteopen}None{\isacharprime}\ {\isacharequal}\ None{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+Then finally we are enabled to use \isa{{\isasymCODEAXIOMS}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}axioms}\isamarkupfalse%
+\isanewline
+\ \ arbitrary{\isacharunderscore}option\ {\isasymequiv}\ None{\isacharprime}%
+\begin{isamarkuptext}%
+A dummy example:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ dummy{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ Some\ x{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ dummy{\isacharunderscore}option\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/arbitrary.ML}
+
+  Another axiomatic extension is code generation
+  for abstracted types.  For this, the  
+  ExecutableRat (see \secref{exec_rat})
+  forms a good example.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1293,10 +1611,24 @@
 }
 \isamarkuptrue%
 %
+\begin{isamarkuptext}%
+Since the code generator framework not only aims to provide
+  a nice Isar interface but also to form a base for
+  code-generation-based applications, here a short
+  description of the most important ML interfaces.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Constants with type discipline: codegen\_consts.ML%
 }
 \isamarkuptrue%
 %
+\begin{isamarkuptext}%
+This Pure module manages identification of (probably overloaded)
+  constants by unique identifiers.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimmlref
 %
 \endisadelimmlref
@@ -1305,12 +1637,27 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const| \\
-  \indexml{CodegenConsts.inst-of-typ}\verb|CodegenConsts.inst_of_typ: theory -> string * typ -> CodegenConsts.const| \\
+  \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const = string * typ list| \\
+  \indexml{CodegenConsts.norm-of-typ}\verb|CodegenConsts.norm_of_typ: theory -> string * typ -> CodegenConsts.const| \\
   \indexml{CodegenConsts.typ-of-inst}\verb|CodegenConsts.typ_of_inst: theory -> CodegenConsts.const -> string * typ| \\
-  \indexml{CodegenConsts.norm}\verb|CodegenConsts.norm: theory -> CodegenConsts.const -> CodegenConsts.const| \\
-  \indexml{CodegenConsts.norm-of-typ}\verb|CodegenConsts.norm_of_typ: theory -> string * typ -> CodegenConsts.const|
-  \end{mldecls}%
+ \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|CodegenConsts.const| is the identifier type:
+     the product of a \emph{string} with a list of \emph{typs}.
+     The \emph{string} is the constant name as represented inside Isabelle;
+     the \emph{typs} are a type instantiation in the sense of System F,
+     with canonical names for type variables.
+
+  \item \verb|CodegenConsts.norm_of_typ|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
+     maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} to its canonical identifier.
+
+  \item \verb|CodegenConsts.typ_of_inst|~\isa{thy}~\isa{const}
+     maps a canonical identifier \isa{const} to a constant
+     expression with appropriate type.
+
+  \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1343,9 +1690,15 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{CodegenData.lthms}\verb|type CodegenData.lthms| \\
-  \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> CodegenData.lthms|
-  \end{mldecls}%
+  \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> thm list Susp.T|
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|CodegenData.lazy|~\isa{f} turns an abstract
+     theorem computation \isa{f} into a suspension of theorems.
+
+  \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1370,21 +1723,134 @@
 \begin{mldecls}
   \indexml{CodegenData.add-func}\verb|CodegenData.add_func: thm -> theory -> theory| \\
   \indexml{CodegenData.del-func}\verb|CodegenData.del_func: thm -> theory -> theory| \\
-  \indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * CodegenData.lthms -> theory -> theory| \\
-  \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * (((string * sort) list * (string * typ list) list) * CodegenData.lthms) -> theory -> theory| \\
-  \indexml{CodegenData.del-datatype}\verb|CodegenData.del_datatype: string -> theory -> theory| \\
+  \indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory| \\
   \indexml{CodegenData.add-inline}\verb|CodegenData.add_inline: thm -> theory -> theory| \\
   \indexml{CodegenData.del-inline}\verb|CodegenData.del_inline: thm -> theory -> theory| \\
-  \indexml{CodegenData.add-inline-proc}\verb|CodegenData.add_inline_proc: (theory -> cterm list -> thm list) -> theory -> theory| \\
-  \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: (theory -> thm list -> thm list) -> theory -> theory| \\
-  \indexml{CodegenData.these-funcs}\verb|CodegenData.these_funcs: theory -> CodegenConsts.const -> thm list| \\
-  \indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) option| \\
+  \indexml{CodegenData.add-inline-proc}\verb|CodegenData.add_inline_proc: (theory -> cterm list -> thm list)|\isasep\isanewline%
+\verb|    -> theory -> theory| \\
+  \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: (theory -> thm list -> thm list)|\isasep\isanewline%
+\verb|    -> theory -> theory| \\
+  \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * (((string * sort) list * (string * typ list) list)|\isasep\isanewline%
+\verb|    * thm list Susp.T) -> theory -> theory| \\
+  \indexml{CodegenData.del-datatype}\verb|CodegenData.del_datatype: string -> theory -> theory| \\
+  \indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string|\isasep\isanewline%
+\verb|    -> ((string * sort) list * (string * typ list) list) option| \\
   \indexml{CodegenData.get-datatype-of-constr}\verb|CodegenData.get_datatype_of_constr: theory -> CodegenConsts.const -> string option|
   \end{mldecls}
 
   \begin{description}
 
-  \item \verb|CodegenData.add_func|~\isa{thm}
+  \item \verb|CodegenData.add_func|~\isa{thm}~\isa{thy} adds function
+     theorem \isa{thm} to executable content.
+
+  \item \verb|CodegenData.del_func|~\isa{thm}~\isa{thy} removes function
+     theorem \isa{thm} from executable content, if present.
+
+  \item \verb|CodegenData.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
+     suspended function equations \isa{lthms} for constant
+     \isa{const} to executable content.
+
+  \item \verb|CodegenData.add_inline|~\isa{thm}~\isa{thy} adds
+     inlining theorem \isa{thm} to executable content.
+
+  \item \verb|CodegenData.del_inline|~\isa{thm}~\isa{thy} remove
+     inlining theorem \isa{thm} from executable content, if present.
+
+  \item \verb|CodegenData.add_inline_proc|~\isa{f}~\isa{thy} adds
+     inline procedure \isa{f} to executable content;
+     \isa{f} is a computation of rewrite rules dependent on
+     the current theory context and the list of all arguments
+     and right hand sides of the function equations belonging
+     to a certain function definition.
+
+  \item \verb|CodegenData.add_preproc|~\isa{f}~\isa{thy} adds
+     generic preprocessor \isa{f} to executable content;
+     \isa{f} is a transformation of the function equations belonging
+     to a certain function definition, depending on the
+     current theory context.
+
+  \item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}spec{\isacharcomma}\ cert{\isacharparenright}{\isacharparenright}}~\isa{thy} adds
+     a datatype to executable content, with type constructor
+     \isa{name} and specification \isa{spec}; \isa{spec} is
+     a pair consisting of a list of type variable with sort
+     constraints and a list of constructors with name
+     and types of arguments.  The addition as datatype
+     has to be justified giving a certificate of suspended
+     theorems as witnesses for injectiveness and distinctness.
+
+  \item \verb|CodegenData.del_datatype|~\isa{name}~\isa{thy}
+     remove a datatype from executable content, if present.
+
+  \item \verb|CodegenData.get_datatype_of_constr|~\isa{thy}~\isa{const}
+     returns type constructor corresponding to
+     constructor \isa{const}; returns \isa{NONE}
+     if \isa{const} is no constructor.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Function equation systems: codegen\_funcgr.ML%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Out of the executable content of a theory, a normalized
+  function equation systems may be constructed containing
+  function definitions for constants.  The system is cached
+  until its underlying executable content changes.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{CodegenFuncgr.T}\verb|type CodegenFuncgr.T| \\
+  \indexml{CodegenFuncgr.make}\verb|CodegenFuncgr.make: theory -> CodegenConsts.const list -> CodegenFuncgr.T| \\
+  \indexml{CodegenFuncgr.funcs}\verb|CodegenFuncgr.funcs: CodegenFuncgr.T -> CodegenConsts.const -> thm list| \\
+  \indexml{CodegenFuncgr.typ}\verb|CodegenFuncgr.typ: CodegenFuncgr.T -> CodegenConsts.const -> typ| \\
+  \indexml{CodegenFuncgr.deps}\verb|CodegenFuncgr.deps: CodegenFuncgr.T|\isasep\isanewline%
+\verb|    -> CodegenConsts.const list -> CodegenConsts.const list list| \\
+  \indexml{CodegenFuncgr.all}\verb|CodegenFuncgr.all: CodegenFuncgr.T -> CodegenConsts.const list|
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|CodegenFuncgr.T| represents
+    a normalized function equation system.
+
+  \item \verb|CodegenFuncgr.make|~\isa{thy}~\isa{cs}
+    returns a normalized function equation system,
+    with the assertion that it contains any function
+    definition for constants \isa{cs} (if existing).
+
+  \item \verb|CodegenFuncgr.funcs|~\isa{funcgr}~\isa{c}
+    retrieves function definition for constant \isa{c}.
+
+  \item \verb|CodegenFuncgr.typ|~\isa{funcgr}~\isa{c}
+    retrieves function type for constant \isa{c}.
+
+  \item \verb|CodegenFuncgr.deps|~\isa{funcgr}~\isa{cs}
+    returns the transitive closure of dependencies for
+    constants \isa{cs} as a partitioning where each partition
+    corresponds to a strongly connected component of
+    dependencies and any partition does \emph{not}
+    depend on partitions further left.
+
+  \item \verb|CodegenFuncgr.all|~\isa{funcgr}
+    returns all currently represented constants.
 
   \end{description}%
 \end{isamarkuptext}%
@@ -1414,9 +1880,34 @@
   \indexml{CodegenConsts.consts-of}\verb|CodegenConsts.consts_of: theory -> term -> CodegenConsts.const list| \\
   \indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
   \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
+  \indexmlstructure{CodegenFuncgr.Constgraph}\verb|structure CodegenFuncgr.Constgraph| \\
   \indexml{CodegenData.typ-func}\verb|CodegenData.typ_func: theory -> thm -> typ| \\
   \indexml{CodegenData.rewrite-func}\verb|CodegenData.rewrite_func: thm list -> thm -> thm| \\
-  \end{mldecls}%
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|CodegenConsts.const_ord|,~\verb|CodegenConsts.eq_const|
+     provide order and equality on constant identifiers.
+
+  \item \verb|CodegenConsts.Consttab|,~\verb|CodegenFuncgr.Constgraph|
+     provide advanced data structures with constant identifiers as keys.
+
+  \item \verb|CodegenConsts.consts_of|~\isa{thy}~\isa{t}
+     returns all constant identifiers mentioned in a term \isa{t}.
+
+  \item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s}
+     reads a constant as a concrete term expression \isa{s}.
+
+  \item \verb|CodegenData.typ_func|~\isa{thy}~\isa{thm}
+     extracts the type of a constant in a function equation \isa{thm}.
+
+  \item \verb|CodegenData.rewrite_func|~\isa{rews}~\isa{thm}
+     rewrites a function equation \isa{thm} with a set of rewrite
+     rules \isa{rews}; only arguments and right hand side are rewritten,
+     not the head of the function equation.
+
+  \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1432,11 +1923,19 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-\begin{warn}
+Implementing code generator applications on top
+  of the framework set out so far usually not only
+  involves using those primitive interfaces
+  but also storing code-dependent data and various
+  other things.
+
+  \begin{warn}
     Some interfaces discussed here have not reached
     a final state yet.
     Changes likely to occur in future.
-  \end{warn}%
+  \end{warn}
+
+  \fixme%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1444,12 +1943,118 @@
 }
 \isamarkuptrue%
 %
+\begin{isamarkuptext}%
+\medskip
+  \begin{tabular}{l}
+  \isa{val\ name{\isacharcolon}\ string} \\
+  \isa{type\ T} \\
+  \isa{val\ empty{\isacharcolon}\ T} \\
+  \isa{val\ merge{\isacharcolon}\ Pretty{\isachardot}pp\ {\isasymrightarrow}\ T\ {\isacharasterisk}\ T\ {\isasymrightarrow}\ T} \\
+  \isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
+  \end{tabular}
+
+  \medskip
+
+  \begin{tabular}{l}
+  \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
+  \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
+  \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
+  \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
+  \end{tabular}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmlfunctor{CodeDataFun}\verb|functor CodeDataFun|
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|CodeDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares code
+  dependent data according to the specification provided as
+  argument structure.  The resulting structure provides data init and
+  access operations as described above.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
 \isamarkupsubsubsection{Datatype hooks%
 }
 \isamarkuptrue%
 %
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
 \begin{isamarkuptext}%
-\emph{Happy proving, happy hacking!}%
+\begin{mldecls}
+  \indexmltype{DatatypeHooks.hook}\verb|type DatatypeHooks.hook = string list -> theory -> theory| \\
+  \indexml{DatatypeHooks.add}\verb|DatatypeHooks.add: DatatypeHooks.hook -> theory -> theory|
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{TypecopyPackage.info}\verb|type TypecopyPackage.info = {|\isasep\isanewline%
+\verb|    vs: (string * sort) list,|\isasep\isanewline%
+\verb|    constr: string,|\isasep\isanewline%
+\verb|    typ: typ,|\isasep\isanewline%
+\verb|    inject: thm,|\isasep\isanewline%
+\verb|    proj: string * typ,|\isasep\isanewline%
+\verb|    proj_def: thm|\isasep\isanewline%
+\verb|  }| \\
+  \indexml{TypecopyPackage.add-typecopy}\verb|TypecopyPackage.add_typecopy: |\isasep\isanewline%
+\verb|    bstring * string list -> typ -> (bstring * bstring) option|\isasep\isanewline%
+\verb|    -> theory -> (string * TypecopyPackage.info) * theory| \\
+  \indexml{TypecopyPackage.get-typecopies}\verb|TypecopyPackage.get_typecopies: theory -> string list| \\
+  \indexml{TypecopyPackage.get-typecopy-info}\verb|TypecopyPackage.get_typecopy_info: theory|\isasep\isanewline%
+\verb|    -> string -> TypecopyPackage.info option| \\
+  \indexmltype{TypecopyPackage.hook}\verb|type TypecopyPackage.hook| \\
+  \indexml{TypecopyPackage.add-hook}\verb|TypecopyPackage.add_hook: TypecopyPackage.hook -> theory -> theory| \\
+  \indexml{TypecopyPackage.get-spec}\verb|TypecopyPackage.get_spec: theory -> string|\isasep\isanewline%
+\verb|    -> (string * sort) list * (string * typ list) list|
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{DatatypeCodegen.hook}\verb|type DatatypeCodegen.hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list|\isasep\isanewline%
+\verb|    -> theory -> theory| \\
+  \indexml{DatatypeCodegen.add-codetypes-hook-bootstrap}\verb|DatatypeCodegen.add_codetypes_hook_bootstrap: |\isasep\isanewline%
+\verb|      DatatypeCodegen.hook -> theory -> theory|
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\begin{isamarkuptext}%
+\fixme
+%  \emph{Happy proving, happy hacking!}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %