Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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.

data ConstraintStatus Source #

Instances

Instances details
Show ConstraintStatus Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Constraints

Methods

showsPrec :: Int -> ConstraintStatus -> ShowS

show :: ConstraintStatus -> String

showList :: [ConstraintStatus] -> ShowS

Eq ConstraintStatus Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Constraints

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, MonadBlock m, HasOptions m, MonadDebug m) => MonadConstraint m where Source #

Monad service class containing methods for adding and solving constraints

Methods

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

Unconditionally add the constraint.

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

Add constraint as awake constraint.

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

(PureTCM m, MonadBlock m) => MonadConstraint (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadConstraint m => MonadConstraint (ReaderT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Constraints

Methods

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

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

solveConstraint :: Constraint -> ReaderT e m () Source #

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

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

stealConstraints :: ProblemId -> ReaderT e m () Source #

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

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

addConstraint' :: Blocker -> 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

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

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

Lenses