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 = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envMutualBlock :: Maybe MutualId
envMutualBlock = 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 <- 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 <- forall i (m :: * -> *). MonadFresh i m => m i
fresh
      forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envMutualBlock :: Maybe MutualId
envMutualBlock = forall a. a -> Maybe a
Just MutualId
i }) 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 forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` 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                   = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
info forall a. Null a => a
empty
  f (Just (MutualBlock MutualInfo
_ Set QName
xs)) = forall a. a -> Maybe a
Just 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 forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` 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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
info forall a. Null a => a
empty
  f (Just mb :: MutualBlock
mb@(MutualBlock MutualInfo
info0 Set QName
xs))
    | forall a. Null a => a -> Bool
null MutualInfo
info0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
info Set QName
xs
    | Bool
otherwise  = 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 forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` 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    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                    = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock forall a. Null a => a
empty forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
Set.singleton QName
x
  f (Just (MutualBlock MutualInfo
mi Set QName
xs)) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
mi forall a b. (a -> b) -> a -> b
$ 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 :: TCM MutualId
currentOrFreshMutualBlock = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall i (m :: * -> *). MonadFresh i m => m i
fresh forall (m :: * -> *) a. Monad m => a -> m a
return forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. Null a => a
empty MutualId
mi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map MutualId MutualBlock) TCState
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 -> TCM MutualId
mutualBlockOf QName
x = do
  [(MutualId, MutualBlock)]
mb <- forall k a. Map k a -> [(k, a)]
Map.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks
  case forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> Set a -> Bool
Set.member QName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. MutualBlock -> Set QName
mutualNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(MutualId, MutualBlock)]
mb of
    (MutualId
i, MutualBlock
_) : [(MutualId, MutualBlock)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return MutualId
i
    [(MutualId, MutualBlock)]
_          -> forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"No mutual block for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x