diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,8 +1,12 @@ # Changelog -## 0.1.5.6 +## 0.1.6.3 -- [??] +- [api] move of RLList, TreeTrie, CHR, Substitutable (partial) from uhc to uhc-util + +## 0.1.6.2 + +- [uhc] as released with uhc 1.1.9.1 ## 0.1.5.5 diff --git a/src/UHC/Util/AssocL.hs b/src/UHC/Util/AssocL.hs --- a/src/UHC/Util/AssocL.hs +++ b/src/UHC/Util/AssocL.hs @@ -1,17 +1,26 @@ module UHC.Util.AssocL - ( Assoc, AssocL + ( -- * Assoc list + Assoc, AssocL , assocLMapElt, assocLMapKey , assocLElts, assocLKeys , assocLGroupSort , assocLMapUnzip , ppAssocL, ppAssocL', ppAssocLV , ppCurlysAssocL + + -- * Utils + , combineToDistinguishedElts ) where import UHC.Util.Pretty import UHC.Util.Utils import Data.List +import Data.Maybe +------------------------------------------------------------------------------------------- +--- AssocL +------------------------------------------------------------------------------------------- + type Assoc k v = (k,v) type AssocL k v = [Assoc k v] @@ -53,4 +62,22 @@ assocLGroupSort :: Ord k => AssocL k v -> AssocL k [v] assocLGroupSort = map (foldr (\(k,v) (_,vs) -> (k,v:vs)) (panic "UHC.Util.AssocL.assocLGroupSort" ,[])) . groupSortOn fst + +------------------------------------------------------------------------------------------- +--- Utils: Combinations +------------------------------------------------------------------------------------------- + +-- | Combine [[x1..xn],..,[y1..ym]] to [[x1..y1],[x2..y1],..,[xn..ym]]. +-- Each element [xi..yi] is distinct based on the the key k in xi==(k,_) +combineToDistinguishedElts :: Eq k => [AssocL k v] -> [AssocL k v] +combineToDistinguishedElts [] = [] +combineToDistinguishedElts [[]] = [] +combineToDistinguishedElts [x] = map (:[]) x +combineToDistinguishedElts (l:ls) + = combine l $ combineToDistinguishedElts ls + where combine l ls + = concatMap (\e@(k,_) + -> mapMaybe (\ll -> maybe (Just (e:ll)) (const Nothing) $ lookup k ll) + ls + ) l diff --git a/src/UHC/Util/CHR.hs b/src/UHC/Util/CHR.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR.hs @@ -0,0 +1,13 @@ + +-- | Wrapper module around CHR stuff + +module UHC.Util.CHR + ( module UHC.Util.CHR.Base + , module UHC.Util.CHR.Key + -- , module UHC.Util.CHR.Solve + ) + where + +import UHC.Util.CHR.Base +import UHC.Util.CHR.Key +-- import UHC.Util.CHR.Solve diff --git a/src/UHC/Util/CHR/Base.hs b/src/UHC/Util/CHR/Base.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR/Base.hs @@ -0,0 +1,246 @@ +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, UndecidableInstances, ExistentialQuantification, ScopedTypeVariables, StandaloneDeriving #-} + +------------------------------------------------------------------------------------------- +--- Constraint Handling Rules +------------------------------------------------------------------------------------------- + +{- | +Derived from work by Gerrit vd Geest, but with searching structures for predicates +to avoid explosion of search space during resolution. +-} + +module UHC.Util.CHR.Base + ( IsConstraint(..) + + , IsCHRConstraint(..) + , CHRConstraint(..) + + , IsCHRGuard(..) + , CHRGuard(..) + + , CHREmptySubstitution(..) + , CHRMatchable(..), CHRMatchableKey + , CHRCheckable(..) + ) + where + +import qualified UHC.Util.TreeTrie as TreeTrie +import UHC.Util.VarMp +import Data.Monoid +import Data.Typeable +import Unsafe.Coerce +import qualified Data.Set as Set +import UHC.Util.Pretty +import UHC.Util.CHR.Key +import Control.Monad +import UHC.Util.Utils +import UHC.Util.Binary +import UHC.Util.Serialize +import UHC.Util.Substitutable + +------------------------------------------------------------------------------------------- +--- Constraint, Guard API +------------------------------------------------------------------------------------------- + +-- | (Class alias) API for constraint requirements +class ( CHRMatchable env c subst + , VarExtractable c + , VarUpdatable c subst + , Typeable c + , Serialize c + , TTKeyable c + , IsConstraint c + , Ord c, Ord (TTKey c) + , PP c, PP (TTKey c) + ) => IsCHRConstraint env c subst + +-- | (Class alias) API for guard requirements +class ( CHRCheckable env g subst + , VarExtractable g + , VarUpdatable g subst + , Typeable g + , Serialize g + , PP g + ) => IsCHRGuard env g subst + +------------------------------------------------------------------------------------------- +--- Existentially quantified Constraint representations to allow for mix of arbitrary universes +------------------------------------------------------------------------------------------- + +data CHRConstraint env subst + = forall c . + ( IsCHRConstraint env c subst + , TTKey (CHRConstraint env subst) ~ TTKey c + , ExtrValVarKey (CHRConstraint env subst) ~ ExtrValVarKey c + ) + => CHRConstraint + { chrConstraint :: c + } + +deriving instance Typeable (CHRConstraint env subst) +-- deriving instance (Data env, Data subst) => Data (CHRConstraint env subst) + +instance TTKeyable (CHRConstraint env subst) where + toTTKey' o (CHRConstraint c) = toTTKey' o c + +instance Show (CHRConstraint env subst) where + show _ = "CHRConstraint" + +instance PP (CHRConstraint env subst) where + pp (CHRConstraint c) = pp c + +instance IsConstraint (CHRConstraint env subst) where + cnstrRequiresSolve (CHRConstraint c) = cnstrRequiresSolve c + +instance Eq (CHRConstraint env subst) where + CHRConstraint (c1 :: c1) == CHRConstraint c2 = case cast c2 of + Just (c2' :: c1) -> c1 == c2' + _ -> False + +instance Ord (CHRConstraint env subst) where + CHRConstraint (c1 :: c1) `compare` CHRConstraint (c2 :: c2) = case cast c2 of + Just (c2' :: c1) -> c1 `compare` c2' + _ -> typeOf (undefined :: c1) `compare` typeOf (undefined :: c2) + +instance (CHRMatchableKey subst ~ TTKey (CHRConstraint env subst)) => CHRMatchable env (CHRConstraint env subst) subst where + chrMatchTo env subst c1 c2 + = case (c1, c2) of + (CHRConstraint (c1' :: c), CHRConstraint c2') -> case cast c2' of + Just (c2'' :: c) -> chrMatchTo env subst c1' c2'' + _ -> Nothing + +instance (Ord (ExtrValVarKey (CHRConstraint env subst))) => VarExtractable (CHRConstraint env subst) where + varFreeSet (CHRConstraint c) = varFreeSet c + +instance VarUpdatable (CHRConstraint env subst) subst where + s `varUpd` CHRConstraint c = CHRConstraint c' + where c' = s `varUpd` c + s `varUpdCyc` CHRConstraint c = (CHRConstraint c', cyc) + where (c', cyc) = s `varUpdCyc` c + +------------------------------------------------------------------------------------------- +--- Existentially quantified Guard representations to allow for mix of arbitrary universes +------------------------------------------------------------------------------------------- + +data CHRGuard env subst + = forall g . + ( IsCHRGuard env g subst + , ExtrValVarKey (CHRGuard env subst) ~ ExtrValVarKey g + ) + => CHRGuard + { chrGuard :: g + } + +deriving instance Typeable (CHRGuard env subst) +-- deriving instance (Data env, Data subst) => Data (CHRGuard env subst) + +instance Show (CHRGuard env subst) where + show _ = "CHRGuard" + +instance PP (CHRGuard env subst) where + pp (CHRGuard c) = pp c + +instance (Ord (ExtrValVarKey (CHRGuard env subst))) => VarExtractable (CHRGuard env subst) where + varFreeSet (CHRGuard g) = varFreeSet g + +instance VarUpdatable (CHRGuard env subst) subst where + s `varUpd` CHRGuard g = CHRGuard g' + where g' = s `varUpd` g + s `varUpdCyc` CHRGuard g = (CHRGuard g', cyc) + where (g', cyc) = s `varUpdCyc` g + +instance CHRCheckable env (CHRGuard env subst) subst where + chrCheck env subst (CHRGuard g) = chrCheck env subst g + +------------------------------------------------------------------------------------------- +--- CHREmptySubstitution +------------------------------------------------------------------------------------------- + +-- | Capability to yield an empty substitution. +class CHREmptySubstitution subst where + chrEmptySubst :: subst + +------------------------------------------------------------------------------------------- +--- CHRMatchable +------------------------------------------------------------------------------------------- + +type family CHRMatchableKey subst :: * + +-- | A Matchable participates in the reduction process as a reducable constraint. +class (TTKeyable x, TTKey x ~ CHRMatchableKey subst) => CHRMatchable env x subst where -- skey | subst -> skey where --- | x -> subst env where + chrMatchTo :: env -> subst -> x -> x -> Maybe subst + +------------------------------------------------------------------------------------------- +--- CHRCheckable +------------------------------------------------------------------------------------------- + +-- | A Checkable participates in the reduction process as a guard, to be checked. +class CHRCheckable env x subst where + chrCheck :: env -> subst -> x -> Maybe subst + +------------------------------------------------------------------------------------------- +--- What a constraint must be capable of +------------------------------------------------------------------------------------------- + +-- | The things a constraints needs to be capable of in order to participate in solving +class IsConstraint c where + -- | Requires solving? Or is just a residue... + cnstrRequiresSolve :: c -> Bool + +------------------------------------------------------------------------------------------- +--- Instances: Serialize +------------------------------------------------------------------------------------------- + +-- Does not work... + +{- +instance (Serialize c, IsCHRConstraint e c s, ExtrValVarKey c ~ ExtrValVarKey (CHRConstraint e s), TTKey c ~ TTKey (CHRConstraint e s)) => Serialize (CHRConstraint e s) where + sput (CHRConstraint a) = sput a + -- sget = sgetCHRConstraint (sget :: SGet c) + sget = liftM CHRConstraint (sget :: SGet c) +-} + +{- +instance (Serialize c, IsCHRConstraint e c s, ExtrValVarKey c ~ ExtrValVarKey (CHRConstraint e s), TTKey c ~ TTKey (CHRConstraint e s)) => Serialize (CHRConstraint e s) where + sput (CHRConstraint a) = sput a + -- sget = sgetCHRConstraint (sget :: SGet c) + sget = liftM CHRConstraint (sget :: SGet c) +-} + +{- +sgetCHRConstraint + :: forall e c s . + ( Serialize c + , IsCHRConstraint e c s + , ExtrValVarKey c ~ ExtrValVarKey (CHRConstraint e s) + , TTKey c ~ TTKey (CHRConstraint e s) + ) => SGet c -> SGet (CHRConstraint e s) +sgetCHRConstraint sgetc + = liftM CHRConstraint sgetc +-} + +{- + = do tr <- (sget :: SGet TypeRep) + if tr == typeRep (Proxy :: Proxy c) + then liftM (CHRConstraint . unsafeCoerce) sgetc + else panic $ "UHC.Util.CHR.Base.sgetCHRConstraint: " ++ show tr ++ " /= " +-} + +{- +sputgetCHRConstraint + :: ( Serialize c + , IsCHRConstraint e c s + , ExtrValVarKey c ~ ExtrValVarKey (CHRConstraint e s) + , TTKey c ~ TTKey (CHRConstraint e s) + ) => ( c -> SPut + , SGet c -> SGet (CHRConstraint e s) + ) +sputgetCHRConstraint = (sput, liftM CHRConstraint) +(sputCHRConstraint, sgetCHRConstraint) = sputgetCHRConstraint +-} + +{- +instance Serialize (CHRGuard e s) where + sput (CHRGuard a) = sput a + sget = liftM CHRGuard sget +-} diff --git a/src/UHC/Util/CHR/Key.hs b/src/UHC/Util/CHR/Key.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR/Key.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} + +module UHC.Util.CHR.Key + ( + TTKeyableOpts(..) + , defaultTTKeyableOpts + + , TTKeyable(..) + , TTKey + , toTTKey + ) + where + +import UHC.Util.TreeTrie + +------------------------------------------------------------------------------------------- +--- TTKeyable +------------------------------------------------------------------------------------------- + +data TTKeyableOpts + = TTKeyableOpts + { ttkoptsVarsAsWild :: Bool -- treat vars as wildcards + } + +defaultTTKeyableOpts = TTKeyableOpts True + +type family TTKey x :: * + +type instance TTKey [x] = TTKey x + +-- | TreeTrie key construction +class TTKeyable x where -- key | x -> key where + toTTKey' :: TTKeyableOpts -> x -> TreeTrieKey (TTKey x) -- option parameterized constuction + toTTKeyParentChildren' :: TTKeyableOpts -> x -> (TreeTrie1Key (TTKey x), [TreeTrieMpKey (TTKey x)]) -- building block: parent of children + children + + -- default impl + toTTKey' o = uncurry ttkAdd' . toTTKeyParentChildren' o + toTTKeyParentChildren' o = ttkParentChildren . toTTKey' o + +toTTKey :: (TTKeyable x, TTKey x ~ TrTrKey x) => x -> TreeTrieKey (TTKey x) +toTTKey = toTTKey' defaultTTKeyableOpts + + diff --git a/src/UHC/Util/CHR/Rule.hs b/src/UHC/Util/CHR/Rule.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR/Rule.hs @@ -0,0 +1,264 @@ +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, UndecidableInstances, ExistentialQuantification, ScopedTypeVariables, StandaloneDeriving #-} +-- {-# LANGUAGE AllowAmbiguousTypes #-} + +------------------------------------------------------------------------------------------- +--- Constraint Handling Rules +------------------------------------------------------------------------------------------- + +{- | +Derived from work by Gerrit vd Geest, but with searching structures for predicates +to avoid explosion of search space during resolution. +-} + +module UHC.Util.CHR.Rule + ( CHRRule(..) + + , Rule(..) + + , (<==>), (==>), (|>) + , MkSolverConstraint(..) + , MkSolverGuard(..) + ) + where + +import qualified UHC.Util.TreeTrie as TreeTrie +import UHC.Util.CHR.Base +import UHC.Util.VarMp +import UHC.Util.Utils +import Data.Monoid +import Data.Typeable +import Data.Data +import qualified Data.Set as Set +import UHC.Util.Pretty +import UHC.Util.CHR.Key +import Control.Monad +import UHC.Util.Binary +import UHC.Util.Serialize +import UHC.Util.Substitutable + +------------------------------------------------------------------------------------------- +--- Existentially quantified Rule representations to allow for mix of arbitrary universes +------------------------------------------------------------------------------------------- + +data CHRRule env subst + = CHRRule + { chrRule :: Rule (CHRConstraint env subst) (CHRGuard env subst) + } + deriving (Typeable) + +type instance TTKey (CHRRule env subst) = TTKey (CHRConstraint env subst) + +deriving instance Typeable (CHRRule env subst) + +instance Show (CHRRule env subst) where + show _ = "CHRRule" + +instance PP (CHRRule env subst) where + pp (CHRRule r) = pp r + +------------------------------------------------------------------------------------------- +--- CHR, derived structures +------------------------------------------------------------------------------------------- + +-- | A CHR (rule) consist of head (simplification + propagation, boundary indicated by an Int), guard, and a body. All may be empty, but not all at the same time. +data Rule cnstr guard + = Rule + { ruleHead :: ![cnstr] + , ruleSimpSz :: !Int -- length of the part of the head which is the simplification part + , ruleGuard :: ![guard] -- subst -> Maybe subst + , ruleBody :: ![cnstr] + } + deriving (Typeable, Data) + +emptyCHRGuard :: [a] +emptyCHRGuard = [] + +instance Show (Rule c g) where + show _ = "Rule" + +instance (PP c,PP g) => PP (Rule c g) where + pp chr + = case chr of + (Rule h@(_:_) sz g b) | sz == 0 -> ppChr ([ppL h, pp "==>"] ++ ppGB g b) + (Rule h@(_:_) sz g b) | sz == length h -> ppChr ([ppL h, pp "<==>"] ++ ppGB g b) + (Rule h@(_:_) sz g b) -> ppChr ([ppL (take sz h), pp "|", ppL (drop sz h), pp "<==>"] ++ ppGB g b) + (Rule [] _ g b) -> ppChr (ppGB g b) + where ppGB g@(_:_) b@(_:_) = [ppL g, "|" >#< ppL b] + ppGB g@(_:_) [] = [ppL g >#< "|"] + ppGB [] b@(_:_) = [ppL b] + ppGB [] [] = [] + ppL [x] = pp x + ppL xs = ppBracketsCommasBlock xs -- ppParensCommasBlock xs + ppChr l = vlist l -- ppCurlysBlock + +type instance TTKey (Rule cnstr guard) = TTKey cnstr + +instance (TTKeyable cnstr) => TTKeyable (Rule cnstr guard) where + toTTKey' o chr = toTTKey' o $ head $ ruleHead chr + +------------------------------------------------------------------------------------------- +--- Var instances +------------------------------------------------------------------------------------------- + +type instance ExtrValVarKey (Rule c g) = ExtrValVarKey c + +instance (VarExtractable c, VarExtractable g, ExtrValVarKey c ~ ExtrValVarKey g) => VarExtractable (Rule c g) where + varFreeSet (Rule {ruleHead=h, ruleGuard=g, ruleBody=b}) + = Set.unions $ concat [map varFreeSet h, map varFreeSet g, map varFreeSet b] + +instance (VarUpdatable c s, VarUpdatable g s) => VarUpdatable (Rule c g) s where + varUpd s r@(Rule {ruleHead=h, ruleGuard=g, ruleBody=b}) + = r {ruleHead = map (varUpd s) h, ruleGuard = map (varUpd s) g, ruleBody = map (varUpd s) b} + +------------------------------------------------------------------------------------------- +--- Construction: Rule +------------------------------------------------------------------------------------------- + +{- +class MkRule c g c' g' r | r c -> g g' c', r g -> c c' g', c c' -> g g' r, g g' -> c c' r, r g' -> c c' g, c' g' r -> c g, r -> c g c' g' where +-- class MkRule c g c' g' r | r -> c' g' c g, c' -> g' r, g' -> c' r, c -> g r, g -> c r where +-- class MkRule c g c' g' r | r -> c' g' c g where + -- | Lift constraint, from In to Out + toSolverConstraint :: c -> c' + -- | Lift guard, from In to Out + toSolverGuard :: g -> g' + -- | Make rule + mkRule :: [c'] -> Int -> [g'] -> [c'] -> r + -- | Add guards to rule + guardRule :: [g'] -> r -> r + +infix 1 <==>, ==> +infixr 0 |> + +(<==>), (==>) :: forall c g c' g' r . (MkRule c g c' g' r) => [c] -> [c] -> r +hs <==> bs = mkRule (map toSolverConstraint hs) (length hs) ([]::[g']) (map toSolverConstraint bs) +hs ==> bs = mkRule (map toSolverConstraint hs) 0 ([]::[g']) (map toSolverConstraint bs) + +(|>) :: (MkRule c g c' g' r) => r -> [g] -> r +r |> g = guardRule (map toSolverGuard g) r + +instance MkRule c g c g (Rule c g) where + toSolverConstraint = id + toSolverGuard = id + mkRule = Rule + guardRule g r = r {ruleGuard = ruleGuard r ++ g} +-} + +class MkSolverConstraint c c' where + toSolverConstraint :: c' -> c + fromSolverConstraint :: c -> Maybe c' + +instance {-# INCOHERENT #-} MkSolverConstraint c c where + toSolverConstraint = id + fromSolverConstraint = Just + +instance {-# OVERLAPS #-} + ( IsCHRConstraint e c s + , TTKey (CHRConstraint e s) ~ TTKey c + , ExtrValVarKey (CHRConstraint e s) ~ ExtrValVarKey c + ) => MkSolverConstraint (CHRConstraint e s) c where + toSolverConstraint = CHRConstraint + fromSolverConstraint (CHRConstraint c) = cast c + +class MkSolverGuard g g' where + toSolverGuard :: g' -> g + fromSolverGuard :: g -> Maybe g' + +instance {-# INCOHERENT #-} MkSolverGuard g g where + toSolverGuard = id + fromSolverGuard = Just + +instance {-# OVERLAPS #-} + ( IsCHRGuard e g s + , ExtrValVarKey (CHRGuard e s) ~ ExtrValVarKey g + ) => MkSolverGuard (CHRGuard e s) g where + toSolverGuard = CHRGuard + fromSolverGuard (CHRGuard g) = cast g + +class MkRule r where + type SolverConstraint r :: * + type SolverGuard r :: * + -- | Make rule + mkRule :: [SolverConstraint r] -> Int -> [SolverGuard r] -> [SolverConstraint r] -> r + -- | Add guards to rule + guardRule :: [SolverGuard r] -> r -> r + +instance MkRule (Rule c g) where + type SolverConstraint (Rule c g) = c + type SolverGuard (Rule c g) = g + mkRule = Rule + guardRule g r = r {ruleGuard = ruleGuard r ++ g} + +instance MkRule (CHRRule e s) where + type SolverConstraint (CHRRule e s) = (CHRConstraint e s) + type SolverGuard (CHRRule e s) = (CHRGuard e s) + mkRule h1 h2 l b = CHRRule $ mkRule h1 h2 l b + guardRule g (CHRRule r) = CHRRule $ guardRule g r + +infix 1 <==>, ==> +infixr 0 |> + +(<==>), (==>) :: (MkRule r, MkSolverConstraint (SolverConstraint r) c1, MkSolverConstraint (SolverConstraint r) c2) => [c1] -> [c2] -> r +hs <==> bs = mkRule (map toSolverConstraint hs) (length hs) [] (map toSolverConstraint bs) +hs ==> bs = mkRule (map toSolverConstraint hs) 0 [] (map toSolverConstraint bs) + +(|>) :: (MkRule r, MkSolverGuard (SolverGuard r) g') => r -> [g'] -> r +r |> g = guardRule (map toSolverGuard g) r + + +{- +-- Below variant runs into typing problem w.r.t. injectivity of type functions... +class MkRule r where + type MkSolverConstraintIn r :: * + type MkSolverGuardIn r :: * + type MkSolverConstraintOut r :: * + type MkSolverGuardOut r :: * + -- | Lift constraint, from In to Out + toSolverConstraint :: MkSolverConstraintIn r -> MkSolverConstraintOut r + -- | Lift guard, from In to Out + toSolverGuard :: MkSolverGuardIn r -> MkSolverGuardOut r + -- | Make rule + mkRule :: [MkSolverConstraintOut r] -> Int -> [MkSolverGuardOut r] -> [MkSolverConstraintOut r] -> r + -- | Add guards to rule + guardRule :: [MkSolverGuardOut r] -> r -> r + +infix 1 <==>, ==> +infixr 0 |> + +(<==>), (==>) :: forall r c . (MkRule r, c ~ MkSolverConstraintIn r) => [c] -> [c] -> r +hs <==> bs = mkRule (map toSolverConstraint hs) (length hs) (map toSolverGuard emptyCHRGuard) (map toSolverConstraint bs) +hs ==> bs = mkRule (map toSolverConstraint hs) 0 (map toSolverGuard emptyCHRGuard) (map toSolverConstraint bs) + +(|>) :: (MkRule r, g ~ MkSolverGuardIn r) => r -> [g] -> r +r |> g = guardRule (map toSolverGuard g) r + +instance MkRule (Rule c g) where + type MkSolverConstraintIn (Rule c g) = c + type MkSolverGuardIn (Rule c g) = g + type MkSolverConstraintOut (Rule c g) = c + type MkSolverGuardOut (Rule c g) = g + toSolverConstraint = id + toSolverGuard = id + mkRule = Rule + guardRule g r = r {ruleGuard = ruleGuard r ++ g} +-} + +------------------------------------------------------------------------------------------- +--- Instances: Serialize +------------------------------------------------------------------------------------------- + +instance (Serialize c,Serialize g) => Serialize (Rule c g) where + sput (Rule a b c d) = sput a >> sput b >> sput c >> sput d + sget = liftM4 Rule sget sget sget sget + +{- +instance (MkSolverConstraint (CHRConstraint e s) x', Serialize x') => Serialize (CHRConstraint e s) where + sput x = maybe (panic "UHC.Util.CHR.Rule.Serialize.MkSolverConstraint.sput") sput $ fromSolverConstraint x + sget = liftM toSolverConstraint sget +-} + +{- +instance Serialize (CHRRule e s) where + sput (CHRRule a) = sput a + sget = liftM CHRRule sget +-} diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs @@ -0,0 +1,808 @@ +{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses #-} + +------------------------------------------------------------------------------------------- +--- CHR TreeTrie based solver shared internals +------------------------------------------------------------------------------------------- + +module UHC.Util.CHR.Solve.TreeTrie.Internal + ( CHRTrie + , CHRTrieKey + , CHRLookupHow + + , chrLookupHowExact + , chrLookupHowWildAtTrie + , chrLookupHowWildAtKey + + , emptyCHRTrie + + , chrToKey + , chrToWorkKey + , chrTrieDeleteListByKey + , chrTrieElems + , chrTrieFromListByKeyWith + , chrTrieFromListPartialExactWith + , chrTrieLookup + , chrTrieToListByKey + , chrTrieUnion + , chrTrieUnionWith + + , CHRKey + , UsedByKey + , ppUsedByKey + + , WorkTime + , initWorkTime + + , WorkKey + , WorkUsedInMap + , WorkTrie + + , Work(..) + + , WorkList(..) + , emptyWorkList + , wlUsedInUnion + , wlToList + , wlCnstrToIns + , wlDeleteByKeyAndInsert' + , wlInsert + + , SolveCount + , scntInc + + , SolveMatchCache' + + , LastQuery + , emptyLastQuery + , lqUnion + , lqSingleton + , lqLookupW + , lqLookupC + + , SolveStep'(..) + , SolveTrace' + , ppSolveTrace + + , SolveState'(..) + , emptySolveState + , stDoneCnstrs + , solveStateResetDone + , chrSolveStateDoneConstraints + , chrSolveStateTrace + + , slvCombine + + , module UHC.Util.CHR.Rule + ) + where + +import UHC.Util.CHR.Base +import UHC.Util.CHR.Key +import UHC.Util.CHR.Rule +-- import UHC.Util.CHR.Constraint.UHC +import UHC.Util.Substitutable +import UHC.Util.VarLookup +import UHC.Util.VarMp +import UHC.Util.AssocL +import UHC.Util.TreeTrie as TreeTrie +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.List as List +import Data.Typeable +import Data.Data +import Data.Maybe +import UHC.Util.Pretty as Pretty +import UHC.Util.Serialize +import Control.Monad +import Control.Monad.State.Strict +import UHC.Util.Utils + +------------------------------------------------------------------------------------------- +--- Choice of Trie structure +------------------------------------------------------------------------------------------- + +type CHRTrie v = TreeTrie.TreeTrie (TTKey v) v +type CHRTrieKey v = TreeTrie.TreeTrieKey (TTKey v) +type CHRLookupHow = TreeTrieLookup + +chrLookupHowExact = TTL_Exact +chrLookupHowWildAtTrie = TTL_WildInTrie +chrLookupHowWildAtKey = TTL_WildInKey + +emptyCHRTrie = TreeTrie.empty + +chrTrieFromListByKeyWith :: (Ord (TTKey v)) => (v -> v -> v) -> [(CHRTrieKey v,v)] -> CHRTrie v +chrTrieFromListByKeyWith = TreeTrie.fromListByKeyWith +{-# INLINE chrTrieFromListByKeyWith #-} + +chrTrieToListByKey :: (Ord (TTKey v)) => CHRTrie v -> [(CHRTrieKey v,v)] +chrTrieToListByKey = TreeTrie.toListByKey +{-# INLINE chrTrieToListByKey #-} + +chrTrieUnionWith :: (Ord (TTKey v)) => (v -> v -> v) -> CHRTrie v -> CHRTrie v -> CHRTrie v +chrTrieUnionWith = TreeTrie.unionWith +{-# INLINE chrTrieUnionWith #-} + +chrTrieUnion :: (Ord (TTKey v)) => CHRTrie v -> CHRTrie v -> CHRTrie v +chrTrieUnion = TreeTrie.union +{-# INLINE chrTrieUnion #-} + +chrTrieElems :: CHRTrie v -> [v] +chrTrieElems = TreeTrie.elems +{-# INLINE chrTrieElems #-} + +chrTrieDeleteListByKey :: (Ord (TTKey v)) => [CHRTrieKey v] -> CHRTrie v -> CHRTrie v +chrTrieDeleteListByKey = TreeTrie.deleteListByKey +{-# INLINE chrTrieDeleteListByKey #-} + +chrTrieFromListPartialExactWith :: (Ord (TTKey v)) => (v -> v -> v) -> [(CHRTrieKey v,v)] -> CHRTrie v +chrTrieFromListPartialExactWith = TreeTrie.fromListByKeyWith +{-# INLINE chrTrieFromListPartialExactWith #-} + +chrTrieLookup' :: (Ord (TTKey v), PP (TTKey v)) => (CHRTrieKey v -> v -> v') -> CHRLookupHow -> CHRTrieKey v -> CHRTrie v -> ([v'],Maybe v') +chrTrieLookup' = TreeTrie.lookupPartialByKey' +{-# INLINE chrTrieLookup' #-} + +chrTrieLookup :: (Ord (TTKey v), PP (TTKey v)) => CHRLookupHow -> CHRTrieKey v -> CHRTrie v -> ([v],Maybe v) +chrTrieLookup = TreeTrie.lookupPartialByKey +{-# INLINE chrTrieLookup #-} + +chrToKey :: (TTKeyable x, TrTrKey x ~ TTKey x) => x -> CHRTrieKey x +chrToKey = ttkFixate . toTTKey +{-# INLINE chrToKey #-} + +chrToWorkKey :: (TTKeyable x) => x -> CHRTrieKey x +chrToWorkKey = ttkFixate . toTTKey' (defaultTTKeyableOpts {ttkoptsVarsAsWild = False}) +{-# INLINE chrToWorkKey #-} + +------------------------------------------------------------------------------------------- +--- CHR store, with fast search +------------------------------------------------------------------------------------------- + +-- type CHRKey = CHRTrieKey +type CHRKey v = CHRTrieKey v +type UsedByKey v = (CHRKey v,Int) + +-- ppUsedByKey :: UsedByKey v -> PP_Doc +ppUsedByKey (k,i) = ppTreeTrieKey k >|< "/" >|< i + +{- +-- | A CHR as stored in a CHRStore, requiring additional info for efficiency +data StoredCHR e s + = StoredCHR + { storedChr :: !(CHRRule e s) -- the Rule + , storedKeyedInx :: !Int -- index of constraint for which is keyed into store + , storedKeys :: ![Maybe (CHRKey (CHRConstraint e s))] -- keys of all constraints; at storedKeyedInx: Nothing + , storedIdent :: !(UsedByKey (CHRConstraint e s)) -- the identification of a CHR, used for propagation rules (see remark at begin) + } + deriving (Typeable) +-} + +{- +deriving instance (Data (TTKey c), Data c, Data g) => Data (StoredCHR c g) + +type instance TTKey (StoredCHR c g) = TTKey c + +instance (TTKeyable (Rule c g)) => TTKeyable (StoredCHR c g) where + toTTKey' o schr = toTTKey' o $ storedChr schr + +-- | The size of the simplification part of a CHR +storedSimpSz :: StoredCHR c g -> Int +storedSimpSz = ruleSimpSz . storedChr +{-# INLINE storedSimpSz #-} + +-- | A CHR store is a trie structure +newtype CHRStore cnstr guard + = CHRStore + { chrstoreTrie :: CHRTrie [StoredCHR cnstr guard] + } + deriving (Typeable) + +deriving instance (Data (TTKey cnstr), Ord (TTKey cnstr), Data cnstr, Data guard) => Data (CHRStore cnstr guard) + +mkCHRStore trie = CHRStore trie + +emptyCHRStore :: CHRStore cnstr guard +emptyCHRStore = mkCHRStore emptyCHRTrie + +-- | Combine lists of stored CHRs by concat, adapting their identification nr to be unique +cmbStoredCHRs :: [StoredCHR c g] -> [StoredCHR c g] -> [StoredCHR c g] +cmbStoredCHRs s1 s2 + = map (\s@(StoredCHR {storedIdent=(k,nr)}) -> s {storedIdent = (k,nr+l)}) s1 ++ s2 + where l = length s2 + +instance Show (StoredCHR c g) where + show _ = "StoredCHR" + +ppStoredCHR :: (PP (TTKey c), PP c, PP g) => StoredCHR c g -> PP_Doc +ppStoredCHR c@(StoredCHR {storedIdent=(idKey,idSeqNr)}) + = storedChr c + >-< indent 2 + (ppParensCommas + [ pp $ storedKeyedInx c + , pp $ storedSimpSz c + , "keys" >#< (ppBracketsCommas $ map (maybe (pp "?") ppTreeTrieKey) $ storedKeys c) + , "ident" >#< ppParensCommas [ppTreeTrieKey idKey,pp idSeqNr] + ]) + +instance (PP (TTKey c), PP c, PP g) => PP (StoredCHR c g) where + pp = ppStoredCHR + +-- | Convert from list to store +chrStoreFromElems :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => [Rule c g] -> CHRStore c g +chrStoreFromElems chrs + = mkCHRStore + $ chrTrieFromListByKeyWith cmbStoredCHRs + [ (k,[StoredCHR chr i ks' (concat ks,0)]) + | chr <- chrs + , let cs = ruleHead chr + simpSz = ruleSimpSz chr + ks = map chrToKey cs + , (c,k,i) <- zip3 cs ks [0..] + , let (ks1,(_:ks2)) = splitAt i ks + ks' = map Just ks1 ++ [Nothing] ++ map Just ks2 + ] + +chrStoreSingletonElem :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => Rule c g -> CHRStore c g +chrStoreSingletonElem x = chrStoreFromElems [x] + +chrStoreUnion :: (Ord (TTKey c)) => CHRStore c g -> CHRStore c g -> CHRStore c g +chrStoreUnion cs1 cs2 = mkCHRStore $ chrTrieUnionWith cmbStoredCHRs (chrstoreTrie cs1) (chrstoreTrie cs2) +{-# INLINE chrStoreUnion #-} + +chrStoreUnions :: (Ord (TTKey c)) => [CHRStore c g] -> CHRStore c g +chrStoreUnions [] = emptyCHRStore +chrStoreUnions [s] = s +chrStoreUnions ss = foldr1 chrStoreUnion ss +{-# INLINE chrStoreUnions #-} + +chrStoreToList :: (Ord (TTKey c)) => CHRStore c g -> [(CHRKey c,[Rule c g])] +chrStoreToList cs + = [ (k,chrs) + | (k,e) <- chrTrieToListByKey $ chrstoreTrie cs + , let chrs = [chr | (StoredCHR {storedChr = chr, storedKeyedInx = 0}) <- e] + , not $ Prelude.null chrs + ] + +chrStoreElems :: (Ord (TTKey c)) => CHRStore c g -> [Rule c g] +chrStoreElems = concatMap snd . chrStoreToList + +ppCHRStore :: (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => CHRStore c g -> PP_Doc +ppCHRStore = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrStoreToList + +ppCHRStore' :: (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => CHRStore c g -> PP_Doc +ppCHRStore' = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrTrieToListByKey . chrstoreTrie + +-} + +------------------------------------------------------------------------------------------- +--- WorkTime, the time/history counter +------------------------------------------------------------------------------------------- + +type WorkTime = Int + +initWorkTime :: WorkTime +initWorkTime = 0 + +------------------------------------------------------------------------------------------- +--- Solver worklist +------------------------------------------------------------------------------------------- + + +type WorkKey v = CHRKey v +type WorkUsedInMap v = Map.Map (Set.Set (CHRKey v)) (Set.Set (UsedByKey v)) +type WorkTrie c = CHRTrie (Work c) + +-- | A chunk of work to do when solving, a constraint + sequence nr +data Work c + = Work + { workKey :: WorkKey c + , workCnstr :: !c -- the constraint to be reduced + , workTime :: WorkTime -- the history count at which the work was added + -- , workUsedIn :: Set.Set (CHRKey c) -- marked with the propagation rules already applied to it + } + +type instance TTKey (Work c) = TTKey c + +-- | The work to be done (wlQueue), also represented as a trie (wlTrie) because efficient check on already worked on is needed. +-- A done set (wlDoneSet) remembers which CHRs (itself a list of constraints) have been solved. +-- To prevent duplicate propagation a mapping from CHRs to a map (wlUsedIn) to the CHRs it is used in is maintained. +data WorkList c + = WorkList + { wlTrie :: !(WorkTrie c) + , wlDoneSet :: !(Set.Set (WorkKey c)) -- accumulative store of all keys added, set semantics, thereby avoiding double entry + , wlQueue :: !(AssocL (WorkKey c) (Work c)) + , wlScanned :: !(AssocL (WorkKey c) (Work c)) -- tried but could not solve, so retry when other succeeds + , wlUsedIn :: !(WorkUsedInMap c) -- which work items are used in which propagation constraints + } + +emptyWorkList = WorkList emptyCHRTrie Set.empty [] [] Map.empty + +-- wlUsedInUnion :: (Ord k, k ~ TTKey c) => WorkUsedInMap c -> WorkUsedInMap c -> WorkUsedInMap c +wlUsedInUnion = Map.unionWith Set.union +{-# INLINE wlUsedInUnion #-} + +instance Show (Work c) where + show _ = "SolveWork" + +instance (PP c) => PP (Work c) where + pp w = pp $ workCnstr w + + + +wlToList :: {- (PP p, PP i) => -} WorkList c -> [c] +wlToList wl = map workCnstr $ chrTrieElems $ wlTrie wl + +wlCnstrToIns :: (TTKeyable c, TTKey c ~ TrTrKey c, Ord (TTKey c)) => WorkList c -> [c] -> AssocL (WorkKey c) c +wlCnstrToIns wl@(WorkList {wlDoneSet = ds}) inscs + = [(chrToWorkKey c,c) | c <- inscs, let k = chrToKey c, not (k `Set.member` ds)] + +wlDeleteByKeyAndInsert' :: (Ord (TTKey c)) => WorkTime -> [WorkKey c] -> AssocL (WorkKey c) c -> WorkList c -> WorkList c +wlDeleteByKeyAndInsert' wtm delkeys inskeycs wl@(WorkList {wlQueue = wlq, wlTrie = wlt, wlDoneSet = ds}) + = wl { wlQueue = Map.toList inswork ++ [ w | w@(k,_) <- wlq, not (k `elem` delkeys) ] + , wlTrie = instrie `chrTrieUnion` chrTrieDeleteListByKey delkeys wlt + , wlDoneSet = Map.keysSet inswork `Set.union` ds + } + where inswork = Map.fromList [ (k,Work k c wtm) | (k,c) <- inskeycs ] + instrie = chrTrieFromListPartialExactWith const $ Map.toList inswork + +wlDeleteByKeyAndInsert :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => WorkTime -> [WorkKey c] -> [c] -> WorkList c -> WorkList c +wlDeleteByKeyAndInsert wtm delkeys inscs wl + = wlDeleteByKeyAndInsert' wtm delkeys (wlCnstrToIns wl inscs) wl + +wlInsert :: (TTKeyable c, Ord (TTKey c), TrTrKey c ~ TTKey c) => WorkTime -> [c] -> WorkList c -> WorkList c +wlInsert wtm = wlDeleteByKeyAndInsert wtm [] +{-# INLINE wlInsert #-} + +------------------------------------------------------------------------------------------- +--- Solver counting +------------------------------------------------------------------------------------------- + +type SolveCount a b = Map.Map a (Map.Map b Int) + +scntUnion :: (Ord a,Ord b) => SolveCount a b -> SolveCount a b -> SolveCount a b +scntUnion = Map.unionWith (Map.unionWith (+)) +{-# INLINE scntUnion #-} + +scntInc :: (Ord a,Ord b) => a -> b -> SolveCount a b -> SolveCount a b +scntInc a b c1 = Map.singleton a (Map.singleton b 1) `scntUnion` c1 +{-# INLINE scntInc #-} + +------------------------------------------------------------------------------------------- +--- Cache for maintaining which WorkKey has already had a match +------------------------------------------------------------------------------------------- + +type SolveMatchCache' c schr s = Map.Map (WorkKey c) [((schr,([WorkKey c],[Work c])),s)] + +------------------------------------------------------------------------------------------- +--- WorkTime of last search +------------------------------------------------------------------------------------------- + + +type LastQueryW v = Map.Map (WorkKey v) WorkTime +type LastQuery v = Map.Map (CHRKey v) (LastQueryW v) + +-- emptyLastQuery :: LastQuery v +emptyLastQuery = Map.empty +{-# INLINE emptyLastQuery #-} + +-- lqSingleton :: CHRKey v -> Set.Set (WorkKey v) -> WorkTime -> LastQuery v +lqSingleton ck wks wtm = Map.singleton ck $ Map.fromList [ (w,wtm) | w <- Set.toList wks ] +{-# INLINE lqSingleton #-} + +-- lqUnion :: LastQuery v -> LastQuery v -> LastQuery v +lqUnion = Map.unionWith Map.union +{-# INLINE lqUnion #-} + +-- lqLookupC :: CHRKey v -> LastQuery v -> LastQueryW v +lqLookupC = Map.findWithDefault Map.empty +{-# INLINE lqLookupC #-} + +-- lqLookupW :: WorkKey v -> LastQueryW v -> WorkTime +lqLookupW = Map.findWithDefault initWorkTime +{-# INLINE lqLookupW #-} + +------------------------------------------------------------------------------------------- +--- Solver trace +------------------------------------------------------------------------------------------- + +-- | A trace step +data SolveStep' c r s + = SolveStep + { stepChr :: r + , stepSubst :: s + , stepNewTodo :: [c] + , stepNewDone :: [c] + } + | SolveStats + { stepStats :: Map.Map String PP_Doc + } + | SolveDbg + { stepPP :: PP_Doc + } + +type SolveTrace' c r s = [SolveStep' c r s] + +instance Show (SolveStep' c r s) where + show _ = "SolveStep" + +instance (PP r, PP c) => {- (PP c, PP g) => -} PP (SolveStep' c r s) where + pp (SolveStep step _ todo done) = "STEP" >#< (step >-< "new todo:" >#< ppBracketsCommas todo >-< "new done:" >#< ppBracketsCommas done) + pp (SolveStats stats ) = "STATS" >#< (ppAssocLV (Map.toList stats)) + pp (SolveDbg p ) = "DBG" >#< p + +ppSolveTrace :: (PP r, PP c) => {- (PP s, PP c, PP g) => -} SolveTrace' c r s -> PP_Doc +ppSolveTrace tr = ppBracketsCommasBlock [ pp st | st <- tr ] + +------------------------------------------------------------------------------------------- +--- Solve state +------------------------------------------------------------------------------------------- + + +data SolveState' c r sr s + = SolveState + { stWorkList :: !(WorkList c) + , stDoneCnstrSet :: !(Set.Set c) + , stTrace :: SolveTrace' c r s + , stCountCnstr :: SolveCount (WorkKey c) String + , stMatchCache :: !(SolveMatchCache' c sr s) + , stHistoryCount :: WorkTime + , stLastQuery :: (LastQuery c) + } + +stDoneCnstrs :: SolveState' c r sr s -> [c] +stDoneCnstrs = Set.toList . stDoneCnstrSet +{-# INLINE stDoneCnstrs #-} + +emptySolveState :: SolveState' c r sr s +emptySolveState = SolveState emptyWorkList Set.empty [] Map.empty Map.empty initWorkTime emptyLastQuery +{-# INLINE emptySolveState #-} + +solveStateResetDone :: SolveState' c r sr s -> SolveState' c r sr s +solveStateResetDone s = s {stDoneCnstrSet = Set.empty} +{-# INLINE solveStateResetDone #-} + +chrSolveStateDoneConstraints :: SolveState' c r sr s -> [c] +chrSolveStateDoneConstraints = stDoneCnstrs +{-# INLINE chrSolveStateDoneConstraints #-} + +chrSolveStateTrace :: SolveState' c r sr s -> SolveTrace' c r s +chrSolveStateTrace = stTrace +{-# INLINE chrSolveStateTrace #-} + +------------------------------------------------------------------------------------------- +--- Solver +------------------------------------------------------------------------------------------- + +{- + +-- | (Class alias) API for solving requirements +class ( IsCHRConstraint env c s + , IsCHRGuard env g s + , VarLookupCmb s s + , VarUpdatable s s + , CHREmptySubstitution s + , TrTrKey c ~ TTKey c + ) => IsCHRSolvable env c g s + +-} + +{- +chrSolve + :: forall env c g s . + ( IsCHRSolvable env c g s + ) + => env + -> CHRStore c g + -> [c] + -> [c] +chrSolve env chrStore cnstrs + = work ++ done + where (work, done, _ :: SolveTrace c g s) = chrSolve' env chrStore cnstrs +-} + +{- + +-- | Solve +chrSolve' + :: forall env c g s . + ( IsCHRSolvable env c g s + ) + => env + -> CHRStore c g + -> [c] + -> ([c],[c],SolveTrace c g s) +chrSolve' env chrStore cnstrs + = (wlToList (stWorkList finalState), stDoneCnstrs finalState, stTrace finalState) + where finalState = chrSolve'' env chrStore cnstrs emptySolveState + +-- | Solve +chrSolve'' + :: forall env c g s . + ( IsCHRSolvable env c g s + ) + => env + -> CHRStore c g + -> [c] + -> SolveState c g s + -> SolveState c g s +chrSolve'' env chrStore cnstrs prevState + = flip execState prevState $ chrSolveM env chrStore cnstrs + +-- | Solve +chrSolveM + :: forall env c g s . + ( IsCHRSolvable env c g s + ) + => env + -> CHRStore c g + -> [c] + -> State (SolveState c g s) () +chrSolveM env chrStore cnstrs = do + modify initState + iter +{- + modify $ + addStats Map.empty + [ ("workMatches",ppAssocLV [(ppTreeTrieKey k,pp (fromJust l)) + | (k,c) <- Map.toList $ stCountCnstr st, let l = Map.lookup "workMatched" c, isJust l]) + ] +-} + modify $ \st -> st {stMatchCache = Map.empty} + where iter = do + st <- get + case st of + (SolveState {stWorkList = wl@(WorkList {wlQueue = (workHd@(workHdKey,_) : workTl)})}) -> + case matches of + (_:_) -> do + put +{- + $ addStats Map.empty + [ ("(0) yes work", ppTreeTrieKey workHdKey) + ] + $ +-} + stmatch + expandMatch matches + where -- expandMatch :: SolveState c g s -> [((StoredCHR c g, ([WorkKey c], [Work c])), s)] -> SolveState c g s + expandMatch ( ( ( schr@(StoredCHR {storedIdent = chrId, storedChr = chr@(Rule {ruleBody = b, ruleSimpSz = simpSz})}) + , (keys,works) + ) + , subst + ) : tlMatch + ) = do + st@(SolveState {stWorkList = wl, stHistoryCount = histCount}) <- get + let (tlMatchY,tlMatchN) = partition (\(r@(_,(ks,_)),_) -> not (any (`elem` keysSimp) ks || slvIsUsedByPropPart (wlUsedIn wl') r)) tlMatch + (keysSimp,keysProp) = splitAt simpSz keys + usedIn = Map.singleton (Set.fromList keysProp) (Set.singleton chrId) + (bTodo,bDone) = splitDone $ map (varUpd subst) b + bTodo' = wlCnstrToIns wl bTodo + wl' = wlDeleteByKeyAndInsert' histCount keysSimp bTodo' + $ wl { wlUsedIn = usedIn `wlUsedInUnion` wlUsedIn wl + , wlScanned = [] + , wlQueue = wlQueue wl ++ wlScanned wl + } + st' = st { stWorkList = wl' +{- + , stTrace = SolveStep chr' subst (assocLElts bTodo') bDone : {- SolveDbg (ppwork >-< ppdbg) : -} stTrace st +-} + , stDoneCnstrSet = Set.unions [Set.fromList bDone, Set.fromList $ map workCnstr $ take simpSz works, stDoneCnstrSet st] + , stMatchCache = if List.null bTodo' then stMatchCache st else Map.empty + , stHistoryCount = histCount + 1 + } +{- + chr'= subst `varUpd` chr + ppwork = "workkey" >#< ppTreeTrieKey workHdKey >#< ":" >#< (ppBracketsCommas (map (ppTreeTrieKey . fst) workTl) >-< ppBracketsCommas (map (ppTreeTrieKey . fst) $ wlScanned wl)) + >-< "workkeys" >#< ppBracketsCommas (map ppTreeTrieKey keys) + >-< "worktrie" >#< wlTrie wl + >-< "schr" >#< schr + >-< "usedin" >#< (ppBracketsCommasBlock $ map (\(k,s) -> ppKs k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl) + >-< "usedin'" >#< (ppBracketsCommasBlock $ map (\(k,s) -> ppKs k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl') + where ppKs ks = ppBracketsCommas $ map ppTreeTrieKey $ Set.toList ks +-} + put +{- + $ addStats Map.empty + [ ("chr",pp chr') + , ("leftover sz", pp (length tlMatchY)) + , ("filtered out sz", pp (length tlMatchN)) + , ("new done sz", pp (length bDone)) + , ("new todo sz", pp (length bTodo)) + , ("wl queue sz", pp (length (wlQueue wl'))) + , ("wl usedin sz", pp (Map.size (wlUsedIn wl'))) + , ("done sz", pp (Set.size (stDoneCnstrSet st'))) + , ("hist cnt", pp histCount) + ] + $ +-} + st' + expandMatch tlMatchY + + expandMatch _ + = iter + + _ -> do + put +{- + $ addStats Map.empty + [ ("no match work", ppTreeTrieKey workHdKey) + , ("wl queue sz", pp (length (wlQueue wl'))) + ] + $ +-} + st' + iter + where wl' = wl { wlScanned = workHd : wlScanned wl, wlQueue = workTl } + st' = stmatch { stWorkList = wl', stTrace = SolveDbg (ppdbg) : {- -} stTrace stmatch } + where (matches,lastQuery,ppdbg,stats) = workMatches st +{- + stmatch = addStats stats [("(a) workHd", ppTreeTrieKey workHdKey), ("(b) matches", ppBracketsCommasBlock [ s `varUpd` storedChr schr | ((schr,_),s) <- matches ])] +-} + stmatch = + (st { stCountCnstr = scntInc workHdKey "workMatched" $ stCountCnstr st + , stMatchCache = Map.insert workHdKey [] (stMatchCache st) + , stLastQuery = lastQuery + }) + _ -> do + return () + + mkStats stats new = stats `Map.union` Map.fromList (assocLMapKey showPP new) +{- + addStats stats new st = st { stTrace = SolveStats (mkStats stats new) : stTrace st } +-} + addStats _ _ st = st + + workMatches st@(SolveState {stWorkList = WorkList {wlQueue = (workHd@(workHdKey,Work {workTime = workHdTm}) : _), wlTrie = wlTrie, wlUsedIn = wlUsedIn}, stHistoryCount = histCount, stLastQuery = lastQuery}) + | isJust mbInCache = ( fromJust mbInCache + , lastQuery + , Pretty.empty, mkStats Map.empty [("cache sz",pp (Map.size (stMatchCache st)))] + ) + | otherwise = ( r5 + , foldr lqUnion lastQuery [ lqSingleton ck wks histCount | (_,(_,(ck,wks))) <- r23 ] +{- + -- , Pretty.empty + , pp2 >-< {- pp2b >-< pp2c >-< -} pp3 + , mkStats Map.empty [("(1) lookup sz",pp (length r2)), ("(2) cand sz",pp (length r3)), ("(3) unused cand sz",pp (length r4)), ("(4) final cand sz",pp (length r5))] +-} + , Pretty.empty + , Map.empty + ) + where -- cache result, if present use that, otherwise the below computation + mbInCache = Map.lookup workHdKey (stMatchCache st) + + -- results, stepwise computed for later reference in debugging output + -- basic search result + r2 :: [StoredCHR c g] -- CHRs matching workHdKey + r2 = concat -- flatten + $ TreeTrie.lookupResultToList -- convert to list + $ chrTrieLookup chrLookupHowWildAtTrie workHdKey -- lookup the store, allowing too many results + $ chrstoreTrie chrStore + + -- lookup further info in wlTrie, in particular to find out what has been done already + r23 :: [( StoredCHR c g -- the CHR + , ( [( [(CHRKey c, Work c)] -- for each CHR the list of constraints, all possible work matches + , [(CHRKey c, Work c)] + )] + , (CHRKey c, Set.Set (CHRKey c)) + ) )] + r23 = map (\c -> (c, slvCandidate workHdKey lastQuery wlTrie c)) r2 + + -- possible matches + r3, r4 + :: [( StoredCHR c g -- the matched CHR + , ( [CHRKey c] -- possible matching constraints (matching with the CHR constraints), as Keys, as Works + , [Work c] + ) )] + r3 = concatMap (\(c,cands) -> zip (repeat c) (map unzip $ slvCombine cands)) $ r23 + + -- same, but now restricted to not used earlier as indicated by the worklist + r4 = filter (not . slvIsUsedByPropPart wlUsedIn) r3 + + -- finally, the 'real' match of the 'real' constraint, yielding (by tupling) substitutions instantiating the found trie matches + r5 :: [( ( StoredCHR c g + , ( [CHRKey c] + , [Work c] + ) ) + , s + )] + r5 = mapMaybe (\r@(chr,kw@(_,works)) -> fmap (\s -> (r,s)) $ slvMatch env chr (map workCnstr works)) r4 +{- + -- debug info + pp2 = "lookups" >#< ("for" >#< ppTreeTrieKey workHdKey >-< ppBracketsCommasBlock r2) + -- pp2b = "cand1" >#< (ppBracketsCommasBlock $ map (ppBracketsCommasBlock . map (ppBracketsCommasBlock . map (\(k,w) -> ppTreeTrieKey k >#< w)) . fst . candidate) r2) + -- pp2c = "cand2" >#< (ppBracketsCommasBlock $ map (ppBracketsCommasBlock . map (ppBracketsCommasBlock) . combineToDistinguishedElts . fst . candidate) r2) + pp3 = "candidates" >#< (ppBracketsCommasBlock $ map (\(chr,(ks,ws)) -> "chr" >#< chr >-< "keys" >#< ppBracketsCommas (map ppTreeTrieKey ks) >-< "works" >#< ppBracketsCommasBlock ws) $ r3) +-} + initState st = st { stWorkList = wlInsert (stHistoryCount st) wlnew $ stWorkList st, stDoneCnstrSet = Set.unions [Set.fromList done, stDoneCnstrSet st] } + where (wlnew,done) = splitDone cnstrs + splitDone = partition cnstrRequiresSolve + +-- | Extract candidates matching a CHRKey. +-- Return a list of CHR matches, +-- each match expressed as the list of constraints (in the form of Work + Key) found in the workList wlTrie, thus giving all combis with constraints as part of a CHR, +-- partititioned on before or after last query time (to avoid work duplication later) +slvCandidate + :: (Ord (TTKey c), PP (TTKey c)) + => CHRKey c + -> LastQuery c + -> WorkTrie c + -> StoredCHR c g + -> ( [( [(CHRKey c, Work c)] + , [(CHRKey c, Work c)] + )] + , (CHRKey c, Set.Set (CHRKey c)) + ) +slvCandidate workHdKey lastQuery wlTrie (StoredCHR {storedIdent = (ck,_), storedKeys = ks, storedChr = chr}) + = ( map (maybe (lkup chrLookupHowExact workHdKey) (lkup chrLookupHowWildAtKey)) ks + , ( ck + , Set.fromList $ map (maybe workHdKey id) ks + ) ) + where lkup how k = partition (\(_,w) -> workTime w < lastQueryTm) $ map (\w -> (workKey w,w)) $ TreeTrie.lookupResultToList $ chrTrieLookup how k wlTrie + where lastQueryTm = lqLookupW k $ lqLookupC ck lastQuery +{-# INLINE slvCandidate #-} + +-} + +slvCombine :: Eq k => ([([Assoc k v], [Assoc k v])], t) -> [AssocL k v] +slvCombine ([],_) = [] +slvCombine ((lh:lt),_) + = concatMap combineToDistinguishedElts l2 + where l2 = g2 [] lh lt + where g2 ll l [] = [mk ll l []] + g2 ll l lr@(lrh:lrt) = mk ll l lr : g2 (ll ++ [l]) lrh lrt + mk ll (bef,aft) lr = map fst ll ++ [aft] ++ map cmb lr + where cmb (a,b) = a++b +{-# INLINE slvCombine #-} + +{- + +-- | Check whether the CHR propagation part of a match already has been used (i.e. propagated) earlier, +-- this to avoid duplicate propagation. +slvIsUsedByPropPart + :: (Ord k, Ord (TTKey c)) + => Map.Map (Set.Set k) (Set.Set (UsedByKey c)) + -> (StoredCHR c g, ([k], t)) + -> Bool +slvIsUsedByPropPart wlUsedIn (chr,(keys,_)) + = fnd $ drop (storedSimpSz chr) keys + where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup (Set.fromList k) wlUsedIn +{-# INLINE slvIsUsedByPropPart #-} + +-- | Match the stored CHR with a set of possible constraints, giving a substitution on success +slvMatch + :: ( CHREmptySubstitution s + , CHRMatchable env c s + , CHRCheckable env g s + , VarLookupCmb s s + ) + => env -> StoredCHR c g -> [c] -> Maybe s +slvMatch env chr cnstrs + = foldl cmb (Just chrEmptySubst) $ matches chr cnstrs ++ checks chr + where matches (StoredCHR {storedChr = Rule {ruleHead = hc}}) cnstrs + = zipWith mt hc cnstrs + where mt cFr cTo subst = chrMatchTo env subst cFr cTo + checks (StoredCHR {storedChr = Rule {ruleGuard = gd}}) + = map chk gd + where chk g subst = chrCheck env subst g + cmb (Just s) next = fmap (|+> s) $ next s + cmb _ _ = Nothing +{-# INLINE slvMatch #-} + +-} + +------------------------------------------------------------------------------------------- +--- Instances: Serialize +------------------------------------------------------------------------------------------- + +{- + +instance (Ord (TTKey c), Serialize (TTKey c), Serialize c, Serialize g) => Serialize (CHRStore c g) where + sput (CHRStore a) = sput a + sget = liftM CHRStore sget + +instance (Ord (TTKey c), Serialize (TTKey c), Serialize c, Serialize g) => Serialize (StoredCHR c g) where + sput (StoredCHR a b c d) = sput a >> sput b >> sput c >> sput d + sget = liftM4 StoredCHR sget sget sget sget + + +-} diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs @@ -0,0 +1,506 @@ +{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses #-} + +------------------------------------------------------------------------------------------- +--- CHR solver +------------------------------------------------------------------------------------------- + +{-| +Derived from work by Gerrit vd Geest, but greatly adapted to use more efficient searching. + +Assumptions (to be documented further) +- The key [Trie.TrieKey Key] used to lookup a constraint in a CHR should be distinguishing enough to be used for the prevention + of the application of a propagation rule for a 2nd time. + +This is a monomorphic Solver, i.e. the solver is polymorph but therefore can only work on 1 type of constraints, rules, etc. +-} + +module UHC.Util.CHR.Solve.TreeTrie.Mono + ( CHRStore + , emptyCHRStore + + , chrStoreFromElems + , chrStoreUnion + , chrStoreUnions + , chrStoreSingletonElem + , chrStoreToList + , chrStoreElems + + , ppCHRStore + , ppCHRStore' + + , SolveStep'(..) + , SolveStep + , SolveTrace + , ppSolveTrace + + , SolveState + , emptySolveState + , solveStateResetDone + , chrSolveStateDoneConstraints + , chrSolveStateTrace + + , IsCHRSolvable(..) + , chrSolve' + , chrSolve'' + , chrSolveM + ) + where + +import UHC.Util.CHR.Base +import UHC.Util.CHR.Key +import UHC.Util.CHR.Solve.TreeTrie.Internal +import UHC.Util.Substitutable +import UHC.Util.VarLookup +import UHC.Util.VarMp +import UHC.Util.AssocL +import UHC.Util.TreeTrie as TreeTrie +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.List as List +import Data.Typeable +import Data.Data +import Data.Maybe +import UHC.Util.Pretty as Pretty +import UHC.Util.Serialize +import Control.Monad +import Control.Monad.State.Strict +import UHC.Util.Utils + +------------------------------------------------------------------------------------------- +--- CHR store, with fast search +------------------------------------------------------------------------------------------- + +-- | A CHR as stored in a CHRStore, requiring additional info for efficiency +data StoredCHR c g + = StoredCHR + { storedChr :: !(Rule c g) -- the Rule + , storedKeyedInx :: !Int -- index of constraint for which is keyed into store + , storedKeys :: ![Maybe (CHRKey c)] -- keys of all constraints; at storedKeyedInx: Nothing + , storedIdent :: !(UsedByKey c) -- the identification of a CHR, used for propagation rules (see remark at begin) + } + deriving (Typeable) + +deriving instance (Data (TTKey c), Data c, Data g) => Data (StoredCHR c g) + +type instance TTKey (StoredCHR c g) = TTKey c + +instance (TTKeyable (Rule c g)) => TTKeyable (StoredCHR c g) where + toTTKey' o schr = toTTKey' o $ storedChr schr + +-- | The size of the simplification part of a CHR +storedSimpSz :: StoredCHR c g -> Int +storedSimpSz = ruleSimpSz . storedChr +{-# INLINE storedSimpSz #-} + +-- | A CHR store is a trie structure +newtype CHRStore cnstr guard + = CHRStore + { chrstoreTrie :: CHRTrie [StoredCHR cnstr guard] + } + deriving (Typeable) + +deriving instance (Data (TTKey cnstr), Ord (TTKey cnstr), Data cnstr, Data guard) => Data (CHRStore cnstr guard) + +mkCHRStore trie = CHRStore trie + +emptyCHRStore :: CHRStore cnstr guard +emptyCHRStore = mkCHRStore emptyCHRTrie + +-- | Combine lists of stored CHRs by concat, adapting their identification nr to be unique +cmbStoredCHRs :: [StoredCHR c g] -> [StoredCHR c g] -> [StoredCHR c g] +cmbStoredCHRs s1 s2 + = map (\s@(StoredCHR {storedIdent=(k,nr)}) -> s {storedIdent = (k,nr+l)}) s1 ++ s2 + where l = length s2 + +instance Show (StoredCHR c g) where + show _ = "StoredCHR" + +ppStoredCHR :: (PP (TTKey c), PP c, PP g) => StoredCHR c g -> PP_Doc +ppStoredCHR c@(StoredCHR {storedIdent=(idKey,idSeqNr)}) + = storedChr c + >-< indent 2 + (ppParensCommas + [ pp $ storedKeyedInx c + , pp $ storedSimpSz c + , "keys" >#< (ppBracketsCommas $ map (maybe (pp "?") ppTreeTrieKey) $ storedKeys c) + , "ident" >#< ppParensCommas [ppTreeTrieKey idKey,pp idSeqNr] + ]) + +instance (PP (TTKey c), PP c, PP g) => PP (StoredCHR c g) where + pp = ppStoredCHR + +-- | Convert from list to store +chrStoreFromElems :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => [Rule c g] -> CHRStore c g +chrStoreFromElems chrs + = mkCHRStore + $ chrTrieFromListByKeyWith cmbStoredCHRs + [ (k,[StoredCHR chr i ks' (concat ks,0)]) + | chr <- chrs + , let cs = ruleHead chr + simpSz = ruleSimpSz chr + ks = map chrToKey cs + , (c,k,i) <- zip3 cs ks [0..] + , let (ks1,(_:ks2)) = splitAt i ks + ks' = map Just ks1 ++ [Nothing] ++ map Just ks2 + ] + +chrStoreSingletonElem :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => Rule c g -> CHRStore c g +chrStoreSingletonElem x = chrStoreFromElems [x] + +chrStoreUnion :: (Ord (TTKey c)) => CHRStore c g -> CHRStore c g -> CHRStore c g +chrStoreUnion cs1 cs2 = mkCHRStore $ chrTrieUnionWith cmbStoredCHRs (chrstoreTrie cs1) (chrstoreTrie cs2) +{-# INLINE chrStoreUnion #-} + +chrStoreUnions :: (Ord (TTKey c)) => [CHRStore c g] -> CHRStore c g +chrStoreUnions [] = emptyCHRStore +chrStoreUnions [s] = s +chrStoreUnions ss = foldr1 chrStoreUnion ss +{-# INLINE chrStoreUnions #-} + +chrStoreToList :: (Ord (TTKey c)) => CHRStore c g -> [(CHRKey c,[Rule c g])] +chrStoreToList cs + = [ (k,chrs) + | (k,e) <- chrTrieToListByKey $ chrstoreTrie cs + , let chrs = [chr | (StoredCHR {storedChr = chr, storedKeyedInx = 0}) <- e] + , not $ Prelude.null chrs + ] + +chrStoreElems :: (Ord (TTKey c)) => CHRStore c g -> [Rule c g] +chrStoreElems = concatMap snd . chrStoreToList + +ppCHRStore :: (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => CHRStore c g -> PP_Doc +ppCHRStore = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrStoreToList + +ppCHRStore' :: (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => CHRStore c g -> PP_Doc +ppCHRStore' = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrTrieToListByKey . chrstoreTrie + +------------------------------------------------------------------------------------------- +--- Solver trace +------------------------------------------------------------------------------------------- + +type SolveStep c g s = SolveStep' c (Rule c g) s +type SolveTrace c g s = SolveTrace' c (Rule c g) s + +------------------------------------------------------------------------------------------- +--- Cache for maintaining which WorkKey has already had a match +------------------------------------------------------------------------------------------- + +-- type SolveMatchCache c g s = Map.Map (CHRKey c) [((StoredCHR c g,([WorkKey c],[Work c])),s)] +-- type SolveMatchCache c g s = Map.Map (WorkKey c) [((StoredCHR c g,([WorkKey c],[Work c])),s)] +type SolveMatchCache c g s = SolveMatchCache' c (StoredCHR c g) s + +------------------------------------------------------------------------------------------- +--- Solve state +------------------------------------------------------------------------------------------- + +type SolveState c g s = SolveState' c (Rule c g) (StoredCHR c g) s + +------------------------------------------------------------------------------------------- +--- Solver +------------------------------------------------------------------------------------------- + +-- | (Class alias) API for solving requirements +class ( IsCHRConstraint env c s + , IsCHRGuard env g s + , VarLookupCmb s s + , VarUpdatable s s + , CHREmptySubstitution s + , TrTrKey c ~ TTKey c + ) => IsCHRSolvable env c g s + +{- +chrSolve + :: forall env c g s . + ( IsCHRSolvable env c g s + ) + => env + -> CHRStore c g + -> [c] + -> [c] +chrSolve env chrStore cnstrs + = work ++ done + where (work, done, _ :: SolveTrace c g s) = chrSolve' env chrStore cnstrs +-} + +-- | Solve +chrSolve' + :: forall env c g s . + ( IsCHRSolvable env c g s + ) + => env + -> CHRStore c g + -> [c] + -> ([c],[c],SolveTrace c g s) +chrSolve' env chrStore cnstrs + = (wlToList (stWorkList finalState), stDoneCnstrs finalState, stTrace finalState) + where finalState = chrSolve'' env chrStore cnstrs emptySolveState + +-- | Solve +chrSolve'' + :: forall env c g s . + ( IsCHRSolvable env c g s + ) + => env + -> CHRStore c g + -> [c] + -> SolveState c g s + -> SolveState c g s +chrSolve'' env chrStore cnstrs prevState + = flip execState prevState $ chrSolveM env chrStore cnstrs + +-- | Solve +chrSolveM + :: forall env c g s . + ( IsCHRSolvable env c g s + ) + => env + -> CHRStore c g + -> [c] + -> State (SolveState c g s) () +chrSolveM env chrStore cnstrs = do + modify initState + iter +{- + modify $ + addStats Map.empty + [ ("workMatches",ppAssocLV [(ppTreeTrieKey k,pp (fromJust l)) + | (k,c) <- Map.toList $ stCountCnstr st, let l = Map.lookup "workMatched" c, isJust l]) + ] +-} + modify $ \st -> st {stMatchCache = Map.empty} + where iter = do + st <- get + case st of + (SolveState {stWorkList = wl@(WorkList {wlQueue = (workHd@(workHdKey,_) : workTl)})}) -> + case matches of + (_:_) -> do + put +{- + $ addStats Map.empty + [ ("(0) yes work", ppTreeTrieKey workHdKey) + ] + $ +-} + stmatch + expandMatch matches + where -- expandMatch :: SolveState c g s -> [((StoredCHR c g, ([WorkKey c], [Work c])), s)] -> SolveState c g s + expandMatch ( ( ( schr@(StoredCHR {storedIdent = chrId, storedChr = chr@(Rule {ruleBody = b, ruleSimpSz = simpSz})}) + , (keys,works) + ) + , subst + ) : tlMatch + ) = do + st@(SolveState {stWorkList = wl, stHistoryCount = histCount}) <- get + let (tlMatchY,tlMatchN) = partition (\(r@(_,(ks,_)),_) -> not (any (`elem` keysSimp) ks || slvIsUsedByPropPart (wlUsedIn wl') r)) tlMatch + (keysSimp,keysProp) = splitAt simpSz keys + usedIn = Map.singleton (Set.fromList keysProp) (Set.singleton chrId) + (bTodo,bDone) = splitDone $ map (varUpd subst) b + bTodo' = wlCnstrToIns wl bTodo + wl' = wlDeleteByKeyAndInsert' histCount keysSimp bTodo' + $ wl { wlUsedIn = usedIn `wlUsedInUnion` wlUsedIn wl + , wlScanned = [] + , wlQueue = wlQueue wl ++ wlScanned wl + } + st' = st { stWorkList = wl' +{- + , stTrace = SolveStep chr' subst (assocLElts bTodo') bDone : {- SolveDbg (ppwork >-< ppdbg) : -} stTrace st +-} + , stDoneCnstrSet = Set.unions [Set.fromList bDone, Set.fromList $ map workCnstr $ take simpSz works, stDoneCnstrSet st] + , stMatchCache = if List.null bTodo' then stMatchCache st else Map.empty + , stHistoryCount = histCount + 1 + } +{- + chr'= subst `varUpd` chr + ppwork = "workkey" >#< ppTreeTrieKey workHdKey >#< ":" >#< (ppBracketsCommas (map (ppTreeTrieKey . fst) workTl) >-< ppBracketsCommas (map (ppTreeTrieKey . fst) $ wlScanned wl)) + >-< "workkeys" >#< ppBracketsCommas (map ppTreeTrieKey keys) + >-< "worktrie" >#< wlTrie wl + >-< "schr" >#< schr + >-< "usedin" >#< (ppBracketsCommasBlock $ map (\(k,s) -> ppKs k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl) + >-< "usedin'" >#< (ppBracketsCommasBlock $ map (\(k,s) -> ppKs k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl') + where ppKs ks = ppBracketsCommas $ map ppTreeTrieKey $ Set.toList ks +-} + put +{- + $ addStats Map.empty + [ ("chr",pp chr') + , ("leftover sz", pp (length tlMatchY)) + , ("filtered out sz", pp (length tlMatchN)) + , ("new done sz", pp (length bDone)) + , ("new todo sz", pp (length bTodo)) + , ("wl queue sz", pp (length (wlQueue wl'))) + , ("wl usedin sz", pp (Map.size (wlUsedIn wl'))) + , ("done sz", pp (Set.size (stDoneCnstrSet st'))) + , ("hist cnt", pp histCount) + ] + $ +-} + st' + expandMatch tlMatchY + + expandMatch _ + = iter + + _ -> do + put +{- + $ addStats Map.empty + [ ("no match work", ppTreeTrieKey workHdKey) + , ("wl queue sz", pp (length (wlQueue wl'))) + ] + $ +-} + st' + iter + where wl' = wl { wlScanned = workHd : wlScanned wl, wlQueue = workTl } + st' = stmatch { stWorkList = wl', stTrace = SolveDbg (ppdbg) : {- -} stTrace stmatch } + where (matches,lastQuery,ppdbg,stats) = workMatches st +{- + stmatch = addStats stats [("(a) workHd", ppTreeTrieKey workHdKey), ("(b) matches", ppBracketsCommasBlock [ s `varUpd` storedChr schr | ((schr,_),s) <- matches ])] +-} + stmatch = + (st { stCountCnstr = scntInc workHdKey "workMatched" $ stCountCnstr st + , stMatchCache = Map.insert workHdKey [] (stMatchCache st) + , stLastQuery = lastQuery + }) + _ -> do + return () + + mkStats stats new = stats `Map.union` Map.fromList (assocLMapKey showPP new) +{- + addStats stats new st = st { stTrace = SolveStats (mkStats stats new) : stTrace st } +-} + addStats _ _ st = st + + workMatches st@(SolveState {stWorkList = WorkList {wlQueue = (workHd@(workHdKey,Work {workTime = workHdTm}) : _), wlTrie = wlTrie, wlUsedIn = wlUsedIn}, stHistoryCount = histCount, stLastQuery = lastQuery}) + | isJust mbInCache = ( fromJust mbInCache + , lastQuery + , Pretty.empty, mkStats Map.empty [("cache sz",pp (Map.size (stMatchCache st)))] + ) + | otherwise = ( r5 + , foldr lqUnion lastQuery [ lqSingleton ck wks histCount | (_,(_,(ck,wks))) <- r23 ] +{- + -- , Pretty.empty + , pp2 >-< {- pp2b >-< pp2c >-< -} pp3 + , mkStats Map.empty [("(1) lookup sz",pp (length r2)), ("(2) cand sz",pp (length r3)), ("(3) unused cand sz",pp (length r4)), ("(4) final cand sz",pp (length r5))] +-} + , Pretty.empty + , Map.empty + ) + where -- cache result, if present use that, otherwise the below computation + mbInCache = Map.lookup workHdKey (stMatchCache st) + + -- results, stepwise computed for later reference in debugging output + -- basic search result + r2 :: [StoredCHR c g] -- CHRs matching workHdKey + r2 = concat -- flatten + $ TreeTrie.lookupResultToList -- convert to list + $ chrTrieLookup chrLookupHowWildAtTrie workHdKey -- lookup the store, allowing too many results + $ chrstoreTrie chrStore + + -- lookup further info in wlTrie, in particular to find out what has been done already + r23 :: [( StoredCHR c g -- the CHR + , ( [( [(CHRKey c, Work c)] -- for each CHR the list of constraints, all possible work matches + , [(CHRKey c, Work c)] + )] + , (CHRKey c, Set.Set (CHRKey c)) + ) )] + r23 = map (\c -> (c, slvCandidate workHdKey lastQuery wlTrie c)) r2 + + -- possible matches + r3, r4 + :: [( StoredCHR c g -- the matched CHR + , ( [CHRKey c] -- possible matching constraints (matching with the CHR constraints), as Keys, as Works + , [Work c] + ) )] + r3 = concatMap (\(c,cands) -> zip (repeat c) (map unzip $ slvCombine cands)) $ r23 + + -- same, but now restricted to not used earlier as indicated by the worklist + r4 = filter (not . slvIsUsedByPropPart wlUsedIn) r3 + + -- finally, the 'real' match of the 'real' constraint, yielding (by tupling) substitutions instantiating the found trie matches + r5 :: [( ( StoredCHR c g + , ( [CHRKey c] + , [Work c] + ) ) + , s + )] + r5 = mapMaybe (\r@(chr,kw@(_,works)) -> fmap (\s -> (r,s)) $ slvMatch env chr (map workCnstr works)) r4 +{- + -- debug info + pp2 = "lookups" >#< ("for" >#< ppTreeTrieKey workHdKey >-< ppBracketsCommasBlock r2) + -- pp2b = "cand1" >#< (ppBracketsCommasBlock $ map (ppBracketsCommasBlock . map (ppBracketsCommasBlock . map (\(k,w) -> ppTreeTrieKey k >#< w)) . fst . candidate) r2) + -- pp2c = "cand2" >#< (ppBracketsCommasBlock $ map (ppBracketsCommasBlock . map (ppBracketsCommasBlock) . combineToDistinguishedElts . fst . candidate) r2) + pp3 = "candidates" >#< (ppBracketsCommasBlock $ map (\(chr,(ks,ws)) -> "chr" >#< chr >-< "keys" >#< ppBracketsCommas (map ppTreeTrieKey ks) >-< "works" >#< ppBracketsCommasBlock ws) $ r3) +-} + initState st = st { stWorkList = wlInsert (stHistoryCount st) wlnew $ stWorkList st, stDoneCnstrSet = Set.unions [Set.fromList done, stDoneCnstrSet st] } + where (wlnew,done) = splitDone cnstrs + splitDone = partition cnstrRequiresSolve + +-- | Extract candidates matching a CHRKey. +-- Return a list of CHR matches, +-- each match expressed as the list of constraints (in the form of Work + Key) found in the workList wlTrie, thus giving all combis with constraints as part of a CHR, +-- partititioned on before or after last query time (to avoid work duplication later) +slvCandidate + :: (Ord (TTKey c), PP (TTKey c)) + => CHRKey c + -> LastQuery c + -> WorkTrie c + -> StoredCHR c g + -> ( [( [(CHRKey c, Work c)] + , [(CHRKey c, Work c)] + )] + , (CHRKey c, Set.Set (CHRKey c)) + ) +slvCandidate workHdKey lastQuery wlTrie (StoredCHR {storedIdent = (ck,_), storedKeys = ks, storedChr = chr}) + = ( map (maybe (lkup chrLookupHowExact workHdKey) (lkup chrLookupHowWildAtKey)) ks + , ( ck + , Set.fromList $ map (maybe workHdKey id) ks + ) ) + where lkup how k = partition (\(_,w) -> workTime w < lastQueryTm) $ map (\w -> (workKey w,w)) $ TreeTrie.lookupResultToList $ chrTrieLookup how k wlTrie + where lastQueryTm = lqLookupW k $ lqLookupC ck lastQuery +{-# INLINE slvCandidate #-} + +-- | Check whether the CHR propagation part of a match already has been used (i.e. propagated) earlier, +-- this to avoid duplicate propagation. +slvIsUsedByPropPart + :: (Ord k, Ord (TTKey c)) + => Map.Map (Set.Set k) (Set.Set (UsedByKey c)) + -> (StoredCHR c g, ([k], t)) + -> Bool +slvIsUsedByPropPart wlUsedIn (chr,(keys,_)) + = fnd $ drop (storedSimpSz chr) keys + where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup (Set.fromList k) wlUsedIn +{-# INLINE slvIsUsedByPropPart #-} + +-- | Match the stored CHR with a set of possible constraints, giving a substitution on success +slvMatch + :: ( CHREmptySubstitution s + , CHRMatchable env c s + , CHRCheckable env g s + , VarLookupCmb s s + ) + => env -> StoredCHR c g -> [c] -> Maybe s +slvMatch env chr cnstrs + = foldl cmb (Just chrEmptySubst) $ matches chr cnstrs ++ checks chr + where matches (StoredCHR {storedChr = Rule {ruleHead = hc}}) cnstrs + = zipWith mt hc cnstrs + where mt cFr cTo subst = chrMatchTo env subst cFr cTo + checks (StoredCHR {storedChr = Rule {ruleGuard = gd}}) + = map chk gd + where chk g subst = chrCheck env subst g + cmb (Just s) next = fmap (|+> s) $ next s + cmb _ _ = Nothing +{-# INLINE slvMatch #-} + +------------------------------------------------------------------------------------------- +--- Instances: Serialize +------------------------------------------------------------------------------------------- + +instance (Ord (TTKey c), Serialize (TTKey c), Serialize c, Serialize g) => Serialize (CHRStore c g) where + sput (CHRStore a) = sput a + sget = liftM CHRStore sget + +instance (Serialize c, Serialize g, Serialize (TTKey c)) => Serialize (StoredCHR c g) where + sput (StoredCHR a b c d) = sput a >> sput b >> sput c >> sput d + sget = liftM4 StoredCHR sget sget sget sget + diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Poly.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Poly.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Poly.hs @@ -0,0 +1,506 @@ +{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses #-} + +------------------------------------------------------------------------------------------- +--- CHR solver +------------------------------------------------------------------------------------------- + +{-| +Derived from work by Gerrit vd Geest, but greatly adapted to use more efficient searching. + +Assumptions (to be documented further) +- The key [Trie.TrieKey Key] used to lookup a constraint in a CHR should be distinguishing enough to be used for the prevention + of the application of a propagation rule for a 2nd time. + +This is a polymorphic Solver, i.e. the solver is unaware of the type of constraints, rules, etc. because of this type hidden existentially. +Tying stuff together is now done by phantom types for environment and substitution, instantiated/relevant only when solving. +-} + +module UHC.Util.CHR.Solve.TreeTrie.Poly + ( + CHRStore + , emptyCHRStore + + , chrStoreFromElems + , chrStoreSingletonElem + , chrStoreUnion + , chrStoreUnions + , chrStoreToList + , chrStoreElems + + , ppCHRStore + , ppCHRStore' + + , SolveStep'(..) + , SolveStep + , SolveTrace + , ppSolveTrace + + , SolveState + , emptySolveState + , solveStateResetDone + , chrSolveStateDoneConstraints + , chrSolveStateTrace + + , IsCHRSolvable(..) + , chrSolve' + , chrSolve'' + , chrSolveM + ) + where + +import UHC.Util.CHR.Base +import UHC.Util.CHR.Key +import UHC.Util.CHR.Solve.TreeTrie.Internal +import UHC.Util.Substitutable +import UHC.Util.VarLookup +import UHC.Util.VarMp +import UHC.Util.AssocL +import UHC.Util.TreeTrie as TreeTrie +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.List as List +import Data.Typeable +import Data.Data +import Data.Maybe +import UHC.Util.Pretty as Pretty +import UHC.Util.Serialize +import Control.Monad +import Control.Monad.State.Strict +import UHC.Util.Utils + +------------------------------------------------------------------------------------------- +--- CHR store, with fast search +------------------------------------------------------------------------------------------- + +-- | A CHR as stored in a CHRStore, requiring additional info for efficiency +data StoredCHR e s + = StoredCHR + { storedChr :: !(CHRRule e s) -- the Rule + , storedKeyedInx :: !Int -- index of constraint for which is keyed into store + , storedKeys :: ![Maybe (CHRKey (CHRConstraint e s))] -- keys of all constraints; at storedKeyedInx: Nothing + , storedIdent :: !(UsedByKey (CHRConstraint e s)) -- the identification of a CHR, used for propagation rules (see remark at begin) + } + deriving (Typeable) + +deriving instance (Data (TTKey (CHRConstraint e s)), Data (CHRRule e s), Data e, Data s) => Data (StoredCHR e s) + +type instance TTKey (StoredCHR e s) = TTKey (CHRRule e s) + +instance (TTKeyable (CHRRule e s)) => TTKeyable (StoredCHR e s) where + toTTKey' o schr = toTTKey' o $ storedChr schr + +-- | The size of the simplification part of a CHR +storedSimpSz :: StoredCHR e s -> Int +storedSimpSz = ruleSimpSz . chrRule . storedChr +{-# INLINE storedSimpSz #-} + +-- | A CHR store is a trie structure +newtype CHRStore e s + = CHRStore + { chrstoreTrie :: CHRTrie [StoredCHR e s] + } + deriving (Typeable) + +deriving instance (Ord (TTKey (CHRRule e s)), Data e, Data s, Data (TTKey (CHRRule e s)), Data (TTKey (CHRConstraint e s)), Data (CHRRule e s)) => Data (CHRStore e s) + +mkCHRStore trie = CHRStore trie + +emptyCHRStore :: CHRStore cnstr guard +emptyCHRStore = mkCHRStore emptyCHRTrie + +-- | Combine lists of stored CHRs by concat, adapting their identification nr to be unique +cmbStoredCHRs :: [StoredCHR e s] -> [StoredCHR e s] -> [StoredCHR e s] +cmbStoredCHRs s1 s2 + = map (\s@(StoredCHR {storedIdent=(k,nr)}) -> s {storedIdent = (k,nr+l)}) s1 ++ s2 + where l = length s2 + +instance Show (StoredCHR e s) where + show _ = "StoredCHR" + +ppStoredCHR :: (PP (TTKey (CHRConstraint e s))) => StoredCHR e s -> PP_Doc +ppStoredCHR c@(StoredCHR {storedIdent=(idKey,idSeqNr)}) + = storedChr c + >-< indent 2 + (ppParensCommas + [ pp $ storedKeyedInx c + , pp $ storedSimpSz c + , "keys" >#< (ppBracketsCommas $ map (maybe (pp "?") ppTreeTrieKey) $ storedKeys c) + , "ident" >#< ppParensCommas [ppTreeTrieKey idKey,pp idSeqNr] + ]) + +instance (PP (TTKey (CHRConstraint e s))) => PP (StoredCHR e s) where + pp = ppStoredCHR + +-- | Convert from list to store +chrStoreFromElems + :: (Ord (TTKey (CHRConstraint e s)), TTKey (CHRConstraint e s) ~ TrTrKey (CHRConstraint e s)) + => [CHRRule e s] + -> CHRStore e s +chrStoreFromElems cruls + = mkCHRStore + $ chrTrieFromListByKeyWith cmbStoredCHRs + [ (k,[StoredCHR crul i ks' (concat ks,0)]) + | crul@(CHRRule rul) <- cruls + , let cs = ruleHead rul + simpSz = ruleSimpSz rul + ks = map chrToKey cs + , (c,k,i) <- zip3 cs ks [0..] + , let (ks1,(_:ks2)) = splitAt i ks + ks' = map Just ks1 ++ [Nothing] ++ map Just ks2 + ] + + +chrStoreSingletonElem + :: (Ord (TTKey (CHRConstraint e s)), TTKey (CHRConstraint e s) ~ TrTrKey (CHRConstraint e s)) + => CHRRule e s + -> CHRStore e s +chrStoreSingletonElem x = chrStoreFromElems [x] + +chrStoreUnion :: (Ord (TTKey (CHRConstraint e s))) => CHRStore e s -> CHRStore e s -> CHRStore e s +chrStoreUnion cs1 cs2 = mkCHRStore $ chrTrieUnionWith cmbStoredCHRs (chrstoreTrie cs1) (chrstoreTrie cs2) +{-# INLINE chrStoreUnion #-} + +chrStoreUnions :: (Ord (TTKey (CHRConstraint e s))) => [CHRStore e s] -> CHRStore e s +chrStoreUnions [] = emptyCHRStore +chrStoreUnions [s] = s +chrStoreUnions ss = foldr1 chrStoreUnion ss +{-# INLINE chrStoreUnions #-} + +chrStoreToList :: (Ord (TTKey (CHRConstraint e s))) => CHRStore e s -> [(CHRKey (CHRConstraint e s),[CHRRule e s])] +chrStoreToList cs + = [ (k,chrs) + | (k,e) <- chrTrieToListByKey $ chrstoreTrie cs + , let chrs = [chr | (StoredCHR {storedChr = chr, storedKeyedInx = 0}) <- e] + , not $ Prelude.null chrs + ] + +chrStoreElems :: (Ord (TTKey (CHRConstraint e s))) => CHRStore e s -> [CHRRule e s] +chrStoreElems = concatMap snd . chrStoreToList + +ppCHRStore :: (PP (TTKey (CHRConstraint e s)), Ord (TTKey (CHRConstraint e s))) => {- (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => -} CHRStore e s -> PP_Doc +ppCHRStore = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrStoreToList + +ppCHRStore' :: (PP (TTKey (CHRConstraint e s)), Ord (TTKey (CHRConstraint e s))) => CHRStore e s -> PP_Doc +ppCHRStore' = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrTrieToListByKey . chrstoreTrie + +------------------------------------------------------------------------------------------- +--- Solver trace +------------------------------------------------------------------------------------------- + +type SolveStep e s = SolveStep' (CHRConstraint e s) (CHRRule e s) s +type SolveTrace e s = SolveTrace' (CHRConstraint e s) (CHRRule e s) s + +------------------------------------------------------------------------------------------- +--- Cache for maintaining which WorkKey has already had a match +------------------------------------------------------------------------------------------- + +type SolveMatchCache e s = SolveMatchCache' (CHRConstraint e s) (StoredCHR e s) s + +------------------------------------------------------------------------------------------- +--- Solve state +------------------------------------------------------------------------------------------- + +type SolveState e s = SolveState' (CHRConstraint e s) (CHRRule e s) (StoredCHR e s) s + +------------------------------------------------------------------------------------------- +--- Solver +------------------------------------------------------------------------------------------- + + +-- | (Class alias) API for solving requirements +class ( VarLookupCmb s s + , VarUpdatable s s + , CHREmptySubstitution s + , TrTrKey (CHRConstraint e s) ~ TTKey (CHRConstraint e s) + , CHRMatchableKey s ~ TrTrKey (CHRConstraint e s) + , PP (CHRMatchableKey s) + , Ord (CHRMatchableKey s) + ) => IsCHRSolvable e s + +-- | Solve +chrSolve' + :: forall e c s . + ( IsCHRSolvable e s + , c ~ CHRConstraint e s + ) + => e + -> CHRStore e s + -> [c] + -> ([c],[c],SolveTrace e s) +chrSolve' env chrStore cnstrs + = (wlToList (stWorkList finalState), stDoneCnstrs finalState, stTrace finalState) + where finalState = chrSolve'' env chrStore cnstrs emptySolveState + +-- | Solve +chrSolve'' + :: forall e c s . + ( IsCHRSolvable e s + , c ~ CHRConstraint e s + ) + => e + -> CHRStore e s + -> [c] + -> SolveState e s + -> SolveState e s +chrSolve'' env chrStore cnstrs prevState + = flip execState prevState $ chrSolveM env chrStore cnstrs + + +-- | Solve +chrSolveM + :: forall e c s . + ( IsCHRSolvable e s + , c ~ CHRConstraint e s + ) + => e + -> CHRStore e s + -> [c] + -> State (SolveState e s) () +chrSolveM env chrStore cnstrs = do + modify initState + iter +{- + modify $ + addStats Map.empty + [ ("workMatches",ppAssocLV [(ppTreeTrieKey k,pp (fromJust l)) + | (k,c) <- Map.toList $ stCountCnstr st, let l = Map.lookup "workMatched" c, isJust l]) + ] +-} + modify $ \st -> st {stMatchCache = Map.empty} + where iter = do + st <- get + case st of + (SolveState {stWorkList = wl@(WorkList {wlQueue = (workHd@(workHdKey,_) : workTl)})}) -> + case matches of + (_:_) -> do + put +{- + $ addStats Map.empty + [ ("(0) yes work", ppTreeTrieKey workHdKey) + ] + $ +-} + stmatch + expandMatch matches + where -- expandMatch :: SolveState e s -> [((StoredCHR e s, ([WorkKey c], [Work c])), s)] -> SolveState e s + expandMatch ( ( ( schr@(StoredCHR {storedIdent = chrId, storedChr = chr@(CHRRule {chrRule = Rule {ruleBody = b, ruleSimpSz = simpSz}})}) + , (keys,works) + ) + , subst + ) : tlMatch + ) = do + st@(SolveState {stWorkList = wl, stHistoryCount = histCount}) <- get + let (tlMatchY,tlMatchN) = partition (\(r@(_,(ks,_)),_) -> not (any (`elem` keysSimp) ks || slvIsUsedByPropPart (wlUsedIn wl') r)) tlMatch + (keysSimp,keysProp) = splitAt simpSz keys + usedIn = Map.singleton (Set.fromList keysProp) (Set.singleton chrId) + (bTodo,bDone) = splitDone $ map (varUpd subst) b + bTodo' = wlCnstrToIns wl bTodo + wl' = wlDeleteByKeyAndInsert' histCount keysSimp bTodo' + $ wl { wlUsedIn = usedIn `wlUsedInUnion` wlUsedIn wl + , wlScanned = [] + , wlQueue = wlQueue wl ++ wlScanned wl + } + st' = st { stWorkList = wl' +{- + , stTrace = SolveStep chr' subst (assocLElts bTodo') bDone : {- SolveDbg (ppwork >-< ppdbg) : -} stTrace st +-} + , stDoneCnstrSet = Set.unions [Set.fromList bDone, Set.fromList $ map workCnstr $ take simpSz works, stDoneCnstrSet st] + , stMatchCache = if List.null bTodo' then stMatchCache st else Map.empty + , stHistoryCount = histCount + 1 + } +{- + chr'= subst `varUpd` chr + ppwork = "workkey" >#< ppTreeTrieKey workHdKey >#< ":" >#< (ppBracketsCommas (map (ppTreeTrieKey . fst) workTl) >-< ppBracketsCommas (map (ppTreeTrieKey . fst) $ wlScanned wl)) + >-< "workkeys" >#< ppBracketsCommas (map ppTreeTrieKey keys) + >-< "worktrie" >#< wlTrie wl + >-< "schr" >#< schr + >-< "usedin" >#< (ppBracketsCommasBlock $ map (\(k,s) -> ppKs k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl) + >-< "usedin'" >#< (ppBracketsCommasBlock $ map (\(k,s) -> ppKs k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl') + where ppKs ks = ppBracketsCommas $ map ppTreeTrieKey $ Set.toList ks +-} + put +{- + $ addStats Map.empty + [ ("chr",pp chr') + , ("leftover sz", pp (length tlMatchY)) + , ("filtered out sz", pp (length tlMatchN)) + , ("new done sz", pp (length bDone)) + , ("new todo sz", pp (length bTodo)) + , ("wl queue sz", pp (length (wlQueue wl'))) + , ("wl usedin sz", pp (Map.size (wlUsedIn wl'))) + , ("done sz", pp (Set.size (stDoneCnstrSet st'))) + , ("hist cnt", pp histCount) + ] + $ +-} + st' + expandMatch tlMatchY + + expandMatch _ + = iter + + _ -> do + put +{- + $ addStats Map.empty + [ ("no match work", ppTreeTrieKey workHdKey) + , ("wl queue sz", pp (length (wlQueue wl'))) + ] + $ +-} + st' + iter + where wl' = wl { wlScanned = workHd : wlScanned wl, wlQueue = workTl } + st' = stmatch { stWorkList = wl', stTrace = SolveDbg (ppdbg) : {- -} stTrace stmatch } + where (matches,lastQuery,ppdbg,stats) = workMatches st +{- + stmatch = addStats stats [("(a) workHd", ppTreeTrieKey workHdKey), ("(b) matches", ppBracketsCommasBlock [ s `varUpd` storedChr schr | ((schr,_),s) <- matches ])] +-} + stmatch = + (st { stCountCnstr = scntInc workHdKey "workMatched" $ stCountCnstr st + , stMatchCache = Map.insert workHdKey [] (stMatchCache st) + , stLastQuery = lastQuery + }) + _ -> do + return () + + mkStats stats new = stats `Map.union` Map.fromList (assocLMapKey showPP new) +{- + addStats stats new st = st { stTrace = SolveStats (mkStats stats new) : stTrace st } +-} + addStats _ _ st = st + + workMatches st@(SolveState {stWorkList = WorkList {wlQueue = (workHd@(workHdKey,Work {workTime = workHdTm}) : _), wlTrie = wlTrie, wlUsedIn = wlUsedIn}, stHistoryCount = histCount, stLastQuery = lastQuery}) + | isJust mbInCache = ( fromJust mbInCache + , lastQuery + , Pretty.empty, mkStats Map.empty [("cache sz",pp (Map.size (stMatchCache st)))] + ) + | otherwise = ( r5 + , foldr lqUnion lastQuery [ lqSingleton ck wks histCount | (_,(_,(ck,wks))) <- r23 ] +{- + -- , Pretty.empty + , pp2 >-< {- pp2b >-< pp2c >-< -} pp3 + , mkStats Map.empty [("(1) lookup sz",pp (length r2)), ("(2) cand sz",pp (length r3)), ("(3) unused cand sz",pp (length r4)), ("(4) final cand sz",pp (length r5))] +-} + , Pretty.empty + , Map.empty + ) + where -- cache result, if present use that, otherwise the below computation + mbInCache = Map.lookup workHdKey (stMatchCache st) + + -- results, stepwise computed for later reference in debugging output + -- basic search result + r2 :: [StoredCHR e s] -- CHRs matching workHdKey + r2 = concat -- flatten + $ TreeTrie.lookupResultToList -- convert to list + $ chrTrieLookup chrLookupHowWildAtTrie workHdKey -- lookup the store, allowing too many results + $ chrstoreTrie chrStore + + -- lookup further info in wlTrie, in particular to find out what has been done already + r23 :: [( StoredCHR e s -- the CHR + , ( [( [(CHRKey c, Work c)] -- for each CHR the list of constraints, all possible work matches + , [(CHRKey c, Work c)] + )] + , (CHRKey c, Set.Set (CHRKey c)) + ) )] + r23 = map (\c -> (c, slvCandidate workHdKey lastQuery wlTrie c)) r2 + + -- possible matches + r3, r4 + :: [( StoredCHR e s -- the matched CHR + , ( [CHRKey c] -- possible matching constraints (matching with the CHR constraints), as Keys, as Works + , [Work c] + ) )] + r3 = concatMap (\(c,cands) -> zip (repeat c) (map unzip $ slvCombine cands)) $ r23 + + -- same, but now restricted to not used earlier as indicated by the worklist + r4 = filter (not . slvIsUsedByPropPart wlUsedIn) r3 + + -- finally, the 'real' match of the 'real' constraint, yielding (by tupling) substitutions instantiating the found trie matches + r5 :: [( ( StoredCHR e s + , ( [CHRKey c] + , [Work c] + ) ) + , s + )] + r5 = mapMaybe (\r@(chr,kw@(_,works)) -> fmap (\s -> (r,s)) $ slvMatch env chr (map workCnstr works)) r4 +{- + -- debug info + pp2 = "lookups" >#< ("for" >#< ppTreeTrieKey workHdKey >-< ppBracketsCommasBlock r2) + -- pp2b = "cand1" >#< (ppBracketsCommasBlock $ map (ppBracketsCommasBlock . map (ppBracketsCommasBlock . map (\(k,w) -> ppTreeTrieKey k >#< w)) . fst . candidate) r2) + -- pp2c = "cand2" >#< (ppBracketsCommasBlock $ map (ppBracketsCommasBlock . map (ppBracketsCommasBlock) . combineToDistinguishedElts . fst . candidate) r2) + pp3 = "candidates" >#< (ppBracketsCommasBlock $ map (\(chr,(ks,ws)) -> "chr" >#< chr >-< "keys" >#< ppBracketsCommas (map ppTreeTrieKey ks) >-< "works" >#< ppBracketsCommasBlock ws) $ r3) +-} + initState st = st { stWorkList = wlInsert (stHistoryCount st) wlnew $ stWorkList st, stDoneCnstrSet = Set.unions [Set.fromList done, stDoneCnstrSet st] } + where (wlnew,done) = splitDone cnstrs + splitDone = partition cnstrRequiresSolve +{- -} + +-- | Extract candidates matching a CHRKey. +-- Return a list of CHR matches, +-- each match expressed as the list of constraints (in the form of Work + Key) found in the workList wlTrie, thus giving all combis with constraints as part of a CHR, +-- partititioned on before or after last query time (to avoid work duplication later) +slvCandidate + :: (Ord (TTKey c), PP (TTKey c), c ~ CHRConstraint e s) + => CHRKey c + -> LastQuery c + -> WorkTrie c + -> StoredCHR e s + -> ( [( [(CHRKey c, Work c)] + , [(CHRKey c, Work c)] + )] + , (CHRKey c, Set.Set (CHRKey c)) + ) +slvCandidate workHdKey lastQuery wlTrie (StoredCHR {storedIdent = (ck,_), storedKeys = ks, storedChr = chr}) + = ( map (maybe (lkup chrLookupHowExact workHdKey) (lkup chrLookupHowWildAtKey)) ks + , ( ck + , Set.fromList $ map (maybe workHdKey id) ks + ) ) + where lkup how k = partition (\(_,w) -> workTime w < lastQueryTm) $ map (\w -> (workKey w,w)) $ TreeTrie.lookupResultToList $ chrTrieLookup how k wlTrie + where lastQueryTm = lqLookupW k $ lqLookupC ck lastQuery +{-# INLINE slvCandidate #-} + + +-- | Check whether the CHR propagation part of a match already has been used (i.e. propagated) earlier, +-- this to avoid duplicate propagation. +slvIsUsedByPropPart + :: (Ord k, Ord (TTKey c), c ~ CHRConstraint e s) + => Map.Map (Set.Set k) (Set.Set (UsedByKey c)) + -> (StoredCHR e s, ([k], t)) + -> Bool +slvIsUsedByPropPart wlUsedIn (chr,(keys,_)) + = fnd $ drop (storedSimpSz chr) keys + where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup (Set.fromList k) wlUsedIn +{-# INLINE slvIsUsedByPropPart #-} + +-- | Match the stored CHR with a set of possible constraints, giving a substitution on success +slvMatch + :: ( IsCHRSolvable e s + ) + => e -> StoredCHR e s -> [CHRConstraint e s] -> Maybe s +slvMatch env chr cnstrs + = foldl cmb (Just chrEmptySubst) $ matches chr cnstrs ++ checks chr + where matches (StoredCHR {storedChr = CHRRule { chrRule = Rule {ruleHead = hc}}}) cnstrs + = zipWith mt hc cnstrs + where mt cFr cTo subst = chrMatchTo env subst cFr cTo + checks (StoredCHR {storedChr = CHRRule { chrRule = Rule {ruleGuard = gd}}}) + = map chk gd + where chk g subst = chrCheck env subst g + cmb (Just s) next = fmap (|+> s) $ next s + cmb _ _ = Nothing +{-# INLINE slvMatch #-} + + +------------------------------------------------------------------------------------------- +--- Instances: Serialize +------------------------------------------------------------------------------------------- + +instance (Ord (TTKey (CHRConstraint e s)), Serialize (TTKey (CHRConstraint e s)), Serialize (CHRRule e s)) => Serialize (CHRStore e s) where + sput (CHRStore a) = sput a + sget = liftM CHRStore sget + +instance (Serialize (CHRRule e s), Serialize (TTKey (CHRConstraint e s))) => Serialize (StoredCHR e s) where + sput (StoredCHR a b c d) = sput a >> sput b >> sput c >> sput d + sget = liftM4 StoredCHR sget sget sget sget + + diff --git a/src/UHC/Util/Pretty.hs b/src/UHC/Util/Pretty.hs --- a/src/UHC/Util/Pretty.hs +++ b/src/UHC/Util/Pretty.hs @@ -73,6 +73,9 @@ -- * Misc , ppDots, ppMb, ppUnless, ppWhen + -- * Render + , showPP + -- * IO , hPutWidthPPLn, putWidthPPLn , hPutPPLn, putPPLn @@ -447,6 +450,13 @@ instance (PP a, PP b, PP c, PP d, PP e, PP f, PP g, PP h, PP i, PP j) => PP (a,b,c,d,e,f,g,h,i,j) where pp (a,b,c,d,e,f,g,h,i,j) = ppParensCommasBlock [a,b,c,d,e,f,g,h,i,j] -} + +------------------------------------------------------------------------- +-- Render +------------------------------------------------------------------------- + +showPP :: PP a => a -> String +showPP x = disp (pp x) 1000 "" ------------------------------------------------------------------------- -- PP printing to file diff --git a/src/UHC/Util/PrettySimple.hs b/src/UHC/Util/PrettySimple.hs --- a/src/UHC/Util/PrettySimple.hs +++ b/src/UHC/Util/PrettySimple.hs @@ -28,6 +28,8 @@ where import System.IO +import Data.Data +import Data.Typeable ------------------------------------------------------------------------- -- Doc structure @@ -38,6 +40,7 @@ { cchEmp :: !Bool -- ^ is it empty , cchSng :: !Bool -- ^ is it a single line } + deriving (Typeable, Data) -- | Doc structure data Doc @@ -46,6 +49,7 @@ | Hor !Cached !Doc !Doc -- horizontal positioning | Ver !Cached !Doc !Doc -- vertical positioning | Ind !Int !Doc -- indent + deriving (Typeable, Data) type PP_Doc = Doc diff --git a/src/UHC/Util/RLList.hs b/src/UHC/Util/RLList.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/RLList.hs @@ -0,0 +1,130 @@ +{-# LANGUAGE CPP, StandaloneDeriving #-} + +------------------------------------------------------------------------------------------- +--- Run length encoded list, to be used as an identification of scope in UHC +------------------------------------------------------------------------------------------- + +module UHC.Util.RLList + ( -- * Run length list + RLList(..) + , concat, singleton, empty, toList, fromList + + -- * Predicates, observations + , length, null + , isPrefixOf + + -- * Misc + , inits, init, initLast + , headTail + ) + where + +import Prelude hiding (length, init, null, concat) +import qualified Prelude as P +import Data.Maybe +import qualified Data.List as L +import Data.List hiding (concat, init, null, isPrefixOf, length, inits) +import Control.Monad +import UHC.Util.Utils +import UHC.Util.Binary +import UHC.Util.Serialize + +------------------------------------------------------------------------------------------- +--- Run length encoded list +------------------------------------------------------------------------------------------- + +newtype RLList a + = RLList { unRLList :: [(a,Int)] } + deriving (Eq) + +instance Ord a => Ord (RLList a) where + (RLList []) `compare` (RLList []) = EQ + (RLList []) `compare` (RLList _ ) = LT + (RLList _ ) `compare` (RLList []) = GT + (RLList ((x1,c1):l1)) `compare` (RLList ((x2,c2):l2)) | x1 == x2 = if c1 == c2 + then RLList l1 `compare` RLList l2 + else c1 `compare` c2 + | x1 < x2 = LT + | x1 > x2 = GT + +instance Show a => Show (RLList a) where + show = show . toList + +concat :: Eq a => RLList a -> RLList a -> RLList a +concat (RLList []) rll2 = rll2 +concat rll1 (RLList []) = rll1 +concat (RLList l1) (RLList l2@(h2@(x2,c2):t2)) + | x1 == x2 = RLList (h1 ++ [(x1,c1+c2)] ++ t2) + | otherwise = RLList (l1 ++ l2) + where (h1,t1@(x1,c1)) = fromJust (initlast l1) + +empty :: RLList a +empty = RLList [] + +singleton :: a -> RLList a +singleton x = RLList [(x,1)] + +toList :: RLList a -> [a] +toList (RLList l) = concatMap (\(x,c) -> replicate c x) l + +fromList :: Eq a => [a] -> RLList a +fromList l = RLList [ (x,L.length g) | g@(x:_) <- group l ] + +length :: RLList a -> Int +length (RLList l) = sum $ map snd l + +null :: RLList a -> Bool +null (RLList []) = True +null (RLList _ ) = False + +isPrefixOf :: Eq a => RLList a -> RLList a -> Bool +isPrefixOf (RLList []) _ = True +isPrefixOf _ (RLList []) = False +isPrefixOf (RLList ((x1,c1):l1)) (RLList ((x2,c2):l2)) + | x1 == x2 = if c1 < c2 + then True + else if c1 > c2 + then False + else isPrefixOf (RLList l1) (RLList l2) + | otherwise = False + +------------------------------------------------------------------------------------------- +--- Misc +------------------------------------------------------------------------------------------- + +initLast :: Eq a => RLList a -> Maybe (RLList a,a) +initLast (RLList l ) = il [] l + where il acc [(x,1)] = Just (RLList (reverse acc),x) + il acc [(x,c)] = Just (RLList (reverse ((x,c-1):acc)),x) + il acc (a:as) = il (a:acc) as + il _ _ = Nothing + +init :: Eq a => RLList a -> RLList a +init = fst . fromJust . initLast + +inits :: Eq a => RLList a -> [RLList a] +inits = map fromList . L.inits . toList + +headTail :: RLList a -> Maybe (a,RLList a) +headTail (RLList []) = Nothing +headTail (RLList ((x,1):t)) = Just (x,RLList t) +headTail (RLList ((x,c):t)) = Just (x,RLList ((x,c-1):t)) + +------------------------------------------------------------------------------------------- +--- Instances: Typeable, Data +------------------------------------------------------------------------------------------- + +#if __GLASGOW_HASKELL__ >= 708 +deriving instance Typeable RLList +#else +deriving instance Typeable1 RLList +#endif +deriving instance Data x => Data (RLList x) + +------------------------------------------------------------------------------------------- +--- Instances: Binary, Serialize +------------------------------------------------------------------------------------------- + +instance Binary a => Binary (RLList a) where + put (RLList a) = put a + get = liftM RLList get diff --git a/src/UHC/Util/Serialize.hs b/src/UHC/Util/Serialize.hs --- a/src/UHC/Util/Serialize.hs +++ b/src/UHC/Util/Serialize.hs @@ -98,6 +98,7 @@ import System.IO (openBinaryFile) import UHC.Util.Utils import Data.Typeable +import Data.Typeable.Internal import qualified Data.Map as Map import qualified Data.Set as Set -- import qualified UHC.Utils.RelMap as RelMap @@ -374,6 +375,15 @@ instance Serialize Int16 where sput = sputPlain sget = sgetPlain + +instance Serialize TyCon where + sput tc = sput (tyConPackage tc) >> sput (tyConModule tc) >> sput (tyConName tc) + sget = liftM3 mkTyCon3 sget sget sget + +instance Serialize TypeRep where + sput tr = sput tc >> sput ka >> sput ta + where (tc,ka,ta) = splitPolyTyConApp tr + sget = liftM3 mkPolyTyConApp sget sget sget {- instance Serialize String where diff --git a/src/UHC/Util/Substitutable.hs b/src/UHC/Util/Substitutable.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/Substitutable.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} + +module UHC.Util.Substitutable + ( + VarUpdatable(..) + , VarExtractable(..) + + , SubstVarKey + , SubstVarVal + , ExtrValVarKey + ) + where + +import qualified Data.Set as Set +import UHC.Util.VarMp + +------------------------------------------------------------------------------------------- +--- Substitutable classes +------------------------------------------------------------------------------------------- + +infixr 6 `varUpd` +infixr 6 `varUpdCyc` + +-- | Invariant: SubstVarKey subst = ExtrValVarKey (SubstVarVal subst) +type family SubstVarKey subst :: * +type family SubstVarVal subst :: * +type family ExtrValVarKey vv :: * + +type instance ExtrValVarKey [vv] = ExtrValVarKey vv + +class VarUpdatable vv subst where -- skey sval | subst -> skey sval where + varUpd :: subst -> vv -> vv + varUpdCyc :: subst -> vv -> (vv, VarMp' (SubstVarKey subst) (SubstVarVal subst)) + s `varUpdCyc` x = (s `varUpd` x,emptyVarMp) + +class Ord (ExtrValVarKey vv) => VarExtractable vv where -- k | vv -> k where + varFree :: vv -> [ExtrValVarKey vv] + varFreeSet :: vv -> Set.Set (ExtrValVarKey vv) + + -- default + varFree = Set.toList . varFreeSet + varFreeSet = Set.fromList . varFree + diff --git a/src/UHC/Util/TreeTrie.hs b/src/UHC/Util/TreeTrie.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/TreeTrie.hs @@ -0,0 +1,686 @@ +{-# LANGUAGE CPP, ScopedTypeVariables, StandaloneDeriving, TypeFamilies, MultiParamTypeClasses #-} + +------------------------------------------------------------------------------------------- +--- TreeTrie, variation which allows matching on subtrees marked as a variable (kind of unification) +------------------------------------------------------------------------------------------- + +{- | +A TreeTrie is a search structure where the key actually consists of a +tree of keys, represented as a list of layers in the tree, 1 for every +depth, starting at the top, which are iteratively used for searching. +The search structure for common path/prefixes is shared, the trie +branches to multiple corresponding to available children, length +equality of children is used in searching (should match) + +The TreeTrie structure implemented in this module deviates from the +usual TreeTrie implementations in that it allows wildcard matches +besides the normal full match. The objective is to also be able to +retrieve values for which (at insertion time) it has been indicated that +part does not need full matching. This intentionally is similar to +unification, where matching on a variable will succeed for arbitrary +values. Unification is not the job of this TreeTrie implementation, but +by returning partial matches as well, a list of possible match +candidates is returned. +-} + +module UHC.Util.TreeTrie + ( -- * Key into TreeTrie + TreeTrie1Key(..) + , TreeTrieMp1Key(..) + , TreeTrieMpKey + , TreeTrieKey + + , TrTrKey + + , ppTreeTrieKey + + , ttkSingleton + , ttkAdd', ttkAdd + , ttkChildren + , ttkFixate + + , ttkParentChildren + + -- * Keyable + , TreeTrieKeyable(..) + + -- * TreeTrie + , TreeTrie + , emptyTreeTrie + , empty + , toListByKey, toList + , fromListByKeyWith, fromList + + -- * Lookup + , TreeTrieLookup(..) + + , lookupPartialByKey + , lookupPartialByKey' + , lookupByKey + , lookup + , lookupResultToList + + -- * Properties/observations + , isEmpty, null + , elems + + -- * Construction + , singleton, singletonKeyable + , unionWith, union, unionsWith, unions + , insertByKeyWith, insertByKey + + -- * Deletion + , deleteByKey, delete + , deleteListByKey + ) + where + +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.Maybe +import Prelude hiding (lookup,null) +import qualified UHC.Util.FastSeq as Seq +import qualified Data.List as List +import UHC.Util.Utils +import UHC.Util.Pretty hiding (empty) +import qualified UHC.Util.Pretty as PP +import Control.Monad +import Data.Typeable(Typeable) +import Data.Generics(Data) +import UHC.Util.Serialize + +------------------------------------------------------------------------------------------- +--- Key into TreeTrie +------------------------------------------------------------------------------------------- + +-- | Both key and trie can allow partial matching, indicated by TreeTrie1Key +data TreeTrie1Key k + = TT1K_One !k + | TT1K_Any -- used to wildcard match a single node in a tree + deriving (Eq, Ord) + +-- | A key in a layer of TreeTrieMpKey +data TreeTrieMp1Key k + = TTM1K [TreeTrie1Key k] + | TTM1K_Any -- used to wildcard match multiple children, internal only + deriving (Eq, Ord) + +-- | The key into a map used internally by the trie +type TreeTrieMpKey k + = [TreeTrieMp1Key k] + +-- | The key used externally to index into a trie +type TreeTrieKey k + = [TreeTrieMpKey k] + +#if __GLASGOW_HASKELL__ >= 708 +deriving instance Typeable TreeTrie1Key +deriving instance Typeable TreeTrieMp1Key +#else +deriving instance Typeable1 TreeTrie1Key +deriving instance Typeable1 TreeTrieMp1Key +#endif +deriving instance Data x => Data (TreeTrie1Key x) +deriving instance Data x => Data (TreeTrieMp1Key x) + +instance Show k => Show (TreeTrie1Key k) where + show TT1K_Any = "*" + show (TT1K_One k) = "1:" ++ show k + +instance Show k => Show (TreeTrieMp1Key k) where + show (TTM1K_Any ) = "**" -- ++ show i + show (TTM1K k) = show k + +instance PP k => PP (TreeTrie1Key k) where + pp TT1K_Any = pp "*" + pp (TT1K_One k) = "1:" >|< k + +instance PP k => PP (TreeTrieMp1Key k) where + pp = ppTreeTrieMp1Key + +ppTreeTrieMp1Key :: PP k => TreeTrieMp1Key k -> PP_Doc +ppTreeTrieMp1Key (TTM1K l) = ppBracketsCommas l +ppTreeTrieMp1Key (TTM1K_Any ) = pp "**" -- >|< i + +ppTreeTrieMpKey :: PP k => TreeTrieMpKey k -> PP_Doc +ppTreeTrieMpKey = ppListSep "<" ">" "," . map ppTreeTrieMp1Key + +-- | Pretty print TrieKey +ppTreeTrieKey :: PP k => TreeTrieKey k -> PP_Doc +ppTreeTrieKey = ppBracketsCommas . map ppTreeTrieMpKey + + +------------------------------------------------------------------------------------------- +--- TreeTrieMpKey inductive construction from new node and children keys +------------------------------------------------------------------------------------------- + +-- | Make singleton, which should at end be stripped from bottom layer of empty TTM1K [] +ttkSingleton :: TreeTrie1Key k -> TreeTrieKey k +ttkSingleton k = [TTM1K [k]] : ttkEmpty + +-- | empty key +ttkEmpty :: TreeTrieKey k +ttkEmpty = [[TTM1K []]] + +-- | Construct intermediate structure for children for a new Key +-- length ks >= 2 +ttkChildren :: [TreeTrieKey k] -> [TreeTrieMpKey k] +ttkChildren ks + = [TTM1K $ concat [k | TTM1K k <- concat hs]] -- first level children are put together in singleton list of list with all children + : merge (split tls) -- and the rest is just concatenated + where (hs,tls) = split ks + split = unzip . map hdAndTl + merge (hs,[]) = [concat hs] + merge (hs,tls) = concat hs : merge (split $ filter (not . List.null) tls) + +-- | Add a new layer with single node on top, combining the rest. +ttkAdd' :: TreeTrie1Key k -> [TreeTrieMpKey k] -> TreeTrieKey k +ttkAdd' k ks = [TTM1K [k]] : ks + +-- | Add a new layer with single node on top, combining the rest. +-- length ks >= 2 +ttkAdd :: TreeTrie1Key k -> [TreeTrieKey k] -> TreeTrieKey k +ttkAdd k ks = ttkAdd' k (ttkChildren ks) + +-- | Fixate by removing lowest layer empty children +ttkFixate :: TreeTrieKey k -> TreeTrieKey k +ttkFixate (kk:kks) | all (\(TTM1K k) -> List.null k) kk = [] + | otherwise = kk : ttkFixate kks +ttkFixate _ = [] + +------------------------------------------------------------------------------------------- +--- TreeTrieKey deconstruction +------------------------------------------------------------------------------------------- + +-- | Split key into parent and children components, inverse of ttkAdd' +ttkParentChildren :: TreeTrieKey k -> ( TreeTrie1Key k, [TreeTrieMpKey k] ) +ttkParentChildren k + = case k of + ([TTM1K [h]] : t) -> (h,t) + +------------------------------------------------------------------------------------------- +--- TreeTrieMpKey matching +------------------------------------------------------------------------------------------- + +-- | Match 1st arg with wildcards to second, returning the to be propagated key to next layer in tree +matchTreeTrieMpKeyTo :: Eq k => TreeTrieMpKey k -> TreeTrieMpKey k -> Maybe (TreeTrieMpKey k -> TreeTrieMpKey k) +matchTreeTrieMpKeyTo l r + | all isJust llrr = Just (\k -> concat $ zipWith ($) (concatMap (fromJust) llrr) k) + | otherwise = Nothing + where llrr = zipWith m l r + m (TTM1K l) (TTM1K r) | length l == length r && all isJust lr + = Just (concatMap fromJust lr) + | otherwise = Nothing + where lr = zipWith m1 l r + m (TTM1K_Any ) (TTM1K []) = Just [] + m (TTM1K_Any ) (TTM1K r ) = Just [const $ replicate (length r) TTM1K_Any] + m1 TT1K_Any _ = Just [const [TTM1K_Any]] + m1 (TT1K_One l) (TT1K_One r) | l == r = Just [\x -> [x]] + m1 _ _ = Nothing + +------------------------------------------------------------------------------------------- +--- Keyable +------------------------------------------------------------------------------------------- + +type family TrTrKey x :: * + +-- | Keyable values, i.e. capable of yielding a TreeTrieKey for retrieval from a trie +class TreeTrieKeyable x where + toTreeTrieKey :: x -> TreeTrieKey (TrTrKey x) + +------------------------------------------------------------------------------------------- +--- TreeTrie structure +------------------------------------------------------------------------------------------- + +-- | Child structure +type TreeTrieChildren k v + = Map.Map (TreeTrieMpKey k) (TreeTrie k v) + +-- | The trie structure, branching out on (1) kind, (2) nr of children, (3) actual key +data TreeTrie k v + = TreeTrie + { ttrieMbVal :: Maybe v -- value + , ttrieSubs :: TreeTrieChildren k v -- children + } + deriving (Typeable, Data) + +emptyTreeTrie, empty :: TreeTrie k v +emptyTreeTrie = TreeTrie Nothing Map.empty + +empty = emptyTreeTrie + +{- +-- %%[9999 export(ppTreeTrieAsIs) +-- | PP a TreeTrie as is, directly corresponding to original structure +ppTreeTrieAsIs :: (PP k, PP v) => TreeTrie k v -> PP_Doc +ppTreeTrieAsIs t + = "V:" >#< (maybe PP.empty pp $ ttrieMbVal t) + >-< "P:" >#< (ppSub $ ttriePartSubs t) + >-< "N:" >#< (ppSub $ ttrieSubs t) + where ppKV (k,v) = k >-< indent 2 (":" >#< ppTreeTrieAsIs v) + ppSub = ppBracketsCommasBlock . map ppKV . Map.toList +-} + +instance (Show k, Show v) => Show (TreeTrie k v) where + showsPrec _ t = showList $ toListByKey t + +instance (PP k, PP v) => PP (TreeTrie k v) where + pp t = ppBracketsCommasBlock $ map (\(a,b) -> ppTreeTrieKey a >#< ":" >#< b) $ toListByKey t + +------------------------------------------------------------------------------------------- +--- Conversion +------------------------------------------------------------------------------------------- + +-- Reconstruction of original key-value pairs. + +toFastSeqSubs :: TreeTrieChildren k v -> Seq.FastSeq (TreeTrieKey k,v) +toFastSeqSubs ttries + = Seq.unions + [ Seq.map (\(ks,v) -> (k:ks,v)) $ toFastSeq True t + | (k,t) <- Map.toList ttries + ] + +toFastSeq :: Bool -> TreeTrie k v -> Seq.FastSeq (TreeTrieKey k,v) +toFastSeq inclEmpty ttrie + = (case ttrieMbVal ttrie of + Just v | inclEmpty -> Seq.singleton ([],v) + _ -> Seq.empty + ) + Seq.:++: toFastSeqSubs (ttrieSubs ttrie) + +toListByKey, toList :: TreeTrie k v -> [(TreeTrieKey k,v)] +toListByKey = Seq.toList . toFastSeq True + +toList = toListByKey + +fromListByKeyWith :: Ord k => (v -> v -> v) -> [(TreeTrieKey k,v)] -> TreeTrie k v +fromListByKeyWith cmb = unionsWith cmb . map (uncurry singleton) + +fromListByKey :: Ord k => [(TreeTrieKey k,v)] -> TreeTrie k v +fromListByKey = unions . map (uncurry singleton) + +fromListWith :: Ord k => (v -> v -> v) -> [(TreeTrieKey k,v)] -> TreeTrie k v +fromListWith cmb = fromListByKeyWith cmb + +fromList :: Ord k => [(TreeTrieKey k,v)] -> TreeTrie k v +fromList = fromListByKey + +------------------------------------------------------------------------------------------- +--- TreeTrie lookup/insertion, how to +------------------------------------------------------------------------------------------- + +-- | How to lookup in a TreeTrie +data TreeTrieLookup + = TTL_Exact -- lookup with exact match + | TTL_WildInTrie -- lookup with wildcard matching in trie + | TTL_WildInKey -- lookup with wildcard matching in key + deriving (Eq) + +------------------------------------------------------------------------------------------- +--- Lookup +------------------------------------------------------------------------------------------- + +-- | Normal lookup for exact match + partial matches (which require some sort of further unification, determining whether it was found) +lookupPartialByKey' :: forall k v v' . (PP k,Ord k) => (TreeTrieKey k -> v -> v') -> TreeTrieLookup -> TreeTrieKey k -> TreeTrie k v -> ([v'],Maybe v') +lookupPartialByKey' mkRes ttrieLookup keys ttrie + = l id mkRes keys ttrie + where l :: (TreeTrieMpKey k -> TreeTrieMpKey k) -> (TreeTrieKey k -> v -> v') -> TreeTrieKey k -> TreeTrie k v -> ([v'],Maybe v') + l = case ttrieLookup of + -- Exact match + TTL_Exact -> \updTKey mkRes keys ttrie -> + case keys of + [] -> dflt mkRes ttrie + (k : ks) + -> case Map.lookup k $ ttrieSubs ttrie of + Just ttrie' + -> ([], m) + where (_,m) = l id (res mkRes k) ks ttrie' + _ -> ([], Nothing) + + -- Match with possible wildcard in Trie + TTL_WildInTrie -> \updTKey mkRes keys ttrie -> + -- tr "TTL_WildInTrie" (ppTreeTrieKey keys >#< (ppTreeTrieMpKey $ updTKey $ replicate (5) (TTM1K []))) $ + case keys of + [] -> dflt mkRes ttrie + (k : ks) + -> (catMaybes mbs ++ concat subs, Nothing) + where (subs,mbs) + = unzip + [ case ks of + [] -> l id (res mkRes k) [] t + (ksk:ksks) | Map.null (ttrieSubs t) -> match (res mkRes k) (fromJust mbm) ks + | otherwise -> l (fromJust mbm) (res mkRes k) ks t + where match mkRes m (km:kms) + = case matchTreeTrieMpKeyTo kt' km of + Just m -> match (res mkRes k) m kms + _ -> ([], Nothing) + where kt' = m $ repeat (TTM1K []) + match mkRes _ [] + = l id (res mkRes k) [] t + | (kt,t) <- Map.toList $ ttrieSubs ttrie + , let kt' = updTKey kt + mbm = -- (\v -> tr "XX" (ppTreeTrieMpKey kt >#< (ppTreeTrieMpKey $ updTKey $ replicate (5) (TTM1K [])) >#< ppTreeTrieMpKey kt' >#< ppTreeTrieMpKey k >#< maybe (pp "--") (\f -> ppTreeTrieMpKey $ f $ repeat (TTM1K [])) v) v) $ + matchTreeTrieMpKeyTo kt' k + , isJust mbm + ] + + -- Match with possible wildcard in Key + TTL_WildInKey -> \updTKey mkRes keys ttrie -> + case keys of + [] -> dflt mkRes ttrie + (k : ks) + -> (catMaybes mbs ++ concat subs, Nothing) + where (subs,mbs) + = unzip + [ case ks of + (ksk:ksks) -> l id (res mkRes kt) (fromJust m ksk : ksks) t + [] | Map.null (ttrieSubs t) -> l id (res mkRes kt) [] t + | otherwise -> l id (res mkRes kt) [fromJust m $ repeat (TTM1K [])] t + | (kt,t) <- Map.toList $ ttrieSubs ttrie + , let m = -- (\v -> tr "YY" (ppTreeTrieMpKey k >#< ppTreeTrieMpKey kt >#< maybe (pp "--") (\f -> ppTreeTrieMpKey $ f $ repeat (TTM1K [])) v) v) $ + matchTreeTrieMpKeyTo k kt + , isJust m + ] + + -- Utils + where dflt mkRes ttrie = ([],fmap (mkRes []) $ ttrieMbVal ttrie) + res mkRes k = \ks v -> mkRes (k : ks) v + +lookupPartialByKey :: (PP k,Ord k) => TreeTrieLookup -> TreeTrieKey k -> TreeTrie k v -> ([v],Maybe v) +lookupPartialByKey = lookupPartialByKey' (\_ v -> v) + +lookupByKey, lookup :: (PP k,Ord k) => TreeTrieKey k -> TreeTrie k v -> Maybe v +lookupByKey keys ttrie = snd $ lookupPartialByKey TTL_WildInTrie keys ttrie + +lookup = lookupByKey + +-- | Convert the lookup result to a list of results +lookupResultToList :: ([v],Maybe v) -> [v] +lookupResultToList (vs,mv) = maybeToList mv ++ vs + +------------------------------------------------------------------------------------------- +--- Observation +------------------------------------------------------------------------------------------- + +isEmpty :: TreeTrie k v -> Bool +isEmpty ttrie + = isNothing (ttrieMbVal ttrie) + && Map.null (ttrieSubs ttrie) + +null :: TreeTrie k v -> Bool +null = isEmpty + +elems :: TreeTrie k v -> [v] +elems = map snd . toListByKey + +------------------------------------------------------------------------------------------- +--- Construction +------------------------------------------------------------------------------------------- + +singleton :: Ord k => TreeTrieKey k -> v -> TreeTrie k v +singleton keys val + = s keys + where s [] = TreeTrie (Just val) Map.empty + s (k : ks) = TreeTrie Nothing (Map.singleton k $ singleton ks val) + +singletonKeyable :: (Ord (TrTrKey v),TreeTrieKeyable v) => v -> TreeTrie (TrTrKey v) v +singletonKeyable val = singleton (toTreeTrieKey val) val + +------------------------------------------------------------------------------------------- +--- Union, insert, ... +------------------------------------------------------------------------------------------- + +unionWith :: Ord k => (v -> v -> v) -> TreeTrie k v -> TreeTrie k v -> TreeTrie k v +unionWith cmb t1 t2 + = TreeTrie + { ttrieMbVal = mkMb cmb (ttrieMbVal t1) (ttrieMbVal t2) + , ttrieSubs = Map.unionWith (unionWith cmb) (ttrieSubs t1) (ttrieSubs t2) + } + where mkMb _ j Nothing = j + mkMb _ Nothing j = j + mkMb cmb (Just x1) (Just x2) = Just $ cmb x1 x2 + +union :: Ord k => TreeTrie k v -> TreeTrie k v -> TreeTrie k v +union = unionWith const + +unionsWith :: Ord k => (v -> v -> v) -> [TreeTrie k v] -> TreeTrie k v +unionsWith cmb [] = emptyTreeTrie +unionsWith cmb ts = foldr1 (unionWith cmb) ts + +unions :: Ord k => [TreeTrie k v] -> TreeTrie k v +unions = unionsWith const + +insertByKeyWith :: Ord k => (v -> v -> v) -> TreeTrieKey k -> v -> TreeTrie k v -> TreeTrie k v +insertByKeyWith cmb keys val ttrie = unionsWith cmb [singleton keys val,ttrie] + +insertByKey :: Ord k => TreeTrieKey k -> v -> TreeTrie k v -> TreeTrie k v +insertByKey = insertByKeyWith const + +insert :: Ord k => TreeTrieKey k -> v -> TreeTrie k v -> TreeTrie k v +insert = insertByKey + +insertKeyable :: (Ord (TrTrKey v),TreeTrieKeyable v) => v -> TreeTrie (TrTrKey v) v -> TreeTrie (TrTrKey v) v +insertKeyable val = insertByKey (toTreeTrieKey val) val + +------------------------------------------------------------------------------------------- +--- Delete, ... +------------------------------------------------------------------------------------------- + +deleteByKey, delete :: Ord k => TreeTrieKey k -> TreeTrie k v -> TreeTrie k v +deleteByKey keys ttrie + = d keys ttrie + where d [] t + = t {ttrieMbVal = Nothing} + d (k : ks) t + = case fmap (d ks) $ Map.lookup k $ ttrieSubs t of + Just c | isEmpty c -> t { ttrieSubs = k `Map.delete` ttrieSubs t } + | otherwise -> t { ttrieSubs = Map.insert k c $ ttrieSubs t } + _ -> t + +delete = deleteByKey + +deleteListByKey :: Ord k => [TreeTrieKey k] -> TreeTrie k v -> TreeTrie k v +deleteListByKey keys ttrie = foldl (\t k -> deleteByKey k t) ttrie keys + +------------------------------------------------------------------------------------------- +--- Instances: Serialize +------------------------------------------------------------------------------------------- + +instance Serialize k => Serialize (TreeTrie1Key k) where + sput (TT1K_Any ) = sputWord8 0 + sput (TT1K_One a ) = sputWord8 1 >> sput a + sget + = do t <- sgetWord8 + case t of + 0 -> return TT1K_Any + 1 -> liftM TT1K_One sget + +instance Serialize k => Serialize (TreeTrieMp1Key k) where + sput (TTM1K_Any ) = sputWord8 0 -- >> sput a + sput (TTM1K a ) = sputWord8 1 >> sput a + sget + = do t <- sgetWord8 + case t of + 0 -> return TTM1K_Any -- sget + 1 -> liftM TTM1K sget + +instance (Ord k, Serialize k, Serialize v) => Serialize (TreeTrie k v) where + sput (TreeTrie a b) = sput a >> sput b + sget = liftM2 TreeTrie sget sget + +------------------------------------------------------------------------------------------- +--- Test +------------------------------------------------------------------------------------------- + +{- +test1 + = fromListByKey + [ ( [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_Any, TT1K_One "P"]] + , [TTM1K [TT1K_One "D", TT1K_One "F"], TTM1K []] + ] + , "C (* D F) P" + ) + , ( [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_One "B", TT1K_One "P"]] + , [TTM1K [TT1K_One "D", TT1K_One "F"], TTM1K []] + ] + , "C (B D F) P" + ) + , ( [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_One "B", TT1K_One "P"]] + , [TTM1K [], TTM1K [TT1K_One "Q", TT1K_One "R"]] + ] + , "C B (P Q R)" + ) + , ( [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_One "B", TT1K_Any]] + ] + , "C B *" + ) + ] + +m1 = fromJust + $ fmap (\f -> f $ [TTM1K [], TTM1K [TT1K_One "Z"]]) + $ matchTreeTrieMpKeyTo + [TTM1K [TT1K_Any, TT1K_One "P"]] + [TTM1K [TT1K_One "B", TT1K_One "P"]] + +m2 = fmap (\f -> f $ repeat (TTM1K [])) + $ matchTreeTrieMpKeyTo + m1 + [TTM1K [TT1K_One "D", TT1K_One "F"], TTM1K [TT1K_One "Z"]] + +m3 = fromJust + $ fmap (\f -> f $ [TTM1K [TT1K_Any, TT1K_One "P"]]) + $ matchTreeTrieMpKeyTo + [TTM1K [TT1K_One "C"]] + [TTM1K [TT1K_One "C"]] + +m4 = fmap (\f -> f $ repeat (TTM1K [])) + $ matchTreeTrieMpKeyTo + m3 + [TTM1K [TT1K_One "B", TT1K_One "P"]] + +m5 = fmap (\f -> f $ repeat (TTM1K [])) + $ matchTreeTrieMpKeyTo + (fromJust m4) + [TTM1K [TT1K_One "D", TT1K_One "F"], TTM1K []] + +l1t1 = lookupPartialByKey' (,) TTL_Exact + [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_Any, TT1K_One "P"]] + ] + +l2t1 = lookupPartialByKey' (,) TTL_WildInTrie + [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_One "B", TT1K_One "P"]] + ] + +l3t1 = lookupPartialByKey' (,) TTL_WildInKey + [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_Any, TT1K_One "P"]] + ] + +l4t1 = lookupPartialByKey' (,) TTL_WildInKey + [ [TTM1K [TT1K_Any :: TreeTrie1Key String]] + ] + +l5t1 = lookupPartialByKey' (,) TTL_WildInTrie + [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_One "B", TT1K_One "P"]] + , [TTM1K [TT1K_One "D", TT1K_One "F"], TTM1K []] + ] + +l6t1 = lookupPartialByKey' (,) TTL_WildInKey + [ [TTM1K [TT1K_One "C"]] + , [TTM1K [TT1K_Any, TT1K_One "P"]] + , [TTM1K [TT1K_One "D", TT1K_One "F"], TTM1K []] + ] + +-} + +{- + + , [<[1:S:Prf]>,<[1:S:occ]>,<[*,1:S:\]>,<[],[*]>] + : [ Prove (m_10_0\l_12_0,,??) + ==> + (m_10_0 == (m_11_0 | ...)) \ l_12_0@off_13_0 + | [ Prove (m_11_0\l_12_0,,??) + , Red (m_10_0\l_12_0,,??) < label l_12_0@off_13_0 < [(m_11_0\l_12_0,,??)]] + , Prove ({||}\l_12_0,,??) + ==> + Red ({||}\l_12_0,,??) < label l_12_0@0 < []] + + [<[1:S:Prf]>,<[1:S:occ]>,<[1:S:[0,0],1:S:\]>,<[],[1:H:3]>,<[1:U:3_48_0_0,1:U:3_48_0_1]>]: 1 + +-} + +{- +test2 + = fromListByKey + [ ( [ [TTM1K [TT1K_One "P"]] + , [TTM1K [TT1K_One "O"]] + , [TTM1K [TT1K_Any, TT1K_One "SL"]] + , [TTM1K [], TTM1K [TT1K_Any]] + ] + , "P (O * (SL *))" + ) + ] + +l1t2 = lookupPartialByKey' (,) TTL_WildInTrie + [ [TTM1K [TT1K_One "P"]] + , [TTM1K [TT1K_One "O"]] + , [TTM1K [TT1K_One "Sc", TT1K_One "SL"]] + , [TTM1K [], TTM1K [TT1K_One "3"]] + , [TTM1K [TT1K_One "3_48_0_0", TT1K_One "3_48_0_1"]] + ] + +-} + +{- +test3 + = fromListByKey + [ ( [[TTM1K [TT1K_One "1:S:Prf"]] + ,[TTM1K [TT1K_One "1:S:occ"]] + ,[TTM1K [TT1K_Any, TT1K_One "1:H:Language.UHC.JS.ECMA.Types.ToJS"]] + ,[TTM1K [], TTM1K [TT1K_One "1:H:UHC.Base.Maybe",TT1K_Any]] + ,[TTM1K [TT1K_Any], TTM1K []] + ] + , "xx" + ) + ] + +l1t3 = lookupPartialByKey' (,) TTL_WildInTrie + [[TTM1K [TT1K_One "1:S:Prf"]] + ,[TTM1K [TT1K_One "1:S:occ"]] + ,[TTM1K [TT1K_One "1:S:[0,0,0,0,0,0]", TT1K_One "1:H:Language.UHC.JS.ECMA.Types.ToJS"]] + ,[TTM1K [],TTM1K [TT1K_One "1:H:UHC.Base.Maybe", TT1K_One "1:H:Language.UHC.JS.ECMA.Types.JSAny"]] + ,[TTM1K [TT1K_One "1:H:Language.UHC.JS.ECMA.Types.JSAny"], TTM1K [TT1K_One "1:U:12_398_1_0"]] + ,[TTM1K [TT1K_One "1:H:Language.UHC.JS.ECMA.Types.JSObject_"], TTM1K []] + ,[TTM1K [TT1K_One "1:H:Language.UHC.JS.W3C.HTML5.NodePtr"]] + ] + + + +-} + +{- + , [<[1:S:Prf]> + ,<[1:S:occ]> + ,<[*,1:H:Language.UHC.JS.ECMA.Types.ToJS]> + ,<[],[1:H:UHC.Base.Maybe,*]> + ,<[*],[]> + ] + +, DBG lookups for + [<[1:S:Prf]> + ,<[1:S:occ]> + ,<[1:S:[0,0,0,0,0,0],1:H:Language.UHC.JS.ECMA.Types.ToJS]> + ,<[],[1:H:UHC.Base.Maybe,1:H:Language.UHC.JS.ECMA.Types.JSAny]> + ,<[1:H:Language.UHC.JS.ECMA.Types.JSAny],[1:U:12_398_1_0]> + ,<[1:H:Language.UHC.JS.ECMA.Types.JSObject_],[]> + ,<[1:H:Language.UHC.JS.W3C.HTML5.NodePtr]> + ] + +-} diff --git a/src/UHC/Util/Utils.hs b/src/UHC/Util/Utils.hs --- a/src/UHC/Util/Utils.hs +++ b/src/UHC/Util/Utils.hs @@ -20,6 +20,7 @@ , firstNotEmpty , listSaturate, listSaturateWith , spanOnRest + , filterMb -- * Tuple , tup123to1, tup123to2 @@ -109,6 +110,7 @@ -- import UHC.Util.Pretty import Data.Char import Data.List +import Data.Maybe import Data.Typeable import GHC.Generics import qualified Data.Set as Set @@ -217,6 +219,11 @@ | p xs = (x:ys, zs) | otherwise = ([],xs) where (ys,zs) = spanOnRest p xs' + +-- | variant on 'filter', where predicate also yields a result +filterMb :: (a -> Maybe b) -> [a] -> [b] +filterMb p = catMaybes . map p +{-# INLINE filterMb #-} ------------------------------------------------------------------------- -- Tupling, untupling diff --git a/uhc-util.cabal b/uhc-util.cabal --- a/uhc-util.cabal +++ b/uhc-util.cabal @@ -1,5 +1,5 @@ Name: uhc-util -Version: 0.1.6.2 +Version: 0.1.6.3 cabal-version: >= 1.6 License: BSD3 Copyright: Utrecht University, Department of Information and Computing Sciences, Software Technology group @@ -21,7 +21,7 @@ library Build-Depends: - base >= 4.6 && < 5, + base >= 4.8 && < 5, mtl >= 2, fgl >= 5.4, hashable >= 1.1, @@ -40,6 +40,12 @@ UHC.Util.AGraph, UHC.Util.AssocL, UHC.Util.Binary, + UHC.Util.CHR, + UHC.Util.CHR.Key, + UHC.Util.CHR.Base, + UHC.Util.CHR.Rule, + UHC.Util.CHR.Solve.TreeTrie.Mono, + UHC.Util.CHR.Solve.TreeTrie.Poly, UHC.Util.CompileRun, UHC.Util.CompileRun2, UHC.Util.CompileRun3, @@ -59,14 +65,19 @@ UHC.Util.PrettyUtils, UHC.Util.Rel, UHC.Util.RelMap, + UHC.Util.RLList, UHC.Util.ScanUtils, UHC.Util.ScopeMapGam, UHC.Util.Serialize, + UHC.Util.Substitutable, UHC.Util.Time, + UHC.Util.TreeTrie, UHC.Util.Utils, UHC.Util.VarLookup, UHC.Util.VarMp + Other-Modules: + UHC.Util.CHR.Solve.TreeTrie.Internal Ghc-Options: HS-Source-Dirs: src Build-Tools: - Extensions: NoMagicHash, DeriveGeneric, DeriveDataTypeable + Extensions: NoMagicHash, DeriveGeneric, DeriveDataTypeable, TypeFamilies, FlexibleContexts