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

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 :: 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 -> Constraint -> m ProblemConstraint

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

buildConstraint :: Constraint -> TCM ProblemConstraint

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

Monad service class containing methods for adding and solving constraints

Methods

addConstraint :: Constraint -> m ()

Unconditionally add the constraint.

addAwakeConstraint :: Constraint -> m ()

Add constraint as awake constraint.

catchPatternErr :: m a -> m a -> m a

`catchPatternErr handle m` runs m, handling pattern violations with handle (doesn't roll back the state)

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

stealConstraints :: ProblemId -> m ()

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

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

Instances

MonadConstraint TCM

Defined in Agda.TypeChecking.Constraints

Methods

addConstraint :: Constraint -> TCM ()

addAwakeConstraint :: Constraint -> TCM ()

catchPatternErr :: TCM a -> TCM a -> TCM a

solveConstraint :: Constraint -> TCM ()

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

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

stealConstraints :: ProblemId -> TCM ()

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

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

(MonadTCEnv m, ReadTCState m, HasOptions m, MonadDebug m) => MonadConstraint (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addConstraint :: Constraint -> PureConversionT m ()

addAwakeConstraint :: Constraint -> PureConversionT m ()

catchPatternErr :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a

solveConstraint :: Constraint -> PureConversionT m ()

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

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

stealConstraints :: ProblemId -> PureConversionT m ()

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

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

addConstraint' :: Constraint -> TCM ()

Add new a constraint

addAwakeConstraint' :: Constraint -> TCM ()

addConstraintTo :: Lens' Constraints TCState -> 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

Lenses

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

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