    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Monad.Closure where

    import Control.Monad

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Env
    import Agda.TypeChecking.Monad.State

    import Agda.Utils.Lens

    {-# INLINE enterClosure #-}
    enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure c a)
                 => c -> (a -> m b) -> m b
    enterClosure :: forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure c
    c a -> m b
    k | Closure Signature
    _sig TCEnv
    env ScopeInfo
    scope Map ModuleName CheckpointId
    cps a
    x <- c
    c c -> Lens' c (Closure a) -> Closure a
    forall o i. o -> Lens' o i -> i
    ^. (Closure a -> f (Closure a)) -> c -> f c
    forall b a. LensClosure b a => Lens' b (Closure a)
    Lens' c (Closure a)
    lensClosure = do
      isDbg <- Lens' TCEnv Bool -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eIsDebugPrinting
      withScope_ scope
        $ locallyTCState stModuleCheckpoints (const cps)
        $ withEnv env{ envIsDebugPrinting = isDbg }
        $ k x

    {-# INLINE withClosure  #-}
    withClosure :: (MonadTCEnv m, ReadTCState m) => Closure a -> (a -> m b) -> m (Closure b)
    withClosure :: forall (m :: * -> *) a b.
    (MonadTCEnv m, ReadTCState m) =>
    Closure a -> (a -> m b) -> m (Closure b)
    withClosure Closure a
    cl a -> m b
    k = Closure a -> (a -> m (Closure b)) -> m (Closure b)
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure Closure a
    cl ((a -> m (Closure b)) -> m (Closure b))
    -> (a -> m (Closure b)) -> m (Closure b)
    forall a b. (a -> b) -> a -> b
    $ a -> m b
    k (a -> m b) -> (b -> m (Closure b)) -> a -> m (Closure b)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> b -> m (Closure b)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure

    {-# INLINE mapClosure  #-}
    mapClosure :: (MonadTCEnv m, ReadTCState m) => (a -> m b) -> Closure a -> m (Closure b)
    mapClosure :: forall (m :: * -> *) a b.
    (MonadTCEnv m, ReadTCState m) =>
    (a -> m b) -> Closure a -> m (Closure b)
    mapClosure = (Closure a -> (a -> m b) -> m (Closure b))
    -> (a -> m b) -> Closure a -> m (Closure b)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Closure a -> (a -> m b) -> m (Closure b)
    forall (m :: * -> *) a b.
    (MonadTCEnv m, ReadTCState m) =>
    Closure a -> (a -> m b) -> m (Closure b)
    withClosure