module Agda.TypeChecking.MetaVars where
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Error
import Data.Function
import Data.Typeable (Typeable)
import Data.List as List hiding (sort)
import Data.Map (Map)
import qualified Data.Map as Map
import Agda.Syntax.Common
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Position
import Agda.Syntax.Literal
import qualified Agda.Syntax.Abstract as A
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Exception
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Free
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Eliminators
import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem)
import Agda.TypeChecking.MetaVars.Occurs
import Agda.TypeChecking.Conversion
import Agda.Utils.Fresh
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Permutation
import qualified Agda.Utils.VarSet as Set
import Agda.TypeChecking.Monad.Debug
#include "../undefined.h"
import Agda.Utils.Impossible
findIdx :: Eq a => [a] -> a -> Maybe Int
findIdx vs v = findIndex (==v) (reverse vs)
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm x = do
reportSLn "tc.meta.blocked" 12 $ "is " ++ show x ++ " a blocked term? "
i <- mvInstantiation <$> lookupMeta x
let r = case i of
BlockedConst{} -> True
PostponedTypeCheckingProblem{} -> True
InstV{} -> False
InstS{} -> False
Open{} -> False
OpenIFS{} -> False
reportSLn "tc.meta.blocked" 12 $
if r then " yes, because " ++ show i else " no"
return r
isEtaExpandable :: MetaId -> TCM Bool
isEtaExpandable x = do
i <- mvInstantiation <$> lookupMeta x
return $ case i of
Open{} -> True
OpenIFS{} -> False
InstV{} -> False
InstS{} -> False
BlockedConst{} -> False
PostponedTypeCheckingProblem{} -> False
assignTerm :: MetaId -> Term -> TCM ()
assignTerm x t = do
whenM (isFrozen x) __IMPOSSIBLE__
assignTerm' x t
assignTerm' :: MetaId -> Term -> TCM ()
assignTerm' x t = do
reportSLn "tc.meta.assign" 70 $ show x ++ " := " ++ show t
whenM (not <$> asks envAssignMetas) __IMPOSSIBLE__
let i = metaInstance (killRange t)
verboseS "profile.metas" 10 $ liftTCM $ tickMax "max-open-metas" . size =<< getOpenMetas
modifyMetaStore $ ins x i
etaExpandListeners x
wakeupConstraints x
reportSLn "tc.meta.assign" 20 $ "completed assignment of " ++ show x
where
metaInstance = InstV
ins x i store = Map.adjust (inst i) x store
inst i mv = mv { mvInstantiation = i }
newSortMeta :: TCM Sort
newSortMeta =
ifM typeInType (return $ mkType 0) $
ifM hasUniversePolymorphism (newSortMetaCtx =<< getContextArgs)
$ do i <- createMetaInfo
x <- newMeta i normalMetaPriority (idP 0) (IsSort () topSort)
return $ Type $ Max [Plus 0 $ MetaLevel x []]
newSortMetaCtx :: Args -> TCM Sort
newSortMetaCtx vs =
ifM typeInType (return $ mkType 0) $ do
i <- createMetaInfo
tel <- getContextTelescope
let t = telePi_ tel topSort
x <- newMeta i normalMetaPriority (idP 0) (IsSort () t)
reportSDoc "tc.meta.new" 50 $
text "new sort meta" <+> prettyTCM x <+> text ":" <+> prettyTCM t
return $ Type $ Max [Plus 0 $ MetaLevel x vs]
newTypeMeta :: Sort -> TCM Type
newTypeMeta s = El s <$> newValueMeta RunMetaOccursCheck (sort s)
newTypeMeta_ :: TCM Type
newTypeMeta_ = newTypeMeta =<< (workOnTypes $ newSortMeta)
newIFSMeta :: MetaNameSuggestion -> Type -> [(Term, Type)] -> TCM Term
newIFSMeta s t cands = do
vs <- getContextArgs
tel <- getContextTelescope
newIFSMetaCtx s (telePi_ tel t) vs cands
newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> [(Term, Type)] -> TCM Term
newIFSMetaCtx s t vs cands = do
reportSDoc "tc.meta.new" 50 $ fsep
[ text "new ifs meta:"
, nest 2 $ prettyTCM vs <+> text "|-"
]
i0 <- createMetaInfo
let i = i0 { miNameSuggestion = s }
let TelV tel _ = telView' t
perm = idP (size tel)
x <- newMeta' OpenIFS i normalMetaPriority perm (HasType () t)
reportSDoc "tc.meta.new" 50 $ fsep
[ nest 2 $ text (show x) <+> text ":" <+> prettyTCM t
]
solveConstraint_ $ FindInScope x cands
return (MetaV x vs)
newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term
newNamedValueMeta b s t = do
v <- newValueMeta b t
setValueMetaName v s
return v
newValueMeta :: RunMetaOccursCheck -> Type -> TCM Term
newValueMeta b t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx b (telePi_ tel t) vs
newValueMetaCtx :: RunMetaOccursCheck -> Type -> Args -> TCM Term
newValueMetaCtx b t ctx =
instantiateFull =<< newValueMetaCtx' b t ctx
newValueMeta' :: RunMetaOccursCheck -> Type -> TCM Term
newValueMeta' b t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx' b (telePi_ tel t) vs
newValueMetaCtx' :: RunMetaOccursCheck -> Type -> Args -> TCM Term
newValueMetaCtx' b t vs = do
i <- createMetaInfo' b
let TelV tel a = telView' t
perm = idP (size tel)
x <- newMeta i normalMetaPriority perm (HasType () t)
reportSDoc "tc.meta.new" 50 $ fsep
[ text "new meta:"
, nest 2 $ prettyTCM vs <+> text "|-"
, nest 2 $ text (show x) <+> text ":" <+> prettyTCM t
]
etaExpandMetaSafe x
let u = shared $ MetaV x vs
boundedSizeMetaHook u tel a
return u
newTelMeta :: Telescope -> TCM Args
newTelMeta tel = newArgsMeta (abstract tel $ El Prop $ Sort Prop)
type Condition = Dom Type -> Abs Type -> Bool
trueCondition _ _ = True
newArgsMeta :: Type -> TCM Args
newArgsMeta = newArgsMeta' trueCondition
newArgsMeta' :: Condition -> Type -> TCM Args
newArgsMeta' condition t = do
args <- getContextArgs
tel <- getContextTelescope
newArgsMetaCtx' condition t tel args
newArgsMetaCtx :: Type -> Telescope -> Args -> TCM Args
newArgsMetaCtx = newArgsMetaCtx' trueCondition
newArgsMetaCtx' :: Condition -> Type -> Telescope -> Args -> TCM Args
newArgsMetaCtx' condition (El s tm) tel ctx = do
tm <- reduce tm
case ignoreSharing tm of
Pi dom@(Dom h r a) codom | condition dom codom -> do
arg <- (Arg h r) <$> do
applyRelevanceToContext r $
newValueMetaCtx RunMetaOccursCheck (telePi_ tel a) ctx
args <- newArgsMetaCtx' condition (El s tm `piApply` [arg]) tel ctx
return $ arg : args
_ -> return []
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta r pars = do
args <- getContextArgs
tel <- getContextTelescope
newRecordMetaCtx r pars tel args
newRecordMetaCtx :: QName -> Args -> Telescope -> Args -> TCM Term
newRecordMetaCtx r pars tel ctx = do
ftel <- flip apply pars <$> getRecordFieldTypes r
fields <- newArgsMetaCtx (telePi_ ftel $ sort Prop) tel ctx
con <- getRecordConstructor r
return $ Con con fields
newQuestionMark :: Type -> TCM Term
newQuestionMark t = do
m <- newValueMeta' DontRunMetaOccursCheck t
let MetaV x _ = ignoreSharing m
ii <- fresh
addInteractionPoint ii x
return m
blockTerm :: Type -> TCM Term -> TCM Term
blockTerm t blocker = do
(pid, v) <- newProblem blocker
blockTermOnProblem t v pid
blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term
blockTermOnProblem t v pid =
ifM (isProblemSolved pid `or2M` isSizeProblem pid) (return v) $ do
i <- createMetaInfo
vs <- getContextArgs
tel <- getContextTelescope
x <- newMeta' (BlockedConst $ abstract tel v)
i lowMetaPriority (idP $ size tel)
(HasType () $ telePi_ tel t)
escapeContextToTopLevel $ addConstraint (Guarded (UnBlock x) pid)
reportSDoc "tc.meta.blocked" 20 $ vcat
[ text "blocked" <+> prettyTCM x <+> text ":=" <+> escapeContextToTopLevel (prettyTCM $ abstract tel v)
, text " by" <+> (prettyTCM =<< getConstraintsForProblem pid) ]
inst <- isInstantiatedMeta x
case inst of
True -> instantiate (MetaV x vs)
False -> do
v <- newValueMeta DontRunMetaOccursCheck t
i <- liftTCM fresh
cmp <- buildProblemConstraint 0 (ValueCmp CmpEq t v (MetaV x vs))
listenToMeta (CheckConstraint i cmp) x
return v
unblockedTester :: Type -> TCM Bool
unblockedTester t = ifBlocked (unEl t) (\ m t -> return False) (\ t -> return True)
postponeTypeCheckingProblem_ :: A.Expr -> Type -> TCM Term
postponeTypeCheckingProblem_ e t = do
postponeTypeCheckingProblem e t (unblockedTester t)
postponeTypeCheckingProblem :: A.Expr -> Type -> TCM Bool -> TCM Term
postponeTypeCheckingProblem e t unblock = do
i <- createMetaInfo' DontRunMetaOccursCheck
tel <- getContextTelescope
cl <- buildClosure (e, t, unblock)
m <- newMeta' (PostponedTypeCheckingProblem cl)
i normalMetaPriority (idP (size tel))
$ HasType () $ telePi_ tel t
vs <- getContextArgs
v <- newValueMeta DontRunMetaOccursCheck t
cmp <- buildProblemConstraint 0 (ValueCmp CmpEq t v (MetaV m vs))
i <- liftTCM fresh
listenToMeta (CheckConstraint i cmp) m
addConstraint (UnBlock m)
return v
etaExpandListeners :: MetaId -> TCM ()
etaExpandListeners m = do
ls <- getMetaListeners m
clearMetaListeners m
mapM_ wakeupListener ls
wakeupListener :: Listener -> TCM ()
wakeupListener (EtaExpand x) = etaExpandMetaSafe x
wakeupListener (CheckConstraint _ c) = do
reportSDoc "tc.meta.blocked" 20 $ text "waking boxed constraint" <+> prettyTCM c
addAwakeConstraints [c]
solveAwakeConstraints
etaExpandMetaSafe :: MetaId -> TCM ()
etaExpandMetaSafe = etaExpandMeta [SingletonRecords,Levels]
data MetaKind =
Records
| SingletonRecords
| Levels
deriving (Eq, Enum, Bounded, Show)
allMetaKinds :: [MetaKind]
allMetaKinds = [minBound .. maxBound]
etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()
etaExpandMeta kinds m = whenM (isEtaExpandable m) $ do
verboseBracket "tc.meta.eta" 20 ("etaExpandMeta " ++ show m) $ do
let waitFor x = do
reportSDoc "tc.meta.eta" 20 $ do
text "postponing eta-expansion of meta variable" <+>
prettyTCM m <+>
text "which is blocked by" <+> prettyTCM x
listenToMeta (EtaExpand m) x
dontExpand = do
reportSDoc "tc.meta.eta" 20 $ do
text "we do not expand meta variable" <+> prettyTCM m <+>
text ("(requested was expansion of " ++ show kinds ++ ")")
meta <- lookupMeta m
let HasType _ a = mvJudgement meta
TelV tel b <- telView a
ifBlocked (unEl b) (\ x _ -> waitFor x) $ \ t -> case ignoreSharing t of
lvl@(Def r ps) ->
ifM (isEtaRecord r) (do
let expand = do
u <- abstract tel <$> do withMetaInfo' meta $ newRecordMetaCtx r ps tel $ teleArgs tel
inTopContext $ do
verboseS "tc.meta.eta" 15 $ do
du <- prettyTCM u
reportSLn "" 0 $ "eta expanding: " ++ show m ++ " --> " ++ show du
noConstraints $ assignTerm' m u
if Records `elem` kinds then
expand
else if (SingletonRecords `elem` kinds) then do
singleton <- isSingletonRecord r ps
case singleton of
Left x -> waitFor x
Right False -> dontExpand
Right True -> expand
else dontExpand
) $ ifM (andM [ return $ Levels `elem` kinds
, typeInType
, (Just lvl ==) <$> getBuiltin' builtinLevel
]) (do
reportSLn "tc.meta.eta" 20 $ "Expanding level meta to 0 (type-in-type)"
noConstraints $ assignTerm m (abstract tel $ Level $ Max [])
) $ dontExpand
_ -> dontExpand
etaExpandBlocked :: Reduce t => Blocked t -> TCM (Blocked t)
etaExpandBlocked t@NotBlocked{} = return t
etaExpandBlocked (Blocked m t) = do
etaExpandMeta [Records] m
t <- reduceB t
case t of
Blocked m' _ | m /= m' -> etaExpandBlocked t
_ -> return t
assignV :: MetaId -> Args -> Term -> TCM ()
assignV x args v = ifM (not <$> asks envAssignMetas) patternViolation $ do
reportSDoc "tc.meta.assign" 10 $ do
text "term" <+> prettyTCM (MetaV x args) <+> text ":=" <+> prettyTCM v
liftTCM $ nowSolvingConstraints (assign x args v) `finally` solveAwakeConstraints
assign :: MetaId -> Args -> Term -> TCM ()
assign x args v = do
mvar <- lookupMeta x
v <- instantiate v
reportSLn "tc.meta.assign" 50 $ "MetaVars.assign: assigning to " ++ show v
case (ignoreSharing v, mvJudgement mvar) of
(Sort Inf, HasType{}) -> typeError SetOmegaNotValidType
_ -> return ()
when (mvFrozen mvar == Frozen) $ do
reportSLn "tc.meta.assign" 25 $ "aborting: meta is frozen!"
patternViolation
whenM (isBlockedTerm x) patternViolation
reportSLn "tc.meta.assign" 50 $ "MetaVars.assign: I want to see whether rhs is blocked"
reportSDoc "tc.meta.assign" 25 $ do
v0 <- reduceB v
case v0 of
Blocked m0 _ -> text "r.h.s. blocked on:" <+> prettyTCM m0
NotBlocked{} -> text "r.h.s. not blocked"
args <- etaContract =<< normalise args
let varsL = freeVars args
let relVL = Set.toList $ relevantVars varsL
let fromIrrVar (Var i []) = return [i]
fromIrrVar (Con c vs) =
ifM (isNothing <$> isRecordConstructor c) (return []) $
concat <$> mapM (fromIrrVar . unArg) vs
fromIrrVar (Shared p) = fromIrrVar (derefPtr p)
fromIrrVar _ = return []
irrVL <- concat <$> mapM fromIrrVar
[ v | Arg h r v <- args, irrelevantOrUnused r ]
reportSDoc "tc.meta.assign" 20 $
let pr (Var n []) = text (show n)
pr (Def c []) = prettyTCM c
pr _ = text ".."
in vcat
[ text "mvar args:" <+> sep (map (pr . unArg) args)
, text "fvars lhs (rel):" <+> sep (map (text . show) relVL)
, text "fvars lhs (irr):" <+> sep (map (text . show) irrVL)
]
v <- liftTCM $ occursCheck x (relVL, irrVL) v
reportSLn "tc.meta.assign" 15 "passed occursCheck"
verboseS "tc.meta.assign" 30 $ do
let n = size v
when (n > 200) $ reportSDoc "" 0 $
sep [ text "size" <+> text (show n)
, nest 2 $ text "term" <+> prettyTCM v
]
let fvs = allVars $ freeVars v
reportSDoc "tc.meta.assign" 20 $
text "fvars rhs:" <+> sep (map (text . show) $ Set.toList fvs)
ids <- do
res <- runErrorT $ inverseSubst args
case res of
Right (Just ids) -> do
reportSDoc "tc.meta.assign" 50 $
text "inverseSubst returns:" <+> sep (map prettyTCM ids)
return ids
Right Nothing -> attemptPruning x args fvs
Left () -> patternViolation
ids <- do
res <- runErrorT $ checkLinearity (`Set.member` fvs) ids
case res of
Right ids -> return ids
Left () -> attemptPruning x args fvs
reportSDoc "tc.meta.assign" 25 $
text "preparing to instantiate: " <+> prettyTCM v
v' <- do
tel <- getContextTelescope
let iargs = map (defaultArg . substitute ids) $ downFrom $ size tel
v' = raise (size args) (abstract tel v) `apply` iargs
return v'
let t = jMetaType $ mvJudgement mvar
reportSDoc "tc.meta.assign" 15 $ text "type of meta =" <+> prettyTCM t
TelV tel0 core0 <- telView t
let n = length args
reportSDoc "tc.meta.assign" 30 $ text "tel0 =" <+> prettyTCM tel0
reportSDoc "tc.meta.assign" 30 $ text "#args =" <+> text (show n)
when (size tel0 < n) __IMPOSSIBLE__
let tel' = telFromList $ take n $ telToList tel0
reportSDoc "tc.meta.assign" 10 $
text "solving" <+> prettyTCM x <+> text ":=" <+> prettyTCM (abstract tel' v')
inTopContext $ assignTerm x (killRange $ abstract tel' v')
return ()
where
substitute :: [(Nat,Term)] -> Nat -> Term
substitute ids i = maybe __IMPOSSIBLE__ id $ lookup i ids
attemptPruning x args fvs = do
killResult <- prune x args $ Set.toList fvs
reportSDoc "tc.meta.assign" 10 $
text "pruning" <+> prettyTCM x <+> (text $
if killResult `elem` [PrunedSomething,PrunedEverything] then "succeeded"
else "failed")
patternViolation
instance (PrettyTCM a, PrettyTCM b) => PrettyTCM (a,b) where
prettyTCM (a, b) = parens $ prettyTCM a <> comma <> prettyTCM b
type FVs = Set.VarSet
type SubstCand = [(Nat,Term)]
instance Error () where
noMsg = ()
checkLinearity :: (Nat -> Bool) -> SubstCand -> ErrorT () TCM SubstCand
checkLinearity elemFVs ids0 = do
let ids = sortBy (compare `on` fst) $ filter (elemFVs . fst) ids0
let grps = groupOn fst ids
concat <$> mapM makeLinear grps
where
makeLinear :: SubstCand -> ErrorT () TCM SubstCand
makeLinear [] = __IMPOSSIBLE__
makeLinear grp@[_] = return grp
makeLinear (p@(i,t) : _) =
ifM ((Right True ==) <$> do isSingletonTypeModuloRelevance =<< typeOfBV i)
(return [p])
(throwError ())
type Res = Maybe [(Arg Nat, Term)]
inverseSubst :: Args -> ErrorT () TCM (Maybe SubstCand)
inverseSubst args = fmap (map (mapFst unArg)) <$> loop (zip args terms)
where
loop = foldM isVarOrIrrelevant (Just [])
terms = map var (downFrom (size args))
failure = do
lift $ reportSDoc "tc.meta.assign" 15 $ vcat
[ text "not all arguments are variables: " <+> prettyTCM args
, text " aborting assignment" ]
throwError ()
isVarOrIrrelevant :: Res -> (Arg Term, Term) -> ErrorT () TCM Res
isVarOrIrrelevant vars (arg, t) =
case ignoreSharing <$> arg of
Arg h r (Var i []) -> return $ (Arg h r i, t) `cons` vars
Arg h r (Con c vs) -> do
isRC <- lift $ isRecordConstructor c
case isRC of
Just (_, Record{ recFields = fs }) -> do
let aux (Arg _ _ v) (Arg h' r' f) =
(Arg (min h h') (max r r') v,
Def f [defaultArg t])
res <- loop $ zipWith aux vs fs
return $ res `append` vars
Just _ -> __IMPOSSIBLE__
Nothing | irrelevantOrUnused r -> return vars
| otherwise -> failure
Arg h r _ | irrelevantOrUnused r -> return vars
Arg _ _ Var{} -> return $ Nothing
Arg _ _ v@(Def{}) -> do
elV <- lift $ elimView v
case elV of
VarElim{} -> return $ Nothing
_ -> failure
Arg _ _ Lam{} -> failure
Arg _ _ Lit{} -> failure
Arg _ _ MetaV{} -> failure
Arg _ _ Pi{} -> return $ Nothing
Arg _ _ Sort{} -> return $ Nothing
Arg _ _ Level{} -> return $ Nothing
Arg _ _ DontCare{} -> __IMPOSSIBLE__
Arg h r (Shared p) -> isVarOrIrrelevant vars (Arg h r $ derefPtr p, t)
append :: Res -> Res -> Res
append Nothing _ = Nothing
append (Just res) vars = foldr cons vars res
cons :: (Arg Nat, Term) -> Res -> Res
cons a Nothing = Nothing
cons a@(Arg h Irrelevant i, t) (Just vars)
| any ((i==) . unArg . fst) vars = Just vars
| otherwise = Just $ a : vars
cons a@(Arg h r i, t) (Just vars) = Just $ a :
filter (not . (\ a@(Arg h r j, t) -> r == Irrelevant && i == j)) vars
updateMeta :: MetaId -> Term -> TCM ()
updateMeta mI v = do
mv <- lookupMeta mI
withMetaInfo' mv $ do
args <- getContextArgs
noConstraints $ assignV mI args v
allMetas :: Type -> [MetaId]
allMetas = foldTerm metas
where
metas (MetaV m _) = [m]
metas _ = []