filled remaining gaps
authorhaftmann
Fri Oct 17 10:14:38 2008 +0200 (2008-10-17)
changeset 28635cc53d2ab0170
parent 28634 764ef122a164
child 28636 d5342d4c7360
filled remaining gaps
doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
doc-src/IsarAdvanced/Codegen/Thy/Further.thy
doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy
doc-src/IsarAdvanced/Codegen/Thy/ML.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex
doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex
doc-src/IsarAdvanced/Codegen/codegen.tex
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 17 10:14:12 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 17 10:14:38 2008 +0200
     1.3 @@ -109,13 +109,30 @@
     1.4    by the serializer is just the tip of the iceberg:
     1.5  
     1.6    \begin{itemize}
     1.7 -    \item parametrise @{text serialisation}
     1.8 -    \item @{text library} @{text reserved}
     1.9 -    \item @{text "includes"} @{text reserved}
    1.10 +    \item @{text serialisation} can be \emph{parametrised} such that
    1.11 +      logical entities are mapped to target-specific ones
    1.12 +      (e.g. target-specific list syntax,
    1.13 +        see also \secref{sec:adaption_mechanisms})
    1.14 +    \item Such parametrisations can involve references to a
    1.15 +      target-specific standard @{text library} (e.g. using
    1.16 +      the @{text Haskell} @{verbatim Maybe} type instead
    1.17 +      of the @{text HOL} @{type "option"} type);
    1.18 +      if such are used, the corresponding identifiers
    1.19 +      (in our example, @{verbatim Maybe}, @{verbatim Nothing}
    1.20 +      and @{verbatim Just}) also have to be considered @{text reserved}.
    1.21 +    \item Even more, the user can enrich the library of the
    1.22 +      target-language by providing code snippets
    1.23 +      (\qt{@{text "includes"}}) which are prepended to
    1.24 +      any generated code (see \secref{sec:include});  this typically
    1.25 +      also involves further @{text reserved} identifiers.
    1.26    \end{itemize}
    1.27 +
    1.28 +  \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
    1.29 +  have to act consistently;  it is at the discretion of the user
    1.30 +  to take care for this.
    1.31  *}
    1.32  
    1.33 -subsection {* Common adaption cases *}
    1.34 +subsection {* Common adaption patterns *}
    1.35  
    1.36  text {*
    1.37    The @{theory HOL} @{theory Main} theory already provides a code
    1.38 @@ -160,7 +177,7 @@
    1.39  *}
    1.40  
    1.41  
    1.42 -subsection {* Adaption mechanisms \label{sec:adaption_mechanisms} *}
    1.43 +subsection {* Parametrising serialisation \label{sec:adaption_mechanisms} *}
    1.44  
    1.45  text {*
    1.46    Consider the following function and its corresponding
    1.47 @@ -322,7 +339,7 @@
    1.48    (Haskell -)
    1.49  
    1.50  
    1.51 -subsection {* Enhancing the target language context *}
    1.52 +subsection {* Enhancing the target language context \label{sec:include} *}
    1.53  
    1.54  text {*
    1.55    In rare cases it is necessary to \emph{enrich} the context of a
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Further.thy	Fri Oct 17 10:14:12 2008 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy	Fri Oct 17 10:14:38 2008 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4    When invoking the @{command export_code} command it is possible to leave
     2.5    out the @{keyword "module_name"} part;  then code is distributed over
     2.6    different modules, where the module name space roughly is induced
     2.7 -  by the @{text Isabelle} theory namespace.
     2.8 +  by the @{text Isabelle} theory name space.
     2.9  
    2.10    Then sometimes the awkward situation occurs that dependencies between
    2.11    definitions introduce cyclic dependencies between modules, which in the
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Fri Oct 17 10:14:12 2008 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Fri Oct 17 10:14:38 2008 +0200
     3.3 @@ -123,8 +123,29 @@
     3.4    how it works.
     3.5  
     3.6    \begin{figure}[h]
     3.7 -    \centering
     3.8 -    \includegraphics[width=0.7\textwidth]{codegen_process}
     3.9 +    \begin{tikzpicture}[x = 4.2cm, y = 1cm]
    3.10 +      \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
    3.11 +      \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
    3.12 +      \tikzstyle process_arrow=[->, semithick, color = green];
    3.13 +      \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory};
    3.14 +      \node (eqn) at (2, 2) [style=entity] {defining equations};
    3.15 +      \node (iml) at (2, 0) [style=entity] {intermediate language};
    3.16 +      \node (seri) at (1, 0) [style=process] {serialisation};
    3.17 +      \node (SML) at (0, 3) [style=entity] {@{text SML}};
    3.18 +      \node (OCaml) at (0, 2) [style=entity] {@{text OCaml}};
    3.19 +      \node (further) at (0, 1) [style=entity] {@{text "\<dots>"}};
    3.20 +      \node (Haskell) at (0, 0) [style=entity] {@{text Haskell}};
    3.21 +      \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
    3.22 +        node [style=process, near start] {selection}
    3.23 +        node [style=process, near end] {preprocessing}
    3.24 +        (eqn);
    3.25 +      \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
    3.26 +      \draw [style=process_arrow] (iml) -- (seri);
    3.27 +      \draw [style=process_arrow] (seri) -- (SML);
    3.28 +      \draw [style=process_arrow] (seri) -- (OCaml);
    3.29 +      \draw [style=process_arrow, dashed] (seri) -- (further);
    3.30 +      \draw [style=process_arrow] (seri) -- (Haskell);
    3.31 +    \end{tikzpicture}
    3.32      \caption{Code generator architecture}
    3.33      \label{fig:arch}
    3.34    \end{figure}
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Fri Oct 17 10:14:12 2008 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Fri Oct 17 10:14:38 2008 +0200
     4.3 @@ -128,7 +128,7 @@
     4.4    \begin{tabular}{l}
     4.5    @{text "type T"} \\
     4.6    @{text "val empty: T"} \\
     4.7 -  @{text "val purge: theory \<rightarrow> CodeUnit.const list option \<rightarrow> T \<rightarrow> T"}
     4.8 +  @{text "val purge: theory \<rightarrow> string list option \<rightarrow> T \<rightarrow> T"}
     4.9    \end{tabular}
    4.10  
    4.11    \begin{description}
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 17 10:14:12 2008 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 17 10:14:38 2008 +0200
     5.3 @@ -146,14 +146,31 @@
     5.4    by the serializer is just the tip of the iceberg:
     5.5  
     5.6    \begin{itemize}
     5.7 -    \item parametrise \isa{serialisation}
     5.8 -    \item \isa{library} \isa{reserved}
     5.9 -    \item \isa{includes} \isa{reserved}
    5.10 -  \end{itemize}%
    5.11 +    \item \isa{serialisation} can be \emph{parametrised} such that
    5.12 +      logical entities are mapped to target-specific ones
    5.13 +      (e.g. target-specific list syntax,
    5.14 +        see also \secref{sec:adaption_mechanisms})
    5.15 +    \item Such parametrisations can involve references to a
    5.16 +      target-specific standard \isa{library} (e.g. using
    5.17 +      the \isa{Haskell} \verb|Maybe| type instead
    5.18 +      of the \isa{HOL} \isa{option} type);
    5.19 +      if such are used, the corresponding identifiers
    5.20 +      (in our example, \verb|Maybe|, \verb|Nothing|
    5.21 +      and \verb|Just|) also have to be considered \isa{reserved}.
    5.22 +    \item Even more, the user can enrich the library of the
    5.23 +      target-language by providing code snippets
    5.24 +      (\qt{\isa{includes}}) which are prepended to
    5.25 +      any generated code (see \secref{sec:include});  this typically
    5.26 +      also involves further \isa{reserved} identifiers.
    5.27 +  \end{itemize}
    5.28 +
    5.29 +  \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
    5.30 +  have to act consistently;  it is at the discretion of the user
    5.31 +  to take care for this.%
    5.32  \end{isamarkuptext}%
    5.33  \isamarkuptrue%
    5.34  %
    5.35 -\isamarkupsubsection{Common adaption cases%
    5.36 +\isamarkupsubsection{Common adaption patterns%
    5.37  }
    5.38  \isamarkuptrue%
    5.39  %
    5.40 @@ -200,7 +217,7 @@
    5.41  \end{isamarkuptext}%
    5.42  \isamarkuptrue%
    5.43  %
    5.44 -\isamarkupsubsection{Adaption mechanisms \label{sec:adaption_mechanisms}%
    5.45 +\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%
    5.46  }
    5.47  \isamarkuptrue%
    5.48  %
    5.49 @@ -605,7 +622,7 @@
    5.50  %
    5.51  \endisadelimquotett
    5.52  %
    5.53 -\isamarkupsubsection{Enhancing the target language context%
    5.54 +\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
    5.55  }
    5.56  \isamarkuptrue%
    5.57  %
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex	Fri Oct 17 10:14:12 2008 +0200
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex	Fri Oct 17 10:14:38 2008 +0200
     6.3 @@ -41,7 +41,7 @@
     6.4  When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave
     6.5    out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part;  then code is distributed over
     6.6    different modules, where the module name space roughly is induced
     6.7 -  by the \isa{Isabelle} theory namespace.
     6.8 +  by the \isa{Isabelle} theory name space.
     6.9  
    6.10    Then sometimes the awkward situation occurs that dependencies between
    6.11    definitions introduce cyclic dependencies between modules, which in the
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 17 10:14:12 2008 +0200
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 17 10:14:38 2008 +0200
     7.3 @@ -288,8 +288,29 @@
     7.4    how it works.
     7.5  
     7.6    \begin{figure}[h]
     7.7 -    \centering
     7.8 -    \includegraphics[width=0.7\textwidth]{codegen_process}
     7.9 +    \begin{tikzpicture}[x = 4.2cm, y = 1cm]
    7.10 +      \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
    7.11 +      \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
    7.12 +      \tikzstyle process_arrow=[->, semithick, color = green];
    7.13 +      \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory};
    7.14 +      \node (eqn) at (2, 2) [style=entity] {defining equations};
    7.15 +      \node (iml) at (2, 0) [style=entity] {intermediate language};
    7.16 +      \node (seri) at (1, 0) [style=process] {serialisation};
    7.17 +      \node (SML) at (0, 3) [style=entity] {\isa{SML}};
    7.18 +      \node (OCaml) at (0, 2) [style=entity] {\isa{OCaml}};
    7.19 +      \node (further) at (0, 1) [style=entity] {\isa{{\isacharquery}}};
    7.20 +      \node (Haskell) at (0, 0) [style=entity] {\isa{Haskell}};
    7.21 +      \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
    7.22 +        node [style=process, near start] {selection}
    7.23 +        node [style=process, near end] {preprocessing}
    7.24 +        (eqn);
    7.25 +      \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
    7.26 +      \draw [style=process_arrow] (iml) -- (seri);
    7.27 +      \draw [style=process_arrow] (seri) -- (SML);
    7.28 +      \draw [style=process_arrow] (seri) -- (OCaml);
    7.29 +      \draw [style=process_arrow, dashed] (seri) -- (further);
    7.30 +      \draw [style=process_arrow] (seri) -- (Haskell);
    7.31 +    \end{tikzpicture}
    7.32      \caption{Code generator architecture}
    7.33      \label{fig:arch}
    7.34    \end{figure}
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Fri Oct 17 10:14:12 2008 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Fri Oct 17 10:14:38 2008 +0200
     8.3 @@ -186,7 +186,7 @@
     8.4    \begin{tabular}{l}
     8.5    \isa{type\ T} \\
     8.6    \isa{val\ empty{\isacharcolon}\ T} \\
     8.7 -  \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
     8.8 +  \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
     8.9    \end{tabular}
    8.10  
    8.11    \begin{description}
     9.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Oct 17 10:14:12 2008 +0200
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Oct 17 10:14:38 2008 +0200
     9.3 @@ -7,6 +7,8 @@
     9.4  \usepackage{../../iman,../../extra,../../isar,../../proof}
     9.5  \usepackage{../../isabelle,../../isabellesym}
     9.6  \usepackage{style}
     9.7 +\usepackage{pgf}
     9.8 +\usepackage{pgflibraryshapes}
     9.9  \usepackage{tikz}
    9.10  \usepackage{../../pdfsetup}
    9.11