# HG changeset patch
# User haftmann
# Date 1223613950 -7200
# Node ID 056255ade52a732f295ddc6889bd3dd3e4341244
# Parent  625e44455f52884b40b4117f12cfdeac60c4fbf5
some adaption

diff -r 625e44455f52 -r 056255ade52a doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 10 06:45:49 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 10 06:45:50 2008 +0200
@@ -2,8 +2,68 @@
 imports Setup
 begin
 
+setup %invisible {* Code_Target.extend_target ("SML ", ("SML", 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 accomodates \qt{already existing} ingredients of
+  a target language environment, for three reasons:
+
+  \begin{itemize}
+    \item improving readability and aethetics 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, makeing it easy to produce garbage.
+    \item More or less subtle erros 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 {*
+  \begin{tikzpicture}
+    \draw (0, 0) circle (1cm);
+    \draw (0.5, 0) circle (0.5cm);
+    \draw (0, 0.5) circle (0.5cm);
+    \draw (-0.5, 0) circle (0.5cm);
+    \draw (0, -0.5) circle (0.5cm);
+  \end{tikzpicture}
+*}
+
 subsection {* Common adaption cases *}
 
 text {*
@@ -23,11 +83,12 @@
        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_chr"}.
+       @{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\<Colon>nat"} / @{const "Suc"}
-       is eliminated;  includes @{theory "Code_Integer"}.
+       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
@@ -51,16 +112,7 @@
 subsection {* Adaption mechanisms \label{sec:adaption_mechanisms} *}
 
 text {*
-  \begin{warn}
-    The mechanisms shown here are especially for the curious;  the user
-    rarely needs to do anything on his own beyond the defaults in @{text HOL}.
-    Adaption is a delicated task which requires a lot of dilligence since
-    it happend \emph{completely} outside the logic.
-  \end{warn}
-*}
-
-text {*
-  \noindent Consider the following function and its corresponding
+  Consider the following function and its corresponding
   SML code:
 *}
 
@@ -120,6 +172,17 @@
 text %quoteme {*@{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 %quoteme "SML " bool true false andalso
+
+text {*
   \noindent Next, we try to map HOL pairs to SML pairs, using the
   infix ``@{verbatim "*"}'' type constructor and parentheses:
 *}
@@ -135,7 +198,8 @@
   (SML "!((_),/ (_))")
 
 text {*
-  \noindent The initial bang ``@{verbatim "!"}'' tells the serializer to never put
+  \noindent The initial bang ``@{verbatim "!"}'' tells the serializer
+  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.
@@ -155,9 +219,6 @@
   ``@{verbatim "fn '_ => _"}'' the first
   ``@{verbatim "_"}'' is a proper underscore while the
   second ``@{verbatim "_"}'' is a placeholder.
-
-  The HOL theories provide further
-  examples for custom serialisations.
 *}
 
 
@@ -209,4 +270,24 @@
 code_instance %tt bar :: eq
   (Haskell -)
 
+
+subsection {* Enhancing the target language context *}
+
+text {*
+  In rare cases it is neccessary to \emph{enrich} the context of a
+  target language;  this is accomplished using the @{command "code_include"}
+  command:
+*}
+
+code_include %tt Haskell "Errno"
+{*errno i = error ("Error number: " ++ show i)*}
+
+code_reserved %tt 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 625e44455f52 -r 056255ade52a doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 10 06:45:49 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 10 06:45:50 2008 +0200
@@ -15,13 +15,93 @@
 {\isafoldtheory}%
 %
 \isadelimtheory
+\isanewline
 %
 \endisadelimtheory
 %
+\isadeliminvisible
+\isanewline
+%
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{setup}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}SML\ {\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ 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 accomodates \qt{already existing} ingredients of
+  a target language environment, for three reasons:
+
+  \begin{itemize}
+    \item improving readability and aethetics 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, makeing it easy to produce garbage.
+    \item More or less subtle erros 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}%
+\begin{tikzpicture}
+    \draw (0, 0) circle (1cm);
+    \draw (0.5, 0) circle (0.5cm);
+    \draw (0, 0.5) circle (0.5cm);
+    \draw (-0.5, 0) circle (0.5cm);
+    \draw (0, -0.5) circle (0.5cm);
+  \end{tikzpicture}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Common adaption cases%
 }
 \isamarkuptrue%
@@ -43,11 +123,12 @@
        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-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}.
+       \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}}}.
+       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
@@ -73,17 +154,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-\begin{warn}
-    The mechanisms shown here are especially for the curious;  the user
-    rarely needs to do anything on his own beyond the defaults in \isa{HOL}.
-    Adaption is a delicated task which requires a lot of dilligence since
-    it happend \emph{completely} outside the logic.
-  \end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\noindent Consider the following function and its corresponding
+Consider the following function and its corresponding
   SML code:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -289,6 +360,30 @@
 \endisadelimquoteme
 %
 \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%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
+\ {\isachardoublequoteopen}SML\ {\isachardoublequoteclose}\ bool\ true\ false\ andalso%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
 \noindent Next, we try to map HOL pairs to SML pairs, using the
   infix ``\verb|*|'' type constructor and parentheses:%
 \end{isamarkuptext}%
@@ -326,7 +421,8 @@
 \endisadelimtt
 %
 \begin{isamarkuptext}%
-\noindent The initial bang ``\verb|!|'' tells the serializer to never put
+\noindent The initial bang ``\verb|!|'' tells the serializer
+  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.
@@ -345,10 +441,7 @@
   using ``\verb|'|''; thus, in
   ``\verb|fn '_ => _|'' the first
   ``\verb|_|'' is a proper underscore while the
-  second ``\verb|_|'' is a placeholder.
-
-  The HOL theories provide further
-  examples for custom serialisations.%
+  second ``\verb|_|'' is a placeholder.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -460,10 +553,44 @@
 \isadelimtt
 %
 \endisadelimtt
+%
+\isamarkupsubsection{Enhancing the target language context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In rare cases it is neccessary 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%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
+\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}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\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
-\isanewline
 %
 \endisadelimtheory
 %