%
\begin{isabellebody}%
\def\isabellecontext{Further}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Further\isanewline
\isakeyword{imports}\ Setup\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsection{Further issues \label{sec:further}%
}
\isamarkuptrue%
%
\isamarkupsubsection{Modules namespace%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} command it is possible to
leave out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} part; then code is
distributed over different modules, where the module name space
roughly is induced by the Isabelle theory name space.
Then sometimes the awkward situation occurs that dependencies
between definitions introduce cyclic dependencies between modules,
which in the \isa{Haskell} world leaves you to the mercy of the
\isa{Haskell} implementation you are using, while for \isa{SML}/\isa{OCaml} 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%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}\isamarkupfalse%
\ SML\isanewline
\ \ A\ ABC\isanewline
\ \ B\ ABC\isanewline
\ \ C\ ABC%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent we explicitly map all those modules on \emph{ABC},
resulting in an ad-hoc merge of this three modules at serialisation
time.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Locales and interpretation%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A technical issue comes to surface when generating code from
specifications stemming from locale interpretation.
Let us assume a locale specifying a power operation on arbitrary
types:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{locale}\isamarkupfalse%
\ power\ {\isaliteral{3D}{\isacharequal}}\isanewline
\ \ \isakeyword{fixes}\ power\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isakeyword{assumes}\ power{\isaliteral{5F}{\isacharunderscore}}commute{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}power\ x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ power\ y\ {\isaliteral{3D}{\isacharequal}}\ power\ y\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ power\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{begin}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Inside that locale we can lift \isa{power} to exponent
lists by means of specification relative to that locale:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{primrec}\isamarkupfalse%
\ powers\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}powers\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ id{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}powers\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ power\ x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ powers\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ powers{\isaliteral{5F}{\isacharunderscore}}append{\isaliteral{3A}{\isacharcolon}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}powers\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ powers\ xs\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ powers\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}induct\ xs{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ powers{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{3A}{\isacharcolon}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}powers\ xs\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ power\ x\ {\isaliteral{3D}{\isacharequal}}\ power\ x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ powers\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}induct\ xs{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ del{\isaliteral{3A}{\isacharcolon}}\ o{\isaliteral{5F}{\isacharunderscore}}apply\ id{\isaliteral{5F}{\isacharunderscore}}apply\ add{\isaliteral{3A}{\isacharcolon}}\ o{\isaliteral{5F}{\isacharunderscore}}assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
\ \ \ \ \ \ simp\ del{\isaliteral{3A}{\isacharcolon}}\ o{\isaliteral{5F}{\isacharunderscore}}apply\ add{\isaliteral{3A}{\isacharcolon}}\ o{\isaliteral{5F}{\isacharunderscore}}assoc\ power{\isaliteral{5F}{\isacharunderscore}}commute{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ powers{\isaliteral{5F}{\isacharunderscore}}rev{\isaliteral{3A}{\isacharcolon}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}powers\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ powers\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}induct\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ powers{\isaliteral{5F}{\isacharunderscore}}append\ powers{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
After an interpretation of this locale (say, \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} \isa{fun{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{3A}{\isacharcolon}}} \isa{{\isaliteral{22}{\isachardoublequote}}power\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}), one would expect to have a constant \isa{fun{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a} for which code
can be generated. But this not the case: internally, the term
\isa{fun{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{2E}{\isachardot}}powers} is an abbreviation for the foundational
term \isa{{\isaliteral{22}{\isachardoublequote}}power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
(see \cite{isabelle-locale} for the details behind).
Fortunately, with minor effort the desired behaviour can be
achieved. First, a dedicated definition of the constant on which
the local \isa{powers} after interpretation is supposed to be
mapped on:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{definition}\isamarkupfalse%
\ funpows\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
\ \ {\isaliteral{5B}{\isacharbrackleft}}code\ del{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}funpows\ {\isaliteral{3D}{\isacharequal}}\ power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ f{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent In general, the pattern is \isa{c\ {\isaliteral{3D}{\isacharequal}}\ t} where \isa{c}
is the name of the future constant and \isa{t} the foundational
term corresponding to the local constant after interpretation.
The interpretation itself is enriched with an equation \isa{t\ {\isaliteral{3D}{\isacharequal}}\ c}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
\ fun{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{3A}{\isacharcolon}}\ power\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ f{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ funpows{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isaliteral{5F}{\isacharunderscore}}locales\isanewline
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ fun{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}iff\ funpow{\isaliteral{5F}{\isacharunderscore}}mult\ mult{\isaliteral{5F}{\isacharunderscore}}commute\ funpows{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This additional equation is trivially proved by the
definition itself.
After this setup procedure, code generation can continue as usual:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isatagquotetypewriter
%
\begin{isamarkuptext}%
funpow\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
funpow\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ f\ {\isaliteral{3D}{\isacharequal}}\ id{\isaliteral{3B}{\isacharsemicolon}}\isanewline
funpow\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ f\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{2E}{\isachardot}}\ funpow\ n\ f{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
funpows\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}Nat{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
funpows\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ id{\isaliteral{3B}{\isacharsemicolon}}\isanewline
funpows\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ funpow\ x\ {\isaliteral{2E}{\isachardot}}\ funpows\ xs{\isaliteral{3B}{\isacharsemicolon}}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquotetypewriter
{\isafoldquotetypewriter}%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isamarkupsubsection{Imperative data structures%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
If you consider imperative data structures as inevitable for a
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
is available in session \isa{Imperative{\isaliteral{5F}{\isacharunderscore}}HOL}, together with a
short primer document.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{ML system interfaces \label{sec:ml}%
}
\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 fundamental ML
interfaces.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Managing executable content%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
\indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
\indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: |\isasep\isanewline%
\verb| string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
\verb| -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
\indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
\indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
\verb| -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool| \\
\indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
\end{mldecls}
\begin{description}
\item \verb|Code.read_const|~\isa{thy}~\isa{s}
reads a constant as a concrete term expression \isa{s}.
\item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
theorem \isa{thm} to executable content.
\item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
theorem \isa{thm} from executable content, if present.
\item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
the preprocessor simpset.
\item \verb|Code_Preproc.add_functrans|~\isa{{\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ f{\isaliteral{29}{\isacharparenright}}}~\isa{thy} adds
function transformer \isa{f} (named \isa{name}) to executable content;
\isa{f} is a transformer of the code equations belonging
to a certain function definition, depending on the
current theory context. Returning \isa{NONE} indicates that no
transformation took place; otherwise, the whole process will be iterated
with the new code equations.
\item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
function transformer named \isa{name} from executable content.
\item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
a datatype to executable content, with generation
set \isa{cs}.
\item \verb|Code.get_type_of_constr_or_abstr|~\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
%
\isamarkupsubsubsection{Data depending on the theory's executable content%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
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.
Due to incrementality of code generation, changes in the theory's
executable content have to be propagated in a certain fashion.
Additionally, such changes may occur not only during theory
extension but also during theory merge, which is a little bit nasty
from an implementation point of view. The framework provides a
solution to this technical challenge by providing a functorial data
slot \verb|Code_Data|; on instantiation of this functor, the
following types and operations are required:
\medskip
\begin{tabular}{l}
\isa{type\ T} \\
\isa{val\ empty{\isaliteral{3A}{\isacharcolon}}\ T} \\
\end{tabular}
\begin{description}
\item \isa{T} the type of data to store.
\item \isa{empty} initial (empty) data.
\end{description}
\noindent An instance of \verb|Code_Data| provides the
following interface:
\medskip
\begin{tabular}{l}
\isa{change{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} \\
\isa{change{\isaliteral{5F}{\isacharunderscore}}yield{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ T{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ T}
\end{tabular}
\begin{description}
\item \isa{change} update of current data (cached!) by giving a
continuation.
\item \isa{change{\isaliteral{5F}{\isacharunderscore}}yield} update with side result.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: