28447
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{ML}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
\isacommand{theory}\isamarkupfalse%
|
|
11 |
\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
|
|
12 |
\isakeyword{imports}\ Setup\isanewline
|
|
13 |
\isakeyword{begin}%
|
|
14 |
\endisatagtheory
|
|
15 |
{\isafoldtheory}%
|
|
16 |
%
|
|
17 |
\isadelimtheory
|
|
18 |
%
|
|
19 |
\endisadelimtheory
|
|
20 |
%
|
|
21 |
\isamarkupsection{ML system interfaces \label{sec:ml}%
|
|
22 |
}
|
|
23 |
\isamarkuptrue%
|
|
24 |
%
|
|
25 |
\begin{isamarkuptext}%
|
|
26 |
Since the code generator framework not only aims to provide
|
|
27 |
a nice Isar interface but also to form a base for
|
|
28 |
code-generation-based applications, here a short
|
|
29 |
description of the most important ML interfaces.%
|
|
30 |
\end{isamarkuptext}%
|
|
31 |
\isamarkuptrue%
|
|
32 |
%
|
|
33 |
\isamarkupsubsection{Executable theory content: \isa{Code}%
|
|
34 |
}
|
|
35 |
\isamarkuptrue%
|
|
36 |
%
|
|
37 |
\begin{isamarkuptext}%
|
|
38 |
This Pure module implements the core notions of
|
|
39 |
executable content of a theory.%
|
|
40 |
\end{isamarkuptext}%
|
|
41 |
\isamarkuptrue%
|
|
42 |
%
|
|
43 |
\isamarkupsubsubsection{Managing executable content%
|
|
44 |
}
|
|
45 |
\isamarkuptrue%
|
|
46 |
%
|
|
47 |
\isadelimmlref
|
|
48 |
%
|
|
49 |
\endisadelimmlref
|
|
50 |
%
|
|
51 |
\isatagmlref
|
|
52 |
%
|
|
53 |
\begin{isamarkuptext}%
|
|
54 |
\begin{mldecls}
|
30121
|
55 |
\indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
|
|
56 |
\indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
|
|
57 |
\indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
|
31150
|
58 |
\indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
|
|
59 |
\indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
|
|
60 |
\indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
|
28447
|
61 |
\verb| -> theory -> theory| \\
|
31150
|
62 |
\indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
|
30121
|
63 |
\indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
|
|
64 |
\indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
|
28447
|
65 |
\verb| -> (string * sort) list * (string * typ list) list| \\
|
30121
|
66 |
\indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
|
28447
|
67 |
\end{mldecls}
|
|
68 |
|
|
69 |
\begin{description}
|
|
70 |
|
|
71 |
\item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
|
|
72 |
theorem \isa{thm} to executable content.
|
|
73 |
|
|
74 |
\item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
|
|
75 |
theorem \isa{thm} from executable content, if present.
|
|
76 |
|
|
77 |
\item \verb|Code.add_eqnl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
|
29560
|
78 |
suspended code equations \isa{lthms} for constant
|
28447
|
79 |
\isa{const} to executable content.
|
|
80 |
|
31150
|
81 |
\item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
|
28447
|
82 |
the preprocessor simpset.
|
|
83 |
|
31150
|
84 |
\item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
|
28447
|
85 |
function transformer \isa{f} (named \isa{name}) to executable content;
|
29560
|
86 |
\isa{f} is a transformer of the code equations belonging
|
28447
|
87 |
to a certain function definition, depending on the
|
|
88 |
current theory context. Returning \isa{NONE} indicates that no
|
|
89 |
transformation took place; otherwise, the whole process will be iterated
|
29560
|
90 |
with the new code equations.
|
28447
|
91 |
|
31150
|
92 |
\item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
|
28447
|
93 |
function transformer named \isa{name} from executable content.
|
|
94 |
|
|
95 |
\item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
|
|
96 |
a datatype to executable content, with generation
|
|
97 |
set \isa{cs}.
|
|
98 |
|
|
99 |
\item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
|
|
100 |
returns type constructor corresponding to
|
|
101 |
constructor \isa{const}; returns \isa{NONE}
|
|
102 |
if \isa{const} is no constructor.
|
|
103 |
|
|
104 |
\end{description}%
|
|
105 |
\end{isamarkuptext}%
|
|
106 |
\isamarkuptrue%
|
|
107 |
%
|
|
108 |
\endisatagmlref
|
|
109 |
{\isafoldmlref}%
|
|
110 |
%
|
|
111 |
\isadelimmlref
|
|
112 |
%
|
|
113 |
\endisadelimmlref
|
|
114 |
%
|
|
115 |
\isamarkupsubsection{Auxiliary%
|
|
116 |
}
|
|
117 |
\isamarkuptrue%
|
|
118 |
%
|
|
119 |
\isadelimmlref
|
|
120 |
%
|
|
121 |
\endisadelimmlref
|
|
122 |
%
|
|
123 |
\isatagmlref
|
|
124 |
%
|
|
125 |
\begin{isamarkuptext}%
|
|
126 |
\begin{mldecls}
|
30121
|
127 |
\indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
|
|
128 |
\indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
|
28447
|
129 |
\end{mldecls}
|
|
130 |
|
|
131 |
\begin{description}
|
|
132 |
|
|
133 |
\item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s}
|
|
134 |
reads a constant as a concrete term expression \isa{s}.
|
|
135 |
|
|
136 |
\item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm}
|
29560
|
137 |
rewrites a code equation \isa{thm} with a simpset \isa{ss};
|
28447
|
138 |
only arguments and right hand side are rewritten,
|
29560
|
139 |
not the head of the code equation.
|
28447
|
140 |
|
|
141 |
\end{description}%
|
|
142 |
\end{isamarkuptext}%
|
|
143 |
\isamarkuptrue%
|
|
144 |
%
|
|
145 |
\endisatagmlref
|
|
146 |
{\isafoldmlref}%
|
|
147 |
%
|
|
148 |
\isadelimmlref
|
|
149 |
%
|
|
150 |
\endisadelimmlref
|
|
151 |
%
|
|
152 |
\isamarkupsubsection{Implementing code generator applications%
|
|
153 |
}
|
|
154 |
\isamarkuptrue%
|
|
155 |
%
|
|
156 |
\begin{isamarkuptext}%
|
|
157 |
Implementing code generator applications on top
|
|
158 |
of the framework set out so far usually not only
|
|
159 |
involves using those primitive interfaces
|
|
160 |
but also storing code-dependent data and various
|
|
161 |
other things.%
|
|
162 |
\end{isamarkuptext}%
|
|
163 |
\isamarkuptrue%
|
|
164 |
%
|
|
165 |
\isamarkupsubsubsection{Data depending on the theory's executable content%
|
|
166 |
}
|
|
167 |
\isamarkuptrue%
|
|
168 |
%
|
|
169 |
\begin{isamarkuptext}%
|
|
170 |
Due to incrementality of code generation, changes in the
|
|
171 |
theory's executable content have to be propagated in a
|
|
172 |
certain fashion. Additionally, such changes may occur
|
|
173 |
not only during theory extension but also during theory
|
|
174 |
merge, which is a little bit nasty from an implementation
|
|
175 |
point of view. The framework provides a solution
|
|
176 |
to this technical challenge by providing a functorial
|
|
177 |
data slot \verb|CodeDataFun|; on instantiation
|
|
178 |
of this functor, the following types and operations
|
|
179 |
are required:
|
|
180 |
|
|
181 |
\medskip
|
|
182 |
\begin{tabular}{l}
|
|
183 |
\isa{type\ T} \\
|
|
184 |
\isa{val\ empty{\isacharcolon}\ T} \\
|
28635
|
185 |
\isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
|
28447
|
186 |
\end{tabular}
|
|
187 |
|
|
188 |
\begin{description}
|
|
189 |
|
|
190 |
\item \isa{T} the type of data to store.
|
|
191 |
|
|
192 |
\item \isa{empty} initial (empty) data.
|
|
193 |
|
|
194 |
\item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
|
|
195 |
\isa{consts} indicates the kind
|
|
196 |
of change: \verb|NONE| stands for a fundamental change
|
|
197 |
which invalidates any existing code, \isa{SOME\ consts}
|
|
198 |
hints that executable content for constants \isa{consts}
|
|
199 |
has changed.
|
|
200 |
|
|
201 |
\end{description}
|
|
202 |
|
|
203 |
\noindent An instance of \verb|CodeDataFun| provides the following
|
|
204 |
interface:
|
|
205 |
|
|
206 |
\medskip
|
|
207 |
\begin{tabular}{l}
|
|
208 |
\isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
|
|
209 |
\isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
|
|
210 |
\isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
|
|
211 |
\end{tabular}
|
|
212 |
|
|
213 |
\begin{description}
|
|
214 |
|
|
215 |
\item \isa{get} retrieval of the current data.
|
|
216 |
|
|
217 |
\item \isa{change} update of current data (cached!)
|
|
218 |
by giving a continuation.
|
|
219 |
|
|
220 |
\item \isa{change{\isacharunderscore}yield} update with side result.
|
|
221 |
|
|
222 |
\end{description}%
|
|
223 |
\end{isamarkuptext}%
|
|
224 |
\isamarkuptrue%
|
|
225 |
%
|
|
226 |
\begin{isamarkuptext}%
|
|
227 |
\bigskip
|
|
228 |
|
|
229 |
\emph{Happy proving, happy hacking!}%
|
|
230 |
\end{isamarkuptext}%
|
|
231 |
\isamarkuptrue%
|
|
232 |
%
|
|
233 |
\isadelimtheory
|
|
234 |
%
|
|
235 |
\endisadelimtheory
|
|
236 |
%
|
|
237 |
\isatagtheory
|
|
238 |
\isacommand{end}\isamarkupfalse%
|
|
239 |
%
|
|
240 |
\endisatagtheory
|
|
241 |
{\isafoldtheory}%
|
|
242 |
%
|
|
243 |
\isadelimtheory
|
|
244 |
%
|
|
245 |
\endisadelimtheory
|
|
246 |
\isanewline
|
|
247 |
\end{isabellebody}%
|
|
248 |
%%% Local Variables:
|
|
249 |
%%% mode: latex
|
|
250 |
%%% TeX-master: "root"
|
|
251 |
%%% End:
|