updated;
authorwenzelm
Sun Nov 05 21:44:41 2006 +0100 (2006-11-05)
changeset 211860c51cd55a79c
parent 21185 50eca91d8699
child 21187 16fb5afbf228
updated;
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Sun Nov 05 21:44:40 2006 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Sun Nov 05 21:44:41 2006 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4    in most cases while allowing for detailed customization.
     1.5    This manifests in the structure of this tutorial: this introduction
     1.6    continues with a short introduction of concepts.  Section
     1.7 -  \secref{sec:basics} explains how to use the framework naivly,
     1.8 +  \secref{sec:basics} explains how to use the framework naively,
     1.9    presuming a reasonable default setup.  Then, section
    1.10    \secref{sec:advanced} deals with advanced topics,
    1.11    introducing further aspects of the code generator framework
    1.12 @@ -183,15 +183,15 @@
    1.13  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    1.14  \ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
    1.15  \begin{isamarkuptext}%
    1.16 -The \isasymCODEGEN command takes a space-seperated list of
    1.17 +The \isasymCODEGEN command takes a space-separated list of
    1.18    constants together with \qn{serialization directives}
    1.19    in parentheses. These start with a \qn{target language}
    1.20 -  identifer, followed by arguments, their semantics
    1.21 +  identifier, followed by arguments, their semantics
    1.22    depending on the target. In the SML case, a filename
    1.23    is given where to write the generated code to.
    1.24  
    1.25    Internally, the function equations for all selected
    1.26 -  constants are taken, including any tranitivly required
    1.27 +  constants are taken, including any transitively required
    1.28    constants, datatypes and classes, resulting in the following
    1.29    code:
    1.30  
    1.31 @@ -296,7 +296,7 @@
    1.32    function equations (the additional stuff displayed
    1.33    shall not bother us for the moment). If this table does
    1.34    not provide at least one function
    1.35 -  equation, the table of primititve definitions is searched
    1.36 +  equation, the table of primitive definitions is searched
    1.37    whether it provides one.
    1.38  
    1.39    The typical HOL tools are already set up in a way that
    1.40 @@ -412,9 +412,9 @@
    1.41    here we just illustrate its impact on code generation.
    1.42  
    1.43    In a target language, type classes may be represented
    1.44 -  nativly (as in the case of Haskell). For languages
    1.45 +  natively (as in the case of Haskell). For languages
    1.46    like SML, they are implemented using \emph{dictionaries}.
    1.47 -  Our following example specifiedsa class \qt{null},
    1.48 +  Our following example specifies a class \qt{null},
    1.49    assigning to each of its inhabitants a \qt{null} value:%
    1.50  \end{isamarkuptext}%
    1.51  \isamarkuptrue%
    1.52 @@ -477,7 +477,7 @@
    1.53  \isanewline
    1.54  \ \ {\isachardoublequoteopen}dummy\ {\isacharequal}\ head\ {\isacharbrackleft}Some\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ None{\isacharbrackright}{\isachardoublequoteclose}%
    1.55  \begin{isamarkuptext}%
    1.56 -Type classes offer a suitable occassion to introduce
    1.57 +Type classes offer a suitable occasion to introduce
    1.58    the Haskell serializer.  Its usage is almost the same
    1.59    as SML, but, in accordance with conventions
    1.60    some Haskell systems enforce, each module ends
    1.61 @@ -530,7 +530,7 @@
    1.62  \noindent print all cached function equations (i.e.~\emph{after}
    1.63    any applied transformation. Inside the brackets a
    1.64    list of constants may be given; their function
    1.65 -  euqations are added to the cache if not already present.%
    1.66 +  equations are added to the cache if not already present.%
    1.67  \end{isamarkuptext}%
    1.68  \isamarkuptrue%
    1.69  %
    1.70 @@ -565,7 +565,7 @@
    1.71    which should be suitable for most applications. Common extensions
    1.72    and modifications are available by certain theories of the HOL
    1.73    library; beside being useful in applications, they may serve
    1.74 -  as a tutorial for cutomizing the code generator setup.
    1.75 +  as a tutorial for customizing the code generator setup.
    1.76  
    1.77    \begin{description}
    1.78  
    1.79 @@ -574,7 +574,7 @@
    1.80      \item[ExecutableRat] implements rational
    1.81         numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
    1.82      \item[EfficientNat] implements natural numbers by integers,
    1.83 -       which in geneal will result in higher efficency; pattern
    1.84 +       which in general will result in higher efficency; pattern
    1.85         matching with \isa{{\isadigit{0}}} / \isa{Suc}
    1.86         is eliminated. \label{eff_nat}
    1.87      \item[MLString] provides an additional datatype \isa{mlstring};
    1.88 @@ -593,7 +593,7 @@
    1.89  \begin{isamarkuptext}%
    1.90  Before selected function theorems are turned into abstract
    1.91    code, a chain of definitional transformation steps is carried
    1.92 -  out: \emph{preprocessing}. There are three possibilites
    1.93 +  out: \emph{preprocessing}. There are three possibilities
    1.94    to customize preprocessing: \emph{inline theorems},
    1.95    \emph{inline procedures} and \emph{generic preprocessors}.
    1.96  
    1.97 @@ -603,7 +603,7 @@
    1.98    hand side and the arguments of the left hand side of an
    1.99    equation, but never to the constant heading the left hand side.
   1.100    Inline theorems may be declared an undeclared using the
   1.101 -  \emph{code inline} or \emph{code noinline} attribute respectivly.
   1.102 +  \emph{code inline} or \emph{code noinline} attribute respectively.
   1.103  
   1.104    Some common applications:%
   1.105  \end{isamarkuptext}%
   1.106 @@ -687,7 +687,7 @@
   1.107    \begin{warn}
   1.108      The order in which single preprocessing steps are carried
   1.109      out currently is not specified; in particular, preprocessing
   1.110 -    is \emph{no} fixpoint process.  Keep this in mind when
   1.111 +    is \emph{no} fix point process.  Keep this in mind when
   1.112      setting up the preprocessor.
   1.113  
   1.114      Further, the attribute \emph{code unfold}
   1.115 @@ -776,7 +776,7 @@
   1.116  \lstsml{Thy/examples/bool2.ML}
   1.117  
   1.118    This still is not perfect: the parentheses
   1.119 -  around \qt{andalso} are superfluos.  Though the serializer
   1.120 +  around \qt{andalso} are superfluous.  Though the serializer
   1.121    by no means attempts to imitate the rich Isabelle syntax
   1.122    framework, it provides some common idioms, notably
   1.123    associative infixes with precedences which may be used here:%
   1.124 @@ -812,22 +812,63 @@
   1.125    inserts a space which may be used as a break if necessary
   1.126    during pretty printing.
   1.127  
   1.128 -  So far,%
   1.129 +  So far, we did only provide more idiomatic serializations for
   1.130 +  constructs which would be executable on their own.  Target-specific
   1.131 +  serializations may also be used to \emph{implement} constructs
   1.132 +  which have no implicit notion of executability.  For example,
   1.133 +  take the HOL integers:%
   1.134 +\end{isamarkuptext}%
   1.135 +\isamarkuptrue%
   1.136 +\isacommand{definition}\isamarkupfalse%
   1.137 +\isanewline
   1.138 +\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
   1.139 +\ \ {\isachardoublequoteopen}double{\isacharunderscore}inc\ k\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
   1.140 +\isanewline
   1.141 +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   1.142 +\ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   1.143 +\begin{isamarkuptext}%
   1.144 +will fail: \isa{int} in HOL is implemented using a quotient
   1.145 +  type, which does not provide any notion of executability.
   1.146 +  \footnote{Eventually, we also want to provide executability
   1.147 +  for quotients.}.  However, we could use the SML builtin
   1.148 +  integers:%
   1.149  \end{isamarkuptext}%
   1.150  \isamarkuptrue%
   1.151  \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   1.152  \ int\isanewline
   1.153  \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}int{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.154 -\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.155  \isanewline
   1.156  \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.157  \ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
   1.158 -\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharminus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
   1.159  \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharasterisk}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
   1.160 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharminus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.161 -\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{6}}\ {\isachardoublequoteopen}{\isacharplus}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{6}}\ {\isachardoublequoteopen}{\isacharminus}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}%
   1.162 -\isamarkupsubsection{Types matter%
   1.163 -}
   1.164 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.165 +\isanewline
   1.166 +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   1.167 +\ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   1.168 +\begin{isamarkuptext}%
   1.169 +resulting in:
   1.170 +
   1.171 +  \lstsml{Thy/examples/integers.ML}%
   1.172 +\end{isamarkuptext}%
   1.173 +\isamarkuptrue%
   1.174 +%
   1.175 +\begin{isamarkuptext}%
   1.176 +These examples give a glimpse what powerful mechanisms
   1.177 +  custom serializations provide; however their usage
   1.178 +  requires careful thinking in order not to introduce
   1.179 +  inconsistencies -- or, in other words:
   1.180 +  custom serializations are completely axiomatic.
   1.181 +
   1.182 +  A further noteworthy details is that any special
   1.183 +  character in a custom serialization may be quoted
   1.184 +  using \qt{'}; thus, in \qt{fn '\_ => \_} the first
   1.185 +  \qt{'\_} is a proper underscore while the
   1.186 +  second \qt{\_} is a placeholder.
   1.187 +
   1.188 +  The HOL theories provide further
   1.189 +  examples for custom serializations and form
   1.190 +  a recommended tutorial on how to use them properly.%
   1.191 +\end{isamarkuptext}%
   1.192  \isamarkuptrue%
   1.193  %
   1.194  \isamarkupsubsection{Concerning operational equality%
   1.195 @@ -865,7 +906,7 @@
   1.196  \endisadelimproof
   1.197  %
   1.198  \begin{isamarkuptext}%
   1.199 -The membership test during preprocessing is rewritting,
   1.200 +The membership test during preprocessing is rewriting,
   1.201    resulting in \isa{op\ mem}, which itself
   1.202    performs an explicit equality check.%
   1.203  \end{isamarkuptext}%
   1.204 @@ -903,7 +944,7 @@
   1.205  \isanewline
   1.206  \isacommand{defs}\isamarkupfalse%
   1.207  \isanewline
   1.208 -\ \ eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}eq\ {\isasymequiv}\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}{\isachardoublequoteclose}%
   1.209 +\ \ eq\ {\isacharcolon}\ {\isachardoublequoteopen}eq\ {\isasymequiv}\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}{\isachardoublequoteclose}%
   1.210  \begin{isamarkuptext}%
   1.211  This merely introduces a class \isa{eq} with corresponding
   1.212    operation \isa{eq}, which by definition is isomorphic
   1.213 @@ -933,23 +974,37 @@
   1.214  \end{isamarkuptext}%
   1.215  \isamarkuptrue%
   1.216  %
   1.217 -\begin {description}
   1.218 -    \item[code lemmas and customary serializations for equality]
   1.219 -      Examine the following: \\
   1.220 +\isamarkupsubsubsection{code lemmas and customary serializations for equality%
   1.221 +}
   1.222 +\isamarkuptrue%
   1.223 +%
   1.224 +\begin{isamarkuptext}%
   1.225 +Examine the following:%
   1.226 +\end{isamarkuptext}%
   1.227 +\isamarkuptrue%
   1.228  \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.229  \ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   1.230  \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
   1.231 -\\ What is wrong here? Since \isa{op\ {\isacharequal}} is nothing else then
   1.232 +\begin{isamarkuptext}%
   1.233 +What is wrong here? Since \isa{op\ {\isacharequal}} is nothing else then
   1.234    a plain constant, this customary serialization will refer
   1.235    to polymorphic equality \isa{op\ {\isacharequal}}.
   1.236    Instead, we want the specific equality on \isa{int},
   1.237 -  by using the overloaded constant \isa{Code{\isacharunderscore}Generator{\isachardot}eq}: \\
   1.238 +  by using the overloaded constant \isa{Code{\isacharunderscore}Generator{\isachardot}eq}:%
   1.239 +\end{isamarkuptext}%
   1.240 +\isamarkuptrue%
   1.241  \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.242  \ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   1.243  \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
   1.244 -\\ \item[typedecls interpretated by customary serializations] A
   1.245 -  common idiom is to use unspecified types for formalizations
   1.246 -  and interpret them for a specific target language: \\
   1.247 +\isamarkupsubsubsection{typedecls interpretated by customary serializations%
   1.248 +}
   1.249 +\isamarkuptrue%
   1.250 +%
   1.251 +\begin{isamarkuptext}%
   1.252 +A common idiom is to use unspecified types for formalizations
   1.253 +  and interpret them for a specific target language:%
   1.254 +\end{isamarkuptext}%
   1.255 +\isamarkuptrue%
   1.256  \isacommand{typedecl}\isamarkupfalse%
   1.257  \ key\isanewline
   1.258  \isanewline
   1.259 @@ -977,10 +1032,13 @@
   1.260  \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   1.261  \ key\isanewline
   1.262  \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}string{\isachardoublequoteclose}{\isacharparenright}%
   1.263 -\\ This, though, is not sufficient: \isa{key} is no instance
   1.264 +\begin{isamarkuptext}%
   1.265 +This, though, is not sufficient: \isa{key} is no instance
   1.266    of \isa{eq} since \isa{key} is no datatype; the instance
   1.267    has to be declared manually, including a serialization
   1.268 -  for the particular instance of \isa{Code{\isacharunderscore}Generator{\isachardot}eq}: \\
   1.269 +  for the particular instance of \isa{Code{\isacharunderscore}Generator{\isachardot}eq}:%
   1.270 +\end{isamarkuptext}%
   1.271 +\isamarkuptrue%
   1.272  \isacommand{instance}\isamarkupfalse%
   1.273  \ key\ {\isacharcolon}{\isacharcolon}\ eq%
   1.274  \isadelimproof
   1.275 @@ -1001,7 +1059,10 @@
   1.276  \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.277  \ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   1.278  \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
   1.279 -\\ Then everything goes fine: \\
   1.280 +\begin{isamarkuptext}%
   1.281 +Then everything goes fine:%
   1.282 +\end{isamarkuptext}%
   1.283 +\isamarkuptrue%
   1.284  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   1.285  \ lookup\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lookup{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   1.286  \begin{isamarkuptext}%
   1.287 @@ -1009,25 +1070,79 @@
   1.288  \end{isamarkuptext}%
   1.289  \isamarkuptrue%
   1.290  %
   1.291 -\item[lexicographic orderings and corregularity] Another sublety
   1.292 +\isamarkupsubsubsection{lexicographic orderings and coregularity%
   1.293 +}
   1.294 +\isamarkuptrue%
   1.295 +%
   1.296 +\begin{isamarkuptext}%
   1.297 +Another subtlety
   1.298    enters the stage when definitions of overloaded constants
   1.299    are dependent on operational equality.  For example, let
   1.300 -  us define a lexicographic ordering on tuples: \\
   1.301 +  us define a lexicographic ordering on tuples: \\%
   1.302 +\end{isamarkuptext}%
   1.303 +\isamarkuptrue%
   1.304 +%
   1.305 +\isadelimML
   1.306 +%
   1.307 +\endisadelimML
   1.308 +%
   1.309 +\isatagML
   1.310 +%
   1.311 +\endisatagML
   1.312 +{\isafoldML}%
   1.313 +%
   1.314 +\isadelimML
   1.315 +%
   1.316 +\endisadelimML
   1.317  \isanewline
   1.318 +\isacommand{instance}\isamarkupfalse%
   1.319 +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
   1.320 +\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   1.321 +\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.322 +\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}p{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ \ {\isacharequal}\ p{\isadigit{2}}{\isachardoublequoteclose}%
   1.323 +\isadelimproof
   1.324 +\ %
   1.325 +\endisadelimproof
   1.326 +%
   1.327 +\isatagproof
   1.328 +\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   1.329  \isanewline
   1.330  %
   1.331 -\\ Then code generation will fail.  Why?  The definition
   1.332 +\endisatagproof
   1.333 +{\isafoldproof}%
   1.334 +%
   1.335 +\isadelimproof
   1.336 +%
   1.337 +\endisadelimproof
   1.338 +%
   1.339 +\isadelimML
   1.340 +%
   1.341 +\endisadelimML
   1.342 +%
   1.343 +\isatagML
   1.344 +%
   1.345 +\endisatagML
   1.346 +{\isafoldML}%
   1.347 +%
   1.348 +\isadelimML
   1.349 +%
   1.350 +\endisadelimML
   1.351 +%
   1.352 +\begin{isamarkuptext}%
   1.353 +Then code generation will fail.  Why?  The definition
   1.354    of \isa{op\ {\isasymle}} depends on equality on both arguments,
   1.355 -  which are polymorhpic and impose an additional \isa{eq}
   1.356 +  which are polymorphic and impose an additional \isa{eq}
   1.357    class constraint, thus violating the type discipline
   1.358    for class operations.
   1.359  
   1.360 -  The solution is to add \isa{eq} to both sort arguments: \\
   1.361 +  The solution is to add \isa{eq} to both sort arguments:%
   1.362 +\end{isamarkuptext}%
   1.363 +\isamarkuptrue%
   1.364  \isacommand{instance}\isamarkupfalse%
   1.365  \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequoteopen}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isachardoublequoteclose}{\isacharcomma}\ {\isachardoublequoteopen}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\ ord\isanewline
   1.366 -\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   1.367 +\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   1.368  \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.369 -\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymor}\ p{\isadigit{1}}\ {\isacharequal}\ p{\isadigit{2}}{\isachardoublequoteclose}%
   1.370 +\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}p{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ \ {\isacharequal}\ p{\isadigit{2}}{\isachardoublequoteclose}%
   1.371  \isadelimproof
   1.372  \ %
   1.373  \endisadelimproof
   1.374 @@ -1042,7 +1157,10 @@
   1.375  %
   1.376  \endisadelimproof
   1.377  %
   1.378 -\\ Then code generation succeeds: \\
   1.379 +\begin{isamarkuptext}%
   1.380 +Then code generation succeeds:%
   1.381 +\end{isamarkuptext}%
   1.382 +\isamarkuptrue%
   1.383  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   1.384  \ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   1.385  \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   1.386 @@ -1051,10 +1169,113 @@
   1.387  \end{isamarkuptext}%
   1.388  \isamarkuptrue%
   1.389  %
   1.390 -\item[Haskell serialization]
   1.391 +\isamarkupsubsubsection{Haskell serialization%
   1.392 +}
   1.393 +\isamarkuptrue%
   1.394 +%
   1.395 +\begin{isamarkuptext}%
   1.396 +For convenience, the default
   1.397 +  HOL setup for Haskell maps the \isa{eq} class to
   1.398 +  its counterpart in Haskell, giving custom serializations
   1.399 +  for the class (\isasymCODECLASS) and its operation:%
   1.400 +\end{isamarkuptext}%
   1.401 +\isamarkuptrue%
   1.402 +%
   1.403 +\isadelimML
   1.404 +%
   1.405 +\endisadelimML
   1.406 +%
   1.407 +\isatagML
   1.408 +%
   1.409 +\endisatagML
   1.410 +{\isafoldML}%
   1.411 +%
   1.412 +\isadelimML
   1.413 +%
   1.414 +\endisadelimML
   1.415 +\isanewline
   1.416 +\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
   1.417 +\ eq\isanewline
   1.418 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ eq\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.419 +\isanewline
   1.420 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.421 +\ eq\isanewline
   1.422 +\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.423 +%
   1.424 +\isadelimML
   1.425 +%
   1.426 +\endisadelimML
   1.427 +%
   1.428 +\isatagML
   1.429 +%
   1.430 +\endisatagML
   1.431 +{\isafoldML}%
   1.432 +%
   1.433 +\isadelimML
   1.434 +%
   1.435 +\endisadelimML
   1.436  %
   1.437 -\end {description}
   1.438 +\begin{isamarkuptext}%
   1.439 +A problem now occurs whenever a type which
   1.440 +  is an instance of \isa{eq} in HOL is mapped
   1.441 +  on a Haskell-builtin type which is also an instance
   1.442 +  of Haskell \isa{Eq}:%
   1.443 +\end{isamarkuptext}%
   1.444 +\isamarkuptrue%
   1.445 +\isacommand{typedecl}\isamarkupfalse%
   1.446 +\ bar\isanewline
   1.447 +\isanewline
   1.448 +\isacommand{instance}\isamarkupfalse%
   1.449 +\ bar\ {\isacharcolon}{\isacharcolon}\ eq%
   1.450 +\isadelimproof
   1.451 +\ %
   1.452 +\endisadelimproof
   1.453 +%
   1.454 +\isatagproof
   1.455 +\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   1.456 +%
   1.457 +\endisatagproof
   1.458 +{\isafoldproof}%
   1.459 +%
   1.460 +\isadelimproof
   1.461  %
   1.462 +\endisadelimproof
   1.463 +\isanewline
   1.464 +\isanewline
   1.465 +\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   1.466 +\ bar\isanewline
   1.467 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
   1.468 +\begin{isamarkuptext}%
   1.469 +The code generator would produce
   1.470 +    an additional instance, which of course is rejected.
   1.471 +    To suppress this additional instance, use
   1.472 +    \isasymCODEINSTANCE:%
   1.473 +\end{isamarkuptext}%
   1.474 +\isamarkuptrue%
   1.475 +\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
   1.476 +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
   1.477 +\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
   1.478 +\isamarkupsubsection{Types matter%
   1.479 +}
   1.480 +\isamarkuptrue%
   1.481 +%
   1.482 +\begin{isamarkuptext}%
   1.483 +Imagine the following quick-and-dirty setup for implementing
   1.484 +  some sets as lists:%
   1.485 +\end{isamarkuptext}%
   1.486 +\isamarkuptrue%
   1.487 +\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   1.488 +\ set\isanewline
   1.489 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharunderscore}\ list{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.490 +\isanewline
   1.491 +\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.492 +\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ insert\isanewline
   1.493 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharcolon}{\isacharcolon}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.494 +\isanewline
   1.495 +\isacommand{definition}\isamarkupfalse%
   1.496 +\isanewline
   1.497 +\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
   1.498 +\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbraceright}{\isachardoublequoteclose}%
   1.499  \isamarkupsubsection{Axiomatic extensions%
   1.500  }
   1.501  \isamarkuptrue%