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

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 ()

addAndUnblocker :: MonadBlock m => Blocker -> m a -> m a

addOrUnblocker :: MonadBlock m => Blocker -> m a -> m a

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

Add new a constraint

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

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

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

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