--- a/doc-src/Classes/Thy/document/Classes.tex Wed Dec 23 11:32:08 2009 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed Dec 23 11:32:40 2009 +0100
@@ -1148,7 +1148,6 @@
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}\\
\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
\hspace*{0pt}\\
\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
@@ -1233,8 +1232,31 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~val nat{\char95}aux :~IntInf.int -> nat -> nat\\
+\hspace*{0pt} ~val nat :~IntInf.int -> nat\\
+\hspace*{0pt} ~type 'a semigroup\\
+\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
+\hspace*{0pt} ~type 'a monoidl\\
+\hspace*{0pt} ~val semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup\\
+\hspace*{0pt} ~val neutral :~'a monoidl -> 'a\\
+\hspace*{0pt} ~type 'a monoid\\
+\hspace*{0pt} ~val monoidl{\char95}monoid :~'a monoid -> 'a monoidl\\
+\hspace*{0pt} ~type 'a group\\
+\hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\
+\hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\
+\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\
+\hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\
+\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\
+\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\
+\hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\
+\hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\
+\hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\
+\hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\
+\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\
+\hspace*{0pt} ~val example :~IntInf.int\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
@@ -1245,18 +1267,18 @@
\hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
-\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
+\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}semigroup{\char95}monoidl A{\char95};\\
-\hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
+\hspace*{0pt}val semigroup{\char95}monoidl = {\char35}semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup;\\
+\hspace*{0pt}val neutral = {\char35}neutral :~'a monoidl -> 'a;\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
-\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}monoidl{\char95}monoid A{\char95};\\
+\hspace*{0pt}val monoidl{\char95}monoid = {\char35}monoidl{\char95}monoid :~'a monoid -> 'a monoidl;\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
-\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}monoid{\char95}group A{\char95};\\
-\hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
+\hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\
+\hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\
\hspace*{0pt}\\
\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
\hspace*{0pt}\\
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Dec 23 11:32:08 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Dec 23 11:32:40 2009 +0100
@@ -230,7 +230,7 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
\hspace*{0pt} ~datatype boola = True | False\\
\hspace*{0pt} ~val anda :~boola -> boola -> boola\\
\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\
@@ -243,16 +243,16 @@
\hspace*{0pt}datatype boola = True | False;\\
\hspace*{0pt}\\
\hspace*{0pt}fun anda p True = p\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda p False = False\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda True p = p\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda False p = False;\\
+\hspace*{0pt} ~| anda p False = False\\
+\hspace*{0pt} ~| anda True p = p\\
+\hspace*{0pt} ~| anda False p = False;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = False\\
-\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = True;\\
+\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = anda {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat k n{\char123}{\char92}isacharparenright{\char125}~{\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat n l{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -319,7 +319,7 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
@@ -327,12 +327,12 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat k n{\char123}{\char92}isacharparenright{\char125}~andalso {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat n l{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -380,7 +380,7 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
@@ -388,12 +388,12 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Dec 23 11:32:08 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Dec 23 11:32:40 2009 +0100
@@ -147,37 +147,37 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt}{\char92}~{\char92}~val foldl :~{\char123}{\char92}isacharparenleft{\char125}'a -> 'b -> 'a{\char123}{\char92}isacharparenright{\char125}~-> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
\hspace*{0pt} ~val rev :~'a list -> 'a list\\
-\hspace*{0pt} ~val list{\char95}case :~'a -> {\char123}{\char92}isacharparenleft{\char125}'b -> 'b list -> 'a{\char123}{\char92}isacharparenright{\char125}~-> 'b list -> 'a\\
-\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list\\
+\hspace*{0pt} ~val list{\char95}case :~'a -> ('b -> 'b list -> 'a) -> 'b list -> 'a\\
+\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
\hspace*{0pt} ~val empty :~'a queue\\
\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~foldl f a {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= foldl f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
+\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl {\char123}{\char92}isacharparenleft{\char125}fn xsa => fn x => x ::~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
+\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun list{\char123}{\char92}isacharunderscore{\char125}case f1 f2 {\char123}{\char92}isacharparenleft{\char125}a ::~lista{\char123}{\char92}isacharparenright{\char125}~= f2 a lista\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~list{\char123}{\char92}isacharunderscore{\char125}case f1 f2 [] = f1;\\
+\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\
+\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\
\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (NONE,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125})\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~y ::~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}v ::~va{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~=\\
+\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
+\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
+\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\
\hspace*{0pt} ~~~let\\
-\hspace*{0pt} ~~~~~val y ::~ys = rev {\char123}{\char92}isacharparenleft{\char125}v ::~va{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
\hspace*{0pt} ~~~in\\
-\hspace*{0pt} ~~~~~(SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\
\hspace*{0pt} ~~~end;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -234,15 +234,15 @@
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}foldla ::~forall a b.~{\char123}{\char92}isacharparenleft{\char125}a -> b -> a{\char123}{\char92}isacharparenright{\char125}~-> a -> [b] -> a;\\
+\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\
\hspace*{0pt}foldla f a [] = a;\\
-\hspace*{0pt}foldla f a {\char123}{\char92}isacharparenleft{\char125}x :~xs{\char123}{\char92}isacharparenright{\char125}~= foldla f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
+\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 {\char123}{\char92}isacharparenleft{\char125}{\char92}~xsa x -> x :~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
+\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}list{\char95}case ::~forall a b.~a -> {\char123}{\char92}isacharparenleft{\char125}b -> [b] -> a{\char123}{\char92}isacharparenright{\char125}~-> [b] -> a;\\
-\hspace*{0pt}list{\char95}case f1 f2 {\char123}{\char92}isacharparenleft{\char125}a :~list{\char123}{\char92}isacharparenright{\char125}~= f2 a list;\\
+\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;\\
\hspace*{0pt}\\
\hspace*{0pt}data Queue a = AQueue [a] [a];\\
@@ -251,15 +251,15 @@
\hspace*{0pt}empty = AQueue [] [];\\
\hspace*{0pt}\\
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue [] []{\char123}{\char92}isacharparenright{\char125}~= (Nothing,~AQueue [] []);\\
-\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}v :~va{\char123}{\char92}isacharparenright{\char125}~[]{\char123}{\char92}isacharparenright{\char125}~=\\
+\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} ~~~{\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}~= rev {\char123}{\char92}isacharparenleft{\char125}v :~va{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
\hspace*{0pt}\\
\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
-\hspace*{0pt}enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue xs ys{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x :~xs{\char123}{\char92}isacharparenright{\char125}~ys;\\
+\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
--- a/doc-src/Codegen/Thy/document/Program.tex Wed Dec 23 11:32:08 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex Wed Dec 23 11:32:40 2009 +0100
@@ -87,10 +87,10 @@
\isatypewriter%
\noindent%
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue xs []) =\\
\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\
-\hspace*{0pt} ~~~else dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue [] {\char123}{\char92}isacharparenleft{\char125}rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});%
+\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -280,16 +280,16 @@
\hspace*{0pt} ~mult ::~a -> a -> a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}class {\char123}{\char92}isacharparenleft{\char125}Semigroup a{\char123}{\char92}isacharparenright{\char125}~=> 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.~{\char123}{\char92}isacharparenleft{\char125}Monoid a{\char123}{\char92}isacharparenright{\char125}~=> Nat -> a -> a;\\
+\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
-\hspace*{0pt}pow {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~a = mult a {\char123}{\char92}isacharparenleft{\char125}pow n a{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
\hspace*{0pt}\\
\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
-\hspace*{0pt}plus{\char95}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125};\\
+\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}neutral{\char95}nat ::~Nat;\\
@@ -297,7 +297,7 @@
\hspace*{0pt}\\
\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 {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}mult{\char95}nat m n{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
\hspace*{0pt}\\
\hspace*{0pt}instance Semigroup Nat where {\char123}\\
\hspace*{0pt} ~mult = mult{\char95}nat;\\
@@ -308,7 +308,7 @@
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}bexp ::~Nat -> Nat;\\
-\hspace*{0pt}bexp n = pow n {\char123}{\char92}isacharparenleft{\char125}Suc {\char123}{\char92}isacharparenleft{\char125}Suc Zero{\char95}nat{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
@@ -337,13 +337,13 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
\hspace*{0pt} ~type 'a semigroup\\
-\hspace*{0pt} ~val mult :~'a semigroup{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> 'a\\
+\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
\hspace*{0pt} ~type 'a monoid\\
-\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a semigroup\\
-\hspace*{0pt} ~val neutral :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a\\
-\hspace*{0pt} ~val pow :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~nat -> 'a -> 'a\\
+\hspace*{0pt} ~val semigroup{\char95}monoid :~'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\\
\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
@@ -354,30 +354,30 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a semigroup = {\char123}{\char92}isacharbraceleft{\char125}mult :~'a -> 'a -> 'a{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
-\hspace*{0pt}val mult = {\char35}mult :~'a semigroup{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> 'a;\\
+\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}{\char92}isacharbraceleft{\char125}semigroup{\char95}monoid :~'a semigroup{\char123}{\char92}isacharcomma{\char125}~neutral :~'a{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
-\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a semigroup;\\
-\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a;\\
+\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}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~pow A{\char95}~{\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~a = mult {\char123}{\char92}isacharparenleft{\char125}semigroup{\char95}monoid A{\char95}{\char123}{\char92}isacharparenright{\char125}~a {\char123}{\char92}isacharparenleft{\char125}pow A{\char95}~n a{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
\hspace*{0pt}\\
-\hspace*{0pt}fun plus{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~plus{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = n;\\
+\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;\\
\hspace*{0pt}\\
\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun mult{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = Zero{\char95}nat\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~mult{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}mult{\char95}nat m n{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}fun 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}val semigroup{\char95}nat = {\char123}{\char92}isacharbraceleft{\char125}mult = mult{\char95}nat{\char123}{\char92}isacharbraceright{\char125}~:~nat semigroup;\\
+\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat = {\char123}{\char92}isacharbraceleft{\char125}semigroup{\char95}monoid = semigroup{\char95}nat{\char123}{\char92}isacharcomma{\char125}~neutral = neutral{\char95}nat{\char123}{\char92}isacharbraceright{\char125}\\
+\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
\hspace*{0pt} ~:~nat monoid;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}Suc {\char123}{\char92}isacharparenleft{\char125}Suc Zero{\char95}nat{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -666,33 +666,33 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt}{\char92}~{\char92}~val foldl :~{\char123}{\char92}isacharparenleft{\char125}'a -> 'b -> 'a{\char123}{\char92}isacharparenright{\char125}~-> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
\hspace*{0pt} ~val rev :~'a list -> 'a list\\
\hspace*{0pt} ~val null :~'a list -> bool\\
-\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list\\
+\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
\hspace*{0pt} ~val empty :~'a queue\\
\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~foldl f a {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= foldl f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
+\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl {\char123}{\char92}isacharparenleft{\char125}fn xsa => fn x => x ::~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
+\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
\hspace*{0pt}\\
\hspace*{0pt}fun null [] = true\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~null {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= false;\\
+\hspace*{0pt} ~| null (x ::~xs) = false;\\
\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~y ::~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~=\\
-\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125})\\
-\hspace*{0pt} ~~~~~else dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});\\
+\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
+\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
+\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
+\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125};\\
+\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -778,28 +778,28 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt}{\char92}~{\char92}~type 'a eq\\
-\hspace*{0pt} ~val eq :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool\\
-\hspace*{0pt} ~val eqa :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool\\
-\hspace*{0pt} ~val member :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a list -> bool\\
+\hspace*{0pt} ~type 'a eq\\
+\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
+\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
+\hspace*{0pt} ~val member :~'a eq -> 'a -> 'a list -> bool\\
\hspace*{0pt} ~val collect{\char95}duplicates :\\
-\hspace*{0pt} ~~~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a list -> 'a list -> 'a list -> 'a list\\
+\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a eq = {\char123}{\char92}isacharbraceleft{\char125}eq :~'a -> 'a -> bool{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
-\hspace*{0pt}val eq = {\char35}eq :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool;\\
+\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
+\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
\hspace*{0pt}\\
\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
\hspace*{0pt}\\
\hspace*{0pt}fun member A{\char95}~x [] = false\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~member A{\char95}~x {\char123}{\char92}isacharparenleft{\char125}y ::~ys{\char123}{\char92}isacharparenright{\char125}~= eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
+\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun collect{\char123}{\char92}isacharunderscore{\char125}duplicates A{\char95}~xs ys [] = xs\\
-\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~collect{\char123}{\char92}isacharunderscore{\char125}duplicates A{\char95}~xs ys {\char123}{\char92}isacharparenleft{\char125}z ::~zs{\char123}{\char92}isacharparenright{\char125}~=\\
+\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
+\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
-\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs {\char123}{\char92}isacharparenleft{\char125}z ::~ys{\char123}{\char92}isacharparenright{\char125}~zs)\\
-\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~{\char123}{\char92}isacharparenleft{\char125}z ::~xs{\char123}{\char92}isacharparenright{\char125}~{\char123}{\char92}isacharparenleft{\char125}z ::~ys{\char123}{\char92}isacharparenright{\char125}~zs);\\
+\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
+\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -875,11 +875,11 @@
\isatypewriter%
\noindent%
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~{\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}~= rev xs;\\
+\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
-\hspace*{0pt}strict{\char95}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (y,~AQueue xs ys);%
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -969,10 +969,10 @@
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
\hspace*{0pt}\\
\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
+\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue [] {\char123}{\char92}isacharparenleft{\char125}rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});%
+\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
\end{isamarkuptext}%
\isamarkuptrue%
%