doc-src/Codegen/Thy/document/Adaptation.tex

specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

%
\begin{isabellebody}%
\def\isabellecontext{Adaptation}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Adaptation\isanewline
\isakeyword{imports}\ Setup\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isadeliminvisible
\isanewline
%
\endisadeliminvisible
%
\isataginvisible
\isacommand{setup}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Code{\isaliteral{5F}{\isacharunderscore}}Target{\isaliteral{2E}{\isachardot}}extend{\isaliteral{5F}{\isacharunderscore}}target\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C534D4C3E}{\isasymSML}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}SML{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ K\ I{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\ Code{\isaliteral{5F}{\isacharunderscore}}Target{\isaliteral{2E}{\isachardot}}extend{\isaliteral{5F}{\isacharunderscore}}target\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C534D4C64756D6D793E}{\isasymSMLdummy}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Haskell{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ K\ I{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isamarkupsection{Adaptation to target languages \label{sec:adaptation}%
}
\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 adaptation you have to treat each target
      language separately.

    \item Application is extremely tedious since there is no
      abstraction which would allow for a static check, making it easy
      to produce garbage.

    \item Subtle errors can be introduced unconsciously.

  \end{itemize}

  \noindent However, even if you ought refrain from setting up
  adaptation yourself, already the \isa{HOL} comes with some
  reasonable default adaptations (say, using target language list
  syntax).  There also some common adaptation 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 adaptation principle%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
  conceptually supposed to be:

  \begin{figure}[here]
    \includegraphics{adaptation}
    \caption{The adaptation principle}
    \label{fig:adaptation}
  \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{adaptation} 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:adaptation_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:adaptation} illustrates, all these
  adaptation mechanisms have to act consistently; it is at the
  discretion of the user to take care for this.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Common adaptation patterns%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \isa{HOL} \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:adaptation_mechanisms}).

  \begin{description}

    \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}] represents \isa{HOL} integers by
       big integer literals in target languages.

    \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}] represents \isa{HOL} characters by
       character literals in target languages.

    \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char{\isaliteral{5F}{\isacharunderscore}}chr}] like \isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}, but
       also offers treatment of character codes; includes \isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}.

    \item[\isa{Efficient{\isaliteral{5F}{\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 \isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}
       and \isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}.

    \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}] 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.  Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.

    \item[\isa{String}] provides an additional datatype \isa{String{\isaliteral{2E}{\isachardot}}literal} which is isomorphic to strings; \isa{String{\isaliteral{2E}{\isachardot}}literal}s are mapped to target-language strings.  Useful
       for code setups which involve e.g.~printing (error) messages.
       Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.

  \end{description}

  \begin{warn}
    When importing any of those theories which are not part of
    \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}, 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:adaptation_mechanisms}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Consider the following function and its corresponding SML code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{primrec}\isamarkupfalse%
