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