module Agda.TypeChecking.Monad.Mutual where

import Prelude hiding (null)



import Data.Functor ((<$>))

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 :: TCM a -> TCM a
noMutualBlock = (TCEnv -> TCEnv) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCM a -> TCM a)
-> (TCEnv -> TCEnv) -> TCM a -> TCM 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 :: (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)]
_          -> String -> TCMT IO MutualId
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> TCMT IO MutualId) -> String -> TCMT IO MutualId
forall a b. (a -> b) -> a -> b
$ String
"No mutual block for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x