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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Constraints

Contents

- Lenses

Synopsis

- stealConstraints :: ProblemId -> TCM ()
- solvingProblem :: ProblemId -> TCM a -> TCM a
- solvingProblems :: Set ProblemId -> TCM a -> TCM a
- isProblemSolved :: ProblemId -> TCM Bool
- getConstraintsForProblem :: ProblemId -> TCM Constraints
- getAwakeConstraints :: TCM Constraints
- wakeConstraints :: (ProblemConstraint -> TCM Bool) -> TCM ()
- dropConstraints :: (ProblemConstraint -> Bool) -> TCM ()
- putConstraintsToSleep :: (ProblemConstraint -> Bool) -> TCM ()
- putAllConstraintsToSleep :: TCM ()
- data ConstraintStatus
  - = AwakeConstraint
  - | SleepingConstraint
- holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
- takeAwakeConstraint :: TCM (Maybe ProblemConstraint)
- takeAwakeConstraint' :: (ProblemConstraint -> Bool) -> TCM (Maybe ProblemConstraint)
- getAllConstraints :: TCM Constraints
- withConstraint :: (Constraint -> TCM a) -> ProblemConstraint -> TCM a
- buildProblemConstraint :: Set ProblemId -> Constraint -> TCM ProblemConstraint
- buildProblemConstraint_ :: Constraint -> TCM ProblemConstraint
- buildConstraint :: Constraint -> TCM ProblemConstraint
- addConstraint' :: Constraint -> TCM ()
- addAwakeConstraint' :: Constraint -> TCM ()
- addConstraintTo :: Lens' Constraints TCState -> Constraint -> TCM ()
- addAwakeConstraints :: Constraints -> TCM ()
- nowSolvingConstraints :: TCM a -> TCM a
- isSolvingConstraints :: TCM Bool
- mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState
- mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState
- modifyAwakeConstraints :: (Constraints -> Constraints) -> TCM ()
- modifySleepingConstraints :: (Constraints -> Constraints) -> TCM ()

# Documentation

stealConstraints :: ProblemId -> TCM () Source #

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

solvingProblem :: ProblemId -> TCM a -> TCM a Source #

solvingProblems :: Set ProblemId -> TCM a -> TCM a Source #

isProblemSolved :: ProblemId -> TCM Bool Source #

getConstraintsForProblem :: ProblemId -> TCM Constraints Source #

getAwakeConstraints :: TCM Constraints Source #

Get the awake constraints

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

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

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

putAllConstraintsToSleep :: TCM () Source #

data ConstraintStatus Source #

Constructors

AwakeConstraint |
SleepingConstraint |

Instances

Eq ConstraintStatus Source # |
Instance details Defined in Agda.TypeChecking.Monad.Constraints Methods (==) :: ConstraintStatus -> ConstraintStatus -> Bool Source # (/=) :: ConstraintStatus -> ConstraintStatus -> Bool Source #
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 #

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 :: TCM (Maybe ProblemConstraint) Source #

takeAwakeConstraint' :: (ProblemConstraint -> Bool) -> TCM (Maybe ProblemConstraint) Source #

getAllConstraints :: TCM Constraints Source #

withConstraint :: (Constraint -> TCM a) -> ProblemConstraint -> TCM a Source #

buildProblemConstraint :: Set ProblemId -> Constraint -> TCM ProblemConstraint Source #

buildProblemConstraint_ :: Constraint -> TCM ProblemConstraint Source #

buildConstraint :: Constraint -> TCM ProblemConstraint Source #

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

Add new a constraint

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

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

addAwakeConstraints :: Constraints -> TCM () Source #

Add already awake constraints

nowSolvingConstraints :: TCM a -> TCM a Source #

Start solving constraints

isSolvingConstraints :: TCM Bool Source #

# Lenses

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

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

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

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