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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Monad.Constraints

Contents

- Lenses

Synopsis

- solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a
- solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a
- isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
- getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints
- getAwakeConstraints :: ReadTCState m => m Constraints
- dropConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
- takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints
- putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
- putAllConstraintsToSleep :: MonadConstraint m => m ()
- data ConstraintStatus
  - = AwakeConstraint
  - | SleepingConstraint
- holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
- takeAwakeConstraint :: MonadConstraint m => m (Maybe ProblemConstraint)
- takeAwakeConstraint' :: MonadConstraint m => (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
- getAllConstraints :: ReadTCState m => m Constraints
- withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a
- buildProblemConstraint :: (MonadTCEnv m, ReadTCState m) => Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
- buildProblemConstraint_ :: (MonadTCEnv m, ReadTCState m) => Blocker -> Constraint -> m ProblemConstraint
- buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint
- class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, MonadBlock m, HasOptions m, MonadDebug m) => MonadConstraint m where
  - addConstraint :: Blocker -> Constraint -> m ()
  - addAwakeConstraint :: Blocker -> Constraint -> m ()
  - solveConstraint :: Constraint -> m ()
  - solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m ()
  - wakeConstraints :: (ProblemConstraint -> WakeUp) -> m ()
  - stealConstraints :: ProblemId -> m ()
  - modifyAwakeConstraints :: (Constraints -> Constraints) -> m ()
  - modifySleepingConstraints :: (Constraints -> Constraints) -> m ()
- addAndUnblocker :: MonadBlock m => Blocker -> m a -> m a
- addOrUnblocker :: MonadBlock m => Blocker -> m a -> m a
- addConstraint' :: Blocker -> Constraint -> TCM ()
- addAwakeConstraint' :: Blocker -> Constraint -> TCM ()
- addConstraintTo :: Lens' Constraints TCState -> Blocker -> Constraint -> TCM ()
- nowSolvingConstraints :: MonadTCEnv m => m a -> m a
- isSolvingConstraints :: MonadTCEnv m => m Bool
- catchConstraint :: MonadConstraint m => Constraint -> m () -> m ()
- mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState
- mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState

# Documentation

solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a Source #

solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a Source #

isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool Source #

getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints Source #

getAwakeConstraints :: ReadTCState m => m Constraints Source #

Get the awake constraints

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

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.

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

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

data ConstraintStatus Source #

Constructors

AwakeConstraint |
SleepingConstraint |

#### Instances

Instances details

Show ConstraintStatus Source # |
Instance details Defined in Agda.TypeChecking.Monad.Constraints Methods showsPrec :: Int -> ConstraintStatus -> ShowS Source # show :: ConstraintStatus -> String Source # showList :: [ConstraintStatus] -> ShowS Source #
Eq ConstraintStatus Source # |
Instance details Defined in Agda.TypeChecking.Monad.Constraints Methods (==) :: ConstraintStatus -> ConstraintStatus -> Bool Source # (/=) :: ConstraintStatus -> ConstraintStatus -> Bool Source #

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.

takeAwakeConstraint :: MonadConstraint m => m (Maybe ProblemConstraint) Source #

takeAwakeConstraint' :: MonadConstraint m => (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint) Source #

getAllConstraints :: ReadTCState m => m Constraints Source #

withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a Source #

buildProblemConstraint :: (MonadTCEnv m, ReadTCState m) => Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint Source #

buildProblemConstraint_ :: (MonadTCEnv m, ReadTCState m) => Blocker -> Constraint -> m ProblemConstraint Source #

buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint Source #

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

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 #

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

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

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

solveConstraint :: Constraint -> PureConversionT m () Source #

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

wakeConstraints :: (ProblemConstraint -> WakeUp) -> PureConversionT m () Source #

stealConstraints :: ProblemId -> PureConversionT m () Source #

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

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

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 #

addAndUnblocker :: MonadBlock m => Blocker -> m a -> m a Source #

addOrUnblocker :: MonadBlock m => Blocker -> m a -> m a Source #

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

Add new a constraint

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

addConstraintTo :: Lens' Constraints TCState -> Blocker -> Constraint -> TCM () Source #

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

Start solving constraints

isSolvingConstraints :: MonadTCEnv m => m Bool Source #

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

Add constraint if the action raises a pattern violation

# Lenses

mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState Source #

mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState Source #