{-# 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
  Bool
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
  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' TCState (Map ModuleName CheckpointId)
-> (Map ModuleName CheckpointId -> Map ModuleName CheckpointId)
-> m b
-> m b
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
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 = isDbg }
    (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ a -> m b
k a
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