1 2module Agda.TypeChecking.Monad.Mutual where 3 4import Prelude hiding (null) 5 6 7 8 9import qualified Data.Set as Set 10import qualified Data.Map as Map 11 12import Agda.Syntax.Info as Info 13import Agda.Syntax.Internal 14import Agda.TypeChecking.Monad.Base 15import Agda.TypeChecking.Monad.State 16 17import Agda.Utils.Null 18import Agda.Utils.Pretty ( prettyShow ) 19 20noMutualBlock :: TCM a -> TCM a 21noMutualBlock = localTC $ \e -> e { envMutualBlock = Nothing } 22 23-- | Pass the current mutual block id 24-- or create a new mutual block if we are not already inside on. 25inMutualBlock :: (MutualId -> TCM a) -> TCM a 26inMutualBlock m = do 27 mi <- asksTC envMutualBlock 28 case mi of 29 Nothing -> do 30 i <- fresh 31 localTC (\ e -> e { envMutualBlock = Just i }) $ m i 32 -- Don't create a new mutual block if we're already inside one. 33 Just i -> m i 34 35-- | Set the mutual block info for a block, 36-- possibly overwriting the existing one. 37 38setMutualBlockInfo :: MutualId -> Info.MutualInfo -> TCM () 39setMutualBlockInfo mi info = stMutualBlocks `modifyTCLens` Map.alter f mi 40 where 41 f Nothing = Just $ MutualBlock info empty 42 f (Just (MutualBlock _ xs)) = Just $ MutualBlock info xs 43 44-- | Set the mutual block info for a block if non-existing. 45 46insertMutualBlockInfo :: MutualId -> Info.MutualInfo -> TCM () 47insertMutualBlockInfo mi info = stMutualBlocks `modifyTCLens` Map.alter f mi 48 where 49 f Nothing = Just $ MutualBlock info empty 50 f (Just mb@(MutualBlock info0 xs)) 51 | null info0 = Just $ MutualBlock info xs 52 | otherwise = Just mb 53 54-- | Set the mutual block for a definition. 55 56setMutualBlock :: MutualId -> QName -> TCM () 57setMutualBlock i x = do 58 stMutualBlocks `modifyTCLens` Map.alter f i 59 stSignature `modifyTCLens` updateDefinition x (\ defn -> defn { defMutual = i }) 60 where 61 f Nothing = Just $ MutualBlock empty $ Set.singleton x 62 f (Just (MutualBlock mi xs)) = Just $ MutualBlock mi $ Set.insert x xs 63 64-- | Get the current mutual block, if any, otherwise a fresh mutual 65-- block is returned. 66currentOrFreshMutualBlock :: TCM MutualId 67currentOrFreshMutualBlock = maybe fresh return =<< asksTC envMutualBlock 68 69lookupMutualBlock :: MutualId -> TCM MutualBlock 70lookupMutualBlock mi = do 71 mbs <- useTC stMutualBlocks 72 case Map.lookup mi mbs of 73 Just mb -> return mb 74 Nothing -> return empty -- can end up here if we ask for the current mutual block and there is none 75 76-- | Reverse lookup of a mutual block id for a names. 77mutualBlockOf :: QName -> TCM MutualId 78mutualBlockOf x = do 79 mb <- Map.toList <$> useTC stMutualBlocks 80 case filter (Set.member x . mutualNames . snd) mb of 81 (i, _) : _ -> return i 82 _ -> fail $ "No mutual block for " ++ prettyShow x 83