Agda.TypeChecking.Monad.Constraints

Documentation

solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a

solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a

isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool

isProblemCompletelySolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool

isProblemSolved' :: (MonadTCEnv m, ReadTCState m) => Bool -> ProblemId -> m Bool

getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints

getAwakeConstraints :: ReadTCState m => m Constraints

Get the awake constraints

dropConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()

takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints

Takes out all constraints matching given filter. Danger! The taken constraints need to be solved or put back at some point.

putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()

putAllConstraintsToSleep :: MonadConstraint m => m ()

data ConstraintStatus

Constructors

AwakeConstraint

SleepingConstraint

Instances

Show ConstraintStatus

Defined in Agda.TypeChecking.Monad.Constraints

Methods

showsPrec :: Int -> ConstraintStatus -> ShowS

show :: ConstraintStatus -> String

showList :: [ConstraintStatus] -> ShowS

Eq ConstraintStatus

Defined in Agda.TypeChecking.Monad.Constraints

Methods

(==) :: ConstraintStatus -> ConstraintStatus -> Bool

(/=) :: ConstraintStatus -> ConstraintStatus -> Bool

holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a

Suspend constraints matching the predicate during the execution of the second argument. Caution: held sleeping constraints will not be woken up by events that would normally trigger a wakeup call.

takeAwakeConstraint :: MonadConstraint m => m (Maybe ProblemConstraint)

takeAwakeConstraint' :: MonadConstraint m => (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)

getAllConstraints :: ReadTCState m => m Constraints

withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a

buildProblemConstraint :: (MonadTCEnv m, ReadTCState m) => Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint

buildProblemConstraint_ :: (MonadTCEnv m, ReadTCState m) => Blocker -> Constraint -> m ProblemConstraint

buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint

class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, MonadBlock m, HasOptions m, MonadDebug m) => MonadConstraint m where

Monad service class containing methods for adding and solving constraints

Methods

addConstraint :: Blocker -> Constraint -> m ()

Unconditionally add the constraint.

addAwakeConstraint :: Blocker -> Constraint -> m ()

Add constraint as awake constraint.

solveConstraint :: Constraint -> m ()

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m ()

Solve awake constraints matching the predicate. If the second argument is True solve constraints even if already isSolvingConstraints.

wakeConstraints :: (ProblemConstraint -> WakeUp) -> m ()

stealConstraints :: ProblemId -> m ()

modifyAwakeConstraints :: (Constraints -> Constraints) -> m ()

modifySleepingConstraints :: (Constraints -> Constraints) -> m ()

Instances

MonadConstraint TCM

Defined in Agda.TypeChecking.Constraints

Methods

addConstraint :: Blocker -> Constraint -> TCM ()

addAwakeConstraint :: Blocker -> Constraint -> TCM ()

solveConstraint :: Constraint -> TCM ()

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()

wakeConstraints :: (ProblemConstraint -> WakeUp) -> TCM ()

stealConstraints :: ProblemId -> TCM ()

modifyAwakeConstraints :: (Constraints -> Constraints) -> TCM ()

modifySleepingConstraints :: (Constraints -> Constraints) -> TCM ()

(PureTCM m, MonadBlock m) => MonadConstraint (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addConstraint :: Blocker -> Constraint -> PureConversionT m ()

addAwakeConstraint :: Blocker -> Constraint -> PureConversionT m ()

solveConstraint :: Constraint -> PureConversionT m ()

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> PureConversionT m ()

wakeConstraints :: (ProblemConstraint -> WakeUp) -> PureConversionT m ()

stealConstraints :: ProblemId -> PureConversionT m ()

modifyAwakeConstraints :: (Constraints -> Constraints) -> PureConversionT m ()

modifySleepingConstraints :: (Constraints -> Constraints) -> PureConversionT m ()

MonadConstraint m => MonadConstraint (ReaderT e m)

Defined in Agda.TypeChecking.Monad.Constraints

Methods

addConstraint :: Blocker -> Constraint -> ReaderT e m ()

addAwakeConstraint :: Blocker -> Constraint -> ReaderT e m ()

solveConstraint :: Constraint -> ReaderT e m ()

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> ReaderT e m ()

wakeConstraints :: (ProblemConstraint -> WakeUp) -> ReaderT e m ()

stealConstraints :: ProblemId -> ReaderT e m ()

modifyAwakeConstraints :: (Constraints -> Constraints) -> ReaderT e m ()

modifySleepingConstraints :: (Constraints -> Constraints) -> ReaderT e m ()

addConstraint' :: Blocker -> Constraint -> TCM ()

Add new a constraint

addAwakeConstraint' :: Blocker -> Constraint -> TCM ()

addConstraintTo :: Lens' TCState Constraints -> Blocker -> Constraint -> TCM ()

isBlockingConstraint :: Constraint -> Bool

A problem is considered solved if there are no unsolved blocking constraints belonging to it. There's no really good principle for what constraints are blocking and which are not, but the general idea is that nothing bad should happen if you assume a non-blocking constraint is solvable, but it turns out it isn't. For instance, assuming an equality constraint between two types that turns out to be false can lead to ill typed terms in places where we don't expect them.

nowSolvingConstraints :: MonadTCEnv m => m a -> m a

Start solving constraints

isSolvingConstraints :: MonadTCEnv m => m Bool

catchConstraint :: MonadConstraint m => Constraint -> m () -> m ()

Add constraint if the action raises a pattern violation

isInstanceConstraint :: Constraint -> Bool

canDropRecursiveInstance :: (ReadTCState m, HasOptions m) => m Bool

shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool

wakeConstraints' :: MonadConstraint m => (ProblemConstraint -> WakeUp) -> m ()

Wake constraints matching the given predicate (and aren't instance constraints if shouldPostponeInstanceSearch).

Lenses

mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState

mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState