
diff -r 2775062fd3a9 -r 2f4684e2ea95 doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Mon Mar 02 16:58:39 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,255 +0,0 @@
-%
-\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}
-  \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.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
-  \indexdef{}{ML}{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
-  \indexdef{}{ML}{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
-  \indexdef{}{ML}{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
-\verb|    -> theory -> theory| \\
-  \indexdef{}{ML}{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
-  \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
-  \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
-\verb|    -> (string * sort) list * (string * typ list) list| \\
-  \indexdef{}{ML}{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 code 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 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.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}
-  \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
-  \indexdef{}{ML}{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
-  \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: 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 code equation \isa{thm}.
-
-  \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm}
-     rewrites a code equation \isa{thm} with a simpset \isa{ss};
-     only arguments and right hand side are rewritten,
-     not the head of the code 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}\ string\ 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:




