diff -r 1ca9055ba1f7 -r 985b13c5a61d doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Sep 07 16:49:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Sep 07 16:58:01 2010 +0200 @@ -231,19 +231,19 @@ \hspace*{0pt}\\ \hspace*{0pt}data Queue a = AQueue [a] [a];\\ \hspace*{0pt}\\ -\hspace*{0pt}empty ::~forall a.~Example.Queue a;\\ -\hspace*{0pt}empty = Example.AQueue [] [];\\ +\hspace*{0pt}empty ::~forall a.~Queue a;\\ +\hspace*{0pt}empty = AQueue [] [];\\ \hspace*{0pt}\\ -\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\ -\hspace*{0pt}dequeue (Example.AQueue [] []) = (Nothing,~Example.AQueue [] []);\\ -\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\ -\hspace*{0pt}dequeue (Example.AQueue (v :~va) []) =\\ +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ +\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\ +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ +\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\ \hspace*{0pt} ~let {\char123}\\ \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\ -\hspace*{0pt} ~{\char125}~in (Just y,~Example.AQueue [] ys);\\ +\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\ \hspace*{0pt}\\ -\hspace*{0pt}enqueue ::~forall a.~a -> Example.Queue a -> Example.Queue a;\\ -\hspace*{0pt}enqueue x (Example.AQueue xs ys) = Example.AQueue (x :~xs) ys;\\ +\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ +\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\ \hspace*{0pt}\\ \hspace*{0pt}{\char125}% \end{isamarkuptext}% @@ -397,41 +397,41 @@ \noindent% \hspace*{0pt}module Example where {\char123}\\ \hspace*{0pt}\\ -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\ +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ \hspace*{0pt}\\ -\hspace*{0pt}plus{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\ -\hspace*{0pt}plus{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat m (Example.Suc n);\\ -\hspace*{0pt}plus{\char95}nat Example.Zero{\char95}nat n = n;\\ +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ \hspace*{0pt}\\ \hspace*{0pt}class Semigroup a where {\char123}\\ \hspace*{0pt} ~mult ::~a -> a -> a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}class (Example.Semigroup a) => Monoid a where {\char123}\\ +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ \hspace*{0pt} ~neutral ::~a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}pow ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\ -\hspace*{0pt}pow Example.Zero{\char95}nat a = Example.neutral;\\ -\hspace*{0pt}pow (Example.Suc n) a = Example.mult a (Example.pow n a);\\ +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ \hspace*{0pt}\\ -\hspace*{0pt}mult{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\ -\hspace*{0pt}mult{\char95}nat Example.Zero{\char95}nat n = Example.Zero{\char95}nat;\\ -\hspace*{0pt}mult{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat n (Example.mult{\char95}nat m n);\\ +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ \hspace*{0pt}\\ -\hspace*{0pt}neutral{\char95}nat ::~Example.Nat;\\ -\hspace*{0pt}neutral{\char95}nat = Example.Suc Example.Zero{\char95}nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Example.Semigroup Example.Nat where {\char123}\\ -\hspace*{0pt} ~mult = Example.mult{\char95}nat;\\ +\hspace*{0pt}instance Semigroup Nat where {\char123}\\ +\hspace*{0pt} ~mult = mult{\char95}nat;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}instance Example.Monoid Example.Nat where {\char123}\\ -\hspace*{0pt} ~neutral = Example.neutral{\char95}nat;\\ +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}instance Monoid Nat where {\char123}\\ +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}bexp ::~Example.Nat -> Example.Nat;\\ -\hspace*{0pt}bexp n = Example.pow n (Example.Suc (Example.Suc Example.Zero{\char95}nat));\\ +\hspace*{0pt}bexp ::~Nat -> Nat;\\ +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ \hspace*{0pt}\\ \hspace*{0pt}{\char125}% \end{isamarkuptext}%