3 \def\isabellecontext{Further}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Setup\isanewline
21 \isamarkupsection{Further issues \label{sec:further}%
25 \isamarkupsubsection{Modules namespace%
29 \begin{isamarkuptext}%
30 When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave
31 out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over
32 different modules, where the module name space roughly is induced
33 by the Isabelle theory name space.
35 Then sometimes the awkward situation occurs that dependencies between
36 definitions introduce cyclic dependencies between modules, which in the
37 \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation
38 you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
40 A solution is to declare module names explicitly.
41 Let use assume the three cyclically dependent
42 modules are named \emph{A}, \emph{B} and \emph{C}.
52 \isacommand{code{\isacharunderscore}modulename}\isamarkupfalse%
64 \begin{isamarkuptext}%
66 we explicitly map all those modules on \emph{ABC},
67 resulting in an ad-hoc merge of this three modules
68 at serialisation time.%
72 \isamarkupsubsection{Locales and interpretation%
76 \begin{isamarkuptext}%
77 A technical issue comes to surface when generating code from
78 specifications stemming from locale interpretation.
80 Let us assume a locale specifying a power operation
90 \isacommand{locale}\isamarkupfalse%
91 \ power\ {\isacharequal}\isanewline
92 \ \ \isakeyword{fixes}\ power\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
93 \ \ \isakeyword{assumes}\ power{\isacharunderscore}commute{\isacharcolon}\ {\isachardoublequoteopen}power\ x\ {\isasymcirc}\ power\ y\ {\isacharequal}\ power\ y\ {\isasymcirc}\ power\ x{\isachardoublequoteclose}\isanewline
102 \begin{isamarkuptext}%
103 \noindent Inside that locale we can lift \isa{power} to exponent lists
104 by means of specification relative to that locale:%
113 \isacommand{primrec}\isamarkupfalse%
114 \ powers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
115 \ \ {\isachardoublequoteopen}powers\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isachardoublequoteclose}\isanewline
116 {\isacharbar}\ {\isachardoublequoteopen}powers\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline
118 \isacommand{lemma}\isamarkupfalse%
119 \ powers{\isacharunderscore}append{\isacharcolon}\isanewline
120 \ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ powers\ xs\ {\isasymcirc}\ powers\ ys{\isachardoublequoteclose}\isanewline
121 \ \ \isacommand{by}\isamarkupfalse%
122 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
124 \isacommand{lemma}\isamarkupfalse%
125 \ powers{\isacharunderscore}power{\isacharcolon}\isanewline
126 \ \ {\isachardoublequoteopen}powers\ xs\ {\isasymcirc}\ power\ x\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline
127 \ \ \isacommand{by}\isamarkupfalse%
128 \ {\isacharparenleft}induct\ xs{\isacharparenright}\isanewline
129 \ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}\ o{\isacharunderscore}apply\ id{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcomma}\isanewline
130 \ \ \ \ \ \ simp\ del{\isacharcolon}\ o{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ power{\isacharunderscore}commute{\isacharparenright}\isanewline
132 \isacommand{lemma}\isamarkupfalse%
133 \ powers{\isacharunderscore}rev{\isacharcolon}\isanewline
134 \ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ powers\ xs{\isachardoublequoteclose}\isanewline
135 \ \ \ \ \isacommand{by}\isamarkupfalse%
136 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ powers{\isacharunderscore}append\ powers{\isacharunderscore}power{\isacharparenright}\isanewline
138 \isacommand{end}\isamarkupfalse%
147 \begin{isamarkuptext}%
148 After an interpretation of this locale (say, \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} \isa{fun{\isacharunderscore}power{\isacharcolon}} \isa{{\isachardoublequote}power\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}), one would expect to have a constant \isa{fun{\isacharunderscore}power{\isachardot}powers\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} for which code
149 can be generated. But this not the case: internally, the term
150 \isa{fun{\isacharunderscore}power{\isachardot}powers} is an abbreviation for the foundational
151 term \isa{{\isachardoublequote}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}
152 (see \cite{isabelle-locale} for the details behind).
154 Fortunately, with minor effort the desired behaviour can be achieved.
155 First, a dedicated definition of the constant on which the local \isa{powers}
156 after interpretation is supposed to be mapped on:%
165 \isacommand{definition}\isamarkupfalse%
166 \ funpows\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
167 \ \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}funpows\ {\isacharequal}\ power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequoteclose}%
175 \begin{isamarkuptext}%
176 \noindent In general, the pattern is \isa{c\ {\isacharequal}\ t} where \isa{c} is
177 the name of the future constant and \isa{t} the foundational term
178 corresponding to the local constant after interpretation.
180 The interpretation itself is enriched with an equation \isa{t\ {\isacharequal}\ c}:%
189 \isacommand{interpretation}\isamarkupfalse%
190 \ fun{\isacharunderscore}power{\isacharcolon}\ power\ {\isachardoublequoteopen}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
191 \ \ {\isachardoublequoteopen}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}\ {\isacharequal}\ funpows{\isachardoublequoteclose}\isanewline
192 \ \ \isacommand{by}\isamarkupfalse%
193 \ unfold{\isacharunderscore}locales\isanewline
194 \ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}%
202 \begin{isamarkuptext}%
203 \noindent This additional equation is trivially proved by the definition
206 After this setup procedure, code generation can continue as usual:%
216 \begin{isamarkuptext}%
219 \hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
220 \hspace*{0pt}funpow Zero{\char95}nat f = id;\\
221 \hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
223 \hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
224 \hspace*{0pt}funpows [] = id;\\
225 \hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
236 \isamarkupsubsection{Imperative data structures%
240 \begin{isamarkuptext}%
241 If you consider imperative data structures as inevitable for a
242 specific application, you should consider \emph{Imperative
243 Functional Programming with Isabelle/HOL}
244 \cite{bulwahn-et-al:2008:imperative}; the framework described there
245 is available in session \isa{Imperative{\isacharunderscore}HOL}.%
249 \isamarkupsubsection{ML system interfaces \label{sec:ml}%
253 \begin{isamarkuptext}%
254 Since the code generator framework not only aims to provide a nice
255 Isar interface but also to form a base for code-generation-based
256 applications, here a short description of the most fundamental ML
261 \isamarkupsubsubsection{Managing executable content%
271 \begin{isamarkuptext}%
273 \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
274 \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
275 \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
276 \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
277 \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
278 \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: |\isasep\isanewline%
279 \verb| string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
280 \verb| -> theory -> theory| \\
281 \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
282 \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
283 \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
284 \verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
285 \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
290 \item \verb|Code.read_const|~\isa{thy}~\isa{s}
291 reads a constant as a concrete term expression \isa{s}.
293 \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
294 theorem \isa{thm} to executable content.
296 \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
297 theorem \isa{thm} from executable content, if present.
299 \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
300 the preprocessor simpset.
302 \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
303 function transformer \isa{f} (named \isa{name}) to executable content;
304 \isa{f} is a transformer of the code equations belonging
305 to a certain function definition, depending on the
306 current theory context. Returning \isa{NONE} indicates that no
307 transformation took place; otherwise, the whole process will be iterated
308 with the new code equations.
310 \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
311 function transformer named \isa{name} from executable content.
313 \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
314 a datatype to executable content, with generation
317 \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
318 returns type constructor corresponding to
319 constructor \isa{const}; returns \isa{NONE}
320 if \isa{const} is no constructor.
333 \isamarkupsubsubsection{Data depending on the theory's executable content%
337 \begin{isamarkuptext}%
338 Implementing code generator applications on top
339 of the framework set out so far usually not only
340 involves using those primitive interfaces
341 but also storing code-dependent data and various
344 Due to incrementality of code generation, changes in the
345 theory's executable content have to be propagated in a
346 certain fashion. Additionally, such changes may occur
347 not only during theory extension but also during theory
348 merge, which is a little bit nasty from an implementation
349 point of view. The framework provides a solution
350 to this technical challenge by providing a functorial
351 data slot \verb|Code_Data|; on instantiation
352 of this functor, the following types and operations
358 \isa{val\ empty{\isacharcolon}\ T} \\
363 \item \isa{T} the type of data to store.
365 \item \isa{empty} initial (empty) data.
369 \noindent An instance of \verb|Code_Data| provides the following
374 \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
375 \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
380 \item \isa{change} update of current data (cached!)
381 by giving a continuation.
383 \item \isa{change{\isacharunderscore}yield} update with side result.
394 \isacommand{end}\isamarkupfalse%
406 %%% TeX-master: "root"