Agda.TypeChecking.Constraints

Documentation

addConstraintTCM :: Blocker -> Constraint -> TCM ()

wakeConstraintsTCM :: (ProblemConstraint -> WakeUp) -> TCM ()

stealConstraintsTCM :: ProblemId -> TCM ()

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

noConstraints :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m) => m a -> m a

Don't allow the argument to produce any blocking constraints.

WARNING: this does not mean that the given computation cannot constrain the solution space further. It can well do so, by solving metas.

nonConstraining :: (HasOptions m, MonadConstraint m, MonadDebug m, MonadError TCErr m, MonadFresh ProblemId m, MonadTCEnv m, MonadWarning m) => m a -> m a

Run a computation that should succeeds without constraining the solution space, i.e., not add any information about meta-variables.

newProblem :: (MonadFresh ProblemId m, MonadConstraint m) => m a -> m (ProblemId, a)

Create a fresh problem for the given action.

newProblem_ :: (MonadFresh ProblemId m, MonadConstraint m) => m a -> m ProblemId

ifNoConstraints :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b

ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a

guardConstraint :: Constraint -> TCM () -> TCM ()

guardConstraint c blocker tries to solve blocker first. If successful without constraints, it moves on to solve c, otherwise it adds a c to the constraint pool, blocked by the problem generated by blocker.

whenConstraints :: TCM () -> TCM () -> TCM ()

wakeupConstraints :: MonadMetaSolver m => MetaId -> m ()

Wake up the constraints depending on the given meta.

wakeupConstraints_ :: TCM ()

Wake up all constraints not blocked on a problem.

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

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

solveConstraintTCM :: Constraint -> TCM ()

solveConstraint_ :: Constraint -> TCM ()

checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term

debugConstraints :: TCM ()

updateBlocker :: PureTCM m => Blocker -> m Blocker

addAndUnblocker :: (PureTCM m, MonadBlock m) => Blocker -> m a -> m a

addOrUnblocker :: (PureTCM m, MonadBlock m) => Blocker -> m a -> m a

withReduced :: (Reduce a, IsMeta a, PureTCM m, MonadBlock m) => a -> (a -> m b) -> m b

Orphan instances

MonadConstraint TCM

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