1.1 --- a/doc-src/Classes/Thy/document/Classes.tex Wed Apr 01 12:19:15 2009 +0200
1.2 +++ b/doc-src/Classes/Thy/document/Classes.tex Wed Apr 01 15:16:09 2009 +0200
1.3 @@ -1191,7 +1191,7 @@
1.4 \hspace*{0pt}\\
1.5 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
1.6 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
1.7 -\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
1.8 +\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
1.9 \hspace*{0pt}\\
1.10 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
1.11 \hspace*{0pt}pow{\char95}int k x =\\
1.12 @@ -1272,8 +1272,8 @@
1.13 \hspace*{0pt} ~IntInf.int group;\\
1.14 \hspace*{0pt}\\
1.15 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
1.16 -\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
1.17 -\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
1.18 +\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
1.19 +\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
1.20 \hspace*{0pt}\\
1.21 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
1.22 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
2.1 --- a/doc-src/Codegen/Thy/Adaption.thy Wed Apr 01 12:19:15 2009 +0200
2.2 +++ b/doc-src/Codegen/Thy/Adaption.thy Wed Apr 01 15:16:09 2009 +0200
2.3 @@ -59,42 +59,7 @@
2.4 supposed to be:
2.5
2.6 \begin{figure}[here]
2.7 - \begin{tikzpicture}[scale = 0.5]
2.8 - \tikzstyle water=[color = blue, thick]
2.9 - \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
2.10 - \tikzstyle process=[color = green, semithick, ->]
2.11 - \tikzstyle adaption=[color = red, semithick, ->]
2.12 - \tikzstyle target=[color = black]
2.13 - \foreach \x in {0, ..., 24}
2.14 - \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
2.15 - + (0.25, -0.25) cos + (0.25, 0.25);
2.16 - \draw[style=ice] (1, 0) --
2.17 - (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
2.18 - \draw[style=ice] (9, 0) --
2.19 - (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
2.20 - \draw[style=ice] (15, -6) --
2.21 - (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
2.22 - \draw[style=process]
2.23 - (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
2.24 - \draw[style=process]
2.25 - (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
2.26 - \node (adaption) at (11, -2) [style=adaption] {adaption};
2.27 - \node at (19, 3) [rotate=90] {generated};
2.28 - \node at (19.5, -5) {language};
2.29 - \node at (19.5, -3) {library};
2.30 - \node (includes) at (19.5, -1) {includes};
2.31 - \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
2.32 - \draw[style=process]
2.33 - (includes) -- (serialisation);
2.34 - \draw[style=process]
2.35 - (reserved) -- (serialisation);
2.36 - \draw[style=adaption]
2.37 - (adaption) -- (serialisation);
2.38 - \draw[style=adaption]
2.39 - (adaption) -- (includes);
2.40 - \draw[style=adaption]
2.41 - (adaption) -- (reserved);
2.42 - \end{tikzpicture}
2.43 + \includegraphics{Thy/pictures/adaption}
2.44 \caption{The adaption principle}
2.45 \label{fig:adaption}
2.46 \end{figure}
3.1 --- a/doc-src/Codegen/Thy/Introduction.thy Wed Apr 01 12:19:15 2009 +0200
3.2 +++ b/doc-src/Codegen/Thy/Introduction.thy Wed Apr 01 15:16:09 2009 +0200
3.3 @@ -121,29 +121,7 @@
3.4 how it works.
3.5
3.6 \begin{figure}[h]
3.7 - \begin{tikzpicture}[x = 4.2cm, y = 1cm]
3.8 - \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
3.9 - \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
3.10 - \tikzstyle process_arrow=[->, semithick, color = green];
3.11 - \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory};
3.12 - \node (eqn) at (2, 2) [style=entity] {code equations};
3.13 - \node (iml) at (2, 0) [style=entity] {intermediate language};
3.14 - \node (seri) at (1, 0) [style=process] {serialisation};
3.15 - \node (SML) at (0, 3) [style=entity] {@{text SML}};
3.16 - \node (OCaml) at (0, 2) [style=entity] {@{text OCaml}};
3.17 - \node (further) at (0, 1) [style=entity] {@{text "\<dots>"}};
3.18 - \node (Haskell) at (0, 0) [style=entity] {@{text Haskell}};
3.19 - \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
3.20 - node [style=process, near start] {selection}
3.21 - node [style=process, near end] {preprocessing}
3.22 - (eqn);
3.23 - \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
3.24 - \draw [style=process_arrow] (iml) -- (seri);
3.25 - \draw [style=process_arrow] (seri) -- (SML);
3.26 - \draw [style=process_arrow] (seri) -- (OCaml);
3.27 - \draw [style=process_arrow, dashed] (seri) -- (further);
3.28 - \draw [style=process_arrow] (seri) -- (Haskell);
3.29 - \end{tikzpicture}
3.30 + \includegraphics{Thy/pictures/architecture}
3.31 \caption{Code generator architecture}
3.32 \label{fig:arch}
3.33 \end{figure}
3.34 @@ -164,35 +142,29 @@
3.35
3.36 \begin{itemize}
3.37
3.38 - \item Out of the vast collection of theorems proven in a
3.39 - \qn{theory}, a reasonable subset modelling
3.40 - code equations is \qn{selected}.
3.41 + \item Starting point is a collection of raw code equations in a
3.42 + theory; due to proof irrelevance it is not relevant where they
3.43 + stem from but typically they are either descendant of specification
3.44 + tools or explicit proofs by the user.
3.45 +
3.46 + \item Before these raw code equations are continued
3.47 + with, they can be subjected to theorem transformations. This
3.48 + \qn{preprocessor} is an interface which allows to apply the full
3.49 + expressiveness of ML-based theorem transformations to code
3.50 + generation. The result of the preprocessing step is a
3.51 + structured collection of code equations.
3.52
3.53 - \item On those selected theorems, certain
3.54 - transformations are carried out
3.55 - (\qn{preprocessing}). Their purpose is to turn theorems
3.56 - representing non- or badly executable
3.57 - specifications into equivalent but executable counterparts.
3.58 - The result is a structured collection of \qn{code theorems}.
3.59 -
3.60 - \item Before the selected code equations are continued with,
3.61 - they can be \qn{preprocessed}, i.e. subjected to theorem
3.62 - transformations. This \qn{preprocessor} is an interface which
3.63 - allows to apply
3.64 - the full expressiveness of ML-based theorem transformations
3.65 - to code generation; motivating examples are shown below, see
3.66 - \secref{sec:preproc}.
3.67 - The result of the preprocessing step is a structured collection
3.68 - of code equations.
3.69 -
3.70 - \item These code equations are \qn{translated} to a program
3.71 - in an abstract intermediate language. Think of it as a kind
3.72 + \item These code equations are \qn{translated} to a program in an
3.73 + abstract intermediate language. Think of it as a kind
3.74 of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
3.75 (for datatypes), @{text fun} (stemming from code equations),
3.76 also @{text class} and @{text inst} (for type classes).
3.77
3.78 \item Finally, the abstract program is \qn{serialised} into concrete
3.79 source code of a target language.
3.80 + This step only produces concrete syntax but does not change the
3.81 + program in essence; all conceptual transformations occur in the
3.82 + translation step.
3.83
3.84 \end{itemize}
3.85
4.1 --- a/doc-src/Codegen/Thy/document/Adaption.tex Wed Apr 01 12:19:15 2009 +0200
4.2 +++ b/doc-src/Codegen/Thy/document/Adaption.tex Wed Apr 01 15:16:09 2009 +0200
4.3 @@ -96,42 +96,7 @@
4.4 supposed to be:
4.5
4.6 \begin{figure}[here]
4.7 - \begin{tikzpicture}[scale = 0.5]
4.8 - \tikzstyle water=[color = blue, thick]
4.9 - \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
4.10 - \tikzstyle process=[color = green, semithick, ->]
4.11 - \tikzstyle adaption=[color = red, semithick, ->]
4.12 - \tikzstyle target=[color = black]
4.13 - \foreach \x in {0, ..., 24}
4.14 - \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
4.15 - + (0.25, -0.25) cos + (0.25, 0.25);
4.16 - \draw[style=ice] (1, 0) --
4.17 - (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
4.18 - \draw[style=ice] (9, 0) --
4.19 - (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
4.20 - \draw[style=ice] (15, -6) --
4.21 - (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
4.22 - \draw[style=process]
4.23 - (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
4.24 - \draw[style=process]
4.25 - (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
4.26 - \node (adaption) at (11, -2) [style=adaption] {adaption};
4.27 - \node at (19, 3) [rotate=90] {generated};
4.28 - \node at (19.5, -5) {language};
4.29 - \node at (19.5, -3) {library};
4.30 - \node (includes) at (19.5, -1) {includes};
4.31 - \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
4.32 - \draw[style=process]
4.33 - (includes) -- (serialisation);
4.34 - \draw[style=process]
4.35 - (reserved) -- (serialisation);
4.36 - \draw[style=adaption]
4.37 - (adaption) -- (serialisation);
4.38 - \draw[style=adaption]
4.39 - (adaption) -- (includes);
4.40 - \draw[style=adaption]
4.41 - (adaption) -- (reserved);
4.42 - \end{tikzpicture}
4.43 + \includegraphics{Thy/pictures/adaption}
4.44 \caption{The adaption principle}
4.45 \label{fig:adaption}
4.46 \end{figure}
5.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Apr 01 12:19:15 2009 +0200
5.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Apr 01 15:16:09 2009 +0200
5.3 @@ -284,29 +284,7 @@
5.4 how it works.
5.5
5.6 \begin{figure}[h]
5.7 - \begin{tikzpicture}[x = 4.2cm, y = 1cm]
5.8 - \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
5.9 - \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
5.10 - \tikzstyle process_arrow=[->, semithick, color = green];
5.11 - \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory};
5.12 - \node (eqn) at (2, 2) [style=entity] {code equations};
5.13 - \node (iml) at (2, 0) [style=entity] {intermediate language};
5.14 - \node (seri) at (1, 0) [style=process] {serialisation};
5.15 - \node (SML) at (0, 3) [style=entity] {\isa{SML}};
5.16 - \node (OCaml) at (0, 2) [style=entity] {\isa{OCaml}};
5.17 - \node (further) at (0, 1) [style=entity] {\isa{{\isasymdots}}};
5.18 - \node (Haskell) at (0, 0) [style=entity] {\isa{Haskell}};
5.19 - \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
5.20 - node [style=process, near start] {selection}
5.21 - node [style=process, near end] {preprocessing}
5.22 - (eqn);
5.23 - \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
5.24 - \draw [style=process_arrow] (iml) -- (seri);
5.25 - \draw [style=process_arrow] (seri) -- (SML);
5.26 - \draw [style=process_arrow] (seri) -- (OCaml);
5.27 - \draw [style=process_arrow, dashed] (seri) -- (further);
5.28 - \draw [style=process_arrow] (seri) -- (Haskell);
5.29 - \end{tikzpicture}
5.30 + \includegraphics{Thy/pictures/architecture}
5.31 \caption{Code generator architecture}
5.32 \label{fig:arch}
5.33 \end{figure}
5.34 @@ -327,35 +305,29 @@
5.35
5.36 \begin{itemize}
5.37
5.38 - \item Out of the vast collection of theorems proven in a
5.39 - \qn{theory}, a reasonable subset modelling
5.40 - code equations is \qn{selected}.
5.41 + \item Starting point is a collection of raw code equations in a
5.42 + theory; due to proof irrelevance it is not relevant where they
5.43 + stem from but typically they are either descendant of specification
5.44 + tools or explicit proofs by the user.
5.45 +
5.46 + \item Before these raw code equations are continued
5.47 + with, they can be subjected to theorem transformations. This
5.48 + \qn{preprocessor} is an interface which allows to apply the full
5.49 + expressiveness of ML-based theorem transformations to code
5.50 + generation. The result of the preprocessing step is a
5.51 + structured collection of code equations.
5.52
5.53 - \item On those selected theorems, certain
5.54 - transformations are carried out
5.55 - (\qn{preprocessing}). Their purpose is to turn theorems
5.56 - representing non- or badly executable
5.57 - specifications into equivalent but executable counterparts.
5.58 - The result is a structured collection of \qn{code theorems}.
5.59 -
5.60 - \item Before the selected code equations are continued with,
5.61 - they can be \qn{preprocessed}, i.e. subjected to theorem
5.62 - transformations. This \qn{preprocessor} is an interface which
5.63 - allows to apply
5.64 - the full expressiveness of ML-based theorem transformations
5.65 - to code generation; motivating examples are shown below, see
5.66 - \secref{sec:preproc}.
5.67 - The result of the preprocessing step is a structured collection
5.68 - of code equations.
5.69 -
5.70 - \item These code equations are \qn{translated} to a program
5.71 - in an abstract intermediate language. Think of it as a kind
5.72 + \item These code equations are \qn{translated} to a program in an
5.73 + abstract intermediate language. Think of it as a kind
5.74 of \qt{Mini-Haskell} with four \qn{statements}: \isa{data}
5.75 (for datatypes), \isa{fun} (stemming from code equations),
5.76 also \isa{class} and \isa{inst} (for type classes).
5.77
5.78 \item Finally, the abstract program is \qn{serialised} into concrete
5.79 source code of a target language.
5.80 + This step only produces concrete syntax but does not change the
5.81 + program in essence; all conceptual transformations occur in the
5.82 + translation step.
5.83
5.84 \end{itemize}
5.85
6.1 --- a/doc-src/Codegen/Thy/pictures/adaption.tex Wed Apr 01 12:19:15 2009 +0200
6.2 +++ b/doc-src/Codegen/Thy/pictures/adaption.tex Wed Apr 01 15:16:09 2009 +0200
6.3 @@ -1,7 +1,5 @@
6.4
6.5 \documentclass[12pt]{article}
6.6 -\usepackage{pgf}
6.7 -\usepackage{pgflibraryshapes}
6.8 \usepackage{tikz}
6.9
6.10 \begin{document}
6.11 @@ -10,7 +8,7 @@
6.12 \setlength{\fboxrule}{0.01pt}
6.13 \setlength{\fboxsep}{4pt}
6.14
6.15 -\fbox{
6.16 +\fcolorbox{white}{white}{
6.17
6.18 \begin{tikzpicture}[scale = 0.5]
6.19 \tikzstyle water=[color = blue, thick]
7.1 --- a/doc-src/Codegen/Thy/pictures/architecture.tex Wed Apr 01 12:19:15 2009 +0200
7.2 +++ b/doc-src/Codegen/Thy/pictures/architecture.tex Wed Apr 01 15:16:09 2009 +0200
7.3 @@ -1,8 +1,8 @@
7.4
7.5 \documentclass[12pt]{article}
7.6 -\usepackage{pgf}
7.7 -\usepackage{pgflibraryshapes}
7.8 \usepackage{tikz}
7.9 +\usetikzlibrary{shapes}
7.10 +\usetikzlibrary{arrows}
7.11
7.12 \begin{document}
7.13
7.14 @@ -10,30 +10,39 @@
7.15 \setlength{\fboxrule}{0.01pt}
7.16 \setlength{\fboxsep}{4pt}
7.17
7.18 -\fbox{
7.19 +\fcolorbox{white}{white}{
7.20
7.21 -\begin{tikzpicture}[x = 4.2cm, y = 1cm]
7.22 - \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
7.23 - \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
7.24 - \tikzstyle process_arrow=[->, semithick, color = green];
7.25 - \node (HOL) at (0, 4) [style=entity] {Isabelle/HOL theory};
7.26 - \node (eqn) at (2, 2) [style=entity] {code equations};
7.27 - \node (iml) at (2, 0) [style=entity] {intermediate language};
7.28 - \node (seri) at (1, 0) [style=process] {serialisation};
7.29 - \node (SML) at (0, 3) [style=entity] {SML};
7.30 - \node (OCaml) at (0, 2) [style=entity] {OCaml};
7.31 - \node (further) at (0, 1) [style=entity] {\ldots};
7.32 - \node (Haskell) at (0, 0) [style=entity] {Haskell};
7.33 - \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
7.34 - node [style=process, near start] {selection}
7.35 - node [style=process, near end] {preprocessing}
7.36 - (eqn);
7.37 - \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
7.38 - \draw [style=process_arrow] (iml) -- (seri);
7.39 - \draw [style=process_arrow] (seri) -- (SML);
7.40 - \draw [style=process_arrow] (seri) -- (OCaml);
7.41 - \draw [style=process_arrow, dashed] (seri) -- (further);
7.42 - \draw [style=process_arrow] (seri) -- (Haskell);
7.43 +\newcommand{\sys}[1]{\emph{#1}}
7.44 +
7.45 +\begin{tikzpicture}[x = 4cm, y = 1cm]
7.46 + \tikzstyle positive=[color = black, fill = white];
7.47 + \tikzstyle negative=[color = white, fill = black];
7.48 + \tikzstyle entity=[rounded corners, draw, thick];
7.49 + \tikzstyle process=[ellipse, draw, thick];
7.50 + \tikzstyle arrow=[-stealth, semithick];
7.51 + \node (spec) at (0, 3) [entity, positive] {specification tools};
7.52 + \node (user) at (1, 3) [entity, positive] {user proofs};
7.53 + \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
7.54 + \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
7.55 + \node (pre) at (1.5, 4) [process, positive] {preprocessing};
7.56 + \node (eqn) at (2.5, 4) [entity, positive] {code equations};
7.57 + \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
7.58 + \node (seri) at (1.5, 0) [process, positive] {serialisation};
7.59 + \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
7.60 + \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
7.61 + \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
7.62 + \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
7.63 + \draw [semithick] (spec) -- (spec_user_join);
7.64 + \draw [semithick] (user) -- (spec_user_join);
7.65 + \draw [-diamond, semithick] (spec_user_join) -- (raw);
7.66 + \draw [arrow] (raw) -- (pre);
7.67 + \draw [arrow] (pre) -- (eqn);
7.68 + \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
7.69 + \draw [arrow] (iml) -- (seri);
7.70 + \draw [arrow] (seri) -- (SML);
7.71 + \draw [arrow] (seri) -- (OCaml);
7.72 + \draw [arrow, dashed] (seri) -- (further);
7.73 + \draw [arrow] (seri) -- (Haskell);
7.74 \end{tikzpicture}
7.75
7.76 }
8.1 --- a/doc-src/Codegen/codegen.tex Wed Apr 01 12:19:15 2009 +0200
8.2 +++ b/doc-src/Codegen/codegen.tex Wed Apr 01 15:16:09 2009 +0200
8.3 @@ -5,9 +5,6 @@
8.4 \usepackage{../iman,../extra,../isar,../proof}
8.5 \usepackage{../isabelle,../isabellesym}
8.6 \usepackage{style}
8.7 -\usepackage{pgf}
8.8 -\usepackage{pgflibraryshapes}
8.9 -\usepackage{tikz}
8.10 \usepackage{../pdfsetup}
8.11
8.12 \hyphenation{Isabelle}