# HG changeset patch
# User haftmann
# Date 1276522029 -7200
# Node ID b3d94253e7f27d1fd8094266dd1bf4c4974593b9
# Parent  e482f206821e17c575ebde4708fb62ce56f06d1a
updated generated code

diff -r e482f206821e -r b3d94253e7f2 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Mon Jun 14 15:27:09 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Mon Jun 14 15:27:09 2010 +0200
@@ -234,13 +234,6 @@
 \noindent%
 \hspace*{0pt}module Example where {\char123}\\
 \hspace*{0pt}\\
-\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\
-\hspace*{0pt}foldla f a [] = a;\\
-\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
-\hspace*{0pt}\\
-\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\
-\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
-\hspace*{0pt}\\
 \hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\
 \hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
 \hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
diff -r e482f206821e -r b3d94253e7f2 doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Mon Jun 14 15:27:09 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex	Mon Jun 14 15:27:09 2010 +0200
@@ -323,7 +323,8 @@
 %
 \begin{isamarkuptext}%
 \noindent This is a convenient place to show how explicit dictionary construction
-  manifests in generated code (here, the same example in \isa{SML}):%
+  manifests in generated code (here, the same example in \isa{SML})
+  \cite{Haftmann-Nipkow:2010:code}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -341,7 +342,7 @@
 \hspace*{0pt} ~type 'a semigroup\\
 \hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
 \hspace*{0pt} ~type 'a monoid\\
-\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
+\hspace*{0pt} ~val monoid{\char95}semigroup :~'a monoid -> 'a semigroup\\
 \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
 \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
 \hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
@@ -357,12 +358,12 @@
 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
 \hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
 \hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
+\hspace*{0pt}type 'a monoid = {\char123}monoid{\char95}semigroup :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}val monoid{\char95}semigroup = {\char35}monoid{\char95}semigroup :~'a monoid -> 'a semigroup;\\
 \hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
-\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
+\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (monoid{\char95}semigroup A{\char95}) a (pow A{\char95}~n a);\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
@@ -374,7 +375,7 @@
 \hspace*{0pt}\\
 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
 \hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
+\hspace*{0pt}val monoid{\char95}nat = {\char123}monoid{\char95}semigroup = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
 \hspace*{0pt} ~:~nat monoid;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
diff -r e482f206821e -r b3d94253e7f2 doc-src/Codegen/Thy/examples/Example.hs
--- a/doc-src/Codegen/Thy/examples/Example.hs	Mon Jun 14 15:27:09 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/Example.hs	Mon Jun 14 15:27:09 2010 +0200
@@ -2,13 +2,6 @@
 
 module Example where {
 
-foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;
-foldla f a [] = a;
-foldla f a (x : xs) = foldla f (f a x) xs;
-
-rev :: forall a. [a] -> [a];
-rev xs = foldla (\ xsa x -> x : xsa) [] xs;
-
 list_case :: forall a b. a -> (b -> [b] -> a) -> [b] -> a;
 list_case f1 f2 (a : list) = f2 a list;
 list_case f1 f2 [] = f1;