{-# OPTIONS_GHC -Wunused-imports #-}

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.Syntax.Common.Pretty ( prettyShow )

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,
--   possibly overwriting the existing one.

setMutualBlockInfo :: MutualId -> Info.MutualInfo -> TCM ()
setMutualBlockInfo :: MutualId -> MutualInfo -> TCM ()
setMutualBlockInfo MutualId
mi MutualInfo
info = (Map MutualId MutualBlock -> f (Map MutualId MutualBlock))
-> TCState -> f TCState
Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks Lens' TCState (Map MutualId MutualBlock)
-> (Map MutualId MutualBlock -> Map MutualId MutualBlock) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (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 = (Map MutualId MutualBlock -> f (Map MutualId MutualBlock))
-> TCState -> f TCState
Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks Lens' TCState (Map MutualId MutualBlock)
-> (Map MutualId MutualBlock -> Map MutualId MutualBlock) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (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
  (Map MutualId MutualBlock -> f (Map MutualId MutualBlock))
-> TCState -> f TCState
Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks Lens' TCState (Map MutualId MutualBlock)
-> (Map MutualId MutualBlock -> Map MutualId MutualBlock) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (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
  (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 = 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 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
mi = MutualBlock -> MutualId -> Map MutualId MutualBlock -> MutualBlock
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault MutualBlock
forall a. Null a => a
empty MutualId
mi (Map MutualId MutualBlock -> MutualBlock)
-> tcm (Map MutualId MutualBlock) -> tcm MutualBlock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Map MutualId MutualBlock)
-> tcm (Map MutualId MutualBlock)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map MutualId MutualBlock -> f (Map MutualId MutualBlock))
-> TCState -> f TCState
Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks
   -- can be empty if we ask for the current mutual block and there is none

-- | Reverse lookup of a mutual block id for a name.
mutualBlockOf :: QName -> TCM MutualId
mutualBlockOf :: QName -> TCMT IO MutualId
mutualBlockOf QName
x = do
  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' TCState (Map MutualId MutualBlock)
-> TCMT IO (Map MutualId MutualBlock)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map MutualId MutualBlock -> f (Map MutualId MutualBlock))
-> TCState -> f TCState
Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks
  case filter (Set.member x . mutualNames . snd) mb of
    (MutualId
i, MutualBlock
_) : [(MutualId, MutualBlock)]
_ -> MutualId -> TCMT IO MutualId
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MutualId
i
    [(MutualId, MutualBlock)]
_          -> [Char] -> TCMT IO MutualId
forall a. [Char] -> TCMT IO a
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