module Agda.TypeChecking.Monad.Mutual where
import Prelude hiding (null)
import Control.Monad.Reader
import Data.Functor ((<$>))
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Map as Map
import Agda.Syntax.Info as Info
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.Utils.Lens
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow )
noMutualBlock :: TCM a -> TCM a
noMutualBlock = localTC $ \e -> e { envMutualBlock = Nothing }
inMutualBlock :: (MutualId -> TCM a) -> TCM a
inMutualBlock m = do
mi <- asksTC envMutualBlock
case mi of
Nothing -> do
i <- fresh
localTC (\ e -> e { envMutualBlock = Just i }) $ m i
Just i -> m i
setMutualBlockInfo :: MutualId -> Info.MutualInfo -> TCM ()
setMutualBlockInfo mi info = stMutualBlocks `modifyTCLens` Map.alter f mi
where
f Nothing = Just $ MutualBlock info empty
f (Just (MutualBlock _ xs)) = Just $ MutualBlock info xs
insertMutualBlockInfo :: MutualId -> Info.MutualInfo -> TCM ()
insertMutualBlockInfo mi info = stMutualBlocks `modifyTCLens` Map.alter f mi
where
f Nothing = Just $ MutualBlock info empty
f (Just mb@(MutualBlock info0 xs))
| null info0 = Just $ MutualBlock info xs
| otherwise = Just mb
setMutualBlock :: MutualId -> QName -> TCM ()
setMutualBlock i x = do
stMutualBlocks `modifyTCLens` Map.alter f i
stSignature `modifyTCLens` updateDefinition x (\ defn -> defn { defMutual = i })
where
f Nothing = Just $ MutualBlock empty $ Set.singleton x
f (Just (MutualBlock mi xs)) = Just $ MutualBlock mi $ Set.insert x xs
currentOrFreshMutualBlock :: TCM MutualId
currentOrFreshMutualBlock = maybe fresh return =<< asksTC envMutualBlock
lookupMutualBlock :: MutualId -> TCM MutualBlock
lookupMutualBlock mi = do
mbs <- useTC stMutualBlocks
case Map.lookup mi mbs of
Just mb -> return mb
Nothing -> return empty
mutualBlockOf :: QName -> TCM MutualId
mutualBlockOf x = do
mb <- Map.toList <$> useTC stMutualBlocks
case filter (Set.member x . mutualNames . snd) mb of
(i, _) : _ -> return i
_ -> fail $ "No mutual block for " ++ prettyShow x