{-# 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