toki/idris2-lens
1
0
Fork 0
Code Issues Pull requests Activity

feat: promote filtered from an OptionalFold to an Optional

Browse source
This commit is contained in:
Kiana Sheibani 2025-04-03 00:05:49 -04:00
parent da8f3a05e6
commit d6bae26222
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
2 changed files with 14 additions and 10 deletions

14
src/Control/Lens/Optional.idr
View file

@ -92,6 +92,19 @@ public export
ignored : IndexedOptional i s s a b
ignored = ioptional' (const Nothing) const
||| Construct an `Optional` that can be used to filter the focuses of another
||| optic.
|||
||| To be more specific, this optic passes the value through unchanged if it
||| satisfies the predicate and returns no values if it does not.
|||
||| WARNING: This `Optional` is technically invalid! Its setting capability
||| should only be used in cases where the focuses that pass the filter aren't
||| changed.
public export
filtered : (a -> Bool) -> Optional' a a
filtered p = optional' (\x => if p x then Just x else Nothing) (const id)
||| Extract projection and setter functions from an optional.
public export
@ -121,3 +134,4 @@ withOptional l f = uncurry f (getOptional l)
public export
matching : Optional s t a b -> s -> Either t a
matching = fst . getOptional

10
src/Control/Lens/OptionalFold.idr
View file

@ -62,13 +62,3 @@ public export
ifolding : (s -> Maybe (i, a)) -> IndexedOptionalFold i s a
ifolding f @{MkIsOptFold _} @{ind} =
contrabimap (\x => maybe (Left x) Right (f x)) Left . right . indexed @{ind}
||| Construct an `OptionalFold` that can be used to filter the focuses
||| of another optic.
|||
||| To be more specific, this optic passes the value through unchanged if it
||| satisfies the predicate and returns no values if it does not.
public export
filtered : (a -> Bool) -> OptionalFold a a
filtered p = folding (\x => if p x then Just x else Nothing)