    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Monad.Mutual where

    import Prelude hiding (null)

    import qualified Data.Set as Set
    import qualified Data.IntMap as IntMap

    import Agda.Syntax.Info as Info
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.State

    import Agda.Utils.Null

    noMutualBlock :: TCM a -> TCM a
    noMutualBlock :: forall a. TCM a -> TCM a
    noMutualBlock = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a. (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 = 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
      mi <- (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe MutualId
    envMutualBlock
      case mi of
        Maybe MutualId
    Nothing -> do
          i <- TCMT IO MutualId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
          localTC (\ TCEnv
    e -> TCEnv
    e { envMutualBlock = Just i }) $ m 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 if non-existing.

    insertMutualBlockInfo :: MutualId -> Info.MutualInfo -> TCM ()
    insertMutualBlockInfo :: MutualId -> MutualInfo -> TCM ()
    insertMutualBlockInfo (MutualId Word32
    i) MutualInfo
    info =
      (MutualBlocks -> f MutualBlocks) -> TCState -> f TCState
    Lens' TCState MutualBlocks
    stMutualBlocks Lens' TCState MutualBlocks
    -> (MutualBlocks -> MutualBlocks) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` (Maybe MutualBlock -> Maybe MutualBlock)
    -> Key -> MutualBlocks -> MutualBlocks
    forall a. (Maybe a -> Maybe a) -> Key -> IntMap a -> IntMap a
    IntMap.alter Maybe MutualBlock -> Maybe MutualBlock
    f (Word32 -> Key
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word32
    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
    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 m :: MutualId
    m@(MutualId Word32
    i) QName
    x = do
      (MutualBlocks -> f MutualBlocks) -> TCState -> f TCState
    Lens' TCState MutualBlocks
    stMutualBlocks Lens' TCState MutualBlocks
    -> (MutualBlocks -> MutualBlocks) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` (Maybe MutualBlock -> Maybe MutualBlock)
    -> Key -> MutualBlocks -> MutualBlocks
    forall a. (Maybe a -> Maybe a) -> Key -> IntMap a -> IntMap a
    IntMap.alter Maybe MutualBlock -> Maybe MutualBlock
    f (Word32 -> Key
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word32
    i)
      (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stSignature    Lens' TCState Signature -> (Signature -> Signature) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    x \ Definition
    defn -> Definition
    defn { defMutual = m }
      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 a. a -> TCMT IO a
    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 :: ReadTCState tcm => MutualId -> tcm MutualBlock
    lookupMutualBlock :: forall (tcm :: * -> *).
    ReadTCState tcm =>
    MutualId -> tcm MutualBlock
    lookupMutualBlock (MutualId Word32
    i) =
      MutualBlock -> Key -> MutualBlocks -> MutualBlock
    forall a. a -> Key -> IntMap a -> a
    IntMap.findWithDefault MutualBlock
    forall a. Null a => a
    empty (Word32 -> Key
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word32
    i) (MutualBlocks -> MutualBlock)
    -> tcm MutualBlocks -> tcm MutualBlock
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState MutualBlocks -> tcm MutualBlocks
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (MutualBlocks -> f MutualBlocks) -> TCState -> f TCState
    Lens' TCState MutualBlocks
    stMutualBlocks
        -- can be empty if we ask for the current mutual block and there is none