{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Monad.MetaVars where
import Prelude hiding (null)
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.Fail (MonadFail)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
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.MetaVars
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin (HasBuiltins)
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Constraints (MonadConstraint)
import Agda.TypeChecking.Monad.Debug (MonadDebug, reportSLn)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Signature (HasConstInfo)
import Agda.TypeChecking.Substitute
import {-# SOURCE #-} Agda.TypeChecking.Telescope
import Agda.Utils.Except
import Agda.Utils.Functor ((<.>))
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 qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Impossible
data MetaKind =
Records
| SingletonRecords
| Levels
deriving (Eq, Enum, Bounded, Show)
allMetaKinds :: [MetaKind]
allMetaKinds = [minBound .. maxBound]
data KeepMetas = KeepMetas | RollBackMetas
class ( MonadConstraint m
, MonadReduce m
, MonadAddContext m
, MonadTCEnv m
, ReadTCState m
, HasBuiltins m
, HasConstInfo m
, MonadDebug m
) => MonadMetaSolver m where
newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
Judgement a -> m MetaId
assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
etaExpandMeta :: [MetaKind] -> MetaId -> m ()
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m ()
speculateMetas :: m () -> m KeepMetas -> m ()
dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a
dontAssignMetas cont = do
reportSLn "tc.meta" 45 $ "don't assign metas"
localTC (\ env -> env { envAssignMetas = False }) cont
getMetaStore :: (ReadTCState m) => m MetaStore
getMetaStore = useR stMetaStore
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore f = stMetaStore `modifyTCLens` f
metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet)
metasCreatedBy m = do
before <- IntMap.keysSet <$> useTC stMetaStore
a <- m
after <- IntMap.keysSet <$> useTC stMetaStore
return (a, after IntSet.\\ before)
lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupMeta' m = IntMap.lookup (metaId m) <$> getMetaStore
lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable
lookupMeta m = fromMaybeM failure $ lookupMeta' m
where failure = fail $ "no such meta variable " ++ prettyShow m
metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
metaType x = jMetaType . mvJudgement <$> lookupMeta x
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM m f = modifyMetaStore $ IntMap.adjust f $ metaId m
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar m mv = modifyMetaStore $ IntMap.insert (metaId m) mv
getMetaPriority :: (MonadFail m, ReadTCState m) => MetaId -> m MetaPriority
getMetaPriority = mvPriority <.> lookupMeta
isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isSortMeta m = isSortMeta_ <$> lookupMeta m
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ mv = case mvJudgement mv of
HasType{} -> False
IsSort{} -> True
getMetaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
getMetaType m = do
mv <- lookupMeta m
return $ case mvJudgement mv of
HasType{ jMetaType = t } -> t
IsSort{} -> __IMPOSSIBLE__
getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVar{ mvPermutation = p } = do
args <- getContextArgs
return $ permute (takeP (length args) p) args
getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m)
=> MetaId -> m Type
getMetaTypeInContext m = do
mv@MetaVar{ mvJudgement = j } <- lookupMeta m
case j of
HasType{ jMetaType = t } -> piApplyM t =<< getMetaContextArgs mv
IsSort{} -> __IMPOSSIBLE__
isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize
isGeneralizableMeta x = unArg . miGeneralizable . mvInfo <$> lookupMeta x
class IsInstantiatedMeta a where
isInstantiatedMeta :: (MonadFail m, ReadTCState m) => a -> m 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 n ls) | n == 0 = isInstantiatedMeta ls
isInstantiatedMeta _ = __IMPOSSIBLE__
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' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)
isInstantiatedMeta' m = do
mv <- lookupMeta m
return $ case mvInstantiation mv of
InstV tel v -> Just $ foldr mkLam v tel
_ -> Nothing
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas c = metas c
where
metas c = case c of
ValueCmp _ t u v -> return $ allMetas Set.singleton (t, u, v)
ValueCmpOnFace _ p t u v -> return $ allMetas Set.singleton (p, t, u, v)
ElimCmp _ _ t u es es' -> return $ allMetas Set.singleton (t, u, es, es')
LevelCmp _ l l' -> return $ allMetas Set.singleton (Level l, Level l')
UnquoteTactic m t h g -> return $ Set.fromList [x | Just x <- [m]] `Set.union` allMetas Set.singleton (t, h, g)
Guarded c _ -> metas c
TelCmp _ _ _ tel1 tel2 -> return $ allMetas Set.singleton (tel1, tel2)
SortCmp _ s1 s2 -> return $ allMetas Set.singleton (Sort s1, Sort s2)
UnBlock x -> Set.insert x . Set.unions <$> (mapM listenerMetas =<< getMetaListeners x)
FindInstance{} -> return mempty
IsEmpty{} -> return mempty
CheckFunDef{} -> return mempty
CheckSizeLtSat{} -> return mempty
HasBiggerSort{} -> return mempty
HasPTSRule{} -> return mempty
CheckMetaInst x -> return mempty
listenerMetas EtaExpand{} = return Set.empty
listenerMetas (CheckConstraint _ c) = constraintMetas (clValue $ theConstraint c)
createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo = createMetaInfo' RunMetaOccursCheck
createMetaInfo'
:: (MonadTCEnv m, ReadTCState m)
=> RunMetaOccursCheck -> m MetaInfo
createMetaInfo' b = do
r <- getCurrentRange
cl <- buildClosure r
gen <- viewTC eGeneralizeMetas
return MetaInfo
{ miClosRange = cl
, miMetaOccursCheck = b
, miNameSuggestion = ""
, miGeneralizable = hide $ defaultArg gen
}
setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()
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 :: (MonadFail m, ReadTCState m) => MetaId -> m MetaNameSuggestion
getMetaNameSuggestion mi = miNameSuggestion . mvInfo <$> lookupMeta mi
setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
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 }}
setMetaArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m ()
setMetaArgInfo m i = updateMetaVar m $ \ mv ->
mv { mvInfo = (mvInfo mv)
{ miGeneralizable = setArgInfo i (miGeneralizable (mvInfo mv)) } }
updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange mi r = updateMetaVar mi (setRange r)
setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck mi b = updateMetaVar mi $ \ mvar ->
mvar { mvInfo = (mvInfo mvar) { miMetaOccursCheck = b } }
class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where
freshInteractionId :: m InteractionId
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
instance MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m) where
freshInteractionId = lift freshInteractionId
modifyInteractionPoints = lift . modifyInteractionPoints
instance MonadInteractionPoints m => MonadInteractionPoints (StateT r m) where
freshInteractionId = lift freshInteractionId
modifyInteractionPoints = lift . modifyInteractionPoints
instance MonadInteractionPoints TCM where
freshInteractionId = fresh
modifyInteractionPoints f = stInteractionPoints `modifyTCLens` f
registerInteractionPoint
:: forall m. MonadInteractionPoints m
=> Bool -> Range -> Maybe Nat -> m InteractionId
registerInteractionPoint preciseRange r maybeId = do
m <- useR 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 :: InteractionPoints -> m InteractionId
continue m = do
ii <- case maybeId of
Just i -> return $ InteractionId i
Nothing -> freshInteractionId
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
listToMaybe $ mapMaybe sameRange $ Map.toList m
where
sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange (ii, InteractionPoint r' _ _ _) | r == r' = Just ii
sameRange _ = Nothing
connectInteractionPoint
:: MonadInteractionPoints m
=> InteractionId -> MetaId -> m ()
connectInteractionPoint ii mi = do
ipCl <- asksTC envClause
m <- useR 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 :: MonadInteractionPoints m => InteractionId -> m ()
removeInteractionPoint ii =
modifyInteractionPoints $ Map.update (\ ip -> Just ip{ ipSolved = True }) ii
{-# SPECIALIZE getInteractionPoints :: TCM [InteractionId] #-}
getInteractionPoints :: ReadTCState m => m [InteractionId]
getInteractionPoints = Map.keys <$> useR stInteractionPoints
getInteractionMetas :: ReadTCState m => m [MetaId]
getInteractionMetas =
mapMaybe ipMeta . filter (not . ipSolved) . Map.elems <$> useR stInteractionPoints
getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId,MetaId)]
getInteractionIdsAndMetas =
mapMaybe f . filter (not . ipSolved . snd) . Map.toList <$> useR stInteractionPoints
where f (ii, ip) = (ii,) <$> ipMeta ip
isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId)
isInteractionMeta x = lookup x . map swap <$> getInteractionIdsAndMetas
{-# SPECIALIZE lookupInteractionPoint :: InteractionId -> TCM InteractionPoint #-}
lookupInteractionPoint
:: (MonadFail m, ReadTCState m, MonadError TCErr m)
=> InteractionId -> m InteractionPoint
lookupInteractionPoint ii =
fromMaybeM err $ Map.lookup ii <$> useR stInteractionPoints
where
err = fail $ "no such interaction point: " ++ show ii
lookupInteractionId
:: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)
=> InteractionId -> m MetaId
lookupInteractionId ii = fromMaybeM err2 $ ipMeta <$> lookupInteractionPoint ii
where
err2 = typeError $ GenericError $ "No type nor action available for hole " ++ prettyShow ii ++ ". Possible cause: the hole has not been reached during type checking (do you see yellow?)"
lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)
lookupInteractionMeta ii = lookupInteractionMeta_ ii <$> useR stInteractionPoints
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ ii m = ipMeta =<< Map.lookup ii m
newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
newMeta = newMeta' Open
newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
Judgement a -> TCM MetaId
newMetaTCM' inst frozen 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 = frozen
, mvTwin = Nothing
}
insertMetaVar x mv
return x
{-# SPECIALIZE getInteractionRange :: InteractionId -> TCM Range #-}
getInteractionRange
:: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m)
=> InteractionId -> m Range
getInteractionRange = ipRange <.> lookupInteractionPoint
getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m 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
getMetaVariableSet :: ReadTCState m => m IntSet
getMetaVariableSet = IntMap.keysSet <$> getMetaStore
getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]
getMetaVariables p = do
store <- getMetaStore
return [ MetaId i | (i, mv) <- IntMap.assocs store, p mv ]
getInstantiatedMetas :: ReadTCState m => m [MetaId]
getInstantiatedMetas = getMetaVariables (isInst . mvInstantiation)
where
isInst Open = False
isInst OpenInstance = False
isInst BlockedConst{} = False
isInst PostponedTypeCheckingProblem{} = False
isInst InstV{} = True
getOpenMetas :: ReadTCState m => m [MetaId]
getOpenMetas = getMetaVariables (isOpenMeta . mvInstantiation)
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta Open = True
isOpenMeta OpenInstance = True
isOpenMeta BlockedConst{} = True
isOpenMeta PostponedTypeCheckingProblem{} = True
isOpenMeta InstV{} = False
listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
listenToMeta l m =
updateMetaVar m $ \mv -> mv { mvListeners = Set.insert l $ mvListeners mv }
unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
unlistenToMeta l m =
updateMetaVar m $ \mv -> mv { mvListeners = Set.delete l $ mvListeners mv }
getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener]
getMetaListeners m = Set.toList . mvListeners <$> lookupMeta m
clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
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 $ modifyTCLensM stMetaStore $ IntMap.traverseWithKey (freeze . MetaId)
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 $ IntMap.mapWithKey $ unfreeze . MetaId
where
unfreeze :: MetaId -> MetaVariable -> MetaVariable
unfreeze m mvar
| cond m = mvar { mvFrozen = Instantiable }
| otherwise = mvar
isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isFrozen x = do
mvar <- lookupMeta x
return $ mvFrozen mvar == Frozen
class UnFreezeMeta a where
unfreezeMeta :: MonadMetaSolver m => a -> m ()
instance UnFreezeMeta MetaId where
unfreezeMeta x = do
updateMetaVar x $ \ mv -> mv { mvFrozen = Instantiable }
unfreezeMeta =<< metaType 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
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