{-# LANGUAGE CPP #-} module UHC.Light.Compiler.CHR.Constraint ( Constraint, Constraint' (..) , cnstrReducablePart , CHRIntermediateUntilAssume , mkProve, mkAssume, mkReduction , gathPredLToProveCnstrMp, gathPredLToAssumeCnstrMp , predOccCnstrMpLiftScope , RedHowAnnotation (..) , ByScopeRedHow (..) , UnresolvedTrace' (..), UnresolvedTrace , cnstrMpFromList , ConstraintToInfoTraceMp , cnstrTraceMpSingleton, cnstrTraceMpElimTrace, cnstrTraceMpFromList , ConstraintToInfoMap , emptyCnstrMp , cnstrMpUnion, cnstrMpUnions , mkProveConstraint, mkAssumeConstraint, mkAssumeConstraint' , rhaMbId ) where import UHC.Light.Compiler.Base.Common import UHC.Light.Compiler.Ty import UHC.Util.CHR import UHC.Light.Compiler.CHR.Key import UHC.Util.TreeTrie import UHC.Light.Compiler.Substitutable import UHC.Util.Pretty as PP import UHC.Util.Utils import qualified Data.Set as Set import qualified Data.Map as Map import UHC.Light.Compiler.VarMp import Control.Monad import UHC.Util.Binary import UHC.Util.Serialize import UHC.Light.Compiler.Opts.Base {-# LINE 38 "src/ehc/CHR/Constraint.chs" #-} type instance CHRMatchableKey VarMp = Key {-# LINE 46 "src/ehc/CHR/Constraint.chs" #-} -- | A Constraint is abstracted over the exact predicate, but differentiates on the role: to prove, can be assumed, and side effect of reduction data Constraint' p info = Prove { cnstrPred :: !p } -- proof obligation | Assume { cnstrPred :: !p } -- assumed constraint | Reduction -- 'side effect', residual info used by (e.g.) codegeneration { cnstrPred :: !p -- the pred to which reduction was done , cnstrInfo :: !info -- additional reduction specific info w.r.t. codegeneration , cnstrFromPreds :: ![p] -- the preds from which reduction was done , cnstrVarMp :: VarMp -- additional bindings for type (etc.) variables, i.e. improving substitution } deriving (Eq, Ord, Show) type Constraint = Constraint' CHRPredOcc RedHowAnnotation type instance TTKey (Constraint' p info) = TTKey p {-# LINE 66 "src/ehc/CHR/Constraint.chs" #-} #if __GLASGOW_HASKELL__ >= 708 deriving instance Typeable Constraint' #else deriving instance Typeable2 Constraint' #endif {-# LINE 74 "src/ehc/CHR/Constraint.chs" #-} -- | Dissection of Constraint, including reconstruction function cnstrReducablePart :: Constraint' p info -> Maybe (String,p,p->Constraint' p info) cnstrReducablePart (Prove p) = Just ("Prf",p,Prove) cnstrReducablePart (Assume p) = Just ("Ass",p,Assume) cnstrReducablePart _ = Nothing {-# LINE 82 "src/ehc/CHR/Constraint.chs" #-} instance (CHRMatchable env p s, TTKey p ~ Key) => CHRMatchable env (Constraint' p info) s where chrMatchTo env s c1 c2 = do { (_,p1,_) <- cnstrReducablePart c1 ; (_,p2,_) <- cnstrReducablePart c2 ; chrMatchTo env s p1 p2 } {-# LINE 91 "src/ehc/CHR/Constraint.chs" #-} instance (TTKeyable p, TTKey p ~ Key) => TTKeyable (Constraint' p info) where -- type TTKey (Constraint' p info) = Key toTTKey' o c -- = maybe [] (\(s,p,_) -> ttkAdd (TT1K_One $ Key_Str s) [toTTKey' o p]) $ cnstrReducablePart c = case cnstrReducablePart c of Just (s,p,_) -> ttkAdd' (TT1K_One $ Key_Str s) cs where (_,cs) = toTTKeyParentChildren' o p _ -> panic "TTKeyable (Constraint' p info).toTTKey'" -- ttkEmpty {-# LINE 101 "src/ehc/CHR/Constraint.chs" #-} type instance ExtrValVarKey (Constraint' p info) = ExtrValVarKey p instance (VarExtractable p) => VarExtractable (Constraint' p info) where varFreeSet c = case cnstrReducablePart c of Just (_,p,_) -> varFreeSet p _ -> Set.empty instance (VarUpdatable p s,VarUpdatable info s) => VarUpdatable (Constraint' p info) s where varUpd s (Prove p ) = Prove (varUpd s p) varUpd s (Assume p ) = Assume (varUpd s p) varUpd s r@(Reduction {cnstrPred=p, cnstrInfo=i, cnstrFromPreds=ps}) = r {cnstrPred=varUpd s p, cnstrInfo=varUpd s i, cnstrFromPreds=map (varUpd s) ps} {-# LINE 121 "src/ehc/CHR/Constraint.chs" #-} -- | intermediate structure for holding constraint and related info until it can safely be assumed type CHRIntermediateUntilAssume = (CHRPredOcc,(PredScope,ConstraintToInfoTraceMp)) {-# LINE 126 "src/ehc/CHR/Constraint.chs" #-} mkProve :: CHRPredOcc -> Constraint mkProve = Prove mkAssume :: CHRPredOcc -> Constraint mkAssume = Assume mkReduction :: CHRPredOcc -> RedHowAnnotation -> [CHRPredOcc] -> Constraint mkReduction p i ps = Reduction p i ps varlookupEmpty {-# LINE 159 "src/ehc/CHR/Constraint.chs" #-} mkProveConstraint :: Range -> Pred -> UID -> PredScope -> (Constraint,RedHowAnnotation) mkProveConstraint r pr i sc = (mkProve (mkCHRPredOccRng r pr sc),RedHow_ProveObl i sc) mkAssumeConstraint'' :: Range -> Pred -> VarUIDHsName -> PredScope -> (Constraint,RedHowAnnotation) mkAssumeConstraint'' r pr vun sc = (mkAssume (mkCHRPredOccRng r pr sc),RedHow_Assumption vun sc) mkAssumeConstraint' :: Range -> Pred -> UID -> HsName -> PredScope -> (Constraint,RedHowAnnotation) mkAssumeConstraint' r pr i n sc = mkAssumeConstraint'' r pr (VarUIDHs_Name i n) sc mkAssumeConstraint :: Range -> Pred -> UID -> PredScope -> (Constraint,RedHowAnnotation) mkAssumeConstraint r pr i sc = mkAssumeConstraint'' r pr (VarUIDHs_UID i) sc {-# LINE 177 "src/ehc/CHR/Constraint.chs" #-} gathPredLToProveCnstrMp :: [PredOcc] -> ConstraintToInfoMap gathPredLToProveCnstrMp l = cnstrMpFromList [ rngLift (poRange po) mkProveConstraint (poPr po) (poId po) (poScope po) | po <- l ] gathPredLToAssumeCnstrMp :: [PredOcc] -> ConstraintToInfoMap gathPredLToAssumeCnstrMp l = cnstrMpFromList [ rngLift (poRange po) mkAssumeConstraint (poPr po) (poId po) (poScope po) | po <- l ] {-# LINE 185 "src/ehc/CHR/Constraint.chs" #-} -- | Lift predicate occurrences to new scope, used to lift unproven predicates to an outer scope. predOccCnstrMpLiftScope :: PredScope -> ConstraintToInfoMap -> ConstraintToInfoMap predOccCnstrMpLiftScope sc = Map.mapKeysWith (++) c . Map.map (map i) where c (Prove o@(CHRPredOcc {cpoCxt=cx})) = mkProve (o {cpoCxt = cx {cpocxScope = sc}}) c x = x i (RedHow_ProveObl id _) = RedHow_ProveObl id sc i x = x {-# LINE 202 "src/ehc/CHR/Constraint.chs" #-} data RedHowAnnotation = RedHow_ByInstance !HsName !Pred !PredScope -- inst name, for pred, in scope | RedHow_BySuperClass !HsName !Int !CTag -- field name, offset, tag info of dict | RedHow_ProveObl !UID !PredScope | RedHow_Assumption !VarUIDHsName !PredScope | RedHow_ByScope !ByScopeRedHow -- variant, for distinguishing during debugging | RedHow_ByLabel !Label !LabelOffset !PredScope | RedHow_Lambda !UID !PredScope deriving ( Eq, Ord , Typeable ) {-# LINE 232 "src/ehc/CHR/Constraint.chs" #-} rhaMbId :: RedHowAnnotation -> Maybe UID rhaMbId (RedHow_ProveObl i _) = Just i rhaMbId _ = Nothing {-# LINE 238 "src/ehc/CHR/Constraint.chs" #-} instance Show RedHowAnnotation where show = showPP . pp {-# LINE 243 "src/ehc/CHR/Constraint.chs" #-} instance PP RedHowAnnotation where pp (RedHow_ByInstance s p sc) = "inst" >#< {- ppParens (vm >#< "`varUpd`") >#< -} ppParensCommas [pp p, pp s, pp sc] pp (RedHow_BySuperClass s _ _ ) = "super" >#< s pp (RedHow_ProveObl i sc) = "prove" >#< i >#< sc pp (RedHow_Assumption vun sc) = "assume" >#< ppParensCommas [pp vun, pp sc] pp (RedHow_ByScope v ) = "scope" >|< ppParens v pp (RedHow_ByLabel l o sc) = "label" >#< l >|< "@" >|< o >|< sc pp (RedHow_Lambda i sc) = "lambda" >#< i >#< sc {-# LINE 271 "src/ehc/CHR/Constraint.chs" #-} data ByScopeRedHow = ByScopeRedHow_Prove -- scope reduction based on Prove | ByScopeRedHow_Assume -- scope reduction based on Assume | ByScopeRedHow_Other (AlwaysEq String) -- other reason deriving ( Eq, Ord , Typeable ) -- equality plays no role ?? {- instance Eq ByScopeRedHow where _ == _ = True instance Ord ByScopeRedHow where _ `compare` _ = EQ -} instance Show ByScopeRedHow where show ByScopeRedHow_Prove = "prv" show ByScopeRedHow_Assume = "ass" show (ByScopeRedHow_Other s) = show s instance PP ByScopeRedHow where pp = pp . show {-# LINE 305 "src/ehc/CHR/Constraint.chs" #-} -- | The trace of an unresolved predicate data UnresolvedTrace' p info = UnresolvedTrace_None -- no trace required when all is resolved | UnresolvedTrace_Red -- ok reduction, with failure deeper down { utraceRedFrom :: p , utraceInfoTo2From :: info , utraceRedTo :: [UnresolvedTrace' p info] } | UnresolvedTrace_Fail -- failed reduction { utraceRedFrom :: p -- , utraceInfoTo2From :: info , utraceRedTo :: [UnresolvedTrace' p info] } | UnresolvedTrace_Overlap -- choice could not be made { utraceRedFrom :: p , utraceRedChoices :: [(info,[UnresolvedTrace' p info])] } deriving Show type UnresolvedTrace = UnresolvedTrace' CHRPredOcc RedHowAnnotation instance Eq p => Eq (UnresolvedTrace' p info) where t1 == t2 = True -- utraceRedFrom t1 == utraceRedFrom t2 instance (PP p, PP info) => PP (UnresolvedTrace' p info) where pp x = case x of UnresolvedTrace_None -> PP.empty UnresolvedTrace_Red p i us -> p >|< ":" >#< i >-< indent 2 (vlist $ map pp us) UnresolvedTrace_Fail p us -> p >|< ": FAIL" >-< indent 2 (vlist $ map pp us) UnresolvedTrace_Overlap p uss -> p >|< ": OVERLAP" >-< indent 2 (vlist $ map (\(i,u) -> i >-< indent 2 (vlist $ map pp u)) uss) {-# LINE 342 "src/ehc/CHR/Constraint.chs" #-} -- | Map from constraint to something type ConstraintMp'' p info x = Map.Map (Constraint' p info) [x] type ConstraintMp' x = ConstraintMp'' CHRPredOcc RedHowAnnotation x {-# LINE 348 "src/ehc/CHR/Constraint.chs" #-} cnstrMpSingletonL :: Constraint -> [x] -> ConstraintMp' x cnstrMpSingletonL c xs = Map.singleton c xs cnstrMpSingleton :: Constraint -> x -> ConstraintMp' x cnstrMpSingleton c x = cnstrMpSingletonL c [x] cnstrMpFromList :: [(Constraint,x)] -> ConstraintMp' x cnstrMpFromList l = Map.fromListWith (++) [ (c,[x]) | (c,x) <- l ] cnstrMpMap :: (x -> y) -> ConstraintMp' x -> ConstraintMp' y cnstrMpMap f = Map.map (map f) {-# LINE 362 "src/ehc/CHR/Constraint.chs" #-} -- type ConstraintToInfoTraceMp' p info = ConstraintMp'' p info (info,[UnresolvedTrace' p info]) -- | Map from constraint to info + trace type ConstraintToInfoTraceMp = ConstraintMp' (RedHowAnnotation,[UnresolvedTrace]) {-# LINE 369 "src/ehc/CHR/Constraint.chs" #-} cnstrTraceMpFromList :: [(Constraint,(RedHowAnnotation,[UnresolvedTrace]))] -> ConstraintToInfoTraceMp cnstrTraceMpFromList = cnstrMpFromList cnstrTraceMpSingleton :: Constraint -> RedHowAnnotation -> [UnresolvedTrace] -> ConstraintToInfoTraceMp cnstrTraceMpSingleton c i ts = cnstrMpSingleton c (i,ts) cnstrTraceMpElimTrace :: ConstraintToInfoTraceMp -> ConstraintToInfoMap cnstrTraceMpElimTrace = cnstrMpMap fst cnstrTraceMpLiftTrace :: ConstraintToInfoMap -> ConstraintToInfoTraceMp cnstrTraceMpLiftTrace = cnstrMpMap (\x -> (x,[])) {-# LINE 383 "src/ehc/CHR/Constraint.chs" #-} -- type ConstraintToInfoMap' p info = ConstraintMp'' p info info -- | Map from constraint to info type ConstraintToInfoMap = ConstraintMp' RedHowAnnotation {-# LINE 390 "src/ehc/CHR/Constraint.chs" #-} emptyCnstrMp :: ConstraintMp' x emptyCnstrMp = Map.empty {-# LINE 395 "src/ehc/CHR/Constraint.chs" #-} cnstrMpUnion :: ConstraintMp' x -> ConstraintMp' x -> ConstraintMp' x cnstrMpUnion = Map.unionWith (++) cnstrMpUnions :: [ConstraintMp' x] -> ConstraintMp' x cnstrMpUnions = Map.unionsWith (++) {-# LINE 407 "src/ehc/CHR/Constraint.chs" #-} instance IsConstraint (Constraint' p info) where cnstrRequiresSolve (Reduction {}) = False cnstrRequiresSolve _ = True {-# LINE 417 "src/ehc/CHR/Constraint.chs" #-} instance (PP p, PP info) => PP (Constraint' p info) where pp (Prove p ) = "Prove" >#< p pp (Assume p ) = "Assume" >#< p pp (Reduction {cnstrPred=p, cnstrInfo=i, cnstrFromPreds=ps}) = "Red" >#< p >#< "<" >#< i >#< "<" >#< ppBracketsCommas ps {-# LINE 429 "src/ehc/CHR/Constraint.chs" #-} instance (Serialize p, Serialize i) => Serialize (Constraint' p i) where sput (Prove a ) = sputWord8 0 >> sput a sput (Assume a ) = sputWord8 1 >> sput a sput (Reduction a b c d) = sputWord8 2 >> sput a >> sput b >> sput c >> sput d sget = do t <- sgetWord8 case t of 0 -> liftM Prove sget 1 -> liftM Assume sget 2 -> liftM4 Reduction sget sget sget sget {-# LINE 441 "src/ehc/CHR/Constraint.chs" #-} instance Serialize ByScopeRedHow where sput (ByScopeRedHow_Prove ) = sputWord8 0 sput (ByScopeRedHow_Assume ) = sputWord8 1 sput (ByScopeRedHow_Other a ) = sputWord8 2 >> sput a sget = do t <- sgetWord8 case t of 0 -> return ByScopeRedHow_Prove 1 -> return ByScopeRedHow_Assume 2 -> liftM ByScopeRedHow_Other sget instance Serialize RedHowAnnotation where sput (RedHow_ByInstance a b c ) = sputWord8 0 >> sput a >> sput b >> sput c -- >> sput d sput (RedHow_BySuperClass a b c ) = sputWord8 1 >> sput a >> sput b >> sput c sput (RedHow_ProveObl a b ) = sputWord8 2 >> sput a >> sput b sput (RedHow_Assumption a b ) = sputWord8 3 >> sput a >> sput b sput (RedHow_ByScope a ) = sputWord8 4 >> sput a sput (RedHow_ByLabel a b c ) = sputWord8 5 >> sput a >> sput b >> sput c sput (RedHow_Lambda a b ) = sputWord8 6 >> sput a >> sput b sget = do t <- sgetWord8 case t of 0 -> liftM3 RedHow_ByInstance sget sget sget -- sget 1 -> liftM3 RedHow_BySuperClass sget sget sget 2 -> liftM2 RedHow_ProveObl sget sget 3 -> liftM2 RedHow_Assumption sget sget 4 -> liftM RedHow_ByScope sget 5 -> liftM3 RedHow_ByLabel sget sget sget 6 -> liftM2 RedHow_Lambda sget sget