--- a/doc-src/Classes/Thy/document/Classes.tex Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed Apr 01 15:16:09 2009 +0200
@@ -1191,7 +1191,7 @@
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
+\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
\hspace*{0pt}pow{\char95}int k x =\\
@@ -1272,8 +1272,8 @@
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
-\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
-\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
+\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
+\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
--- a/doc-src/Codegen/Thy/Adaption.thy Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaption.thy Wed Apr 01 15:16:09 2009 +0200
@@ -59,42 +59,7 @@
supposed to be:
\begin{figure}[here]
- \begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaption=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaption) at (11, -2) [style=adaption] {adaption};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (includes);
- \draw[style=adaption]
- (adaption) -- (reserved);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/adaption}
\caption{The adaption principle}
\label{fig:adaption}
\end{figure}
--- a/doc-src/Codegen/Thy/Introduction.thy Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed Apr 01 15:16:09 2009 +0200
@@ -121,29 +121,7 @@
how it works.
\begin{figure}[h]
- \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] {code 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}
+ \includegraphics{Thy/pictures/architecture}
\caption{Code generator architecture}
\label{fig:arch}
\end{figure}
@@ -164,35 +142,29 @@
\begin{itemize}
- \item Out of the vast collection of theorems proven in a
- \qn{theory}, a reasonable subset modelling
- code equations is \qn{selected}.
-
- \item On those selected theorems, certain
- transformations are carried out
- (\qn{preprocessing}). Their purpose is to turn theorems
- representing non- or badly executable
- specifications into equivalent but executable counterparts.
- The result is a structured collection of \qn{code theorems}.
+ \item Starting point is a collection of raw code equations in a
+ theory; due to proof irrelevance it is not relevant where they
+ stem from but typically they are either descendant of specification
+ tools or explicit proofs by the user.
+
+ \item Before these raw code equations are continued
+ with, they can be subjected to theorem transformations. This
+ \qn{preprocessor} is an interface which allows to apply the full
+ expressiveness of ML-based theorem transformations to code
+ generation. The result of the preprocessing step is a
+ structured collection of code equations.
- \item Before the selected code equations are continued with,
- they can be \qn{preprocessed}, i.e. subjected to theorem
- transformations. This \qn{preprocessor} is an interface which
- allows to apply
- the full expressiveness of ML-based theorem transformations
- to code generation; motivating examples are shown below, see
- \secref{sec:preproc}.
- The result of the preprocessing step is a structured collection
- of code equations.
-
- \item These code equations are \qn{translated} to a program
- in an abstract intermediate language. Think of it as a kind
+ \item These code equations are \qn{translated} to a program in an
+ abstract intermediate language. Think of it as a kind
of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
(for datatypes), @{text fun} (stemming from code equations),
also @{text class} and @{text inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into concrete
source code of a target language.
+ This step only produces concrete syntax but does not change the
+ program in essence; all conceptual transformations occur in the
+ translation step.
\end{itemize}
--- a/doc-src/Codegen/Thy/document/Adaption.tex Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaption.tex Wed Apr 01 15:16:09 2009 +0200
@@ -96,42 +96,7 @@
supposed to be:
\begin{figure}[here]
- \begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaption=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaption) at (11, -2) [style=adaption] {adaption};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (includes);
- \draw[style=adaption]
- (adaption) -- (reserved);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/adaption}
\caption{The adaption principle}
\label{fig:adaption}
\end{figure}
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Apr 01 15:16:09 2009 +0200
@@ -284,29 +284,7 @@
how it works.
\begin{figure}[h]
- \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] {code 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{{\isasymdots}}};
- \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}
+ \includegraphics{Thy/pictures/architecture}
\caption{Code generator architecture}
\label{fig:arch}
\end{figure}
@@ -327,35 +305,29 @@
\begin{itemize}
- \item Out of the vast collection of theorems proven in a
- \qn{theory}, a reasonable subset modelling
- code equations is \qn{selected}.
-
- \item On those selected theorems, certain
- transformations are carried out
- (\qn{preprocessing}). Their purpose is to turn theorems
- representing non- or badly executable
- specifications into equivalent but executable counterparts.
- The result is a structured collection of \qn{code theorems}.
+ \item Starting point is a collection of raw code equations in a
+ theory; due to proof irrelevance it is not relevant where they
+ stem from but typically they are either descendant of specification
+ tools or explicit proofs by the user.
+
+ \item Before these raw code equations are continued
+ with, they can be subjected to theorem transformations. This
+ \qn{preprocessor} is an interface which allows to apply the full
+ expressiveness of ML-based theorem transformations to code
+ generation. The result of the preprocessing step is a
+ structured collection of code equations.
- \item Before the selected code equations are continued with,
- they can be \qn{preprocessed}, i.e. subjected to theorem
- transformations. This \qn{preprocessor} is an interface which
- allows to apply
- the full expressiveness of ML-based theorem transformations
- to code generation; motivating examples are shown below, see
- \secref{sec:preproc}.
- The result of the preprocessing step is a structured collection
- of code equations.
-
- \item These code equations are \qn{translated} to a program
- in an abstract intermediate language. Think of it as a kind
+ \item These code equations are \qn{translated} to a program in an
+ abstract intermediate language. Think of it as a kind
of \qt{Mini-Haskell} with four \qn{statements}: \isa{data}
(for datatypes), \isa{fun} (stemming from code equations),
also \isa{class} and \isa{inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into concrete
source code of a target language.
+ This step only produces concrete syntax but does not change the
+ program in essence; all conceptual transformations occur in the
+ translation step.
\end{itemize}
--- a/doc-src/Codegen/Thy/pictures/adaption.tex Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex Wed Apr 01 15:16:09 2009 +0200
@@ -1,7 +1,5 @@
\documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
\usepackage{tikz}
\begin{document}
@@ -10,7 +8,7 @@
\setlength{\fboxrule}{0.01pt}
\setlength{\fboxsep}{4pt}
-\fbox{
+\fcolorbox{white}{white}{
\begin{tikzpicture}[scale = 0.5]
\tikzstyle water=[color = blue, thick]
--- a/doc-src/Codegen/Thy/pictures/architecture.tex Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex Wed Apr 01 15:16:09 2009 +0200
@@ -1,8 +1,8 @@
\documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
\usepackage{tikz}
+\usetikzlibrary{shapes}
+\usetikzlibrary{arrows}
\begin{document}
@@ -10,30 +10,39 @@
\setlength{\fboxrule}{0.01pt}
\setlength{\fboxsep}{4pt}
-\fbox{
+\fcolorbox{white}{white}{
+
+\newcommand{\sys}[1]{\emph{#1}}
-\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] {Isabelle/HOL theory};
- \node (eqn) at (2, 2) [style=entity] {code 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] {SML};
- \node (OCaml) at (0, 2) [style=entity] {OCaml};
- \node (further) at (0, 1) [style=entity] {\ldots};
- \node (Haskell) at (0, 0) [style=entity] {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);
+\begin{tikzpicture}[x = 4cm, y = 1cm]
+ \tikzstyle positive=[color = black, fill = white];
+ \tikzstyle negative=[color = white, fill = black];
+ \tikzstyle entity=[rounded corners, draw, thick];
+ \tikzstyle process=[ellipse, draw, thick];
+ \tikzstyle arrow=[-stealth, semithick];
+ \node (spec) at (0, 3) [entity, positive] {specification tools};
+ \node (user) at (1, 3) [entity, positive] {user proofs};
+ \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
+ \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
+ \node (pre) at (1.5, 4) [process, positive] {preprocessing};
+ \node (eqn) at (2.5, 4) [entity, positive] {code equations};
+ \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
+ \node (seri) at (1.5, 0) [process, positive] {serialisation};
+ \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
+ \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
+ \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
+ \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
+ \draw [semithick] (spec) -- (spec_user_join);
+ \draw [semithick] (user) -- (spec_user_join);
+ \draw [-diamond, semithick] (spec_user_join) -- (raw);
+ \draw [arrow] (raw) -- (pre);
+ \draw [arrow] (pre) -- (eqn);
+ \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
+ \draw [arrow] (iml) -- (seri);
+ \draw [arrow] (seri) -- (SML);
+ \draw [arrow] (seri) -- (OCaml);
+ \draw [arrow, dashed] (seri) -- (further);
+ \draw [arrow] (seri) -- (Haskell);
\end{tikzpicture}
}
--- a/doc-src/Codegen/codegen.tex Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/codegen.tex Wed Apr 01 15:16:09 2009 +0200
@@ -5,9 +5,6 @@
\usepackage{../iman,../extra,../isar,../proof}
\usepackage{../isabelle,../isabellesym}
\usepackage{style}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
-\usepackage{tikz}
\usepackage{../pdfsetup}
\hyphenation{Isabelle}