0 | ||| Bounded Queues
  1 | module Data.BoundedQueue.Unsized
  2 |
  3 | import Data.BoundedQueue.Unsized.Internal
  4 |
  5 | import Data.Seq.Unsized
  6 | import Derive.Prelude
  7 |
  8 | %language ElabReflection
  9 |
 10 | %default total
 11 |
 12 | ||| The empty `BoundedQueue`. O(1)
 13 | export
 14 | empty :  Nat
 15 |       -> BoundedQueue a
 16 | empty l =
 17 |   MkBoundedQueue empty
 18 |                  l
 19 |                  0
 20 |
 21 | ||| Is the `BoundedQueue` empty? O(1)
 22 | export
 23 | null :  BoundedQueue a
 24 |      -> Bool
 25 | null (MkBoundedQueue _ _ 0) =
 26 |   True
 27 | null _                      =
 28 |   False
 29 |
 30 | ||| Naively keeps the first `n` values of a list, and converts
 31 | ||| into a `BoundedQueue` (keeps the order of the elements). O(1)
 32 | export
 33 | fromList :  Nat
 34 |          -> List a
 35 |          -> BoundedQueue a
 36 | fromList n vs =
 37 |   let vs' = take n vs
 38 |     in MkBoundedQueue (fromList vs')
 39 |                       n
 40 |                       (length vs')
 41 |
 42 | ||| Naively keeps the first `n` values of a `SnocList`, and converts
 43 | ||| into a `BoundedQueue` (keeps the order of the elements). O(1)
 44 | export
 45 | fromSnocList :  Nat
 46 |              -> SnocList a
 47 |              -> BoundedQueue a
 48 | fromSnocList n sv =
 49 |   let sv' = take n $ cast sv
 50 |     in MkBoundedQueue (fromList sv')
 51 |                       n
 52 |                       (length sv')
 53 |
 54 | ||| Converts a `BoundedQueue` to a `List`, keeping the order
 55 | ||| of elements. O(n)
 56 | export
 57 | toList :  BoundedQueue a
 58 |        -> List a
 59 | toList (MkBoundedQueue queue _ _) =
 60 |   toList queue
 61 |
 62 | ||| Converts a `BoundedQueue` to a `SnocList`, keeping the order
 63 | ||| of elements. O(n)
 64 | export
 65 | toSnocList :  BoundedQueue a
 66 |            -> SnocList a
 67 | toSnocList (MkBoundedQueue queue _ _) =
 68 |   cast $ toList queue
 69 |
 70 | ||| Append a value at the back of the `BoundedQueue`. O(1)
 71 | export
 72 | enqueue :  BoundedQueue a
 73 |         -> a
 74 |         -> BoundedQueue a
 75 | enqueue (MkBoundedQueue queue queuelimit queuesize) v =
 76 |   case queuelimit == queuesize of
 77 |     True  =>
 78 |       case viewl queue of
 79 |         Nothing          =>
 80 |           MkBoundedQueue queue
 81 |                          queuelimit
 82 |                          queuesize
 83 |         Just (_, queue') =>
 84 |           MkBoundedQueue (queue' `snoc` v)
 85 |                          queuelimit
 86 |                          queuesize
 87 |     False =>
 88 |       MkBoundedQueue (queue `snoc` v)
 89 |                      queuelimit
 90 |                      (queuesize `plus` 1)
 91 |
 92 | ||| Take a value from the front of the `BoundedQueue`. O(1)
 93 | export
 94 | dequeue :  BoundedQueue a
 95 |         -> Maybe (a, BoundedQueue a)
 96 | dequeue (MkBoundedQueue queue queuelimit queuesize) =
 97 |   case viewl queue of
 98 |     Nothing          =>
 99 |       Nothing
100 |     Just (h, queue') =>
101 |       Just (h, MkBoundedQueue queue'
102 |                               queuelimit
103 |                               (queuesize `minus` 1)
104 |            )
105 |
106 | ||| We can prepend an element to our `BoundedQueue`, making it the new
107 | ||| "oldest" element. O(1)
108 | |||
109 | ||| This is against the typical use case for a FIFO data
110 | ||| structure, but it allows us to conveniently implement
111 | ||| `peekOldest`.
112 | export
113 | prepend :  a
114 |         -> BoundedQueue a
115 |         -> BoundedQueue a
116 | prepend x (MkBoundedQueue queue queuelimit queuesize) =
117 |   case queuelimit == queuesize of
118 |     True  =>
119 |       case viewl queue of
120 |         Nothing          =>
121 |           MkBoundedQueue queue
122 |                          queuelimit
123 |                          queuesize
124 |         Just (_, queue') =>
125 |           MkBoundedQueue (x `cons` queue')
126 |                          queuelimit
127 |                          queuesize
128 |     False =>
129 |       MkBoundedQueue (x `cons` queue)
130 |                      queuelimit
131 |                      (queuesize `plus` 1)
132 |
133 | ||| Return the last element of the `BoundedQueue`, plus the unmodified
134 | ||| queue.
135 | |||
136 | ||| Note: `peekOldest` might involve a rearrangement of the elements
137 | |||       just like `dequeue`. In order to keep our amortized O(1)
138 | |||       runtime behavior, the newly arranged queue should be used
139 | |||       henceforth.
140 | export
141 | peekOldest :  BoundedQueue a
142 |            -> Maybe (a, BoundedQueue a)
143 | peekOldest q =
144 |   case dequeue q of
145 |     Just (v, MkBoundedQueue queue
146 |                             queuelimit
147 |                             queuesize
148 |          )  =>
149 |       Just (v, MkBoundedQueue (v `cons` queue)
150 |                               queuelimit
151 |                               (queuesize `plus` 1)
152 |            )
153 |     Nothing =>
154 |       Nothing
155 |
156 | ||| Appends two `BoundedQueues`. O(m + n)
157 | export
158 | (++) :  BoundedQueue a
159 |      -> BoundedQueue a
160 |      -> BoundedQueue a
161 | (MkBoundedQueue queue1 queuelimit1 queuesize1) ++ (MkBoundedQueue queue2 queuelimit2 queuesize2) =
162 |   MkBoundedQueue (queue1 ++ queue2)
163 |                  (queuelimit1 `plus` queuelimit2)
164 |                  (queuesize1 `plus` queuesize2)
165 |
166 | ||| Returns the length of the `BoundedQueue`. O(1).
167 | export
168 | length :  BoundedQueue a
169 |        -> Nat
170 | length (MkBoundedQueue _ _ queuesize) =
171 |   queuesize
172 |
173 | --------------------------------------------------------------------------------
174 | --          Interfaces
175 | --------------------------------------------------------------------------------
176 |
177 | export
178 | Semigroup (BoundedQueue a) where
179 |   (<+>) = (++)
180 |
181 | export
182 | Monoid (BoundedQueue a) where
183 |   neutral = empty 0
184 |
185 | export
186 | Functor BoundedQueue where
187 |   map f (MkBoundedQueue queue queuelimit queuesize) =
188 |     MkBoundedQueue (map f queue)
189 |                    queuelimit
190 |                    queuesize
191 |