1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Codegen/Thy/document/ML.tex Tue Mar 03 11:00:51 2009 +0100
1.3 @@ -0,0 +1,255 @@
1.4 +%
1.5 +\begin{isabellebody}%
1.6 +\def\isabellecontext{ML}%
1.7 +%
1.8 +\isadelimtheory
1.9 +%
1.10 +\endisadelimtheory
1.11 +%
1.12 +\isatagtheory
1.13 +\isacommand{theory}\isamarkupfalse%
1.14 +\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
1.15 +\isakeyword{imports}\ Setup\isanewline
1.16 +\isakeyword{begin}%
1.17 +\endisatagtheory
1.18 +{\isafoldtheory}%
1.19 +%
1.20 +\isadelimtheory
1.21 +%
1.22 +\endisadelimtheory
1.23 +%
1.24 +\isamarkupsection{ML system interfaces \label{sec:ml}%
1.25 +}
1.26 +\isamarkuptrue%
1.27 +%
1.28 +\begin{isamarkuptext}%
1.29 +Since the code generator framework not only aims to provide
1.30 + a nice Isar interface but also to form a base for
1.31 + code-generation-based applications, here a short
1.32 + description of the most important ML interfaces.%
1.33 +\end{isamarkuptext}%
1.34 +\isamarkuptrue%
1.35 +%
1.36 +\isamarkupsubsection{Executable theory content: \isa{Code}%
1.37 +}
1.38 +\isamarkuptrue%
1.39 +%
1.40 +\begin{isamarkuptext}%
1.41 +This Pure module implements the core notions of
1.42 + executable content of a theory.%
1.43 +\end{isamarkuptext}%
1.44 +\isamarkuptrue%
1.45 +%
1.46 +\isamarkupsubsubsection{Managing executable content%
1.47 +}
1.48 +\isamarkuptrue%
1.49 +%
1.50 +\isadelimmlref
1.51 +%
1.52 +\endisadelimmlref
1.53 +%
1.54 +\isatagmlref
1.55 +%
1.56 +\begin{isamarkuptext}%
1.57 +\begin{mldecls}
1.58 + \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
1.59 + \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
1.60 + \indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
1.61 + \indexdef{}{ML}{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
1.62 + \indexdef{}{ML}{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
1.63 + \indexdef{}{ML}{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
1.64 +\verb| -> theory -> theory| \\
1.65 + \indexdef{}{ML}{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
1.66 + \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
1.67 + \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
1.68 +\verb| -> (string * sort) list * (string * typ list) list| \\
1.69 + \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
1.70 + \end{mldecls}
1.71 +
1.72 + \begin{description}
1.73 +
1.74 + \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
1.75 + theorem \isa{thm} to executable content.
1.76 +
1.77 + \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
1.78 + theorem \isa{thm} from executable content, if present.
1.79 +
1.80 + \item \verb|Code.add_eqnl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
1.81 + suspended code equations \isa{lthms} for constant
1.82 + \isa{const} to executable content.
1.83 +
1.84 + \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes
1.85 + the preprocessor simpset.
1.86 +
1.87 + \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
1.88 + function transformer \isa{f} (named \isa{name}) to executable content;
1.89 + \isa{f} is a transformer of the code equations belonging
1.90 + to a certain function definition, depending on the
1.91 + current theory context. Returning \isa{NONE} indicates that no
1.92 + transformation took place; otherwise, the whole process will be iterated
1.93 + with the new code equations.
1.94 +
1.95 + \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes
1.96 + function transformer named \isa{name} from executable content.
1.97 +
1.98 + \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
1.99 + a datatype to executable content, with generation
1.100 + set \isa{cs}.
1.101 +
1.102 + \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
1.103 + returns type constructor corresponding to
1.104 + constructor \isa{const}; returns \isa{NONE}
1.105 + if \isa{const} is no constructor.
1.106 +
1.107 + \end{description}%
1.108 +\end{isamarkuptext}%
1.109 +\isamarkuptrue%
1.110 +%
1.111 +\endisatagmlref
1.112 +{\isafoldmlref}%
1.113 +%
1.114 +\isadelimmlref
1.115 +%
1.116 +\endisadelimmlref
1.117 +%
1.118 +\isamarkupsubsection{Auxiliary%
1.119 +}
1.120 +\isamarkuptrue%
1.121 +%
1.122 +\isadelimmlref
1.123 +%
1.124 +\endisadelimmlref
1.125 +%
1.126 +\isatagmlref
1.127 +%
1.128 +\begin{isamarkuptext}%
1.129 +\begin{mldecls}
1.130 + \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
1.131 + \indexdef{}{ML}{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
1.132 + \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
1.133 + \end{mldecls}
1.134 +
1.135 + \begin{description}
1.136 +
1.137 + \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s}
1.138 + reads a constant as a concrete term expression \isa{s}.
1.139 +
1.140 + \item \verb|Code_Unit.head_eqn|~\isa{thy}~\isa{thm}
1.141 + extracts the constant and its type from a code equation \isa{thm}.
1.142 +
1.143 + \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm}
1.144 + rewrites a code equation \isa{thm} with a simpset \isa{ss};
1.145 + only arguments and right hand side are rewritten,
1.146 + not the head of the code equation.
1.147 +
1.148 + \end{description}%
1.149 +\end{isamarkuptext}%
1.150 +\isamarkuptrue%
1.151 +%
1.152 +\endisatagmlref
1.153 +{\isafoldmlref}%
1.154 +%
1.155 +\isadelimmlref
1.156 +%
1.157 +\endisadelimmlref
1.158 +%
1.159 +\isamarkupsubsection{Implementing code generator applications%
1.160 +}
1.161 +\isamarkuptrue%
1.162 +%
1.163 +\begin{isamarkuptext}%
1.164 +Implementing code generator applications on top
1.165 + of the framework set out so far usually not only
1.166 + involves using those primitive interfaces
1.167 + but also storing code-dependent data and various
1.168 + other things.%
1.169 +\end{isamarkuptext}%
1.170 +\isamarkuptrue%
1.171 +%
1.172 +\isamarkupsubsubsection{Data depending on the theory's executable content%
1.173 +}
1.174 +\isamarkuptrue%
1.175 +%
1.176 +\begin{isamarkuptext}%
1.177 +Due to incrementality of code generation, changes in the
1.178 + theory's executable content have to be propagated in a
1.179 + certain fashion. Additionally, such changes may occur
1.180 + not only during theory extension but also during theory
1.181 + merge, which is a little bit nasty from an implementation
1.182 + point of view. The framework provides a solution
1.183 + to this technical challenge by providing a functorial
1.184 + data slot \verb|CodeDataFun|; on instantiation
1.185 + of this functor, the following types and operations
1.186 + are required:
1.187 +
1.188 + \medskip
1.189 + \begin{tabular}{l}
1.190 + \isa{type\ T} \\
1.191 + \isa{val\ empty{\isacharcolon}\ T} \\
1.192 + \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
1.193 + \end{tabular}
1.194 +
1.195 + \begin{description}
1.196 +
1.197 + \item \isa{T} the type of data to store.
1.198 +
1.199 + \item \isa{empty} initial (empty) data.
1.200 +
1.201 + \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
1.202 + \isa{consts} indicates the kind
1.203 + of change: \verb|NONE| stands for a fundamental change
1.204 + which invalidates any existing code, \isa{SOME\ consts}
1.205 + hints that executable content for constants \isa{consts}
1.206 + has changed.
1.207 +
1.208 + \end{description}
1.209 +
1.210 + \noindent An instance of \verb|CodeDataFun| provides the following
1.211 + interface:
1.212 +
1.213 + \medskip
1.214 + \begin{tabular}{l}
1.215 + \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
1.216 + \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
1.217 + \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
1.218 + \end{tabular}
1.219 +
1.220 + \begin{description}
1.221 +
1.222 + \item \isa{get} retrieval of the current data.
1.223 +
1.224 + \item \isa{change} update of current data (cached!)
1.225 + by giving a continuation.
1.226 +
1.227 + \item \isa{change{\isacharunderscore}yield} update with side result.
1.228 +
1.229 + \end{description}%
1.230 +\end{isamarkuptext}%
1.231 +\isamarkuptrue%
1.232 +%
1.233 +\begin{isamarkuptext}%
1.234 +\bigskip
1.235 +
1.236 + \emph{Happy proving, happy hacking!}%
1.237 +\end{isamarkuptext}%
1.238 +\isamarkuptrue%
1.239 +%
1.240 +\isadelimtheory
1.241 +%
1.242 +\endisadelimtheory
1.243 +%
1.244 +\isatagtheory
1.245 +\isacommand{end}\isamarkupfalse%
1.246 +%
1.247 +\endisatagtheory
1.248 +{\isafoldtheory}%
1.249 +%
1.250 +\isadelimtheory
1.251 +%
1.252 +\endisadelimtheory
1.253 +\isanewline
1.254 +\end{isabellebody}%
1.255 +%%% Local Variables:
1.256 +%%% mode: latex
1.257 +%%% TeX-master: "root"
1.258 +%%% End: