0 | module Control.Lens.Fold
  1 |
  2 | import Data.Bicontravariant
  3 | import Data.Profunctor
  4 | import Data.Profunctor.Costrong
  5 | import Data.Profunctor.Traversing
  6 | import Control.Applicative.Backwards
  7 | import Control.Lens.Optic
  8 | import Control.Lens.Indexed
  9 | import Control.Lens.OptionalFold
 10 | import Control.Lens.Traversal
 11 |
 12 | %default total
 13 |
 14 |
 15 | ------------------------------------------------------------------------------
 16 | -- Type definitions
 17 | ------------------------------------------------------------------------------
 18 |
 19 |
 20 | -- IsFold
 21 |
 22 | public export
 23 | record IsFold p where
 24 |   constructor MkIsFold
 25 |   runIsFold : (Traversing p, Bicontravariant p)
 26 |
 27 | export %hint
 28 | foldToOptFold : IsFold p => IsOptFold p
 29 | foldToOptFold @{MkIsFold _} = MkIsOptFold %search
 30 |
 31 | export %hint
 32 | foldToTraversal : IsFold p => IsTraversal p
 33 | foldToTraversal @{MkIsFold _} = MkIsTraversal %search
 34 |
 35 |
 36 | -- Fold
 37 |
 38 | ||| A fold is a getter that accesses multiple focus elements.
 39 | ||| `Fold s a` is equivalent to `s -> List a`.
 40 | public export
 41 | 0 Fold : (s,a : Type) -> Type
 42 | Fold = Simple (Optic IsFold)
 43 |
 44 | ||| An indexed fold returns indices while getting.
 45 | public export
 46 | 0 IndexedFold : (i,s,a : Type) -> Type
 47 | IndexedFold = Simple . IndexedOptic IsFold
 48 |
 49 |
 50 | ------------------------------------------------------------------------------
 51 | -- Utilities for folds
 52 | ------------------------------------------------------------------------------
 53 |
 54 |
 55 | ||| Derive a fold from a `Foldable` implementation.
 56 | public export
 57 | folded : Foldable f => Fold (f a) a
 58 | folded @{_} @{MkIsFold _} = rphantom . wander traverse_
 59 |
 60 | ||| Construct a fold from an unfolding function.
 61 | |||
 62 | ||| This function is not total, as it may result in an infinite amount
 63 | ||| of focuses.
 64 | public export covering
 65 | unfolded : (s -> Maybe (a, s)) -> Fold s a
 66 | unfolded coalg @{MkIsFold _} = rphantom . wander loop
 67 |   where
 68 |     loop : Applicative f => (a -> f a) -> s -> f ()
 69 |     loop f = maybe (pure ()) (uncurry $ \x,y => f x *> loop f y) . coalg
 70 |
 71 | ||| Construct a fold from a function into a foldable container.
 72 | public export
 73 | folding : Foldable f => (s -> f a) -> Fold s a
 74 | folding @{_} f @{MkIsFold _} = rphantom . contramapFst f . wander traverse_
 75 |
 76 | ||| Construct an indexed fold from a function into a foldable container.
 77 | public export
 78 | ifolding : Foldable f => (s -> f (i, a)) -> IndexedFold i s a
 79 | ifolding @{_} f @{MkIsFold _} @{ind} =
 80 |   rphantom . contramapFst f . wander traverse_  . indexed @{ind}
 81 |
 82 |
 83 | ||| Reverse the order of a fold's focuses.
 84 | public export
 85 | backwards : Fold s a -> Fold s a
 86 | backwards l @{MkIsFold _} = rphantom . wander func
 87 |   where
 88 |     traversing : Applicative f => Traversing (Forget (f ()))
 89 |     traversing =
 90 |       let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
 91 |       in %search
 92 |
 93 |     func : Applicative f => (a -> f a) -> s -> f ()
 94 |     func fn = let _ = traversing in
 95 |       forwards . runForget (l $ MkForget (MkBackwards {f} . ignore . fn))
 96 |
 97 | ||| Construct a fold that replicates the input n times.
 98 | public export
 99 | replicated : Nat -> Fold a a
100 | replicated n @{MkIsFold _} = rphantom . wander (\f,x => rep n (f x))
101 |   where
102 |     rep : Applicative f => Nat -> f a -> f ()
103 |     rep Z _ = pure ()
104 |     rep (S Z) x = ignore x
105 |     rep (S n@(S _)) x = x *> rep n x
106 |
107 |
108 | ||| Map each focus of an optic to a monoid value and combine them.
109 | public export
110 | foldMapOf : Monoid m => Fold s a -> (a -> m) -> s -> m
111 | foldMapOf l = runForget . l . MkForget
112 |
113 | ||| Map each focus of an optic to a monoid value with access to the index and
114 | ||| combine them.
115 | public export
116 | ifoldMapOf : Monoid m => IndexedFold i s a -> (i -> a -> m) -> s -> m
117 | ifoldMapOf l = runForget . l @{%search} @{Idxed} . MkForget . uncurry
118 |
119 | ||| Combine the focuses of an optic using the provided function, starting from
120 | ||| the right.
121 | public export
122 | foldrOf : Fold s a -> (a -> acc -> acc) -> acc -> s -> acc
123 | foldrOf l = flip . foldMapOf @{MkMonoid @{MkSemigroup (.)} id} l
124 |
125 | ||| Combine the focuses of an optic using the provided function with access to
126 | ||| the index, starting from the right.
127 | public export
128 | ifoldrOf : IndexedFold i s a -> (i -> a -> acc -> acc) -> acc -> s -> acc
129 | ifoldrOf l = flip . ifoldMapOf @{MkMonoid @{MkSemigroup (.)} id} l
130 |
131 | ||| Combine the focuses of an optic using the provided function, starting from
132 | ||| the left.
133 | public export
134 | foldlOf : Fold s a -> (acc -> a -> acc) -> acc -> s -> acc
135 | foldlOf l = flip . foldMapOf @{MkMonoid @{MkSemigroup $ flip (.)} id} l . flip
136 |
137 | ||| Combine the focuses of an optic using the provided function with access to
138 | ||| the index, starting from the left.
139 | public export
140 | ifoldlOf : IndexedFold i s a -> (i -> acc -> a -> acc) -> acc -> s -> acc
141 | ifoldlOf l = flip . ifoldMapOf @{MkMonoid @{MkSemigroup $ flip (.)} id} l . (flip .)
142 |
143 | ||| Combine each focus value of an optic using a monoid structure.
144 | public export
145 | concatOf : Monoid m => Fold s m -> s -> m
146 | concatOf l = foldMapOf l id
147 |
148 | ||| Fold over the focuses of an optic using Alternative.
149 | public export
150 | choiceOf : Alternative f => Fold s (Lazy (f a)) -> s -> f a
151 | choiceOf = force .: concatOf @{MonoidAlternative}
152 |
153 | ||| Evaluate each computation of an optic and discard the results.
154 | public export
155 | sequenceOf_ : Applicative f => Fold s (f a) -> s -> f ()
156 | sequenceOf_ l =
157 |   let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
158 |   in foldMapOf l ignore
159 |
160 | ||| Map each focus of an optic to a computation, evaluate those
161 | ||| computations and discard the results.
162 | public export
163 | traverseOf_ : Applicative f => Fold s a -> (a -> f b) -> s -> f ()
164 | traverseOf_ l f =
165 |   let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
166 |   in foldMapOf l (ignore . f)
167 |
168 | ||| Map each focus of an optic to a computation with access to the index,
169 | ||| evaluate those computations and discard the results.
170 | public export
171 | itraverseOf_ : Applicative f => IndexedFold i s a -> (i -> a -> f b) -> s -> f ()
172 | itraverseOf_ l f =
173 |   let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
174 |   in ifoldMapOf l (ignore .: f)
175 |
176 | ||| A version of `traverseOf_` with the arguments flipped.
177 | public export
178 | forOf_ : Applicative f => Fold s a -> s -> (a -> f b) -> f ()
179 | forOf_ = flip . traverseOf_
180 |
181 | ||| A version of `itraverseOf_` with the arguments flipped.
182 | public export
183 | iforOf_ : Applicative f => IndexedFold i s a -> s -> (i -> a -> f b) -> f ()
184 | iforOf_ = flip . itraverseOf_
185 |
186 | ||| The conjunction of an optic containing lazy boolean values.
187 | public export
188 | andOf : Fold s (Lazy Bool) -> s -> Bool
189 | andOf = force .: concatOf @{All}
190 |
191 | ||| The disjunction of an optic containing lazy boolean values.
192 | public export
193 | orOf : Fold s (Lazy Bool) -> s -> Bool
194 | orOf = force .: concatOf @{Any}
195 |
196 | ||| Return `True` if all focuses of the optic satisfy the predicate.
197 | public export
198 | allOf : Fold s a -> (a -> Bool) -> s -> Bool
199 | allOf = foldMapOf @{All}
200 |
201 | ||| Return `True` if all focuses of the indexed optic satisfy the predicate.
202 | public export
203 | iallOf : IndexedFold i s a -> (i -> a -> Bool) -> s -> Bool
204 | iallOf = ifoldMapOf @{All}
205 |
206 | ||| Return `True` if any focuses of the optic satisfy the predicate.
207 | public export
208 | anyOf : Fold s a -> (a -> Bool) -> s -> Bool
209 | anyOf = foldMapOf @{Any}
210 |
211 | ||| Return `True` if any focuses of the indexed optic satisfy the predicate.
212 | public export
213 | ianyOf : IndexedFold i s a -> (i -> a -> Bool) -> s -> Bool
214 | ianyOf = ifoldMapOf @{Any}
215 |
216 |
217 | ||| Return `True` if the element occurs in the focuses of the optic.
218 | public export
219 | elemOf : Eq a => Fold s a -> a -> s -> Bool
220 | elemOf l = anyOf l . (==)
221 |
222 | ||| Calculate the number of focuses of the optic.
223 | public export
224 | lengthOf : Fold s a -> s -> Nat
225 | lengthOf l = foldMapOf @{Additive} l (const 1)
226 |
227 | ||| Access the first focus value of an optic, returning `Nothing` if there are
228 | ||| no focuses.
229 | |||
230 | ||| This is identical to `preview`.
231 | public export
232 | firstOf : Fold s a -> s -> Maybe a
233 | firstOf l = foldMapOf l Just
234 |
235 | ||| Access the first focus value and index of an indexed optic, returning Nothing
236 | ||| if there are no focuses.
237 | |||
238 | ||| This is identical to `ipreview`.
239 | public export
240 | ifirstOf : IndexedFold i s a -> s -> Maybe (i, a)
241 | ifirstOf l = runForget $ l @{%search} @{Idxed} $ MkForget Just
242 |
243 | ||| Access the last focus value of an optic, returning `Nothing` if there are
244 | ||| no focuses.
245 | public export
246 | lastOf : Fold s a -> s -> Maybe a
247 | lastOf l = foldMapOf @{MkMonoid @{MkSemigroup $ flip (<+>)} neutral} l Just
248 |
249 | ||| Access the last focus value and index of an indexed optic, returning Nothing
250 | ||| if there are no focuses.
251 | public export
252 | ilastOf : IndexedFold i s a -> s -> Maybe (i, a)
253 | ilastOf l =
254 |   let _ = MkMonoid @{MkSemigroup $ flip (<+>)} neutral
255 |   in runForget $ l @{%search} @{Idxed} $ MkForget Just
256 |
257 |
258 |
259 | ------------------------------------------------------------------------------
260 | -- Accessing folds
261 | ------------------------------------------------------------------------------
262 |
263 |
264 | ||| Return `True` if the optic focuses on any values.
265 | public export
266 | has : Fold s a -> s -> Bool
267 | has l = anyOf l (const True)
268 |
269 | ||| Return `True` if the optic does not focus on any values.
270 | public export
271 | hasn't : Fold s a -> s -> Bool
272 | hasn't l = allOf l (const False)
273 |
274 |
275 | ||| Access the first focus value of an optic and apply a function to it,
276 | ||| returning `Nothing` if there are no focuses.
277 | public export
278 | previews : Fold s a -> (a -> r) -> s -> Maybe r
279 | previews l f = foldMapOf l (Just . f)
280 |
281 | ||| Access the first focus value of an optic, returning `Nothing` if there are
282 | ||| no focuses.
283 | |||
284 | ||| This is an alias for `firstOf`.
285 | public export
286 | preview : Fold s a -> s -> Maybe a
287 | preview = firstOf
288 |
289 | export infixl 8 ^?, ^@?, ^., ^@.
290 |
291 | ||| Access the first focus value of an optic, returning `Nothing` if there are
292 | ||| no focuses.
293 | |||
294 | ||| This is the operator form of `preview`.
295 | public export
296 | (^?) : s -> Fold s a -> Maybe a
297 | (^?) x l = preview l x
298 |
299 |
300 | ||| Access the first focus value and index of an indexed optic, returning Nothing
301 | ||| if there are no focuses.
302 | |||
303 | ||| This is an alias for `ifirstOf`.
304 | public export
305 | ipreview : IndexedFold i s a -> s -> Maybe (i, a)
306 | ipreview = ifirstOf
307 |
308 | ||| Access the first focus value and index of an indexed optic, returning Nothing
309 | ||| if there are no focuses.
310 | |||
311 | ||| This is the operator form of `ipreview`.
312 | public export
313 | (^@?) : s -> IndexedFold i s a -> Maybe (i, a)
314 | (^@?) x l = ipreview l x
315 |
316 |
317 | ||| Convert a `Fold` into an `OptionalFold` that accesses the first focus element.
318 | |||
319 | ||| For the traversal version of this, see `singular`.
320 | public export
321 | pre : Fold s a -> OptionalFold s a
322 | pre = folding . preview
323 |
324 | ||| Convert an `IndexedFold` into an `IndexedOptionalFold` that accesses the
325 | ||| first focus element.
326 | |||
327 | ||| For the traversal version of this, see `isingular`.
328 | public export
329 | ipre : IndexedFold i s a -> IndexedOptionalFold i s a
330 | ipre = ifolding . ipreview
331 |
332 |
333 | ||| Return a list of all focuses of a fold.
334 | public export
335 | toListOf : Fold s a -> s -> List a
336 | toListOf l = foldrOf l (::) []
337 |
338 | ||| Return a list of all focuses of a fold.
339 | |||
340 | ||| This is the operator form of `toListOf`.
341 | public export
342 | (^..) : s -> Fold s a -> List a
343 | (^..) s l = toListOf l s
344 |
345 |
346 | ||| Return a list of all focuses and indices of an indexed fold.
347 | public export
348 | itoListOf : IndexedFold i s a -> s -> List (i, a)
349 | itoListOf l = ifoldrOf l ((::) .: (,)) []
350 |
351 | ||| Return a list of all focuses and indices of an indexed fold.
352 | |||
353 | ||| This is the operator form of `itoListOf`.
354 | public export
355 | (^@..) : s -> IndexedFold i s a -> List (i, a)
356 | (^@..) x l = itoListOf l x
357 |