{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE GADTs #-}
module Agda.TypeChecking.MetaVars where
import Prelude hiding (null)
import Control.Monad.Reader
import Data.Function
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import qualified Data.Set as Set
import qualified Data.Foldable as Fold
import qualified Data.Traversable as Trav
import Agda.Interaction.Options
import Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position (getRange, killRange)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import qualified Agda.TypeChecking.SyntacticEquality as SynEq
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Lazy
import Agda.TypeChecking.Level (levelType)
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem)
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.MetaVars.Occurs
import Agda.Utils.Except
( ExceptT
, MonadError(throwError, catchError)
, runExceptT
)
import Agda.Utils.Function
import Agda.Utils.Lens
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 Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Singleton
import qualified Agda.Utils.Graph.TopSort as Graph
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.WithDefault
import Agda.Utils.Impossible
instance MonadMetaSolver TCM where
newMeta' = newMetaTCM'
assignV dir x args v t = assignWrapper dir x (map Apply args) v $ assign dir x args v t
assignTerm' = assignTermTCM'
etaExpandMeta = etaExpandMetaTCM
updateMetaVar = updateMetaVarTCM
speculateMetas fallback m = do
(a, s) <- localTCStateSaving m
case a of
KeepMetas -> putTC s
RollBackMetas -> fallback
findIdx :: Eq a => [a] -> a -> Maybe Int
findIdx vs v = List.findIndex (==v) (reverse vs)
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm x = do
reportSLn "tc.meta.blocked" 12 $ "is " ++ prettyShow x ++ " a blocked term? "
i <- mvInstantiation <$> lookupMeta x
let r = case i of
BlockedConst{} -> True
PostponedTypeCheckingProblem{} -> True
InstV{} -> False
Open{} -> False
OpenInstance{} -> False
reportSLn "tc.meta.blocked" 12 $
if r then " yes, because " ++ show i else " no"
return r
isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool
isEtaExpandable kinds x = do
i <- mvInstantiation <$> lookupMeta x
return $ case i of
Open{} -> True
OpenInstance{} -> notElem Records kinds
InstV{} -> False
BlockedConst{} -> False
PostponedTypeCheckingProblem{} -> False
assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm x tel v = do
whenM (isFrozen x) __IMPOSSIBLE__
assignTerm' x tel v
assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTermTCM' x tel v = do
reportSDoc "tc.meta.assign" 70 $ vcat
[ "assignTerm" <+> prettyTCM x <+> " := " <+> prettyTCM v
, nest 2 $ "tel =" <+> prettyList_ (map (text . unArg) tel)
]
whenM (not <$> asksTC envAssignMetas) __IMPOSSIBLE__
verboseS "profile.metas" 10 $ liftTCM $ return ()
modifyMetaStore $ ins x $ InstV tel $ killRange v
etaExpandListeners x
wakeupConstraints x
reportSLn "tc.meta.assign" 20 $ "completed assignment of " ++ prettyShow x
where
ins x i = IntMap.adjust (\ mv -> mv { mvInstantiation = i }) $ metaId x
newSortMetaBelowInf :: TCM Sort
newSortMetaBelowInf = do
x <- newSortMeta
hasBiggerSort x
return x
newSortMeta :: MonadMetaSolver m => m Sort
newSortMeta =
ifM hasUniversePolymorphism (newSortMetaCtx =<< getContextArgs)
$ do i <- createMetaInfo
let j = IsSort () __DUMMY_TYPE__
x <- newMeta Instantiable i normalMetaPriority (idP 0) j
reportSDoc "tc.meta.new" 50 $
"new sort meta" <+> prettyTCM x
return $ MetaS x []
newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort
newSortMetaCtx vs = do
i <- createMetaInfo
tel <- getContextTelescope
let t = telePi_ tel __DUMMY_TYPE__
x <- newMeta Instantiable i normalMetaPriority (idP $ size tel) $ IsSort () t
reportSDoc "tc.meta.new" 50 $
"new sort meta" <+> prettyTCM x <+> ":" <+> prettyTCM t
return $ MetaS x $ map Apply vs
newTypeMeta' :: Comparison -> Sort -> TCM Type
newTypeMeta' cmp s = El s . snd <$> newValueMeta RunMetaOccursCheck cmp (sort s)
newTypeMeta :: Sort -> TCM Type
newTypeMeta = newTypeMeta' CmpLeq
newTypeMeta_ :: TCM Type
newTypeMeta_ = newTypeMeta' CmpEq =<< (workOnTypes $ newSortMeta)
newLevelMeta :: MonadMetaSolver m => m Level
newLevelMeta = do
(x, v) <- newValueMeta RunMetaOccursCheck CmpEq =<< levelType
return $ case v of
Level l -> l
MetaV x vs -> Max 0 [Plus 0 (MetaLevel x vs)]
_ -> Max 0 [Plus 0 (UnreducedLevel v)]
newInstanceMeta
:: MonadMetaSolver m
=> MetaNameSuggestion -> Type -> m (MetaId, Term)
newInstanceMeta s t = do
vs <- getContextArgs
ctx <- getContextTelescope
newInstanceMetaCtx s (telePi_ ctx t) vs
newInstanceMetaCtx
:: MonadMetaSolver m
=> MetaNameSuggestion -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx s t vs = do
reportSDoc "tc.meta.new" 50 $ fsep
[ "new instance meta:"
, nest 2 $ prettyTCM vs <+> "|-"
]
i0 <- createMetaInfo' DontRunMetaOccursCheck
let i = i0 { miNameSuggestion = s }
TelV tel _ <- telView t
let perm = idP (size tel)
x <- newMeta' OpenInstance Instantiable i normalMetaPriority perm (HasType () CmpLeq t)
reportSDoc "tc.meta.new" 50 $ fsep
[ nest 2 $ pretty x <+> ":" <+> prettyTCM t
]
let c = FindInstance x Nothing Nothing
ifM isSolvingConstraints (addConstraint c) (addAwakeConstraint c)
etaExpandMetaSafe x
return (x, MetaV x $ map Apply vs)
newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta b s cmp t = do
(x, v) <- newValueMeta b cmp t
setMetaNameSuggestion x s
return (x, v)
newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' b s cmp t = do
(x, v) <- newValueMeta' b cmp t
setMetaNameSuggestion x s
return (x, v)
newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta b cmp t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx Instantiable b cmp t tel (idP $ size tel) vs
newValueMetaCtx
:: MonadMetaSolver m
=> Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
newValueMetaCtx frozen b cmp t tel perm ctx =
mapSndM instantiateFull =<< newValueMetaCtx' frozen b cmp t tel perm ctx
newValueMeta'
:: MonadMetaSolver m
=> RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' b cmp t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx' Instantiable b cmp t tel (idP $ size tel) vs
newValueMetaCtx'
:: MonadMetaSolver m
=> Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
newValueMetaCtx' frozen b cmp a tel perm vs = do
i <- createMetaInfo' b
let t = telePi_ tel a
x <- newMeta frozen i normalMetaPriority perm (HasType () cmp t)
reportSDoc "tc.meta.new" 50 $ fsep
[ text $ "new meta (" ++ show (i ^. lensIsAbstract) ++ "):"
, nest 2 $ prettyTCM vs <+> "|-"
, nest 2 $ pretty x <+> ":" <+> prettyTCM t
]
etaExpandMetaSafe x
let u = MetaV x $ map Apply vs
boundedSizeMetaHook u tel a
return (x, u)
newTelMeta :: MonadMetaSolver m => Telescope -> m Args
newTelMeta tel = newArgsMeta (abstract tel $ __DUMMY_TYPE__)
type Condition = Dom Type -> Abs Type -> Bool
trueCondition :: Condition
trueCondition _ _ = True
newArgsMeta :: MonadMetaSolver m => Type -> m Args
newArgsMeta = newArgsMeta' trueCondition
newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args
newArgsMeta' condition t = do
args <- getContextArgs
tel <- getContextTelescope
newArgsMetaCtx' Instantiable condition t tel (idP $ size tel) args
newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx = newArgsMetaCtx' Instantiable trueCondition
newArgsMetaCtx'
:: MonadMetaSolver m
=> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' frozen condition (El s tm) tel perm ctx = do
tm <- reduce tm
case tm of
Pi dom@(Dom{domInfo = info, unDom = a}) codom | condition dom codom -> do
let mod = getModality info
tel' = telFromList . map (mod `inverseApplyModality`) . telToList $ tel
ctx' = (map . mapModality) (mod `inverseComposeModality`) ctx
(m, u) <- applyModalityToContext info $
newValueMetaCtx frozen RunMetaOccursCheck CmpLeq a tel' perm ctx'
setMetaArgInfo m (getArgInfo dom)
setMetaNameSuggestion m (absName codom)
args <- newArgsMetaCtx' frozen condition (codom `absApp` u) tel perm ctx
return $ Arg info u : args
_ -> return []
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta r pars = do
args <- getContextArgs
tel <- getContextTelescope
newRecordMetaCtx Instantiable r pars tel (idP $ size tel) args
newRecordMetaCtx
:: Frozen
-> QName
-> Args
-> Telescope -> Permutation -> Args -> TCM Term
newRecordMetaCtx frozen r pars tel perm ctx = do
ftel <- flip apply pars <$> getRecordFieldTypes r
fields <- newArgsMetaCtx' frozen trueCondition
(telePi_ ftel __DUMMY_TYPE__) tel perm ctx
con <- getRecordConstructor r
return $ Con con ConOSystem (map Apply fields)
newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark ii cmp = newQuestionMark' (newValueMeta' RunMetaOccursCheck) ii cmp
newQuestionMark'
:: (Comparison -> Type -> TCM (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark' new ii cmp t = do
let existing x = (x,) . MetaV x . map Apply <$> getContextArgs
flip (caseMaybeM $ lookupInteractionMeta ii) existing $ do
(x, m) <- new cmp t
connectInteractionPoint ii x
return (x, m)
blockTerm
:: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m)
=> Type -> m Term -> m Term
blockTerm t blocker = do
(pid, v) <- newProblem blocker
blockTermOnProblem t v pid
blockTermOnProblem
:: (MonadMetaSolver m, MonadFresh Nat m)
=> Type -> Term -> ProblemId -> m Term
blockTermOnProblem t v pid =
ifM (isProblemSolved pid `or2M` isSizeProblem pid) (return v) $ do
i <- createMetaInfo
es <- map Apply <$> getContextArgs
tel <- getContextTelescope
x <- newMeta' (BlockedConst $ abstract tel v)
Instantiable i lowMetaPriority (idP $ size tel)
(HasType () CmpLeq $ telePi_ tel t)
inTopContext $ addConstraint (Guarded (UnBlock x) pid)
reportSDoc "tc.meta.blocked" 20 $ vcat
[ "blocked" <+> prettyTCM x <+> ":=" <+> inTopContext (prettyTCM $ abstract tel v)
, " by" <+> (prettyTCM =<< getConstraintsForProblem pid) ]
inst <- isInstantiatedMeta x
case inst of
True -> instantiate (MetaV x es)
False -> do
(m', v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t
reportSDoc "tc.meta.blocked" 30 $ "setting twin of" <+> prettyTCM m' <+> "to be" <+> prettyTCM x
updateMetaVar m' (\ mv -> mv { mvTwin = Just x })
i <- fresh
cmp <- buildProblemConstraint_ (ValueCmp CmpEq (AsTermsOf t) v (MetaV x es))
reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp
listenToMeta (CheckConstraint i cmp) x
return v
blockTypeOnProblem
:: (MonadMetaSolver m, MonadFresh Nat m)
=> Type -> ProblemId -> m Type
blockTypeOnProblem (El s a) pid = El s <$> blockTermOnProblem (El Inf $ Sort s) a pid
unblockedTester :: Type -> TCM Bool
unblockedTester t = ifBlocked t (\ m t -> return False) (\ _ t -> return True)
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ p = do
postponeTypeCheckingProblem p (unblock p)
where
unblock (CheckExpr _ _ t) = unblockedTester t
unblock (CheckArgs _ _ _ t _ _) = unblockedTester t
unblock (CheckProjAppToKnownPrincipalArg _ _ _ _ _ _ _ _ t) = unblockedTester t
unblock (CheckLambda _ _ _ t) = unblockedTester t
unblock (DoQuoteTerm _ _ _) = __IMPOSSIBLE__
postponeTypeCheckingProblem :: TypeCheckingProblem -> TCM Bool -> TCM Term
postponeTypeCheckingProblem p unblock = do
i <- createMetaInfo' DontRunMetaOccursCheck
tel <- getContextTelescope
cl <- buildClosure p
let t = problemType p
m <- newMeta' (PostponedTypeCheckingProblem cl unblock)
Instantiable i normalMetaPriority (idP (size tel))
$ HasType () CmpLeq $ telePi_ tel t
inTopContext $ reportSDoc "tc.meta.postponed" 20 $ vcat
[ "new meta" <+> prettyTCM m <+> ":" <+> prettyTCM (telePi_ tel t)
, "for postponed typechecking problem" <+> prettyTCM p
]
es <- map Apply <$> getContextArgs
(_, v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t
cmp <- buildProblemConstraint_ (ValueCmp CmpEq (AsTermsOf t) v (MetaV m es))
reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp
i <- liftTCM fresh
listenToMeta (CheckConstraint i cmp) m
addConstraint (UnBlock m)
return v
problemType :: TypeCheckingProblem -> Type
problemType (CheckExpr _ _ t ) = t
problemType (CheckArgs _ _ _ _ t _ ) = t
problemType (CheckProjAppToKnownPrincipalArg _ _ _ _ _ t _ _ _) = t
problemType (CheckLambda _ _ _ t ) = t
problemType (DoQuoteTerm _ _ t) = t
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 $ "waking boxed constraint" <+> prettyTCM c
modifyAwakeConstraints (c:)
solveAwakeConstraints
etaExpandMetaSafe :: (MonadMetaSolver m) => MetaId -> m ()
etaExpandMetaSafe = etaExpandMeta [SingletonRecords,Levels]
etaExpandMetaTCM :: [MetaKind] -> MetaId -> TCM ()
etaExpandMetaTCM kinds m = whenM ((not <$> isFrozen m) `and2M` asksTC envAssignMetas `and2M` isEtaExpandable kinds m) $ do
verboseBracket "tc.meta.eta" 20 ("etaExpandMeta " ++ prettyShow m) $ do
let waitFor x = do
reportSDoc "tc.meta.eta" 20 $ do
"postponing eta-expansion of meta variable" <+>
prettyTCM m <+>
"which is blocked by" <+> prettyTCM x
listenToMeta (EtaExpand m) x
dontExpand = do
reportSDoc "tc.meta.eta" 20 $ do
"we do not expand meta variable" <+> prettyTCM m <+>
text ("(requested was expansion of " ++ show kinds ++ ")")
meta <- lookupMeta m
case mvJudgement meta of
IsSort{} -> dontExpand
HasType _ cmp a -> do
reportSDoc "tc.meta.eta" 40 $ sep
[ text "considering eta-expansion at type "
, prettyTCM a
, text " raw: "
, pretty a
]
TelV tel b <- telView a
reportSDoc "tc.meta.eta" 40 $ sep
[ text "considering eta-expansion at type"
, addContext tel (prettyTCM b)
, text "under telescope"
, prettyTCM tel
]
if any domFinite (flattenTel tel) then dontExpand else do
addContext tel $ do
ifBlocked (unEl b) (\ x _ -> waitFor x) $ \ _ t -> case t of
lvl@(Def r es) ->
ifM (isEtaRecord r) (do
let ps = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
let expand = do
u <- withMetaInfo' meta $
newRecordMetaCtx (mvFrozen meta) r ps tel (idP $ size tel) $ teleArgs tel
inTopContext $ do
reportSDoc "tc.meta.eta" 15 $ sep
[ "eta expanding: " <+> pretty m <+> " --> "
, nest 2 $ prettyTCM u
]
noConstraints $ assignTerm' m (telToArgs tel) 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 (telToArgs tel) $ Level $ ClosedLevel 0
) $ dontExpand
_ -> dontExpand
etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, Reduce t)
=> Blocked t -> m (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
assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m)
=> CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper dir x es v doAssign = do
ifNotM (asksTC envAssignMetas) dontAssign $ do
reportSDoc "tc.meta.assign" 10 $ do
"term" <+> prettyTCM (MetaV x es) <+> text (":" ++ show dir) <+> prettyTCM v
nowSolvingConstraints doAssign `finally` solveAwakeConstraints
where dontAssign = do
reportSLn "tc.meta.assign" 10 "don't assign metas"
patternViolation
assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign dir x args v target = do
mvar <- lookupMeta x
let t = jMetaType $ mvJudgement mvar
v <- instantiate v
reportSDoc "tc.meta.assign" 45 $
"MetaVars.assign: assigning to " <+> prettyTCM v
reportSLn "tc.meta.assign" 75 $
"MetaVars.assign: assigning meta " ++ show x ++ " with args " ++ show args ++ " to " ++ show v
case (v, mvJudgement mvar) of
(Sort s, HasType{}) -> hasBiggerSort s
_ -> return ()
when (mvFrozen mvar == Frozen) $ do
reportSLn "tc.meta.assign" 25 $ "aborting: meta is frozen!"
patternViolation
whenM (isBlockedTerm x) $ do
reportSLn "tc.meta.assign" 25 $ "aborting: meta is a blocked term!"
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 _ -> "r.h.s. blocked on:" <+> prettyTCM m0
NotBlocked{} -> "r.h.s. not blocked"
subtypingForSizeLt dir x mvar t args v $ \ v -> do
reportSDoc "tc.meta.assign.proj" 45 $ do
cxt <- getContextTelescope
vcat
[ "context before projection expansion"
, nest 2 $ inTopContext $ prettyTCM cxt
]
expandProjectedVars args (v, target) $ \ args (v, target) -> do
reportSDoc "tc.meta.assign.proj" 45 $ do
cxt <- getContextTelescope
vcat
[ "context after projection expansion"
, nest 2 $ inTopContext $ prettyTCM cxt
]
let
vars = freeVars args
relVL = filterVarMapToList isRelevant vars
nonstrictVL = filterVarMapToList isNonStrict vars
irrVL = filterVarMapToList (liftM2 (&&) isIrrelevant isUnguarded) vars
reportSDoc "tc.meta.assign" 20 $
let pr (Var n []) = text (show n)
pr (Def c []) = prettyTCM c
pr _ = ".."
in vcat
[ "mvar args:" <+> sep (map (pr . unArg) args)
, "fvars lhs (rel):" <+> sep (map (text . show) relVL)
, "fvars lhs (nonstrict):" <+> sep (map (text . show) nonstrictVL)
, "fvars lhs (irr):" <+> sep (map (text . show) irrVL)
]
v <- liftTCM $ occursCheck x vars v
reportSLn "tc.meta.assign" 15 "passed occursCheck"
verboseS "tc.meta.assign" 30 $ do
let n = termSize v
when (n > 200) $ reportSDoc "tc.meta.assign" 30 $
sep [ "size" <+> text (show n)
, nest 2 $ "term" <+> prettyTCM v
]
let fvs = allFreeVars v
reportSDoc "tc.meta.assign" 20 $
"fvars rhs:" <+> sep (map (text . show) $ VarSet.toList fvs)
mids <- do
res <- runExceptT $ inverseSubst args
case res of
Right ids -> do
reportSDoc "tc.meta.assign" 50 $
"inverseSubst returns:" <+> sep (map prettyTCM ids)
let boundVars = VarSet.fromList $ map fst ids
if | fvs `VarSet.isSubsetOf` boundVars -> return $ Just ids
| otherwise -> return Nothing
Left CantInvert -> return Nothing
Left NeutralArg -> Just <$> attemptPruning x args fvs
Left ProjectedVar{} -> Just <$> attemptPruning x args fvs
case mids of
Nothing -> patternViolation
Just ids -> do
ids <- do
res <- runExceptT $ checkLinearity ids
case res of
Right ids -> return ids
Left () -> attemptPruning x args fvs
let n = length args
TelV tel' _ <- telViewUpToPath n t
let sigma = parallelS $ reverse $ map unArg args
hasSubtyping <- collapseDefault . optSubtyping <$> pragmaOptions
when hasSubtyping $ forM_ ids $ \(i , u) -> do
a <- applySubst sigma <$> addContext tel' (infer u)
a' <- typeOfBV i
checkSubtypeIsEqual a' a
`catchError` \case
TypeError{} -> patternViolation
err -> throwError err
m <- getContextSize
assignMeta' m x t n ids v
where
attemptPruning
:: MetaId
-> Args
-> FVs
-> TCM a
attemptPruning x args fvs = do
killResult <- prune x args $ (`VarSet.member` fvs)
reportSDoc "tc.meta.assign" 10 $
"pruning" <+> prettyTCM x <+> do
text $
if killResult `elem` [PrunedSomething,PrunedEverything] then "succeeded"
else "failed"
patternViolation
assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta m x t ids v = do
let n = length ids
cand = List.sort $ zip ids $ map var $ downFrom n
assignMeta' m x t n cand v
assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' m x t n ids v = do
reportSDoc "tc.meta.assign" 25 $
"preparing to instantiate: " <+> prettyTCM v
let assocToList i l = case l of
_ | i >= m -> []
((j,u) : l) | i == j -> Just u : assocToList (i+1) l
_ -> Nothing : assocToList (i+1) l
ivs = assocToList 0 ids
rho = prependS __IMPOSSIBLE__ ivs $ raiseS n
v' = applySubst rho v
inTopContext $ do
reportSDoc "tc.meta.assign" 15 $ "type of meta =" <+> prettyTCM t
(telv@(TelV tel' a),bs) <- telViewUpToPathBoundary n t
reportSDoc "tc.meta.assign" 30 $ "tel' =" <+> prettyTCM tel'
reportSDoc "tc.meta.assign" 30 $ "#args =" <+> text (show n)
when (size tel' < n)
patternViolation
whenM ((not . optCompareSorts <$> pragmaOptions) `or2M`
(optCumulativity <$> pragmaOptions)) $ case unEl a of
Sort s -> addContext tel' $ do
m <- lookupMeta x
cmp <- ifM (not . optCumulativity <$> pragmaOptions) (return CmpEq) $
case mvJudgement m of
HasType{ jComparison = cmp } -> return cmp
IsSort{} -> __IMPOSSIBLE__
s' <- sortOf v'
reportSDoc "tc.meta.assign" 40 $
"Instantiating sort" <+> prettyTCM s <+>
"to sort" <+> prettyTCM s' <+> "of solution" <+> prettyTCM v'
traceCall (CheckMetaSolution (getRange m) x a v') $
compareSort cmp s' s
_ -> return ()
let vsol = abstract tel' v'
whenM (optDoubleCheck <$> pragmaOptions) $ do
m <- lookupMeta x
reportSDoc "tc.meta.check" 30 $ "double checking solution"
catchConstraint (CheckMetaInst x) $
addContext tel' $ checkSolutionForMeta x m v' a
reportSDoc "tc.meta.assign" 10 $
"solving" <+> prettyTCM x <+> ":=" <+> prettyTCM vsol
v' <- blockOnBoundary telv bs v'
assignTerm x (telToArgs tel') v'
where
blockOnBoundary :: TelView -> Boundary -> Term -> TCM Term
blockOnBoundary telv [] v = return v
blockOnBoundary (TelV tel t) bs v = addContext tel $
blockTerm t $ do
neg <- primINeg
forM_ bs $ \ (r,(x,y)) -> do
equalTermOnFace (neg `apply1` r) t x v
equalTermOnFace r t y v
return v
checkMetaInst :: MetaId -> TCM ()
checkMetaInst x = do
m <- lookupMeta x
let postpone = addConstraint $ CheckMetaInst x
case mvInstantiation m of
BlockedConst{} -> postpone
PostponedTypeCheckingProblem{} -> postpone
Open{} -> postpone
OpenInstance{} -> postpone
InstV xs v -> do
let n = size xs
t = jMetaType $ mvJudgement m
(telv@(TelV tel a),bs) <- telViewUpToPathBoundary n t
catchConstraint (CheckMetaInst x) $ addContext tel $ checkSolutionForMeta x m v a
checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta x m v a = do
reportSDoc "tc.meta.check" 30 $ "checking solution for meta" <+> prettyTCM x
case mvJudgement m of
HasType{ jComparison = cmp } -> do
reportSDoc "tc.meta.check" 30 $ nest 2 $
prettyTCM x <+> " : " <+> prettyTCM a <+> ":=" <+> prettyTCM v
reportSDoc "tc.meta.check" 50 $ nest 2 $ do
ctx <- getContext
inTopContext $ "in context: " <+> prettyTCM (PrettyContext ctx)
traceCall (CheckMetaSolution (getRange m) x a v) $
checkInternal v cmp a
IsSort{} -> void $ do
reportSDoc "tc.meta.check" 30 $ nest 2 $
prettyTCM x <+> ":=" <+> prettyTCM v <+> " is a sort"
s <- shouldBeSort (El __DUMMY_SORT__ v)
traceCall (CheckMetaSolution (getRange m) x (sort (univSort Nothing s)) (Sort s)) $
checkSort defaultAction s
checkSubtypeIsEqual :: Type -> Type -> TCM ()
checkSubtypeIsEqual a b = do
reportSDoc "tc.meta.subtype" 30 $
"checking that subtype" <+> prettyTCM a <+>
"of" <+> prettyTCM b <+> "is actually equal."
((a, b), equal) <- SynEq.checkSyntacticEquality a b
unless equal $ do
cumulativity <- optCumulativity <$> pragmaOptions
reduce (unEl b) >>= \case
Sort sb -> reduce (unEl a) >>= \case
Sort sa | cumulativity -> equalSort sa sb
| otherwise -> return ()
MetaV{} -> patternViolation
Dummy{} -> return ()
_ -> patternViolation
Pi b1 b2 -> reduce (unEl a) >>= \case
Pi a1 a2
| getRelevance a1 /= getRelevance b1 -> patternViolation
| getQuantity a1 /= getQuantity b1 -> patternViolation
| getCohesion a1 /= getCohesion b1 -> patternViolation
| otherwise -> do
checkSubtypeIsEqual (unDom b1) (unDom a1)
underAbstractionAbs a1 a2 $ \a2' -> checkSubtypeIsEqual a2' (absBody b2)
MetaV{} -> patternViolation
Dummy{} -> return ()
_ -> patternViolation
MetaV{} -> patternViolation
_ -> return ()
subtypingForSizeLt
:: CompareDirection
-> MetaId
-> MetaVariable
-> Type
-> Args
-> Term
-> (Term -> TCM ())
-> TCM ()
subtypingForSizeLt DirEq x mvar t args v cont = cont v
subtypingForSizeLt dir x mvar t args v cont = do
let fallback = cont v
(mSize, mSizeLt) <- getBuiltinSize
caseMaybe mSize fallback $ \ qSize -> do
caseMaybe mSizeLt fallback $ \ qSizeLt -> do
v <- reduce v
case v of
Def q [Apply (Arg ai u)] | q == qSizeLt -> do
TelV tel _ <- telView t
let size = sizeType_ qSize
t' = telePi tel size
y <- newMeta Instantiable (mvInfo mvar) (mvPriority mvar) (mvPermutation mvar)
(HasType __IMPOSSIBLE__ CmpLeq t')
let yArgs = MetaV y $ map Apply args
addConstraint $ dirToCmp (`ValueCmp` AsSizes) dir yArgs u
let xArgs = MetaV x $ map Apply args
v' = Def qSizeLt [Apply $ Arg ai yArgs]
c = dirToCmp (`ValueCmp` (AsTermsOf sizeUniv)) dir xArgs v'
catchConstraint c $ cont v'
_ -> fallback
expandProjectedVars
:: ( Show a, PrettyTCM a, NoProjectedVar a
, ReduceAndEtaContract a
, PrettyTCM b, Subst Term b
)
=> a
-> b
-> (a -> b -> TCM c)
-> TCM c
expandProjectedVars args v ret = loop (args, v) where
loop (args, v) = do
reportSDoc "tc.meta.assign.proj" 45 $ "meta args: " <+> prettyTCM args
args <- callByName $ reduceAndEtaContract args
reportSDoc "tc.meta.assign.proj" 45 $ "norm args: " <+> prettyTCM args
reportSDoc "tc.meta.assign.proj" 85 $ "norm args: " <+> text (show args)
let done = ret args v
case noProjectedVar args of
Right () -> do
reportSDoc "tc.meta.assign.proj" 40 $
"no projected var found in args: " <+> prettyTCM args
done
Left (ProjVarExc i _) -> etaExpandProjectedVar i (args, v) done loop
etaExpandProjectedVar :: (PrettyTCM a, Subst Term a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar i v fail succeed = do
reportSDoc "tc.meta.assign.proj" 40 $
"trying to expand projected variable" <+> prettyTCM (var i)
caseMaybeM (etaExpandBoundVar i) fail $ \ (delta, sigma, tau) -> do
reportSDoc "tc.meta.assign.proj" 25 $
"eta-expanding var " <+> prettyTCM (var i) <+>
" in terms " <+> prettyTCM v
unsafeInTopContext $ addContext delta $
succeed $ applySubst tau v
class NoProjectedVar a where
noProjectedVar :: a -> Either ProjVarExc ()
data ProjVarExc = ProjVarExc Int [(ProjOrigin, QName)]
instance NoProjectedVar Term where
noProjectedVar t =
case t of
Var i es
| qs@(_:_) <- takeWhileJust id $ map isProjElim es -> Left $ ProjVarExc i qs
Con (ConHead _ Inductive (_:_)) _ es | Just vs <- allApplyElims es -> noProjectedVar vs
_ -> return ()
instance NoProjectedVar a => NoProjectedVar (Arg a) where
noProjectedVar = Fold.mapM_ noProjectedVar
instance NoProjectedVar a => NoProjectedVar [a] where
noProjectedVar = Fold.mapM_ noProjectedVar
class (TermLike a, Subst Term a, Reduce a) => ReduceAndEtaContract a where
reduceAndEtaContract :: a -> TCM a
default reduceAndEtaContract
:: (Traversable f, TermLike b, Subst Term b, Reduce b, ReduceAndEtaContract b, f b ~ a)
=> a -> TCM a
reduceAndEtaContract = Trav.mapM reduceAndEtaContract
instance ReduceAndEtaContract a => ReduceAndEtaContract [a] where
instance ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) where
instance ReduceAndEtaContract Term where
reduceAndEtaContract u = do
reduce u >>= \case
Lam ai (Abs x b) -> etaLam ai x =<< reduceAndEtaContract b
Con c ci es -> etaCon c ci es $ \ r c ci args -> do
args <- reduceAndEtaContract args
etaContractRecord r c ci args
v -> return v
type FVs = VarSet
type SubstCand = [(Int,Term)]
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
checkLinearity ids0 = do
let ids = List.sortBy (compare `on` fst) ids0
let grps = groupOn fst ids
concat <$> mapM makeLinear grps
where
makeLinear :: SubstCand -> ExceptT () TCM SubstCand
makeLinear [] = __IMPOSSIBLE__
makeLinear grp@[_] = return grp
makeLinear (p@(i,t) : _) =
ifM ((Right True ==) <$> do lift . isSingletonTypeModuloRelevance =<< typeOfBV i)
(return [p])
(throwError ())
type Res = [(Arg Nat, Term)]
data InvertExcept
= CantInvert
| NeutralArg
| ProjectedVar Int [(ProjOrigin, QName)]
inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand
inverseSubst args = map (mapFst unArg) <$> loop (zip args terms)
where
loop = foldM isVarOrIrrelevant []
terms = map var (downFrom (size args))
failure = do
lift $ reportSDoc "tc.meta.assign" 15 $ vcat
[ "not all arguments are variables: " <+> prettyTCM args
, " aborting assignment" ]
throwError CantInvert
neutralArg = throwError NeutralArg
isVarOrIrrelevant :: Res -> (Arg Term, Term) -> ExceptT InvertExcept TCM Res
isVarOrIrrelevant vars (Arg info v, t) = do
let irr | isIrrelevant info = True
| DontCare{} <- v = True
| otherwise = False
case stripDontCare v of
Var i [] -> return $ (Arg info i, t) `cons` vars
Var i es | Just qs <- mapM isProjElim es ->
throwError $ ProjectedVar i qs
Con c ci es -> do
let fallback
| isIrrelevant info = return vars
| otherwise = failure
irrProj <- optIrrelevantProjections <$> pragmaOptions
(lift $ isRecordConstructor $ conName c) >>= \case
Just (_, r@Record{ recFields = fs })
| YesEta <- recEtaEquality r
, length fs == length es
, hasQuantity0 info || all usableQuantity fs
, irrProj || all isRelevant fs -> do
let aux (Arg _ v) Dom{domInfo = info', unDom = f} = (Arg ai v,) $ t `applyE` [Proj ProjSystem f] where
ai = ArgInfo
{ argInfoHiding = min (getHiding info) (getHiding info')
, argInfoModality = Modality
{ modRelevance = max (getRelevance info) (getRelevance info')
, modQuantity = max (getQuantity info) (getQuantity info')
, modCohesion = max (getCohesion info) (getCohesion info')
}
, argInfoOrigin = min (getOrigin info) (getOrigin info')
, argInfoFreeVariables = unknownFreeVariables
}
vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
res <- loop $ zipWith aux vs fs
return $ res `append` vars
| otherwise -> fallback
_ -> fallback
_ | irr -> return vars
Var{} -> neutralArg
Def{} -> neutralArg
Lam{} -> failure
Lit{} -> failure
MetaV{} -> failure
Pi{} -> neutralArg
Sort{} -> neutralArg
Level{} -> neutralArg
DontCare{} -> __IMPOSSIBLE__
Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s
append :: Res -> Res -> Res
append res vars = foldr cons vars res
cons :: (Arg Nat, Term) -> Res -> Res
cons a@(Arg ai i, t) vars
| isIrrelevant ai = applyUnless (any ((i==) . unArg . fst) vars) (a :) vars
| otherwise = a :
filter (not . (\ a@(Arg info j, t) -> isIrrelevant info && i == j)) vars
openMetasToPostulates :: TCM ()
openMetasToPostulates = do
m <- asksTC envCurrentModule
ms <- IntMap.assocs <$> useTC stMetaStore
forM_ ms $ \ (x, mv) -> do
when (isOpenMeta $ mvInstantiation mv) $ do
let t = dummyTypeToOmega $ jMetaType $ mvJudgement mv
let r = clValue $ miClosRange $ mvInfo mv
let s = "unsolved#meta." ++ show x
n <- freshName r s
let q = A.QName m n
reportSDoc "meta.postulate" 20 $ vcat
[ text ("Turning " ++ if isSortMeta_ mv then "sort" else "value" ++ " meta ")
<+> prettyTCM (MetaId x) <+> " into postulate."
, nest 2 $ vcat
[ "Name: " <+> prettyTCM q
, "Type: " <+> prettyTCM t
]
]
addConstant q $ defaultDefn defaultArgInfo q t Axiom
let inst = InstV [] $ Def q []
updateMetaVar (MetaId x) $ \ mv0 -> mv0 { mvInstantiation = inst }
return ()
where
dummyTypeToOmega t =
case telView' t of
TelV tel (El _ Dummy{}) -> abstract tel topSort
_ -> t
dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas metas = do
metaGraph <- concat <$> do
forM metas $ \ m -> do
deps <- allMetas (\ m' -> if m' `elem` metas then singleton m' else mempty) <$> getType m
return [ (m, m') | m' <- Set.toList deps ]
return $ Graph.topSort metas metaGraph
where
getType m = do
mv <- lookupMeta m
case mvJudgement mv of
IsSort{} -> return Nothing
HasType{ jMetaType = t } -> Just <$> instantiateFull t