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