# HG changeset patch # User nipkow # Date 1282042183 -7200 # Node ID 6e7f8121b4f73cd74afd26c5c30a77ba00d82599 # Parent 4c065e97ecee6cb6aafe1f492878adcd6f90e3b6# Parent abc655166d615f5d95b822561469e9dcfbd50b9d merged diff -r abc655166d61 -r 6e7f8121b4f7 doc-src/Codegen/Thy/Adaptation.thy --- a/doc-src/Codegen/Thy/Adaptation.thy Tue Aug 17 12:49:33 2010 +0200 +++ b/doc-src/Codegen/Thy/Adaptation.thy Tue Aug 17 12:49:43 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 abc655166d61 -r 6e7f8121b4f7 doc-src/Codegen/Thy/Refinement.thy --- a/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 12:49:33 2010 +0200 +++ b/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 12:49:43 2010 +0200 @@ -4,6 +4,72 @@ section {* Program and datatype refinement \label{sec:refinement} *} +text {* + Code generation by shallow embedding (cf.~\secref{sec:principle}) + allows to choose code equations and datatype constructors freely, + given that some very basic syntactic properties are met; this + flexibility opens up mechanisms for refinement which allow to extend + the scope and quality of generated code dramatically. +*} + + +subsection {* Program refinement *} + +text {* + Program refinement works by choosing appropriate code equations + explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci + numbers: +*} + +fun %quote fib :: "nat \ nat" where + "fib 0 = 0" + | "fib (Suc 0) = Suc 0" + | "fib (Suc (Suc n)) = fib n + fib (Suc n)" + +text {* + \noindent The runtime of the corresponding code grows exponential due + to two recursive calls: +*} + +text %quote {*@{code_stmts fib (consts) fib (Haskell)}*} + +text {* + \noindent A more efficient implementation would use dynamic + programming, e.g.~sharing of common intermediate results between + recursive calls. This idea is expressed by an auxiliary operation + which computes a Fibonacci number and its successor simultaneously: +*} + +definition %quote fib_step :: "nat \ nat \ nat" where + "fib_step n = (fib (Suc n), fib n)" + +text {* + \noindent This operation can be implemented by recursion using + dynamic programming: +*} + +lemma %quote [code]: + "fib_step 0 = (Suc 0, 0)" + "fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))" + by (simp_all add: fib_step_def) + +text {* + \noindent What remains is to implement @{const fib} by @{const + fib_step} as follows: +*} + +lemma %quote [code]: + "fib 0 = 0" + "fib (Suc n) = fst (fib_step n)" + by (simp_all add: fib_step_def) + +text {* + \noindent The resulting code shows only linear growth of runtime: +*} + +text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*} + + subsection {* Datatypes \label{sec:datatypes} *} text {* diff -r abc655166d61 -r 6e7f8121b4f7 doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Tue Aug 17 12:49:33 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Tue Aug 17 12:49:43 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% % diff -r abc655166d61 -r 6e7f8121b4f7 doc-src/Codegen/Thy/document/Refinement.tex --- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 12:49:33 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 12:49:43 2010 +0200 @@ -22,6 +22,175 @@ } \isamarkuptrue% % +\begin{isamarkuptext}% +Code generation by shallow embedding (cf.~\secref{sec:principle}) + allows to choose code equations and datatype constructors freely, + given that some very basic syntactic properties are met; this + flexibility opens up mechanisms for refinement which allow to extend + the scope and quality of generated code dramatically.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Program refinement% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Program refinement works by choosing appropriate code equations + explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci + numbers:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{fun}\isamarkupfalse% +\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The runtime of the corresponding code grows exponential due + to two recursive calls:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}fib ::~Nat -> Nat;\\ +\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\ +\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\ +\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent A more efficient implementation would use dynamic + programming, e.g.~sharing of common intermediate results between + recursive calls. This idea is expressed by an auxiliary operation + which computes a Fibonacci number and its successor simultaneously:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymtimes}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ n\ {\isacharequal}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharcomma}\ fib\ n{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This operation can be implemented by recursion using + dynamic programming:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n\ in\ {\isacharparenleft}m\ {\isacharplus}\ q{\isacharcomma}\ m{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fib{\isacharunderscore}step{\isacharunderscore}def{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent What remains is to implement \isa{fib} by \isa{fib{\isacharunderscore}step} as follows:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fib{\isacharunderscore}step{\isacharunderscore}def{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The resulting code shows only linear growth of runtime:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\ +\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\ +\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\ +\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\ +\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\ +\hspace*{0pt}\\ +\hspace*{0pt}fib ::~Nat -> Nat;\\ +\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\ +\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% \isamarkupsubsection{Datatypes \label{sec:datatypes}% } \isamarkuptrue%