1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Further}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Further\isanewline |
|
12 \isakeyword{imports}\ Setup\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupsection{Further issues \label{sec:further}% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \isamarkupsubsection{Further reading% |
|
26 } |
|
27 \isamarkuptrue% |
|
28 % |
|
29 \begin{isamarkuptext}% |
|
30 Do dive deeper into the issue of code generation, you should visit |
|
31 the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which |
|
32 contains exhaustive syntax diagrams.% |
|
33 \end{isamarkuptext}% |
|
34 \isamarkuptrue% |
|
35 % |
|
36 \isamarkupsubsection{Modules% |
|
37 } |
|
38 \isamarkuptrue% |
|
39 % |
|
40 \begin{isamarkuptext}% |
|
41 When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave |
|
42 out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over |
|
43 different modules, where the module name space roughly is induced |
|
44 by the \isa{Isabelle} theory name space. |
|
45 |
|
46 Then sometimes the awkward situation occurs that dependencies between |
|
47 definitions introduce cyclic dependencies between modules, which in the |
|
48 \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation |
|
49 you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible. |
|
50 |
|
51 A solution is to declare module names explicitly. |
|
52 Let use assume the three cyclically dependent |
|
53 modules are named \emph{A}, \emph{B} and \emph{C}. |
|
54 Then, by stating% |
|
55 \end{isamarkuptext}% |
|
56 \isamarkuptrue% |
|
57 % |
|
58 \isadelimquote |
|
59 % |
|
60 \endisadelimquote |
|
61 % |
|
62 \isatagquote |
|
63 \isacommand{code{\isacharunderscore}modulename}\isamarkupfalse% |
|
64 \ SML\isanewline |
|
65 \ \ A\ ABC\isanewline |
|
66 \ \ B\ ABC\isanewline |
|
67 \ \ C\ ABC% |
|
68 \endisatagquote |
|
69 {\isafoldquote}% |
|
70 % |
|
71 \isadelimquote |
|
72 % |
|
73 \endisadelimquote |
|
74 % |
|
75 \begin{isamarkuptext}% |
|
76 we explicitly map all those modules on \emph{ABC}, |
|
77 resulting in an ad-hoc merge of this three modules |
|
78 at serialisation time.% |
|
79 \end{isamarkuptext}% |
|
80 \isamarkuptrue% |
|
81 % |
|
82 \isamarkupsubsection{Evaluation oracle% |
|
83 } |
|
84 \isamarkuptrue% |
|
85 % |
|
86 \begin{isamarkuptext}% |
|
87 Code generation may also be used to \emph{evaluate} expressions |
|
88 (using \isa{SML} as target language of course). |
|
89 For instance, the \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} allows to reduce an expression to a |
|
90 normal form with respect to the underlying code equations:% |
|
91 \end{isamarkuptext}% |
|
92 \isamarkuptrue% |
|
93 % |
|
94 \isadelimquote |
|
95 % |
|
96 \endisadelimquote |
|
97 % |
|
98 \isatagquote |
|
99 \isacommand{value}\isamarkupfalse% |
|
100 \ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}% |
|
101 \endisatagquote |
|
102 {\isafoldquote}% |
|
103 % |
|
104 \isadelimquote |
|
105 % |
|
106 \endisadelimquote |
|
107 % |
|
108 \begin{isamarkuptext}% |
|
109 \noindent will display \isa{{\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}}. |
|
110 |
|
111 The \hyperlink{method.eval}{\mbox{\isa{eval}}} method tries to reduce a goal by code generation to \isa{True} |
|
112 and solves it in that case, but fails otherwise:% |
|
113 \end{isamarkuptext}% |
|
114 \isamarkuptrue% |
|
115 % |
|
116 \isadelimquote |
|
117 % |
|
118 \endisadelimquote |
|
119 % |
|
120 \isatagquote |
|
121 \isacommand{lemma}\isamarkupfalse% |
|
122 \ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}\ {\isacharequal}\ {\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline |
|
123 \ \ \isacommand{by}\isamarkupfalse% |
|
124 \ eval% |
|
125 \endisatagquote |
|
126 {\isafoldquote}% |
|
127 % |
|
128 \isadelimquote |
|
129 % |
|
130 \endisadelimquote |
|
131 % |
|
132 \begin{isamarkuptext}% |
|
133 \noindent The soundness of the \hyperlink{method.eval}{\mbox{\isa{eval}}} method depends crucially |
|
134 on the correctness of the code generator; this is one of the reasons |
|
135 why you should not use adaption (see \secref{sec:adaption}) frivolously.% |
|
136 \end{isamarkuptext}% |
|
137 \isamarkuptrue% |
|
138 % |
|
139 \isamarkupsubsection{Code antiquotation% |
|
140 } |
|
141 \isamarkuptrue% |
|
142 % |
|
143 \begin{isamarkuptext}% |
|
144 In scenarios involving techniques like reflection it is quite common |
|
145 that code generated from a theory forms the basis for implementing |
|
146 a proof procedure in \isa{SML}. To facilitate interfacing of generated code |
|
147 with system code, the code generator provides a \isa{code} antiquotation:% |
|
148 \end{isamarkuptext}% |
|
149 \isamarkuptrue% |
|
150 % |
|
151 \isadelimquote |
|
152 % |
|
153 \endisadelimquote |
|
154 % |
|
155 \isatagquote |
|
156 \isacommand{datatype}\isamarkupfalse% |
|
157 \ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\isanewline |
|
158 \isanewline |
|
159 \isacommand{ML}\isamarkupfalse% |
|
160 \ {\isacharverbatimopen}\isanewline |
|
161 \ \ fun\ eval{\isacharunderscore}form\ % |
|
162 \isaantiq |
|
163 code\ T% |
|
164 \endisaantiq |
|
165 \ {\isacharequal}\ true\isanewline |
|
166 \ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ % |
|
167 \isaantiq |
|
168 code\ F% |
|
169 \endisaantiq |
|
170 \ {\isacharequal}\ false\isanewline |
|
171 \ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}% |
|
172 \isaantiq |
|
173 code\ And% |
|
174 \endisaantiq |
|
175 \ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
176 \ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ andalso\ eval{\isacharunderscore}form\ q\isanewline |
|
177 \ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}% |
|
178 \isaantiq |
|
179 code\ Or% |
|
180 \endisaantiq |
|
181 \ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
182 \ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline |
|
183 {\isacharverbatimclose}% |
|
184 \endisatagquote |
|
185 {\isafoldquote}% |
|
186 % |
|
187 \isadelimquote |
|
188 % |
|
189 \endisadelimquote |
|
190 % |
|
191 \begin{isamarkuptext}% |
|
192 \noindent \isa{code} takes as argument the name of a constant; after the |
|
193 whole \isa{SML} is read, the necessary code is generated transparently |
|
194 and the corresponding constant names are inserted. This technique also |
|
195 allows to use pattern matching on constructors stemming from compiled |
|
196 \isa{datatypes}. |
|
197 |
|
198 For a less simplistic example, theory \hyperlink{theory.Ferrack}{\mbox{\isa{Ferrack}}} is |
|
199 a good reference.% |
|
200 \end{isamarkuptext}% |
|
201 \isamarkuptrue% |
|
202 % |
|
203 \isamarkupsubsection{Imperative data structures% |
|
204 } |
|
205 \isamarkuptrue% |
|
206 % |
|
207 \begin{isamarkuptext}% |
|
208 If you consider imperative data structures as inevitable for a specific |
|
209 application, you should consider |
|
210 \emph{Imperative Functional Programming with Isabelle/HOL} |
|
211 (\cite{bulwahn-et-al:2008:imperative}); |
|
212 the framework described there is available in theory \hyperlink{theory.Imperative-HOL}{\mbox{\isa{Imperative{\isacharunderscore}HOL}}}.% |
|
213 \end{isamarkuptext}% |
|
214 \isamarkuptrue% |
|
215 % |
|
216 \isadelimtheory |
|
217 % |
|
218 \endisadelimtheory |
|
219 % |
|
220 \isatagtheory |
|
221 \isacommand{end}\isamarkupfalse% |
|
222 % |
|
223 \endisatagtheory |
|
224 {\isafoldtheory}% |
|
225 % |
|
226 \isadelimtheory |
|
227 % |
|
228 \endisadelimtheory |
|
229 \isanewline |
|
230 \end{isabellebody}% |
|
231 %%% Local Variables: |
|
232 %%% mode: latex |
|
233 %%% TeX-master: "root" |
|
234 %%% End: |
|