{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Constraints where
import Prelude hiding (null)
import Control.Monad
import qualified Data.List as List
import qualified Data.Set as Set
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.LevelConstraints
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Sort
import Agda.TypeChecking.MetaVars.Mention
import Agda.TypeChecking.Warnings
import {-# SOURCE #-} Agda.TypeChecking.Rules.Application
import {-# SOURCE #-} Agda.TypeChecking.Rules.Def
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import {-# SOURCE #-} Agda.TypeChecking.Empty
import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Impossible
instance MonadConstraint TCM where
catchPatternErr = catchPatternErrTCM
addConstraint = addConstraintTCM
addAwakeConstraint = addAwakeConstraint'
solveConstraint = solveConstraintTCM
solveSomeAwakeConstraints = solveSomeAwakeConstraintsTCM
wakeConstraints = wakeConstraintsTCM
stealConstraints = stealConstraintsTCM
modifyAwakeConstraints = modifyTC . mapAwakeConstraints
modifySleepingConstraints = modifyTC . mapSleepingConstraints
catchPatternErrTCM :: TCM a -> TCM a -> TCM a
catchPatternErrTCM handle v =
catchError_ v $ \err ->
case err of
PatternErr{} -> handle
_ -> throwError err
addConstraintTCM :: Constraint -> TCM ()
addConstraintTCM c = do
pids <- asksTC envActiveProblems
reportSDoc "tc.constr.add" 20 $ hsep
[ "adding constraint"
, text (show $ Set.toList pids)
, prettyTCM c ]
c <- reduce =<< instantiateFull c
caseMaybeM (simpl c) (addConstraint' c) $ \ cs -> do
reportSDoc "tc.constr.add" 20 $ " simplified:" <+> prettyList (map prettyTCM cs)
mapM_ solveConstraint_ cs
unless (isInstanceConstraint c) $
wakeConstraints' (isWakeableInstanceConstraint . clValue . theConstraint)
where
isWakeableInstanceConstraint :: Constraint -> TCM Bool
isWakeableInstanceConstraint = \case
FindInstance _ b _ -> maybe (return True) isInstantiatedMeta b
_ -> return False
isLvl LevelCmp{} = True
isLvl _ = False
simpl :: Constraint -> TCM (Maybe [Constraint])
simpl c
| isLvl c = do
lvlcs <- instantiateFull =<< do
List.filter (isLvl . clValue) . map theConstraint <$> getAllConstraints
unless (null lvlcs) $ do
reportSDoc "tc.constr.lvl" 40 $ vcat
[ "simplifying level constraint" <+> prettyTCM c
, nest 2 $ hang "using" 2 $ prettyTCM lvlcs
]
return $ simplifyLevelConstraint c $ map clValue lvlcs
| otherwise = return Nothing
wakeConstraintsTCM :: (ProblemConstraint-> TCM Bool) -> TCM ()
wakeConstraintsTCM wake = do
c <- useR stSleepingConstraints
(wakeup, sleepin) <- partitionM wake c
reportSLn "tc.constr.wake" 50 $
"waking up " ++ show (List.map (Set.toList . constraintProblems) wakeup) ++ "\n" ++
" still sleeping: " ++ show (List.map (Set.toList . constraintProblems) sleepin)
modifySleepingConstraints $ const sleepin
modifyAwakeConstraints (++ wakeup)
stealConstraintsTCM :: ProblemId -> TCM ()
stealConstraintsTCM pid = do
current <- asksTC envActiveProblems
reportSLn "tc.constr.steal" 50 $ "problem " ++ show (Set.toList current) ++ " is stealing problem " ++ show pid ++ "'s constraints!"
let rename pc@(PConstr pids c) | Set.member pid pids = PConstr (Set.union current pids) c
| otherwise = pc
whenM (Set.member pid <$> asksTC envActiveProblems) __IMPOSSIBLE__
modifyAwakeConstraints $ List.map rename
modifySleepingConstraints $ List.map rename
noConstraints
:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> m a -> m a
noConstraints problem = do
(pid, x) <- newProblem problem
cs <- getConstraintsForProblem pid
unless (null cs) $ do
w <- warning_ (UnsolvedConstraints cs)
typeError $ NonFatalErrors [ w ]
return x
newProblem
:: (MonadFresh ProblemId m, MonadConstraint m)
=> m a -> m (ProblemId, a)
newProblem action = do
pid <- fresh
x <- nowSolvingConstraints $ solvingProblem pid action
solveAwakeConstraints
return (pid, x)
newProblem_
:: (MonadFresh ProblemId m, MonadConstraint m)
=> m a -> m ProblemId
newProblem_ action = fst <$> newProblem action
ifNoConstraints :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
ifNoConstraints check ifNo ifCs = do
(pid, x) <- newProblem check
ifM (isProblemSolved pid) (ifNo x) (ifCs pid x)
ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ check ifNo ifCs = ifNoConstraints check (const ifNo) (\pid _ -> ifCs pid)
guardConstraint :: Constraint -> TCM () -> TCM ()
guardConstraint c blocker =
ifNoConstraints_ blocker (solveConstraint c) (addConstraint . Guarded c)
whenConstraints :: TCM () -> TCM () -> TCM ()
whenConstraints action handler =
ifNoConstraints_ action (return ()) $ \pid -> do
stealConstraints pid
handler
wakeConstraints' :: (ProblemConstraint -> TCM Bool) -> TCM ()
wakeConstraints' p = do
skipInstance <- shouldPostponeInstanceSearch
wakeConstraints (\ c -> (&&) (not $ skipInstance && isInstanceConstraint (clValue $ theConstraint c)) <$> p c)
wakeupConstraints :: MetaId -> TCM ()
wakeupConstraints x = do
wakeConstraints' (return . mentionsMeta x)
solveAwakeConstraints
wakeupConstraints_ :: TCM ()
wakeupConstraints_ = do
wakeConstraints' (return . const True)
solveAwakeConstraints
solveAwakeConstraints :: (MonadConstraint m) => m ()
solveAwakeConstraints = solveAwakeConstraints' False
solveAwakeConstraints' :: (MonadConstraint m) => Bool -> m ()
solveAwakeConstraints' = solveSomeAwakeConstraints (const True)
solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM solveThis force = do
verboseS "profile.constraints" 10 $ liftTCM $ tickMax "max-open-constraints" . List.genericLength =<< getAllConstraints
whenM ((force ||) . not <$> isSolvingConstraints) $ nowSolvingConstraints $ do
locallyTC eActiveProblems (const Set.empty) solve
where
solve = do
reportSDoc "tc.constr.solve" 10 $ hsep [ "Solving awake constraints."
, text . show . length =<< getAwakeConstraints
, "remaining." ]
whenJustM (takeAwakeConstraint' solveThis) $ \ c -> do
withConstraint solveConstraint c
solve
solveConstraintTCM :: Constraint -> TCM ()
solveConstraintTCM c = do
verboseS "profile.constraints" 10 $ liftTCM $ tick "attempted-constraints"
verboseBracket "tc.constr.solve" 20 "solving constraint" $ do
pids <- asksTC envActiveProblems
reportSDoc "tc.constr.solve.constr" 20 $ text (show $ Set.toList pids) <+> prettyTCM c
solveConstraint_ c
solveConstraint_ :: Constraint -> TCM ()
solveConstraint_ (ValueCmp cmp a u v) = compareAs cmp a u v
solveConstraint_ (ValueCmpOnFace cmp p a u v) = compareTermOnFace cmp p a u v
solveConstraint_ (ElimCmp cmp fs a e u v) = compareElims cmp fs a e u v
solveConstraint_ (TelCmp a b cmp tela telb) = compareTel a b cmp tela telb
solveConstraint_ (SortCmp cmp s1 s2) = compareSort cmp s1 s2
solveConstraint_ (LevelCmp cmp a b) = compareLevel cmp a b
solveConstraint_ c0@(Guarded c pid) = do
ifM (isProblemSolved pid)
(do
reportSLn "tc.constr.solve" 50 $ "Guarding problem " ++ show pid ++ " is solved, moving on..."
solveConstraint_ c)
$ do
reportSLn "tc.constr.solve" 50 $ "Guarding problem " ++ show pid ++ " is still unsolved."
addConstraint c0
solveConstraint_ (IsEmpty r t) = ensureEmptyType r t
solveConstraint_ (CheckSizeLtSat t) = checkSizeLtSat t
solveConstraint_ (UnquoteTactic _ tac hole goal) = unquoteTactic tac hole goal
solveConstraint_ (UnBlock m) =
ifM (isFrozen m `or2M` (not <$> asksTC envAssignMetas)) (addConstraint $ UnBlock m) $ do
inst <- mvInstantiation <$> lookupMeta m
reportSDoc "tc.constr.unblock" 15 $ text ("unblocking a metavar yields the constraint: " ++ show inst)
case inst of
BlockedConst t -> do
reportSDoc "tc.constr.blocked" 15 $
text ("blocked const " ++ prettyShow m ++ " :=") <+> prettyTCM t
assignTerm m [] t
PostponedTypeCheckingProblem cl unblock -> enterClosure cl $ \prob -> do
ifNotM unblock (addConstraint $ UnBlock m) $ do
tel <- getContextTelescope
v <- liftTCM $ checkTypeCheckingProblem prob
assignTerm m (telToArgs tel) v
InstV{} -> __IMPOSSIBLE__
Open -> __IMPOSSIBLE__
OpenInstance -> __IMPOSSIBLE__
solveConstraint_ (FindInstance m b cands) = findInstance m cands
solveConstraint_ (CheckFunDef d i q cs) = withoutCache $
checkFunDef d i q cs
solveConstraint_ (HasBiggerSort a) = hasBiggerSort a
solveConstraint_ (HasPTSRule a b) = hasPTSRule a b
solveConstraint_ (CheckMetaInst m) = checkMetaInst m
checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
checkTypeCheckingProblem p = case p of
CheckExpr cmp e t -> checkExpr' cmp e t
CheckArgs eh r args t0 t1 k -> checkArguments eh r args t0 t1 k
CheckProjAppToKnownPrincipalArg cmp e o ds args t k v0 pt ->
checkProjAppToKnownPrincipalArg cmp e o ds args t k v0 pt
CheckLambda cmp args body target -> checkPostponedLambda cmp args body target
DoQuoteTerm cmp et t -> doQuoteTerm cmp et t
debugConstraints :: TCM ()
debugConstraints = verboseS "tc.constr" 50 $ do
awake <- useTC stAwakeConstraints
sleeping <- useTC stSleepingConstraints
reportSDoc "tc.constr" 50 $ vcat
[ "Current constraints"
, nest 2 $ vcat [ "awake " <+> vcat (map prettyTCM awake)
, "asleep" <+> vcat (map prettyTCM sleeping) ] ]