module Agda.TypeChecking.Monad.MetaVars where
import Control.Applicative
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.Foldable as Fold
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Options (reportSLn)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Functor ((<.>))
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Tuple
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
dontAssignMetas :: TCM a -> TCM a
dontAssignMetas = local $ \ env -> env { envAssignMetas = False }
getMetaStore :: TCM MetaStore
getMetaStore = use stMetaStore
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore f = stMetaStore %= f
lookupMeta :: MetaId -> TCM MetaVariable
lookupMeta m = fromMaybeM failure $ Map.lookup m <$> getMetaStore
where failure = fail $ "no such meta variable " ++ prettyShow m
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVar m f = modifyMetaStore $ Map.adjust f m
getMetaPriority :: MetaId -> TCM MetaPriority
getMetaPriority = mvPriority <.> lookupMeta
isSortMeta :: MetaId -> TCM Bool
isSortMeta m = isSortMeta_ <$> lookupMeta m
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ mv = case mvJudgement mv of
HasType{} -> False
IsSort{} -> True
getMetaType :: MetaId -> TCM Type
getMetaType m = do
mv <- lookupMeta m
return $ case mvJudgement mv of
HasType{ jMetaType = t } -> t
IsSort{} -> __IMPOSSIBLE__
getMetaTypeInContext :: MetaId -> TCM Type
getMetaTypeInContext m = do
MetaVar{ mvJudgement = j, mvPermutation = p } <- lookupMeta m
case j of
HasType{ jMetaType = t } -> do
vs <- getContextArgs
piApplyM t $ permute (takeP (size vs) p) vs
IsSort{} -> __IMPOSSIBLE__
class IsInstantiatedMeta a where
isInstantiatedMeta :: a -> TCM Bool
instance IsInstantiatedMeta MetaId where
isInstantiatedMeta m = isJust <$> isInstantiatedMeta' m
instance IsInstantiatedMeta Term where
isInstantiatedMeta = loop where
loop v =
case ignoreSharing v of
MetaV x _ -> isInstantiatedMeta x
DontCare v -> loop v
Level l -> isInstantiatedMeta l
Lam _ b -> isInstantiatedMeta b
Con _ vs -> isInstantiatedMeta vs
_ -> __IMPOSSIBLE__
instance IsInstantiatedMeta Level where
isInstantiatedMeta (Max ls) = isInstantiatedMeta ls
instance IsInstantiatedMeta PlusLevel where
isInstantiatedMeta (Plus n l) | n == 0 = isInstantiatedMeta l
isInstantiatedMeta _ = __IMPOSSIBLE__
instance IsInstantiatedMeta LevelAtom where
isInstantiatedMeta (MetaLevel x es) = isInstantiatedMeta x
isInstantiatedMeta _ = __IMPOSSIBLE__
instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where
isInstantiatedMeta = andM . map isInstantiatedMeta
instance IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) where
isInstantiatedMeta = isInstantiatedMeta . maybeToList
instance IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) where
isInstantiatedMeta = isInstantiatedMeta . unArg
instance IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) where
isInstantiatedMeta = isInstantiatedMeta . unAbs
isInstantiatedMeta' :: MetaId -> TCM (Maybe Term)
isInstantiatedMeta' m = do
mv <- lookupMeta m
return $ case mvInstantiation mv of
InstV tel v -> Just $ foldr mkLam v tel
InstS v -> Just v
_ -> Nothing
createMetaInfo :: TCM MetaInfo
createMetaInfo = createMetaInfo' RunMetaOccursCheck
createMetaInfo' :: RunMetaOccursCheck -> TCM MetaInfo
createMetaInfo' b = do
r <- getCurrentRange
cl <- buildClosure r
return MetaInfo
{ miClosRange = cl
, miMetaOccursCheck = b
, miNameSuggestion = ""
}
setValueMetaName :: Term -> MetaNameSuggestion -> TCM ()
setValueMetaName v s = do
case ignoreSharing v of
MetaV mi _ -> setMetaNameSuggestion mi s
u -> do
reportSLn "tc.meta.name" 70 $
"cannot set meta name; newMeta returns " ++ show u
return ()
getMetaNameSuggestion :: MetaId -> TCM MetaNameSuggestion
getMetaNameSuggestion mi = miNameSuggestion . mvInfo <$> lookupMeta mi
setMetaNameSuggestion :: MetaId -> MetaNameSuggestion -> TCM ()
setMetaNameSuggestion mi s = do
reportSLn "tc.meta.name" 20 $
"setting name of meta " ++ prettyShow mi ++ " to " ++ s
updateMetaVar mi $ \ mvar ->
mvar { mvInfo = (mvInfo mvar) { miNameSuggestion = s }}
updateMetaVarRange :: MetaId -> Range -> TCM ()
updateMetaVarRange mi r = updateMetaVar mi (setRange r)
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
modifyInteractionPoints f =
stInteractionPoints %= f
registerInteractionPoint :: Range -> Maybe Nat -> TCM InteractionId
registerInteractionPoint r maybeId = do
ii <- case maybeId of
Just i -> return $ InteractionId i
Nothing -> fresh
m <- use stInteractionPoints
let ip = InteractionPoint { ipRange = r, ipMeta = Nothing }
case Map.insertLookupWithKey (\ key new old -> old) ii ip m of
(Just ip0, _)
| ipRange ip /= ipRange ip0 -> __IMPOSSIBLE__
| otherwise -> return ii
(Nothing, m') -> do
modifyInteractionPoints (const m')
return ii
connectInteractionPoint :: InteractionId -> MetaId -> TCM ()
connectInteractionPoint ii mi = do
m <- use stInteractionPoints
let ip = InteractionPoint { ipRange = __IMPOSSIBLE__, ipMeta = Just mi }
case Map.insertLookupWithKey (\ key new old -> new { ipRange = ipRange old }) ii ip m of
(Nothing, _) -> __IMPOSSIBLE__
(Just _, m') -> modifyInteractionPoints $ const m'
removeInteractionPoint :: InteractionId -> TCM ()
removeInteractionPoint ii = do
scope <- getInteractionScope ii
modifyInteractionPoints $ Map.delete ii
getInteractionPoints :: TCM [InteractionId]
getInteractionPoints = Map.keys <$> use stInteractionPoints
getInteractionMetas :: TCM [MetaId]
getInteractionMetas = mapMaybe ipMeta . Map.elems <$> use stInteractionPoints
getInteractionIdsAndMetas :: TCM [(InteractionId,MetaId)]
getInteractionIdsAndMetas = mapMaybe f . Map.toList <$> use stInteractionPoints
where f (ii, ip) = (ii,) <$> ipMeta ip
isInteractionMeta :: MetaId -> TCM (Maybe InteractionId)
isInteractionMeta x = lookup x . map swap <$> getInteractionIdsAndMetas
lookupInteractionPoint :: InteractionId -> TCM InteractionPoint
lookupInteractionPoint ii =
fromMaybeM err $ Map.lookup ii <$> use stInteractionPoints
where
err = fail $ "no such interaction point: " ++ show ii
lookupInteractionId :: InteractionId -> TCM MetaId
lookupInteractionId ii = fromMaybeM err2 $ ipMeta <$> lookupInteractionPoint ii
where
err2 = typeError $ GenericError $ "No type nor action available for hole " ++ show ii
newMeta :: MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId
newMeta = newMeta' Open
newMeta' :: MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation ->
Judgement a -> TCM MetaId
newMeta' inst mi p perm j = do
x <- fresh
let j' = j { jMetaId = x }
mv = MetaVar mi p perm j' inst Set.empty Instantiable
stMetaStore %= Map.insert x mv
return x
getInteractionRange :: InteractionId -> TCM Range
getInteractionRange = ipRange <.> lookupInteractionPoint
getMetaRange :: MetaId -> TCM Range
getMetaRange = getRange <.> lookupMeta
getInteractionScope :: InteractionId -> TCM ScopeInfo
getInteractionScope = getMetaScope <.> lookupMeta <=< lookupInteractionId
withMetaInfo' :: MetaVariable -> TCM a -> TCM a
withMetaInfo' mv = withMetaInfo (miClosRange $ mvInfo mv)
withMetaInfo :: Closure Range -> TCM a -> TCM a
withMetaInfo mI cont = enterClosure mI $ \ r ->
setCurrentRange r cont
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 }
withFreezeMetas :: TCM a -> TCM a
withFreezeMetas cont = do
ms <- Set.fromList <$> freezeMetas
x <- cont
unfreezeMetas' (`Set.member` ms)
return x
freezeMetas :: TCM [MetaId]
freezeMetas = execWriterT $ stMetaStore %== Map.traverseWithKey freeze
where
freeze :: Monad m => MetaId -> MetaVariable -> WriterT [MetaId] m MetaVariable
freeze m mvar
| mvFrozen mvar == Frozen = return mvar
| otherwise = do
tell [m]
return $ mvar { mvFrozen = Frozen }
unfreezeMetas :: TCM ()
unfreezeMetas = unfreezeMetas' $ const True
unfreezeMetas' :: (MetaId -> Bool) -> TCM ()
unfreezeMetas' cond = modifyMetaStore $ Map.mapWithKey unfreeze where
unfreeze :: MetaId -> MetaVariable -> MetaVariable
unfreeze m mvar
| cond m = mvar { mvFrozen = Instantiable }
| otherwise = mvar
isFrozen :: MetaId -> TCM Bool
isFrozen x = do
mvar <- lookupMeta x
return $ mvFrozen mvar == Frozen
class UnFreezeMeta a where
unfreezeMeta :: a -> TCM ()
instance UnFreezeMeta MetaId where
unfreezeMeta x = do
updateMetaVar x $ \ mv -> mv { mvFrozen = Instantiable }
unfreezeMeta =<< do jMetaType . mvJudgement <$> lookupMeta x
instance UnFreezeMeta Type where
unfreezeMeta (El s t) = unfreezeMeta s >> unfreezeMeta t
instance UnFreezeMeta Term where
unfreezeMeta (Shared p) = unfreezeMeta $ derefPtr p
unfreezeMeta (MetaV x _) = unfreezeMeta x
unfreezeMeta (Sort s) = unfreezeMeta s
unfreezeMeta (Level l) = unfreezeMeta l
unfreezeMeta (DontCare t) = unfreezeMeta t
unfreezeMeta (Lam _ v) = unfreezeMeta v
unfreezeMeta _ = return ()
instance UnFreezeMeta Sort where
unfreezeMeta (Type l) = unfreezeMeta l
unfreezeMeta _ = return ()
instance UnFreezeMeta Level where
unfreezeMeta (Max ls) = unfreezeMeta ls
instance UnFreezeMeta PlusLevel where
unfreezeMeta (Plus _ a) = unfreezeMeta a
unfreezeMeta ClosedLevel{} = return ()
instance UnFreezeMeta LevelAtom where
unfreezeMeta (MetaLevel x _) = unfreezeMeta x
unfreezeMeta (BlockedLevel _ t) = unfreezeMeta t
unfreezeMeta (NeutralLevel _ t) = unfreezeMeta t
unfreezeMeta (UnreducedLevel t) = unfreezeMeta t
instance UnFreezeMeta a => UnFreezeMeta [a] where
unfreezeMeta = mapM_ unfreezeMeta
instance UnFreezeMeta a => UnFreezeMeta (Abs a) where
unfreezeMeta = Fold.mapM_ unfreezeMeta