# HG changeset patch # User haftmann # Date 1241618467 -7200 # Node ID 555b56b66fcf85ccd70b5a6cc1c95cac221c22b9 # Parent 396d4d6a1594f468b9db30dbed42a19f3d2fbd95 adaptation replaces adaption diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Makefile --- a/doc-src/Codegen/Makefile Wed May 06 16:01:06 2009 +0200 +++ b/doc-src/Codegen/Makefile Wed May 06 16:01:07 2009 +0200 @@ -17,7 +17,7 @@ dvi: $(NAME).dvi -$(NAME).dvi: $(FILES) isabelle_isar.eps architecture.eps adaption.eps +$(NAME).dvi: $(FILES) isabelle_isar.eps architecture.eps adaptation.eps $(LATEX) $(NAME) $(BIBTEX) $(NAME) $(LATEX) $(NAME) @@ -25,7 +25,7 @@ pdf: $(NAME).pdf -$(NAME).pdf: $(FILES) isabelle_isar.pdf architecture.pdf adaption.pdf +$(NAME).pdf: $(FILES) isabelle_isar.pdf architecture.pdf adaptation.pdf $(PDFLATEX) $(NAME) $(BIBTEX) $(NAME) $(PDFLATEX) $(NAME) @@ -37,17 +37,17 @@ architecture.dvi: Thy/pictures/architecture.tex latex -output-directory=$(dir $@) $< -adaption.dvi: Thy/pictures/adaption.tex +adaptation.dvi: Thy/pictures/adaptation.tex latex -output-directory=$(dir $@) $< architecture.eps: architecture.dvi dvips -E -o $@ $< -adaption.eps: adaption.dvi +adaptation.eps: adaptation.dvi dvips -E -o $@ $< architecture.pdf: architecture.eps epstopdf --outfile=$@ $< -adaption.pdf: adaption.eps +adaptation.pdf: adaptation.eps epstopdf --outfile=$@ $< diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/Adaptation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/Adaptation.thy Wed May 06 16:01:07 2009 +0200 @@ -0,0 +1,326 @@ +theory Adaptation +imports Setup +begin + +setup %invisible {* Code_Target.extend_target ("\", ("SML", K I)) *} + +section {* Adaptation to target languages \label{sec:adaptation} *} + +subsection {* Adapting code generation *} + +text {* + 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 @{text "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 separate. + \item Application is extremely tedious since there is no abstraction + which would allow for a static check, making it easy to produce garbage. + \item More or less 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. +*} + +subsection {* The adaptation principle *} + +text {* + 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 + @{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}) + \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}. + \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. + \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. +*} + +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}). + + \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 + 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"} + and @{theory "Code_Index"}. + \item[@{theory "Code_Index"}] 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 message_string} which is isomorphic to strings; + @{typ message_string}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. + \end{warn} +*} + + +subsection {* Parametrising serialisation \label{sec:adaptation_mechanisms} *} + +text {* + Consider the following function and its corresponding + SML code: +*} + +primrec %quote in_interval :: "nat \ nat \ nat \ bool" where + "in_interval (k, l) n \ k \ n \ n \ l" +(*<*) +code_type %invisible bool + (SML) +code_const %invisible True and False and "op \" and Not + (SML and and and) +(*>*) +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}: +*} + +code_type %quotett bool + (SML "bool") +code_const %quotett True and False and "op \" + (SML "true" and "false" and "_ andalso _") + +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. +*} + +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: +*} + +code_const %quotett "op \" + (SML infixl 1 "andalso") + +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: +*} + +code_reserved %quote "\" bool true false andalso + +text {* + \noindent Next, we try to map HOL pairs to SML pairs, using the + infix ``@{verbatim "*"}'' type constructor and parentheses: +*} +(*<*) +code_type %invisible * + (SML) +code_const %invisible Pair + (SML) +(*>*) +code_type %quotett * + (SML infix 2 "*") +code_const %quotett Pair + (SML "!((_),/ (_))") + +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. + + 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. +*} + + +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} +*} + +code_class %quotett eq + (Haskell "Eq") + +code_const %quotett "op =" + (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}: +*} + +typedecl %quote bar + +instantiation %quote bar :: eq +begin + +definition %quote "eq_class.eq (x\bar) y \ x = y" + +instance %quote by default (simp add: eq_bar_def) + +end %quote (*<*) + +(*>*) code_type %quotett bar + (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"}: +*} + +code_instance %quotett bar :: eq + (Haskell -) + + +subsection {* Enhancing the target language context \label{sec:include} *} + +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: +*} + +code_include %quotett Haskell "Errno" +{*errno i = error ("Error number: " ++ show i)*} + +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. +*} + +end diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/Adaption.thy --- a/doc-src/Codegen/Thy/Adaption.thy Wed May 06 16:01:06 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,326 +0,0 @@ -theory Adaption -imports Setup -begin - -setup %invisible {* Code_Target.extend_target ("\", ("SML", K I)) *} - -section {* Adaption to target languages \label{sec:adaption} *} - -subsection {* Adapting code generation *} - -text {* - 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 @{text "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 adaption you have to treat each target language separate. - \item Application is extremely tedious since there is no abstraction - which would allow for a static check, making it easy to produce garbage. - \item More or less subtle errors can be introduced unconsciously. - \end{itemize} - - \noindent However, even if you ought refrain from setting up adaption - yourself, already the @{text "HOL"} comes with some reasonable default - adaptions (say, using target language list syntax). There also some - common adaption 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 adaption principle *} - -text {* - Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually - supposed to be: - - \begin{figure}[here] - \includegraphics{adaption} - \caption{The adaption principle} - \label{fig:adaption} - \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 adaption} 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:adaption_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}. - \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. - \end{itemize} - - \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms - have to act consistently; it is at the discretion of the user - to take care for this. -*} - -subsection {* Common adaption 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:adaption_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 - 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"} - and @{theory "Code_Index"}. - \item[@{theory "Code_Index"}] 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 "Code_Message"}] provides an additional datatype - @{typ message_string} which is isomorphic to strings; - @{typ message_string}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. - \end{warn} -*} - - -subsection {* Parametrising serialisation \label{sec:adaption_mechanisms} *} - -text {* - Consider the following function and its corresponding - SML code: -*} - -primrec %quote in_interval :: "nat \ nat \ nat \ bool" where - "in_interval (k, l) n \ k \ n \ n \ l" -(*<*) -code_type %invisible bool - (SML) -code_const %invisible True and False and "op \" and Not - (SML and and and) -(*>*) -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}: -*} - -code_type %quotett bool - (SML "bool") -code_const %quotett True and False and "op \" - (SML "true" and "false" and "_ andalso _") - -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. -*} - -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: -*} - -code_const %quotett "op \" - (SML infixl 1 "andalso") - -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: -*} - -code_reserved %quote "\" bool true false andalso - -text {* - \noindent Next, we try to map HOL pairs to SML pairs, using the - infix ``@{verbatim "*"}'' type constructor and parentheses: -*} -(*<*) -code_type %invisible * - (SML) -code_const %invisible Pair - (SML) -(*>*) -code_type %quotett * - (SML infix 2 "*") -code_const %quotett Pair - (SML "!((_),/ (_))") - -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. - - 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. -*} - - -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} -*} - -code_class %quotett eq - (Haskell "Eq") - -code_const %quotett "op =" - (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}: -*} - -typedecl %quote bar - -instantiation %quote bar :: eq -begin - -definition %quote "eq_class.eq (x\bar) y \ x = y" - -instance %quote by default (simp add: eq_bar_def) - -end %quote (*<*) - -(*>*) code_type %quotett bar - (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"}: -*} - -code_instance %quotett bar :: eq - (Haskell -) - - -subsection {* Enhancing the target language context \label{sec:include} *} - -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: -*} - -code_include %quotett Haskell "Errno" -{*errno i = error ("Error number: " ++ show i)*} - -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. -*} - -end diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Wed May 06 16:01:06 2009 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Wed May 06 16:01:07 2009 +0200 @@ -66,7 +66,7 @@ text {* \noindent The soundness of the @{method eval} method depends crucially on the correctness of the code generator; this is one of the reasons - why you should not use adaption (see \secref{sec:adaption}) frivolously. + why you should not use adaptation (see \secref{sec:adaptation}) frivolously. *} subsection {* Code antiquotation *} diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/Introduction.thy --- a/doc-src/Codegen/Thy/Introduction.thy Wed May 06 16:01:06 2009 +0200 +++ b/doc-src/Codegen/Thy/Introduction.thy Wed May 06 16:01:07 2009 +0200 @@ -28,8 +28,8 @@ This manifests in the structure of this tutorial: after a short conceptual introduction with an example (\secref{sec:intro}), we discuss the generic customisation facilities (\secref{sec:program}). - A further section (\secref{sec:adaption}) is dedicated to the matter of - \qn{adaption} to specific target language environments. After some + A further section (\secref{sec:adaptation}) is dedicated to the matter of + \qn{adaptation} to specific target language environments. After some further issues (\secref{sec:further}) we conclude with an overview of some ML programming interfaces (\secref{sec:ml}). diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/ROOT.ML --- a/doc-src/Codegen/Thy/ROOT.ML Wed May 06 16:01:06 2009 +0200 +++ b/doc-src/Codegen/Thy/ROOT.ML Wed May 06 16:01:07 2009 +0200 @@ -4,6 +4,6 @@ use_thy "Introduction"; use_thy "Program"; -use_thy "Adaption"; +use_thy "Adaptation"; use_thy "Further"; use_thy "ML"; diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/document/Adaptation.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed May 06 16:01:07 2009 +0200 @@ -0,0 +1,642 @@ +% +\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% +\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\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 separate. + \item Application is extremely tedious since there is no abstraction + which would allow for a static check, making it easy to produce garbage. + \item More or less 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 \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}). + + \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 + 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}}} + and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}. + \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] 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.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype + \isa{message{\isacharunderscore}string} which is isomorphic to strings; + \isa{message{\isacharunderscore}string}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. + \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{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isadeliminvisible +% +\endisadeliminvisible +% +\isataginvisible +% +\endisataginvisible +{\isafoldinvisible}% +% +\isadeliminvisible +% +\endisadeliminvisible +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example = \\ +\hspace*{0pt}struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype boola = True | False;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun anda x True = x\\ +\hspace*{0pt} ~| anda x False = False\\ +\hspace*{0pt} ~| anda True x = x\\ +\hspace*{0pt} ~| anda False x = False;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\ +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\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}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquotett +% +\endisadelimquotett +% +\isatagquotett +\isacommand{code{\isacharunderscore}type}\isamarkupfalse% +\ bool\isanewline +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline +\isacommand{code{\isacharunderscore}const}\isamarkupfalse% +\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagquotett +{\isafoldquotett}% +% +\isadelimquotett +% +\endisadelimquotett +% +\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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example = \\ +\hspace*{0pt}struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\ +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquotett +% +\endisadelimquotett +% +\isatagquotett +\isacommand{code{\isacharunderscore}const}\isamarkupfalse% +\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline +\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}% +\endisatagquotett +{\isafoldquotett}% +% +\isadelimquotett +% +\endisadelimquotett +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example = \\ +\hspace*{0pt}struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\ +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymSML}{\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{\isacharunderscore}type}\isamarkupfalse% +\ {\isacharasterisk}\isanewline +\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\isacommand{code{\isacharunderscore}const}\isamarkupfalse% +\ Pair\isanewline +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\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 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% +% +\isamarkupsubsection{\isa{Haskell} serialisation% +} +\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}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquotett +% +\endisadelimquotett +% +\isatagquotett +\isacommand{code{\isacharunderscore}class}\isamarkupfalse% +\ eq\isanewline +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline +\isanewline +\isacommand{code{\isacharunderscore}const}\isamarkupfalse% +\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline +\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagquotett +{\isafoldquotett}% +% +\isadelimquotett +% +\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}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{typedecl}\isamarkupfalse% +\ bar\isanewline +\isanewline +\isacommand{instantiation}\isamarkupfalse% +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline +\isakeyword{begin}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{instance}\isamarkupfalse% +\ \isacommand{by}\isamarkupfalse% +\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline +\isanewline +\isacommand{end}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isadelimquotett +\ % +\endisadelimquotett +% +\isatagquotett +\isacommand{code{\isacharunderscore}type}\isamarkupfalse% +\ bar\isanewline +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\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 + \isa{code{\isacharunderscore}instance}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquotett +% +\endisadelimquotett +% +\isatagquotett +\isacommand{code{\isacharunderscore}instance}\isamarkupfalse% +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline +\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\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 \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} + command:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquotett +% +\endisadelimquotett +% +\isatagquotett +\isacommand{code{\isacharunderscore}include}\isamarkupfalse% +\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline +{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline +\isanewline +\isacommand{code{\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{\isacharunderscore}include}}}} behaves + with respect to a particular target language.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/document/Adaption.tex --- a/doc-src/Codegen/Thy/document/Adaption.tex Wed May 06 16:01:06 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,642 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Adaption}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ Adaption\isanewline -\isakeyword{imports}\ Setup\isanewline -\isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -\isanewline -% -\endisadelimtheory -% -\isadeliminvisible -\isanewline -% -\endisadeliminvisible -% -\isataginvisible -\isacommand{setup}\isamarkupfalse% -\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}% -\endisataginvisible -{\isafoldinvisible}% -% -\isadeliminvisible -% -\endisadeliminvisible -% -\isamarkupsection{Adaption to target languages \label{sec:adaption}% -} -\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 adaption you have to treat each target language separate. - \item Application is extremely tedious since there is no abstraction - which would allow for a static check, making it easy to produce garbage. - \item More or less subtle errors can be introduced unconsciously. - \end{itemize} - - \noindent However, even if you ought refrain from setting up adaption - yourself, already the \isa{HOL} comes with some reasonable default - adaptions (say, using target language list syntax). There also some - common adaption 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 adaption principle% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually - supposed to be: - - \begin{figure}[here] - \includegraphics{adaption} - \caption{The adaption principle} - \label{fig:adaption} - \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{adaption} 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:adaption_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:adaption} illustrates, all these adaption mechanisms - have to act consistently; it is at the discretion of the user - to take care for this.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Common adaption patterns% -} -\isamarkuptrue% -% -\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:adaption_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 - 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}}} - and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}. - \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] 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.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype - \isa{message{\isacharunderscore}string} which is isomorphic to strings; - \isa{message{\isacharunderscore}string}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. - \end{warn}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Consider the following function and its corresponding - SML code:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{primrec}\isamarkupfalse% -\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\isadeliminvisible -% -\endisadeliminvisible -% -\isataginvisible -% -\endisataginvisible -{\isafoldinvisible}% -% -\isadeliminvisible -% -\endisadeliminvisible -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example = \\ -\hspace*{0pt}struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype boola = True | False;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun anda x True = x\\ -\hspace*{0pt} ~| anda x False = False\\ -\hspace*{0pt} ~| anda True x = x\\ -\hspace*{0pt} ~| anda False x = False;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ -\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\ -\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ -\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\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}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquotett -% -\endisadelimquotett -% -\isatagquotett -\isacommand{code{\isacharunderscore}type}\isamarkupfalse% -\ bool\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline -\isacommand{code{\isacharunderscore}const}\isamarkupfalse% -\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}% -\endisatagquotett -{\isafoldquotett}% -% -\isadelimquotett -% -\endisadelimquotett -% -\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.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example = \\ -\hspace*{0pt}struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ -\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\ -\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ -\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquotett -% -\endisadelimquotett -% -\isatagquotett -\isacommand{code{\isacharunderscore}const}\isamarkupfalse% -\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline -\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}% -\endisatagquotett -{\isafoldquotett}% -% -\isadelimquotett -% -\endisadelimquotett -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example = \\ -\hspace*{0pt}struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ -\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\ -\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ -\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymSML}{\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{\isacharunderscore}type}\isamarkupfalse% -\ {\isacharasterisk}\isanewline -\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline -\isacommand{code{\isacharunderscore}const}\isamarkupfalse% -\ Pair\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\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 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% -% -\isamarkupsubsection{\isa{Haskell} serialisation% -} -\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}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquotett -% -\endisadelimquotett -% -\isatagquotett -\isacommand{code{\isacharunderscore}class}\isamarkupfalse% -\ eq\isanewline -\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline -\isanewline -\isacommand{code{\isacharunderscore}const}\isamarkupfalse% -\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline -\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% -\endisatagquotett -{\isafoldquotett}% -% -\isadelimquotett -% -\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}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{typedecl}\isamarkupfalse% -\ bar\isanewline -\isanewline -\isacommand{instantiation}\isamarkupfalse% -\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline -\isakeyword{begin}\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{instance}\isamarkupfalse% -\ \isacommand{by}\isamarkupfalse% -\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline -\isanewline -\isacommand{end}\isamarkupfalse% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\isadelimquotett -\ % -\endisadelimquotett -% -\isatagquotett -\isacommand{code{\isacharunderscore}type}\isamarkupfalse% -\ bar\isanewline -\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\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 - \isa{code{\isacharunderscore}instance}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquotett -% -\endisadelimquotett -% -\isatagquotett -\isacommand{code{\isacharunderscore}instance}\isamarkupfalse% -\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline -\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\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 \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} - command:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquotett -% -\endisadelimquotett -% -\isatagquotett -\isacommand{code{\isacharunderscore}include}\isamarkupfalse% -\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline -{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline -\isanewline -\isacommand{code{\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{\isacharunderscore}include}}}} behaves - with respect to a particular target language.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{end}\isamarkupfalse% -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\isanewline -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Wed May 06 16:01:06 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Further.tex Wed May 06 16:01:07 2009 +0200 @@ -132,7 +132,7 @@ \begin{isamarkuptext}% \noindent The soundness of the \hyperlink{method.eval}{\mbox{\isa{eval}}} method depends crucially on the correctness of the code generator; this is one of the reasons - why you should not use adaption (see \secref{sec:adaption}) frivolously.% + why you should not use adaptation (see \secref{sec:adaptation}) frivolously.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Wed May 06 16:01:06 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed May 06 16:01:07 2009 +0200 @@ -46,8 +46,8 @@ This manifests in the structure of this tutorial: after a short conceptual introduction with an example (\secref{sec:intro}), we discuss the generic customisation facilities (\secref{sec:program}). - A further section (\secref{sec:adaption}) is dedicated to the matter of - \qn{adaption} to specific target language environments. After some + A further section (\secref{sec:adaptation}) is dedicated to the matter of + \qn{adaptation} to specific target language environments. After some further issues (\secref{sec:further}) we conclude with an overview of some ML programming interfaces (\secref{sec:ml}). @@ -229,7 +229,7 @@ \hspace*{0pt}module Example where {\char123}\\ \hspace*{0pt}\\ \hspace*{0pt}\\ -\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\ +\hspace*{0pt}foldla ::~forall a{\char95}1 b{\char95}1.~(a{\char95}1 -> b{\char95}1 -> a{\char95}1) -> a{\char95}1 -> [b{\char95}1] -> a{\char95}1;\\ \hspace*{0pt}foldla f a [] = a;\\ \hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\ \hspace*{0pt}\\ diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/Thy/pictures/adaption.tex --- a/doc-src/Codegen/Thy/pictures/adaption.tex Wed May 06 16:01:06 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,52 +0,0 @@ - -\documentclass[12pt]{article} -\usepackage{tikz} - -\begin{document} - -\thispagestyle{empty} -\setlength{\fboxrule}{0.01pt} -\setlength{\fboxsep}{4pt} - -\fcolorbox{white}{white}{ - -\begin{tikzpicture}[scale = 0.5] - \tikzstyle water=[color = blue, thick] - \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white] - \tikzstyle process=[color = green, semithick, ->] - \tikzstyle adaption=[color = red, semithick, ->] - \tikzstyle target=[color = black] - \foreach \x in {0, ..., 24} - \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin - + (0.25, -0.25) cos + (0.25, 0.25); - \draw[style=ice] (1, 0) -- - (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle; - \draw[style=ice] (9, 0) -- - (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle; - \draw[style=ice] (15, -6) -- - (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle; - \draw[style=process] - (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3); - \draw[style=process] - (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3); - \node (adaption) at (11, -2) [style=adaption] {adaption}; - \node at (19, 3) [rotate=90] {generated}; - \node at (19.5, -5) {language}; - \node at (19.5, -3) {library}; - \node (includes) at (19.5, -1) {includes}; - \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57 - \draw[style=process] - (includes) -- (serialisation); - \draw[style=process] - (reserved) -- (serialisation); - \draw[style=adaption] - (adaption) -- (serialisation); - \draw[style=adaption] - (adaption) -- (includes); - \draw[style=adaption] - (adaption) -- (reserved); -\end{tikzpicture} - -} - -\end{document} diff -r 396d4d6a1594 -r 555b56b66fcf doc-src/Codegen/codegen.tex --- a/doc-src/Codegen/codegen.tex Wed May 06 16:01:06 2009 +0200 +++ b/doc-src/Codegen/codegen.tex Wed May 06 16:01:07 2009 +0200 @@ -32,7 +32,7 @@ \input{Thy/document/Introduction.tex} \input{Thy/document/Program.tex} -\input{Thy/document/Adaption.tex} +\input{Thy/document/Adaptation.tex} \input{Thy/document/Further.tex} \input{Thy/document/ML.tex}