Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Constraints

Contents

Synopsis

Documentation

getAwakeConstraints :: ReadTCState m => m Constraints Source #

Get the awake constraints

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

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

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

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.

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

Monad service class containing methods for adding and solving constraints

Methods

addConstraint :: Constraint -> m () Source #

Unconditionally add the constraint.

addAwakeConstraint :: Constraint -> m () Source #

Add constraint as awake constraint.

catchPatternErr :: m a -> m a -> m a Source #

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

solveConstraint :: Constraint -> m () Source #

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

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

wakeConstraints :: (ProblemConstraint -> m Bool) -> m () Source #

stealConstraints :: ProblemId -> m () Source #

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

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

Instances

Instances details
MonadConstraint TCM Source # 
Instance details

Defined in Agda.TypeChecking.Constraints

(MonadTCEnv m, ReadTCState m, HasOptions m, MonadDebug m) => MonadConstraint (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

addConstraint' :: Constraint -> TCM () Source #

Add new a constraint

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

Start solving constraints

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

Add constraint if the action raises a pattern violation

Lenses