229 \noindent% |
229 \noindent% |
230 \hspace*{0pt}module Example where {\char123}\\ |
230 \hspace*{0pt}module Example where {\char123}\\ |
231 \hspace*{0pt}\\ |
231 \hspace*{0pt}\\ |
232 \hspace*{0pt}data Queue a = AQueue [a] [a];\\ |
232 \hspace*{0pt}data Queue a = AQueue [a] [a];\\ |
233 \hspace*{0pt}\\ |
233 \hspace*{0pt}\\ |
234 \hspace*{0pt}empty ::~forall a.~Queue a;\\ |
234 \hspace*{0pt}empty ::~forall a.~Example.Queue a;\\ |
235 \hspace*{0pt}empty = AQueue [] [];\\ |
235 \hspace*{0pt}empty = Example.AQueue [] [];\\ |
236 \hspace*{0pt}\\ |
236 \hspace*{0pt}\\ |
237 \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ |
237 \hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\ |
238 \hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\ |
238 \hspace*{0pt}dequeue (Example.AQueue [] []) = (Nothing,~Example.AQueue [] []);\\ |
239 \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ |
239 \hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\ |
240 \hspace*{0pt}dequeue (AQueue (v :~va) []) =\\ |
240 \hspace*{0pt}dequeue (Example.AQueue (v :~va) []) =\\ |
241 \hspace*{0pt} ~let {\char123}\\ |
241 \hspace*{0pt} ~let {\char123}\\ |
242 \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\ |
242 \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\ |
243 \hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\ |
243 \hspace*{0pt} ~{\char125}~in (Just y,~Example.AQueue [] ys);\\ |
244 \hspace*{0pt}\\ |
244 \hspace*{0pt}\\ |
245 \hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ |
245 \hspace*{0pt}enqueue ::~forall a.~a -> Example.Queue a -> Example.Queue a;\\ |
246 \hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\ |
246 \hspace*{0pt}enqueue x (Example.AQueue xs ys) = Example.AQueue (x :~xs) ys;\\ |
247 \hspace*{0pt}\\ |
247 \hspace*{0pt}\\ |
248 \hspace*{0pt}{\char125}% |
248 \hspace*{0pt}{\char125}% |
249 \end{isamarkuptext}% |
249 \end{isamarkuptext}% |
250 \isamarkuptrue% |
250 \isamarkuptrue% |
251 % |
251 % |
395 \begin{isamarkuptext}% |
395 \begin{isamarkuptext}% |
396 \isatypewriter% |
396 \isatypewriter% |
397 \noindent% |
397 \noindent% |
398 \hspace*{0pt}module Example where {\char123}\\ |
398 \hspace*{0pt}module Example where {\char123}\\ |
399 \hspace*{0pt}\\ |
399 \hspace*{0pt}\\ |
400 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ |
400 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\ |
401 \hspace*{0pt}\\ |
401 \hspace*{0pt}\\ |
402 \hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ |
402 \hspace*{0pt}plus{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\ |
403 \hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ |
403 \hspace*{0pt}plus{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat m (Example.Suc n);\\ |
404 \hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ |
404 \hspace*{0pt}plus{\char95}nat Example.Zero{\char95}nat n = n;\\ |
405 \hspace*{0pt}\\ |
405 \hspace*{0pt}\\ |
406 \hspace*{0pt}class Semigroup a where {\char123}\\ |
406 \hspace*{0pt}class Semigroup a where {\char123}\\ |
407 \hspace*{0pt} ~mult ::~a -> a -> a;\\ |
407 \hspace*{0pt} ~mult ::~a -> a -> a;\\ |
408 \hspace*{0pt}{\char125};\\ |
408 \hspace*{0pt}{\char125};\\ |
409 \hspace*{0pt}\\ |
409 \hspace*{0pt}\\ |
410 \hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ |
410 \hspace*{0pt}class (Example.Semigroup a) => Monoid a where {\char123}\\ |
411 \hspace*{0pt} ~neutral ::~a;\\ |
411 \hspace*{0pt} ~neutral ::~a;\\ |
412 \hspace*{0pt}{\char125};\\ |
412 \hspace*{0pt}{\char125};\\ |
413 \hspace*{0pt}\\ |
413 \hspace*{0pt}\\ |
414 \hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ |
414 \hspace*{0pt}pow ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\ |
415 \hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ |
415 \hspace*{0pt}pow Example.Zero{\char95}nat a = Example.neutral;\\ |
416 \hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ |
416 \hspace*{0pt}pow (Example.Suc n) a = Example.mult a (Example.pow n a);\\ |
417 \hspace*{0pt}\\ |
417 \hspace*{0pt}\\ |
418 \hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ |
418 \hspace*{0pt}mult{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\ |
419 \hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ |
419 \hspace*{0pt}mult{\char95}nat Example.Zero{\char95}nat n = Example.Zero{\char95}nat;\\ |
420 \hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
420 \hspace*{0pt}mult{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat n (Example.mult{\char95}nat m n);\\ |
421 \hspace*{0pt}\\ |
421 \hspace*{0pt}\\ |
422 \hspace*{0pt}neutral{\char95}nat ::~Nat;\\ |
422 \hspace*{0pt}neutral{\char95}nat ::~Example.Nat;\\ |
423 \hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ |
423 \hspace*{0pt}neutral{\char95}nat = Example.Suc Example.Zero{\char95}nat;\\ |
424 \hspace*{0pt}\\ |
424 \hspace*{0pt}\\ |
425 \hspace*{0pt}instance Semigroup Nat where {\char123}\\ |
425 \hspace*{0pt}instance Example.Semigroup Example.Nat where {\char123}\\ |
426 \hspace*{0pt} ~mult = mult{\char95}nat;\\ |
426 \hspace*{0pt} ~mult = Example.mult{\char95}nat;\\ |
427 \hspace*{0pt}{\char125};\\ |
427 \hspace*{0pt}{\char125};\\ |
428 \hspace*{0pt}\\ |
428 \hspace*{0pt}\\ |
429 \hspace*{0pt}instance Monoid Nat where {\char123}\\ |
429 \hspace*{0pt}instance Example.Monoid Example.Nat where {\char123}\\ |
430 \hspace*{0pt} ~neutral = neutral{\char95}nat;\\ |
430 \hspace*{0pt} ~neutral = Example.neutral{\char95}nat;\\ |
431 \hspace*{0pt}{\char125};\\ |
431 \hspace*{0pt}{\char125};\\ |
432 \hspace*{0pt}\\ |
432 \hspace*{0pt}\\ |
433 \hspace*{0pt}bexp ::~Nat -> Nat;\\ |
433 \hspace*{0pt}bexp ::~Example.Nat -> Example.Nat;\\ |
434 \hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ |
434 \hspace*{0pt}bexp n = Example.pow n (Example.Suc (Example.Suc Example.Zero{\char95}nat));\\ |
435 \hspace*{0pt}\\ |
435 \hspace*{0pt}\\ |
436 \hspace*{0pt}{\char125}% |
436 \hspace*{0pt}{\char125}% |
437 \end{isamarkuptext}% |
437 \end{isamarkuptext}% |
438 \isamarkuptrue% |
438 \isamarkuptrue% |
439 % |
439 % |
468 \hspace*{0pt} ~type 'a monoid\\ |
468 \hspace*{0pt} ~type 'a monoid\\ |
469 \hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\ |
469 \hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\ |
470 \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ |
470 \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ |
471 \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ |
471 \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ |
472 \hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ |
472 \hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ |
|
473 \hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ |
473 \hspace*{0pt} ~val neutral{\char95}nat :~nat\\ |
474 \hspace*{0pt} ~val neutral{\char95}nat :~nat\\ |
474 \hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ |
|
475 \hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ |
475 \hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ |
476 \hspace*{0pt} ~val bexp :~nat -> nat\\ |
476 \hspace*{0pt} ~val bexp :~nat -> nat\\ |
477 \hspace*{0pt}end = struct\\ |
477 \hspace*{0pt}end = struct\\ |
478 \hspace*{0pt}\\ |
478 \hspace*{0pt}\\ |
479 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
479 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
492 \hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ |
492 \hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ |
493 \hspace*{0pt}\\ |
493 \hspace*{0pt}\\ |
494 \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ |
494 \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ |
495 \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
495 \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ |
496 \hspace*{0pt}\\ |
496 \hspace*{0pt}\\ |
|
497 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ |
|
498 \hspace*{0pt}\\ |
497 \hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ |
499 \hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ |
498 \hspace*{0pt}\\ |
|
499 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ |
|
500 \hspace*{0pt}\\ |
500 \hspace*{0pt}\\ |
501 \hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ |
501 \hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ |
502 \hspace*{0pt} ~:~nat monoid;\\ |
502 \hspace*{0pt} ~:~nat monoid;\\ |
503 \hspace*{0pt}\\ |
503 \hspace*{0pt}\\ |
504 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ |
504 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ |