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