Agda.TypeChecking.Monad.Constraints

Documentation

stealConstraints :: ProblemId -> TCM ()

Add all constraints belonging to the given problem to the current problem(s).

solvingProblem :: ProblemId -> TCM a -> TCM a

solvingProblems :: Set ProblemId -> TCM a -> TCM a

isProblemSolved :: ProblemId -> TCM Bool

getConstraintsForProblem :: ProblemId -> TCM Constraints

getAwakeConstraints :: TCM Constraints

Get the awake constraints

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

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

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

putAllConstraintsToSleep :: TCM ()

data ConstraintStatus

Constructors

AwakeConstraint

SleepingConstraint

Instances

Eq ConstraintStatus

Defined in Agda.TypeChecking.Monad.Constraints

Methods

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

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

Show ConstraintStatus

Defined in Agda.TypeChecking.Monad.Constraints

Methods

showsPrec :: Int -> ConstraintStatus -> ShowS

show :: ConstraintStatus -> String

showList :: [ConstraintStatus] -> ShowS

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 :: TCM (Maybe ProblemConstraint)

takeAwakeConstraint' :: (ProblemConstraint -> Bool) -> TCM (Maybe ProblemConstraint)

getAllConstraints :: TCM Constraints

withConstraint :: (Constraint -> TCM a) -> ProblemConstraint -> TCM a

buildProblemConstraint :: Set ProblemId -> Constraint -> TCM ProblemConstraint

buildProblemConstraint_ :: Constraint -> TCM ProblemConstraint

buildConstraint :: Constraint -> TCM ProblemConstraint

addConstraint' :: Constraint -> TCM ()

Add new a constraint

addAwakeConstraint' :: Constraint -> TCM ()

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

addAwakeConstraints :: Constraints -> TCM ()

Add already awake constraints

nowSolvingConstraints :: TCM a -> TCM a

Start solving constraints

isSolvingConstraints :: TCM Bool

Lenses

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

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

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

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