0 | ||| Immutable FIFO Queues
  1 | module Data.Queue
  2 |
  3 | import Derive.Prelude
  4 |
  5 | %language ElabReflection
  6 |
  7 | %default total
  8 |
  9 | ||| An immutable first-in first-out structure with amortized
 10 | ||| O(1) enqueue and dequeue operations.
 11 | export
 12 | record Queue a where
 13 |   constructor Q
 14 |   front : List a
 15 |   back  : SnocList a
 16 |
 17 | ||| The empty `Queue`. O(1)
 18 | export %inline
 19 | empty : Queue a
 20 | empty = Q [] [<]
 21 |
 22 | ||| Converts a list to a `Queue`, keeping the order of
 23 | ||| elements. O(1)
 24 | export %inline
 25 | fromList : List a -> Queue a
 26 | fromList vs = Q vs [<]
 27 |
 28 | ||| Converts a `SnocList` to a `Queue`, keeping the order of
 29 | ||| elements. O(1)
 30 | export %inline
 31 | fromSnocList : SnocList a -> Queue a
 32 | fromSnocList sv = Q [] sv
 33 |
 34 | ||| Converts a `Queue` to a `SnocList`, keeping the order
 35 | ||| of elements. O(n)
 36 | export %inline
 37 | toSnocList : Queue a -> SnocList a
 38 | toSnocList (Q f b) = b <>< f
 39 |
 40 | ||| Append a value at the back of the `Queue`. O(1)
 41 | export
 42 | enqueue : Queue a -> a -> Queue a
 43 | enqueue (Q f b) v = Q f (b :< v)
 44 |
 45 | ||| Append a list of values at the back of the `Queue`. O(1)
 46 | export
 47 | enqueueAll : Queue a -> List a -> Queue a
 48 | enqueueAll (Q f b) vs = Q f (b <>< vs)
 49 |
 50 | ||| Take a value from the front of the `Queue`.
 51 | |||
 52 | ||| In case of the front being empty, this transfers
 53 | ||| the back to the front, which runs in O(n). However,
 54 | ||| every element in the `Queue` is thus shifted at most
 55 | ||| once before being dequeued, so this runs in amortized
 56 | ||| O(1).
 57 | export
 58 | dequeue : Queue a -> Maybe (a, Queue a)
 59 | dequeue (Q front back) =
 60 |   case front of
 61 |     h::t => Just (h, Q t back)
 62 |     []   =>
 63 |       case back <>> [] of
 64 |         h::t => Just (h, Q t [<])
 65 |         []   => Nothing
 66 |
 67 | ||| We can prepend an element to our `Queue`, making it the new
 68 | ||| "oldest" element. O(1)
 69 | |||
 70 | ||| This is against the typical use case for a FIFO data
 71 | ||| structure, but it allows us to conveniently implement
 72 | ||| `peekOldest`.
 73 | export
 74 | prepend : a -> Queue a -> Queue a
 75 | prepend x (Q f b) = Q (x::f) b
 76 |
 77 | ||| Return the last element of the `Queue`, plus the unmodified
 78 | ||| `Queue`.
 79 | |||
 80 | ||| Note: `peekOldest` might involve a rearrangement of the elements
 81 | |||       just like `dequeue`. In order to keep our amortized O(1)
 82 | |||       runtime behavior, the newly arranged `Queue` should be used
 83 | |||       henceforth.
 84 | export
 85 | peekOldest : Queue a -> Maybe (a, Queue a)
 86 | peekOldest q =
 87 |   case dequeue q of
 88 |     Just (v,Q f b) => Just (v, Q (v::f) b)
 89 |     Nothing     => Nothing
 90 |
 91 | ||| Appends two `Queue`s. O(m + n)
 92 | export
 93 | (++) : Queue a -> Queue a -> Queue a
 94 | Q f1 b1 ++ Q f2 b2 = Q (f1 ++ (b1 <>> f2)) b2
 95 |
 96 | ||| Returns the length of the `Queue`. O(n).
 97 | export
 98 | length : Queue a -> Nat
 99 | length (Q f b) = length f + length b
100 |
101 | ||| Keeps only those values in a queue for which the given predicate
102 | ||| returns `True`.
103 | export
104 | filter : (a -> Bool) -> Queue a -> Queue a
105 | filter f (Q front back) = Q (filter f front) (filter f back)
106 |
107 | ||| Maps the values in a queue, keeping only those for which the given
108 | ||| function returns a `Just`.
109 | export
110 | mapMaybe : (a -> Maybe b) -> Queue a -> Queue b
111 | mapMaybe f (Q front back) = Q (mapMaybe f front) (mapMaybe f back)
112 |
113 | --------------------------------------------------------------------------------
114 | --          Interfaces
115 | --------------------------------------------------------------------------------
116 |
117 | %runElab derive "Queue" [Show,Eq]
118 |
119 | export %inline
120 | Semigroup (Queue a) where
121 |   (<+>) = (++)
122 |
123 | export %inline
124 | Monoid (Queue a) where
125 |   neutral = empty
126 |
127 | export
128 | Functor Queue where
129 |   map f (Q front back) = Q (map f front) (map f back)
130 |
131 | export
132 | Foldable Queue where
133 |   toList (Q f b) = b <>> f
134 |   foldr f acc = foldr f acc . toSnocList
135 |   foldl f acc = foldl f acc . toList
136 |   foldMap f = foldMap f . toList
137 |   foldlM f acc = foldlM f acc . toList
138 |   null (Q f b) = null f || null b
139 |
140 | export
141 | Traversable Queue where
142 |   traverse f (Q front back) = [| Q (traverse f front) (traverse f back) |]
143 |