diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,5 +1,17 @@ # Changelog +## 0.1.6.5 + +- [libs] updated version lowerbound for hashable and fclabels +- [chr] dependency on logict-state lib, as prep for new solver +- [chr] CHR rules have an additional priority field, as prep for new solver +- [api] additional PP instances +- [serialize] generic impl of Serialize more efficiently generates tags (1 per datatype instead of log(nr of constructors)) + +## 0.1.6.4 + +- [api] move of RLList functionality encoding lexical scoping to separate module LexScope (taken from UHC) + ## 0.1.6.3 - [api] move of RLList, TreeTrie, CHR, Substitutable (partial) from uhc to uhc-util diff --git a/src/UHC/Util/CHR/Base.hs b/src/UHC/Util/CHR/Base.hs --- a/src/UHC/Util/CHR/Base.hs +++ b/src/UHC/Util/CHR/Base.hs @@ -18,9 +18,13 @@ , IsCHRGuard(..) , CHRGuard(..) + , IsCHRPrio(..) + , CHRPrio(..) + , CHREmptySubstitution(..) , CHRMatchable(..), CHRMatchableKey , CHRCheckable(..) + , CHRPrioEvaluatable(..) ) where @@ -63,6 +67,15 @@ , PP g ) => IsCHRGuard env g subst +-- | (Class alias) API for priority requirements +class ( CHRPrioEvaluatable env p subst + , Typeable p + , Serialize p + , PP p + ) => IsCHRPrio env p subst + +instance {-# OVERLAPPABLE #-} IsCHRPrio env () subst + ------------------------------------------------------------------------------------------- --- Existentially quantified Constraint representations to allow for mix of arbitrary universes ------------------------------------------------------------------------------------------- @@ -153,6 +166,41 @@ chrCheck env subst (CHRGuard g) = chrCheck env subst g ------------------------------------------------------------------------------------------- +--- Existentially quantified Prio representations to allow for mix of arbitrary universes +------------------------------------------------------------------------------------------- + +data CHRPrio env subst + = forall p . + ( IsCHRPrio env p subst + ) + => CHRPrio + { chrPrio :: p + } + +deriving instance Typeable (CHRPrio env subst) +-- deriving instance (Data env, Data subst) => Data (CHRGuard env subst) + +instance Show (CHRPrio env subst) where + show _ = "CHRPrio" + +instance PP (CHRPrio env subst) where + pp (CHRPrio 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 CHRPrioEvaluatable env (CHRPrio env subst) subst where + chrPrioEval env subst (CHRPrio p) = chrPrioEval env subst p + +------------------------------------------------------------------------------------------- --- CHREmptySubstitution ------------------------------------------------------------------------------------------- @@ -177,6 +225,17 @@ -- | 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 + +------------------------------------------------------------------------------------------- +--- CHRPrioEvaluatable +------------------------------------------------------------------------------------------- + +-- | A PrioEvaluatable participates in the reduction process to indicate the rule priority, higher prio takes precedence +class CHRPrioEvaluatable env x subst where + chrPrioEval :: env -> subst -> x -> Int + +instance {-# OVERLAPPABLE #-} CHRPrioEvaluatable env () subst where + chrPrioEval _ _ _ = minBound ------------------------------------------------------------------------------------------- --- What a constraint must be capable of diff --git a/src/UHC/Util/CHR/Rule.hs b/src/UHC/Util/CHR/Rule.hs --- a/src/UHC/Util/CHR/Rule.hs +++ b/src/UHC/Util/CHR/Rule.hs @@ -18,6 +18,7 @@ , (<==>), (==>), (|>) , MkSolverConstraint(..) , MkSolverGuard(..) + , MkSolverPrio(..) ) where @@ -27,7 +28,7 @@ import UHC.Util.Utils import Data.Monoid import Data.Typeable -import Data.Data +-- import Data.Data import qualified Data.Set as Set import UHC.Util.Pretty import UHC.Util.CHR.Key @@ -42,7 +43,7 @@ data CHRRule env subst = CHRRule - { chrRule :: Rule (CHRConstraint env subst) (CHRGuard env subst) + { chrRule :: Rule (CHRConstraint env subst) (CHRGuard env subst) () } deriving (Typeable) @@ -61,28 +62,29 @@ ------------------------------------------------------------------------------------------- -- | 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 +data Rule cnstr guard prio = Rule { ruleHead :: ![cnstr] - , ruleSimpSz :: !Int -- length of the part of the head which is the simplification part - , ruleGuard :: ![guard] -- subst -> Maybe subst + , ruleSimpSz :: !Int -- ^ length of the part of the head which is the simplification part + , ruleGuard :: ![guard] , ruleBody :: ![cnstr] + , rulePrio :: !(Maybe prio) -- ^ optional priority, if absent it is considered the lowest possible } - deriving (Typeable, Data) + deriving (Typeable) emptyCHRGuard :: [a] emptyCHRGuard = [] -instance Show (Rule c g) where +instance Show (Rule c g p) where show _ = "Rule" -instance (PP c,PP g) => PP (Rule c g) where +instance (PP c, PP g, PP p) => PP (Rule c g p) 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) + (Rule h@(_:_) sz g b p) | sz == 0 -> ppChr ([ppL h, pp "==>"] ++ ppGB g b) + (Rule h@(_:_) sz g b p) | sz == length h -> ppChr ([ppL h, pp "<==>"] ++ ppGB g b) + (Rule h@(_:_) sz g b p) -> ppChr ([ppL (take sz h), pp "|", ppL (drop sz h), pp "<==>"] ++ ppGB g b) + (Rule [] _ g b p) -> ppChr (ppGB g b) where ppGB g@(_:_) b@(_:_) = [ppL g, "|" >#< ppL b] ppGB g@(_:_) [] = [ppL g >#< "|"] ppGB [] b@(_:_) = [ppL b] @@ -91,22 +93,22 @@ ppL xs = ppBracketsCommasBlock xs -- ppParensCommasBlock xs ppChr l = vlist l -- ppCurlysBlock -type instance TTKey (Rule cnstr guard) = TTKey cnstr +type instance TTKey (Rule cnstr guard prio) = TTKey cnstr -instance (TTKeyable cnstr) => TTKeyable (Rule cnstr guard) where +instance (TTKeyable cnstr) => TTKeyable (Rule cnstr guard prio) where toTTKey' o chr = toTTKey' o $ head $ ruleHead chr ------------------------------------------------------------------------------------------- --- Var instances ------------------------------------------------------------------------------------------- -type instance ExtrValVarKey (Rule c g) = ExtrValVarKey c +type instance ExtrValVarKey (Rule c g p) = ExtrValVarKey c -instance (VarExtractable c, VarExtractable g, ExtrValVarKey c ~ ExtrValVarKey g) => VarExtractable (Rule c g) where +instance (VarExtractable c, VarExtractable g, ExtrValVarKey c ~ ExtrValVarKey g) => VarExtractable (Rule c g p) 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 +instance (VarUpdatable c s, VarUpdatable g s) => VarUpdatable (Rule c g p) 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} @@ -114,36 +116,6 @@ --- 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' @@ -175,81 +147,65 @@ toSolverGuard = CHRGuard fromSolverGuard (CHRGuard g) = cast g +class MkSolverPrio p p' where + toSolverPrio :: p' -> p + fromSolverPrio :: p -> Maybe p' + +instance {-# INCOHERENT #-} MkSolverPrio p p where + toSolverPrio = id + fromSolverPrio = Just + +instance {-# OVERLAPS #-} + ( IsCHRPrio e p s + -- , ExtrValVarKey (CHRPrio e s) ~ ExtrValVarKey p + ) => MkSolverPrio (CHRPrio e s) p where + toSolverPrio = CHRPrio + fromSolverPrio (CHRPrio p) = cast p + class MkRule r where type SolverConstraint r :: * type SolverGuard r :: * + type SolverPrio r :: * -- | Make rule - mkRule :: [SolverConstraint r] -> Int -> [SolverGuard r] -> [SolverConstraint r] -> r + mkRule :: [SolverConstraint r] -> Int -> [SolverGuard r] -> [SolverConstraint r] -> Maybe (SolverPrio r) -> r -- | Add guards to rule guardRule :: [SolverGuard r] -> r -> r + -- | Add prio to rule + prioritizeRule :: SolverPrio r -> r -> r -instance MkRule (Rule c g) where - type SolverConstraint (Rule c g) = c - type SolverGuard (Rule c g) = g +instance MkRule (Rule c g p) where + type SolverConstraint (Rule c g p) = c + type SolverGuard (Rule c g p) = g + type SolverPrio (Rule c g p) = p mkRule = Rule guardRule g r = r {ruleGuard = ruleGuard r ++ g} + prioritizeRule p r = r {rulePrio = Just p} 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 + type SolverPrio (CHRRule e s) = () + mkRule h1 h2 l b p = CHRRule $ mkRule h1 h2 l b p guardRule g (CHRRule r) = CHRRule $ guardRule g r + prioritizeRule p (CHRRule r) = CHRRule $ prioritizeRule p 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) +(<==>), (==>) :: forall r c1 c2 . (MkRule r, MkSolverConstraint (SolverConstraint r) c1, MkSolverConstraint (SolverConstraint r) c2) => [c1] -> [c2] -> r +hs <==> bs = mkRule (map toSolverConstraint hs) (length hs) [] (map toSolverConstraint bs) Nothing +hs ==> bs = mkRule (map toSolverConstraint hs) 0 [] (map toSolverConstraint bs) Nothing (|>) :: (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 (Serialize c,Serialize g,Serialize p) => Serialize (Rule c g p) where + sput (Rule a b c d e) = sput a >> sput b >> sput c >> sput d >> sput e + sget = liftM5 Rule sget sget sget sget sget {- instance (MkSolverConstraint (CHRConstraint e s) x', Serialize x') => Serialize (CHRConstraint e s) where diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs --- a/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs @@ -1,7 +1,7 @@ {-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses #-} ------------------------------------------------------------------------------------------- ---- CHR TreeTrie based solver shared internals +-- | CHR TreeTrie based solver shared internals ------------------------------------------------------------------------------------------- module UHC.Util.CHR.Solve.TreeTrie.Internal @@ -183,7 +183,7 @@ type instance TTKey (StoredCHR c g) = TTKey c -instance (TTKeyable (Rule c g)) => TTKeyable (StoredCHR c g) where +instance (TTKeyable (Rule c g p)) => TTKeyable (StoredCHR c g) where toTTKey' o schr = toTTKey' o $ storedChr schr -- | The size of the simplification part of a CHR @@ -229,7 +229,7 @@ pp = ppStoredCHR -- | Convert from list to store -chrStoreFromElems :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => [Rule c g] -> CHRStore c g +chrStoreFromElems :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => [Rule c g p] -> CHRStore c g p chrStoreFromElems chrs = mkCHRStore $ chrTrieFromListByKeyWith cmbStoredCHRs @@ -243,20 +243,20 @@ 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 :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => Rule c g p -> CHRStore c g p chrStoreSingletonElem x = chrStoreFromElems [x] -chrStoreUnion :: (Ord (TTKey c)) => CHRStore c g -> CHRStore c g -> CHRStore c g +chrStoreUnion :: (Ord (TTKey c)) => CHRStore c g p -> CHRStore c g p -> CHRStore c g p chrStoreUnion cs1 cs2 = mkCHRStore $ chrTrieUnionWith cmbStoredCHRs (chrstoreTrie cs1) (chrstoreTrie cs2) {-# INLINE chrStoreUnion #-} -chrStoreUnions :: (Ord (TTKey c)) => [CHRStore c g] -> CHRStore c g +chrStoreUnions :: (Ord (TTKey c)) => [CHRStore c g p] -> CHRStore c g p 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 :: (Ord (TTKey c)) => CHRStore c g p -> [(CHRKey c,[Rule c g p])] chrStoreToList cs = [ (k,chrs) | (k,e) <- chrTrieToListByKey $ chrstoreTrie cs @@ -264,13 +264,13 @@ , not $ Prelude.null chrs ] -chrStoreElems :: (Ord (TTKey c)) => CHRStore c g -> [Rule c g] +chrStoreElems :: (Ord (TTKey c)) => CHRStore c g p -> [Rule c g p] chrStoreElems = concatMap snd . chrStoreToList -ppCHRStore :: (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => CHRStore c g -> PP_Doc +ppCHRStore :: (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => CHRStore c g p -> 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' :: (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => CHRStore c g p -> PP_Doc ppCHRStore' = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrTrieToListByKey . chrstoreTrie -} @@ -474,275 +474,6 @@ --- 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),_) @@ -754,55 +485,3 @@ 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 --- a/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs @@ -71,51 +71,51 @@ ------------------------------------------------------------------------------------------- -- | A CHR as stored in a CHRStore, requiring additional info for efficiency -data StoredCHR c g +data StoredCHR c g p = StoredCHR - { storedChr :: !(Rule c g) -- the Rule + { storedChr :: !(Rule c g p) -- 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) +-- deriving instance (Data (TTKey c), Data c, Data g) => Data (StoredCHR c g p) -type instance TTKey (StoredCHR c g) = TTKey c +type instance TTKey (StoredCHR c g p) = TTKey c -instance (TTKeyable (Rule c g)) => TTKeyable (StoredCHR c g) where +instance (TTKeyable (Rule c g p)) => TTKeyable (StoredCHR c g p) where toTTKey' o schr = toTTKey' o $ storedChr schr -- | The size of the simplification part of a CHR -storedSimpSz :: StoredCHR c g -> Int +storedSimpSz :: StoredCHR c g p -> Int storedSimpSz = ruleSimpSz . storedChr {-# INLINE storedSimpSz #-} -- | A CHR store is a trie structure -newtype CHRStore cnstr guard +newtype CHRStore cnstr guard prio = CHRStore - { chrstoreTrie :: CHRTrie [StoredCHR cnstr guard] + { chrstoreTrie :: CHRTrie [StoredCHR cnstr guard prio] } deriving (Typeable) -deriving instance (Data (TTKey cnstr), Ord (TTKey cnstr), Data cnstr, Data guard) => Data (CHRStore cnstr guard) +-- deriving instance (Data (TTKey cnstr), Ord (TTKey cnstr), Data cnstr, Data guard) => Data (CHRStore cnstr guard prio) mkCHRStore trie = CHRStore trie -emptyCHRStore :: CHRStore cnstr guard +emptyCHRStore :: CHRStore cnstr guard prio 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 :: [StoredCHR c g p] -> [StoredCHR c g p] -> [StoredCHR c g p] 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 +instance Show (StoredCHR c g p) where show _ = "StoredCHR" -ppStoredCHR :: (PP (TTKey c), PP c, PP g) => StoredCHR c g -> PP_Doc +ppStoredCHR :: (PP (TTKey c), PP c, PP g, PP p) => StoredCHR c g p -> PP_Doc ppStoredCHR c@(StoredCHR {storedIdent=(idKey,idSeqNr)}) = storedChr c >-< indent 2 @@ -126,11 +126,11 @@ , "ident" >#< ppParensCommas [ppTreeTrieKey idKey,pp idSeqNr] ]) -instance (PP (TTKey c), PP c, PP g) => PP (StoredCHR c g) where +instance (PP (TTKey c), PP c, PP g, PP p) => PP (StoredCHR c g p) 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 :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => [Rule c g p] -> CHRStore c g p chrStoreFromElems chrs = mkCHRStore $ chrTrieFromListByKeyWith cmbStoredCHRs @@ -144,20 +144,20 @@ 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 :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => Rule c g p -> CHRStore c g p chrStoreSingletonElem x = chrStoreFromElems [x] -chrStoreUnion :: (Ord (TTKey c)) => CHRStore c g -> CHRStore c g -> CHRStore c g +chrStoreUnion :: (Ord (TTKey c)) => CHRStore c g p -> CHRStore c g p -> CHRStore c g p chrStoreUnion cs1 cs2 = mkCHRStore $ chrTrieUnionWith cmbStoredCHRs (chrstoreTrie cs1) (chrstoreTrie cs2) {-# INLINE chrStoreUnion #-} -chrStoreUnions :: (Ord (TTKey c)) => [CHRStore c g] -> CHRStore c g +chrStoreUnions :: (Ord (TTKey c)) => [CHRStore c g p] -> CHRStore c g p 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 :: (Ord (TTKey c)) => CHRStore c g p -> [(CHRKey c,[Rule c g p])] chrStoreToList cs = [ (k,chrs) | (k,e) <- chrTrieToListByKey $ chrstoreTrie cs @@ -165,35 +165,35 @@ , not $ Prelude.null chrs ] -chrStoreElems :: (Ord (TTKey c)) => CHRStore c g -> [Rule c g] +chrStoreElems :: (Ord (TTKey c)) => CHRStore c g p -> [Rule c g p] chrStoreElems = concatMap snd . chrStoreToList -ppCHRStore :: (PP c, PP g, Ord (TTKey c), PP (TTKey c)) => CHRStore c g -> PP_Doc +ppCHRStore :: (PP c, PP g, PP p, Ord (TTKey c), PP (TTKey c)) => CHRStore c g p -> 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' :: (PP c, PP g, PP p, Ord (TTKey c), PP (TTKey c)) => CHRStore c g p -> 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 +type SolveStep c g p s = SolveStep' c (Rule c g p) s +type SolveTrace c g p s = SolveTrace' c (Rule c g p) 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 +-- type SolveMatchCache c g p s = Map.Map (CHRKey c) [((StoredCHR c g p,([WorkKey c],[Work c])),s)] +-- type SolveMatchCache c g p s = Map.Map (WorkKey c) [((StoredCHR c g p,([WorkKey c],[Work c])),s)] +type SolveMatchCache c g p s = SolveMatchCache' c (StoredCHR c g p) s ------------------------------------------------------------------------------------------- --- Solve state ------------------------------------------------------------------------------------------- -type SolveState c g s = SolveState' c (Rule c g) (StoredCHR c g) s +type SolveState c g p s = SolveState' c (Rule c g p) (StoredCHR c g p) s ------------------------------------------------------------------------------------------- --- Solver @@ -202,61 +202,62 @@ -- | (Class alias) API for solving requirements class ( IsCHRConstraint env c s , IsCHRGuard env g s + , IsCHRPrio env p s , VarLookupCmb s s , VarUpdatable s s , CHREmptySubstitution s , TrTrKey c ~ TTKey c - ) => IsCHRSolvable env c g s + ) => IsCHRSolvable env c g p s {- chrSolve - :: forall env c g s . - ( IsCHRSolvable env c g s + :: forall env c g p s . + ( IsCHRSolvable env c g p s ) => env - -> CHRStore c g + -> CHRStore c g p -> [c] -> [c] chrSolve env chrStore cnstrs = work ++ done - where (work, done, _ :: SolveTrace c g s) = chrSolve' env chrStore cnstrs + where (work, done, _ :: SolveTrace c g p s) = chrSolve' env chrStore cnstrs -} -- | Solve chrSolve' - :: forall env c g s . - ( IsCHRSolvable env c g s + :: forall env c g p s . + ( IsCHRSolvable env c g p s ) => env - -> CHRStore c g + -> CHRStore c g p -> [c] - -> ([c],[c],SolveTrace c g s) + -> ([c],[c],SolveTrace c g p 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 + :: forall env c g p s . + ( IsCHRSolvable env c g p s ) => env - -> CHRStore c g + -> CHRStore c g p -> [c] - -> SolveState c g s - -> SolveState c g s + -> SolveState c g p s + -> SolveState c g p 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 + :: forall env c g p s . + ( IsCHRSolvable env c g p s ) => env - -> CHRStore c g + -> CHRStore c g p -> [c] - -> State (SolveState c g s) () + -> State (SolveState c g p s) () chrSolveM env chrStore cnstrs = do modify initState iter @@ -283,7 +284,7 @@ -} stmatch expandMatch matches - where -- expandMatch :: SolveState c g s -> [((StoredCHR c g, ([WorkKey c], [Work c])), s)] -> SolveState c g s + where -- expandMatch :: SolveState c g p s -> [((StoredCHR c g p, ([WorkKey c], [Work c])), s)] -> SolveState c g p s expandMatch ( ( ( schr@(StoredCHR {storedIdent = chrId, storedChr = chr@(Rule {ruleBody = b, ruleSimpSz = simpSz})}) , (keys,works) ) @@ -391,14 +392,14 @@ -- results, stepwise computed for later reference in debugging output -- basic search result - r2 :: [StoredCHR c g] -- CHRs matching workHdKey + r2 :: [StoredCHR c g p] -- 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 + r23 :: [( StoredCHR c g p -- the CHR , ( [( [(CHRKey c, Work c)] -- for each CHR the list of constraints, all possible work matches , [(CHRKey c, Work c)] )] @@ -408,7 +409,7 @@ -- possible matches r3, r4 - :: [( StoredCHR c g -- the matched CHR + :: [( StoredCHR c g p -- the matched CHR , ( [CHRKey c] -- possible matching constraints (matching with the CHR constraints), as Keys, as Works , [Work c] ) )] @@ -418,7 +419,7 @@ 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 + r5 :: [( ( StoredCHR c g p , ( [CHRKey c] , [Work c] ) ) @@ -445,7 +446,7 @@ => CHRKey c -> LastQuery c -> WorkTrie c - -> StoredCHR c g + -> StoredCHR c g p -> ( [( [(CHRKey c, Work c)] , [(CHRKey c, Work c)] )] @@ -465,7 +466,7 @@ slvIsUsedByPropPart :: (Ord k, Ord (TTKey c)) => Map.Map (Set.Set k) (Set.Set (UsedByKey c)) - -> (StoredCHR c g, ([k], t)) + -> (StoredCHR c g p, ([k], t)) -> Bool slvIsUsedByPropPart wlUsedIn (chr,(keys,_)) = fnd $ drop (storedSimpSz chr) keys @@ -479,7 +480,7 @@ , CHRCheckable env g s , VarLookupCmb s s ) - => env -> StoredCHR c g -> [c] -> Maybe s + => env -> StoredCHR c g p -> [c] -> Maybe s slvMatch env chr cnstrs = foldl cmb (Just chrEmptySubst) $ matches chr cnstrs ++ checks chr where matches (StoredCHR {storedChr = Rule {ruleHead = hc}}) cnstrs @@ -496,11 +497,11 @@ --- Instances: Serialize ------------------------------------------------------------------------------------------- -instance (Ord (TTKey c), Serialize (TTKey c), Serialize c, Serialize g) => Serialize (CHRStore c g) where +instance (Ord (TTKey c), Serialize (TTKey c), Serialize c, Serialize g, Serialize p) => Serialize (CHRStore c g p) where sput (CHRStore a) = sput a sget = liftM CHRStore sget -instance (Serialize c, Serialize g, Serialize (TTKey c)) => Serialize (StoredCHR c g) where +instance (Serialize c, Serialize g, Serialize p, Serialize (TTKey c)) => Serialize (StoredCHR c g p) 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/MonoBacktrackPrio.hs b/src/UHC/Util/CHR/Solve/TreeTrie/MonoBacktrackPrio.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR/Solve/TreeTrie/MonoBacktrackPrio.hs @@ -0,0 +1,541 @@ +{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses #-} + +------------------------------------------------------------------------------------------- +--- CHR solver +------------------------------------------------------------------------------------------- + +{-| +Under development (as of 20160218). + +Solver is: +- Monomorphic, i.e. the solver is polymorph but therefore can only work on 1 type of constraints, rules, etc. +- Knows about variables for which substitutions can be found, substitutions are part of found solutions. +- Backtracking (on variable bindings/substitutions), multiple solution alternatives are explored. +- Found rules are applied in an order described by priorities associated with rules. Priorities can be dynamic, i.e. depend on terms in rules. +-} + +module UHC.Util.CHR.Solve.TreeTrie.MonoBacktrackPrio + ( + ) +{- + ( 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 + +------------------------------------------------------------------------------------------- +--- The CHR monad, state, etc +------------------------------------------------------------------------------------------- + +-- | Global state +data CHRGlobState cnstr guard prio + = CHRGlobState + { chrgstStore :: !(CHRStore cnstr guard prio) -- ^ Actual database of rules, to be searched + , chrgstNextFreeRuleInx :: !Int -- ^ Next free rule identification, used by solving to identify whether a rule has been used for a constraint. + -- The numbering is applied to constraints inside a rule which can be matched. + } + deriving (Typeable) + +------------------------------------------------------------------------------------------- +--- CHR store, with fast search +------------------------------------------------------------------------------------------- + +-- | A CHR as stored in a CHRStore, requiring additional info for efficiency +data StoredCHR c g p + = StoredCHR + { storedChr :: !(Rule c g p) -- 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 p) + +type instance TTKey (StoredCHR c g p) = TTKey c + +instance (TTKeyable (Rule c g p)) => TTKeyable (StoredCHR c g p) where + toTTKey' o schr = toTTKey' o $ storedChr schr + +-- | The size of the simplification part of a CHR +storedSimpSz :: StoredCHR c g p -> Int +storedSimpSz = ruleSimpSz . storedChr +{-# INLINE storedSimpSz #-} +-} + +-- | A CHR store is a trie structure +newtype CHRStore cnstr guard prio + = CHRStore + { chrstoreTrie :: CHRTrie [StoredCHR cnstr guard prio] + } + deriving (Typeable) + +{- +-- deriving instance (Data (TTKey cnstr), Ord (TTKey cnstr), Data cnstr, Data guard) => Data (CHRStore cnstr guard prio) + +mkCHRStore trie = CHRStore trie + +emptyCHRStore :: CHRStore cnstr guard prio +emptyCHRStore = mkCHRStore emptyCHRTrie + +-- | Combine lists of stored CHRs by concat, adapting their identification nr to be unique +cmbStoredCHRs :: [StoredCHR c g p] -> [StoredCHR c g p] -> [StoredCHR c g p] +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 p) where + show _ = "StoredCHR" + +ppStoredCHR :: (PP (TTKey c), PP c, PP g, PP p) => StoredCHR c g p -> 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 p) => PP (StoredCHR c g p) where + pp = ppStoredCHR + +-- | Convert from list to store +chrStoreFromElems :: (TTKeyable c, Ord (TTKey c), TTKey c ~ TrTrKey c) => [Rule c g p] -> CHRStore c g p +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 p -> CHRStore c g p +chrStoreSingletonElem x = chrStoreFromElems [x] + +chrStoreUnion :: (Ord (TTKey c)) => CHRStore c g p -> CHRStore c g p -> CHRStore c g p +chrStoreUnion cs1 cs2 = mkCHRStore $ chrTrieUnionWith cmbStoredCHRs (chrstoreTrie cs1) (chrstoreTrie cs2) +{-# INLINE chrStoreUnion #-} + +chrStoreUnions :: (Ord (TTKey c)) => [CHRStore c g p] -> CHRStore c g p +chrStoreUnions [] = emptyCHRStore +chrStoreUnions [s] = s +chrStoreUnions ss = foldr1 chrStoreUnion ss +{-# INLINE chrStoreUnions #-} + +chrStoreToList :: (Ord (TTKey c)) => CHRStore c g p -> [(CHRKey c,[Rule c g p])] +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 p -> [Rule c g p] +chrStoreElems = concatMap snd . chrStoreToList + +ppCHRStore :: (PP c, PP g, PP p, Ord (TTKey c), PP (TTKey c)) => CHRStore c g p -> PP_Doc +ppCHRStore = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrStoreToList + +ppCHRStore' :: (PP c, PP g, PP p, Ord (TTKey c), PP (TTKey c)) => CHRStore c g p -> PP_Doc +ppCHRStore' = ppCurlysCommasBlock . map (\(k,v) -> ppTreeTrieKey k >-< indent 2 (":" >#< ppBracketsCommasBlock v)) . chrTrieToListByKey . chrstoreTrie + +-} + +------------------------------------------------------------------------------------------- +--- Solver trace +------------------------------------------------------------------------------------------- + +{- +type SolveStep c g p s = SolveStep' c (Rule c g p) s +type SolveTrace c g p s = SolveTrace' c (Rule c g p) s +-} + +------------------------------------------------------------------------------------------- +--- Cache for maintaining which WorkKey has already had a match +------------------------------------------------------------------------------------------- + +{- +-- type SolveMatchCache c g p s = Map.Map (CHRKey c) [((StoredCHR c g p,([WorkKey c],[Work c])),s)] +-- type SolveMatchCache c g p s = Map.Map (WorkKey c) [((StoredCHR c g p,([WorkKey c],[Work c])),s)] +type SolveMatchCache c g p s = SolveMatchCache' c (StoredCHR c g p) s +-} + +------------------------------------------------------------------------------------------- +--- Solve state +------------------------------------------------------------------------------------------- + +{- +type SolveState c g p s = SolveState' c (Rule c g p) (StoredCHR c g p) 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 p s +-} + +{- +chrSolve + :: forall env c g p s . + ( IsCHRSolvable env c g p s + ) + => env + -> CHRStore c g p + -> [c] + -> [c] +chrSolve env chrStore cnstrs + = work ++ done + where (work, done, _ :: SolveTrace c g p s) = chrSolve' env chrStore cnstrs +-} + +{- +-- | Solve +chrSolve' + :: forall env c g p s . + ( IsCHRSolvable env c g p s + ) + => env + -> CHRStore c g p + -> [c] + -> ([c],[c],SolveTrace c g p 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 p s . + ( IsCHRSolvable env c g p s + ) + => env + -> CHRStore c g p + -> [c] + -> SolveState c g p s + -> SolveState c g p s +chrSolve'' env chrStore cnstrs prevState + = flip execState prevState $ chrSolveM env chrStore cnstrs + +-- | Solve +chrSolveM + :: forall env c g p s . + ( IsCHRSolvable env c g p s + ) + => env + -> CHRStore c g p + -> [c] + -> State (SolveState c g p 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 p s -> [((StoredCHR c g p, ([WorkKey c], [Work c])), s)] -> SolveState c g p 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 p] -- 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 p -- 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 p -- 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 p + , ( [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 p + -> ( [( [(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 p, ([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 p -> [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 p) => Serialize (CHRStore c g p) where + sput (CHRStore a) = sput a + sget = liftM CHRStore sget + +instance (Serialize c, Serialize g, Serialize p, Serialize (TTKey c)) => Serialize (StoredCHR c g p) 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 --- a/src/UHC/Util/CHR/Solve/TreeTrie/Poly.hs +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Poly.hs @@ -101,7 +101,7 @@ } 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) +-- 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 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 @@ -86,12 +86,13 @@ -- import UU.Pretty -- import UHC.Util.Chitil.Pretty -import UHC.Util.PrettySimple -import UHC.Util.Utils -import UHC.Util.FPath -import UHC.Util.Time -import System.IO -import Data.List +import UHC.Util.PrettySimple +import UHC.Util.Utils +import UHC.Util.FPath +import UHC.Util.Time +import System.IO +import Data.List +import qualified Data.Set as Set ------------------------------------------------------------------------- -- PP utils for lists @@ -162,7 +163,7 @@ ppBlockWithStrings' = ppBlockWithStrings'' False {-# INLINE ppBlockWithStrings' #-} --- | See 'ppBlock', but with string delimiters aligned properly, yielding a list of elements +-- | See 'ppBlock', but with string delimiters aligned properly, yielding a list of elements, preferring single line horizontal placement ppBlockWithStringsH' :: (PP a) => String -> String -> String -> [a] -> [PP_Doc] ppBlockWithStringsH' = ppBlockWithStrings'' True {-# INLINE ppBlockWithStringsH' #-} @@ -171,7 +172,7 @@ ppBlockWithStrings :: (PP a) => String -> String -> String -> [a] -> PP_Doc ppBlockWithStrings o c s = vlist . ppBlockWithStrings' o c s --- | See 'ppBlock', but with string delimiters aligned properly +-- | See 'ppBlock', but with string delimiters aligned properly, preferring single line horizontal placement ppBlockWithStringsH :: (PP a) => String -> String -> String -> [a] -> PP_Doc ppBlockWithStringsH o c s = vlist . ppBlockWithStringsH' o c s @@ -200,7 +201,7 @@ ppCurlysBlock = ppBlockWithStrings "{" "}" " " {-# INLINE ppCurlysBlock #-} --- | PP horizontally or vertically with "{", " ", and "}" in a possibly multiline block structure +-- | PP horizontally or vertically with "{", " ", and "}" in a possibly multiline block structure, preferring single line horizontal placement ppCurlysBlockH :: PP a => [a] -> PP_Doc ppCurlysBlockH = ppBlockWithStringsH "{" "}" " " {-# INLINE ppCurlysBlockH #-} @@ -210,7 +211,7 @@ ppCurlysSemisBlock = ppBlockWithStrings "{" "}" "; " {-# INLINE ppCurlysSemisBlock #-} --- | PP horizontally or vertically with "{", ";", and "}" in a possibly multiline block structure +-- | PP horizontally or vertically with "{", ";", and "}" in a possibly multiline block structure, preferring single line horizontal placement ppCurlysSemisBlockH :: PP a => [a] -> PP_Doc ppCurlysSemisBlockH = ppBlockWithStringsH "{" "}" "; " {-# INLINE ppCurlysSemisBlockH #-} @@ -220,7 +221,7 @@ ppCurlysCommasBlock = ppBlockWithStrings "{" "}" ", " {-# INLINE ppCurlysCommasBlock #-} --- | PP horizontally or vertically with "{", ",", and "}" in a possibly multiline block structure +-- | PP horizontally or vertically with "{", ",", and "}" in a possibly multiline block structure, preferring single line horizontal placement ppCurlysCommasBlockH :: PP a => [a] -> PP_Doc ppCurlysCommasBlockH = ppBlockWithStringsH "{" "}" ", " {-# INLINE ppCurlysCommasBlockH #-} @@ -230,7 +231,7 @@ ppParensSemisBlock = ppBlockWithStrings "(" ")" "; " {-# INLINE ppParensSemisBlock #-} --- | PP horizontally or vertically with "(", ";", and ")" in a possibly multiline block structure +-- | PP horizontally or vertically with "(", ";", and ")" in a possibly multiline block structure, preferring single line horizontal placement ppParensSemisBlockH :: PP a => [a] -> PP_Doc ppParensSemisBlockH = ppBlockWithStringsH "(" ")" "; " {-# INLINE ppParensSemisBlockH #-} @@ -240,7 +241,7 @@ ppParensCommasBlock = ppBlockWithStrings "(" ")" ", " {-# INLINE ppParensCommasBlock #-} --- | PP horizontally or vertically with "(", ",", and ")" in a possibly multiline block structure +-- | PP horizontally or vertically with "(", ",", and ")" in a possibly multiline block structure, preferring single line horizontal placement ppParensCommasBlockH :: PP a => [a] -> PP_Doc ppParensCommasBlockH = ppBlockWithStringsH "(" ")" ", " {-# INLINE ppParensCommasBlockH #-} @@ -410,9 +411,12 @@ -- Instances ------------------------------------------------------------------------- -instance PP a => PP (Maybe a) where +instance {-# OVERLAPPABLE #-} PP a => PP (Maybe a) where pp = maybe (pp "?") pp +instance {-# OVERLAPPABLE #-} PP a => PP (Set.Set a) where + pp = ppCurlysCommasBlockH . Set.toList + instance PP Bool where pp = pp . show @@ -421,6 +425,9 @@ instance PP FPath where pp = pp . fpathToStr + +instance PP () where + pp _ = pp "()" instance (PP a, PP b) => PP (a,b) where pp (a,b) = "(" >|< a >-|-< "," >|< b >-|-< ")" diff --git a/src/UHC/Util/RLList/LexScope.hs b/src/UHC/Util/RLList/LexScope.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/RLList/LexScope.hs @@ -0,0 +1,69 @@ +------------------------------------------------------------------------------------------- +--- Run length encoded list, interpretation/usage as encoding of lexical scope +------------------------------------------------------------------------------------------- + +{- | + LexScope represents a lexical scoping, encoded as a list of Int. +-} + +module UHC.Util.RLList.LexScope + ( -- * Lexical scope + LexScope + , enter + , leave + + , isVisibleIn + , common + , parents + + , compareByLength + + -- * Re-export + , module RLL + ) + where + +import UHC.Util.RLList as RLL +import Prelude hiding (concat, null, init, length) +import Data.Maybe + +------------------------------------------------------------------------------------------- +--- Lexical scope: construction +------------------------------------------------------------------------------------------- + +type LexScope = RLList Int + +-- | Enter a new scope +enter :: Int -> LexScope -> LexScope +enter x s = s `concat` singleton x + +-- | Leave a scope, if possible +leave :: LexScope -> Maybe LexScope +leave s = fmap fst $ initLast s + +------------------------------------------------------------------------------------------- +--- Lexical scope: observations +------------------------------------------------------------------------------------------- + +-- | Is scope visible from other scope? +isVisibleIn :: LexScope -> LexScope -> Bool +isVisibleIn sOuter sInner = sOuter `isPrefixOf` sInner + +-- | The common outer scope, which is empty if there is no common scope +common :: LexScope -> LexScope -> LexScope +common s1 s2 + = commonPrefix s1 s2 + where commonPrefix xxs yys + | isJust ht1 && isJust ht2 && x == y = singleton x `concat` commonPrefix xs ys + | otherwise = empty + where ht1@(~(Just (x,xs))) = headTail xxs + ht2@(~(Just (y,ys))) = headTail yys + +-- | All possible parent scopes +parents :: LexScope -> [LexScope] +parents s | not (null s) = inits $ init s +parents _ = [] + +-- | Compare by length +compareByLength :: LexScope -> LexScope -> Ordering +compareByLength s t = length s `compare` length t 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 @@ -74,6 +74,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE UndecidableInstances #-} module UHC.Util.Serialize ( SPut @@ -101,8 +102,10 @@ import Data.Typeable.Internal import qualified Data.Map as Map import qualified Data.Set as Set +import qualified Data.List as List -- import qualified UHC.Utils.RelMap as RelMap import Data.Maybe +import Data.Bits import Data.Word import Data.Int import Data.Array @@ -201,9 +204,11 @@ ; St.put (s { sputsPut = sputsPut s >> p }) } +{-# INLINE liftP #-} liftG :: Bn.Get x -> SGet x liftG g = lift g +{-# INLINE liftG #-} sputPlain :: (Bn.Binary x,Serialize x) => x -> SPut sputPlain x = liftP (Bn.put x) @@ -481,67 +486,70 @@ gsget :: SGet (x y) gsput :: x y -> SPut -instance (Datatype d, SerializeSum x) => GSerialize (D1 d x) where +instance (Datatype d, SerializeSumTagged x) => GSerialize (D1 d x) where -- - gsget = M1 <$> sumGetTagged + gsget = do + tg <- sgetWord8 + M1 <$> sumGetTagged tg -- - gsput (M1 x) = sumPutTagged x + gsput (M1 x) = sumPutTagged [] x -class SerializeSum x where - sumGetTagged :: SGet (x y) - sumPutTagged :: x y -> SPut +class SerializeSumTagged x where + sumGetTagged :: Word8 -> SGet (x y) + sumPutTagged :: [Word8] -> x y -> SPut -instance (SerializeProduct x, Constructor c) => SerializeSum (C1 c x) where +instance (SerializeProduct x) => SerializeSumTagged (C1 c x) where -- - sumGetTagged = M1 <$> productGetMVec + sumGetTagged _ = M1 <$> productGet {-# INLINE sumGetTagged #-} -- - sumPutTagged (M1 x) = productPutMVec x + sumPutTagged tg (M1 x) = sputWord8 (List.foldl' (\acc t -> (acc `shiftL` 1) .|. t) 0 tg) >> productPut x {-# INLINE sumPutTagged #-} -instance (SerializeSum a, SerializeSum b) => SerializeSum (a :+: b) where - sumGetTagged = do - x <- sgetWord8 - case x of - 0 -> L1 <$> sumGetTagged - 1 -> R1 <$> sumGetTagged +instance (SerializeSumTagged a, SerializeSumTagged b) => SerializeSumTagged (a :+: b) where + sumGetTagged tg = + if tg `testBit` 0 + then L1 <$> sumGetTagged tg' + else R1 <$> sumGetTagged tg' + where tg' = tg `shiftR` 1 {-# INLINE sumGetTagged #-} - sumPutTagged (L1 x) = sputWord8 0 >> sumPutTagged x - sumPutTagged (R1 x) = sputWord8 1 >> sumPutTagged x + sumPutTagged tg x = case x of + L1 x' -> sumPutTagged (1:tg) x' + R1 x' -> sumPutTagged (0:tg) x' {-# INLINE sumPutTagged #-} class SerializeProduct x where - productGetMVec :: SGet (x y) - productPutMVec :: x y -> SPut + productGet :: SGet (x y) + productPut :: x y -> SPut instance (SerializeProduct a, SerializeProduct b) => SerializeProduct (a :*: b) where - productGetMVec = - (:*:) <$> productGetMVec - <*> productGetMVec - {-# INLINE productGetMVec #-} + productGet = + (:*:) <$> productGet + <*> productGet + {-# INLINE productGet #-} - productPutMVec (a :*: b) = do - productPutMVec a - productPutMVec b - {-# INLINE productPutMVec #-} + productPut (a :*: b) = do + productPut a + productPut b + {-# INLINE productPut #-} instance SerializeProduct x => SerializeProduct (S1 s x) where - productGetMVec = M1 <$> productGetMVec - {-# INLINE productGetMVec #-} + productGet = M1 <$> productGet + {-# INLINE productGet #-} - productPutMVec (M1 x) = productPutMVec x - {-# INLINE productPutMVec #-} + productPut (M1 x) = productPut x + {-# INLINE productPut #-} instance Serialize x => SerializeProduct (K1 i x) where - productGetMVec = K1 <$> sget - {-# INLINE productGetMVec #-} + productGet = K1 <$> sget + {-# INLINE productGet #-} - productPutMVec (K1 x) = sput x - {-# INLINE productPutMVec #-} + productPut (K1 x) = sput x + {-# INLINE productPut #-} instance SerializeProduct U1 where - productGetMVec = return U1 - {-# INLINE productGetMVec #-} - productPutMVec _ = return () - {-# INLINE productPutMVec #-} + productGet = return U1 + {-# INLINE productGet #-} + productPut _ = return () + {-# INLINE productPut #-} diff --git a/src/UHC/Util/TreeTrie.hs b/src/UHC/Util/TreeTrie.hs --- a/src/UHC/Util/TreeTrie.hs +++ b/src/UHC/Util/TreeTrie.hs @@ -164,7 +164,7 @@ -- | Construct intermediate structure for children for a new Key -- length ks >= 2 -ttkChildren :: [TreeTrieKey k] -> [TreeTrieMpKey k] +ttkChildren :: [TreeTrieKey k] -> TreeTrieKey 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 @@ -174,7 +174,7 @@ 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' :: TreeTrie1Key k -> TreeTrieKey k -> TreeTrieKey k ttkAdd' k ks = [TTM1K [k]] : ks -- | Add a new layer with single node on top, combining the rest. @@ -193,7 +193,7 @@ ------------------------------------------------------------------------------------------- -- | Split key into parent and children components, inverse of ttkAdd' -ttkParentChildren :: TreeTrieKey k -> ( TreeTrie1Key k, [TreeTrieMpKey k] ) +ttkParentChildren :: TreeTrieKey k -> ( TreeTrie1Key k, TreeTrieKey k ) ttkParentChildren k = case k of ([TTM1K [h]] : t) -> (h,t) 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.3 +Version: 0.1.6.5 cabal-version: >= 1.6 License: BSD3 Copyright: Utrecht University, Department of Information and Computing Sciences, Software Technology group @@ -24,7 +24,7 @@ base >= 4.8 && < 5, mtl >= 2, fgl >= 5.4, - hashable >= 1.1, + hashable >= 1.2.4, containers >= 0.4, directory >= 1.1, array >= 0.3, @@ -34,8 +34,9 @@ uulib >= 0.9.19, time-compat >= 0.1.0.1, time >= 1.2, - fclabels >= 2.0.2, - syb >= 0.3.6 + fclabels >= 2.0.3, + syb >= 0.3.6, + logict-state >= 0.1.0.0 Exposed-Modules: UHC.Util.AGraph, UHC.Util.AssocL, @@ -46,6 +47,7 @@ UHC.Util.CHR.Rule, UHC.Util.CHR.Solve.TreeTrie.Mono, UHC.Util.CHR.Solve.TreeTrie.Poly, + UHC.Util.CHR.Solve.TreeTrie.MonoBacktrackPrio, UHC.Util.CompileRun, UHC.Util.CompileRun2, UHC.Util.CompileRun3, @@ -66,6 +68,7 @@ UHC.Util.Rel, UHC.Util.RelMap, UHC.Util.RLList, + UHC.Util.RLList.LexScope, UHC.Util.ScanUtils, UHC.Util.ScopeMapGam, UHC.Util.Serialize,