# HG changeset patch # User haftmann # Date 1285249577 -7200 # Node ID 0afaf89ab591a1e0bca9a98e21e9f6c0e15610aa # Parent 5096018d5359689d05b3f53c33cba0b2b9d34e62 more canonical type setting of type writer code examples diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Classes/Thy/Classes.thy --- a/doc-src/Classes/Thy/Classes.thy Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Classes/Thy/Classes.thy Thu Sep 23 15:46:17 2010 +0200 @@ -601,18 +601,31 @@ \noindent This maps to Haskell as follows: *} (*<*)code_include %invisible Haskell "Natural" -(*>*) -text %quote {*@{code_stmts example (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts example (Haskell)} + \end{typewriter} +*} text {* \noindent The code in SML has explicit dictionary passing: *} -text %quote {*@{code_stmts example (SML)}*} +text %quote {* + \begin{typewriter} + @{code_stmts example (SML)} + \end{typewriter} +*} + text {* \noindent In Scala, implicts are used as dictionaries: *} (*<*)code_include %invisible Scala "Natural" -(*>*) -text %quote {*@{code_stmts example (Scala)}*} +text %quote {* + \begin{typewriter} + @{code_stmts example (Scala)} + \end{typewriter} +*} subsection {* Inspecting the type class universe *} diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Classes/Thy/document/Classes.tex --- a/doc-src/Classes/Thy/document/Classes.tex Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Classes/Thy/document/Classes.tex Thu Sep 23 15:46:17 2010 +0200 @@ -1130,70 +1130,71 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}module Example where {\char123}\\ -\hspace*{0pt}\\ -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\ -\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\ -\hspace*{0pt}\\ -\hspace*{0pt}nat ::~Integer -> Nat;\\ -\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}class Semigroup a where {\char123}\\ -\hspace*{0pt} ~mult ::~a -> a -> a;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\ -\hspace*{0pt} ~neutral ::~a;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\ -\hspace*{0pt} ~inverse ::~a -> a;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\ -\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\ -\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\ -\hspace*{0pt}\\ -\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\ -\hspace*{0pt}pow{\char95}int k x =\\ -\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\ -\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\ -\hspace*{0pt}\\ -\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\ -\hspace*{0pt}mult{\char95}int i j = i + j;\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Semigroup Integer where {\char123}\\ -\hspace*{0pt} ~mult = mult{\char95}int;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}neutral{\char95}int ::~Integer;\\ -\hspace*{0pt}neutral{\char95}int = 0;\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Monoidl Integer where {\char123}\\ -\hspace*{0pt} ~neutral = neutral{\char95}int;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Monoid Integer where {\char123}\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ -\hspace*{0pt}inverse{\char95}int i = negate i;\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Group Integer where {\char123}\\ -\hspace*{0pt} ~inverse = inverse{\char95}int;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}example ::~Integer;\\ -\hspace*{0pt}example = pow{\char95}int 10 (-2);\\ -\hspace*{0pt}\\ -\hspace*{0pt}{\char125}% +\begin{typewriter} + module\ Example\ where\ {\isacharbraceleft}\isanewline +\isanewline +data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline +\isanewline +nat{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline +nat{\isacharunderscore}aux\ i\ n\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharless}{\isacharequal}\ {\isadigit{0}}\ then\ n\ else\ nat{\isacharunderscore}aux\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +nat\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline +nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline +\isanewline +class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline +\ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoidl\ a\ where\ {\isacharbraceleft}\isanewline +\ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +class\ {\isacharparenleft}Monoidl\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +class\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Group\ a\ where\ {\isacharbraceleft}\isanewline +\ \ inverse\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +pow{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline +pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ mult\ x\ {\isacharparenleft}pow{\isacharunderscore}nat\ n\ x{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Group\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\isanewline +\ \ {\isacharparenleft}if\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline +\ \ \ \ else\ inverse\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}negate\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +mult{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline +mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ i\ {\isacharplus}\ j{\isacharsemicolon}\isanewline +\isanewline +instance\ Semigroup\ Integer\ where\ {\isacharbraceleft}\isanewline +\ \ mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +neutral{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline +neutral{\isacharunderscore}int\ {\isacharequal}\ {\isadigit{0}}{\isacharsemicolon}\isanewline +\isanewline +instance\ Monoidl\ Integer\ where\ {\isacharbraceleft}\isanewline +\ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +instance\ Monoid\ Integer\ where\ {\isacharbraceleft}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +inverse{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline +inverse{\isacharunderscore}int\ i\ {\isacharequal}\ negate\ i{\isacharsemicolon}\isanewline +\isanewline +instance\ Group\ Integer\ where\ {\isacharbraceleft}\isanewline +\ \ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +example\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline +example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +{\isacharbraceright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -1216,86 +1217,87 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\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 pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\ -\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\ -\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\ -\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\ -\hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\ -\hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\ -\hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\ -\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ -\hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\ -\hspace*{0pt} ~val example :~IntInf.int\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun nat{\char95}aux i n =\\ -\hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\ -\hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\ -\hspace*{0pt}\\ -\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}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}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}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}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 pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\ -\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\ -\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\ -\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\ -\hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\ -\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ -\hspace*{0pt}\\ -\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ -\hspace*{0pt}\\ -\hspace*{0pt}val monoidl{\char95}int =\\ -\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\ -\hspace*{0pt} ~IntInf.int monoidl;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\ -\hspace*{0pt} ~IntInf.int group;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val example :~IntInf.int =\\ -\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% +\begin{typewriter} + structure\ Example\ {\isacharcolon}\ sig\isanewline +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline +\ \ val\ nat{\isacharunderscore}aux\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline +\ \ val\ nat\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\isanewline +\ \ type\ {\isacharprime}a\ semigroup\isanewline +\ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ type\ {\isacharprime}a\ monoidl\isanewline +\ \ val\ semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline +\ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ type\ {\isacharprime}a\ monoid\isanewline +\ \ val\ monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl\isanewline +\ \ type\ {\isacharprime}a\ group\isanewline +\ \ val\ monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid\isanewline +\ \ val\ inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ val\ pow{\isacharunderscore}nat\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ val\ pow{\isacharunderscore}int\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ val\ mult{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline +\ \ val\ semigroup{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup\isanewline +\ \ val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline +\ \ val\ monoidl{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoidl\isanewline +\ \ val\ monoid{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid\isanewline +\ \ val\ inverse{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline +\ \ val\ group{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ group\isanewline +\ \ val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline +end\ {\isacharequal}\ struct\isanewline +\isanewline +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline +\isanewline +fun\ nat{\isacharunderscore}aux\ i\ n\ {\isacharequal}\isanewline +\ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}i{\isacharcomma}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharparenright}\ then\ n\isanewline +\ \ \ \ else\ nat{\isacharunderscore}aux\ {\isacharparenleft}IntInf{\isachardot}{\isacharminus}\ {\isacharparenleft}i{\isacharcomma}\ {\isacharparenleft}{\isadigit{1}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +fun\ nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline +\isanewline +type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline +val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline +\isanewline +type\ {\isacharprime}a\ monoidl\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline +val\ semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline +val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline +\isanewline +type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoidl{\isacharbraceright}{\isacharsemicolon}\isanewline +val\ monoidl{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl{\isacharsemicolon}\isanewline +\isanewline +type\ {\isacharprime}a\ group\ {\isacharequal}\ {\isacharbraceleft}monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ monoid{\isacharcomma}\ inverse\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline +val\ monoid{\isacharunderscore}group\ {\isacharequal}\ {\isacharhash}monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid{\isacharsemicolon}\isanewline +val\ inverse\ {\isacharequal}\ {\isacharhash}inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline +\isanewline +fun\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral\ {\isacharparenleft}monoidl{\isacharunderscore}monoid\ A{\isacharunderscore}{\isacharparenright}\isanewline +\ \ {\isacharbar}\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\isanewline +\ \ \ \ mult\ {\isacharparenleft}{\isacharparenleft}semigroup{\isacharunderscore}monoidl\ o\ monoidl{\isacharunderscore}monoid{\isacharparenright}\ A{\isacharunderscore}{\isacharparenright}\ x\ {\isacharparenleft}pow{\isacharunderscore}nat\ A{\isacharunderscore}\ n\ x{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +fun\ pow{\isacharunderscore}int\ A{\isacharunderscore}\ k\ x\ {\isacharequal}\isanewline +\ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharcomma}\ k{\isacharparenright}\isanewline +\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}monoid{\isacharunderscore}group\ A{\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline +\ \ \ \ else\ inverse\ A{\isacharunderscore}\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}monoid{\isacharunderscore}group\ A{\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}nat\ {\isacharparenleft}IntInf{\isachardot}{\isachartilde}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +fun\ mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +val\ semigroup{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup{\isacharsemicolon}\isanewline +\isanewline +val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +val\ monoidl{\isacharunderscore}int\ {\isacharequal}\isanewline +\ \ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ semigroup{\isacharunderscore}int{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline +\ \ IntInf{\isachardot}int\ monoidl{\isacharsemicolon}\isanewline +\isanewline +val\ monoid{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharequal}\ monoidl{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid{\isacharsemicolon}\isanewline +\isanewline +fun\ inverse{\isacharunderscore}int\ i\ {\isacharequal}\ IntInf{\isachardot}{\isachartilde}\ i{\isacharsemicolon}\isanewline +\isanewline +val\ group{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoid{\isacharunderscore}group\ {\isacharequal}\ monoid{\isacharunderscore}int{\isacharcomma}\ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline +\ \ IntInf{\isachardot}int\ group{\isacharsemicolon}\isanewline +\isanewline +val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\isanewline +\ \ pow{\isacharunderscore}int\ group{\isacharunderscore}int\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}\ {\isacharparenleft}{\isachartilde}{\isadigit{2}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -1331,76 +1333,77 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}object Example {\char123}\\ -\hspace*{0pt}\\ -\hspace*{0pt}abstract sealed class nat\\ -\hspace*{0pt}final case object Zero{\char95}nat extends nat\\ -\hspace*{0pt}final case class Suc(a:~nat) extends nat\\ -\hspace*{0pt}\\ -\hspace*{0pt}def nat{\char95}aux(i:~BigInt,~n:~nat):~nat =\\ -\hspace*{0pt} ~(if (i <= BigInt(0)) n else nat{\char95}aux(i - BigInt(1),~Suc(n)))\\ -\hspace*{0pt}\\ -\hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\ -\hspace*{0pt}\\ -\hspace*{0pt}trait semigroup[A] {\char123}\\ -\hspace*{0pt} ~val `Example.mult`:~(A,~A) => A\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\ -\hspace*{0pt} ~A.`Example.mult`(a,~b)\\ -\hspace*{0pt}\\ -\hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\ -\hspace*{0pt} ~val `Example.neutral`:~A\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example.neutral`\\ -\hspace*{0pt}\\ -\hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}\\ -\hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\ -\hspace*{0pt} ~val `Example.inverse`:~A => A\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example.inverse`(a)\\ -\hspace*{0pt}\\ -\hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\ -\hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\ -\hspace*{0pt} ~case (Suc(n),~x) => mult[A](x,~pow{\char95}nat[A](n,~x))\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}\\ -\hspace*{0pt}def pow{\char95}int[A:~group](k:~BigInt,~x:~A):~A =\\ -\hspace*{0pt} ~(if (BigInt(0) <= k) pow{\char95}nat[A](nat(k),~x)\\ -\hspace*{0pt} ~~~else inverse[A](pow{\char95}nat[A](nat((- k)),~x)))\\ -\hspace*{0pt}\\ -\hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\ -\hspace*{0pt}\\ -\hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\ -\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}\\ -\hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\ -\hspace*{0pt}\\ -\hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\ -\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ -\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}\\ -\hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\ -\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ -\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}\\ -\hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\ -\hspace*{0pt}\\ -\hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\ -\hspace*{0pt} ~val `Example.inverse` = (a:~BigInt) => inverse{\char95}int(a)\\ -\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ -\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ -\hspace*{0pt}{\char125}\\ -\hspace*{0pt}\\ -\hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\ -\hspace*{0pt}\\ -\hspace*{0pt}{\char125}~/* object Example */% +\begin{typewriter} + object\ Example\ {\isacharbraceleft}\isanewline +\isanewline +abstract\ sealed\ class\ nat\isanewline +final\ case\ object\ Zero{\isacharunderscore}nat\ extends\ nat\isanewline +final\ case\ class\ Suc{\isacharparenleft}a{\isacharcolon}\ nat{\isacharparenright}\ extends\ nat\isanewline +\isanewline +def\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ n{\isacharcolon}\ nat{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\isanewline +\ \ {\isacharparenleft}if\ {\isacharparenleft}i\ {\isacharless}{\isacharequal}\ BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ n\ else\ nat{\isacharunderscore}aux{\isacharparenleft}i\ {\isacharminus}\ BigInt{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharcomma}\ Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline +\isanewline +def\ nat{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}\isanewline +\isanewline +trait\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharcolon}\ {\isacharparenleft}A{\isacharcomma}\ A{\isacharparenright}\ {\isacharequal}{\isachargreater}\ A\isanewline +{\isacharbraceright}\isanewline +def\ mult{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}a{\isacharcolon}\ A{\isacharcomma}\ b{\isacharcolon}\ A{\isacharparenright}{\isacharparenleft}implicit\ A{\isacharcolon}\ semigroup{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\isanewline +\ \ A{\isachardot}{\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline +\isanewline +trait\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ extends\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}{\isacharcolon}\ A\isanewline +{\isacharbraceright}\isanewline +def\ neutral{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}implicit\ A{\isacharcolon}\ monoidl{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ A{\isachardot}{\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\isanewline +\isanewline +trait\ monoid{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline +{\isacharbraceright}\isanewline +\isanewline +trait\ group{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoid{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}{\isacharcolon}\ A\ {\isacharequal}{\isachargreater}\ A\isanewline +{\isacharbraceright}\isanewline +def\ inverse{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}a{\isacharcolon}\ A{\isacharparenright}{\isacharparenleft}implicit\ A{\isacharcolon}\ group{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ A{\isachardot}{\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}{\isacharparenleft}a{\isacharparenright}\isanewline +\isanewline +def\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharcolon}\ monoid{\isacharbrackright}{\isacharparenleft}xa{\isadigit{0}}{\isacharcolon}\ nat{\isacharcomma}\ x{\isacharcolon}\ A{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ {\isacharparenleft}xa{\isadigit{0}}{\isacharcomma}\ x{\isacharparenright}\ match\ {\isacharbraceleft}\isanewline +\ \ case\ {\isacharparenleft}Zero{\isacharunderscore}nat{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}{\isachargreater}\ neutral{\isacharbrackleft}A{\isacharbrackright}\isanewline +\ \ case\ {\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}x{\isacharcomma}\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}n{\isacharcomma}\ x{\isacharparenright}{\isacharparenright}\isanewline +{\isacharbraceright}\isanewline +\isanewline +def\ pow{\isacharunderscore}int{\isacharbrackleft}A{\isacharcolon}\ group{\isacharbrackright}{\isacharparenleft}k{\isacharcolon}\ BigInt{\isacharcomma}\ x{\isacharcolon}\ A{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\isanewline +\ \ {\isacharparenleft}if\ {\isacharparenleft}BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}\ {\isacharless}{\isacharequal}\ k{\isacharparenright}\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}nat{\isacharparenleft}k{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}\isanewline +\ \ \ \ else\ inverse{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}nat{\isacharparenleft}{\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline +\isanewline +def\ mult{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ j{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ i\ {\isacharplus}\ j\isanewline +\isanewline +implicit\ def\ semigroup{\isacharunderscore}int{\isacharcolon}\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline +{\isacharbraceright}\isanewline +\isanewline +def\ neutral{\isacharunderscore}int{\isacharcolon}\ BigInt\ {\isacharequal}\ BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}\isanewline +\isanewline +implicit\ def\ monoidl{\isacharunderscore}int{\isacharcolon}\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline +{\isacharbraceright}\isanewline +\isanewline +implicit\ def\ monoid{\isacharunderscore}int{\isacharcolon}\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline +{\isacharbraceright}\isanewline +\isanewline +def\ inverse{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ {\isacharparenleft}{\isacharminus}\ i{\isacharparenright}\isanewline +\isanewline +implicit\ def\ group{\isacharunderscore}int{\isacharcolon}\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ inverse{\isacharunderscore}int{\isacharparenleft}a{\isacharparenright}\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline +\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline +{\isacharbraceright}\isanewline +\isanewline +def\ example{\isacharcolon}\ BigInt\ {\isacharequal}\ pow{\isacharunderscore}int{\isacharbrackleft}BigInt{\isacharbrackright}{\isacharparenleft}BigInt{\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharparenright}{\isacharcomma}\ BigInt{\isacharparenleft}{\isacharminus}\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline +\isanewline +{\isacharbraceright}\ {\isacharslash}{\isacharasterisk}\ object\ Example\ {\isacharasterisk}{\isacharslash}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Classes/style.sty --- a/doc-src/Classes/style.sty Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Classes/style.sty Thu Sep 23 15:46:17 2010 +0200 @@ -26,6 +26,12 @@ \renewcommand{\endisatagquote}{\end{quote}} \newcommand{\quotebreak}{\\[1.2ex]} +%% typewriter text +\newenvironment{typewriter}{\renewcommand{\isadigit}[1]{{##1}}% +\def\isacharunderscore{\_}% +\parindent0pt\fontsize{9pt}{0pt}% +\tt\setlength{\baselineskip}{8pt}\renewcommand{\baselinestretch}{1}}{} + %% presentation \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/Adaptation.thy --- a/doc-src/Codegen/Thy/Adaptation.thy Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/Adaptation.thy Thu Sep 23 15:46:17 2010 +0200 @@ -175,7 +175,11 @@ code_const %invisible True and False and "op \" and Not (SML and and and) (*>*) -text %quote {*@{code_stmts in_interval (SML)}*} +text %quote {* + \begin{typewriter} + @{code_stmts in_interval (SML)} + \end{typewriter} +*} text {* \noindent Though this is correct code, it is a little bit @@ -204,7 +208,11 @@ placeholder for the type constructor's (the constant's) arguments. *} -text %quote {*@{code_stmts in_interval (SML)}*} +text %quote {* + \begin{typewriter} + @{code_stmts in_interval (SML)} + \end{typewriter} +*} text {* \noindent This still is not perfect: the parentheses around the @@ -217,7 +225,11 @@ code_const %quotett "op \" (SML infixl 1 "andalso") -text %quote {*@{code_stmts in_interval (SML)}*} +text %quote {* + \begin{typewriter} + @{code_stmts in_interval (SML)} + \end{typewriter} +*} text {* \noindent The attentive reader may ask how we assert that no diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/Foundations.thy --- a/doc-src/Codegen/Thy/Foundations.thy Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/Foundations.thy Thu Sep 23 15:46:17 2010 +0200 @@ -161,7 +161,11 @@ is determined syntactically. The resulting code: *} -text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts dequeue (consts) dequeue (Haskell)} + \end{typewriter} +*} text {* \noindent You may note that the equality test @{term "xs = []"} has @@ -215,7 +219,11 @@ equality check, as can be seen in the corresponding @{text SML} code: *} -text %quote {*@{code_stmts collect_duplicates (SML)}*} +text %quote {* + \begin{typewriter} + @{code_stmts collect_duplicates (SML)} + \end{typewriter} +*} text {* \noindent Obviously, polymorphic equality is implemented the Haskell @@ -251,7 +259,11 @@ for the pattern @{term "AQueue [] []"}: *} -text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)} + \end{typewriter} +*} text {* \noindent In some cases it is desirable to have this @@ -290,7 +302,11 @@ exception at the appropriate position: *} -text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)} + \end{typewriter} +*} text {* \noindent This feature however is rarely needed in practice. Note diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Thu Sep 23 15:46:17 2010 +0200 @@ -112,7 +112,11 @@ After this setup procedure, code generation can continue as usual: *} -text %quote {*@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)} + \end{typewriter} +*} subsection {* Imperative data structures *} diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/Introduction.thy --- a/doc-src/Codegen/Thy/Introduction.thy Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/Introduction.thy Thu Sep 23 15:46:17 2010 +0200 @@ -70,7 +70,11 @@ text {* \noindent resulting in the following code: *} -text %quote {*@{code_stmts empty enqueue dequeue (SML)}*} +text %quote {* + \begin{typewriter} + @{code_stmts empty enqueue dequeue (SML)} + \end{typewriter} +*} text {* \noindent The @{command_def export_code} command takes a @@ -91,7 +95,11 @@ \noindent This is the corresponding code: *} -text %quote {*@{code_stmts empty enqueue dequeue (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts empty enqueue dequeue (Haskell)} + \end{typewriter} +*} text {* \noindent For more details about @{command export_code} see @@ -164,7 +172,11 @@ native classes: *} -text %quote {*@{code_stmts bexp (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts bexp (Haskell)} + \end{typewriter} +*} text {* \noindent This is a convenient place to show how explicit dictionary @@ -172,7 +184,11 @@ @{text SML}: *} -text %quote {*@{code_stmts bexp (SML)}*} +text %quote {* + \begin{typewriter} + @{code_stmts bexp (SML)} + \end{typewriter} +*} text {* \noindent Note the parameters with trailing underscore (@{verbatim diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/Refinement.thy --- a/doc-src/Codegen/Thy/Refinement.thy Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/Refinement.thy Thu Sep 23 15:46:17 2010 +0200 @@ -31,7 +31,11 @@ to two recursive calls: *} -text %quote {*@{code_stmts fib (consts) fib (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts fib (consts) fib (Haskell)} + \end{typewriter} +*} text {* \noindent A more efficient implementation would use dynamic @@ -67,7 +71,11 @@ \noindent The resulting code shows only linear growth of runtime: *} -text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*} +text %quote {* + \begin{typewriter} + @{code_stmts fib (consts) fib fib_step (Haskell)} + \end{typewriter} +*} subsection {* Datatype refinement *} @@ -153,7 +161,11 @@ \noindent The resulting code looks as expected: *} -text %quote {*@{code_stmts empty enqueue dequeue (SML)}*} +text %quote {* + \begin{typewriter} + @{code_stmts empty enqueue dequeue (SML)} + \end{typewriter} +*} text {* The same techniques can also be applied to types which are not @@ -248,7 +260,9 @@ *} text %quote {* - @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)} + \begin{typewriter} + @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)} + \end{typewriter} *} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *) text {* diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Thu Sep 23 15:46:17 2010 +0200 @@ -235,34 +235,35 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\ -\hspace*{0pt} ~datatype boola = True | False\\ -\hspace*{0pt} ~val conj :~boola -> boola -> boola\\ -\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\ -\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> boola\\ -\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> boola\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype boola = True | False;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun conj p True = p\\ -\hspace*{0pt} ~| conj p False = False\\ -\hspace*{0pt} ~| conj True p = p\\ -\hspace*{0pt} ~| conj False p = False;\\ -\hspace*{0pt}\\ -\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{\char95}interval (k,~l) n = conj (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% +\begin{typewriter} + structure\ Example\ {\isacharcolon}\ sig\isanewline +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline +\ \ datatype\ boola\ {\isacharequal}\ True\ {\isacharbar}\ False\isanewline +\ \ val\ conj\ {\isacharcolon}\ boola\ {\isacharminus}{\isachargreater}\ boola\ {\isacharminus}{\isachargreater}\ boola\isanewline +\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline +\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline +\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ boola\isanewline +end\ {\isacharequal}\ struct\isanewline +\isanewline +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline +\isanewline +datatype\ boola\ {\isacharequal}\ True\ {\isacharbar}\ False{\isacharsemicolon}\isanewline +\isanewline +fun\ conj\ p\ True\ {\isacharequal}\ p\isanewline +\ \ {\isacharbar}\ conj\ p\ False\ {\isacharequal}\ False\isanewline +\ \ {\isacharbar}\ conj\ True\ p\ {\isacharequal}\ p\isanewline +\ \ {\isacharbar}\ conj\ False\ p\ {\isacharequal}\ False{\isacharsemicolon}\isanewline +\isanewline +fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline +\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ False\isanewline +and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline +\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ True{\isacharsemicolon}\isanewline +\isanewline +fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ conj\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n{\isacharparenright}\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -320,25 +321,26 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\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\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\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{\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*)% +\begin{typewriter} + structure\ Example\ {\isacharcolon}\ sig\isanewline +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline +\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline +\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline +\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline +end\ {\isacharequal}\ struct\isanewline +\isanewline +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline +\isanewline +fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline +\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ false\isanewline +and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline +\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ true{\isacharsemicolon}\isanewline +\isanewline +fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n{\isacharparenright}\ andalso\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -380,25 +382,26 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\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\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\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{\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*)% +\begin{typewriter} + structure\ Example\ {\isacharcolon}\ sig\isanewline +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline +\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline +\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline +\ \ val\ in{\isacharunderscore}interval\ {\isacharcolon}\ nat\ {\isacharasterisk}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline +end\ {\isacharequal}\ struct\isanewline +\isanewline +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline +\isanewline +fun\ less{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ m\ n\isanewline +\ \ {\isacharbar}\ less{\isacharunderscore}nat\ n\ Zero{\isacharunderscore}nat\ {\isacharequal}\ false\isanewline +and\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}nat\ m\ n\isanewline +\ \ {\isacharbar}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ true{\isacharsemicolon}\isanewline +\isanewline +fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n\ andalso\ less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharsemicolon}\isanewline +\isanewline +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/document/Foundations.tex --- a/doc-src/Codegen/Thy/document/Foundations.tex Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Thu Sep 23 15:46:17 2010 +0200 @@ -245,13 +245,13 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ -\hspace*{0pt}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ -\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% +\begin{typewriter} + dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline +dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline +dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon} + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -347,33 +347,34 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~type 'a equal\\ -\hspace*{0pt} ~val equal :~'a equal -> 'a -> 'a -> bool\\ -\hspace*{0pt} ~val eq :~'a equal -> 'a -> 'a -> bool\\ -\hspace*{0pt} ~val member :~'a equal -> 'a list -> 'a -> bool\\ -\hspace*{0pt} ~val collect{\char95}duplicates :\\ -\hspace*{0pt} ~~~'a equal -> 'a list -> 'a list -> 'a list -> 'a list\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a equal = {\char123}equal :~'a -> 'a -> bool{\char125};\\ -\hspace*{0pt}val equal = {\char35}equal :~'a equal -> 'a -> 'a -> bool;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun eq A{\char95}~a b = equal A{\char95}~a b;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun member A{\char95}~[] y = false\\ -\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eq A{\char95}~x y orelse member A{\char95}~xs y;\\ -\hspace*{0pt}\\ -\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}~xs z\\ -\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys 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*)% +\begin{typewriter} + structure\ Example\ {\isacharcolon}\ sig\isanewline +\ \ type\ {\isacharprime}a\ equal\isanewline +\ \ val\ equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline +\ \ val\ eq\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline +\ \ val\ member\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline +\ \ val\ collect{\isacharunderscore}duplicates\ {\isacharcolon}\isanewline +\ \ \ \ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline +end\ {\isacharequal}\ struct\isanewline +\isanewline +type\ {\isacharprime}a\ equal\ {\isacharequal}\ {\isacharbraceleft}equal\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool{\isacharbraceright}{\isacharsemicolon}\isanewline +val\ equal\ {\isacharequal}\ {\isacharhash}equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool{\isacharsemicolon}\isanewline +\isanewline +fun\ eq\ A{\isacharunderscore}\ a\ b\ {\isacharequal}\ equal\ A{\isacharunderscore}\ a\ b{\isacharsemicolon}\isanewline +\isanewline +fun\ member\ A{\isacharunderscore}\ {\isacharbrackleft}{\isacharbrackright}\ y\ {\isacharequal}\ false\isanewline +\ \ {\isacharbar}\ member\ A{\isacharunderscore}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ y\ {\isacharequal}\ eq\ A{\isacharunderscore}\ x\ y\ orelse\ member\ A{\isacharunderscore}\ xs\ y{\isacharsemicolon}\isanewline +\isanewline +fun\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline +\ \ {\isacharbar}\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ zs{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}if\ member\ A{\isacharunderscore}\ xs\ z\isanewline +\ \ \ \ \ \ then\ {\isacharparenleft}if\ member\ A{\isacharunderscore}\ ys\ z\ then\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ ys\ zs\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}\isanewline +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -442,14 +443,14 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~let {\char123}\\ -\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% +\begin{typewriter} + strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ let\ {\isacharbraceleft}\isanewline +\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ xs{\isacharsemicolon}\isanewline +\ \ {\isacharbraceright}\ in\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon} + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -533,16 +534,16 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ -\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 (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ -\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% +\begin{typewriter} + empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline +empty{\isacharunderscore}queue\ {\isacharequal}\ error\ {\isachardoublequote}empty{\isacharunderscore}queue{\isachardoublequote}{\isacharsemicolon}\isanewline +\isanewline +strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ {\isacharparenleft}if\ null\ xs\ then\ empty{\isacharunderscore}queue\isanewline +\ \ \ \ else\ strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon} + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Further.tex Thu Sep 23 15:46:17 2010 +0200 @@ -214,15 +214,15 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\ -\hspace*{0pt}funpow Zero{\char95}nat f = id;\\ -\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\ -\hspace*{0pt}\\ -\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\ -\hspace*{0pt}funpows [] = id;\\ -\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;% +\begin{typewriter} + funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +funpow\ Zero{\isacharunderscore}nat\ f\ {\isacharequal}\ id{\isacharsemicolon}\isanewline +funpow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ f\ {\isacharequal}\ f\ {\isachardot}\ funpow\ n\ f{\isacharsemicolon}\isanewline +\isanewline +funpows\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharbrackleft}Nat{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +funpows\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isacharsemicolon}\isanewline +funpows\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ funpow\ x\ {\isachardot}\ funpows\ xs{\isacharsemicolon} + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Thu Sep 23 15:46:17 2010 +0200 @@ -140,41 +140,42 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~val id :~'a -> 'a\\ -\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\ -\hspace*{0pt} ~val rev :~'a list -> '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 id x = (fn xa => xa) x;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun fold f [] = id\\ -\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ -\hspace*{0pt}\\ -\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 (v ::~va);\\ -\hspace*{0pt} ~~~in\\ -\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\ -\hspace*{0pt} ~~~end;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% +\begin{typewriter} + structure\ Example\ {\isacharcolon}\ sig\isanewline +\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline +\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline +\ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline +\ \ val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\isanewline +\ \ val\ dequeue\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ option\ {\isacharasterisk}\ {\isacharprime}a\ queue\isanewline +\ \ val\ enqueue\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\isanewline +end\ {\isacharequal}\ struct\isanewline +\isanewline +fun\ id\ x\ {\isacharequal}\ {\isacharparenleft}fn\ xa\ {\isacharequal}{\isachargreater}\ xa{\isacharparenright}\ x{\isacharsemicolon}\isanewline +\isanewline +fun\ fold\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id\isanewline +\ \ {\isacharbar}\ fold\ f\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ fold\ f\ xs\ o\ f\ x{\isacharsemicolon}\isanewline +\isanewline +fun\ rev\ xs\ {\isacharequal}\ fold\ {\isacharparenleft}fn\ a\ {\isacharequal}{\isachargreater}\ fn\ b\ {\isacharequal}{\isachargreater}\ a\ {\isacharcolon}{\isacharcolon}\ b{\isacharparenright}\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline +\isanewline +datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list{\isacharsemicolon}\isanewline +\isanewline +val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +fun\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline +\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline +\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}v\ {\isacharcolon}{\isacharcolon}\ va{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ let\isanewline +\ \ \ \ \ \ val\ y\ {\isacharcolon}{\isacharcolon}\ ys\ {\isacharequal}\ rev\ {\isacharparenleft}v\ {\isacharcolon}{\isacharcolon}\ va{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ in\isanewline +\ \ \ \ \ \ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline +\ \ \ \ end{\isacharsemicolon}\isanewline +\isanewline +fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -225,27 +226,28 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}module Example where {\char123}\\ -\hspace*{0pt}\\ -\hspace*{0pt}data Queue a = AQueue [a] [a];\\ -\hspace*{0pt}\\ -\hspace*{0pt}empty ::~forall a.~Queue a;\\ -\hspace*{0pt}empty = AQueue [] [];\\ -\hspace*{0pt}\\ -\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,~AQueue [] ys);\\ -\hspace*{0pt}\\ -\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}% +\begin{typewriter} + module\ Example\ where\ {\isacharbraceleft}\isanewline +\isanewline +data\ Queue\ a\ {\isacharequal}\ AQueue\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline +\isanewline +empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a{\isacharsemicolon}\isanewline +empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline +\isanewline +dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline +dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline +dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline +dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}v\ {\isacharcolon}\ va{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ let\ {\isacharbraceleft}\isanewline +\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ {\isacharparenleft}v\ {\isacharcolon}\ va{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ {\isacharbraceright}\ in\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +enqueue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a\ {\isacharminus}{\isachargreater}\ Queue\ a\ {\isacharminus}{\isachargreater}\ Queue\ a{\isacharsemicolon}\isanewline +enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ ys{\isacharsemicolon}\isanewline +\isanewline +{\isacharbraceright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -393,47 +395,48 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}module Example where {\char123}\\ -\hspace*{0pt}\\ -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ -\hspace*{0pt}\\ -\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 (Semigroup a) => Monoid a where {\char123}\\ -\hspace*{0pt} ~neutral ::~a;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\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 ::~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}instance Semigroup Nat where {\char123}\\ -\hspace*{0pt} ~mult = mult{\char95}nat;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\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 ::~Nat -> Nat;\\ -\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ -\hspace*{0pt}\\ -\hspace*{0pt}{\char125}% +\begin{typewriter} + module\ Example\ where\ {\isacharbraceleft}\isanewline +\isanewline +data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline +\isanewline +plus{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline +plus{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\isanewline +plus{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ n{\isacharsemicolon}\isanewline +\isanewline +class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline +\ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline +\ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +pow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +pow\ Zero{\isacharunderscore}nat\ a\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline +pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ mult\ a\ {\isacharparenleft}pow\ n\ a{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +mult{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline +mult{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline +mult{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ n\ {\isacharparenleft}mult{\isacharunderscore}nat\ m\ n{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +instance\ Semigroup\ Nat\ where\ {\isacharbraceleft}\isanewline +\ \ mult\ {\isacharequal}\ mult{\isacharunderscore}nat{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +neutral{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat{\isacharsemicolon}\isanewline +neutral{\isacharunderscore}nat\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline +\isanewline +instance\ Monoid\ Nat\ where\ {\isacharbraceleft}\isanewline +\ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}nat{\isacharsemicolon}\isanewline +{\isacharbraceright}{\isacharsemicolon}\isanewline +\isanewline +bexp\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline +bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +{\isacharbraceright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -458,52 +461,53 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\ -\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\ -\hspace*{0pt} ~type 'a semigroup\\ -\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\ -\hspace*{0pt} ~type 'a monoid\\ -\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\ -\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ -\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ -\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ -\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ -\hspace*{0pt} ~val neutral{\char95}nat :~nat\\ -\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ -\hspace*{0pt} ~val bexp :~nat -> nat\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ -\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ -\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ -\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\ -\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ -\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ -\hspace*{0pt}\\ -\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}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ -\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 (Suc (Suc Zero{\char95}nat));\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% +\begin{typewriter} + structure\ Example\ {\isacharcolon}\ sig\isanewline +\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline +\ \ val\ plus{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline +\ \ type\ {\isacharprime}a\ semigroup\isanewline +\ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ type\ {\isacharprime}a\ monoid\isanewline +\ \ val\ semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline +\ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ val\ pow\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ val\ mult{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline +\ \ val\ semigroup{\isacharunderscore}nat\ {\isacharcolon}\ nat\ semigroup\isanewline +\ \ val\ neutral{\isacharunderscore}nat\ {\isacharcolon}\ nat\isanewline +\ \ val\ monoid{\isacharunderscore}nat\ {\isacharcolon}\ nat\ monoid\isanewline +\ \ val\ bexp\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline +end\ {\isacharequal}\ struct\isanewline +\isanewline +datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline +\isanewline +fun\ plus{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline +\ \ {\isacharbar}\ plus{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ n{\isacharsemicolon}\isanewline +\isanewline +type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline +val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline +\isanewline +type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline +val\ semigroup{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline +val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline +\isanewline +fun\ pow\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ a\ {\isacharequal}\ neutral\ A{\isacharunderscore}\isanewline +\ \ {\isacharbar}\ pow\ A{\isacharunderscore}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ mult\ {\isacharparenleft}semigroup{\isacharunderscore}monoid\ A{\isacharunderscore}{\isacharparenright}\ a\ {\isacharparenleft}pow\ A{\isacharunderscore}\ n\ a{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +fun\ mult{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ Zero{\isacharunderscore}nat\isanewline +\ \ {\isacharbar}\ mult{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ n\ {\isacharparenleft}mult{\isacharunderscore}nat\ m\ n{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +val\ semigroup{\isacharunderscore}nat\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}nat{\isacharbraceright}\ {\isacharcolon}\ nat\ semigroup{\isacharsemicolon}\isanewline +\isanewline +val\ neutral{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline +\isanewline +val\ monoid{\isacharunderscore}nat\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoid\ {\isacharequal}\ semigroup{\isacharunderscore}nat{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}nat{\isacharbraceright}\isanewline +\ \ {\isacharcolon}\ nat\ monoid{\isacharsemicolon}\isanewline +\isanewline +fun\ bexp\ n\ {\isacharequal}\ pow\ monoid{\isacharunderscore}nat\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/Thy/document/Refinement.tex --- a/doc-src/Codegen/Thy/document/Refinement.tex Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Thu Sep 23 15:46:17 2010 +0200 @@ -72,12 +72,12 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}fib ::~Nat -> Nat;\\ -\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\ -\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\ -\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));% +\begin{typewriter} + fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline +fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline +fib\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline +fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon} + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -170,17 +170,17 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\ -\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\ -\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\ -\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\ -\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\ -\hspace*{0pt}\\ -\hspace*{0pt}fib ::~Nat -> Nat;\\ -\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\ -\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;% +\begin{typewriter} + fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline +fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ let\ {\isacharbraceleft}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceright}\ in\ {\isacharparenleft}plus{\isacharunderscore}nat\ m\ q{\isacharcomma}\ m{\isacharparenright}{\isacharsemicolon}\isanewline +fib{\isacharunderscore}step\ Zero{\isacharunderscore}nat\ {\isacharequal}\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline +fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isacharsemicolon}\isanewline +fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon} + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -348,41 +348,42 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~val id :~'a -> 'a\\ -\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\ -\hspace*{0pt} ~val rev :~'a list -> 'a list\\ -\hspace*{0pt} ~val null :~'a list -> bool\\ -\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 id x = (fn xa => xa) x;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun fold f [] = id\\ -\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun null [] = true\\ -\hspace*{0pt} ~| null (x ::~xs) = false;\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ -\hspace*{0pt}\\ -\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 (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% +\begin{typewriter} + structure\ Example\ {\isacharcolon}\ sig\isanewline +\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline +\ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline +\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline +\ \ val\ null\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ bool\isanewline +\ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline +\ \ val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\isanewline +\ \ val\ dequeue\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ option\ {\isacharasterisk}\ {\isacharprime}a\ queue\isanewline +\ \ val\ enqueue\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\isanewline +end\ {\isacharequal}\ struct\isanewline +\isanewline +fun\ id\ x\ {\isacharequal}\ {\isacharparenleft}fn\ xa\ {\isacharequal}{\isachargreater}\ xa{\isacharparenright}\ x{\isacharsemicolon}\isanewline +\isanewline +fun\ fold\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id\isanewline +\ \ {\isacharbar}\ fold\ f\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ fold\ f\ xs\ o\ f\ x{\isacharsemicolon}\isanewline +\isanewline +fun\ rev\ xs\ {\isacharequal}\ fold\ {\isacharparenleft}fn\ a\ {\isacharequal}{\isachargreater}\ fn\ b\ {\isacharequal}{\isachargreater}\ a\ {\isacharcolon}{\isacharcolon}\ b{\isacharparenright}\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline +\isanewline +fun\ null\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ true\isanewline +\ \ {\isacharbar}\ null\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ false{\isacharsemicolon}\isanewline +\isanewline +datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list{\isacharsemicolon}\isanewline +\isanewline +val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +fun\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline +\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline +\ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % @@ -584,36 +585,37 @@ \isatagquote % \begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}module Example where {\char123}\\ -\hspace*{0pt}\\ -\hspace*{0pt}newtype Dlist a = Dlist [a];\\ -\hspace*{0pt}\\ -\hspace*{0pt}empty ::~forall a.~Dlist a;\\ -\hspace*{0pt}empty = Dlist [];\\ -\hspace*{0pt}\\ -\hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\ -\hspace*{0pt}member [] y = False;\\ -\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\ -\hspace*{0pt}\\ -\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> [a] -> [a];\\ -\hspace*{0pt}insert x xs = (if member xs x then xs else x :~xs);\\ -\hspace*{0pt}\\ -\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\ -\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\ -\hspace*{0pt}\\ -\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\ -\hspace*{0pt}inserta x dxs = Dlist (insert x (list{\char95}of{\char95}dlist dxs));\\ -\hspace*{0pt}\\ -\hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\ -\hspace*{0pt}remove1 x [] = [];\\ -\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\ -\hspace*{0pt}\\ -\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\ -\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\ -\hspace*{0pt}\\ -\hspace*{0pt}{\char125}% +\begin{typewriter} + module\ Example\ where\ {\isacharbraceleft}\isanewline +\isanewline +newtype\ Dlist\ a\ {\isacharequal}\ Dlist\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline +\isanewline +empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a{\isacharsemicolon}\isanewline +empty\ {\isacharequal}\ Dlist\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline +\isanewline +member\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Bool{\isacharsemicolon}\isanewline +member\ {\isacharbrackleft}{\isacharbrackright}\ y\ {\isacharequal}\ False{\isacharsemicolon}\isanewline +member\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ y\ {\isacharequal}\ x\ {\isacharequal}{\isacharequal}\ y\ {\isacharbar}{\isacharbar}\ member\ xs\ y{\isacharsemicolon}\isanewline +\isanewline +insert\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline +insert\ x\ xs\ {\isacharequal}\ {\isacharparenleft}if\ member\ xs\ x\ then\ xs\ else\ x\ {\isacharcolon}\ xs{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline +list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharparenleft}Dlist\ x{\isacharparenright}\ {\isacharequal}\ x{\isacharsemicolon}\isanewline +\isanewline +inserta\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline +inserta\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}insert\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +remove{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline +remove{\isadigit{1}}\ x\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline +remove{\isadigit{1}}\ x\ {\isacharparenleft}y\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isacharequal}{\isacharequal}\ y\ then\ xs\ else\ y\ {\isacharcolon}\ remove{\isadigit{1}}\ x\ xs{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +remove\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline +remove\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isanewline +{\isacharbraceright}\isanewline + + \end{typewriter}% \end{isamarkuptext}% \isamarkuptrue% % diff -r 5096018d5359 -r 0afaf89ab591 doc-src/Codegen/style.sty --- a/doc-src/Codegen/style.sty Thu Sep 23 13:28:53 2010 +0200 +++ b/doc-src/Codegen/style.sty Thu Sep 23 15:46:17 2010 +0200 @@ -26,9 +26,15 @@ \renewcommand{\endisatagquote}{\end{quote}} \newcommand{\quotebreak}{\\[1.2ex]} +%% typewriter text +\newenvironment{typewriter}{\renewcommand{\isadigit}[1]{{##1}}% +\def\isacharunderscore{\_}% +\parindent0pt\fontsize{9pt}{0pt}% +\tt\setlength{\baselineskip}{8pt}\renewcommand{\baselinestretch}{1}}{} + \isakeeptag{quotett} \renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle} -\renewcommand{\endisatagquotett}{\end{quote}\isabellestyle{it}\isastyle} +\renewcommand{\endisatagquotett}{\end{quote}} %% a trick \newcommand{\isasymSML}{SML}