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} |
|
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| \\ |
|
58 \indexdef{}{ML}{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\ |
|
59 \indexdef{}{ML}{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\ |
|
60 \indexdef{}{ML}{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% |
|
61 \verb| -> theory -> theory| \\ |
|
62 \indexdef{}{ML}{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\ |
|
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% |
|
65 \verb| -> (string * sort) list * (string * typ list) list| \\ |
|
66 \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option| |
|
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 |
|
78 suspended code equations \isa{lthms} for constant |
|
79 \isa{const} to executable content. |
|
80 |
|
81 \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes |
|
82 the preprocessor simpset. |
|
83 |
|
84 \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds |
|
85 function transformer \isa{f} (named \isa{name}) to executable content; |
|
86 \isa{f} is a transformer of the code equations belonging |
|
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 |
|
90 with the new code equations. |
|
91 |
|
92 \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes |
|
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} |
|
127 \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\ |
|
128 \indexdef{}{ML}{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\ |
|
129 \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\ |
|
130 \end{mldecls} |
|
131 |
|
132 \begin{description} |
|
133 |
|
134 \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s} |
|
135 reads a constant as a concrete term expression \isa{s}. |
|
136 |
|
137 \item \verb|Code_Unit.head_eqn|~\isa{thy}~\isa{thm} |
|
138 extracts the constant and its type from a code equation \isa{thm}. |
|
139 |
|
140 \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm} |
|
141 rewrites a code equation \isa{thm} with a simpset \isa{ss}; |
|
142 only arguments and right hand side are rewritten, |
|
143 not the head of the code equation. |
|
144 |
|
145 \end{description}% |
|
146 \end{isamarkuptext}% |
|
147 \isamarkuptrue% |
|
148 % |
|
149 \endisatagmlref |
|
150 {\isafoldmlref}% |
|
151 % |
|
152 \isadelimmlref |
|
153 % |
|
154 \endisadelimmlref |
|
155 % |
|
156 \isamarkupsubsection{Implementing code generator applications% |
|
157 } |
|
158 \isamarkuptrue% |
|
159 % |
|
160 \begin{isamarkuptext}% |
|
161 Implementing code generator applications on top |
|
162 of the framework set out so far usually not only |
|
163 involves using those primitive interfaces |
|
164 but also storing code-dependent data and various |
|
165 other things.% |
|
166 \end{isamarkuptext}% |
|
167 \isamarkuptrue% |
|
168 % |
|
169 \isamarkupsubsubsection{Data depending on the theory's executable content% |
|
170 } |
|
171 \isamarkuptrue% |
|
172 % |
|
173 \begin{isamarkuptext}% |
|
174 Due to incrementality of code generation, changes in the |
|
175 theory's executable content have to be propagated in a |
|
176 certain fashion. Additionally, such changes may occur |
|
177 not only during theory extension but also during theory |
|
178 merge, which is a little bit nasty from an implementation |
|
179 point of view. The framework provides a solution |
|
180 to this technical challenge by providing a functorial |
|
181 data slot \verb|CodeDataFun|; on instantiation |
|
182 of this functor, the following types and operations |
|
183 are required: |
|
184 |
|
185 \medskip |
|
186 \begin{tabular}{l} |
|
187 \isa{type\ T} \\ |
|
188 \isa{val\ empty{\isacharcolon}\ T} \\ |
|
189 \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T} |
|
190 \end{tabular} |
|
191 |
|
192 \begin{description} |
|
193 |
|
194 \item \isa{T} the type of data to store. |
|
195 |
|
196 \item \isa{empty} initial (empty) data. |
|
197 |
|
198 \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content; |
|
199 \isa{consts} indicates the kind |
|
200 of change: \verb|NONE| stands for a fundamental change |
|
201 which invalidates any existing code, \isa{SOME\ consts} |
|
202 hints that executable content for constants \isa{consts} |
|
203 has changed. |
|
204 |
|
205 \end{description} |
|
206 |
|
207 \noindent An instance of \verb|CodeDataFun| provides the following |
|
208 interface: |
|
209 |
|
210 \medskip |
|
211 \begin{tabular}{l} |
|
212 \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\ |
|
213 \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\ |
|
214 \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T} |
|
215 \end{tabular} |
|
216 |
|
217 \begin{description} |
|
218 |
|
219 \item \isa{get} retrieval of the current data. |
|
220 |
|
221 \item \isa{change} update of current data (cached!) |
|
222 by giving a continuation. |
|
223 |
|
224 \item \isa{change{\isacharunderscore}yield} update with side result. |
|
225 |
|
226 \end{description}% |
|
227 \end{isamarkuptext}% |
|
228 \isamarkuptrue% |
|
229 % |
|
230 \begin{isamarkuptext}% |
|
231 \bigskip |
|
232 |
|
233 \emph{Happy proving, happy hacking!}% |
|
234 \end{isamarkuptext}% |
|
235 \isamarkuptrue% |
|
236 % |
|
237 \isadelimtheory |
|
238 % |
|
239 \endisadelimtheory |
|
240 % |
|
241 \isatagtheory |
|
242 \isacommand{end}\isamarkupfalse% |
|
243 % |
|
244 \endisatagtheory |
|
245 {\isafoldtheory}% |
|
246 % |
|
247 \isadelimtheory |
|
248 % |
|
249 \endisadelimtheory |
|
250 \isanewline |
|
251 \end{isabellebody}% |
|
252 %%% Local Variables: |
|
253 %%% mode: latex |
|
254 %%% TeX-master: "root" |
|
255 %%% End: |
|