    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE CPP        #-}

    -- | A cut-down implementation of lenses, with names taken from
    --   Edward Kmett's lens package.

    module Agda.Utils.Lens
      ( module Agda.Utils.Lens
      , (<&>) -- reexported from Agda.Utils.Functor
      ) where

    import Control.Applicative ( Const(Const), getConst )
    import Control.Monad.State
    import Control.Monad.Reader
    import Control.Monad.Writer

    import Data.Map (Map)
    import qualified Data.Map as Map

    import Data.Functor.Identity

    import Agda.Utils.Functor ((<&>))

    -- * Type-preserving lenses.

    -- | Van Laarhoven style homogeneous lenses.
    --   Mnemoic: "Lens inner outer".
    type Lens' i o = forall f. Functor f => (i -> f i) -> o -> f o

    type LensGet i o = o -> i
    type LensSet i o = i -> o -> o
    type LensMap i o = (i -> i) -> o -> o

    -- * Some simple lenses.

    lFst :: Lens' a (a, b)
    lFst f (x, y) = (, y) <$> f x

    lSnd :: Lens' b (a, b)
    lSnd f (x, y) = (x,) <$> f y

    -- * Elementary lens operations.

    infixl 8 ^.
    -- | Get inner part @i@ of structure @o@ as designated by @Lens' i o@.
    (^.) :: o -> Lens' i o -> i
    o ^. l = getConst $ l Const o

    -- | Set inner part @i@ of structure @o@ as designated by @Lens' i o@.
    set :: Lens' i o -> LensSet i o
    set l = over l . const

    -- | Modify inner part @i@ of structure @o@ using a function @i -> i@.
    over :: Lens' i o -> LensMap i o
    over l f o = runIdentity $ l (Identity . f) o

    -- * State accessors and modifiers using 'StateT'.

    -- | Focus on a part of the state for a stateful computation.
    focus :: Monad m => Lens' i o -> StateT i m a -> StateT o m a
    focus l m = StateT $ \ o -> do
      (a, i) <- runStateT m (o ^. l)
      return (a, set l i o)

    -- * State accessors and modifiers using 'MonadState'.

    -- | Read a part of the state.
    use :: MonadState o m => Lens' i o -> m i
    use l = do !x <- gets (^. l)
               return x

    infix 4 .=
    -- | Write a part of the state.
    (.=) :: MonadState o m => Lens' i o -> i -> m ()
    l .= i = modify $ set l i

    infix 4 %=
    -- | Modify a part of the state.
    (%=) :: MonadState o m => Lens' i o -> (i -> i) -> m ()
    l %= f = modify $ over l f

    infix 4 %==
    -- | Modify a part of the state monadically.
    (%==) :: MonadState o m => Lens' i o -> (i -> m i) -> m ()
    l %== f = put =<< l f =<< get

    infix 4 %%=
    -- | Modify a part of the state monadically, and return some result.
    (%%=) :: MonadState o m => Lens' i o -> (i -> m (i, r)) -> m r
    l %%= f = do
      o <- get
      (o', r) <- runWriterT $ l (WriterT . f) o
      put o'
      return r

    -- | Modify a part of the state locally.
    locallyState :: MonadState o m => Lens' i o -> (i -> i) -> m r -> m r
    locallyState l f k = do
      old <- use l
      l %= f
      x <- k
      l .= old
      return x

    -- * Read-only state accessors and modifiers.

    -- | Ask for part of read-only state.
    view :: MonadReader o m => Lens' i o -> m i
    view l = asks (^. l)

    -- | Modify a part of the state in a subcomputation.
    locally :: MonadReader o m => Lens' i o -> (i -> i) -> m a -> m a
    locally l = local . over l

    locally' :: ((o -> o) -> m a -> m a) -> Lens' i o -> (i -> i) -> m a -> m a
    locally' local l = local . over l

    key :: Ord k => k -> Lens' (Maybe v) (Map k v)
    key k f m = f (Map.lookup k m) <&> \ v -> Map.alter (const v) k m