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 enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure a c) => c -> (a -> m b) -> m b enterClosure :: forall (m :: * -> *) a c b. (MonadTCEnv m, ReadTCState m, LensClosure a c) => 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 forall o i. o -> Lens' i o -> i ^. forall a b. LensClosure a b => Lens' (Closure a) b lensClosure = do Bool isDbg <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a viewTC Lens' Bool TCEnv eIsDebugPrinting forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a withScope_ ScopeInfo scope forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) a b. ReadTCState m => Lens' a TCState -> (a -> a) -> m b -> m b locallyTCState Lens' (Map ModuleName CheckpointId) TCState stModuleCheckpoints (forall a b. a -> b -> a const Map ModuleName CheckpointId cps) forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) a. MonadTCEnv m => TCEnv -> m a -> m a withEnv TCEnv env{ envIsDebugPrinting :: Bool envIsDebugPrinting = Bool isDbg } forall a b. (a -> b) -> a -> b $ a -> m b k a x 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 = forall (m :: * -> *) a c b. (MonadTCEnv m, ReadTCState m, LensClosure a c) => c -> (a -> m b) -> m b enterClosure Closure a cl forall a b. (a -> b) -> a -> b $ a -> m b k forall (m :: * -> *) a b c. Monad m => (a -> m b) -> (b -> m c) -> a -> m c >=> forall (m :: * -> *) a. (MonadTCEnv m, ReadTCState m) => a -> m (Closure a) buildClosure 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 = forall a b c. (a -> b -> c) -> b -> a -> c flip forall (m :: * -> *) a b. (MonadTCEnv m, ReadTCState m) => Closure a -> (a -> m b) -> m (Closure b) withClosure