| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Constraints
Contents
Synopsis
- catchPatternErrTCM :: TCM a -> TCM a -> TCM a
- addConstraintTCM :: Constraint -> TCM ()
- wakeConstraintsTCM :: (ProblemConstraint -> TCM Bool) -> TCM ()
- stealConstraintsTCM :: ProblemId -> TCM ()
- noConstraints :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId 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 -> TCM Bool) -> 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 :: Constraint -> TCM () Source #
wakeConstraintsTCM :: (ProblemConstraint -> TCM Bool) -> 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.
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 #
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 Guarded c cs constraint
to the blocker-generated constraints cs.
wakeConstraints' :: (ProblemConstraint -> TCM Bool) -> 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.
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 #
debugConstraints :: TCM () Source #
Orphan instances
| MonadConstraint TCM Source # | |
Methods addConstraint :: Constraint -> TCM () Source # addAwakeConstraint :: Constraint -> TCM () Source # catchPatternErr :: TCM a -> TCM a -> TCM a Source # solveConstraint :: Constraint -> TCM () Source # solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM () Source # wakeConstraints :: (ProblemConstraint -> TCM Bool) -> TCM () Source # stealConstraints :: ProblemId -> TCM () Source # modifyAwakeConstraints :: (Constraints -> Constraints) -> TCM () Source # modifySleepingConstraints :: (Constraints -> Constraints) -> TCM () Source # | |