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 :: TCM a -> TCM a
noMutualBlock = local $ \e -> e { envMutualBlock = Nothing }
inMutualBlock :: 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 :: 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 :: TCM [Set QName]
getMutualBlocks = gets $ Map.elems . stMutualBlocks
currentMutualBlock :: TCM MutualId
currentMutualBlock = maybe fresh return =<< asks envMutualBlock
lookupMutualBlock :: MutualId -> TCM (Set QName)
lookupMutualBlock mi = do
mb <- gets stMutualBlocks
case Map.lookup mi mb of
Just qs -> return qs
Nothing -> return Set.empty
findMutualBlock :: 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