content: {-# LANGUAGE MonadComprehensions #-}
  
  module Language.Haskell.Exference.Core.Internal.ConstraintSolver
    ( isPossible
    , filterUnresolved
    )
  where
  
  
  
  import Language.Haskell.Exference.Core.Types
  import Language.Haskell.Exference.Core.TypeUtils
  import Language.Haskell.Exference.Core.Internal.Unify
  
  import qualified Data.Set as S
  import Control.Monad ( mplus, guard, join )
  import Control.Applicative ( (<|>), (<$>), liftA2 )
  import Data.Foldable ( asum )
  import Data.Maybe ( fromMaybe )
  import Data.Traversable ( traverse )
  
  import qualified Data.Map.Strict as M
  import qualified Data.IntMap.Strict as IntMap
  
  import Debug.Trace
  
  
  
  -- returns Nothing if one of the constraints is refutable
  -- otherwise Just a list of open constraints (that could neither be
  -- solved nor refuted).
  isPossible :: QueryClassEnv -> [HsConstraint] -> Maybe [HsConstraint]
  isPossible = checkPossibleGeneric (Just . return) (const Nothing)
  
  -- returns Nothing if any of the constraints contains variables
  -- (as variables cannot be proven).
  -- Otherwise returns the list of constraints that cannot be proven,
  -- and removing all those that can be proven.
  filterUnresolved :: QueryClassEnv -> [HsConstraint] -> Maybe [HsConstraint]
  filterUnresolved = checkPossibleGeneric (const Nothing) (Just . return)
  
  checkPossibleGeneric :: (HsConstraint -> Maybe [HsConstraint])
                       -> (HsConstraint -> Maybe [HsConstraint])
                       -> QueryClassEnv
                       -> [HsConstraint]
                       -> Maybe [HsConstraint]
  checkPossibleGeneric containsVarsResult otherwiseResult qClassEnv = fmap concat . traverse g where
    g c = if constraintContainsVariables c
      then containsVarsResult c
      else possibleFromGiven c <|> possibleFromInstance c <|> otherwiseResult c
    possibleFromGiven :: HsConstraint -> Maybe [HsConstraint]
    possibleFromGiven c = [ [] | S.member c $ qClassEnv_inflatedConstraints qClassEnv ]
    possibleFromInstance :: HsConstraint -> Maybe [HsConstraint]
    possibleFromInstance c = asum $ f <$> is where
      (HsConstraint cclass cparams) = c
      is = M.findWithDefault []
                             (tclass_name cclass)
                             ( sClassEnv_instances
                               $ qClassEnv_env qClassEnv )
      f (HsInstance instConstrs _iclass instParams) = do
        substs <- unifyRightEqs $ zipWith TypeEq cparams instParams
        checkPossibleGeneric containsVarsResult otherwiseResult
          qClassEnv
          (map (snd . constraintApplySubsts substs) instConstrs)
  