-- | General functions for stateful manipulation of the scope.

-- This module has been originally created to avoid import cycles between
-- Agda.Syntax.Scope.Monad and Agda.Syntax.Scope.UnusedImports.

module Agda.Syntax.Scope.State where

import Agda.Syntax.Abstract.Name as A ( ModuleName )
import Agda.Syntax.Position ( SetRange(setRange), noRange )
import Agda.Syntax.Scope.Base (scopeCurrent)

import Agda.TypeChecking.Monad.Base ( TCM, MonadTCState, ReadTCState )
import Agda.TypeChecking.Monad.State (useScope, modifyScope, recomputeInverseScope)

import Agda.Utils.Lens (set)
import Agda.Utils.Monad (MonadTrans (lift))

---------------------------------------------------------------------------
-- * The scope checking monad
---------------------------------------------------------------------------

-- | To simplify interaction between scope checking and type checking (in
--   particular when chasing imports), we use the same monad.
type ScopeM = TCM

---------------------------------------------------------------------------
-- * Current module
---------------------------------------------------------------------------

getCurrentModule :: ReadTCState m => m A.ModuleName
getCurrentModule :: forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule = Range -> ModuleName -> ModuleName
forall a. SetRange a => Range -> a -> a
setRange Range
forall a. Range' a
noRange (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' ScopeInfo ModuleName -> m ModuleName
forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
useScope (ModuleName -> f ModuleName) -> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo ModuleName
scopeCurrent

setCurrentModule :: MonadTCState m => A.ModuleName -> m ()
setCurrentModule :: forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
m = do
  (ScopeInfo -> ScopeInfo) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope ((ScopeInfo -> ScopeInfo) -> m ())
-> (ScopeInfo -> ScopeInfo) -> m ()
forall a b. (a -> b) -> a -> b
$ Lens' ScopeInfo ModuleName -> LensSet ScopeInfo ModuleName
forall o i. Lens' o i -> LensSet o i
set (ModuleName -> f ModuleName) -> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo ModuleName
scopeCurrent ModuleName
m
  m ()
forall (m :: * -> *). MonadTCState m => m ()
recomputeInverseScope

withCurrentModule :: (ReadTCState m, MonadTCState m) => A.ModuleName -> m a -> m a
withCurrentModule :: forall (m :: * -> *) a.
(ReadTCState m, MonadTCState m) =>
ModuleName -> m a -> m a
withCurrentModule ModuleName
new m a
action = do
  old <- m ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  setCurrentModule new
  x   <- action
  setCurrentModule old
  return x

withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => A.ModuleName -> t ScopeM a -> t ScopeM a
withCurrentModule' :: forall (t :: (* -> *) -> * -> *) a.
(MonadTrans t, Monad (t ScopeM)) =>
ModuleName -> t ScopeM a -> t ScopeM a
withCurrentModule' ModuleName
new t ScopeM a
action = do
  old <- ScopeM ModuleName -> t ScopeM ModuleName
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  lift $ setCurrentModule new
  x   <- action
  lift $ setCurrentModule old
  return x