\ in{\isaliteral{5F}{\isacharunderscore}}interval\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}in{\isaliteral{5F}{\isacharunderscore}}interval\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ l{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n\ {\isaliteral{5C3C616E643E}{\isasymand}}\ n\ {\isaliteral{5C3C6C653E}{\isasymle}}\ l{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isataginvisible
%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline
\ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline
\ \ datatype\ boola\ {\isaliteral{3D}{\isacharequal}}\ True\ {\isaliteral{7C}{\isacharbar}}\ False\isanewline
\ \ val\ conj\ {\isaliteral{3A}{\isacharcolon}}\ boola\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ boola\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ boola\isanewline
\ \ val\ less{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ boola\isanewline
\ \ val\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ boola\isanewline
\ \ val\ in{\isaliteral{5F}{\isacharunderscore}}interval\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2A}{\isacharasterisk}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ boola\isanewline
end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
\isanewline
datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
datatype\ boola\ {\isaliteral{3D}{\isacharequal}}\ True\ {\isaliteral{7C}{\isacharbar}}\ False{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
fun\ conj\ p\ True\ {\isaliteral{3D}{\isacharequal}}\ p\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ conj\ p\ False\ {\isaliteral{3D}{\isacharequal}}\ False\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ conj\ True\ p\ {\isaliteral{3D}{\isacharequal}}\ p\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ conj\ False\ p\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
fun\ less{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ less{\isaliteral{5F}{\isacharunderscore}}nat\ n\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ False\isanewline
and\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ less{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
fun\ in{\isaliteral{5F}{\isacharunderscore}}interval\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ l{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ conj\ {\isaliteral{28}{\isacharparenleft}}less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ k\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ n\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquotetypewriter
{\isafoldquotetypewriter}%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\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{\isaliteral{5F}{\isacharunderscore}}type}\isamarkupfalse%
\ bool\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}SML\ {\isaliteral{22}{\isachardoublequoteopen}}bool{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}\isamarkupfalse%
\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}SML\ {\isaliteral{22}{\isachardoublequoteopen}}true{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}false{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5F}{\isacharunderscore}}\ andalso\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
\endisatagquotett
{\isafoldquotett}%
%
\isadelimquotett
%
\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\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,
  \indexdef{}{command}{code\_const}\hypertarget{command.code-const}{\hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\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%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline
\ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline
\ \ val\ less{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
\ \ val\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
\ \ val\ in{\isaliteral{5F}{\isacharunderscore}}interval\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2A}{\isacharasterisk}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
\isanewline
datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
fun\ less{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ less{\isaliteral{5F}{\isacharunderscore}}nat\ n\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ false\isanewline
and\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ less{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
fun\ in{\isaliteral{5F}{\isacharunderscore}}interval\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ l{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ k\ n{\isaliteral{29}{\isacharparenright}}\ andalso\ {\isaliteral{28}{\isacharparenleft}}less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ n\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquotetypewriter
{\isafoldquotetypewriter}%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\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{\isaliteral{5F}{\isacharunderscore}}const}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isaliteral{22}{\isachardoublequoteopen}}andalso{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
\endisatagquotett
{\isafoldquotett}%
%
\isadelimquotett
%
\endisadelimquotett
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline
\ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline
\ \ val\ less{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
\ \ val\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
\ \ val\ in{\isaliteral{5F}{\isacharunderscore}}interval\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2A}{\isacharasterisk}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
\isanewline
datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
fun\ less{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ less{\isaliteral{5F}{\isacharunderscore}}nat\ n\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ false\isanewline
and\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ less{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n\isanewline
\ \ {\isaliteral{7C}{\isacharbar}}\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
fun\ in{\isaliteral{5F}{\isacharunderscore}}interval\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ l{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ k\ n\ andalso\ less{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}nat\ n\ l{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquotetypewriter
{\isafoldquotetypewriter}%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\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
  \indexdef{}{command}{code\_reserved}\hypertarget{command.code-reserved}{\hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C534D4C64756D6D793E}{\isasymSMLdummy}}{\isaliteral{22}{\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{\isaliteral{5F}{\isacharunderscore}}type}\isamarkupfalse%
\ prod\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}\isamarkupfalse%
\ Pair\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}SML\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{21}{\isacharbang}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\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 detail 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{equal} class to its counterpart in \isa{Haskell},
  giving custom serialisations for the class \isa{equal} (by command
  \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}) and its operation \isa{HOL{\isaliteral{2E}{\isachardot}}equal}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquotett
%
\endisadelimquotett
%
\isatagquotett
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}\isamarkupfalse%
\ equal\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}Haskell\ {\isaliteral{22}{\isachardoublequoteopen}}Eq{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}HOL{\isaliteral{2E}{\isachardot}}equal{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
\endisatagquotett
{\isafoldquotett}%
%
\isadelimquotett
%
\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent A problem now occurs whenever a type which is an instance
  of \isa{equal} 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\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ equal\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}HOL{\isaliteral{2E}{\isachardot}}equal\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}bar{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{by}\isamarkupfalse%
\ default\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ equal{\isaliteral{5F}{\isacharunderscore}}bar{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\isadelimquotett
\ %
\endisadelimquotett
%
\isatagquotett
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}\isamarkupfalse%
\ bar\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}Haskell\ {\isaliteral{22}{\isachardoublequoteopen}}Integer{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\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 \indexdef{}{command}{code\_instance}\hypertarget{command.code-instance}{\hyperlink{command.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquotett
%
\endisadelimquotett
%
\isatagquotett
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}\isamarkupfalse%
\ bar\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ equal\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}Haskell\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\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 \indexdef{}{command}{code\_include}\hypertarget{command.code-include}{\hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquotett
%
\endisadelimquotett
%
\isatagquotett
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}\isamarkupfalse%
\ Haskell\ {\isaliteral{22}{\isachardoublequoteopen}}Errno{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
{\isaliteral{7B2A}{\isacharverbatimopen}}errno\ i\ {\isaliteral{3D}{\isacharequal}}\ error\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Error\ number{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ show\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
\isanewline
\isacommand{code{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}include}}}} behaves with respect to a particular
  target language.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: