1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Codegen/Thy/document/Adaption.tex Tue Mar 03 11:00:51 2009 +0100
1.3 @@ -0,0 +1,679 @@
1.4 +%
1.5 +\begin{isabellebody}%
1.6 +\def\isabellecontext{Adaption}%
1.7 +%
1.8 +\isadelimtheory
1.9 +%
1.10 +\endisadelimtheory
1.11 +%
1.12 +\isatagtheory
1.13 +\isacommand{theory}\isamarkupfalse%
1.14 +\ Adaption\isanewline
1.15 +\isakeyword{imports}\ Setup\isanewline
1.16 +\isakeyword{begin}%
1.17 +\endisatagtheory
1.18 +{\isafoldtheory}%
1.19 +%
1.20 +\isadelimtheory
1.21 +\isanewline
1.22 +%
1.23 +\endisadelimtheory
1.24 +%
1.25 +\isadeliminvisible
1.26 +\isanewline
1.27 +%
1.28 +\endisadeliminvisible
1.29 +%
1.30 +\isataginvisible
1.31 +\isacommand{setup}\isamarkupfalse%
1.32 +\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
1.33 +\endisataginvisible
1.34 +{\isafoldinvisible}%
1.35 +%
1.36 +\isadeliminvisible
1.37 +%
1.38 +\endisadeliminvisible
1.39 +%
1.40 +\isamarkupsection{Adaption to target languages \label{sec:adaption}%
1.41 +}
1.42 +\isamarkuptrue%
1.43 +%
1.44 +\isamarkupsubsection{Adapting code generation%
1.45 +}
1.46 +\isamarkuptrue%
1.47 +%
1.48 +\begin{isamarkuptext}%
1.49 +The aspects of code generation introduced so far have two aspects
1.50 + in common:
1.51 +
1.52 + \begin{itemize}
1.53 + \item They act uniformly, without reference to a specific
1.54 + target language.
1.55 + \item They are \emph{safe} in the sense that as long as you trust
1.56 + the code generator meta theory and implementation, you cannot
1.57 + produce programs that yield results which are not derivable
1.58 + in the logic.
1.59 + \end{itemize}
1.60 +
1.61 + \noindent In this section we will introduce means to \emph{adapt} the serialiser
1.62 + to a specific target language, i.e.~to print program fragments
1.63 + in a way which accommodates \qt{already existing} ingredients of
1.64 + a target language environment, for three reasons:
1.65 +
1.66 + \begin{itemize}
1.67 + \item improving readability and aesthetics of generated code
1.68 + \item gaining efficiency
1.69 + \item interface with language parts which have no direct counterpart
1.70 + in \isa{HOL} (say, imperative data structures)
1.71 + \end{itemize}
1.72 +
1.73 + \noindent Generally, you should avoid using those features yourself
1.74 + \emph{at any cost}:
1.75 +
1.76 + \begin{itemize}
1.77 + \item The safe configuration methods act uniformly on every target language,
1.78 + whereas for adaption you have to treat each target language separate.
1.79 + \item Application is extremely tedious since there is no abstraction
1.80 + which would allow for a static check, making it easy to produce garbage.
1.81 + \item More or less subtle errors can be introduced unconsciously.
1.82 + \end{itemize}
1.83 +
1.84 + \noindent However, even if you ought refrain from setting up adaption
1.85 + yourself, already the \isa{HOL} comes with some reasonable default
1.86 + adaptions (say, using target language list syntax). There also some
1.87 + common adaption cases which you can setup by importing particular
1.88 + library theories. In order to understand these, we provide some clues here;
1.89 + these however are not supposed to replace a careful study of the sources.%
1.90 +\end{isamarkuptext}%
1.91 +\isamarkuptrue%
1.92 +%
1.93 +\isamarkupsubsection{The adaption principle%
1.94 +}
1.95 +\isamarkuptrue%
1.96 +%
1.97 +\begin{isamarkuptext}%
1.98 +The following figure illustrates what \qt{adaption} is conceptually
1.99 + supposed to be:
1.100 +
1.101 + \begin{figure}[here]
1.102 + \begin{tikzpicture}[scale = 0.5]
1.103 + \tikzstyle water=[color = blue, thick]
1.104 + \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
1.105 + \tikzstyle process=[color = green, semithick, ->]
1.106 + \tikzstyle adaption=[color = red, semithick, ->]
1.107 + \tikzstyle target=[color = black]
1.108 + \foreach \x in {0, ..., 24}
1.109 + \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
1.110 + + (0.25, -0.25) cos + (0.25, 0.25);
1.111 + \draw[style=ice] (1, 0) --
1.112 + (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
1.113 + \draw[style=ice] (9, 0) --
1.114 + (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
1.115 + \draw[style=ice] (15, -6) --
1.116 + (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
1.117 + \draw[style=process]
1.118 + (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
1.119 + \draw[style=process]
1.120 + (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
1.121 + \node (adaption) at (11, -2) [style=adaption] {adaption};
1.122 + \node at (19, 3) [rotate=90] {generated};
1.123 + \node at (19.5, -5) {language};
1.124 + \node at (19.5, -3) {library};
1.125 + \node (includes) at (19.5, -1) {includes};
1.126 + \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
1.127 + \draw[style=process]
1.128 + (includes) -- (serialisation);
1.129 + \draw[style=process]
1.130 + (reserved) -- (serialisation);
1.131 + \draw[style=adaption]
1.132 + (adaption) -- (serialisation);
1.133 + \draw[style=adaption]
1.134 + (adaption) -- (includes);
1.135 + \draw[style=adaption]
1.136 + (adaption) -- (reserved);
1.137 + \end{tikzpicture}
1.138 + \caption{The adaption principle}
1.139 + \label{fig:adaption}
1.140 + \end{figure}
1.141 +
1.142 + \noindent In the tame view, code generation acts as broker between
1.143 + \isa{logic}, \isa{intermediate\ language} and
1.144 + \isa{target\ language} by means of \isa{translation} and
1.145 + \isa{serialisation}; for the latter, the serialiser has to observe
1.146 + the structure of the \isa{language} itself plus some \isa{reserved}
1.147 + keywords which have to be avoided for generated code.
1.148 + However, if you consider \isa{adaption} mechanisms, the code generated
1.149 + by the serializer is just the tip of the iceberg:
1.150 +
1.151 + \begin{itemize}
1.152 + \item \isa{serialisation} can be \emph{parametrised} such that
1.153 + logical entities are mapped to target-specific ones
1.154 + (e.g. target-specific list syntax,
1.155 + see also \secref{sec:adaption_mechanisms})
1.156 + \item Such parametrisations can involve references to a
1.157 + target-specific standard \isa{library} (e.g. using
1.158 + the \isa{Haskell} \verb|Maybe| type instead
1.159 + of the \isa{HOL} \isa{option} type);
1.160 + if such are used, the corresponding identifiers
1.161 + (in our example, \verb|Maybe|, \verb|Nothing|
1.162 + and \verb|Just|) also have to be considered \isa{reserved}.
1.163 + \item Even more, the user can enrich the library of the
1.164 + target-language by providing code snippets
1.165 + (\qt{\isa{includes}}) which are prepended to
1.166 + any generated code (see \secref{sec:include}); this typically
1.167 + also involves further \isa{reserved} identifiers.
1.168 + \end{itemize}
1.169 +
1.170 + \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
1.171 + have to act consistently; it is at the discretion of the user
1.172 + to take care for this.%
1.173 +\end{isamarkuptext}%
1.174 +\isamarkuptrue%
1.175 +%
1.176 +\isamarkupsubsection{Common adaption patterns%
1.177 +}
1.178 +\isamarkuptrue%
1.179 +%
1.180 +\begin{isamarkuptext}%
1.181 +The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
1.182 + generator setup
1.183 + which should be suitable for most applications. Common extensions
1.184 + and modifications are available by certain theories of the \isa{HOL}
1.185 + library; beside being useful in applications, they may serve
1.186 + as a tutorial for customising the code generator setup (see below
1.187 + \secref{sec:adaption_mechanisms}).
1.188 +
1.189 + \begin{description}
1.190 +
1.191 + \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
1.192 + integer literals in target languages.
1.193 + \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by
1.194 + character literals in target languages.
1.195 + \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
1.196 + but also offers treatment of character codes; includes
1.197 + \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
1.198 + \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
1.199 + which in general will result in higher efficiency; pattern
1.200 + matching with \isa{{\isadigit{0}}} / \isa{Suc}
1.201 + is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
1.202 + and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
1.203 + \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
1.204 + \isa{index} which is mapped to target-language built-in integers.
1.205 + Useful for code setups which involve e.g. indexing of
1.206 + target-language arrays.
1.207 + \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
1.208 + \isa{message{\isacharunderscore}string} which is isomorphic to strings;
1.209 + \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
1.210 + Useful for code setups which involve e.g. printing (error) messages.
1.211 +
1.212 + \end{description}
1.213 +
1.214 + \begin{warn}
1.215 + When importing any of these theories, they should form the last
1.216 + items in an import list. Since these theories adapt the
1.217 + code generator setup in a non-conservative fashion,
1.218 + strange effects may occur otherwise.
1.219 + \end{warn}%
1.220 +\end{isamarkuptext}%
1.221 +\isamarkuptrue%
1.222 +%
1.223 +\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%
1.224 +}
1.225 +\isamarkuptrue%
1.226 +%
1.227 +\begin{isamarkuptext}%
1.228 +Consider the following function and its corresponding
1.229 + SML code:%
1.230 +\end{isamarkuptext}%
1.231 +\isamarkuptrue%
1.232 +%
1.233 +\isadelimquote
1.234 +%
1.235 +\endisadelimquote
1.236 +%
1.237 +\isatagquote
1.238 +\isacommand{primrec}\isamarkupfalse%
1.239 +\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.240 +\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
1.241 +\endisatagquote
1.242 +{\isafoldquote}%
1.243 +%
1.244 +\isadelimquote
1.245 +%
1.246 +\endisadelimquote
1.247 +%
1.248 +\isadeliminvisible
1.249 +%
1.250 +\endisadeliminvisible
1.251 +%
1.252 +\isataginvisible
1.253 +%
1.254 +\endisataginvisible
1.255 +{\isafoldinvisible}%
1.256 +%
1.257 +\isadeliminvisible
1.258 +%
1.259 +\endisadeliminvisible
1.260 +%
1.261 +\isadelimquote
1.262 +%
1.263 +\endisadelimquote
1.264 +%
1.265 +\isatagquote
1.266 +%
1.267 +\begin{isamarkuptext}%
1.268 +\isatypewriter%
1.269 +\noindent%
1.270 +\hspace*{0pt}structure Example = \\
1.271 +\hspace*{0pt}struct\\
1.272 +\hspace*{0pt}\\
1.273 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1.274 +\hspace*{0pt}\\
1.275 +\hspace*{0pt}datatype boola = True | False;\\
1.276 +\hspace*{0pt}\\
1.277 +\hspace*{0pt}fun anda x True = x\\
1.278 +\hspace*{0pt} ~| anda x False = False\\
1.279 +\hspace*{0pt} ~| anda True x = x\\
1.280 +\hspace*{0pt} ~| anda False x = False;\\
1.281 +\hspace*{0pt}\\
1.282 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
1.283 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
1.284 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
1.285 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
1.286 +\hspace*{0pt}\\
1.287 +\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
1.288 +\hspace*{0pt}\\
1.289 +\hspace*{0pt}end;~(*struct Example*)%
1.290 +\end{isamarkuptext}%
1.291 +\isamarkuptrue%
1.292 +%
1.293 +\endisatagquote
1.294 +{\isafoldquote}%
1.295 +%
1.296 +\isadelimquote
1.297 +%
1.298 +\endisadelimquote
1.299 +%
1.300 +\begin{isamarkuptext}%
1.301 +\noindent Though this is correct code, it is a little bit unsatisfactory:
1.302 + boolean values and operators are materialised as distinguished
1.303 + entities with have nothing to do with the SML-built-in notion
1.304 + of \qt{bool}. This results in less readable code;
1.305 + additionally, eager evaluation may cause programs to
1.306 + loop or break which would perfectly terminate when
1.307 + the existing SML \verb|bool| would be used. To map
1.308 + the HOL \isa{bool} on SML \verb|bool|, we may use
1.309 + \qn{custom serialisations}:%
1.310 +\end{isamarkuptext}%
1.311 +\isamarkuptrue%
1.312 +%
1.313 +\isadelimquotett
1.314 +%
1.315 +\endisadelimquotett
1.316 +%
1.317 +\isatagquotett
1.318 +\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
1.319 +\ bool\isanewline
1.320 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
1.321 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
1.322 +\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
1.323 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
1.324 +\endisatagquotett
1.325 +{\isafoldquotett}%
1.326 +%
1.327 +\isadelimquotett
1.328 +%
1.329 +\endisadelimquotett
1.330 +%
1.331 +\begin{isamarkuptext}%
1.332 +\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
1.333 + as arguments together with a list of custom serialisations.
1.334 + Each custom serialisation starts with a target language
1.335 + identifier followed by an expression, which during
1.336 + code serialisation is inserted whenever the type constructor
1.337 + would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
1.338 + the corresponding mechanism. Each ``\verb|_|'' in
1.339 + a serialisation expression is treated as a placeholder
1.340 + for the type constructor's (the constant's) arguments.%
1.341 +\end{isamarkuptext}%
1.342 +\isamarkuptrue%
1.343 +%
1.344 +\isadelimquote
1.345 +%
1.346 +\endisadelimquote
1.347 +%
1.348 +\isatagquote
1.349 +%
1.350 +\begin{isamarkuptext}%
1.351 +\isatypewriter%
1.352 +\noindent%
1.353 +\hspace*{0pt}structure Example = \\
1.354 +\hspace*{0pt}struct\\
1.355 +\hspace*{0pt}\\
1.356 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1.357 +\hspace*{0pt}\\
1.358 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
1.359 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
1.360 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
1.361 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
1.362 +\hspace*{0pt}\\
1.363 +\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
1.364 +\hspace*{0pt}\\
1.365 +\hspace*{0pt}end;~(*struct Example*)%
1.366 +\end{isamarkuptext}%
1.367 +\isamarkuptrue%
1.368 +%
1.369 +\endisatagquote
1.370 +{\isafoldquote}%
1.371 +%
1.372 +\isadelimquote
1.373 +%
1.374 +\endisadelimquote
1.375 +%
1.376 +\begin{isamarkuptext}%
1.377 +\noindent This still is not perfect: the parentheses
1.378 + around the \qt{andalso} expression are superfluous.
1.379 + Though the serialiser
1.380 + by no means attempts to imitate the rich Isabelle syntax
1.381 + framework, it provides some common idioms, notably
1.382 + associative infixes with precedences which may be used here:%
1.383 +\end{isamarkuptext}%
1.384 +\isamarkuptrue%
1.385 +%
1.386 +\isadelimquotett
1.387 +%
1.388 +\endisadelimquotett
1.389 +%
1.390 +\isatagquotett
1.391 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
1.392 +\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
1.393 +\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
1.394 +\endisatagquotett
1.395 +{\isafoldquotett}%
1.396 +%
1.397 +\isadelimquotett
1.398 +%
1.399 +\endisadelimquotett
1.400 +%
1.401 +\isadelimquote
1.402 +%
1.403 +\endisadelimquote
1.404 +%
1.405 +\isatagquote
1.406 +%
1.407 +\begin{isamarkuptext}%
1.408 +\isatypewriter%
1.409 +\noindent%
1.410 +\hspace*{0pt}structure Example = \\
1.411 +\hspace*{0pt}struct\\
1.412 +\hspace*{0pt}\\
1.413 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1.414 +\hspace*{0pt}\\
1.415 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
1.416 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
1.417 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
1.418 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
1.419 +\hspace*{0pt}\\
1.420 +\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
1.421 +\hspace*{0pt}\\
1.422 +\hspace*{0pt}end;~(*struct Example*)%
1.423 +\end{isamarkuptext}%
1.424 +\isamarkuptrue%
1.425 +%
1.426 +\endisatagquote
1.427 +{\isafoldquote}%
1.428 +%
1.429 +\isadelimquote
1.430 +%
1.431 +\endisadelimquote
1.432 +%
1.433 +\begin{isamarkuptext}%
1.434 +\noindent The attentive reader may ask how we assert that no generated
1.435 + code will accidentally overwrite. For this reason the serialiser has
1.436 + an internal table of identifiers which have to be avoided to be used
1.437 + for new declarations. Initially, this table typically contains the
1.438 + keywords of the target language. It can be extended manually, thus avoiding
1.439 + accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
1.440 +\end{isamarkuptext}%
1.441 +\isamarkuptrue%
1.442 +%
1.443 +\isadelimquote
1.444 +%
1.445 +\endisadelimquote
1.446 +%
1.447 +\isatagquote
1.448 +\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
1.449 +\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
1.450 +\endisatagquote
1.451 +{\isafoldquote}%
1.452 +%
1.453 +\isadelimquote
1.454 +%
1.455 +\endisadelimquote
1.456 +%
1.457 +\begin{isamarkuptext}%
1.458 +\noindent Next, we try to map HOL pairs to SML pairs, using the
1.459 + infix ``\verb|*|'' type constructor and parentheses:%
1.460 +\end{isamarkuptext}%
1.461 +\isamarkuptrue%
1.462 +%
1.463 +\isadeliminvisible
1.464 +%
1.465 +\endisadeliminvisible
1.466 +%
1.467 +\isataginvisible
1.468 +%
1.469 +\endisataginvisible
1.470 +{\isafoldinvisible}%
1.471 +%
1.472 +\isadeliminvisible
1.473 +%
1.474 +\endisadeliminvisible
1.475 +%
1.476 +\isadelimquotett
1.477 +%
1.478 +\endisadelimquotett
1.479 +%
1.480 +\isatagquotett
1.481 +\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
1.482 +\ {\isacharasterisk}\isanewline
1.483 +\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
1.484 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
1.485 +\ Pair\isanewline
1.486 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
1.487 +\endisatagquotett
1.488 +{\isafoldquotett}%
1.489 +%
1.490 +\isadelimquotett
1.491 +%
1.492 +\endisadelimquotett
1.493 +%
1.494 +\begin{isamarkuptext}%
1.495 +\noindent The initial bang ``\verb|!|'' tells the serialiser
1.496 + never to put
1.497 + parentheses around the whole expression (they are already present),
1.498 + while the parentheses around argument place holders
1.499 + tell not to put parentheses around the arguments.
1.500 + The slash ``\verb|/|'' (followed by arbitrary white space)
1.501 + inserts a space which may be used as a break if necessary
1.502 + during pretty printing.
1.503 +
1.504 + These examples give a glimpse what mechanisms
1.505 + custom serialisations provide; however their usage
1.506 + requires careful thinking in order not to introduce
1.507 + inconsistencies -- or, in other words:
1.508 + custom serialisations are completely axiomatic.
1.509 +
1.510 + A further noteworthy details is that any special
1.511 + character in a custom serialisation may be quoted
1.512 + using ``\verb|'|''; thus, in
1.513 + ``\verb|fn '_ => _|'' the first
1.514 + ``\verb|_|'' is a proper underscore while the
1.515 + second ``\verb|_|'' is a placeholder.%
1.516 +\end{isamarkuptext}%
1.517 +\isamarkuptrue%
1.518 +%
1.519 +\isamarkupsubsection{\isa{Haskell} serialisation%
1.520 +}
1.521 +\isamarkuptrue%
1.522 +%
1.523 +\begin{isamarkuptext}%
1.524 +For convenience, the default
1.525 + \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
1.526 + its counterpart in \isa{Haskell}, giving custom serialisations
1.527 + for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
1.528 + \isa{eq{\isacharunderscore}class{\isachardot}eq}%
1.529 +\end{isamarkuptext}%
1.530 +\isamarkuptrue%
1.531 +%
1.532 +\isadelimquotett
1.533 +%
1.534 +\endisadelimquotett
1.535 +%
1.536 +\isatagquotett
1.537 +\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
1.538 +\ eq\isanewline
1.539 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
1.540 +\isanewline
1.541 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
1.542 +\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
1.543 +\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
1.544 +\endisatagquotett
1.545 +{\isafoldquotett}%
1.546 +%
1.547 +\isadelimquotett
1.548 +%
1.549 +\endisadelimquotett
1.550 +%
1.551 +\begin{isamarkuptext}%
1.552 +\noindent A problem now occurs whenever a type which
1.553 + is an instance of \isa{eq} in \isa{HOL} is mapped
1.554 + on a \isa{Haskell}-built-in type which is also an instance
1.555 + of \isa{Haskell} \isa{Eq}:%
1.556 +\end{isamarkuptext}%
1.557 +\isamarkuptrue%
1.558 +%
1.559 +\isadelimquote
1.560 +%
1.561 +\endisadelimquote
1.562 +%
1.563 +\isatagquote
1.564 +\isacommand{typedecl}\isamarkupfalse%
1.565 +\ bar\isanewline
1.566 +\isanewline
1.567 +\isacommand{instantiation}\isamarkupfalse%
1.568 +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
1.569 +\isakeyword{begin}\isanewline
1.570 +\isanewline
1.571 +\isacommand{definition}\isamarkupfalse%
1.572 +\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
1.573 +\isanewline
1.574 +\isacommand{instance}\isamarkupfalse%
1.575 +\ \isacommand{by}\isamarkupfalse%
1.576 +\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline
1.577 +\isanewline
1.578 +\isacommand{end}\isamarkupfalse%
1.579 +%
1.580 +\endisatagquote
1.581 +{\isafoldquote}%
1.582 +%
1.583 +\isadelimquote
1.584 +%
1.585 +\endisadelimquote
1.586 +\isanewline
1.587 +%
1.588 +\isadelimquotett
1.589 +\isanewline
1.590 +%
1.591 +\endisadelimquotett
1.592 +%
1.593 +\isatagquotett
1.594 +\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
1.595 +\ bar\isanewline
1.596 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
1.597 +\endisatagquotett
1.598 +{\isafoldquotett}%
1.599 +%
1.600 +\isadelimquotett
1.601 +%
1.602 +\endisadelimquotett
1.603 +%
1.604 +\begin{isamarkuptext}%
1.605 +\noindent The code generator would produce
1.606 + an additional instance, which of course is rejected by the \isa{Haskell}
1.607 + compiler.
1.608 + To suppress this additional instance, use
1.609 + \isa{code{\isacharunderscore}instance}:%
1.610 +\end{isamarkuptext}%
1.611 +\isamarkuptrue%
1.612 +%
1.613 +\isadelimquotett
1.614 +%
1.615 +\endisadelimquotett
1.616 +%
1.617 +\isatagquotett
1.618 +\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
1.619 +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
1.620 +\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
1.621 +\endisatagquotett
1.622 +{\isafoldquotett}%
1.623 +%
1.624 +\isadelimquotett
1.625 +%
1.626 +\endisadelimquotett
1.627 +%
1.628 +\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
1.629 +}
1.630 +\isamarkuptrue%
1.631 +%
1.632 +\begin{isamarkuptext}%
1.633 +In rare cases it is necessary to \emph{enrich} the context of a
1.634 + target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
1.635 + command:%
1.636 +\end{isamarkuptext}%
1.637 +\isamarkuptrue%
1.638 +%
1.639 +\isadelimquotett
1.640 +%
1.641 +\endisadelimquotett
1.642 +%
1.643 +\isatagquotett
1.644 +\isacommand{code{\isacharunderscore}include}\isamarkupfalse%
1.645 +\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
1.646 +{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
1.647 +\isanewline
1.648 +\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
1.649 +\ Haskell\ Errno%
1.650 +\endisatagquotett
1.651 +{\isafoldquotett}%
1.652 +%
1.653 +\isadelimquotett
1.654 +%
1.655 +\endisadelimquotett
1.656 +%
1.657 +\begin{isamarkuptext}%
1.658 +\noindent Such named \isa{include}s are then prepended to every generated code.
1.659 + Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves
1.660 + with respect to a particular target language.%
1.661 +\end{isamarkuptext}%
1.662 +\isamarkuptrue%
1.663 +%
1.664 +\isadelimtheory
1.665 +%
1.666 +\endisadelimtheory
1.667 +%
1.668 +\isatagtheory
1.669 +\isacommand{end}\isamarkupfalse%
1.670 +%
1.671 +\endisatagtheory
1.672 +{\isafoldtheory}%
1.673 +%
1.674 +\isadelimtheory
1.675 +%
1.676 +\endisadelimtheory
1.677 +\isanewline
1.678 +\end{isabellebody}%
1.679 +%%% Local Variables:
1.680 +%%% mode: latex
1.681 +%%% TeX-master: "root"
1.682 +%%% End: