module Agda.Utils.Lens
( module Agda.Utils.Lens
, (<&>)
) where
import Control.Monad.State
import Control.Monad.Reader
import Data.Functor.Constant
import Data.Functor.Identity
import Agda.Utils.Functor ((<&>))
type Lens' i o = forall f. Functor f => (i -> f i) -> o -> f o
infixl 8 ^.
(^.) :: o -> Lens' i o -> i
o ^. l = getConstant $ l Constant o
set :: Lens' i o -> i -> o -> o
set l = over l . const
over :: Lens' i o -> (i -> i) -> o -> o
over l f o = runIdentity $ l (Identity . f) o
use :: MonadState o m => Lens' i o -> m i
use l = gets (^. l)
infix 4 .=
(.=) :: MonadState o m => Lens' i o -> i -> m ()
l .= i = modify $ set l i
infix 4 %=
(%=) :: MonadState o m => Lens' i o -> (i -> i) -> m ()
l %= f = modify $ over l f
view :: MonadReader o m => Lens' i o -> m i
view l = asks (^. l)
locally :: MonadReader o m => Lens' i o -> (i -> i) -> m a -> m a
locally l = local . over l