# HG changeset patch
# User haftmann
# Date 1224231278 -7200
# Node ID cc53d2ab01704b11b792c5547351c041ef424c25
# Parent  764ef122a164da07ae65a6bdfe43b2087afd9169
filled remaining gaps

diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 17 10:14:38 2008 +0200
@@ -109,13 +109,30 @@
   by the serializer is just the tip of the iceberg:
 
   \begin{itemize}
-    \item parametrise @{text serialisation}
-    \item @{text library} @{text reserved}
-    \item @{text "includes"} @{text reserved}
+    \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 cases *}
+subsection {* Common adaption patterns *}
 
 text {*
   The @{theory HOL} @{theory Main} theory already provides a code
@@ -160,7 +177,7 @@
 *}
 
 
-subsection {* Adaption mechanisms \label{sec:adaption_mechanisms} *}
+subsection {* Parametrising serialisation \label{sec:adaption_mechanisms} *}
 
 text {*
   Consider the following function and its corresponding
@@ -322,7 +339,7 @@
   (Haskell -)
 
 
-subsection {* Enhancing the target language context *}
+subsection {* Enhancing the target language context \label{sec:include} *}
 
 text {*
   In rare cases it is necessary to \emph{enrich} the context of a
diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/Thy/Further.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Further.thy	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy	Fri Oct 17 10:14:38 2008 +0200
@@ -18,7 +18,7 @@
   When invoking the @{command export_code} command it is possible to leave
   out the @{keyword "module_name"} part;  then code is distributed over
   different modules, where the module name space roughly is induced
-  by the @{text Isabelle} theory namespace.
+  by the @{text Isabelle} theory name space.
 
   Then sometimes the awkward situation occurs that dependencies between
   definitions introduce cyclic dependencies between modules, which in the
diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Fri Oct 17 10:14:38 2008 +0200
@@ -123,8 +123,29 @@
   how it works.
 
   \begin{figure}[h]
-    \centering
-    \includegraphics[width=0.7\textwidth]{codegen_process}
+    \begin{tikzpicture}[x = 4.2cm, y = 1cm]
+      \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
+      \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
+      \tikzstyle process_arrow=[->, semithick, color = green];
+      \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory};
+      \node (eqn) at (2, 2) [style=entity] {defining equations};
+      \node (iml) at (2, 0) [style=entity] {intermediate language};
+      \node (seri) at (1, 0) [style=process] {serialisation};
+      \node (SML) at (0, 3) [style=entity] {@{text SML}};
+      \node (OCaml) at (0, 2) [style=entity] {@{text OCaml}};
+      \node (further) at (0, 1) [style=entity] {@{text "\<dots>"}};
+      \node (Haskell) at (0, 0) [style=entity] {@{text Haskell}};
+      \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
+        node [style=process, near start] {selection}
+        node [style=process, near end] {preprocessing}
+        (eqn);
+      \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
+      \draw [style=process_arrow] (iml) -- (seri);
+      \draw [style=process_arrow] (seri) -- (SML);
+      \draw [style=process_arrow] (seri) -- (OCaml);
+      \draw [style=process_arrow, dashed] (seri) -- (further);
+      \draw [style=process_arrow] (seri) -- (Haskell);
+    \end{tikzpicture}
     \caption{Code generator architecture}
     \label{fig:arch}
   \end{figure}
diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/Thy/ML.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Fri Oct 17 10:14:38 2008 +0200
@@ -128,7 +128,7 @@
   \begin{tabular}{l}
   @{text "type T"} \\
   @{text "val empty: T"} \\
-  @{text "val purge: theory \<rightarrow> CodeUnit.const list option \<rightarrow> T \<rightarrow> T"}
+  @{text "val purge: theory \<rightarrow> string list option \<rightarrow> T \<rightarrow> T"}
   \end{tabular}
 
   \begin{description}
diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 17 10:14:38 2008 +0200
@@ -146,14 +146,31 @@
   by the serializer is just the tip of the iceberg:
 
   \begin{itemize}
-    \item parametrise \isa{serialisation}
-    \item \isa{library} \isa{reserved}
-    \item \isa{includes} \isa{reserved}
-  \end{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 cases%
+\isamarkupsubsection{Common adaption patterns%
 }
 \isamarkuptrue%
 %
@@ -200,7 +217,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Adaption mechanisms \label{sec:adaption_mechanisms}%
+\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%
 }
 \isamarkuptrue%
 %
@@ -605,7 +622,7 @@
 %
 \endisadelimquotett
 %
-\isamarkupsubsection{Enhancing the target language context%
+\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
 }
 \isamarkuptrue%
 %
diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex	Fri Oct 17 10:14:38 2008 +0200
@@ -41,7 +41,7 @@
 When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave
   out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part;  then code is distributed over
   different modules, where the module name space roughly is induced
-  by the \isa{Isabelle} theory namespace.
+  by the \isa{Isabelle} theory name space.
 
   Then sometimes the awkward situation occurs that dependencies between
   definitions introduce cyclic dependencies between modules, which in the
diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 17 10:14:38 2008 +0200
@@ -288,8 +288,29 @@
   how it works.
 
   \begin{figure}[h]
-    \centering
-    \includegraphics[width=0.7\textwidth]{codegen_process}
+    \begin{tikzpicture}[x = 4.2cm, y = 1cm]
+      \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
+      \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
+      \tikzstyle process_arrow=[->, semithick, color = green];
+      \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory};
+      \node (eqn) at (2, 2) [style=entity] {defining equations};
+      \node (iml) at (2, 0) [style=entity] {intermediate language};
+      \node (seri) at (1, 0) [style=process] {serialisation};
+      \node (SML) at (0, 3) [style=entity] {\isa{SML}};
+      \node (OCaml) at (0, 2) [style=entity] {\isa{OCaml}};
+      \node (further) at (0, 1) [style=entity] {\isa{{\isacharquery}}};
+      \node (Haskell) at (0, 0) [style=entity] {\isa{Haskell}};
+      \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
+        node [style=process, near start] {selection}
+        node [style=process, near end] {preprocessing}
+        (eqn);
+      \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
+      \draw [style=process_arrow] (iml) -- (seri);
+      \draw [style=process_arrow] (seri) -- (SML);
+      \draw [style=process_arrow] (seri) -- (OCaml);
+      \draw [style=process_arrow, dashed] (seri) -- (further);
+      \draw [style=process_arrow] (seri) -- (Haskell);
+    \end{tikzpicture}
     \caption{Code generator architecture}
     \label{fig:arch}
   \end{figure}
diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Fri Oct 17 10:14:38 2008 +0200
@@ -186,7 +186,7 @@
   \begin{tabular}{l}
   \isa{type\ T} \\
   \isa{val\ empty{\isacharcolon}\ T} \\
-  \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
+  \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
   \end{tabular}
 
   \begin{description}
diff -r 764ef122a164 -r cc53d2ab0170 doc-src/IsarAdvanced/Codegen/codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Oct 17 10:14:12 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Oct 17 10:14:38 2008 +0200
@@ -7,6 +7,8 @@
 \usepackage{../../iman,../../extra,../../isar,../../proof}
 \usepackage{../../isabelle,../../isabellesym}
 \usepackage{style}
+\usepackage{pgf}
+\usepackage{pgflibraryshapes}
 \usepackage{tikz}
 \usepackage{../../pdfsetup}