module Agda.TypeChecking.Monad.Constraints where
import Control.Monad.State
import Data.Map as Map
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Signature
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Closure
getConstraints :: MonadTCM tcm => tcm Constraints
getConstraints = gets stConstraints
lookupConstraint :: MonadTCM tcm => Int -> tcm ConstraintClosure
lookupConstraint i =
do cs <- getConstraints
unless (i < length cs) $ fail $ "no such constraint: " ++ show i
return $ cs !! i
takeConstraints :: MonadTCM tcm => tcm Constraints
takeConstraints =
do cs <- getConstraints
modify $ \s -> s { stConstraints = [] }
return cs
withConstraint :: MonadTCM tcm => (Constraint -> tcm a) -> ConstraintClosure -> tcm a
withConstraint = flip enterClosure
addConstraints :: MonadTCM tcm => Constraints -> tcm ()
addConstraints cs = modify $ \st -> st { stConstraints = cs ++ stConstraints st }
buildConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
buildConstraint c = do
cl <- buildClosure c
return [cl]