    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