{-# 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