doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
changeset 28447 df77ed974a78
child 28456 7a558c872104
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Wed Oct 01 13:33:54 2008 +0200
     1.3 @@ -0,0 +1,484 @@
     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 +%
    1.22 +\endisadelimtheory
    1.23 +%
    1.24 +\isamarkupsection{Adaption to target languages \label{sec:adaption}%
    1.25 +}
    1.26 +\isamarkuptrue%
    1.27 +%
    1.28 +\isamarkupsubsection{Common adaption cases%
    1.29 +}
    1.30 +\isamarkuptrue%
    1.31 +%
    1.32 +\begin{isamarkuptext}%
    1.33 +The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
    1.34 +  generator setup
    1.35 +  which should be suitable for most applications. Common extensions
    1.36 +  and modifications are available by certain theories of the \isa{HOL}
    1.37 +  library; beside being useful in applications, they may serve
    1.38 +  as a tutorial for customising the code generator setup (see below
    1.39 +  \secref{sec:adaption_mechanisms}).
    1.40 +
    1.41 +  \begin{description}
    1.42 +
    1.43 +    \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
    1.44 +       integer literals in target languages.
    1.45 +    \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by 
    1.46 +       character literals in target languages.
    1.47 +    \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
    1.48 +       but also offers treatment of character codes; includes
    1.49 +       \hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}.
    1.50 +    \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
    1.51 +       which in general will result in higher efficiency; pattern
    1.52 +       matching with \isa{{\isadigit{0}}} / \isa{Suc}
    1.53 +       is eliminated;  includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}.
    1.54 +    \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
    1.55 +       \isa{index} which is mapped to target-language built-in integers.
    1.56 +       Useful for code setups which involve e.g. indexing of
    1.57 +       target-language arrays.
    1.58 +    \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
    1.59 +       \isa{message{\isacharunderscore}string} which is isomorphic to strings;
    1.60 +       \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
    1.61 +       Useful for code setups which involve e.g. printing (error) messages.
    1.62 +
    1.63 +  \end{description}
    1.64 +
    1.65 +  \begin{warn}
    1.66 +    When importing any of these theories, they should form the last
    1.67 +    items in an import list.  Since these theories adapt the
    1.68 +    code generator setup in a non-conservative fashion,
    1.69 +    strange effects may occur otherwise.
    1.70 +  \end{warn}%
    1.71 +\end{isamarkuptext}%
    1.72 +\isamarkuptrue%
    1.73 +%
    1.74 +\isamarkupsubsection{Adaption mechanisms \label{sec:adaption_mechanisms}%
    1.75 +}
    1.76 +\isamarkuptrue%
    1.77 +%
    1.78 +\begin{isamarkuptext}%
    1.79 +\begin{warn}
    1.80 +    The mechanisms shown here are especially for the curious;  the user
    1.81 +    rarely needs to do anything on his own beyond the defaults in \isa{HOL}.
    1.82 +    Adaption is a delicated task which requires a lot of dilligence since
    1.83 +    it happend \emph{completely} outside the logic.
    1.84 +  \end{warn}%
    1.85 +\end{isamarkuptext}%
    1.86 +\isamarkuptrue%
    1.87 +%
    1.88 +\begin{isamarkuptext}%
    1.89 +Consider the following function and its corresponding
    1.90 +  SML code:%
    1.91 +\end{isamarkuptext}%
    1.92 +\isamarkuptrue%
    1.93 +%
    1.94 +\isadelimquoteme
    1.95 +%
    1.96 +\endisadelimquoteme
    1.97 +%
    1.98 +\isatagquoteme
    1.99 +\isacommand{primrec}\isamarkupfalse%
   1.100 +\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   1.101 +\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
   1.102 +\endisatagquoteme
   1.103 +{\isafoldquoteme}%
   1.104 +%
   1.105 +\isadelimquoteme
   1.106 +%
   1.107 +\endisadelimquoteme
   1.108 +%
   1.109 +\isadeliminvisible
   1.110 +%
   1.111 +\endisadeliminvisible
   1.112 +%
   1.113 +\isataginvisible
   1.114 +%
   1.115 +\endisataginvisible
   1.116 +{\isafoldinvisible}%
   1.117 +%
   1.118 +\isadeliminvisible
   1.119 +%
   1.120 +\endisadeliminvisible
   1.121 +%
   1.122 +\isadelimquoteme
   1.123 +%
   1.124 +\endisadelimquoteme
   1.125 +%
   1.126 +\isatagquoteme
   1.127 +%
   1.128 +\begin{isamarkuptext}%
   1.129 +\isaverbatim%
   1.130 +\noindent%
   1.131 +\verb|structure Example = |\newline%
   1.132 +\verb|struct|\newline%
   1.133 +\newline%
   1.134 +\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
   1.135 +\newline%
   1.136 +\verb|datatype boola = False |\verb,|,\verb| True;|\newline%
   1.137 +\newline%
   1.138 +\verb|fun anda x True = x|\newline%
   1.139 +\verb|  |\verb,|,\verb| anda x False = False|\newline%
   1.140 +\verb|  |\verb,|,\verb| anda True x = x|\newline%
   1.141 +\verb|  |\verb,|,\verb| anda False x = False;|\newline%
   1.142 +\newline%
   1.143 +\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
   1.144 +\verb|  |\verb,|,\verb| less_nat n Zero_nat = False|\newline%
   1.145 +\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
   1.146 +\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = True;|\newline%
   1.147 +\newline%
   1.148 +\verb|fun in_interval (k, l) n = anda (less_eq_nat k n) (less_eq_nat n l);|\newline%
   1.149 +\newline%
   1.150 +\verb|end; (*struct Example*)|%
   1.151 +\end{isamarkuptext}%
   1.152 +\isamarkuptrue%
   1.153 +%
   1.154 +\endisatagquoteme
   1.155 +{\isafoldquoteme}%
   1.156 +%
   1.157 +\isadelimquoteme
   1.158 +%
   1.159 +\endisadelimquoteme
   1.160 +%
   1.161 +\begin{isamarkuptext}%
   1.162 +\noindent Though this is correct code, it is a little bit unsatisfactory:
   1.163 +  boolean values and operators are materialised as distinguished
   1.164 +  entities with have nothing to do with the SML-built-in notion
   1.165 +  of \qt{bool}.  This results in less readable code;
   1.166 +  additionally, eager evaluation may cause programs to
   1.167 +  loop or break which would perfectly terminate when
   1.168 +  the existing SML \verb|bool| would be used.  To map
   1.169 +  the HOL \isa{bool} on SML \verb|bool|, we may use
   1.170 +  \qn{custom serialisations}:%
   1.171 +\end{isamarkuptext}%
   1.172 +\isamarkuptrue%
   1.173 +%
   1.174 +\isadelimtt
   1.175 +%
   1.176 +\endisadelimtt
   1.177 +%
   1.178 +\isatagtt
   1.179 +\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   1.180 +\ bool\isanewline
   1.181 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.182 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.183 +\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
   1.184 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
   1.185 +\endisatagtt
   1.186 +{\isafoldtt}%
   1.187 +%
   1.188 +\isadelimtt
   1.189 +%
   1.190 +\endisadelimtt
   1.191 +%
   1.192 +\begin{isamarkuptext}%
   1.193 +\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
   1.194 +  as arguments together with a list of custom serialisations.
   1.195 +  Each custom serialisation starts with a target language
   1.196 +  identifier followed by an expression, which during
   1.197 +  code serialisation is inserted whenever the type constructor
   1.198 +  would occur.  For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
   1.199 +  the corresponding mechanism.  Each ``\verb|_|'' in
   1.200 +  a serialisation expression is treated as a placeholder
   1.201 +  for the type constructor's (the constant's) arguments.%
   1.202 +\end{isamarkuptext}%
   1.203 +\isamarkuptrue%
   1.204 +%
   1.205 +\isadelimquoteme
   1.206 +%
   1.207 +\endisadelimquoteme
   1.208 +%
   1.209 +\isatagquoteme
   1.210 +%
   1.211 +\begin{isamarkuptext}%
   1.212 +\isaverbatim%
   1.213 +\noindent%
   1.214 +\verb|structure Example = |\newline%
   1.215 +\verb|struct|\newline%
   1.216 +\newline%
   1.217 +\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
   1.218 +\newline%
   1.219 +\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
   1.220 +\verb|  |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
   1.221 +\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
   1.222 +\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
   1.223 +\newline%
   1.224 +\verb|fun in_interval (k, l) n = (less_eq_nat k n) andalso (less_eq_nat n l);|\newline%
   1.225 +\newline%
   1.226 +\verb|end; (*struct Example*)|%
   1.227 +\end{isamarkuptext}%
   1.228 +\isamarkuptrue%
   1.229 +%
   1.230 +\endisatagquoteme
   1.231 +{\isafoldquoteme}%
   1.232 +%
   1.233 +\isadelimquoteme
   1.234 +%
   1.235 +\endisadelimquoteme
   1.236 +%
   1.237 +\begin{isamarkuptext}%
   1.238 +\noindent This still is not perfect: the parentheses
   1.239 +  around the \qt{andalso} expression are superfluous.
   1.240 +  Though the serializer
   1.241 +  by no means attempts to imitate the rich Isabelle syntax
   1.242 +  framework, it provides some common idioms, notably
   1.243 +  associative infixes with precedences which may be used here:%
   1.244 +\end{isamarkuptext}%
   1.245 +\isamarkuptrue%
   1.246 +%
   1.247 +\isadelimtt
   1.248 +%
   1.249 +\endisadelimtt
   1.250 +%
   1.251 +\isatagtt
   1.252 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.253 +\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
   1.254 +\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
   1.255 +\endisatagtt
   1.256 +{\isafoldtt}%
   1.257 +%
   1.258 +\isadelimtt
   1.259 +%
   1.260 +\endisadelimtt
   1.261 +%
   1.262 +\isadelimquoteme
   1.263 +%
   1.264 +\endisadelimquoteme
   1.265 +%
   1.266 +\isatagquoteme
   1.267 +%
   1.268 +\begin{isamarkuptext}%
   1.269 +\isaverbatim%
   1.270 +\noindent%
   1.271 +\verb|structure Example = |\newline%
   1.272 +\verb|struct|\newline%
   1.273 +\newline%
   1.274 +\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
   1.275 +\newline%
   1.276 +\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
   1.277 +\verb|  |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
   1.278 +\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
   1.279 +\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
   1.280 +\newline%
   1.281 +\verb|fun in_interval (k, l) n = less_eq_nat k n andalso less_eq_nat n l;|\newline%
   1.282 +\newline%
   1.283 +\verb|end; (*struct Example*)|%
   1.284 +\end{isamarkuptext}%
   1.285 +\isamarkuptrue%
   1.286 +%
   1.287 +\endisatagquoteme
   1.288 +{\isafoldquoteme}%
   1.289 +%
   1.290 +\isadelimquoteme
   1.291 +%
   1.292 +\endisadelimquoteme
   1.293 +%
   1.294 +\begin{isamarkuptext}%
   1.295 +\noindent Next, we try to map HOL pairs to SML pairs, using the
   1.296 +  infix ``\verb|*|'' type constructor and parentheses:%
   1.297 +\end{isamarkuptext}%
   1.298 +\isamarkuptrue%
   1.299 +%
   1.300 +\isadeliminvisible
   1.301 +%
   1.302 +\endisadeliminvisible
   1.303 +%
   1.304 +\isataginvisible
   1.305 +%
   1.306 +\endisataginvisible
   1.307 +{\isafoldinvisible}%
   1.308 +%
   1.309 +\isadeliminvisible
   1.310 +%
   1.311 +\endisadeliminvisible
   1.312 +%
   1.313 +\isadelimtt
   1.314 +%
   1.315 +\endisadelimtt
   1.316 +%
   1.317 +\isatagtt
   1.318 +\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   1.319 +\ {\isacharasterisk}\isanewline
   1.320 +\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.321 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.322 +\ Pair\isanewline
   1.323 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
   1.324 +\endisatagtt
   1.325 +{\isafoldtt}%
   1.326 +%
   1.327 +\isadelimtt
   1.328 +%
   1.329 +\endisadelimtt
   1.330 +%
   1.331 +\begin{isamarkuptext}%
   1.332 +\noindent The initial bang ``\verb|!|'' tells the serializer to never put
   1.333 +  parentheses around the whole expression (they are already present),
   1.334 +  while the parentheses around argument place holders
   1.335 +  tell not to put parentheses around the arguments.
   1.336 +  The slash ``\verb|/|'' (followed by arbitrary white space)
   1.337 +  inserts a space which may be used as a break if necessary
   1.338 +  during pretty printing.
   1.339 +
   1.340 +  These examples give a glimpse what mechanisms
   1.341 +  custom serialisations provide; however their usage
   1.342 +  requires careful thinking in order not to introduce
   1.343 +  inconsistencies -- or, in other words:
   1.344 +  custom serialisations are completely axiomatic.
   1.345 +
   1.346 +  A further noteworthy details is that any special
   1.347 +  character in a custom serialisation may be quoted
   1.348 +  using ``\verb|'|''; thus, in
   1.349 +  ``\verb|fn '_ => _|'' the first
   1.350 +  ``\verb|_|'' is a proper underscore while the
   1.351 +  second ``\verb|_|'' is a placeholder.
   1.352 +
   1.353 +  The HOL theories provide further
   1.354 +  examples for custom serialisations.%
   1.355 +\end{isamarkuptext}%
   1.356 +\isamarkuptrue%
   1.357 +%
   1.358 +\isamarkupsubsection{\isa{Haskell} serialisation%
   1.359 +}
   1.360 +\isamarkuptrue%
   1.361 +%
   1.362 +\begin{isamarkuptext}%
   1.363 +For convenience, the default
   1.364 +  \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
   1.365 +  its counterpart in \isa{Haskell}, giving custom serialisations
   1.366 +  for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
   1.367 +  \isa{eq{\isacharunderscore}class{\isachardot}eq}%
   1.368 +\end{isamarkuptext}%
   1.369 +\isamarkuptrue%
   1.370 +%
   1.371 +\isadelimtt
   1.372 +%
   1.373 +\endisadelimtt
   1.374 +%
   1.375 +\isatagtt
   1.376 +\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
   1.377 +\ eq\isanewline
   1.378 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.379 +\isanewline
   1.380 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.381 +\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
   1.382 +\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
   1.383 +\endisatagtt
   1.384 +{\isafoldtt}%
   1.385 +%
   1.386 +\isadelimtt
   1.387 +%
   1.388 +\endisadelimtt
   1.389 +%
   1.390 +\begin{isamarkuptext}%
   1.391 +\noindent A problem now occurs whenever a type which
   1.392 +  is an instance of \isa{eq} in \isa{HOL} is mapped
   1.393 +  on a \isa{Haskell}-built-in type which is also an instance
   1.394 +  of \isa{Haskell} \isa{Eq}:%
   1.395 +\end{isamarkuptext}%
   1.396 +\isamarkuptrue%
   1.397 +%
   1.398 +\isadelimquoteme
   1.399 +%
   1.400 +\endisadelimquoteme
   1.401 +%
   1.402 +\isatagquoteme
   1.403 +\isacommand{typedecl}\isamarkupfalse%
   1.404 +\ bar\isanewline
   1.405 +\isanewline
   1.406 +\isacommand{instantiation}\isamarkupfalse%
   1.407 +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
   1.408 +\isakeyword{begin}\isanewline
   1.409 +\isanewline
   1.410 +\isacommand{definition}\isamarkupfalse%
   1.411 +\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
   1.412 +\isanewline
   1.413 +\isacommand{instance}\isamarkupfalse%
   1.414 +\ \isacommand{by}\isamarkupfalse%
   1.415 +\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline
   1.416 +\isanewline
   1.417 +\isacommand{end}\isamarkupfalse%
   1.418 +%
   1.419 +\endisatagquoteme
   1.420 +{\isafoldquoteme}%
   1.421 +%
   1.422 +\isadelimquoteme
   1.423 +%
   1.424 +\endisadelimquoteme
   1.425 +\isanewline
   1.426 +%
   1.427 +\isadelimtt
   1.428 +\isanewline
   1.429 +%
   1.430 +\endisadelimtt
   1.431 +%
   1.432 +\isatagtt
   1.433 +\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   1.434 +\ bar\isanewline
   1.435 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
   1.436 +\endisatagtt
   1.437 +{\isafoldtt}%
   1.438 +%
   1.439 +\isadelimtt
   1.440 +%
   1.441 +\endisadelimtt
   1.442 +%
   1.443 +\begin{isamarkuptext}%
   1.444 +\noindent The code generator would produce
   1.445 +  an additional instance, which of course is rejectedby the \isa{Haskell}
   1.446 +  compiler.
   1.447 +  To suppress this additional instance, use
   1.448 +  \isa{code{\isacharunderscore}instance}:%
   1.449 +\end{isamarkuptext}%
   1.450 +\isamarkuptrue%
   1.451 +%
   1.452 +\isadelimtt
   1.453 +%
   1.454 +\endisadelimtt
   1.455 +%
   1.456 +\isatagtt
   1.457 +\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
   1.458 +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
   1.459 +\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
   1.460 +\endisatagtt
   1.461 +{\isafoldtt}%
   1.462 +%
   1.463 +\isadelimtt
   1.464 +%
   1.465 +\endisadelimtt
   1.466 +\isanewline
   1.467 +%
   1.468 +\isadelimtheory
   1.469 +\isanewline
   1.470 +%
   1.471 +\endisadelimtheory
   1.472 +%
   1.473 +\isatagtheory
   1.474 +\isacommand{end}\isamarkupfalse%
   1.475 +%
   1.476 +\endisatagtheory
   1.477 +{\isafoldtheory}%
   1.478 +%
   1.479 +\isadelimtheory
   1.480 +%
   1.481 +\endisadelimtheory
   1.482 +\isanewline
   1.483 +\end{isabellebody}%
   1.484 +%%% Local Variables:
   1.485 +%%% mode: latex
   1.486 +%%% TeX-master: "root"
   1.487 +%%% End: