{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Monad.MetaVars where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Foldable as Fold
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
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.Debug (reportSLn)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Substitute
import {-# SOURCE #-} Agda.TypeChecking.Telescope
import Agda.Utils.Functor ((<.>))
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Tuple
import Agda.Utils.Size
import qualified Agda.Utils.Maybe.Strict as Strict
#include "undefined.h"
import Agda.Utils.Impossible
dontAssignMetas :: TCM a -> TCM a
dontAssignMetas cont = do
reportSLn "tc.meta" 45 $ "don't assign metas"
local (\ env -> env { envAssignMetas = False }) cont
getMetaStore :: TCM MetaStore
getMetaStore = use stMetaStore
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore f = stMetaStore %= f
metasCreatedBy :: TCM a -> TCM (a, Set MetaId)
metasCreatedBy m = do
before <- Map.keysSet <$> use stMetaStore
a <- m
after <- Map.keysSet <$> use stMetaStore
return (a, after Set.\\ before)
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 v of
MetaV x _ -> isInstantiatedMeta x
DontCare v -> loop v
Level l -> isInstantiatedMeta l
Lam _ b -> isInstantiatedMeta b
Con _ _ es | Just vs <- allApplyElims es -> 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
_ -> Nothing
allMetas :: TermLike a => a -> [MetaId]
allMetas = foldTerm metas
where
metas (MetaV m _) = [m]
metas (Level l) = levelMetas l
metas _ = []
levelMetas (Max as) = concatMap plusLevelMetas as
plusLevelMetas ClosedLevel{} = []
plusLevelMetas (Plus _ l) = levelAtomMetas l
levelAtomMetas (MetaLevel m _) = [m]
levelAtomMetas _ = []
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 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 = unless (null s || isUnderscore 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)
setMetaOccursCheck :: MetaId -> RunMetaOccursCheck -> TCM ()
setMetaOccursCheck mi b = updateMetaVar mi $ \ mvar ->
mvar { mvInfo = (mvInfo mvar) { miMetaOccursCheck = b } }
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
modifyInteractionPoints f =
stInteractionPoints %= f
registerInteractionPoint :: Bool -> Range -> Maybe Nat -> TCM InteractionId
registerInteractionPoint preciseRange r maybeId = do
m <- use stInteractionPoints
if not preciseRange || isJust maybeId then continue m else do
Strict.caseMaybe (rangeFile r) (continue m) $ \ _ -> do
caseMaybe (findInteractionPoint_ r m) (continue m) return
where
continue m = do
ii <- case maybeId of
Just i -> return $ InteractionId i
Nothing -> fresh
let ip = InteractionPoint { ipRange = r, ipMeta = Nothing, ipSolved = False, ipClause = IPNoClause }
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
findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
findInteractionPoint_ r m = do
guard $ not $ null r
headMaybe $ mapMaybe sameRange $ Map.toList m
where
sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange (ii, InteractionPoint r' _ _ _) | r == r' = Just ii
sameRange _ = Nothing
connectInteractionPoint :: InteractionId -> MetaId -> TCM ()
connectInteractionPoint ii mi = do
ipCl <- asks envClause
m <- use stInteractionPoints
let ip = InteractionPoint { ipRange = __IMPOSSIBLE__, ipMeta = Just mi, ipSolved = False, ipClause = ipCl }
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
stInteractionPoints %= Map.update (\ ip -> Just ip{ ipSolved = True }) ii
getInteractionPoints :: TCM [InteractionId]
getInteractionPoints = Map.keys <$> use stInteractionPoints
getInteractionMetas :: TCM [MetaId]
getInteractionMetas =
mapMaybe ipMeta . filter (not . ipSolved) . Map.elems <$> use stInteractionPoints
getInteractionIdsAndMetas :: TCM [(InteractionId,MetaId)]
getInteractionIdsAndMetas =
mapMaybe f . filter (not . ipSolved . snd) . 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 ++ ". Possible cause: the hole has not been reached during type checking (do you see yellow?)"
lookupInteractionMeta :: InteractionId -> TCM (Maybe MetaId)
lookupInteractionMeta ii = lookupInteractionMeta_ ii <$> use stInteractionPoints
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ ii m = ipMeta =<< Map.lookup ii m
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{ mvInfo = mi
, mvPriority = p
, mvPermutation = perm
, mvJudgement = j'
, mvInstantiation = inst
, mvListeners = Set.empty
, mvFrozen = 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
getOpenMetas :: TCM [MetaId]
getOpenMetas = do
store <- getMetaStore
return [ i | (i, MetaVar{ mvInstantiation = mi }) <- Map.assocs store, isOpenMeta mi ]
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta Open = True
isOpenMeta OpenIFS = True
isOpenMeta BlockedConst{} = True
isOpenMeta PostponedTypeCheckingProblem{} = True
isOpenMeta InstV{} = 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 = freezeMetas' $ const True
freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId]
freezeMetas' p = execWriterT $ stMetaStore %== Map.traverseWithKey freeze
where
freeze :: Monad m => MetaId -> MetaVariable -> WriterT [MetaId] m MetaVariable
freeze m mvar
| p m && mvFrozen mvar /= Frozen = do
tell [m]
return $ mvar { mvFrozen = Frozen }
| otherwise = return mvar
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 (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 (MetaS x _) = unfreezeMeta x
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