0 | ||| General purpose linear two-end finite sequences.
  1 | |||
  2 | ||| This is implemented by finger tree.
  3 | module Data.Seq1.Unsized
  4 |
  5 | import Control.WellFounded
  6 | import Data.Linear.Ref1
  7 | import public Data.Zippable
  8 |
  9 | import Data.Seq.Internal
 10 |
 11 | %default total
 12 |
 13 | ||| A linear two-end finite sequence.
 14 | export
 15 | data Seq1 : (s : Type) -> (e : Type) -> Type where
 16 |   MkSeq1 : Ref s (FingerTree (Elem e))
 17 |         -> Seq1 s e
 18 |
 19 | ||| O(1). The empty sequence.
 20 | export
 21 | empty : F1 s (Seq1 s e)
 22 | empty t =
 23 |   let tr # t := ref1 Empty t
 24 |     in MkSeq1 tr # t
 25 |
 26 | ||| O(1). A singleton sequence.
 27 | export
 28 | singleton :  e
 29 |           -> F1 s (Seq1 s e)
 30 | singleton a t =
 31 |   let tr # t := ref1 (Single (MkElem a)) t
 32 |     in MkSeq1 tr # t
 33 |
 34 | ||| O(n). A sequence of length n with a the value of every element.
 35 | export
 36 | replicate :  (n : Nat)
 37 |           -> (a : e)
 38 |           -> F1 s (Seq1 s e)
 39 | replicate n a t =
 40 |   let tr # t := ref1 (replicate' n a) t
 41 |     in MkSeq1 tr # t
 42 |
 43 | ||| O(1). The number of elements in the sequence.
 44 | export
 45 | length :  Seq1 s a
 46 |        -> F1 s Nat
 47 | length (MkSeq1 tr) t =
 48 |   let tr' # t := read1 tr t
 49 |     in length' tr' # t
 50 |
 51 | ||| O(n). Reverse the sequence.
 52 | export
 53 | reverse :  Seq1 s a
 54 |         -> F1' s
 55 | reverse (MkSeq1 tr) t =
 56 |   casmod1 tr (\tr' => reverseTree id tr') t
 57 |
 58 | export infixr 5 `cons`
 59 | ||| O(1). Add an element to the left end of a sequence.
 60 | export
 61 | cons :  e
 62 |      -> Seq1 s e
 63 |      -> F1' s
 64 | (a `cons` (MkSeq1 tr)) t =
 65 |   casmod1 tr (\tr' => MkElem a `consTree` tr') t
 66 |
 67 | export infixl 5 `snoc`
 68 | ||| O(1). Add an element to the right end of a sequence.
 69 | export
 70 | snoc :  Seq1 s e
 71 |      -> e
 72 |      -> F1' s
 73 | ((MkSeq1 tr) `snoc` a) t =
 74 |   casmod1 tr (\tr' => tr' `snocTree` MkElem a) t
 75 |
 76 | ||| O(1). View from the left of the sequence.
 77 | export
 78 | viewl :  Seq1 s e
 79 |       -> F1 s (Maybe (e, Seq1 s e))
 80 | viewl (MkSeq1 tr) t =
 81 |   casupdate1 tr
 82 |     (\tr' =>
 83 |       case viewLTree tr' of
 84 |         Just (MkElem a, tr'') =>
 85 |           (tr'', Just (a, MkSeq1 tr))
 86 |         Nothing               =>
 87 |           (tr', Nothing)
 88 |     ) t
 89 |
 90 | ||| O(1). The first element of the sequence.
 91 | export
 92 | head :  Seq1 s e
 93 |      -> F1 s (Maybe e)
 94 | head (MkSeq1 tr) t =
 95 |   let tr' # t := read1 tr t
 96 |    in case viewLTree tr' of
 97 |         Just (MkElem a, _) =>
 98 |           Just a # t
 99 |         Nothing            =>
100 |           Nothing # t
101 |
102 | ||| O(1). The elements after the head of the sequence.
103 | ||| Returns an empty sequence when the sequence is empty.
104 | export
105 | tail :  Seq1 s e
106 |      -> F1' s
107 | tail (MkSeq1 tr) t =
108 |   casmod1 tr
109 |     (\tr' =>
110 |       case viewLTree tr' of
111 |         Just (MkElem _, tr'') =>
112 |           tr''
113 |         Nothing               =>
114 |           tr'
115 |     ) t
116 |
117 | ||| O(1). View from the right of the sequence.
118 | export
119 | viewr :  Seq1 s e
120 |       -> F1 s (Maybe (Seq1 s e, e))
121 | viewr (MkSeq1 tr) t =
122 |   casupdate1 tr
123 |     (\tr' =>
124 |       case viewRTree tr' of
125 |         Just (tr'', MkElem a) =>
126 |           (tr'', Just (MkSeq1 tr, a))
127 |         Nothing               =>
128 |           (tr', Nothing)
129 |     ) t
130 |
131 | ||| O(1). The elements before the last element of the sequence.
132 | ||| Returns an empty sequence when the sequence is empty.
133 | export
134 | init :  Seq1 s e
135 |      -> F1' s
136 | init (MkSeq1 tr) t =
137 |   casmod1 tr
138 |     (\tr' =>
139 |       case viewRTree tr' of
140 |         Just (tr'', MkElem _) =>
141 |           tr''
142 |         Nothing               =>
143 |           tr'
144 |     ) t
145 |
146 | ||| O(1). The last element of the sequence.
147 | export
148 | last :  Seq1 s e
149 |      -> F1 s (Maybe e)
150 | last (MkSeq1 tr) t =
151 |   let tr' # t := read1 tr t
152 |     in case viewRTree tr' of
153 |          Just (_, MkElem a) =>
154 |            Just a # t
155 |          Nothing            =>
156 |            Nothing # t
157 |
158 | ||| O(n). Turn a list into a sequence.
159 | export
160 | fromList :  List e
161 |          -> F1 s (Seq1 s e)
162 | fromList xs t =
163 |   let tr # t := ref1 (foldr (\x, acc => MkElem x `consTree` acc) Empty xs) t
164 |     in (MkSeq1 tr) # t
165 |
166 | ||| Turn a sequence into a list. O(n)
167 | export
168 | toList :  Seq1 s e
169 |        -> F1 s (List e)
170 | toList seq t =
171 |   go seq Lin t
172 |   where
173 |     go :  Seq1 s e
174 |        -> (sl : SnocList e)
175 |        -> F1 s (List e)
176 |     go seq sl t =
177 |       let tr # t := Data.Seq1.Unsized.viewl seq t
178 |         in case tr of
179 |              Nothing       =>
180 |                (sl <>> []) # t
181 |              Just (x, tr') =>
182 |                (assert_total (go tr' (sl :< x))) t
183 |
184 | ||| O(log(min(i, n-i))). The element at the specified position.
185 | export
186 | index :  Nat
187 |       -> Seq1 s e
188 |       -> F1 s (Maybe e)
189 | index i (MkSeq1 tr) t =
190 |   let tr' # t := read1 tr t
191 |     in case i < length' tr' of
192 |          True  =>
193 |            let (_, MkElem a) := lookupTree i tr'
194 |             in Just a # t
195 |          False =>
196 |            Nothing # t
197 |
198 | ||| O(log(min(i, n-i))). Update the element at the specified position.
199 | ||| If the position is out of range, the original sequence is returned.
200 | export
201 | adjust :  (e -> e)
202 |        -> Nat
203 |        -> Seq1 s e
204 |        -> F1' s
205 | adjust f i (MkSeq1 tr) t =
206 |   casmod1 tr
207 |     (\tr' =>
208 |       case i < length' tr' of
209 |         True  =>
210 |           adjustTree (const (map f)) i tr'
211 |         False => tr'
212 |     ) t
213 |
214 | ||| O(log(min(i, n-i))). Replace the element at the specified position.
215 | ||| If the position is out of range, the original sequence is returned.
216 | export
217 | update :  Nat
218 |        -> e
219 |        -> Seq1 s e
220 |        -> F1' s
221 | update i a seq t =
222 |   adjust (const a) i seq t
223 |
224 | ||| Dump the internal structure of the finger tree.
225 | export
226 | show' :  Show e
227 |       => Seq1 s e
228 |       -> F1 s String
229 | show' (MkSeq1 tr) t =
230 |   let tr' # t := read1 tr t
231 |     in showPrec Open tr' # t
232 |