doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
author haftmann
Mon Nov 03 14:15:25 2008 +0100 (2008-11-03)
changeset 28714 1992553cccfe
parent 28679 d7384e8e99b3
child 28727 185110a4b97a
permissions -rw-r--r--
improved verbatim mechanism
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Adaption}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Adaption\isanewline
    12 \isakeyword{imports}\ Setup\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 \isanewline
    19 %
    20 \endisadelimtheory
    21 %
    22 \isadeliminvisible
    23 \isanewline
    24 %
    25 \endisadeliminvisible
    26 %
    27 \isataginvisible
    28 \isacommand{setup}\isamarkupfalse%
    29 \ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
    30 \endisataginvisible
    31 {\isafoldinvisible}%
    32 %
    33 \isadeliminvisible
    34 %
    35 \endisadeliminvisible
    36 %
    37 \isamarkupsection{Adaption to target languages \label{sec:adaption}%
    38 }
    39 \isamarkuptrue%
    40 %
    41 \isamarkupsubsection{Adapting code generation%
    42 }
    43 \isamarkuptrue%
    44 %
    45 \begin{isamarkuptext}%
    46 The aspects of code generation introduced so far have two aspects
    47   in common:
    48 
    49   \begin{itemize}
    50     \item They act uniformly, without reference to a specific
    51        target language.
    52     \item They are \emph{safe} in the sense that as long as you trust
    53        the code generator meta theory and implementation, you cannot
    54        produce programs that yield results which are not derivable
    55        in the logic.
    56   \end{itemize}
    57 
    58   \noindent In this section we will introduce means to \emph{adapt} the serialiser
    59   to a specific target language, i.e.~to print program fragments
    60   in a way which accommodates \qt{already existing} ingredients of
    61   a target language environment, for three reasons:
    62 
    63   \begin{itemize}
    64     \item improving readability and aesthetics of generated code
    65     \item gaining efficiency
    66     \item interface with language parts which have no direct counterpart
    67       in \isa{HOL} (say, imperative data structures)
    68   \end{itemize}
    69 
    70   \noindent Generally, you should avoid using those features yourself
    71   \emph{at any cost}:
    72 
    73   \begin{itemize}
    74     \item The safe configuration methods act uniformly on every target language,
    75       whereas for adaption you have to treat each target language separate.
    76     \item Application is extremely tedious since there is no abstraction
    77       which would allow for a static check, making it easy to produce garbage.
    78     \item More or less subtle errors can be introduced unconsciously.
    79   \end{itemize}
    80 
    81   \noindent However, even if you ought refrain from setting up adaption
    82   yourself, already the \isa{HOL} comes with some reasonable default
    83   adaptions (say, using target language list syntax).  There also some
    84   common adaption cases which you can setup by importing particular
    85   library theories.  In order to understand these, we provide some clues here;
    86   these however are not supposed to replace a careful study of the sources.%
    87 \end{isamarkuptext}%
    88 \isamarkuptrue%
    89 %
    90 \isamarkupsubsection{The adaption principle%
    91 }
    92 \isamarkuptrue%
    93 %
    94 \begin{isamarkuptext}%
    95 The following figure illustrates what \qt{adaption} is conceptually
    96   supposed to be:
    97 
    98   \begin{figure}[here]
    99     \begin{tikzpicture}[scale = 0.5]
   100       \tikzstyle water=[color = blue, thick]
   101       \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
   102       \tikzstyle process=[color = green, semithick, ->]
   103       \tikzstyle adaption=[color = red, semithick, ->]
   104       \tikzstyle target=[color = black]
   105       \foreach \x in {0, ..., 24}
   106         \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
   107           + (0.25, -0.25) cos + (0.25, 0.25);
   108       \draw[style=ice] (1, 0) --
   109         (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
   110       \draw[style=ice] (9, 0) --
   111         (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
   112       \draw[style=ice] (15, -6) --
   113         (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
   114       \draw[style=process]
   115         (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
   116       \draw[style=process]
   117         (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
   118       \node (adaption) at (11, -2) [style=adaption] {adaption};
   119       \node at (19, 3) [rotate=90] {generated};
   120       \node at (19.5, -5) {language};
   121       \node at (19.5, -3) {library};
   122       \node (includes) at (19.5, -1) {includes};
   123       \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
   124       \draw[style=process]
   125         (includes) -- (serialisation);
   126       \draw[style=process]
   127         (reserved) -- (serialisation);
   128       \draw[style=adaption]
   129         (adaption) -- (serialisation);
   130       \draw[style=adaption]
   131         (adaption) -- (includes);
   132       \draw[style=adaption]
   133         (adaption) -- (reserved);
   134     \end{tikzpicture}
   135     \caption{The adaption principle}
   136     \label{fig:adaption}
   137   \end{figure}
   138 
   139   \noindent In the tame view, code generation acts as broker between
   140   \isa{logic}, \isa{intermediate\ language} and
   141   \isa{target\ language} by means of \isa{translation} and
   142   \isa{serialisation};  for the latter, the serialiser has to observe
   143   the structure of the \isa{language} itself plus some \isa{reserved}
   144   keywords which have to be avoided for generated code.
   145   However, if you consider \isa{adaption} mechanisms, the code generated
   146   by the serializer is just the tip of the iceberg:
   147 
   148   \begin{itemize}
   149     \item \isa{serialisation} can be \emph{parametrised} such that
   150       logical entities are mapped to target-specific ones
   151       (e.g. target-specific list syntax,
   152         see also \secref{sec:adaption_mechanisms})
   153     \item Such parametrisations can involve references to a
   154       target-specific standard \isa{library} (e.g. using
   155       the \isa{Haskell} \verb|Maybe| type instead
   156       of the \isa{HOL} \isa{option} type);
   157       if such are used, the corresponding identifiers
   158       (in our example, \verb|Maybe|, \verb|Nothing|
   159       and \verb|Just|) also have to be considered \isa{reserved}.
   160     \item Even more, the user can enrich the library of the
   161       target-language by providing code snippets
   162       (\qt{\isa{includes}}) which are prepended to
   163       any generated code (see \secref{sec:include});  this typically
   164       also involves further \isa{reserved} identifiers.
   165   \end{itemize}
   166 
   167   \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
   168   have to act consistently;  it is at the discretion of the user
   169   to take care for this.%
   170 \end{isamarkuptext}%
   171 \isamarkuptrue%
   172 %
   173 \isamarkupsubsection{Common adaption patterns%
   174 }
   175 \isamarkuptrue%
   176 %
   177 \begin{isamarkuptext}%
   178 The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
   179   generator setup
   180   which should be suitable for most applications.  Common extensions
   181   and modifications are available by certain theories of the \isa{HOL}
   182   library; beside being useful in applications, they may serve
   183   as a tutorial for customising the code generator setup (see below
   184   \secref{sec:adaption_mechanisms}).
   185 
   186   \begin{description}
   187 
   188     \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
   189        integer literals in target languages.
   190     \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by 
   191        character literals in target languages.
   192     \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
   193        but also offers treatment of character codes; includes
   194        \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
   195     \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
   196        which in general will result in higher efficiency; pattern
   197        matching with \isa{{\isadigit{0}}} / \isa{Suc}
   198        is eliminated;  includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
   199        and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
   200     \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
   201        \isa{index} which is mapped to target-language built-in integers.
   202        Useful for code setups which involve e.g. indexing of
   203        target-language arrays.
   204     \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
   205        \isa{message{\isacharunderscore}string} which is isomorphic to strings;
   206        \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
   207        Useful for code setups which involve e.g. printing (error) messages.
   208 
   209   \end{description}
   210 
   211   \begin{warn}
   212     When importing any of these theories, they should form the last
   213     items in an import list.  Since these theories adapt the
   214     code generator setup in a non-conservative fashion,
   215     strange effects may occur otherwise.
   216   \end{warn}%
   217 \end{isamarkuptext}%
   218 \isamarkuptrue%
   219 %
   220 \isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%
   221 }
   222 \isamarkuptrue%
   223 %
   224 \begin{isamarkuptext}%
   225 Consider the following function and its corresponding
   226   SML code:%
   227 \end{isamarkuptext}%
   228 \isamarkuptrue%
   229 %
   230 \isadelimquote
   231 %
   232 \endisadelimquote
   233 %
   234 \isatagquote
   235 \isacommand{primrec}\isamarkupfalse%
   236 \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   237 \ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
   238 \endisatagquote
   239 {\isafoldquote}%
   240 %
   241 \isadelimquote
   242 %
   243 \endisadelimquote
   244 %
   245 \isadeliminvisible
   246 %
   247 \endisadeliminvisible
   248 %
   249 \isataginvisible
   250 %
   251 \endisataginvisible
   252 {\isafoldinvisible}%
   253 %
   254 \isadeliminvisible
   255 %
   256 \endisadeliminvisible
   257 %
   258 \isadelimquote
   259 %
   260 \endisadelimquote
   261 %
   262 \isatagquote
   263 %
   264 \begin{isamarkuptext}%
   265 \isaverbatim%
   266 \noindent%
   267 \hspace*{0pt}structure Example = \\
   268 \hspace*{0pt}struct\\
   269 \hspace*{0pt}\\
   270 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   271 \hspace*{0pt}\\
   272 \hspace*{0pt}datatype boola = False | True;\\
   273 \hspace*{0pt}\\
   274 \hspace*{0pt}fun anda x True = x\\
   275 \hspace*{0pt} ~| anda x False = False\\
   276 \hspace*{0pt} ~| anda True x = x\\
   277 \hspace*{0pt} ~| anda False x = False;\\
   278 \hspace*{0pt}\\
   279 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
   280 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
   281 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
   282 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
   283 \hspace*{0pt}\\
   284 \hspace*{0pt}fun in{\char95}interval (k, l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
   285 \hspace*{0pt}\\
   286 \hspace*{0pt}end; (*struct Example*)%
   287 \end{isamarkuptext}%
   288 \isamarkuptrue%
   289 %
   290 \endisatagquote
   291 {\isafoldquote}%
   292 %
   293 \isadelimquote
   294 %
   295 \endisadelimquote
   296 %
   297 \begin{isamarkuptext}%
   298 \noindent Though this is correct code, it is a little bit unsatisfactory:
   299   boolean values and operators are materialised as distinguished
   300   entities with have nothing to do with the SML-built-in notion
   301   of \qt{bool}.  This results in less readable code;
   302   additionally, eager evaluation may cause programs to
   303   loop or break which would perfectly terminate when
   304   the existing SML \verb|bool| would be used.  To map
   305   the HOL \isa{bool} on SML \verb|bool|, we may use
   306   \qn{custom serialisations}:%
   307 \end{isamarkuptext}%
   308 \isamarkuptrue%
   309 %
   310 \isadelimquotett
   311 %
   312 \endisadelimquotett
   313 %
   314 \isatagquotett
   315 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   316 \ bool\isanewline
   317 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
   318 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   319 \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
   320 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
   321 \endisatagquotett
   322 {\isafoldquotett}%
   323 %
   324 \isadelimquotett
   325 %
   326 \endisadelimquotett
   327 %
   328 \begin{isamarkuptext}%
   329 \noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
   330   as arguments together with a list of custom serialisations.
   331   Each custom serialisation starts with a target language
   332   identifier followed by an expression, which during
   333   code serialisation is inserted whenever the type constructor
   334   would occur.  For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
   335   the corresponding mechanism.  Each ``\verb|_|'' in
   336   a serialisation expression is treated as a placeholder
   337   for the type constructor's (the constant's) arguments.%
   338 \end{isamarkuptext}%
   339 \isamarkuptrue%
   340 %
   341 \isadelimquote
   342 %
   343 \endisadelimquote
   344 %
   345 \isatagquote
   346 %
   347 \begin{isamarkuptext}%
   348 \isaverbatim%
   349 \noindent%
   350 \hspace*{0pt}structure Example = \\
   351 \hspace*{0pt}struct\\
   352 \hspace*{0pt}\\
   353 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   354 \hspace*{0pt}\\
   355 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
   356 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
   357 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
   358 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
   359 \hspace*{0pt}\\
   360 \hspace*{0pt}fun in{\char95}interval (k, l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
   361 \hspace*{0pt}\\
   362 \hspace*{0pt}end; (*struct Example*)%
   363 \end{isamarkuptext}%
   364 \isamarkuptrue%
   365 %
   366 \endisatagquote
   367 {\isafoldquote}%
   368 %
   369 \isadelimquote
   370 %
   371 \endisadelimquote
   372 %
   373 \begin{isamarkuptext}%
   374 \noindent This still is not perfect: the parentheses
   375   around the \qt{andalso} expression are superfluous.
   376   Though the serialiser
   377   by no means attempts to imitate the rich Isabelle syntax
   378   framework, it provides some common idioms, notably
   379   associative infixes with precedences which may be used here:%
   380 \end{isamarkuptext}%
   381 \isamarkuptrue%
   382 %
   383 \isadelimquotett
   384 %
   385 \endisadelimquotett
   386 %
   387 \isatagquotett
   388 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   389 \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
   390 \ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
   391 \endisatagquotett
   392 {\isafoldquotett}%
   393 %
   394 \isadelimquotett
   395 %
   396 \endisadelimquotett
   397 %
   398 \isadelimquote
   399 %
   400 \endisadelimquote
   401 %
   402 \isatagquote
   403 %
   404 \begin{isamarkuptext}%
   405 \isaverbatim%
   406 \noindent%
   407 \hspace*{0pt}structure Example = \\
   408 \hspace*{0pt}struct\\
   409 \hspace*{0pt}\\
   410 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   411 \hspace*{0pt}\\
   412 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
   413 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
   414 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
   415 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
   416 \hspace*{0pt}\\
   417 \hspace*{0pt}fun in{\char95}interval (k, l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
   418 \hspace*{0pt}\\
   419 \hspace*{0pt}end; (*struct Example*)%
   420 \end{isamarkuptext}%
   421 \isamarkuptrue%
   422 %
   423 \endisatagquote
   424 {\isafoldquote}%
   425 %
   426 \isadelimquote
   427 %
   428 \endisadelimquote
   429 %
   430 \begin{isamarkuptext}%
   431 \noindent The attentive reader may ask how we assert that no generated
   432   code will accidentally overwrite.  For this reason the serialiser has
   433   an internal table of identifiers which have to be avoided to be used
   434   for new declarations.  Initially, this table typically contains the
   435   keywords of the target language.  It can be extended manually, thus avoiding
   436   accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
   437 \end{isamarkuptext}%
   438 \isamarkuptrue%
   439 %
   440 \isadelimquote
   441 %
   442 \endisadelimquote
   443 %
   444 \isatagquote
   445 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
   446 \ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
   447 \endisatagquote
   448 {\isafoldquote}%
   449 %
   450 \isadelimquote
   451 %
   452 \endisadelimquote
   453 %
   454 \begin{isamarkuptext}%
   455 \noindent Next, we try to map HOL pairs to SML pairs, using the
   456   infix ``\verb|*|'' type constructor and parentheses:%
   457 \end{isamarkuptext}%
   458 \isamarkuptrue%
   459 %
   460 \isadeliminvisible
   461 %
   462 \endisadeliminvisible
   463 %
   464 \isataginvisible
   465 %
   466 \endisataginvisible
   467 {\isafoldinvisible}%
   468 %
   469 \isadeliminvisible
   470 %
   471 \endisadeliminvisible
   472 %
   473 \isadelimquotett
   474 %
   475 \endisadelimquotett
   476 %
   477 \isatagquotett
   478 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   479 \ {\isacharasterisk}\isanewline
   480 \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   481 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   482 \ Pair\isanewline
   483 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
   484 \endisatagquotett
   485 {\isafoldquotett}%
   486 %
   487 \isadelimquotett
   488 %
   489 \endisadelimquotett
   490 %
   491 \begin{isamarkuptext}%
   492 \noindent The initial bang ``\verb|!|'' tells the serialiser
   493   never to put
   494   parentheses around the whole expression (they are already present),
   495   while the parentheses around argument place holders
   496   tell not to put parentheses around the arguments.
   497   The slash ``\verb|/|'' (followed by arbitrary white space)
   498   inserts a space which may be used as a break if necessary
   499   during pretty printing.
   500 
   501   These examples give a glimpse what mechanisms
   502   custom serialisations provide; however their usage
   503   requires careful thinking in order not to introduce
   504   inconsistencies -- or, in other words:
   505   custom serialisations are completely axiomatic.
   506 
   507   A further noteworthy details is that any special
   508   character in a custom serialisation may be quoted
   509   using ``\verb|'|''; thus, in
   510   ``\verb|fn '_ => _|'' the first
   511   ``\verb|_|'' is a proper underscore while the
   512   second ``\verb|_|'' is a placeholder.%
   513 \end{isamarkuptext}%
   514 \isamarkuptrue%
   515 %
   516 \isamarkupsubsection{\isa{Haskell} serialisation%
   517 }
   518 \isamarkuptrue%
   519 %
   520 \begin{isamarkuptext}%
   521 For convenience, the default
   522   \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
   523   its counterpart in \isa{Haskell}, giving custom serialisations
   524   for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
   525   \isa{eq{\isacharunderscore}class{\isachardot}eq}%
   526 \end{isamarkuptext}%
   527 \isamarkuptrue%
   528 %
   529 \isadelimquotett
   530 %
   531 \endisadelimquotett
   532 %
   533 \isatagquotett
   534 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
   535 \ eq\isanewline
   536 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
   537 \isanewline
   538 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   539 \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
   540 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
   541 \endisatagquotett
   542 {\isafoldquotett}%
   543 %
   544 \isadelimquotett
   545 %
   546 \endisadelimquotett
   547 %
   548 \begin{isamarkuptext}%
   549 \noindent A problem now occurs whenever a type which
   550   is an instance of \isa{eq} in \isa{HOL} is mapped
   551   on a \isa{Haskell}-built-in type which is also an instance
   552   of \isa{Haskell} \isa{Eq}:%
   553 \end{isamarkuptext}%
   554 \isamarkuptrue%
   555 %
   556 \isadelimquote
   557 %
   558 \endisadelimquote
   559 %
   560 \isatagquote
   561 \isacommand{typedecl}\isamarkupfalse%
   562 \ bar\isanewline
   563 \isanewline
   564 \isacommand{instantiation}\isamarkupfalse%
   565 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
   566 \isakeyword{begin}\isanewline
   567 \isanewline
   568 \isacommand{definition}\isamarkupfalse%
   569 \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
   570 \isanewline
   571 \isacommand{instance}\isamarkupfalse%
   572 \ \isacommand{by}\isamarkupfalse%
   573 \ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline
   574 \isanewline
   575 \isacommand{end}\isamarkupfalse%
   576 %
   577 \endisatagquote
   578 {\isafoldquote}%
   579 %
   580 \isadelimquote
   581 %
   582 \endisadelimquote
   583 \isanewline
   584 %
   585 \isadelimquotett
   586 \isanewline
   587 %
   588 \endisadelimquotett
   589 %
   590 \isatagquotett
   591 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   592 \ bar\isanewline
   593 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
   594 \endisatagquotett
   595 {\isafoldquotett}%
   596 %
   597 \isadelimquotett
   598 %
   599 \endisadelimquotett
   600 %
   601 \begin{isamarkuptext}%
   602 \noindent The code generator would produce
   603   an additional instance, which of course is rejected by the \isa{Haskell}
   604   compiler.
   605   To suppress this additional instance, use
   606   \isa{code{\isacharunderscore}instance}:%
   607 \end{isamarkuptext}%
   608 \isamarkuptrue%
   609 %
   610 \isadelimquotett
   611 %
   612 \endisadelimquotett
   613 %
   614 \isatagquotett
   615 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
   616 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
   617 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
   618 \endisatagquotett
   619 {\isafoldquotett}%
   620 %
   621 \isadelimquotett
   622 %
   623 \endisadelimquotett
   624 %
   625 \isamarkupsubsection{Enhancing the target language context \label{sec:include}%
   626 }
   627 \isamarkuptrue%
   628 %
   629 \begin{isamarkuptext}%
   630 In rare cases it is necessary to \emph{enrich} the context of a
   631   target language;  this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
   632   command:%
   633 \end{isamarkuptext}%
   634 \isamarkuptrue%
   635 %
   636 \isadelimquotett
   637 %
   638 \endisadelimquotett
   639 %
   640 \isatagquotett
   641 \isacommand{code{\isacharunderscore}include}\isamarkupfalse%
   642 \ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
   643 {\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
   644 \isanewline
   645 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
   646 \ Haskell\ Errno%
   647 \endisatagquotett
   648 {\isafoldquotett}%
   649 %
   650 \isadelimquotett
   651 %
   652 \endisadelimquotett
   653 %
   654 \begin{isamarkuptext}%
   655 \noindent Such named \isa{include}s are then prepended to every generated code.
   656   Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves
   657   with respect to a particular target language.%
   658 \end{isamarkuptext}%
   659 \isamarkuptrue%
   660 %
   661 \isadelimtheory
   662 %
   663 \endisadelimtheory
   664 %
   665 \isatagtheory
   666 \isacommand{end}\isamarkupfalse%
   667 %
   668 \endisatagtheory
   669 {\isafoldtheory}%
   670 %
   671 \isadelimtheory
   672 %
   673 \endisadelimtheory
   674 \isanewline
   675 \end{isabellebody}%
   676 %%% Local Variables:
   677 %%% mode: latex
   678 %%% TeX-master: "root"
   679 %%% End: