    {-# LANGUAGE CPP #-}
    module Agda.TypeChecking.Constraints where

    import System.IO

    import Control.Monad.State
    import Control.Monad.Reader
    import Control.Monad.Error
    import Control.Applicative
    import Data.Map as Map
    import Data.List as List
    import Data.Set as Set

    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce

    import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (checkExpr)
    import {-# SOURCE #-} Agda.TypeChecking.Conversion
    import {-# SOURCE #-} Agda.TypeChecking.MetaVars
    import {-# SOURCE #-} Agda.TypeChecking.Empty
    import Agda.TypeChecking.Free

    import Agda.Utils.Fresh

    #include "../undefined.h"
    import Agda.Utils.Impossible

    -- | Catch pattern violation errors and adds a constraint.
    --
    catchConstraint :: MonadTCM tcm => Constraint -> TCM Constraints -> tcm Constraints
    catchConstraint c v = liftTCM $
       catchError v $ \err ->
       case errError err of
           PatternErr s -> put s >> buildConstraint c
           _	    -> throwError err

    -- | Try to solve the constraints to be added.
    addNewConstraints :: MonadTCM tcm => Constraints -> tcm ()
    addNewConstraints cs = do addConstraints cs; wakeupConstraints

    -- | Don't allow the argument to produce any constraints.
    noConstraints :: MonadTCM tcm => tcm Constraints -> tcm ()
    noConstraints m = do
        cs <- solveConstraints =<< m
        unless (List.null cs) $ typeError $ UnsolvedConstraints cs
        return ()

    -- | Guard constraint
    guardConstraint :: MonadTCM tcm => tcm Constraints -> Constraint -> tcm Constraints
    guardConstraint m c = do
        cs <- solveConstraints =<< m
        case List.partition isNonBlocking cs of
    	(scs, []) -> (scs ++) <$> solveConstraint c
    	(scs, cs) -> (scs ++) <$> buildConstraint (Guarded c cs)
        where
    	isNonBlocking = isNB . clValue
    	isNB SortCmp{}        = True
    	isNB ValueCmp{}       = False
    	isNB TypeCmp{}        = False
    	isNB TelCmp{}         = False
    	isNB (Guarded c _)    = isNB c
    	isNB UnBlock{}        = False
            isNB IsEmpty{}        = False

    -- | We ignore the constraint ids and (as in Agda) retry all constraints every time.
    --   We probably generate very few constraints.
    wakeupConstraints :: MonadTCM tcm => tcm ()
    wakeupConstraints = do
        cs <- takeConstraints
        cs <- solveConstraints cs
        addConstraints cs

    solveConstraints :: MonadTCM tcm => Constraints -> tcm Constraints
    solveConstraints [] = return []
    solveConstraints cs = do
        reportSDoc "tc.constr.solve" 60 $
          sep [ text "{ solving", nest 2 $ prettyTCM cs ]
        n  <- length <$> getInstantiatedMetas
        cs0 <- return cs
        cs <- concat <$> mapM (withConstraint solveConstraint) cs
        n' <- length <$> getInstantiatedMetas
        reportSDoc "tc.constr.solve" 70 $
          sep [ text "new constraints", nest 2 $ prettyTCM cs ]
        cs <- if (n' > n)
    	then solveConstraints cs -- Go again if we made progress
    	else return cs
        reportSLn "tc.constr.solve" 60 $ "solved constraints }"
        return cs

    solveConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
    solveConstraint (ValueCmp cmp a u v) = compareTerm cmp a u v
    solveConstraint (TypeCmp cmp a b)    = compareType cmp a b
    solveConstraint (TelCmp cmp a b)     = compareTel  cmp a b
    solveConstraint (SortCmp cmp s1 s2)  = compareSort cmp s1 s2
    solveConstraint (Guarded c cs)       = guardConstraint (return cs) c
    solveConstraint (IsEmpty t)          = isEmptyTypeC t
    solveConstraint (UnBlock m)          = do
        inst <- mvInstantiation <$> lookupMeta m
        reportSDoc "tc.constr.unblock" 15 $ text ("unblocking a metavar yields the constraint: " ++ show inst)
        case inst of
          BlockedConst t -> do
            reportSDoc "tc.constr.blocked" 15 $
              text ("blocked const " ++ show m ++ " :=") <+> prettyTCM t
            assignTerm m t
            return []
          PostponedTypeCheckingProblem cl -> enterClosure cl $ \(e, t, unblock) -> do
            b <- liftTCM unblock
            if not b
              then buildConstraint $ UnBlock m
              else do
                tel <- getContextTelescope
                v   <- liftTCM $ checkExpr e t
                assignTerm m $ teleLam tel v
                return []
          -- Andreas, 2009-02-09, the following were IMPOSSIBLE cases
          -- somehow they pop up in the context of sized types
          --
          -- already solved metavariables: no constraints left (Ulf, is that correct?)
          InstV{} -> return []
          InstS{} -> return []
          -- Open (whatever that means)
          Open -> __IMPOSSIBLE__