module Agda.TypeChecking.Monad.Mutual where

import Prelude hiding (null)




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.Null
import Agda.Utils.Pretty ( prettyShow )

noMutualBlock :: TCM a -> TCM a
noMutualBlock :: forall a. TCM a -> TCM a
noMutualBlock = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envMutualBlock :: Maybe MutualId
envMutualBlock = Maybe MutualId
forall a. Maybe a
Nothing }

-- | Pass the current mutual block id
--   or create a new mutual block if we are not already inside on.
inMutualBlock :: (MutualId -> TCM a) -> TCM a
inMutualBlock :: forall a. (MutualId -> TCM a) -> TCM a
inMutualBlock MutualId -> TCM a
m = do
  Maybe MutualId
mi <- (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock
  case Maybe MutualId
mi of
    Maybe MutualId
Nothing -> do
      MutualId
i <- TCMT IO MutualId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
      (TCEnv -> TCEnv) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envMutualBlock :: Maybe MutualId
envMutualBlock = MutualId -> Maybe MutualId
forall a. a -> Maybe a
Just MutualId
i }) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ MutualId -> TCM a
m MutualId
i
    -- Don't create a new mutual block if we're already inside one.
    Just MutualId
i -> MutualId -> TCM a
m MutualId
i

-- | Set the mutual block info for a block,
--   possibly overwriting the existing one.

setMutualBlockInfo :: MutualId -> Info.MutualInfo -> TCM ()
setMutualBlockInfo :: MutualId -> MutualInfo -> TCM ()
setMutualBlockInfo MutualId
mi MutualInfo
info = Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks Lens' (Map MutualId MutualBlock) TCState
-> (Map MutualId MutualBlock -> Map MutualId MutualBlock) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (Maybe MutualBlock -> Maybe MutualBlock)
-> MutualId -> Map MutualId MutualBlock -> Map MutualId MutualBlock
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter Maybe MutualBlock -> Maybe MutualBlock
f MutualId
mi
  where
  f :: Maybe MutualBlock -> Maybe MutualBlock
f Maybe MutualBlock
Nothing                   = MutualBlock -> Maybe MutualBlock
forall a. a -> Maybe a
Just (MutualBlock -> Maybe MutualBlock)
-> MutualBlock -> Maybe MutualBlock
forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
info Set QName
forall a. Null a => a
empty
  f (Just (MutualBlock MutualInfo
_ Set QName
xs)) = MutualBlock -> Maybe MutualBlock
forall a. a -> Maybe a
Just (MutualBlock -> Maybe MutualBlock)
-> MutualBlock -> Maybe MutualBlock
forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
info Set QName
xs

-- | Set the mutual block info for a block if non-existing.

insertMutualBlockInfo :: MutualId -> Info.MutualInfo -> TCM ()
insertMutualBlockInfo :: MutualId -> MutualInfo -> TCM ()
insertMutualBlockInfo MutualId
mi MutualInfo
info = Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks Lens' (Map MutualId MutualBlock) TCState
-> (Map MutualId MutualBlock -> Map MutualId MutualBlock) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (Maybe MutualBlock -> Maybe MutualBlock)
-> MutualId -> Map MutualId MutualBlock -> Map MutualId MutualBlock
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter Maybe MutualBlock -> Maybe MutualBlock
f MutualId
mi
  where
  f :: Maybe MutualBlock -> Maybe MutualBlock
f Maybe MutualBlock
Nothing = MutualBlock -> Maybe MutualBlock
forall a. a -> Maybe a
Just (MutualBlock -> Maybe MutualBlock)
-> MutualBlock -> Maybe MutualBlock
forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
info Set QName
forall a. Null a => a
empty
  f (Just mb :: MutualBlock
mb@(MutualBlock MutualInfo
info0 Set QName
xs))
    | MutualInfo -> Bool
forall a. Null a => a -> Bool
null MutualInfo
info0 = MutualBlock -> Maybe MutualBlock
forall a. a -> Maybe a
Just (MutualBlock -> Maybe MutualBlock)
-> MutualBlock -> Maybe MutualBlock
forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
info Set QName
xs
    | Bool
otherwise  = MutualBlock -> Maybe MutualBlock
forall a. a -> Maybe a
Just MutualBlock
mb

-- | Set the mutual block for a definition.

setMutualBlock :: MutualId -> QName -> TCM ()
setMutualBlock :: MutualId -> QName -> TCM ()
setMutualBlock MutualId
i QName
x = do
  Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks Lens' (Map MutualId MutualBlock) TCState
-> (Map MutualId MutualBlock -> Map MutualId MutualBlock) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (Maybe MutualBlock -> Maybe MutualBlock)
-> MutualId -> Map MutualId MutualBlock -> Map MutualId MutualBlock
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter Maybe MutualBlock -> Maybe MutualBlock
f MutualId
i
  Lens' Signature TCState
