-- | 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 Mikan.Syntax.Scope.State where

import Data.Map.Strict qualified as Map

import Mikan.Syntax.Abstract.Name as A (ModuleName)
import Mikan.Syntax.Common.Pretty (prettyShow)
import Mikan.Syntax.Position (SetRange(setRange), noRange)
import Mikan.Syntax.Scope.Base (scopeCurrent, Scope, scopeModules)

import Mikan.TypeChecking.Monad.State (useScope, modifyScope, recomputeInverseScope, getScope)
import Mikan.TypeChecking.Monad.Base (TCM, MonadTCState, ReadTCState)
import Mikan.TypeChecking.Monad.Debug (reportSLn)

import Mikan.Utils.Impossible
import Mikan.Utils.Monad (MonadTrans (lift))
import Mikan.Utils.Lens (set, (^.))

---------------------------------------------------------------------------
-- * 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
$ ASetter ScopeInfo ScopeInfo ModuleName ModuleName
-> ModuleName -> ScopeInfo -> ScopeInfo
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter ScopeInfo ScopeInfo ModuleName ModuleName
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 (TCMT IO))) =>
ModuleName -> t (TCMT IO) a -> t (TCMT IO) a
withCurrentModule' ModuleName
new t (TCMT IO) a
action = do
  old <- ScopeM ModuleName -> t (TCMT IO) 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

getNamedScope :: A.ModuleName -> ScopeM Scope
getNamedScope :: ModuleName -> ScopeM Scope
getNamedScope ModuleName
m = do
  scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  case Map.lookup m (scope ^. scopeModules) of
    Just Scope
s  -> Scope -> ScopeM Scope
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Scope
s
    Maybe Scope
Nothing -> do
      [Char] -> VerboseLevel -> [Char] -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"" VerboseLevel
0 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"ERROR: In scope\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ScopeInfo -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ScopeInfo
scope [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\nNO SUCH SCOPE " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
m
      ScopeM Scope
forall a. HasCallStack => a
__IMPOSSIBLE__

getCurrentScope :: ScopeM Scope
getCurrentScope :: ScopeM Scope
getCurrentScope = ModuleName -> ScopeM Scope
getNamedScope (ModuleName -> ScopeM Scope) -> ScopeM ModuleName -> ScopeM Scope
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule