# HG changeset patch # User haftmann # Date 1261564381 -3600 # Node ID 6e82fd81f813596bf60d8387b51a2870b3486e32 # Parent f5dbdbc86b0facc905a43a5dc3264f248c12fa95# Parent 5490151d10528863dc2d45e70190a360419a669e merged diff -r f5dbdbc86b0f -r 6e82fd81f813 doc-src/Classes/Thy/document/Classes.tex --- a/doc-src/Classes/Thy/document/Classes.tex Wed Dec 23 10:41:13 2009 +0100 +++ b/doc-src/Classes/Thy/document/Classes.tex Wed Dec 23 11:33:01 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}\\ diff -r f5dbdbc86b0f -r 6e82fd81f813 doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Dec 23 10:41:13 2009 +0100 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Dec 23 11:33:01 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}% diff -r f5dbdbc86b0f -r 6e82fd81f813 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Dec 23 10:41:13 2009 +0100 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Dec 23 11:33:01 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}% diff -r f5dbdbc86b0f -r 6e82fd81f813 doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Wed Dec 23 10:41:13 2009 +0100 +++ b/doc-src/Codegen/Thy/document/Program.tex Wed Dec 23 11:33:01 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% % diff -r f5dbdbc86b0f -r 6e82fd81f813 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Wed Dec 23 10:41:13 2009 +0100 +++ b/src/Tools/Code/code_haskell.ML Wed Dec 23 11:33:01 2009 +0100 @@ -32,7 +32,7 @@ | SOME class => class; fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs of [] => [] - | classbinds => Pretty.list "(" ")" ( + | classbinds => enum "," "(" ")" ( map (fn (v, class) => str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds) @@ str " => "; @@ -412,11 +412,11 @@ val s = ML_Syntax.print_char c; in if s = "'" then "\\'" else s end; in Literals { - literal_char = enclose "'" "'" o char_haskell, + literal_char = Library.enclose "'" "'" o char_haskell, literal_string = quote o translate_string char_haskell, literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k - else enclose "(" ")" (signed_string_of_int k), - literal_list = Pretty.enum "," "[" "]", + else Library.enclose "(" ")" (signed_string_of_int k), + literal_list = enum "," "[" "]", infix_cons = (5, ":") } end; @@ -451,7 +451,7 @@ val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) (bind :: binds) vars; in - (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) + (brackify fxy o single o enclose "do {" "}" o Pretty.breaks) (ps @| print_term vars' NOBR t'') end | NONE => brackify_infix (1, L) fxy diff -r f5dbdbc86b0f -r 6e82fd81f813 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Wed Dec 23 10:41:13 2009 +0100 +++ b/src/Tools/Code/code_ml.ML Wed Dec 23 11:33:01 2009 +0100 @@ -51,11 +51,11 @@ fun print_product _ [] = NONE | print_product print [x] = SOME (print x) - | print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs); + | print_product print xs = (SOME o enum " *" "" "") (map print xs); fun print_tuple _ _ [] = NONE | print_tuple print fxy [x] = SOME (print fxy x) - | print_tuple print _ xs = SOME (Pretty.list "(" ")" (map (print NOBR) xs)); + | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); (** SML serializer **) @@ -66,13 +66,13 @@ | print_tyco_expr fxy (tyco, [ty]) = concat [print_typ BR ty, (str o deresolve) tyco] | print_tyco_expr fxy (tyco, tys) = - concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] + concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco of NONE => print_tyco_expr fxy (tyco, tys) | SOME (i, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); - fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" "" + fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); @@ -89,7 +89,7 @@ of [] => v_p | [classrel] => brackets [(str o deresolve) classrel, v_p] | classrels => brackets - [Pretty.enum " o" "(" ")" (map (str o deresolve) classrels), v_p] + [enum " o" "(" ")" (map (str o deresolve) classrels), v_p] end and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR @@ -145,9 +145,9 @@ val (ps, vars') = fold_map print_match binds vars; in Pretty.chunks [ - Pretty.block [str ("let"), Pretty.fbrk, Pretty.chunks ps], - Pretty.block [str ("in"), Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body], - str ("end") + Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps], + Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body], + str "end" ] end | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = @@ -174,7 +174,7 @@ let fun print_co (co, []) = str (deresolve co) | print_co (co, tys) = concat [str (deresolve co), str "of", - Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; + enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( str definer @@ -196,7 +196,7 @@ (insert (op =)) ts []); val prolog = if needs_typ then concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] - else Pretty.strs [definer, deresolve name]; + else (concat o map str) [definer, deresolve name]; in concat ( prolog @@ -240,7 +240,7 @@ :: (if is_pseudo_fun inst then [str "()"] else print_dict_args vs) @ str "=" - :: Pretty.list "{" "}" + :: enum "," "{" "}" (map print_superinst superinsts @ map print_classparam classparams) :: str ":" @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs]) @@ -328,7 +328,7 @@ str ("type '" ^ v), (str o deresolve) class, str "=", - Pretty.list "{" "};" ( + enum "," "{" "};" ( map print_superclass_field superclasses @ map print_classparam_field classparams ) @@ -344,7 +344,7 @@ else Pretty.chunks2 ( Pretty.chunks ( str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " =")) - :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls + :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls @| (if is_some some_decls then str "end = struct" else str "struct") ) :: body @@ -357,7 +357,7 @@ literal_numeral = fn unbounded => fn k => if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)" else string_of_int k, - literal_list = Pretty.list "[" "]", + literal_list = enum "," "[" "]", infix_cons = (7, "::") }; @@ -370,13 +370,13 @@ | print_tyco_expr fxy (tyco, [ty]) = concat [print_typ BR ty, (str o deresolve) tyco] | print_tyco_expr fxy (tyco, tys) = - concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] + concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco of NONE => print_tyco_expr fxy (tyco, tys) | SOME (i, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); - fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" "" + fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); @@ -465,7 +465,7 @@ let fun print_co (co, []) = str (deresolve co) | print_co (co, tys) = concat [str (deresolve co), str "of", - Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; + enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( str definer @@ -543,7 +543,7 @@ end; val prolog = if needs_typ then concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] - else Pretty.strs [definer, deresolve name]; + else (concat o map str) [definer, deresolve name]; in pair (print_val_decl print_typscheme (name, vs_ty)) (concat ( @@ -670,7 +670,7 @@ else Pretty.chunks2 ( Pretty.chunks ( str ("module " ^ name ^ (if is_some some_decls then " : sig" else " =")) - :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls + :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls @| (if is_some some_decls then str "end = struct" else str "struct") ) :: body @@ -693,15 +693,15 @@ then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")" else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")" in Literals { - literal_char = enclose "'" "'" o char_ocaml, + literal_char = Library.enclose "'" "'" o char_ocaml, literal_string = quote o translate_string char_ocaml, literal_numeral = fn unbounded => fn k => if k >= 0 then if unbounded then bignum_ocaml k else string_of_int k else if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")" - else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k, - literal_list = Pretty.enum ";" "[" "]", + else (Library.enclose "(" ")" o prefix "-" o string_of_int o op ~) k, + literal_list = enum ";" "[" "]", infix_cons = (6, "::") } end; diff -r f5dbdbc86b0f -r 6e82fd81f813 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Wed Dec 23 10:41:13 2009 +0100 +++ b/src/Tools/Code/code_printer.ML Wed Dec 23 11:33:01 2009 +0100 @@ -18,9 +18,12 @@ val str: string -> Pretty.T val concat: Pretty.T list -> Pretty.T val brackets: Pretty.T list -> Pretty.T + val enclose: string -> string -> Pretty.T list -> Pretty.T + val enum: string -> string -> string -> Pretty.T list -> Pretty.T + val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T val semicolon: Pretty.T list -> Pretty.T val doublesemicolon: Pretty.T list -> Pretty.T - val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T + val indent: int -> Pretty.T -> Pretty.T val string_of_pretty: int -> Pretty.T -> string val writeln_pretty: int -> Pretty.T -> unit @@ -99,11 +102,14 @@ fun xs @| y = xs @ [y]; val str = PrintMode.setmp [] Pretty.str; val concat = Pretty.block o Pretty.breaks; -val brackets = Pretty.enclose "(" ")" o Pretty.breaks; +fun enclose l r = PrintMode.setmp [] (Pretty.enclose l r); +val brackets = enclose "(" ")" o Pretty.breaks; +fun enum sep l r = PrintMode.setmp [] (Pretty.enum sep l r); +fun enum_default default sep l r [] = str default + | enum_default default sep l r xs = enum sep l r xs; fun semicolon ps = Pretty.block [concat ps, str ";"]; fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; -fun enum_default default sep opn cls [] = str default - | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs; +fun indent i = PrintMode.setmp [] (Pretty.indent i); fun string_of_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.string_of) p ^ "\n"; fun writeln_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.writeln) p; @@ -198,7 +204,7 @@ | fixity _ _ = true; fun gen_brackify _ [p] = p - | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps + | gen_brackify true (ps as _::_) = enclose "(" ")" ps | gen_brackify false (ps as _::_) = Pretty.block ps; fun brackify fxy_ctxt = @@ -210,7 +216,7 @@ fun brackify_block fxy_ctxt p1 ps p2 = let val p = Pretty.block_enclose (p1, p2) ps in if fixity BR fxy_ctxt - then Pretty.enclose "(" ")" [p] + then enclose "(" ")" [p] else p end;