55 % |
55 % |
56 \isatagquoteme |
56 \isatagquoteme |
57 \isacommand{lemma}\isamarkupfalse% |
57 \isacommand{lemma}\isamarkupfalse% |
58 \ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline |
58 \ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline |
59 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
59 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline |
60 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
60 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline |
|
61 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
61 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
62 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
62 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
63 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
63 \ \ \isacommand{by}\isamarkupfalse% |
64 \ \ \isacommand{by}\isamarkupfalse% |
64 \ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% |
65 \ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% |
65 \endisatagquoteme |
66 \endisatagquoteme |
84 \isatagquoteme |
85 \isatagquoteme |
85 % |
86 % |
86 \begin{isamarkuptext}% |
87 \begin{isamarkuptext}% |
87 \isaverbatim% |
88 \isaverbatim% |
88 \noindent% |
89 \noindent% |
89 \verb|module Example where {|\newline% |
|
90 \newline% |
|
91 \newline% |
|
92 \verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline% |
|
93 \verb|foldla f a [] = a;|\newline% |
|
94 \verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline% |
|
95 \newline% |
|
96 \verb|rev :: forall a. [a] -> [a];|\newline% |
|
97 \verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline% |
|
98 \newline% |
|
99 \verb|nulla :: forall a. [a] -> Bool;|\newline% |
|
100 \verb|nulla (x : xs) = False;|\newline% |
|
101 \verb|nulla [] = True;|\newline% |
|
102 \newline% |
|
103 \verb|data Queue a = Queue [a] [a];|\newline% |
|
104 \newline% |
|
105 \verb|empty :: forall a. Queue a;|\newline% |
|
106 \verb|empty = Queue [] [];|\newline% |
|
107 \newline% |
|
108 \verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline% |
90 \verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline% |
109 \verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline% |
91 \verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline% |
110 \verb|dequeue (Queue xs []) =|\newline% |
92 \verb|dequeue (Queue xs []) =|\newline% |
111 \verb| (if nulla xs then (Nothing, Queue [] [])|\newline% |
93 \verb| (if nulla xs then (Nothing, Queue [] [])|\newline% |
112 \verb| else dequeue (Queue [] (rev xs)));|\newline% |
94 \verb| else dequeue (Queue [] (rev xs)));|% |
113 \newline% |
|
114 \verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline% |
|
115 \verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline% |
|
116 \newline% |
|
117 \verb|}|% |
|
118 \end{isamarkuptext}% |
95 \end{isamarkuptext}% |
119 \isamarkuptrue% |
96 \isamarkuptrue% |
120 % |
97 % |
121 \endisatagquoteme |
98 \endisatagquoteme |
122 {\isafoldquoteme}% |
99 {\isafoldquoteme}% |