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

Add new functions for indexing optics

Browse source
This commit is contained in:
Kiana Sheibani 2023-04-21 08:26:20 -04:00
parent 27247861d6
commit e0297af9f3
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 23 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Control/Lens/At.idr
View file

@ -1,6 +1,8 @@
module Control.Lens.At module Control.Lens.At
import Control.Lens.Optic import Control.Lens.Optic
import Control.Lens.Indexed
import Control.Lens.Iso
import Control.Lens.Lens import Control.Lens.Lens
import Control.Lens.Optional import Control.Lens.Optional
import Control.Lens.Traversal import Control.Lens.Traversal
@ -17,6 +19,12 @@ interface Ixed i v a | a where
||| An optional that possibly accesses a value at a given index of a container. ||| An optional that possibly accesses a value at a given index of a container.
ix : i -> Optional' a v ix : i -> Optional' a v
||| An indexed version of `ix`.
public export
iix : Ixed i v a => i -> IndexedOptional' i a v
iix i = constIndex i (ix i)
public export public export
[Function] Eq e => Ixed e a (e -> a) where [Function] Eq e => Ixed e a (e -> a) where
ix k = optional' (Just . ($ k)) (\f,x,k' => if k == k' then x else f k') ix k = optional' (Just . ($ k)) (\f,x,k' => if k == k' then x else f k')
@ -32,6 +40,12 @@ interface Ixed i v a => Ixed' i i' v a | a where
||| An lens that infallibly accesses a value at a given index of a container. ||| An lens that infallibly accesses a value at a given index of a container.
ix' : i' -> Lens' a v ix' : i' -> Lens' a v
||| An indexed version of `ix'`.
public export
iix' : Ixed' i i' v a => i' -> IndexedLens' i' a v
iix' i = constIndex i (ix' i)
public export public export
[Function'] Eq e => Ixed' e e a (e -> a) using Function where [Function'] Eq e => Ixed' e e a (e -> a) using Function where
ix' k = lens ($ k) (\f,x,k' => if k == k' then x else f k') ix' k = lens ($ k) (\f,x,k' => if k == k' then x else f k')
@ -40,8 +54,8 @@ public export
||| This interface provides a lens to read, write, add or delete the value ||| This interface provides a lens to read, write, add or delete the value
||| associated to a key in a map or map-like container. ||| associated to a key in a map or map-like container.
||| |||
||| This lens must follow the law: ||| This lens should satisfy:
||| * `ix == at . Just_` ||| * `ix i == at i . Just_`
||| |||
||| If you do not need to add or delete keys, `ix` is more convenient. ||| If you do not need to add or delete keys, `ix` is more convenient.
public export public export
@ -52,6 +66,13 @@ interface Ixed i v a => At i v a | a where
||| If you do not need to add or delete keys, `ix` is more convenient. ||| If you do not need to add or delete keys, `ix` is more convenient.
at : i -> Lens' a (Maybe v) at : i -> Lens' a (Maybe v)
||| An indexed version of `at`.
public export
iat : At i v a => i -> IndexedLens' i a (Maybe v)
iat i = constIndex i (at i)
||| Delete the value at a particular key in a container using `At`. ||| Delete the value at a particular key in a container using `At`.
public export public export
sans : At i v a => i -> a -> a sans : At i v a => i -> a -> a