0 | ||| General purpose two-end finite sequences.
  1 | |||
  2 | ||| This is implemented by finger tree.
  3 | module Data.Seq.Unsized
  4 |
  5 | import Control.WellFounded
  6 | import public Data.Zippable
  7 |
  8 | import Data.Seq.Internal
  9 |
 10 | %default total
 11 |
 12 | ||| A two-end finite sequence.
 13 | export
 14 | data Seq : Type -> Type where
 15 |   MkSeq :  FingerTree (Elem e)
 16 |         -> Seq e
 17 |
 18 | ||| O(1). The empty sequence.
 19 | export
 20 | empty : Seq e
 21 | empty =
 22 |   MkSeq Empty
 23 |
 24 | ||| O(1). A singleton sequence.
 25 | export
 26 | singleton :  e
 27 |           -> Seq e
 28 | singleton a =
 29 |   MkSeq (Single (MkElem a))
 30 |
 31 | ||| O(n). A sequence of length n with a the value of every element.
 32 | export
 33 | replicate :  (n : Nat)
 34 |           -> (a : e)
 35 |           -> Seq e
 36 | replicate n a =
 37 |   MkSeq (replicate' n a)
 38 |
 39 | ||| O(1). The number of elements in the sequence.
 40 | export
 41 | length :  Seq a
 42 |        -> Nat
 43 | length (MkSeq tr) =
 44 |   length' tr
 45 |
 46 | ||| O(n). Reverse the sequence.
 47 | export
 48 | reverse :  Seq a
 49 |         -> Seq a
 50 | reverse (MkSeq tr) =
 51 |   MkSeq (reverseTree id tr)
 52 |
 53 | export infixr 5 `cons`
 54 | ||| O(1). Add an element to the left end of a sequence.
 55 | export
 56 | cons :  e
 57 |      -> Seq e
 58 |      -> Seq e
 59 | a `cons` MkSeq tr =
 60 |   MkSeq (MkElem a `consTree` tr)
 61 |
 62 | export infixl 5 `snoc`
 63 | ||| O(1). Add an element to the right end of a sequence.
 64 | export
 65 | snoc :  Seq e
 66 |      -> e
 67 |      -> Seq e
 68 | MkSeq tr `snoc` a =
 69 |   MkSeq (tr `snocTree` MkElem a)
 70 |
 71 | ||| O(log(min(m, n))). Concatenate two sequences.
 72 | export
 73 | (++) :  Seq e
 74 |      -> Seq e
 75 |      -> Seq e
 76 | MkSeq t1 ++ MkSeq t2 =
 77 |   MkSeq (addTree0 t1 t2)
 78 |
 79 | ||| O(1). View from the left of the sequence.
 80 | export
 81 | viewl :  Seq a
 82 |       -> Maybe (a, Seq a)
 83 | viewl (MkSeq tr) =
 84 |   case viewLTree tr of
 85 |     Just (MkElem a, tr') =>
 86 |       Just (a, MkSeq tr')
 87 |     Nothing              =>
 88 |       Nothing
 89 |
 90 | ||| O(1). The first element of the sequence.
 91 | export
 92 | head :  Seq a
 93 |      -> Maybe a
 94 | head s =
 95 |   fst <$> viewl s
 96 |
 97 | ||| O(1). The elements after the head of the sequence.
 98 | ||| Returns an empty sequence when the sequence is empty.
 99 | export
100 | tail :  Seq a
101 |      -> Seq a
102 | tail s =
103 |   case viewl s of
104 |     Just (_, s') =>
105 |       s'
106 |     Nothing      =>
107 |       empty
108 |
109 | ||| O(1). View from the right of the sequence.
110 | export
111 | viewr :  Seq a
112 |       -> Maybe (Seq a, a)
113 | viewr (MkSeq tr) =
114 |   case viewRTree tr of
115 |     Just (tr', MkElem a) =>
116 |       Just (MkSeq tr', a)
117 |     Nothing              =>
118 |       Nothing
119 |
120 | ||| O(1). The elements before the last element of the sequence.
121 | ||| Returns an empty sequence when the sequence is empty.
122 | export
123 | init :  Seq a
124 |      -> Seq a
125 | init s =
126 |   case viewr s of
127 |     Just (s', _) =>
128 |       s'
129 |     Nothing      =>
130 |       empty
131 |
132 | ||| O(1). The last element of the sequence.
133 | export
134 | last :  Seq a
135 |      -> Maybe a
136 | last s =
137 |   snd <$> viewr s
138 |
139 | ||| O(n). Turn a list into a sequence.
140 | export
141 | fromList :  List a
142 |          -> Seq a
143 | fromList xs =
144 |   MkSeq (foldr (\x, t => MkElem x `consTree` t) Empty xs)
145 |
146 | ||| O(log(min(i, n-i))). The element at the specified position.
147 | export
148 | index :  Nat
149 |       -> Seq a
150 |       -> Maybe a
151 | index i (MkSeq t) =
152 |   if i < length' t
153 |     then
154 |       let (_, MkElem a) = lookupTree i t
155 |         in Just a
156 |     else
157 |       Nothing
158 |
159 | ||| O(log(min(i, n-i))). Update the element at the specified position.
160 | ||| If the position is out of range, the original sequence is returned.
161 | export
162 | adjust :  (a -> a)
163 |        -> Nat
164 |        -> Seq a
165 |        -> Seq a
166 | adjust f i s@(MkSeq t) =
167 |   if i < length' t
168 |     then
169 |       MkSeq $ adjustTree (const (map f)) i t
170 |     else
171 |       s
172 |
173 | ||| O(log(min(i, n-i))). Replace the element at the specified position.
174 | ||| If the position is out of range, the original sequence is returned.
175 | export
176 | update :  Nat
177 |        -> a
178 |        -> Seq a
179 |        -> Seq a
180 | update i a t =
181 |   adjust (const a) i t
182 |
183 | ||| O(log(min(i, n-i))). Split a sequence at a given position.
184 | ||| splitAt i s = (take i s, drop i s)
185 | export
186 | splitAt :  Nat
187 |         -> Seq a
188 |         -> (Seq a, Seq a)
189 | splitAt i s@(MkSeq t) =
190 |   if i < length' t
191 |     then
192 |       let (l, r) = split i t
193 |         in (MkSeq l, MkSeq r)
194 |     else
195 |       (s, empty)
196 |
197 | ||| O(log(min(i,n-i))). The first i elements of a sequence.
198 | ||| If the sequence contains fewer than i elements, the whole sequence is returned.
199 | export
200 | take :  Nat
201 |      -> Seq a
202 |      -> Seq a
203 | take i seq =
204 |   fst (splitAt i seq)
205 |
206 | ||| O(log(min(i,n-i))). Elements of a sequence after the first i.
207 | ||| If the sequence contains fewer than i elements, the empty sequence is returned.
208 | export
209 | drop :  Nat
210 |      -> Seq a
211 |      -> Seq a
212 | drop i seq =
213 |   snd (splitAt i seq)
214 |
215 | ||| Dump the internal structure of the finger tree.
216 | export
217 | show' :  Show a
218 |       => Seq a
219 |       -> String
220 | show' (MkSeq tr) =
221 |   showPrec Open tr
222 |
223 | public export
224 | implementation Eq a => Eq (Seq a) where
225 |   MkSeq x == MkSeq y = x == y
226 |
227 | public export
228 | implementation Ord a => Ord (Seq a) where
229 |   compare (MkSeq x) (MkSeq y) = compare x y
230 |
231 | public export
232 | implementation Functor Seq where
233 |   map f (MkSeq tr) = MkSeq (map (map f) tr)
234 |
235 | public export
236 | implementation Foldable Seq where
237 |   foldr f z (MkSeq tr) = foldr (f . unElem) z tr
238 |   foldl f z (MkSeq tr) = foldl (\acc, (MkElem elem) => f acc elem) z tr
239 |   toList (MkSeq tr) = toList' tr
240 |   null (MkSeq Empty) = True
241 |   null _ = False
242 |
243 | public export
244 | implementation Traversable Seq where
245 |   traverse f (MkSeq tr) = MkSeq <$> traverse (map MkElem . f . unElem) tr
246 |
247 | public export
248 | implementation Show a => Show (Seq a) where
249 |   showPrec p = showPrec p . toList
250 |
251 | public export
252 | implementation Zippable Seq where
253 |   zipWith f (MkSeq x) (MkSeq y) = MkSeq (zipWith' f x y)
254 |   zipWith3 f (MkSeq x) (MkSeq y) (MkSeq z) = MkSeq (zipWith3' f x y z)
255 |   unzipWith f (MkSeq zs) = let (xs, ys) = unzipWith' f zs in (MkSeq xs, MkSeq ys)
256 |   unzipWith3 f (MkSeq ws) = let (xs, ys, zs) = unzipWith3' f ws in (MkSeq xs, MkSeq ys, MkSeq zs)
257 |
258 | public export
259 | implementation Semigroup (Seq a) where
260 |   (<+>) = (++)
261 |
262 | public export
263 | implementation Monoid (Seq a) where
264 |   neutral = empty
265 |
266 | ||| This implementation is differnt from that of Seq.
267 | public export
268 | implementation Applicative Seq where
269 |   pure = singleton
270 |   fs <*> xs = foldMap (\f => map f xs) fs
271 |
272 | public export
273 | [ListLike] Alternative Seq where
274 |   empty = empty
275 |   a <|> b = a ++ b
276 |
277 | public export
278 | [MaybeLike] Alternative Seq where
279 |   empty = empty
280 |   MkSeq Empty <|> b = b
281 |   a <|> _ = a
282 |
283 | public export
284 | implementation Monad Seq where
285 |   xs >>= f = foldMap f xs
286 |
287 | public export
288 | implementation Sized (Seq a) where
289 |   size (MkSeq s) = size s
290 |