stSignature    Lens' Signature TCState -> (Signature -> Signature) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
x (\ Definition
defn -> Definition
defn { defMutual :: MutualId
defMutual = MutualId
i })
  where
  f :: Maybe MutualBlock -> Maybe MutualBlock
f Maybe MutualBlock
Nothing                    = MutualBlock -> Maybe MutualBlock
forall a. a -> Maybe a
Just (MutualBlock -> Maybe MutualBlock)
-> MutualBlock -> Maybe MutualBlock
forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
forall a. Null a => a
empty (Set QName -> MutualBlock) -> Set QName -> MutualBlock
forall a b. (a -> b) -> a -> b
$ QName -> Set QName
forall a. a -> Set a
Set.singleton QName
x
  f (Just (MutualBlock MutualInfo
mi Set QName
xs)) = MutualBlock -> Maybe MutualBlock
forall a. a -> Maybe a
Just (MutualBlock -> Maybe MutualBlock)
-> MutualBlock -> Maybe MutualBlock
forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
mi (Set QName -> MutualBlock) -> Set QName -> MutualBlock
forall a b. (a -> b) -> a -> b
$ QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
x Set QName
xs

-- | Get the current mutual block, if any, otherwise a fresh mutual
-- block is returned.
currentOrFreshMutualBlock :: TCM MutualId
currentOrFreshMutualBlock :: TCMT IO MutualId
currentOrFreshMutualBlock = TCMT IO MutualId
-> (MutualId -> TCMT IO MutualId)
-> Maybe MutualId
-> TCMT IO MutualId
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO MutualId
forall i (m :: * -> *). MonadFresh i m => m i
fresh MutualId -> TCMT IO MutualId
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe MutualId -> TCMT IO MutualId)
-> TCMT IO (Maybe MutualId) -> TCMT IO MutualId
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock

lookupMutualBlock :: MutualId -> TCM MutualBlock
lookupMutualBlock :: MutualId -> TCM MutualBlock
lookupMutualBlock MutualId
mi = do
  Map MutualId MutualBlock
mbs <- Lens' (Map MutualId MutualBlock) TCState
-> TCMT IO (Map MutualId MutualBlock)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks
  case MutualId -> Map MutualId MutualBlock -> Maybe MutualBlock
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup MutualId
mi Map MutualId MutualBlock
mbs of
    Just MutualBlock
mb -> MutualBlock -> TCM MutualBlock
forall (m :: * -> *) a. Monad m => a -> m a
return MutualBlock
mb
    Maybe MutualBlock
Nothing -> MutualBlock -> TCM MutualBlock
forall (m :: * -> *) a. Monad m => a -> m a
return MutualBlock
forall a. Null a => a
empty -- can end up here if we ask for the current mutual block and there is none

-- | Reverse lookup of a mutual block id for a names.
mutualBlockOf :: QName -> TCM MutualId
mutualBlockOf :: QName -> TCMT IO MutualId
mutualBlockOf QName
x = do
  [(MutualId, MutualBlock)]
mb <- Map MutualId MutualBlock -> [(MutualId, MutualBlock)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map MutualId MutualBlock -> [(MutualId, MutualBlock)])
-> TCMT IO (Map MutualId MutualBlock)
-> TCMT IO [(MutualId, MutualBlock)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map MutualId MutualBlock) TCState
-> TCMT IO (Map MutualId MutualBlock)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks
  case ((MutualId, MutualBlock) -> Bool)
-> [(MutualId, MutualBlock)] -> [(MutualId, MutualBlock)]
forall a. (a -> Bool) -> [a] -> [a]
filter (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x (Set QName -> Bool)
-> ((MutualId, MutualBlock) -> Set QName)
-> (MutualId, MutualBlock)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MutualBlock -> Set QName
mutualNames (MutualBlock -> Set QName)
-> ((MutualId, MutualBlock) -> MutualBlock)
-> (MutualId, MutualBlock)
-> Set QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MutualId, MutualBlock) -> MutualBlock
forall a b. (a, b) -> b
snd) [(MutualId, MutualBlock)]
mb of
    (MutualId
i, MutualBlock
_) : [(MutualId, MutualBlock)]
_ -> MutualId -> TCMT IO MutualId
forall (m :: * -> *) a. Monad m => a -> m a
return MutualId
i
    [(MutualId, MutualBlock)]
_          -> [Char] -> TCMT IO MutualId
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> TCMT IO MutualId) -> [Char] -> TCMT IO MutualId
forall a b. (a -> b) -> a -> b
$ [Char]
"No mutual block for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x