--- 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
--- 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
--- 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}
--- 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}
--- 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%
%
--- 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
--- 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}
--- 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}
--- 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}