{-# LANGUAGE CPP #-} module UHC.Light.Compiler.CHR.Constraint ( Constraint (..) , mkReduction , cnstrReducablePart , UnresolvedTrace (..) , cnstrMpSingletonL, cnstrMpFromList , ConstraintToInfoTraceMp , cnstrTraceMpSingleton, cnstrTraceMpLiftTrace, cnstrTraceMpElimTrace, cnstrTraceMpFromList , ConstraintToInfoMap , emptyCnstrMp , cnstrMpUnion, cnstrMpUnions , cnstrRequiresSolve ) where import UHC.Light.Compiler.Base.Common import UHC.Light.Compiler.Ty import UHC.Light.Compiler.CHR import UHC.Light.Compiler.CHR.Key import UHC.Light.Compiler.Base.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 35 "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) {-# LINE 51 "src/ehc/CHR/Constraint.chs" #-} mkReduction :: p -> info -> [p] -> Constraint p info mkReduction p i ps = Reduction p i ps varlookupEmpty {-# LINE 60 "src/ehc/CHR/Constraint.chs" #-} #if __GLASGOW_HASKELL__ >= 708 deriving instance Typeable Constraint #else deriving instance Typeable2 Constraint #endif deriving instance (Data x, Data y) => Data (Constraint x y) {-# LINE 69 "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) => 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 => TTKeyable (Constraint p info) where 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 100 "src/ehc/CHR/Constraint.chs" #-} instance (VarExtractable p v,VarExtractable info v) => VarExtractable (Constraint p info) v 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 118 "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 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 153 "src/ehc/CHR/Constraint.chs" #-} -- | Map from constraint to something type ConstraintMp' p info x = Map.Map (Constraint p info) [x] {-# LINE 158 "src/ehc/CHR/Constraint.chs" #-} cnstrMpSingletonL :: Constraint p i -> [x] -> ConstraintMp' p i x cnstrMpSingletonL c xs = Map.singleton c xs cnstrMpSingleton :: Constraint p i -> x -> ConstraintMp' p i x cnstrMpSingleton c x = cnstrMpSingletonL c [x] cnstrMpFromList :: (Ord p, Ord i) => [(Constraint p i,x)] -> ConstraintMp' p i x cnstrMpFromList l = Map.fromListWith (++) [ (c,[x]) | (c,x) <- l ] cnstrMpMap :: (Ord p, Ord i) => (x -> y) -> ConstraintMp' p i x -> ConstraintMp' p i y cnstrMpMap f = Map.map (map f) {-# LINE 172 "src/ehc/CHR/Constraint.chs" #-} -- | Map from constraint to info + trace type ConstraintToInfoTraceMp p info = ConstraintMp' p info (info,[UnresolvedTrace p info]) {-# LINE 177 "src/ehc/CHR/Constraint.chs" #-} cnstrTraceMpFromList :: (Ord p, Ord i) => [(Constraint p i,(i,[UnresolvedTrace p i]))] -> ConstraintToInfoTraceMp p i cnstrTraceMpFromList = cnstrMpFromList cnstrTraceMpSingleton :: Constraint p i -> i -> [UnresolvedTrace p i] -> ConstraintToInfoTraceMp p i cnstrTraceMpSingleton c i ts = cnstrMpSingleton c (i,ts) cnstrTraceMpElimTrace :: (Ord p, Ord i) => ConstraintToInfoTraceMp p i -> ConstraintToInfoMap p i cnstrTraceMpElimTrace = cnstrMpMap fst cnstrTraceMpLiftTrace :: (Ord p, Ord i) => ConstraintToInfoMap p i -> ConstraintToInfoTraceMp p i cnstrTraceMpLiftTrace = cnstrMpMap (\x -> (x,[])) {-# LINE 191 "src/ehc/CHR/Constraint.chs" #-} -- | Map from constraint to info type ConstraintToInfoMap p info = ConstraintMp' p info info {-# LINE 196 "src/ehc/CHR/Constraint.chs" #-} emptyCnstrMp :: ConstraintMp' p info x emptyCnstrMp = Map.empty {-# LINE 206 "src/ehc/CHR/Constraint.chs" #-} cnstrMpUnion :: (Ord p, Ord i) => ConstraintMp' p i x -> ConstraintMp' p i x -> ConstraintMp' p i x cnstrMpUnion = Map.unionWith (++) cnstrMpUnions :: (Ord p, Ord i) => [ConstraintMp' p i x] -> ConstraintMp' p i x cnstrMpUnions = Map.unionsWith (++) {-# LINE 218 "src/ehc/CHR/Constraint.chs" #-} -- | Predicate for whether solving is required cnstrRequiresSolve :: Constraint p info -> Bool cnstrRequiresSolve (Reduction {}) = False cnstrRequiresSolve _ = True {-# LINE 229 "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 241 "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