module UHC.Light.Compiler.Pred.CHR
( module UHC.Light.Compiler.Pred.CommonCHR
, Guard (..)
, PartialOrdering (..), toOrdering, toPartialOrdering
, isLetProveCandidate, isLetProveFailure )
where
import UHC.Light.Compiler.CHR
import UHC.Light.Compiler.CHR.Constraint
import UHC.Light.Compiler.Pred.CommonCHR
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import UHC.Util.Pretty
import UHC.Util.AGraph
import UHC.Light.Compiler.Base.Common
import UHC.Light.Compiler.Base.TermLike
import UHC.Light.Compiler.Ty
import UHC.Light.Compiler.VarMp
import UHC.Light.Compiler.Substitutable
import UHC.Light.Compiler.Ty.FitsInCommon2
import UHC.Light.Compiler.Ty.FitsIn
import UHC.Light.Compiler.Ty.TreeTrieKey
import UHC.Light.Compiler.Base.HsName.Builtin
import Control.Monad
import UHC.Util.Binary
import UHC.Util.Serialize




{-# LINE 42 "src/ehc/Pred/CHR.chs" #-}
data Guard
  = HasStrictCommonScope    PredScope PredScope PredScope                   -- have strict/proper common scope?
  | IsVisibleInScope        PredScope PredScope                             -- is visible in 2nd scope?
  | NotEqualScope           PredScope PredScope                             -- scopes are unequal
  | EqualScope              PredScope PredScope                             -- scopes are equal
  | IsStrictParentScope     PredScope PredScope PredScope                   -- parent scope of each other?
  | NonEmptyRowLacksLabel   Ty LabelOffset Ty Label                         -- non empty row does not have label?, yielding its position + rest
  deriving (Typeable, Data)

{-# LINE 63 "src/ehc/Pred/CHR.chs" #-}
ppGuard :: Guard -> PP_Doc
ppGuard (HasStrictCommonScope   sc1 sc2 sc3) = ppParensCommas' [sc1 >#< "<" >#< sc2,sc1 >#< "<=" >#< sc3]
ppGuard (IsStrictParentScope    sc1 sc2 sc3) = ppParens (sc1 >#< "==" >#< sc2 >#< "/\\" >#< sc2 >#< "/=" >#< sc3)
ppGuard (IsVisibleInScope       sc1 sc2    ) = sc1 >#< "`visibleIn`" >#< sc2
ppGuard (NotEqualScope          sc1 sc2    ) = sc1 >#< "/=" >#< sc2
ppGuard (EqualScope             sc1 sc2    ) = sc1 >#< "==" >#< sc2
ppGuard (NonEmptyRowLacksLabel  r o t l    ) = ppParens (t >#< "==" >#< ppParens (r >#< "| ...")) >#< "\\" >#< l >|< "@" >|< o

{-# LINE 82 "src/ehc/Pred/CHR.chs" #-}
instance Show Guard where
  show _ = "CHR Guard"

instance PP Guard where
  pp = ppGuard

{-# LINE 94 "src/ehc/Pred/CHR.chs" #-}
instance VarExtractable CHRPredOccCnstrMp TyVarId where
  varFreeSet        x = Set.unions [ varFreeSet k | k <- Map.keys x ]

instance VarUpdatable CHRPredOccCnstrMp VarMp where
  varUpd s x = Map.mapKeysWith (++) (varUpd s) x

instance VarExtractable Guard TyVarId where
  varFreeSet        (HasStrictCommonScope   p1 p2 p3) = Set.unions $ map varFreeSet [p1,p2,p3]
  varFreeSet        (IsStrictParentScope    p1 p2 p3) = Set.unions $ map varFreeSet [p1,p2,p3]
  varFreeSet        (IsVisibleInScope       p1 p2   ) = Set.unions $ map varFreeSet [p1,p2]
  varFreeSet        (NotEqualScope          p1 p2   ) = Set.unions $ map varFreeSet [p1,p2]
  varFreeSet        (EqualScope             p1 p2   ) = Set.unions $ map varFreeSet [p1,p2]
  varFreeSet        (NonEmptyRowLacksLabel  r o t l ) = Set.unions [varFreeSet r,varFreeSet o,varFreeSet t,varFreeSet l]

instance VarUpdatable Guard VarMp where
  varUpd s (HasStrictCommonScope   p1 p2 p3) = HasStrictCommonScope   (s `varUpd` p1) (s `varUpd` p2) (s `varUpd` p3)
  varUpd s (IsStrictParentScope    p1 p2 p3) = IsStrictParentScope    (s `varUpd` p1) (s `varUpd` p2) (s `varUpd` p3)
  varUpd s (IsVisibleInScope       p1 p2   ) = IsVisibleInScope       (s `varUpd` p1) (s `varUpd` p2)
  varUpd s (NotEqualScope          p1 p2   ) = NotEqualScope          (s `varUpd` p1) (s `varUpd` p2)
  varUpd s (EqualScope             p1 p2   ) = EqualScope             (s `varUpd` p1) (s `varUpd` p2)
  varUpd s (NonEmptyRowLacksLabel  r o t l ) = NonEmptyRowLacksLabel  (s `varUpd` r)  (s `varUpd` o)  (s `varUpd` t)  (s `varUpd` l)

{-# LINE 133 "src/ehc/Pred/CHR.chs" #-}
instance VarExtractable VarUIDHsName TyVarId where
  varFreeSet          (VarUIDHs_Var i)  = Set.singleton i
  varFreeSet          _                 = Set.empty

-- instance VarUpdatable VarUIDHsName VarMp where
instance VarLookup m ImplsVarId VarMpInfo => VarUpdatable VarUIDHsName m where
  varUpd s a                   = maybe a id $ varmpAssNmLookupAssNmCyc a s

{-# LINE 143 "src/ehc/Pred/CHR.chs" #-}
instance VarExtractable RedHowAnnotation TyVarId where
  varFreeSet        (RedHow_Assumption   vun sc)  = Set.unions [varFreeSet vun,varFreeSet sc]
  varFreeSet        (RedHow_ByLabel      l o sc)  = Set.unions [varFreeSet l,varFreeSet o,varFreeSet sc]
  varFreeSet        _                             = Set.empty

instance VarUpdatable RedHowAnnotation VarMp where
  varUpd s (RedHow_Assumption   vun sc)  = RedHow_Assumption (varUpd s vun) (varUpd s sc)
  varUpd s (RedHow_ByLabel      l o sc)  = RedHow_ByLabel (varUpd s l) (varUpd s o) (varUpd s sc)
  varUpd _ x                             = x

{-# LINE 166 "src/ehc/Pred/CHR.chs" #-}
instance CHREmptySubstitution VarMp where
  chrEmptySubst = emptyVarMp


{-# LINE 176 "src/ehc/Pred/CHR.chs" #-}
instance CHRCheckable FIIn Guard VarMp where
  chrCheck env subst x
    = chk x
    where subst' = subst |+> fiVarMp env
          chk (HasStrictCommonScope (PredScope_Var vDst) sc1 sc2)
            = do { let sc1' = varUpd subst' sc1
                       sc2' = varUpd subst' sc2
                 ; scDst <- pscpCommon sc1' sc2'
                 ; if scDst == sc1'
                   then Nothing
                   else return $ vDst `varmpScopeUnit` scDst
                 }
          chk (IsStrictParentScope (PredScope_Var vDst) sc1 sc2)
            = do { let sc1' = varUpd subst' sc1
                       sc2' = varUpd subst' sc2
                 ; scDst <- pscpCommon sc1' sc2'
                 ; if scDst == sc1' && sc1' /= sc2'
                   then return $ vDst `varmpScopeUnit` scDst
                   else Nothing
                 }
          chk (NotEqualScope sc1 sc2) | isJust c
            = if fromJust c /= EQ then return emptyVarMp else Nothing
            where c = pscpCmp (varUpd subst' sc1) (varUpd subst' sc2)
          chk (EqualScope sc1 sc2) | isJust c
            = if fromJust c == EQ then return emptyVarMp else Nothing
            where c = pscpCmp (varUpd subst' sc1) (varUpd subst' sc2)
          chk (IsVisibleInScope scDst@(PredScope_Var vDst) sc1) | isJust mbSc
            = chk (IsVisibleInScope (fromJust mbSc) sc1)
            where mbSc = varmpScopeLookupScopeCyc scDst subst'
          chk (IsVisibleInScope (PredScope_Var vDst) sc1)
            = return $ vDst `varmpScopeUnit` sc1
          chk (IsVisibleInScope scDst sc1) | pscpIsVisibleIn (varUpd subst' scDst) (varUpd subst' sc1)
            = return emptyVarMp
          chk (NonEmptyRowLacksLabel r1@(Ty_Var tv _) (LabelOffset_Var vDst) ty lab)
            |  fiAllowTyVarBind env r1
            && not (null exts) && presence == Absent -- tyIsEmptyRow row
            = return $ (vDst `varmpOffsetUnit` LabelOffset_Off offset)
                       `varUpd` (tv `varmpTyUnit` row)
            where (row,exts) = tyRowExtsWithLkup (varmpTyLookupCyc2 subst') ty
                  ((offset,presence),_) = tyExtsOffset lab' $ rowCanonOrder exts
                  (Label_Lab lab') = varUpd subst' lab
          chk _
            = Nothing

{-# LINE 286 "src/ehc/Pred/CHR.chs" #-}
instance CHRMatchable FIIn Pred VarMp where
  chrMatchTo fi subst pr1 pr2
    = do { (_,subst') <- fitPredIntoPred (fi {fiVarMp = subst |+> fiVarMp fi}) pr1 pr2
         ; return subst'
         }

{-# LINE 294 "src/ehc/Pred/CHR.chs" #-}
instance CHRMatchable FIIn CHRPredOccCxt VarMp where
  chrMatchTo e subst (CHRPredOccCxt_Scope1 sc1) (CHRPredOccCxt_Scope1 sc2) = chrMatchTo e subst sc1 sc2

instance CHRMatchable FIIn PredScope VarMp where
  chrMatchTo _ subst (PredScope_Var v1) sc2@(PredScope_Var v2) | v1 == v2    = Just emptyVarMp
  chrMatchTo e subst (PredScope_Var v1) sc2                    | isJust mbSc = chrMatchTo e subst (fromJust mbSc) sc2
                                                                             where mbSc = varmpScopeLookup v1 subst
  chrMatchTo e subst sc1                    (PredScope_Var v2) | isJust mbSc = chrMatchTo e subst sc1 (fromJust mbSc)
                                                                             where mbSc = varmpScopeLookup v2 subst
  chrMatchTo _ subst _                      (PredScope_Var v2)               = Nothing
  chrMatchTo _ subst (PredScope_Var v1) sc2                                  = Just $ v1 `varmpScopeUnit` sc2
  chrMatchTo _ subst (PredScope_Lev l1)     (PredScope_Lev l2) | l1 == l2    = Just emptyVarMp
  chrMatchTo _ subst _                  _                                    = Nothing

{-# LINE 310 "src/ehc/Pred/CHR.chs" #-}
instance CHRMatchable FIIn CHRPredOcc VarMp where
  chrMatchTo fi subst po1 po2
    = do { subst1 <- chrMatchTo fi subst (cpoPr po1) (cpoPr po2)
         ; subst2 <- chrMatchTo fi subst (cpoCxt po1) (cpoCxt po2)
         ; return $ subst2 |+> subst1
         }

{-# LINE 319 "src/ehc/Pred/CHR.chs" #-}
instance CHRMatchable FIIn Label VarMp where
  chrMatchTo _ subst (Label_Var v1) lb2@(Label_Var v2) | v1 == v2    = Just emptyVarMp
  chrMatchTo e subst (Label_Var v1) lb2                | isJust mbLb = chrMatchTo e subst (fromJust mbLb) lb2
                                                                     where mbLb = varmpLabelLookup v1 subst
  chrMatchTo e subst lb1                (Label_Var v2) | isJust mbLb = chrMatchTo e subst lb1 (fromJust mbLb)
                                                                     where mbLb = varmpLabelLookup v2 subst
  chrMatchTo _ subst _                  (Label_Var v2)               = Nothing
  chrMatchTo _ subst (Label_Var v1) lb2                              = Just $ v1 `varmpLabelUnit` lb2
  chrMatchTo _ subst (Label_Lab l1)     (Label_Lab l2) | l1 == l2    = Just emptyVarMp
  chrMatchTo _ subst _              _                                = Nothing

{-# LINE 332 "src/ehc/Pred/CHR.chs" #-}
instance CHRMatchable FIIn LabelOffset VarMp where
  chrMatchTo _ subst (LabelOffset_Var v1) of2@(LabelOffset_Var v2) | v1 == v2    = Just emptyVarMp
  chrMatchTo s subst (LabelOffset_Var v1) of2                      | isJust mbOf = chrMatchTo s subst (fromJust mbOf) of2
                                                                                 where mbOf = varmpOffsetLookup v1 subst
  chrMatchTo s subst of1                      (LabelOffset_Var v2) | isJust mbOf = chrMatchTo s subst of1 (fromJust mbOf)
                                                                                 where mbOf = varmpOffsetLookup v2 subst
  chrMatchTo _ subst _                        (LabelOffset_Var v2)               = Nothing
  chrMatchTo _ subst (LabelOffset_Var v1) of2                                    = Just $ v1 `varmpOffsetUnit` of2
  chrMatchTo _ subst (LabelOffset_Off l1)     (LabelOffset_Off l2) | l1 == l2    = Just emptyVarMp
  chrMatchTo _ subst _                    _                                      = Nothing

{-# LINE 351 "src/ehc/Pred/CHR.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 376 "src/ehc/Pred/CHR.chs" #-}
-- | Consider a pred for proving if: no free tvars, or its free tvars do not coincide with those globally used
isLetProveCandidate :: (VarExtractable x v) => Set.Set v -> x -> Bool
isLetProveCandidate glob x
  = Set.null fv || Set.null (fv `Set.intersection` glob)
  where fv = varFreeSet x

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

{-# LINE 393 "src/ehc/Pred/CHR.chs" #-}
instance Serialize Guard where
  sput (HasStrictCommonScope     a b c  ) = sputWord8 0  >> sput a >> sput b >> sput c
  sput (IsVisibleInScope         a b    ) = sputWord8 1  >> sput a >> sput b
  sput (NotEqualScope            a b    ) = sputWord8 2  >> sput a >> sput b
  sput (EqualScope               a b    ) = sputWord8 3  >> sput a >> sput b
  sput (IsStrictParentScope      a b c  ) = sputWord8 4  >> sput a >> sput b >> sput c
  sput (NonEmptyRowLacksLabel    a b c d) = sputWord8 5  >> sput a >> sput b >> sput c >> sput d
  sget = do t <- sgetWord8
            case t of
              0  -> liftM3 HasStrictCommonScope     sget sget sget
              1  -> liftM2 IsVisibleInScope         sget sget
              2  -> liftM2 NotEqualScope            sget sget
              3  -> liftM2 EqualScope               sget sget
              4  -> liftM3 IsStrictParentScope      sget sget sget
              5  -> liftM4 NonEmptyRowLacksLabel    sget sget sget sget