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