--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Fri Oct 10 15:23:33 2008 +0200
@@ -159,20 +159,20 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
-\isatagquoteme
+\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}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
\isadeliminvisible
%
@@ -187,11 +187,11 @@
%
\endisadeliminvisible
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
-\isatagquoteme
+\isatagquote
%
\begin{isamarkuptext}%
\isaverbatim%
@@ -219,12 +219,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Though this is correct code, it is a little bit unsatisfactory:
@@ -239,23 +239,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\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}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
@@ -270,11 +270,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
-\isatagquoteme
+\isatagquote
%
\begin{isamarkuptext}%
\isaverbatim%
@@ -295,12 +295,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This still is not perfect: the parentheses
@@ -312,26 +312,26 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
-\isatagquoteme
+\isatagquote
%
\begin{isamarkuptext}%
\isaverbatim%
@@ -352,12 +352,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent The attentive reader may ask how we assert that no generated
@@ -369,19 +369,19 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
-\isatagquoteme
+\isatagquote
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
\ {\isachardoublequoteopen}SML\ {\isachardoublequoteclose}\ bool\ true\ false\ andalso%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Next, we try to map HOL pairs to SML pairs, using the
@@ -402,23 +402,23 @@
%
\endisadeliminvisible
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\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}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The initial bang ``\verb|!|'' tells the serializer
@@ -458,11 +458,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
\ eq\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -470,12 +470,12 @@
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent A problem now occurs whenever a type which
@@ -485,11 +485,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
-\isatagquoteme
+\isatagquote
\isacommand{typedecl}\isamarkupfalse%
\ bar\isanewline
\isanewline
@@ -506,29 +506,29 @@
\isanewline
\isacommand{end}\isamarkupfalse%
%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
\isanewline
%
-\isadelimtt
+\isadelimquotett
\isanewline
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ bar\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The code generator would produce
@@ -539,20 +539,20 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\isamarkupsubsection{Enhancing the target language context%
}
@@ -565,23 +565,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\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%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent Such named \isa{include}s are then prepended to every generated code.