Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Constraints

Contents

- Orphan instances

Synopsis

- addConstraintTCM :: Blocker -> Constraint -> TCM ()
- wakeConstraintsTCM :: (ProblemConstraint -> WakeUp) -> TCM ()
- stealConstraintsTCM :: ProblemId -> TCM ()
- noConstraints :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m) => m a -> m a
- nonConstraining :: (HasOptions m, MonadConstraint m, MonadDebug m, MonadError TCErr m, MonadFresh ProblemId m, MonadTCEnv m, MonadWarning m) => m a -> m a
- newProblem :: (MonadFresh ProblemId m, MonadConstraint m) => m a -> m (ProblemId, a)
- 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 ()
- whenConstraints :: TCM () -> TCM () -> TCM ()
- wakeConstraints' :: (ProblemConstraint -> WakeUp) -> TCM ()
- wakeupConstraints :: MetaId -> TCM ()
- wakeupConstraints_ :: TCM ()
- solveAwakeConstraints :: MonadConstraint m => m ()
- solveAwakeConstraints' :: MonadConstraint m => Bool -> m ()
- solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
- solveConstraintTCM :: Constraint -> TCM ()
- solveConstraint_ :: Constraint -> TCM ()
- checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
- debugConstraints :: TCM ()

# Documentation

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

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

stealConstraintsTCM :: ProblemId -> TCM () Source #

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 Source #

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 Source #

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) Source #

Create a fresh problem for the given action.

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

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

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

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

`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 () Source #

wakeConstraints' :: (ProblemConstraint -> WakeUp) -> TCM () Source #

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

wakeupConstraints :: MetaId -> TCM () Source #

Wake up the constraints depending on the given meta.

wakeupConstraints_ :: TCM () Source #

Wake up all constraints not blocked on a problem.

solveAwakeConstraints :: MonadConstraint m => m () Source #

solveAwakeConstraints' :: MonadConstraint m => Bool -> m () Source #

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

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

solveConstraintTCM :: Constraint -> TCM () Source #

solveConstraint_ :: Constraint -> TCM () Source #

checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term Source #

debugConstraints :: TCM () Source #

# Orphan instances

MonadConstraint TCM Source # |

Instance details

Methods

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

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

solveConstraint :: Constraint -> TCM () Source #

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

wakeConstraints :: (ProblemConstraint -> WakeUp) -> TCM () Source #

stealConstraints :: ProblemId -> TCM () Source #

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

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