module Agda.TypeChecking.Monad.MetaVars where
import Control.Applicative
import Control.Monad.State
import Control.Monad.Reader
import qualified Data.Map as Map
import qualified Data.Set as Set
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Signature
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Open
import Agda.TypeChecking.Substitute
import Agda.Utils.Monad
import Agda.Utils.Fresh
import Agda.Utils.Permutation
#include "../../undefined.h"
import Agda.Utils.Impossible
getMetaStore :: MonadTCM tcm => tcm MetaStore
getMetaStore = gets stMetaStore
lookupMeta :: MonadTCM tcm => MetaId -> tcm MetaVariable
lookupMeta m =
do mmv <- Map.lookup m <$> getMetaStore
case mmv of
Just mv -> return mv
_ -> fail $ "no such meta variable " ++ show m
updateMetaVar :: MonadTCM tcm => MetaId -> (MetaVariable -> MetaVariable) -> tcm ()
updateMetaVar m f =
modify $ \st -> st { stMetaStore = Map.adjust f m $ stMetaStore st }
getMetaPriority :: MonadTCM tcm => MetaId -> tcm MetaPriority
getMetaPriority i = mvPriority <$> lookupMeta i
isSortMeta :: MonadTCM tcm => MetaId -> tcm Bool
isSortMeta m = do
mv <- lookupMeta m
return $ case mvJudgement mv of
HasType{} -> False
IsSort{} -> True
isInstantiatedMeta :: MonadTCM tcm => MetaId -> tcm Bool
isInstantiatedMeta m = do
mv <- lookupMeta m
return $ case mvInstantiation mv of
InstV{} -> True
InstS{} -> True
_ -> False
createMetaInfo :: MonadTCM tcm => tcm MetaInfo
createMetaInfo =
do r <- getCurrentRange
buildClosure r
updateMetaVarRange :: MonadTCM tcm => MetaId -> Range -> tcm ()
updateMetaVarRange mi r = updateMetaVar mi (setRange r)
addInteractionPoint :: MonadTCM tcm => InteractionId -> MetaId -> tcm ()
addInteractionPoint ii mi =
modify $ \s -> s { stInteractionPoints =
Map.insert ii mi $ stInteractionPoints s
}
removeInteractionPoint :: MonadTCM tcm => InteractionId -> tcm ()
removeInteractionPoint ii =
modify $ \s -> s { stInteractionPoints =
Map.delete ii $ stInteractionPoints s
}
getInteractionPoints :: MonadTCM tcm => tcm [InteractionId]
getInteractionPoints = Map.keys <$> gets stInteractionPoints
getInteractionMetas :: MonadTCM tcm => tcm [MetaId]
getInteractionMetas = Map.elems <$> gets stInteractionPoints
isInteractionMeta :: MonadTCM tcm => MetaId -> tcm Bool
isInteractionMeta m = fmap (m `elem`) getInteractionMetas
lookupInteractionId :: MonadTCM tcm => InteractionId -> tcm MetaId
lookupInteractionId ii =
do mmi <- Map.lookup ii <$> gets stInteractionPoints
case mmi of
Just mi -> return mi
_ -> fail $ "no such interaction point: " ++ show ii
judgementInteractionId :: MonadTCM tcm => InteractionId -> tcm (Judgement Type MetaId)
judgementInteractionId ii =
do mi <- lookupInteractionId ii
mvJudgement <$> lookupMeta mi
newMeta :: MonadTCM tcm => MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> tcm MetaId
newMeta = newMeta' Open
newMeta' :: MonadTCM tcm => MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation ->
Judgement Type a -> tcm MetaId
newMeta' inst mi p perm j = do
x <- fresh
let mv = MetaVar mi p perm (fmap (const x) j) inst Set.empty
modify $ \st -> st { stMetaStore = Map.insert x mv $ stMetaStore st }
return x
getInteractionRange :: MonadTCM tcm => InteractionId -> tcm Range
getInteractionRange ii = do
mi <- lookupInteractionId ii
getMetaRange mi
getMetaRange :: MonadTCM tcm => MetaId -> tcm Range
getMetaRange mi = getRange <$> lookupMeta mi
getInteractionScope :: MonadTCM tcm => InteractionId -> tcm ScopeInfo
getInteractionScope ii =
do mi <- lookupInteractionId ii
mv <- lookupMeta mi
return $ getMetaScope mv
withMetaInfo :: MonadTCM tcm => MetaInfo -> tcm a -> tcm a
withMetaInfo mI m = enterClosure mI $ \r -> setCurrentRange r m
getInstantiatedMetas :: MonadTCM tcm => tcm [MetaId]
getInstantiatedMetas = do
store <- getMetaStore
return [ i | (i, MetaVar{ mvInstantiation = mi }) <- Map.assocs store, isInst mi ]
where
isInst Open = False
isInst (BlockedConst _) = False
isInst (PostponedTypeCheckingProblem _) = False
isInst (InstV _) = True
isInst (InstS _) = True
getOpenMetas :: MonadTCM tcm => tcm [MetaId]
getOpenMetas = do
store <- getMetaStore
return [ i | (i, MetaVar{ mvInstantiation = mi }) <- Map.assocs store, isOpen mi ]
where
isOpen Open = True
isOpen (BlockedConst _) = True
isOpen (PostponedTypeCheckingProblem _) = True
isOpen (InstV _) = False
isOpen (InstS _) = False
listenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm ()
listenToMeta l m =
updateMetaVar m $ \mv -> mv { mvListeners = Set.insert l $ mvListeners mv }
unlistenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm ()
unlistenToMeta l m =
updateMetaVar m $ \mv -> mv { mvListeners = Set.delete l $ mvListeners mv }
getMetaListeners :: MonadTCM tcm => MetaId -> tcm [MetaId]
getMetaListeners m = Set.toList . mvListeners <$> lookupMeta m
clearMetaListeners :: MonadTCM tcm => MetaId -> tcm ()
clearMetaListeners m =
updateMetaVar m $ \mv -> mv { mvListeners = Set.empty }