module Agda.TypeChecking.Constraints where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import qualified Data.List as List
import qualified Data.Set as Set
import Agda.Syntax.Internal
import Agda.TypeChecking.Free
import Agda.TypeChecking.Monad
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.LevelConstraints
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.MetaVars.Mention
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Empty
import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Lens
import Agda.Utils.Size
import qualified Agda.Utils.VarSet as VarSet
#include "undefined.h"
import Agda.Utils.Impossible
catchConstraint :: Constraint -> TCM () -> TCM ()
catchConstraint c v = liftTCM $
catchError_ v $ \err ->
case err of
PatternErr{} -> addConstraint c
_ -> throwError err
addConstraint :: Constraint -> TCM ()
addConstraint c = do
pids <- asks envActiveProblems
reportSDoc "tc.constr.add" 20 $ hsep
[ text "adding constraint"
, text (show $ Set.toList pids)
, prettyTCM c ]
c <- reduce =<< instantiateFull c
c' <- simpl c
if (c /= c')
then do
reportSDoc "tc.constr.add" 20 $ text " simplified:" <+> prettyTCM c'
solveConstraint_ c'
else addConstraint' c'
unless (isIFSConstraint c) $
wakeConstraints (isWakeableIFSConstraint . clValue . theConstraint)
where
isWakeableIFSConstraint :: Constraint -> TCM Bool
isWakeableIFSConstraint (FindInScope _ b _) = caseMaybe b (return True) (\m -> isInstantiatedMeta m)
isWakeableIFSConstraint _ = return False
isIFSConstraint :: Constraint -> Bool
isIFSConstraint FindInScope{} = True
isIFSConstraint _ = False
isLvl LevelCmp{} = True
isLvl _ = False
simpl :: Constraint -> TCM Constraint
simpl c = if not $ isLvl c then return c else do
cs <- map theConstraint <$> getAllConstraints
lvls <- instantiateFull $ List.filter (isLvl . clValue) cs
when (not $ null lvls) $ do
reportSDoc "tc.constr.lvl" 40 $ text "simplifying level constraint" <+> prettyTCM c
$$ nest 2 (hang (text "using") 2 (prettyTCM lvls))
let c' = simplifyLevelConstraint c $ map clValue lvls
reportSDoc "tc.constr.lvl" 40 $
if c' /= c then text "simplified to" <+> prettyTCM c'
else text "no simplification"
return c'
noConstraints :: TCM a -> TCM a
noConstraints problem = liftTCM $ do
(pid, x) <- newProblem problem
cs <- getConstraintsForProblem pid
w <- warning_ (UnsolvedConstraints cs)
unless (null cs) $ typeError $ NonFatalErrors [ w ]
return x
newProblem :: TCM a -> TCM (ProblemId, a)
newProblem action = do
pid <- fresh
x <- nowSolvingConstraints $ solvingProblem pid action
solveAwakeConstraints
return (pid, x)
newProblem_ :: TCM () -> TCM 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
wakeupConstraints :: MetaId -> TCM ()
wakeupConstraints x = do
wakeConstraints (return . mentionsMeta x)
solveAwakeConstraints
wakeupConstraints_ :: TCM ()
wakeupConstraints_ = do
wakeConstraints (return . const True)
solveAwakeConstraints
solveAwakeConstraints :: TCM ()
solveAwakeConstraints = solveAwakeConstraints' False
solveAwakeConstraints' :: Bool -> TCM ()
solveAwakeConstraints' force = do
verboseS "profile.constraints" 10 $ liftTCM $ tickMax "max-open-constraints" . List.genericLength =<< getAllConstraints
whenM ((force ||) . not <$> isSolvingConstraints) $ nowSolvingConstraints $ do
locally eActiveProblems (const Set.empty) solve
where
solve = do
reportSDoc "tc.constr.solve" 10 $ hsep [ text "Solving awake constraints."
, text . show . length =<< getAwakeConstraints
, text "remaining." ]
whenJustM takeAwakeConstraint $ \ c -> do
withConstraint solveConstraint c
solve
solveConstraint :: Constraint -> TCM ()
solveConstraint c = do
verboseS "profile.constraints" 10 $ liftTCM $ tick "attempted-constraints"
verboseBracket "tc.constr.solve" 20 "solving constraint" $ do
pids <- asks envActiveProblems
reportSDoc "tc.constr.solve" 20 $ text (show $ Set.toList pids) <+> prettyTCM c
solveConstraint_ c
solveConstraint_ :: Constraint -> TCM ()
solveConstraint_ (ValueCmp cmp a u v) = compareTerm cmp a u v
solveConstraint_ (ElimCmp cmp a e u v) = compareElims cmp a e u v
solveConstraint_ (TypeCmp cmp a b) = compareType cmp a b
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) = isEmptyType r t
solveConstraint_ (CheckSizeLtSat t) = checkSizeLtSat t
solveConstraint_ (UnBlock m) =
ifM (isFrozen m) (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{} -> return ()
Open -> __IMPOSSIBLE__
OpenIFS -> __IMPOSSIBLE__
solveConstraint_ (FindInScope m b cands) = findInScope m cands
checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
checkTypeCheckingProblem p = case p of
CheckExpr e t -> checkExpr e t
CheckArgs eh r args t0 t1 k -> checkArguments' eh r args t0 t1 k
CheckLambda args body target -> checkPostponedLambda args body target
UnquoteTactic tac hole t -> unquoteTactic tac hole t $ return hole
debugConstraints :: TCM ()
debugConstraints = verboseS "tc.constr" 50 $ do
awake <- use stAwakeConstraints
sleeping <- use stSleepingConstraints
reportSDoc "" 0 $ vcat
[ text "Current constraints"
, nest 2 $ vcat [ text "awake " <+> vcat (map prettyTCM awake)
, text "asleep" <+> vcat (map prettyTCM sleeping) ] ]