doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex

-%
-\begin{isabellebody}%
-\def\isabellecontext{Adaption}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Adaption\isanewline
-\isakeyword{imports}\ Setup\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-%
-\isadeliminvisible
-\isanewline
-%
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isamarkupsection{Adaption to target languages \label{sec:adaption}%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Adapting code generation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The aspects of code generation introduced so far have two aspects
-  in common:
-
-  \begin{itemize}
-    \item They act uniformly, without reference to a specific
-       target language.
-    \item They are \emph{safe} in the sense that as long as you trust
-       the code generator meta theory and implementation, you cannot
-       produce programs that yield results which are not derivable
-       in the logic.
-  \end{itemize}
-
-  \noindent In this section we will introduce means to \emph{adapt} the serialiser
-  to a specific target language, i.e.~to print program fragments
-  in a way which accommodates \qt{already existing} ingredients of
-  a target language environment, for three reasons:
-
-  \begin{itemize}
-    \item improving readability and aesthetics of generated code
-    \item gaining efficiency
-    \item interface with language parts which have no direct counterpart
-      in \isa{HOL} (say, imperative data structures)
-  \end{itemize}
-
-  \noindent Generally, you should avoid using those features yourself
-  \emph{at any cost}:
-
-  \begin{itemize}
-    \item The safe configuration methods act uniformly on every target language,
-      whereas for adaption you have to treat each target language separate.
-    \item Application is extremely tedious since there is no abstraction
-      which would allow for a static check, making it easy to produce garbage.
-    \item More or less subtle errors can be introduced unconsciously.
-  \end{itemize}
-
-  \noindent However, even if you ought refrain from setting up adaption
-  yourself, already the \isa{HOL} comes with some reasonable default
-  adaptions (say, using target language list syntax).  There also some
-  common adaption cases which you can setup by importing particular
-  library theories.  In order to understand these, we provide some clues here;
-  these however are not supposed to replace a careful study of the sources.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{The adaption principle%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The following figure illustrates what \qt{adaption} is conceptually
-  supposed to be:
-
-  \begin{figure}[here]
-    \begin{tikzpicture}[scale = 0.5]
-      \tikzstyle water=[color = blue, thick]
-      \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
-      \tikzstyle process=[color = green, semithick, ->]
-      \tikzstyle adaption=[color = red, semithick, ->]
-      \tikzstyle target=[color = black]
-      \foreach \x in {0, ..., 24}
-        \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
-          + (0.25, -0.25) cos + (0.25, 0.25);
-      \draw[style=ice] (1, 0) --
-        (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
-      \draw[style=ice] (9, 0) --
-        (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
-      \draw[style=ice] (15, -6) --
-        (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
-      \draw[style=process]
-        (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
-      \draw[style=process]
-        (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
-      \node (adaption) at (11, -2) [style=adaption] {adaption};
-      \node at (19, 3) [rotate=90] {generated};
-      \node at (19.5, -5) {language};
-      \node at (19.5, -3) {library};
-      \node (includes) at (19.5, -1) {includes};
-      \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
-      \draw[style=process]
-        (includes) -- (serialisation);
-      \draw[style=process]
-        (reserved) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (includes);
-      \draw[style=adaption]
-        (adaption) -- (reserved);
-    \end{tikzpicture}
-    \caption{The adaption principle}
-    \label{fig:adaption}
-  \end{figure}
-
-  \noindent In the tame view, code generation acts as broker between
-  \isa{logic}, \isa{intermediate\ language} and
-  \isa{target\ language} by means of \isa{translation} and
-  \isa{serialisation};  for the latter, the serialiser has to observe
-  the structure of the \isa{language} itself plus some \isa{reserved}
-  keywords which have to be avoided for generated code.
-  However, if you consider \isa{adaption} mechanisms, the code generated
-  by the serializer is just the tip of the iceberg:
-
-  \begin{itemize}
-    \item \isa{serialisation} can be \emph{parametrised} such that
-      logical entities are mapped to target-specific ones
-      (e.g. target-specific list syntax,
-        see also \secref{sec:adaption_mechanisms})
-    \item Such parametrisations can involve references to a
-      target-specific standard \isa{library} (e.g. using
-      the \isa{Haskell} \verb|Maybe| type instead
-      of the \isa{HOL} \isa{option} type);
-      if such are used, the corresponding identifiers
-      (in our example, \verb|Maybe|, \verb|Nothing|
-      and \verb|Just|) also have to be considered \isa{reserved}.
-    \item Even more, the user can enrich the library of the
-      target-language by providing code snippets
-      (\qt{\isa{includes}}) which are prepended to
-      any generated code (see \secref{sec:include});  this typically
-      also involves further \isa{reserved} identifiers.
-  \end{itemize}
-
-  \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
-  have to act consistently;  it is at the discretion of the user
-  to take care for this.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Common adaption patterns%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
-  generator setup
-  which should be suitable for most applications.  Common extensions
-  and modifications are available by certain theories of the \isa{HOL}
-  library; beside being useful in applications, they may serve
-  as a tutorial for customising the code generator setup (see below
-  \secref{sec:adaption_mechanisms}).
-
-  \begin{description}
-
-    \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
-       integer literals in target languages.
-    \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by 
-       character literals in target languages.
-    \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
-       but also offers treatment of character codes; includes
-       \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
-    \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
-       which in general will result in higher efficiency; pattern
-       matching with \isa{{\isadigit{0}}} / \isa{Suc}
-       is eliminated;  includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
-       and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
-    \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
-       \isa{index} which is mapped to target-language built-in integers.
-       Useful for code setups which involve e.g. indexing of
-       target-language arrays.
-    \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
-       \isa{message{\isacharunderscore}string} which is isomorphic to strings;
-       \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
-       Useful for code setups which involve e.g. printing (error) messages.
-
-  \end{description}
-
-  \begin{warn}
-    When importing any of these theories, they should form the last
-    items in an import list.  Since these theories adapt the
-    code generator setup in a non-conservative fashion,
-    strange effects may occur otherwise.
-  \end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Consider the following function and its corresponding
-  SML code:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{primrec}\isamarkupfalse%
-\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype boola = True | False;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun anda x True = x\\
-\hspace*{0pt} ~| anda x False = False\\
-\hspace*{0pt} ~| anda True x = x\\
-\hspace*{0pt} ~| anda False x = False;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Though this is correct code, it is a little bit unsatisfactory:
-  boolean values and operators are materialised as distinguished
-  entities with have nothing to do with the SML-built-in notion
-  of \qt{bool}.  This results in less readable code;
-  additionally, eager evaluation may cause programs to
-  loop or break which would perfectly terminate when
-  the existing SML \verb|bool| would be used.  To map
-  the HOL \isa{bool} on SML \verb|bool|, we may use
-  \qn{custom serialisations}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ bool\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
-  as arguments together with a list of custom serialisations.
-  Each custom serialisation starts with a target language
-  identifier followed by an expression, which during
-  code serialisation is inserted whenever the type constructor
-  would occur.  For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
-  the corresponding mechanism.  Each ``\verb|_|'' in
-  a serialisation expression is treated as a placeholder
-  for the type constructor's (the constant's) arguments.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This still is not perfect: the parentheses
-  around the \qt{andalso} expression are superfluous.
-  Though the serialiser
-  by no means attempts to imitate the rich Isabelle syntax
-  framework, it provides some common idioms, notably
-  associative infixes with precedences which may be used here:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The attentive reader may ask how we assert that no generated
-  code will accidentally overwrite.  For this reason the serialiser has
-  an internal table of identifiers which have to be avoided to be used
-  for new declarations.  Initially, this table typically contains the
-  keywords of the target language.  It can be extended manually, thus avoiding
-  accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Next, we try to map HOL pairs to SML pairs, using the
-  infix ``\verb|*|'' type constructor and parentheses:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ {\isacharasterisk}\isanewline
-\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ Pair\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent The initial bang ``\verb|!|'' tells the serialiser
-  never to put
-  parentheses around the whole expression (they are already present),
-  while the parentheses around argument place holders
-  tell not to put parentheses around the arguments.
-  The slash ``\verb|/|'' (followed by arbitrary white space)
-  inserts a space which may be used as a break if necessary
-  during pretty printing.
-
-  These examples give a glimpse what mechanisms
-  custom serialisations provide; however their usage
-  requires careful thinking in order not to introduce
-  inconsistencies -- or, in other words:
-  custom serialisations are completely axiomatic.
-
-  A further noteworthy details is that any special
-  character in a custom serialisation may be quoted
-  using ``\verb|'|''; thus, in
-  ``\verb|fn '_ => _|'' the first
-  ``\verb|_|'' is a proper underscore while the
-  second ``\verb|_|'' is a placeholder.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{\isa{Haskell} serialisation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-For convenience, the default
-  \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
-  its counterpart in \isa{Haskell}, giving custom serialisations
-  for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
-  \isa{eq{\isacharunderscore}class{\isachardot}eq}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
-\ eq\isanewline
-\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent A problem now occurs whenever a type which
-  is an instance of \isa{eq} in \isa{HOL} is mapped
-  on a \isa{Haskell}-built-in type which is also an instance
-  of \isa{Haskell} \isa{Eq}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{typedecl}\isamarkupfalse%
-\ bar\isanewline
-\isanewline
-\isacommand{instantiation}\isamarkupfalse%
-\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{by}\isamarkupfalse%
-\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-\isanewline
-%
-\isadelimquotett
-\isanewline
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ bar\isanewline
-\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent The code generator would produce
-  an additional instance, which of course is rejected by the \isa{Haskell}
-  compiler.
-  To suppress this additional instance, use
-  \isa{code{\isacharunderscore}instance}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
-\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
-\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In rare cases it is necessary to \emph{enrich} the context of a
-  target language;  this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
-  command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}include}\isamarkupfalse%
-\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
-{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ Haskell\ Errno%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent Such named \isa{include}s are then prepended to every generated code.
-  Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves
-  with respect to a particular target language.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: