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

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