module Agda.TypeChecking.Monad.Mutual where
import Control.Monad.Reader
import Control.Monad.State
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.Utils.Fresh
import Agda.Utils.Impossible
#include "../../undefined.h"
noMutualBlock :: MonadTCM tcm => tcm a -> tcm a
noMutualBlock = local $ \e -> e { envMutualBlock = Nothing }
inMutualBlock :: MonadTCM tcm => tcm a -> tcm a
inMutualBlock m = do
mi <- asks envMutualBlock
case mi of
Nothing -> do
i <- fresh
flip local m $ \e -> e { envMutualBlock = Just i }
Just _ -> m
setMutualBlock :: MonadTCM tcm => MutualId -> QName -> tcm ()
setMutualBlock i x = do
modify $ \s -> s { stMutualBlocks = Map.insertWith Set.union i (Set.singleton x) $ stMutualBlocks s
, stSignature = (stSignature s)
{ sigDefinitions = setMutId x i $ sigDefinitions $ stSignature s
}
}
where
setMutId x i = flip Map.adjust x $ \defn -> defn { defMutual = i }
getMutualBlocks :: MonadTCM tcm => tcm [Set QName]
getMutualBlocks = gets $ Map.elems . stMutualBlocks
currentMutualBlock :: MonadTCM tcm => tcm MutualId
currentMutualBlock = maybe fresh return =<< asks envMutualBlock
lookupMutualBlock :: MonadTCM tcm => MutualId -> tcm (Set QName)
lookupMutualBlock mi = do
mb <- gets stMutualBlocks
case Map.lookup mi mb of
Just qs -> return qs
Nothing -> fail $ "No such mutual block: " ++ show mi
findMutualBlock :: MonadTCM tcm => QName -> tcm (Set QName)
findMutualBlock f = do
bs <- getMutualBlocks
case filter (Set.member f) bs of
[] -> fail $ "No mutual block for " ++ show f
b : _ -> return b