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

-- | Get the constraints
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

-- | Take constraints (clear all constraints).
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

-- | Add new constraints
addConstraints :: MonadTCM tcm => Constraints -> tcm ()
addConstraints cs = modify $ \st -> st { stConstraints = cs ++ stConstraints st }

-- | Create a new constraint.
buildConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
buildConstraint c = do
    cl <- buildClosure c
    return [cl]