1.1 --- a/doc-src/Codegen/Thy/document/Further.tex Fri Aug 13 13:43:55 2010 +0200
1.2 +++ b/doc-src/Codegen/Thy/document/Further.tex Fri Aug 13 14:40:15 2010 +0200
1.3 @@ -389,6 +389,179 @@
1.4 \end{isamarkuptext}%
1.5 \isamarkuptrue%
1.6 %
1.7 +\isamarkupsubsection{ML system interfaces \label{sec:ml}%
1.8 +}
1.9 +\isamarkuptrue%
1.10 +%
1.11 +\begin{isamarkuptext}%
1.12 +Since the code generator framework not only aims to provide
1.13 + a nice Isar interface but also to form a base for
1.14 + code-generation-based applications, here a short
1.15 + description of the most important ML interfaces.%
1.16 +\end{isamarkuptext}%
1.17 +\isamarkuptrue%
1.18 +%
1.19 +\isamarkupsubsubsection{Managing executable content%
1.20 +}
1.21 +\isamarkuptrue%
1.22 +%
1.23 +\isadelimmlref
1.24 +%
1.25 +\endisadelimmlref
1.26 +%
1.27 +\isatagmlref
1.28 +%
1.29 +\begin{isamarkuptext}%
1.30 +\begin{mldecls}
1.31 + \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
1.32 + \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
1.33 + \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
1.34 + \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
1.35 + \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
1.36 +\verb| -> theory -> theory| \\
1.37 + \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
1.38 + \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
1.39 + \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
1.40 +\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
1.41 + \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
1.42 + \end{mldecls}
1.43 +
1.44 + \begin{description}
1.45 +
1.46 + \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
1.47 + theorem \isa{thm} to executable content.
1.48 +
1.49 + \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
1.50 + theorem \isa{thm} from executable content, if present.
1.51 +
1.52 + \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
1.53 + the preprocessor simpset.
1.54 +
1.55 + \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
1.56 + function transformer \isa{f} (named \isa{name}) to executable content;
1.57 + \isa{f} is a transformer of the code equations belonging
1.58 + to a certain function definition, depending on the
1.59 + current theory context. Returning \isa{NONE} indicates that no
1.60 + transformation took place; otherwise, the whole process will be iterated
1.61 + with the new code equations.
1.62 +
1.63 + \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
1.64 + function transformer named \isa{name} from executable content.
1.65 +
1.66 + \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
1.67 + a datatype to executable content, with generation
1.68 + set \isa{cs}.
1.69 +
1.70 + \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
1.71 + returns type constructor corresponding to
1.72 + constructor \isa{const}; returns \isa{NONE}
1.73 + if \isa{const} is no constructor.
1.74 +
1.75 + \end{description}%
1.76 +\end{isamarkuptext}%
1.77 +\isamarkuptrue%
1.78 +%
1.79 +\endisatagmlref
1.80 +{\isafoldmlref}%
1.81 +%
1.82 +\isadelimmlref
1.83 +%
1.84 +\endisadelimmlref
1.85 +%
1.86 +\isamarkupsubsubsection{Auxiliary%
1.87 +}
1.88 +\isamarkuptrue%
1.89 +%
1.90 +\isadelimmlref
1.91 +%
1.92 +\endisadelimmlref
1.93 +%
1.94 +\isatagmlref
1.95 +%
1.96 +\begin{isamarkuptext}%
1.97 +\begin{mldecls}
1.98 + \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
1.99 + \end{mldecls}
1.100 +
1.101 + \begin{description}
1.102 +
1.103 + \item \verb|Code.read_const|~\isa{thy}~\isa{s}
1.104 + reads a constant as a concrete term expression \isa{s}.
1.105 +
1.106 + \end{description}%
1.107 +\end{isamarkuptext}%
1.108 +\isamarkuptrue%
1.109 +%
1.110 +\endisatagmlref
1.111 +{\isafoldmlref}%
1.112 +%
1.113 +\isadelimmlref
1.114 +%
1.115 +\endisadelimmlref
1.116 +%
1.117 +\isamarkupsubsubsection{Data depending on the theory's executable content%
1.118 +}
1.119 +\isamarkuptrue%
1.120 +%
1.121 +\begin{isamarkuptext}%
1.122 +Implementing code generator applications on top
1.123 + of the framework set out so far usually not only
1.124 + involves using those primitive interfaces
1.125 + but also storing code-dependent data and various
1.126 + other things.
1.127 +
1.128 + Due to incrementality of code generation, changes in the
1.129 + theory's executable content have to be propagated in a
1.130 + certain fashion. Additionally, such changes may occur
1.131 + not only during theory extension but also during theory
1.132 + merge, which is a little bit nasty from an implementation
1.133 + point of view. The framework provides a solution
1.134 + to this technical challenge by providing a functorial
1.135 + data slot \verb|Code_Data|; on instantiation
1.136 + of this functor, the following types and operations
1.137 + are required:
1.138 +
1.139 + \medskip
1.140 + \begin{tabular}{l}
1.141 + \isa{type\ T} \\
1.142 + \isa{val\ empty{\isacharcolon}\ T} \\
1.143 + \end{tabular}
1.144 +
1.145 + \begin{description}
1.146 +
1.147 + \item \isa{T} the type of data to store.
1.148 +
1.149 + \item \isa{empty} initial (empty) data.
1.150 +
1.151 + \end{description}
1.152 +
1.153 + \noindent An instance of \verb|Code_Data| provides the following
1.154 + interface:
1.155 +
1.156 + \medskip
1.157 + \begin{tabular}{l}
1.158 + \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
1.159 + \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
1.160 + \end{tabular}
1.161 +
1.162 + \begin{description}
1.163 +
1.164 + \item \isa{change} update of current data (cached!)
1.165 + by giving a continuation.
1.166 +
1.167 + \item \isa{change{\isacharunderscore}yield} update with side result.
1.168 +
1.169 + \end{description}%
1.170 +\end{isamarkuptext}%
1.171 +\isamarkuptrue%
1.172 +%
1.173 +\begin{isamarkuptext}%
1.174 +\bigskip
1.175 +
1.176 + \emph{Happy proving, happy hacking!}%
1.177 +\end{isamarkuptext}%
1.178 +\isamarkuptrue%
1.179 +%
1.180 \isadelimtheory
1.181 %
1.182 \endisadelimtheory