uhc-light-1.1.9.2: src/UHC/Light/Compiler/CHR/Constraint.hs
{-# 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