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