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 :: TCM MetaStore
getMetaStore = gets stMetaStore
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore f = modify (\ st -> st { stMetaStore = f $ stMetaStore st })
lookupMeta :: 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 :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVar m f =
modify $ \st -> st { stMetaStore = Map.adjust f m $ stMetaStore st }
getMetaPriority :: MetaId -> TCM MetaPriority
getMetaPriority i = mvPriority <$> lookupMeta i
isSortMeta :: MetaId -> TCM Bool
isSortMeta m = do
mv <- lookupMeta m
return $ case mvJudgement mv of
HasType{} -> False
IsSort{} -> True
isInstantiatedMeta :: MetaId -> TCM Bool
isInstantiatedMeta m = do
mv <- lookupMeta m
return $ case mvInstantiation mv of
InstV{} -> True
InstS{} -> True
_ -> False
createMetaInfo :: TCM MetaInfo
createMetaInfo =
do r <- getCurrentRange
buildClosure r
updateMetaVarRange :: MetaId -> Range -> TCM ()
updateMetaVarRange mi r = updateMetaVar mi (setRange r)
addInteractionPoint :: InteractionId -> MetaId -> TCM ()
addInteractionPoint ii mi =
modify $ \s -> s { stInteractionPoints =
Map.insert ii mi $ stInteractionPoints s
}
removeInteractionPoint :: InteractionId -> TCM ()
removeInteractionPoint ii =
modify $ \s -> s { stInteractionPoints =
Map.delete ii $ stInteractionPoints s
}
getInteractionPoints :: TCM [InteractionId]
getInteractionPoints = Map.keys <$> gets stInteractionPoints
getInteractionMetas :: TCM [MetaId]
getInteractionMetas = Map.elems <$> gets stInteractionPoints
isInteractionMeta :: MetaId -> TCM Bool
isInteractionMeta m = fmap (m `elem`) getInteractionMetas
lookupInteractionId :: 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 :: InteractionId -> TCM (Judgement Type MetaId)
judgementInteractionId ii =
do mi <- lookupInteractionId ii
mvJudgement <$> lookupMeta mi
newMeta :: MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> TCM MetaId
newMeta = newMeta' Open
newMeta' :: MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation ->
Judgement Type a -> TCM MetaId
newMeta' inst mi p perm j = do
x <- fresh
let j' = fmap (const x) j
mv = MetaVar mi p perm j' inst Set.empty Instantiable
modify $ \st -> st { stMetaStore = Map.insert x mv $ stMetaStore st }
return x
getInteractionRange :: InteractionId -> TCM Range
getInteractionRange ii = do
mi <- lookupInteractionId ii
getMetaRange mi
getMetaRange :: MetaId -> TCM Range
getMetaRange mi = getRange <$> lookupMeta mi
getInteractionScope :: InteractionId -> TCM ScopeInfo
getInteractionScope ii =
do mi <- lookupInteractionId ii
mv <- lookupMeta mi
return $ getMetaScope mv
withMetaInfo :: MetaInfo -> TCM a -> TCM a
withMetaInfo mI m = enterClosure mI $ \r -> setCurrentRange r m
getInstantiatedMetas :: TCM [MetaId]
getInstantiatedMetas = do
store <- getMetaStore
return [ i | (i, MetaVar{ mvInstantiation = mi }) <- Map.assocs store, isInst mi ]
where
isInst Open = False
isInst OpenIFS = False
isInst (BlockedConst _) = False
isInst (PostponedTypeCheckingProblem _) = False
isInst (InstV _) = True
isInst (InstS _) = True
getOpenMetas :: TCM [MetaId]
getOpenMetas = do
store <- getMetaStore
return [ i | (i, MetaVar{ mvInstantiation = mi }) <- Map.assocs store, isOpen mi ]
where
isOpen Open = True
isOpen OpenIFS = True
isOpen (BlockedConst _) = True
isOpen (PostponedTypeCheckingProblem _) = True
isOpen (InstV _) = False
isOpen (InstS _) = False
listenToMeta :: Listener -> MetaId -> TCM ()
listenToMeta l m =
updateMetaVar m $ \mv -> mv { mvListeners = Set.insert l $ mvListeners mv }
unlistenToMeta :: Listener -> MetaId -> TCM ()
unlistenToMeta l m =
updateMetaVar m $ \mv -> mv { mvListeners = Set.delete l $ mvListeners mv }
getMetaListeners :: MetaId -> TCM [Listener]
getMetaListeners m = Set.toList . mvListeners <$> lookupMeta m
clearMetaListeners :: MetaId -> TCM ()
clearMetaListeners m =
updateMetaVar m $ \mv -> mv { mvListeners = Set.empty }
freezeMetas :: TCM ()
freezeMetas = modifyMetaStore $ Map.map freeze where
freeze :: MetaVariable -> MetaVariable
freeze mvar = mvar { mvFrozen = Frozen }
unfreezeMetas :: TCM ()
unfreezeMetas = modifyMetaStore $ Map.map unfreeze where
unfreeze :: MetaVariable -> MetaVariable
unfreeze mvar = mvar { mvFrozen = Instantiable }
isFrozen :: MetaId -> TCM Bool
isFrozen x = do
mvar <- lookupMeta x
return $ mvFrozen mvar == Frozen