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