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: