168 \endisadelimquote |
168 \endisadelimquote |
169 % |
169 % |
170 \isatagquote |
170 \isatagquote |
171 % |
171 % |
172 \begin{isamarkuptext}% |
172 \begin{isamarkuptext}% |
173 \isatypewriter% |
173 \begin{typewriter} |
174 \noindent% |
174 fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline |
175 \hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\ |
175 fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ let\ {\isacharbraceleft}\isanewline |
176 \hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\ |
176 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n{\isacharsemicolon}\isanewline |
177 \hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\ |
177 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceright}\ in\ {\isacharparenleft}plus{\isacharunderscore}nat\ m\ q{\isacharcomma}\ m{\isacharparenright}{\isacharsemicolon}\isanewline |
178 \hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\ |
178 fib{\isacharunderscore}step\ Zero{\isacharunderscore}nat\ {\isacharequal}\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharsemicolon}\isanewline |
179 \hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\ |
179 \isanewline |
180 \hspace*{0pt}\\ |
180 fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline |
181 \hspace*{0pt}fib ::~Nat -> Nat;\\ |
181 fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isacharsemicolon}\isanewline |
182 \hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\ |
182 fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon} |
183 \hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;% |
183 \end{typewriter}% |
184 \end{isamarkuptext}% |
184 \end{isamarkuptext}% |
185 \isamarkuptrue% |
185 \isamarkuptrue% |
186 % |
186 % |
187 \endisatagquote |
187 \endisatagquote |
188 {\isafoldquote}% |
188 {\isafoldquote}% |
346 \endisadelimquote |
346 \endisadelimquote |
347 % |
347 % |
348 \isatagquote |
348 \isatagquote |
349 % |
349 % |
350 \begin{isamarkuptext}% |
350 \begin{isamarkuptext}% |
351 \isatypewriter% |
351 \begin{typewriter} |
352 \noindent% |
352 structure\ Example\ {\isacharcolon}\ sig\isanewline |
353 \hspace*{0pt}structure Example :~sig\\ |
353 \ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline |
354 \hspace*{0pt} ~val id :~'a -> 'a\\ |
354 \ \ 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 |
355 \hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\ |
355 \ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline |
356 \hspace*{0pt} ~val rev :~'a list -> 'a list\\ |
356 \ \ val\ null\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ bool\isanewline |
357 \hspace*{0pt} ~val null :~'a list -> bool\\ |
357 \ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline |
358 \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ |
358 \ \ val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\isanewline |
359 \hspace*{0pt} ~val empty :~'a queue\\ |
359 \ \ val\ dequeue\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ option\ {\isacharasterisk}\ {\isacharprime}a\ queue\isanewline |
360 \hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\ |
360 \ \ val\ enqueue\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\isanewline |
361 \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\ |
361 end\ {\isacharequal}\ struct\isanewline |
362 \hspace*{0pt}end = struct\\ |
362 \isanewline |
363 \hspace*{0pt}\\ |
363 fun\ id\ x\ {\isacharequal}\ {\isacharparenleft}fn\ xa\ {\isacharequal}{\isachargreater}\ xa{\isacharparenright}\ x{\isacharsemicolon}\isanewline |
364 \hspace*{0pt}fun id x = (fn xa => xa) x;\\ |
364 \isanewline |
365 \hspace*{0pt}\\ |
365 fun\ fold\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id\isanewline |
366 \hspace*{0pt}fun fold f [] = id\\ |
366 \ \ {\isacharbar}\ fold\ f\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ fold\ f\ xs\ o\ f\ x{\isacharsemicolon}\isanewline |
367 \hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\ |
367 \isanewline |
368 \hspace*{0pt}\\ |
368 fun\ rev\ xs\ {\isacharequal}\ fold\ {\isacharparenleft}fn\ a\ {\isacharequal}{\isachargreater}\ fn\ b\ {\isacharequal}{\isachargreater}\ a\ {\isacharcolon}{\isacharcolon}\ b{\isacharparenright}\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline |
369 \hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\ |
369 \isanewline |
370 \hspace*{0pt}\\ |
370 fun\ null\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ true\isanewline |
371 \hspace*{0pt}fun null [] = true\\ |
371 \ \ {\isacharbar}\ null\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ false{\isacharsemicolon}\isanewline |
372 \hspace*{0pt} ~| null (x ::~xs) = false;\\ |
372 \isanewline |
373 \hspace*{0pt}\\ |
373 datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list{\isacharsemicolon}\isanewline |
374 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ |
374 \isanewline |
375 \hspace*{0pt}\\ |
375 val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline |
376 \hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ |
376 \isanewline |
377 \hspace*{0pt}\\ |
377 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 |
378 \hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ |
378 \ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
379 \hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\ |
379 \ \ \ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
380 \hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\ |
380 \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
381 \hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\ |
381 \isanewline |
382 \hspace*{0pt}\\ |
382 fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline |
383 \hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ |
383 \isanewline |
384 \hspace*{0pt}\\ |
384 end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline |
385 \hspace*{0pt}end;~(*struct Example*)% |
385 |
|
386 \end{typewriter}% |
386 \end{isamarkuptext}% |
387 \end{isamarkuptext}% |
387 \isamarkuptrue% |
388 \isamarkuptrue% |
388 % |
389 % |
389 \endisatagquote |
390 \endisatagquote |
390 {\isafoldquote}% |
391 {\isafoldquote}% |
582 \endisadelimquote |
583 \endisadelimquote |
583 % |
584 % |
584 \isatagquote |
585 \isatagquote |
585 % |
586 % |
586 \begin{isamarkuptext}% |
587 \begin{isamarkuptext}% |
587 \isatypewriter% |
588 \begin{typewriter} |
588 \noindent% |
589 module\ Example\ where\ {\isacharbraceleft}\isanewline |
589 \hspace*{0pt}module Example where {\char123}\\ |
590 \isanewline |
590 \hspace*{0pt}\\ |
591 newtype\ Dlist\ a\ {\isacharequal}\ Dlist\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline |
591 \hspace*{0pt}newtype Dlist a = Dlist [a];\\ |
592 \isanewline |
592 \hspace*{0pt}\\ |
593 empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a{\isacharsemicolon}\isanewline |
593 \hspace*{0pt}empty ::~forall a.~Dlist a;\\ |
594 empty\ {\isacharequal}\ Dlist\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline |
594 \hspace*{0pt}empty = Dlist [];\\ |
595 \isanewline |
595 \hspace*{0pt}\\ |
596 member\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Bool{\isacharsemicolon}\isanewline |
596 \hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\ |
597 member\ {\isacharbrackleft}{\isacharbrackright}\ y\ {\isacharequal}\ False{\isacharsemicolon}\isanewline |
597 \hspace*{0pt}member [] y = False;\\ |
598 member\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ y\ {\isacharequal}\ x\ {\isacharequal}{\isacharequal}\ y\ {\isacharbar}{\isacharbar}\ member\ xs\ y{\isacharsemicolon}\isanewline |
598 \hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\ |
599 \isanewline |
599 \hspace*{0pt}\\ |
600 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 |
600 \hspace*{0pt}insert ::~forall a.~(Eq a) => a -> [a] -> [a];\\ |
601 insert\ x\ xs\ {\isacharequal}\ {\isacharparenleft}if\ member\ xs\ x\ then\ xs\ else\ x\ {\isacharcolon}\ xs{\isacharparenright}{\isacharsemicolon}\isanewline |
601 \hspace*{0pt}insert x xs = (if member xs x then xs else x :~xs);\\ |
602 \isanewline |
602 \hspace*{0pt}\\ |
603 list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline |
603 \hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\ |
604 list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharparenleft}Dlist\ x{\isacharparenright}\ {\isacharequal}\ x{\isacharsemicolon}\isanewline |
604 \hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\ |
605 \isanewline |
605 \hspace*{0pt}\\ |
606 inserta\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline |
606 \hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\ |
607 inserta\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}insert\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
607 \hspace*{0pt}inserta x dxs = Dlist (insert x (list{\char95}of{\char95}dlist dxs));\\ |
608 \isanewline |
608 \hspace*{0pt}\\ |
609 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 |
609 \hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\ |
610 remove{\isadigit{1}}\ x\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline |
610 \hspace*{0pt}remove1 x [] = [];\\ |
611 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 |
611 \hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\ |
612 \isanewline |
612 \hspace*{0pt}\\ |
613 remove\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline |
613 \hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\ |
614 remove\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
614 \hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\ |
615 \isanewline |
615 \hspace*{0pt}\\ |
616 {\isacharbraceright}\isanewline |
616 \hspace*{0pt}{\char125}% |
617 |
|
618 \end{typewriter}% |
617 \end{isamarkuptext}% |
619 \end{isamarkuptext}% |
618 \isamarkuptrue% |
620 \isamarkuptrue% |
619 % |
621 % |
620 \endisatagquote |
622 \endisatagquote |
621 {\isafoldquote}% |
623 {\isafoldquote}% |