
  0 | module Control.Lens.At
  1 | 
  2 | import Control.Lens.Optic
  3 | import Control.Lens.Indexed
  4 | import Control.Lens.Iso
  5 | import Control.Lens.Lens
  6 | import Control.Lens.Optional
  7 | import Control.Lens.Traversal
  8 | import Control.Lens.Setter
  9 | 
 10 | %default total
 11 | 
 12 | 
 13 | ||| An interface that provides an `Optional` to access a given index in a
 14 | ||| container, such as an ordinal position in a `List` or `Vect` or a key in a
 15 | ||| map.
 16 | public export
 17 | interface Ixed i v a | a where
 18 |   ||| An optional that possibly accesses a value at a given index of a container.
 19 |   ix : i -> Optional' a v
 20 | 
 21 | ||| An indexed version of `ix`.
 22 | public export
 23 | iix : Ixed i v a => i -> IndexedOptional' i a v
 24 | iix i = constIndex i (ix i)
 25 | 
 26 | 
 27 | public export
 28 | [Function] Eq e => Ixed e a (e -> a) where
 29 |   ix k = optional' (Just . ($ k)) (\f,x,k' => if k == k' then x else f k')
 30 | 
 31 | 
 32 | ||| An interface that provides a lens to access a given index in a collection.
 33 | ||| This is different from `Ixed` in that the lens cannot fail to get a value.
 34 | |||
 35 | ||| Implementations of this interface may use different index types for `ix` and
 36 | ||| `ix'`; for example, `Vect n a` uses `Nat` for `ix` and `Fin n` for `ix'`.
 37 | public export
 38 | interface Ixed i v a => Ixed' i i' v a | a where
 39 |   ||| A lens that infallibly accesses a value at a given index of a container.
 40 |   ix' : i' -> Lens' a v
 41 | 
 42 | ||| An indexed version of `ix'`.
 43 | public export
 44 | iix' : Ixed' i i' v a => i' -> IndexedLens' i' a v
 45 | iix' i = constIndex i (ix' i)
 46 | 
 47 | 
 48 | public export
 49 | [Function'] Eq e => Ixed' e e a (e -> a) using Function where
 50 |   ix' k = lens ($ k) (\f,x,k' => if k == k' then x else f k')
 51 | 
 52 | 
 53 | ||| This interface provides a lens to read, write, add or delete the value
 54 | ||| associated to a key in a map or map-like container.
 55 | |||
 56 | ||| This lens should satisfy:
 57 | ||| * `ix i == at i . Just_`
 58 | |||
 59 | ||| If you do not need to add or delete keys, `ix` is more convenient.
 60 | public export
 61 | interface Ixed i v a => At i v a | a where
 62 |   ||| A lens that can be used to read, write, add or delete a value associated
 63 |   ||| with a key in a map-like container.
 64 |   |||
 65 |   ||| If you do not need to add or delete keys, `ix` is more convenient.
 66 |   at : i -> Lens' a (Maybe v)
 67 | 
 68 | 
 69 | ||| An indexed version of `at`.
 70 | public export
 71 | iat : At i v a => i -> IndexedLens' i a (Maybe v)
 72 | iat i = constIndex i (at i)
 73 | 
 74 | 
 75 | ||| Delete the value at a particular key in a container using `At`.
 76 | public export
 77 | sans : At i v a => i -> a -> a
 78 | sans k = at k .~ Nothing
 79 | 
 80 | ||| Add a value at a particular key in a container using `At`.
 81 | public export
 82 | add : At i v a => i -> v -> a -> a
 83 | add k = (at k ?~)
 84 |