module Agda.TypeChecking.Monad.Env where
import qualified Data.List as List
import Data.Maybe (fromMaybe)
import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name
import Agda.TypeChecking.Monad.Base
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Impossible
{-# SPECIALIZE currentModule :: TCM ModuleName #-}
{-# SPECIALIZE currentModule :: ReduceM ModuleName #-}
currentModule :: MonadTCEnv m => m ModuleName
currentModule = asksTC envCurrentModule
withCurrentModule :: ModuleName -> TCM a -> TCM a
withCurrentModule m =
localTC $ \ e -> e { envCurrentModule = m }
getCurrentPath :: MonadTCEnv m => m AbsolutePath
getCurrentPath = fromMaybe __IMPOSSIBLE__ <$> asksTC envCurrentPath
{-# SPECIALIZE getAnonymousVariables :: ModuleName -> TCM Nat #-}
{-# SPECIALIZE getAnonymousVariables :: ModuleName -> ReduceM Nat #-}
getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat
getAnonymousVariables m = do
ms <- asksTC envAnonymousModules
return $ sum [ n | (m', n) <- ms, mnameToList m' `List.isPrefixOf` mnameToList m ]
withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a
withAnonymousModule m n =
localTC $ \ e -> e { envAnonymousModules = (m, n) : envAnonymousModules e }
withEnv :: MonadTCEnv m => TCEnv -> m a -> m a
withEnv env = localTC $ \ env0 -> env
{ envPrintMetasBare = envPrintMetasBare env0
}
getEnv :: TCM TCEnv
getEnv = askTC
withIncreasedModuleNestingLevel :: TCM a -> TCM a
withIncreasedModuleNestingLevel =
localTC $ \ e -> e { envModuleNestingLevel =
envModuleNestingLevel e + 1 }
withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a
withHighlightingLevel h = localTC $ \ e -> e { envHighlightingLevel = h }
withoutOptionsChecking :: TCM a -> TCM a
withoutOptionsChecking = localTC $ \ e -> e { envCheckOptionConsistency = False }
doExpandLast :: TCM a -> TCM a
doExpandLast = localTC $ \ e -> e { envExpandLast = setExpand (envExpandLast e) }
where
setExpand ReallyDontExpandLast = ReallyDontExpandLast
setExpand _ = ExpandLast
dontExpandLast :: TCM a -> TCM a
dontExpandLast = localTC $ \ e -> e { envExpandLast = DontExpandLast }
reallyDontExpandLast :: TCM a -> TCM a
reallyDontExpandLast = localTC $ \ e -> e { envExpandLast = ReallyDontExpandLast }
{-# SPECIALIZE performedSimplification :: TCM a -> TCM a #-}
performedSimplification :: MonadTCEnv m => m a -> m a
performedSimplification = localTC $ \ e -> e { envSimplification = YesSimplification }
{-# SPECIALIZE performedSimplification' :: Simplification -> TCM a -> TCM a #-}
performedSimplification' :: MonadTCEnv m => Simplification -> m a -> m a
performedSimplification' simpl = localTC $ \ e -> e { envSimplification = simpl `mappend` envSimplification e }
getSimplification :: MonadTCEnv m => m Simplification
getSimplification = asksTC envSimplification
updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
updateAllowedReductions f e = e { envAllowedReductions = f (envAllowedReductions e) }
modifyAllowedReductions :: MonadTCEnv m => (AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions = localTC . updateAllowedReductions
putAllowedReductions :: MonadTCEnv m => AllowedReductions -> m a -> m a
putAllowedReductions = modifyAllowedReductions . const
onlyReduceProjections :: MonadTCEnv m => m a -> m a
onlyReduceProjections = putAllowedReductions [ProjectionReductions]
allowAllReductions :: MonadTCEnv m => m a -> m a
allowAllReductions = putAllowedReductions allReductions
allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a
allowNonTerminatingReductions = putAllowedReductions $ [NonTerminatingReductions] ++ allReductions
onlyReduceTypes :: MonadTCEnv m => m a -> m a
onlyReduceTypes = putAllowedReductions [TypeLevelReductions]
typeLevelReductions :: MonadTCEnv m => m a -> m a
typeLevelReductions = modifyAllowedReductions $ \reds -> if
| TypeLevelReductions `elem` reds ->
applyWhen (NonTerminatingReductions `elem` reds) (NonTerminatingReductions:) allReductions
| otherwise -> reds
insideDotPattern :: TCM a -> TCM a
insideDotPattern = localTC $ \ e -> e { envInsideDotPattern = True }
isInsideDotPattern :: TCM Bool
isInsideDotPattern = asksTC envInsideDotPattern
callByName :: TCM a -> TCM a
callByName = localTC $ \ e -> e { envCallByNeed = False }