module Agda.TypeChecking.MetaVars where
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Error
import Data.Generics
import Data.List as List hiding (sort)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Agda.Utils.IO.Locale as LocIO
import Agda.Syntax.Common
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Internal
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.Reduce
import Agda.TypeChecking.Substitute
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.MetaVars.Occurs
import Agda.TypeChecking.Conversion
import Agda.Utils.Fresh
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Size
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
reportSLn "tc.meta.assign" 70 $ show x ++ " := " ++ show t
whenM (isFrozen x) __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 (sort s)
newTypeMeta_ :: TCM Type
newTypeMeta_ = newTypeMeta =<< (workOnTypes $ newSortMeta)
newIFSMeta :: Type -> TCM Term
newIFSMeta t = do
vs <- getContextArgs
tel <- getContextTelescope
newIFSMetaCtx (telePi_ tel t) vs
newIFSMetaCtx :: Type -> Args -> TCM Term
newIFSMetaCtx t vs = do
i <- createMetaInfo
let TelV tel _ = telView' t
perm = idP (size tel)
x <- newMeta' OpenIFS i normalMetaPriority perm (HasType () t)
reportSDoc "tc.meta.new" 50 $ fsep
[ text "new ifs meta:"
, nest 2 $ prettyTCM vs <+> text "|-"
, nest 2 $ text (show x) <+> text ":" <+> prettyTCM t
]
solveConstraint_ $ FindInScope x
return (MetaV x vs)
newValueMeta :: Type -> TCM Term
newValueMeta t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx (telePi_ tel t) vs
newValueMetaCtx :: Type -> Args -> TCM Term
newValueMetaCtx t ctx = do
m@(MetaV i _) <- newValueMetaCtx' t ctx
instantiateFull m
newValueMeta' :: Type -> TCM Term
newValueMeta' t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx' (telePi_ tel t) vs
newValueMetaCtx' :: Type -> Args -> TCM Term
newValueMetaCtx' t vs = do
i <- createMetaInfo
let TelV tel _ = 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
return $ MetaV x vs
newTelMeta :: Telescope -> TCM Args
newTelMeta tel = newArgsMeta (abstract tel $ El Prop $ Sort Prop)
newArgsMeta :: Type -> TCM Args
newArgsMeta t = do
args <- getContextArgs
tel <- getContextTelescope
newArgsMetaCtx t tel args
newArgsMetaCtx :: Type -> Telescope -> Args -> TCM Args
newArgsMetaCtx (El s tm) tel ctx = do
tm <- reduce tm
case tm of
Pi (Arg h r a) _ -> do
arg <- (Arg h r) <$>
newValueMetaCtx (telePi_ tel a) ctx
args <- newArgsMetaCtx (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@(MetaV x _) <- newValueMeta' t
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) (return v) $ do
i <- createMetaInfo
vs <- getContextArgs
tel <- getContextTelescope
x <- newMeta' (BlockedConst $ abstract tel v)
i lowMetaPriority (idP $ size tel)
(HasType () $ telePi_ tel t)
escapeContext (size tel) $ addConstraint (Guarded (UnBlock x) pid)
reportSDoc "tc.meta.blocked" 20 $ vcat
[ text "blocked" <+> prettyTCM x <+> text ":=" <+> escapeContext (size tel) (prettyTCM $ abstract tel v)
, text " by" <+> (prettyTCM =<< getConstraintsForProblem pid) ]
inst <- isInstantiatedMeta x
case inst of
True -> instantiate (MetaV x vs)
False -> do
v <- newValueMeta t
i <- liftTCM (fresh :: TCM Integer)
cmp <- buildProblemConstraint 0 (ValueCmp CmpEq t v (MetaV x vs))
listenToMeta (CheckConstraint i cmp) x
return v
unblockedTester :: Type -> TCM Bool
unblockedTester t = do
t <- reduceB $ unEl t
case t of
Blocked{} -> return False
NotBlocked MetaV{} -> return False
_ -> 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
tel <- getContextTelescope
cl <- buildClosure (e, t, unblock)
m <- newMeta' (PostponedTypeCheckingProblem cl)
i normalMetaPriority (idP (size tel))
$ HasType () $ telePi_ tel t
v <- newValueMeta t
i <- liftTCM (fresh :: TCM Integer)
vs <- getContextArgs
cmp <- buildProblemConstraint 0 (ValueCmp CmpEq t v (MetaV m vs))
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)
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
meta <- lookupMeta m
let HasType _ a = mvJudgement meta
TelV tel b <- telViewM a
let args = [ Arg h r $ Var i []
| (i, Arg h r _) <- reverse $ zip [0..] $ reverse $ telToList tel
]
bb <- reduceB b
case unEl <$> bb of
Blocked x _ -> listenToMeta (EtaExpand m) x
NotBlocked (MetaV x _) -> listenToMeta (EtaExpand m) x
NotBlocked lvl@(Def r ps) ->
ifM (isEtaRecord r) (do
let expand = do
u <- withMetaInfo (mvInfo meta) $ newRecordMetaCtx r ps tel args
inContext [] $ addCtxTel tel $ do
verboseS "tc.meta.eta" 15 $ do
du <- prettyTCM u
liftIO $ LocIO.putStrLn $ "eta expanding: " ++ show m ++ " --> " ++ show du
noConstraints $ assignV m args u
if Records `elem` kinds then
expand
else if SingletonRecords `elem` kinds then do
singleton <- isSingletonRecord r ps
case singleton of
Left x -> listenToMeta (EtaExpand m) x
Right False -> return ()
Right True -> expand
else
return ()
) $ when (Levels `elem` kinds) $ do
mlvl <- getBuiltin' builtinLevel
tt <- typeInType
if tt && Just lvl == mlvl
then do
reportSLn "tc.meta.eta" 20 $ "Expanding level meta to 0 (type-in-type)"
noConstraints $ assignV m args (Level $ Max [])
else
return ()
_ -> return ()
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 = 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 (v, mvJudgement mvar) of
(Sort Inf, HasType{}) -> typeError $ GenericError "Setω is not a valid type."
_ -> 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 (Arg h Irrelevant (Var i [])) = [i]
fromIrrVar (Arg h Irrelevant (DontCare (Var i []))) = [i]
fromIrrVar _ = []
let irrVL = concat $ map fromIrrVar args
reportSDoc "tc.meta.assign" 20 $
let pr (Var n []) = text (show n)
pr (Def c []) = prettyTCM c
pr (DontCare v) = pr v
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) $ do
d <- sep [ text "size" <+> text (show n)
, nest 2 $ text "term" <+> prettyTCM v
]
liftIO $ LocIO.print d
ids <- checkAllVars args
let fvs = allVars $ freeVars v
reportSDoc "tc.meta.assign" 20 $
text "fvars rhs:" <+> sep (map (text . show) $ Set.toList fvs)
unless (distinct $ filter (`Set.member` fvs) ids) $ 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
reportSDoc "tc.meta.assign" 25 $
text "preparing to instantiate: " <+> prettyTCM v
v' <- do
tel <- getContextTelescope
gamma <- map defaultArg <$> getContextTerms
let iargs = reverse $ zipWith (rename ids) [0..] $ reverse gamma
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 <- telViewM 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')
n <- size <$> getContextTelescope
escapeContext n $ assignTerm x $ killRange (abstract tel' v')
return ()
where
rename :: [Nat] -> Nat -> Arg Term -> Arg Term
rename ids i arg = case findIndex (==i) ids of
Just j -> fmap (const $ Var (fromIntegral j) []) arg
Nothing -> fmap (const __IMPOSSIBLE__) arg
type FVs = Set.VarSet
checkAllVars :: Args -> TCM [Nat]
checkAllVars args =
case allVarOrIrrelevant args of
Nothing -> do
reportSDoc "tc.meta.assign" 15 $ vcat [ text "not all variables: " <+> prettyTCM args
, text " aborting assignment" ]
patternViolation
Just is -> return $ map unArg is
allVarOrIrrelevant :: Args -> Maybe [Arg Nat]
allVarOrIrrelevant args = foldM isVarOrIrrelevant [] args where
isVarOrIrrelevant vars arg =
case arg of
Arg h r (Var i []) -> return $ Arg h r i : removeIrr i vars
Arg h Irrelevant (DontCare (Var i [])) -> return $ addIrrIfNotPresent h i vars
Arg h Irrelevant _ -> return $ Arg h Irrelevant (1) : vars
_ -> Nothing
addIrrIfNotPresent h i vars
| any (\ (Arg _ _ j) -> j == i) vars = Arg h Irrelevant (1) : vars
| otherwise = Arg h Irrelevant i : vars
removeIrr i = map (\ a@(Arg h r j) ->
if r == Irrelevant && i == j then Arg h Irrelevant (1) else a)
updateMeta :: MetaId -> Term -> TCM ()
updateMeta mI v = do
mv <- lookupMeta mI
withMetaInfo (getMetaInfo mv) $ do
args <- getContextArgs
noConstraints $ assignV mI args v