--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Wed Oct 01 13:33:54 2008 +0200
@@ -0,0 +1,255 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{ML}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{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 important ML interfaces.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Executable theory content: \isa{Code}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This Pure module implements the core notions of
+ executable content of a theory.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Managing executable content%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
+ \indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
+ \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory| \\
+ \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
+ \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
+ \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
+\verb| -> theory -> theory| \\
+ \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
+ \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
+ \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
+\verb| -> (string * sort) list * (string * typ list) list| \\
+ \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
+ \end{mldecls}
+
+ \begin{description}
+
+ \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.add_eqnl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
+ suspended defining equations \isa{lthms} for constant
+ \isa{const} to executable content.
+
+ \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes
+ the preprocessor simpset.
+
+ \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
+ function transformer \isa{f} (named \isa{name}) to executable content;
+ \isa{f} is a transformer of the defining 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 defining equations.
+
+ \item \verb|Code.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_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{Auxiliary%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
+ \indexml{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
+ \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: MetaSimplifier.simpset -> thm -> thm| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s}
+ reads a constant as a concrete term expression \isa{s}.
+
+ \item \verb|Code_Unit.head_eqn|~\isa{thy}~\isa{thm}
+ extracts the constant and its type from a defining equation \isa{thm}.
+
+ \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm}
+ rewrites a defining equation \isa{thm} with a simpset \isa{ss};
+ only arguments and right hand side are rewritten,
+ not the head of the defining equation.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Implementing code generator applications%
+}
+\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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Data depending on the theory's executable content%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+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|CodeDataFun|; on instantiation
+ of this functor, the following types and operations
+ are required:
+
+ \medskip
+ \begin{tabular}{l}
+ \isa{type\ T} \\
+ \isa{val\ empty{\isacharcolon}\ T} \\
+ \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
+ \end{tabular}
+
+ \begin{description}
+
+ \item \isa{T} the type of data to store.
+
+ \item \isa{empty} initial (empty) data.
+
+ \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
+ \isa{consts} indicates the kind
+ of change: \verb|NONE| stands for a fundamental change
+ which invalidates any existing code, \isa{SOME\ consts}
+ hints that executable content for constants \isa{consts}
+ has changed.
+
+ \end{description}
+
+ \noindent An instance of \verb|CodeDataFun| provides the following
+ interface:
+
+ \medskip
+ \begin{tabular}{l}
+ \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}
+
+ \begin{description}
+
+ \item \isa{get} retrieval of the current data.
+
+ \item \isa{change} update of current data (cached!)
+ by giving a continuation.
+
+ \item \isa{change{\isacharunderscore}yield} update with side result.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\bigskip
+
+ \emph{Happy proving, happy hacking!}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: