
  0 | module Data.SortedMap.Lens
  1 | 
  2 | import Decidable.Equality
  3 | import Data.SortedMap.Dependent
  4 | import Data.SortedMap
  5 | import public Control.Lens
  6 | 
  7 | %default total
  8 | 
  9 | 
 10 | public export
 11 | Ixed k v (SortedMap k v) where
 12 |   ix k = optional' (lookup k) (flip $ insert k)
 13 | 
 14 | public export
 15 | At k v (SortedMap k v) where
 16 |   at k = lens (lookup k) (flip $ \case
 17 |     Nothing => delete k
 18 |     Just v => insert k v)
 19 | 
 20 | 
 21 | public export
 22 | ixDep : DecEq k => {0 p : k -> Type} -> (x : k) ->
 23 |           Optional' (SortedDMap k p) (p x)
 24 | ixDep {p} x = optional' (lookupPrecise x) (\m,v => insert x v m)
 25 | 
 26 | public export
 27 | atDep : DecEq k => {0 p : k -> Type} -> (x : k) ->
 28 |           Lens' (SortedDMap k p) (Maybe $ p x)
 29 | atDep {p} x = lens (lookupPrecise x) (\m => \case
 30 |   Nothing => delete x m
 31 |   Just v => insert x v m)
 32 | 
 33 | 
 34 | public export
 35 | Each (SortedMap k v) (SortedMap k w) v w where
 36 |   each = traversed
 37 | 
 38 | public export
 39 | IEach k (SortedMap k v) (SortedMap k w) v w where
 40 |   ieach = itraversal func
 41 |     where
 42 |       func : Applicative f => (k -> v -> f w) -> SortedMap k v -> f (SortedMap k w)
 43 |       func f = map (cast {from = SortedDMap k (const w)})
 44 |                 . Dependent.traverse (f %search)
 45 |                 . cast {to = SortedDMap k (const v)}
 46 |