# HG changeset patch # User haftmann # Date 1282041030 -7200 # Node ID ada5814c9d874ca678eef47101503f6ad97ef719 # Parent f55e77f623ab3f6f2ee42b535d345f455d80aee9 tuned whitespace diff -r f55e77f623ab -r ada5814c9d87 doc-src/Codegen/Thy/Adaptation.thy --- a/doc-src/Codegen/Thy/Adaptation.thy Mon Aug 16 22:56:28 2010 +0200 +++ b/doc-src/Codegen/Thy/Adaptation.thy Tue Aug 17 12:30:30 2010 +0200 @@ -13,18 +13,21 @@ in common: \begin{itemize} - \item They act uniformly, without reference to a specific - target language. + + \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. + 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: + \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 @@ -37,26 +40,34 @@ \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 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 @{text "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. + \noindent However, even if you ought refrain from setting up + adaptation yourself, already the @{text "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. *} + subsection {* The adaptation principle *} text {* - Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is conceptually - supposed to be: + Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is + conceptually supposed to be: \begin{figure}[here] \includegraphics{adaptation} @@ -65,79 +76,87 @@ \end{figure} \noindent In the tame view, code generation acts as broker between - @{text logic}, @{text "intermediate language"} and - @{text "target language"} by means of @{text translation} and - @{text serialisation}; for the latter, the serialiser has to observe - the structure of the @{text language} itself plus some @{text reserved} - keywords which have to be avoided for generated code. - However, if you consider @{text adaptation} mechanisms, the code generated - by the serializer is just the tip of the iceberg: + @{text logic}, @{text "intermediate language"} and @{text "target + language"} by means of @{text translation} and @{text + serialisation}; for the latter, the serialiser has to observe the + structure of the @{text language} itself plus some @{text reserved} + keywords which have to be avoided for generated code. However, if + you consider @{text adaptation} mechanisms, the code generated by + the serializer is just the tip of the iceberg: \begin{itemize} + \item @{text 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}) + (e.g. target-specific list syntax, see also + \secref{sec:adaptation_mechanisms}) + \item Such parametrisations can involve references to a - target-specific standard @{text library} (e.g. using - the @{text Haskell} @{verbatim Maybe} type instead - of the @{text HOL} @{type "option"} type); - if such are used, the corresponding identifiers - (in our example, @{verbatim Maybe}, @{verbatim Nothing} - and @{verbatim Just}) also have to be considered @{text reserved}. + target-specific standard @{text library} (e.g. using the @{text + Haskell} @{verbatim Maybe} type instead of the @{text HOL} + @{type "option"} type); if such are used, the corresponding + identifiers (in our example, @{verbatim Maybe}, @{verbatim + Nothing} and @{verbatim Just}) also have to be considered @{text + reserved}. + \item Even more, the user can enrich the library of the - target-language by providing code snippets - (\qt{@{text "includes"}}) which are prepended to - any generated code (see \secref{sec:include}); this typically - also involves further @{text reserved} identifiers. + target-language by providing code snippets (\qt{@{text + "includes"}}) which are prepended to any generated code (see + \secref{sec:include}); this typically also involves further + @{text 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. + \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. *} subsection {* Common adaptation patterns *} text {* The @{theory HOL} @{theory 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 @{text 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}). + generator setup which should be suitable for most applications. + Common extensions and modifications are available by certain + theories of the @{text 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[@{theory "Code_Integer"}] represents @{text HOL} integers by big - integer literals in target languages. - \item[@{theory "Code_Char"}] represents @{text HOL} characters by + \item[@{theory "Code_Integer"}] represents @{text HOL} integers by + big integer literals in target languages. + + \item[@{theory "Code_Char"}] represents @{text HOL} characters by character literals in target languages. - \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"}, - but also offers treatment of character codes; includes - @{theory "Code_Char"}. - \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers, - which in general will result in higher efficiency; pattern - matching with @{term "0\nat"} / @{const "Suc"} - is eliminated; includes @{theory "Code_Integer"} + + \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"}, but + also offers treatment of character codes; includes @{theory + "Code_Char"}. + + \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements + natural numbers by integers, which in general will result in + higher efficiency; pattern matching with @{term "0\nat"} / + @{const "Suc"} is eliminated; includes @{theory "Code_Integer"} and @{theory "Code_Numeral"}. + \item[@{theory "Code_Numeral"}] provides an additional datatype - @{typ index} which is mapped to target-language built-in integers. - Useful for code setups which involve e.g. indexing of - target-language arrays. - \item[@{theory "String"}] provides an additional datatype - @{typ String.literal} which is isomorphic to strings; - @{typ String.literal}s are mapped to target-language strings. - Useful for code setups which involve e.g. printing (error) messages. + @{typ index} which is mapped to target-language built-in + integers. Useful for code setups which involve e.g.~indexing + of target-language arrays. + + \item[@{theory "String"}] provides an additional datatype @{typ + String.literal} which is isomorphic to strings; @{typ + String.literal}s are mapped to target-language strings. Useful + for code setups which involve e.g.~printing (error) messages. \end{description} \begin{warn} When importing any of these theories, they should form the last - items in an import list. Since these theories adapt the - code generator setup in a non-conservative fashion, - strange effects may occur otherwise. + 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} *} @@ -145,8 +164,7 @@ subsection {* Parametrising serialisation \label{sec:adaptation_mechanisms} *} text {* - Consider the following function and its corresponding - SML code: + Consider the following function and its corresponding SML code: *} primrec %quote in_interval :: "nat \ nat \ nat \ bool" where @@ -160,15 +178,14 @@ text %quote {*@{code_stmts in_interval (SML)}*} text {* - \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 @{verbatim "bool"} would be used. To map - the HOL @{typ bool} on SML @{verbatim "bool"}, we may use - \qn{custom serialisations}: + \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 @{verbatim + "bool"} would be used. To map the HOL @{typ bool} on SML @{verbatim + "bool"}, we may use \qn{custom serialisations}: *} code_type %quotett bool @@ -178,25 +195,23 @@ text {* \noindent The @{command code_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, @{command code_const} implements - the corresponding mechanism. Each ``@{verbatim "_"}'' in - a serialisation expression is treated as a placeholder - for the type constructor's (the constant's) arguments. + 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, + @{command code_const} implements the corresponding mechanism. Each + ``@{verbatim "_"}'' in a serialisation expression is treated as a + placeholder for the type constructor's (the constant's) arguments. *} text %quote {*@{code_stmts in_interval (SML)}*} text {* - \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: + \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: *} code_const %quotett "op \" @@ -205,12 +220,13 @@ text %quote {*@{code_stmts in_interval (SML)}*} text {* - \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 @{command "code_reserved"} command: + \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 + @{command "code_reserved"} command: *} code_reserved %quote "\" bool true false andalso @@ -232,37 +248,33 @@ text {* \noindent The initial bang ``@{verbatim "!"}'' 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 ``@{verbatim "/"}'' (followed by arbitrary white space) - inserts a space which may be used as a break if necessary - during pretty printing. + 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 + ``@{verbatim "/"}'' (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. + These examples give a glimpse what mechanisms custom serialisations + provide; however their usage requires careful thinking in order not + to introduce inconsistencies -- or, in other words: custom + serialisations are completely axiomatic. - A further noteworthy details is that any special - character in a custom serialisation may be quoted - using ``@{verbatim "'"}''; thus, in - ``@{verbatim "fn '_ => _"}'' the first - ``@{verbatim "_"}'' is a proper underscore while the - second ``@{verbatim "_"}'' is a placeholder. + A further noteworthy details is that any special character in a + custom serialisation may be quoted using ``@{verbatim "'"}''; thus, + in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a + proper underscore while the second ``@{verbatim "_"}'' is a + placeholder. *} subsection {* @{text Haskell} serialisation *} text {* - For convenience, the default - @{text HOL} setup for @{text Haskell} maps the @{class eq} class to - its counterpart in @{text Haskell}, giving custom serialisations - for the class @{class eq} (by command @{command code_class}) and its operation - @{const HOL.eq} + For convenience, the default @{text HOL} setup for @{text Haskell} + maps the @{class eq} class to its counterpart in @{text Haskell}, + giving custom serialisations for the class @{class eq} (by command + @{command code_class}) and its operation @{const HOL.eq} *} code_class %quotett eq @@ -272,10 +284,10 @@ (Haskell infixl 4 "==") text {* - \noindent A problem now occurs whenever a type which - is an instance of @{class eq} in @{text HOL} is mapped - on a @{text Haskell}-built-in type which is also an instance - of @{text Haskell} @{text Eq}: + \noindent A problem now occurs whenever a type which is an instance + of @{class eq} in @{text HOL} is mapped on a @{text + Haskell}-built-in type which is also an instance of @{text Haskell} + @{text Eq}: *} typedecl %quote bar @@ -293,11 +305,9 @@ (Haskell "Integer") text {* - \noindent The code generator would produce - an additional instance, which of course is rejected by the @{text Haskell} - compiler. - To suppress this additional instance, use - @{text "code_instance"}: + \noindent The code generator would produce an additional instance, + which of course is rejected by the @{text Haskell} compiler. To + suppress this additional instance, use @{text "code_instance"}: *} code_instance %quotett bar :: eq @@ -308,8 +318,8 @@ text {* In rare cases it is necessary to \emph{enrich} the context of a - target language; this is accomplished using the @{command "code_include"} - command: + target language; this is accomplished using the @{command + "code_include"} command: *} code_include %quotett Haskell "Errno" @@ -318,9 +328,10 @@ code_reserved %quotett Haskell Errno text {* - \noindent Such named @{text include}s are then prepended to every generated code. - Inspect such code in order to find out how @{command "code_include"} behaves - with respect to a particular target language. + \noindent Such named @{text include}s are then prepended to every + generated code. Inspect such code in order to find out how + @{command "code_include"} behaves with respect to a particular + target language. *} end diff -r f55e77f623ab -r ada5814c9d87 doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Mon Aug 16 22:56:28 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Tue Aug 17 12:30:30 2010 +0200 @@ -47,18 +47,21 @@ in common: \begin{itemize} - \item They act uniformly, without reference to a specific - target language. + + \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. + 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: + \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 @@ -71,19 +74,26 @@ \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 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.% + \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% % @@ -92,8 +102,8 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is conceptually - supposed to be: +Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is + conceptually supposed to be: \begin{figure}[here] \includegraphics{adaptation} @@ -102,36 +112,34 @@ \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: + \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}) + (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}. + 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. + 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.% + \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% % @@ -141,43 +149,44 @@ % \begin{isamarkuptext}% The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code - generator setup - which should be suitable for most applications. Common extensions - and modifications are available by certain theories of the \isa{HOL} - library; beside being useful in applications, they may serve - as a tutorial for customising the code generator setup (see below - \secref{sec:adaptation_mechanisms}). + 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[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big - integer literals in target languages. - \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by + \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by + big integer literals in target languages. + + \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by character literals in target languages. - \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char}, - but also offers treatment of character codes; includes - \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}. - \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers, - which in general will result in higher efficiency; pattern - matching with \isa{{\isadigit{0}}} / \isa{Suc} - is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}} + + \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char}, but + also offers treatment of character codes; includes \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}. + + \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements + natural numbers by integers, which in general will result in + higher efficiency; pattern matching with \isa{{\isadigit{0}}} / + \isa{Suc} is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}} and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}. + \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\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. - \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype - \isa{String{\isachardot}literal} which is isomorphic to strings; - \isa{String{\isachardot}literal}s are mapped to target-language strings. - Useful for code setups which involve e.g. printing (error) messages. + \isa{index} which is mapped to target-language built-in + integers. Useful for code setups which involve e.g.~indexing + of target-language arrays. + + \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{String{\isachardot}literal} which is isomorphic to strings; \isa{String{\isachardot}literal}s are mapped to target-language strings. Useful + for code setups which involve e.g.~printing (error) messages. \end{description} \begin{warn} When importing any of these theories, they should form the last - items in an import list. Since these theories adapt the - code generator setup in a non-conservative fashion, - strange effects may occur otherwise. + 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% @@ -187,8 +196,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Consider the following function and its corresponding - SML code:% +Consider the following function and its corresponding SML code:% \end{isamarkuptext}% \isamarkuptrue% % @@ -266,15 +274,12 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent Though this is correct code, it is a little bit unsatisfactory: - boolean values and operators are materialised as distinguished - entities with have nothing to do with the SML-built-in notion - of \qt{bool}. This results in less readable code; - additionally, eager evaluation may cause programs to - loop or break which would perfectly terminate when - the existing SML \verb|bool| would be used. To map - the HOL \isa{bool} on SML \verb|bool|, we may use - \qn{custom serialisations}:% +\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% % @@ -298,14 +303,13 @@ % \begin{isamarkuptext}% \noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor - as arguments together with a list of custom serialisations. - Each custom serialisation starts with a target language - identifier followed by an expression, which during - code serialisation is inserted whenever the type constructor - would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements - the corresponding mechanism. Each ``\verb|_|'' in - a serialisation expression is treated as a placeholder - for the type constructor's (the constant's) arguments.% + as arguments together with a list of custom serialisations. Each + custom serialisation starts with a target language identifier + followed by an expression, which during code serialisation is + inserted whenever the type constructor would occur. For constants, + \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements the corresponding mechanism. Each + ``\verb|_|'' in a serialisation expression is treated as a + placeholder for the type constructor's (the constant's) arguments.% \end{isamarkuptext}% \isamarkuptrue% % @@ -346,12 +350,11 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent This still is not perfect: the parentheses - around the \qt{andalso} expression are superfluous. - Though the serialiser - by no means attempts to imitate the rich Isabelle syntax - framework, it provides some common idioms, notably - associative infixes with precedences which may be used here:% +\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% % @@ -407,12 +410,13 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent The attentive reader may ask how we assert that no generated - code will accidentally overwrite. For this reason the serialiser has - an internal table of identifiers which have to be avoided to be used - for new declarations. Initially, this table typically contains the - keywords of the target language. It can be extended manually, thus avoiding - accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:% +\noindent The attentive reader may ask how we assert that no + generated code will accidentally overwrite. For this reason the + serialiser has an internal table of identifiers which have to be + avoided to be used for new declarations. Initially, this table + typically contains the keywords of the target language. It can be + extended manually, thus avoiding accidental overwrites, using the + \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:% \end{isamarkuptext}% \isamarkuptrue% % @@ -469,26 +473,23 @@ % \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. + 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. + These examples give a glimpse what mechanisms custom serialisations + provide; however their usage requires careful thinking in order not + to introduce inconsistencies -- or, in other words: custom + serialisations are completely axiomatic. - A further noteworthy details is that any special - character in a custom serialisation may be quoted - using ``\verb|'|''; thus, in - ``\verb|fn '_ => _|'' the first - ``\verb|_|'' is a proper underscore while the - second ``\verb|_|'' is a placeholder.% + A further noteworthy details is that any special character in a + custom serialisation may be quoted using ``\verb|'|''; thus, + in ``\verb|fn '_ => _|'' the first ``\verb|_|'' is a + proper underscore while the second ``\verb|_|'' is a + placeholder.% \end{isamarkuptext}% \isamarkuptrue% % @@ -497,11 +498,10 @@ \isamarkuptrue% % \begin{isamarkuptext}% -For convenience, the default - \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to - its counterpart in \isa{Haskell}, giving custom serialisations - for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation - \isa{eq{\isacharunderscore}class{\isachardot}eq}% +For convenience, the default \isa{HOL} setup for \isa{Haskell} + maps the \isa{eq} class to its counterpart in \isa{Haskell}, + giving custom serialisations for the class \isa{eq} (by command + \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation \isa{eq{\isacharunderscore}class{\isachardot}eq}% \end{isamarkuptext}% \isamarkuptrue% % @@ -525,10 +525,9 @@ \endisadelimquotett % \begin{isamarkuptext}% -\noindent A problem now occurs whenever a type which - is an instance of \isa{eq} in \isa{HOL} is mapped - on a \isa{Haskell}-built-in type which is also an instance - of \isa{Haskell} \isa{Eq}:% +\noindent A problem now occurs whenever a type which is an instance + of \isa{eq} in \isa{HOL} is mapped on a \isa{Haskell}-built-in type which is also an instance of \isa{Haskell} + \isa{Eq}:% \end{isamarkuptext}% \isamarkuptrue% % @@ -576,11 +575,9 @@ \endisadelimquotett % \begin{isamarkuptext}% -\noindent The code generator would produce - an additional instance, which of course is rejected by the \isa{Haskell} - compiler. - To suppress this additional instance, use - \isa{code{\isacharunderscore}instance}:% +\noindent The code generator would produce an additional instance, + which of course is rejected by the \isa{Haskell} compiler. To + suppress this additional instance, use \isa{code{\isacharunderscore}instance}:% \end{isamarkuptext}% \isamarkuptrue% % @@ -605,8 +602,7 @@ % \begin{isamarkuptext}% In rare cases it is necessary to \emph{enrich} the context of a - target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} - command:% + target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} command:% \end{isamarkuptext}% \isamarkuptrue% % @@ -629,9 +625,10 @@ \endisadelimquotett % \begin{isamarkuptext}% -\noindent Such named \isa{include}s are then prepended to every generated code. - Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves - with respect to a particular target language.% +\noindent Such named \isa{include}s are then prepended to every + generated code. Inspect such code in order to find out how + \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves with respect to a particular + target language.% \end{isamarkuptext}% \isamarkuptrue% %