{-# 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 Data.Typeable import Data.Generics (Data) import UHC.Light.Compiler.Opts.Base {-# LINE 37 "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 53 "src/ehc/CHR/Constraint.chs" #-} mkReduction :: p -> info -> [p] -> Constraint p info mkReduction p i ps = Reduction p i ps varlookupEmpty {-# LINE 62 "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 71 "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 84 "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 93 "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 102 "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 120 "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 155 "src/ehc/CHR/Constraint.chs" #-} -- | Map from constraint to something type ConstraintMp' p info x = Map.Map (Constraint p info) [x] {-# LINE 160 "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 174 "src/ehc/CHR/Constraint.chs" #-} -- | Map from constraint to info + trace type ConstraintToInfoTraceMp p info = ConstraintMp' p info (info,[UnresolvedTrace p info]) {-# LINE 179 "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 193 "src/ehc/CHR/Constraint.chs" #-} -- | Map from constraint to info type ConstraintToInfoMap p info = ConstraintMp' p info info {-# LINE 198 "src/ehc/CHR/Constraint.chs" #-} emptyCnstrMp :: ConstraintMp' p info x emptyCnstrMp = Map.empty {-# LINE 208 "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 220 "src/ehc/CHR/Constraint.chs" #-} -- | Predicate for whether solving is required cnstrRequiresSolve :: Constraint p info -> Bool cnstrRequiresSolve (Reduction {}) = False cnstrRequiresSolve _ = True {-# LINE 231 "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 243 "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