--- a/doc-src/Codegen/Thy/document/Adaptation.tex Mon Aug 27 22:31:16 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,651 +0,0 @@
-%
-\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: