module UHC.Light.Compiler.CHR.CtxtRedOnly.Solve
( module UHC.Util.CHR.Rule
, module UHC.Util.CHR.Solve.TreeTrie.Mono, IsCHRSolvable (..), SolveState, SolveTrace, SolveStep, CHRStore', CHRSolverConstraint
, CHRStore
, PartialOrdering (..), toOrdering, toPartialOrdering
, isLetProveCandidate, isLetProveFailure )
where
import qualified Data.Set as Set
import UHC.Util.Utils
import UHC.Util.CHR
import UHC.Util.CHR.Rule
import UHC.Util.Substitutable
import UHC.Light.Compiler.CHR.CtxtRedOnly.Instances
import UHC.Light.Compiler.CHR.CtxtRedOnly.Key
import UHC.Light.Compiler.VarMp
import UHC.Light.Compiler.Ty
import UHC.Light.Compiler.Ty.FitsInCommon2
import UHC.Util.CHR.Solve.TreeTrie.Mono hiding (IsCHRSolvable (..),SolveState,SolveTrace,SolveStep,CHRStore)
import qualified UHC.Util.CHR.Solve.TreeTrie.Mono as Mono

{-# LINE 24 "src/ehc/CHR/CtxtRedOnly/Solve.chs" #-}
instance Mono.IsCHRSolvable FIIn Constraint Guard VarMp

type CHRSolverConstraint = Constraint

-- | (Class alias) API for solving requirements, hiding Mono/Poly differences
class ( Mono.IsCHRSolvable env c g s
      ) => IsCHRSolvable env c g p s

instance IsCHRSolvable FIIn Constraint Guard Prio VarMp

type CHRStore'  e c g p s = Mono.CHRStore   c g
type SolveState e c g p s = Mono.SolveState c g s
type SolveTrace e c g p s = Mono.SolveTrace c g s
type SolveStep  e c g p s = Mono.SolveStep  c g s

{-# LINE 91 "src/ehc/CHR/CtxtRedOnly/Solve.chs" #-}
-- dummy (for now)
-- type Prio = ()
-- type CHRPrio = Prio

type CHRStore = CHRStore' FIIn Constraint Guard Prio VarMp

{-# LINE 105 "src/ehc/CHR/CtxtRedOnly/Solve.chs" #-}
data PartialOrdering
  = P_LT | P_EQ | P_GT | P_NE
  deriving (Eq,Show)

toPartialOrdering :: Ordering -> PartialOrdering
toPartialOrdering o
  = case o of
      EQ -> P_EQ
      LT -> P_LT
      GT -> P_GT

toOrdering :: PartialOrdering -> Maybe Ordering
toOrdering o
  = case o of
      P_EQ -> Just EQ
      P_LT -> Just LT
      P_GT -> Just GT
      _    -> Nothing

{-# LINE 130 "src/ehc/CHR/CtxtRedOnly/Solve.chs" #-}
-- | Consider a pred for proving if: no free tvars, or its free tvars do not coincide with those globally used
isLetProveCandidate :: (VarExtractable x) => Set.Set (ExtrValVarKey x) -> x -> Bool
isLetProveCandidate glob x
  = Set.null fv || Set.null (fv `Set.intersection` glob)
  where fv = varFreeSet x

isLetProveFailure :: (VarExtractable x) => Set.Set (ExtrValVarKey x) -> x -> Bool
isLetProveFailure glob x
  = Set.null fv
  where fv = varFreeSet x