module Data.Singletons.Map where
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Prelude
import Data.Type.Equality
import Data.Typeable
import Data.Singletons.Class
import Data.Maybe
import Prelude hiding (null, lookup)
import qualified Data.HashMap.Strict as HashMap
import Data.Aeson
import Data.Aeson.Types (Parser)
import Data.Text (Text)
import Data.Hashable
import Data.Vinyl.Core (Rec(..))
import Data.Kind (Type)
data SingMap (k :: Type) (f :: k -> Type) where
Tip :: SingMap k f
Bin :: !Int
-> !(Sing v)
-> !(f v)
-> !(SingMap k f)
-> !(SingMap k f)
-> SingMap k f
type family SingMap' (f :: k -> Type) :: Type where
SingMap' (f :: k -> Type) = SingMap k f
instance (SEq k, SDecide k, EqSing1 f) => Eq (SingMap k f) where
t1 == t2 = (size t1 == size t2) && (toAscList t1 == toAscList t2)
instance (HashableKind k, HashableSing1 f) => Hashable (SingMap k f) where
hashWithSalt i m = hashWithSalt i (toAscList m)
instance (ToJSONKeyKind k, ToJSONSing1 f) => ToJSON (SingMap k f) where
toJSON = Object . foldrWithKey (\s f -> HashMap.insert (toJSONKeyKind s) (toJSONSing1 s f)) HashMap.empty
instance (SOrd k, SDecide k, FromJSONKeyKind k, FromJSONSing1 f) => FromJSON (SingMap k f) where
parseJSON = withObject "SingMap k a" $ fmap fromList . mapM parseSingWith . HashMap.toList
where
parseSingWith :: (Text,Value) -> Parser (SomeSingWith1 k f)
parseSingWith (t,v) = do
SomeSing s :: SomeSing k <- parseJSONKeyKind t
pv <- parseJSONSing1 s v
return (SomeSingWith1 s pv)
empty :: SingMap k f
empty = Tip
singleton :: Sing v -> f v -> SingMap k f
singleton k x = Bin 1 k x Tip Tip
null :: SingMap k f -> Bool
null Tip = True
null Bin{} = False
size :: SingMap k f -> Int
size Tip = 0
size (Bin n _ _ _ _) = n
lookup :: forall k f v. (SOrd k, SDecide k) => Sing v -> SingMap k f -> Maybe (f v)
lookup k = k `seq` go
where
go :: SingMap k f -> Maybe (f v)
go Tip = Nothing
go (Bin _ kx x l r) =
case sCompare k kx of
SLT -> go l
SGT -> go r
SEQ -> case testEquality k kx of
Nothing -> error "lookup: inconsistent SOrd and SDecide instances"
Just Refl -> Just x
lookupAssoc :: forall k f v. (SOrd k, SDecide k) => SomeSing k -> SingMap k f -> Maybe (SomeSingWith1 k f)
lookupAssoc (SomeSing k) = k `seq` go
where
go :: SingMap k f -> Maybe (SomeSingWith1 k f)
go Tip = Nothing
go (Bin _ kx x l r) =
case sCompare k kx of
SLT -> go l
SGT -> go r
SEQ -> case testEquality k kx of
Nothing -> error "lookupAssoc: inconsistent SOrd and SDecide instances"
Just Refl -> Just (SomeSingWith1 kx x)
combine :: (SOrd k, SDecide k) => Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
combine kx x Tip r = insertMin kx x r
combine kx x l Tip = insertMax kx x l
combine kx x l@(Bin sizeL ky y ly ry) r@(Bin sizeR kz z lz rz)
| delta*sizeL <= sizeR = balance kz z (combine kx x l lz) rz
| delta*sizeR <= sizeL = balance ky y ly (combine kx x ry r)
| otherwise = bin kx x l r
insertMax,insertMin :: Sing v -> f v -> SingMap k f -> SingMap k f
insertMax kx x t
= case t of
Tip -> singleton kx x
Bin _ ky y l r
-> balance ky y l (insertMax kx x r)
insertMin kx x t
= case t of
Tip -> singleton kx x
Bin _ ky y l r
-> balance ky y (insertMin kx x l) r
merge :: SOrd k => SingMap k f -> SingMap k f -> SingMap k f
merge Tip r = r
merge l Tip = l
merge l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry)
| delta*sizeL <= sizeR = balance ky y (merge l ly) ry
| delta*sizeR <= sizeL = balance kx x lx (merge rx r)
| otherwise = glue l r
glue :: SingMap k f -> SingMap k f -> SingMap k f
glue Tip r = r
glue l Tip = l
glue l r
| size l > size r = case deleteFindMax l of (SomeSingWith1 km m,l') -> balance km m l' r
| otherwise = case deleteFindMin r of (SomeSingWith1 km m,r') -> balance km m l r'
deleteFindMin :: SingMap k f -> (SomeSingWith1 k f, SingMap k f)
deleteFindMin t
= case t of
Bin _ k x Tip r -> (SomeSingWith1 k x ,r)
Bin _ k x l r -> let (km,l') = deleteFindMin l in (km,balance k x l' r)
Tip -> (error "Map.deleteFindMin: can not return the minimal element of an empty map", Tip)
deleteFindMax :: SingMap k f -> (SomeSingWith1 k f, SingMap k f)
deleteFindMax t
= case t of
Bin _ k x l Tip -> (SomeSingWith1 k x,l)
Bin _ k x l r -> let (km,r') = deleteFindMax r in (km,balance k x l r')
Tip -> (error "Map.deleteFindMax: can not return the maximal element of an empty map", Tip)
delta,ratio :: Int
delta = 4
ratio = 2
balance :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
balance k x l r
| sizeL + sizeR <= 1 = Bin sizeX k x l r
| sizeR >= delta*sizeL = rotateL k x l r
| sizeL >= delta*sizeR = rotateR k x l r
| otherwise = Bin sizeX k x l r
where
sizeL = size l
sizeR = size r
sizeX = sizeL + sizeR + 1
rotateL :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
rotateL k x l r@(Bin _ _ _ ly ry)
| size ly < ratio*size ry = singleL k x l r
| otherwise = doubleL k x l r
rotateL _ _ _ Tip = error "rotateL Tip"
rotateR :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
rotateR k x l@(Bin _ _ _ ly ry) r
| size ry < ratio*size ly = singleR k x l r
| otherwise = doubleR k x l r
rotateR _ _ Tip _ = error "rotateR Tip"
singleL, singleR :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
singleL k1 x1 t1 (Bin _ k2 x2 t2 t3) = bin k2 x2 (bin k1 x1 t1 t2) t3
singleL _ _ _ Tip = error "singleL Tip"
singleR k1 x1 (Bin _ k2 x2 t1 t2) t3 = bin k2 x2 t1 (bin k1 x1 t2 t3)
singleR _ _ Tip _ = error "singleR Tip"
doubleL, doubleR :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
doubleL k1 x1 t1 (Bin _ k2 x2 (Bin _ k3 x3 t2 t3) t4) = bin k3 x3 (bin k1 x1 t1 t2) (bin k2 x2 t3 t4)
doubleL _ _ _ _ = error "doubleL"
doubleR k1 x1 (Bin _ k2 x2 t1 (Bin _ k3 x3 t2 t3)) t4 = bin k3 x3 (bin k2 x2 t1 t2) (bin k1 x1 t3 t4)
doubleR _ _ _ _ = error "doubleR"
bin :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
bin k x l r
= Bin (size l + size r + 1) k x l r
trim :: SOrd k => (SomeSing k -> Ordering) -> (SomeSing k -> Ordering) -> SingMap k f -> SingMap k f
trim _ _ Tip = Tip
trim cmplo cmphi t@(Bin _ kx _ l r)
= case cmplo (SomeSing kx) of
LT -> case cmphi (SomeSing kx) of
GT -> t
_ -> trim cmplo cmphi l
_ -> trim cmplo cmphi r
trimLookupLo :: (SOrd k, SDecide k) => SomeSing k -> (SomeSing k -> Ordering) -> SingMap k f -> (Maybe (SomeSingWith1 k f), SingMap k f)
trimLookupLo _ _ Tip = (Nothing,Tip)
trimLookupLo lo cmphi t@(Bin _ kx x l r)
= case compareSome lo (SomeSing kx) of
LT -> case cmphi (SomeSing kx) of
GT -> (lookupAssoc lo t, t)
_ -> trimLookupLo lo cmphi l
GT -> trimLookupLo lo cmphi r
EQ -> (Just (SomeSingWith1 kx x),trim (compareSome lo) cmphi r)
filterGt :: (SOrd k, SDecide k) => (SomeSing k -> Ordering) -> SingMap k f -> SingMap k f
filterGt cmp = go
where
go Tip = Tip
go (Bin _ kx x l r) = case cmp (SomeSing kx) of
LT -> combine kx x (go l) r
GT -> go r
EQ -> r
filterLt :: (SOrd k, SDecide k) => (SomeSing k -> Ordering) -> SingMap k f -> SingMap k f
filterLt cmp = go
where
go Tip = Tip
go (Bin _ kx x l r) = case cmp (SomeSing kx) of
LT -> go l
GT -> combine kx x l (go r)
EQ -> l
infixl 9 !,\\
(!) :: (SOrd k, SDecide k) => SingMap k f -> Sing v -> f v
(!) m k = find k m
(\\) :: (SOrd k, SDecide k) => SingMap k f -> SingMap k f -> SingMap k f
m1 \\ m2 = difference m1 m2
member :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> Bool
member k = isJust . lookup k
notMember :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> Bool
notMember k m = not (member k m)
find :: (SOrd k, SDecide k) => Sing v -> SingMap k f -> f v
find k m = case lookup k m of
Nothing -> error "SingMap.find: element not in the map"
Just v -> v
findWithDefault :: (SOrd k, SDecide k) => f v -> Sing v -> SingMap k f -> f v
findWithDefault def k m = case lookup k m of
Nothing -> def
Just v -> v
insert :: forall k f v. (SOrd k, SDecide k) => Sing v -> f v -> SingMap k f -> SingMap k f
insert kx x = kx `seq` go
where
go :: SingMap k f -> SingMap k f
go Tip = singleton kx x
go (Bin sz ky y l r) = case sCompare kx ky of
SLT -> balance ky y (go l) r
SGT -> balance ky y l (go r)
SEQ -> Bin sz kx x l r
insertWith :: (SOrd k, SDecide k) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap k f -> SingMap k f
insertWith f = insertWithKey (\_ x' y' -> f x' y')
insertWith' :: (SOrd k, SDecide k) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap k f -> SingMap k f
insertWith' f = insertWithKey' (\_ x' y' -> f x' y')
insertWithKey :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap k f -> SingMap k f
insertWithKey f kx x = kx `seq` go
where
go :: SingMap k f -> SingMap k f
go Tip = singleton kx x
go (Bin sy ky y l r) =
case sCompare kx ky of
SLT -> balance ky y (go l) r
SGT -> balance ky y l (go r)
SEQ -> unifyOnCompareEQ kx ky (Bin sy kx (f kx x y) l r)
insertWithKey' :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap k f -> SingMap k f
insertWithKey' f kx x = kx `seq` go
where
go :: SingMap k f -> SingMap k f
go Tip = singleton kx $! x
go (Bin sy ky y l r) =
case sCompare kx ky of
SLT -> balance ky y (go l) r
SGT -> balance ky y l (go r)
SEQ -> unifyOnCompareEQ kx ky (let x' = f kx x y in seq x' (Bin sy kx x' l r))
insertLookupWithKey :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap k f
-> (Maybe (f v), SingMap k f)
insertLookupWithKey f kx x = kx `seq` go
where
go :: SingMap k f -> (Maybe (f v), SingMap k f)
go Tip = (Nothing, singleton kx x)
go (Bin sy ky y l r) =
case sCompare kx ky of
SLT -> let (found, l') = go l
in (found, balance ky y l' r)
SGT -> let (found, r') = go r
in (found, balance ky y l r')
SEQ -> unifyOnCompareEQ kx ky (Just y, Bin sy kx (f kx x y) l r)
insertLookupWithKey' :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap k f
-> (Maybe (f v), SingMap k f)
insertLookupWithKey' f kx x = kx `seq` go
where
go :: SingMap k f -> (Maybe (f v), SingMap k f)
go Tip = x `seq` (Nothing, singleton kx x)
go (Bin sy ky y l r) =
case sCompare kx ky of
SLT -> let (found, l') = go l
in (found, balance ky y l' r)
SGT -> let (found, r') = go r
in (found, balance ky y l r')
SEQ -> unifyOnCompareEQ kx ky (let x' = f kx x y in x' `seq` (Just y, Bin sy kx x' l r))
delete :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> SingMap k f
delete k = k `seq` go
where
go :: SingMap k f -> SingMap k f
go Tip = Tip
go (Bin _ kx x l r) =
case sCompare k kx of
SLT -> balance kx x (go l) r
SGT -> balance kx x l (go r)
SEQ -> unifyOnCompareEQ k kx (glue l r)
adjust :: (SOrd k, SDecide k) => (f v -> f v) -> Sing v -> SingMap k f -> SingMap k f
adjust f = adjustWithKey (\_ x -> f x)
adjustWithKey :: (SOrd k, SDecide k) => (Sing v -> f v -> f v) -> Sing v -> SingMap k f -> SingMap k f
adjustWithKey f = updateWithKey (\k' x' -> Just (f k' x'))
update :: (SOrd k, SDecide k) => (f v -> Maybe (f v)) -> Sing v -> SingMap k f -> SingMap k f
update f = updateWithKey (\_ x -> f x)
updateWithKey :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap k f -> SingMap k f
updateWithKey f k = k `seq` go
where
go :: SingMap k f -> SingMap k f
go Tip = Tip
go (Bin sx kx x l r) =
case sCompare k kx of
SLT -> balance kx x (go l) r
SGT -> balance kx x l (go r)
SEQ -> unifyOnCompareEQ k kx $ case f kx x of
Just x' -> Bin sx kx x' l r
Nothing -> glue l r
updateLookupWithKey :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap k f -> (Maybe (f v), SingMap k f)
updateLookupWithKey f k = k `seq` go
where
go :: SingMap k f -> (Maybe (f v), SingMap k f)
go Tip = (Nothing,Tip)
go (Bin sx kx x l r) =
case sCompare k kx of
SLT -> let (found,l') = go l in (found,balance kx x l' r)
SGT -> let (found,r') = go r in (found,balance kx x l r')
SEQ -> unifyOnCompareEQ k kx $ case f kx x of
Just x' -> (Just x',Bin sx kx x' l r)
Nothing -> (Just x,glue l r)
alter :: forall k f v. (SOrd k, SDecide k) => (Maybe (f v) -> Maybe (f v)) -> Sing v -> SingMap k f -> SingMap k f
alter f k = k `seq` go
where
go :: SingMap k f -> SingMap k f
go Tip = case f Nothing of
Nothing -> Tip
Just x -> singleton k x
go (Bin sx kx x l r) = case sCompare k kx of
SLT -> balance kx x (go l) r
SGT -> balance kx x l (go r)
SEQ -> unifyOnCompareEQ k kx $ case f (Just x) of
Just x' -> Bin sx kx x' l r
Nothing -> glue l r
findIndex :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> Int
findIndex k t
= case lookupIndex k t of
Nothing -> error "Map.findIndex: element is not in the map"
Just idx -> idx
lookupIndex :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> Maybe Int
lookupIndex k = k `seq` go 0
where
go :: Int -> SingMap k f -> Maybe Int
go !idx Tip = idx `seq` Nothing
go !idx (Bin _ kx _ l r)
= case sCompare k kx of
SLT -> go idx l
SGT -> go (idx + size l + 1) r
SEQ -> Just (idx + size l)
elemAt :: Int -> SingMap k f -> SomeSingWith1 k f
elemAt _ Tip = error "Map.elemAt: index out of range"
elemAt i (Bin _ kx x l r)
= case compare i sizeL of
LT -> elemAt i l
GT -> elemAt (isizeL1) r
EQ -> SomeSingWith1 kx x
where
sizeL = size l
updateAt :: (forall v. Sing v -> f v -> Maybe (f v)) -> Int -> SingMap k f -> SingMap k f
updateAt f i0 t = i0 `seq` go i0 t
where
go _ Tip = error "Map.updateAt: index out of range"
go i (Bin sx kx x l r) = case compare i sizeL of
LT -> balance kx x (go i l) r
GT -> balance kx x l (go (isizeL1) r)
EQ -> case f kx x of
Just x' -> Bin sx kx x' l r
Nothing -> glue l r
where
sizeL = size l
deleteAt :: Int -> SingMap k f -> SingMap k f
deleteAt i m
= updateAt (\_ _ -> Nothing) i m
findMin :: SingMap k f -> SomeSingWith1 k f
findMin (Bin _ kx x Tip _) = SomeSingWith1 kx x
findMin (Bin _ _ _ l _) = findMin l
findMin Tip = error "Map.findMin: empty map has no minimal element"
findMax :: SingMap k f -> SomeSingWith1 k f
findMax (Bin _ kx x _ Tip) = SomeSingWith1 kx x
findMax (Bin _ _ _ _ r) = findMax r
findMax Tip = error "Map.findMax: empty map has no maximal element"
deleteMin :: SingMap k f -> SingMap k f
deleteMin (Bin _ _ _ Tip r) = r
deleteMin (Bin _ kx x l r) = balance kx x (deleteMin l) r
deleteMin Tip = Tip
deleteMax :: SingMap k f -> SingMap k f
deleteMax (Bin _ _ _ l Tip) = l
deleteMax (Bin _ kx x l r) = balance kx x l (deleteMax r)
deleteMax Tip = Tip
updateMinWithKey :: (forall v. Sing v -> f v -> Maybe (f v)) -> SingMap k f -> SingMap k f
updateMinWithKey f = go
where
go (Bin sx kx x Tip r) = case f kx x of
Nothing -> r
Just x' -> Bin sx kx x' Tip r
go (Bin _ kx x l r) = balance kx x (go l) r
go Tip = Tip
updateMaxWithKey :: (forall v. Sing v -> f v -> Maybe (f v)) -> SingMap k f -> SingMap k f
updateMaxWithKey f = go
where
go (Bin sx kx x l Tip) = case f kx x of
Nothing -> l
Just x' -> Bin sx kx x' l Tip
go (Bin _ kx x l r) = balance kx x l (go r)
go Tip = Tip
minViewWithKey :: SingMap k f -> Maybe (SomeSingWith1 k f, SingMap k f)
minViewWithKey Tip = Nothing
minViewWithKey x = Just (deleteFindMin x)
maxViewWithKey :: SingMap k f -> Maybe (SomeSingWith1 k f, SingMap k f)
maxViewWithKey Tip = Nothing
maxViewWithKey x = Just (deleteFindMax x)
unions :: (SOrd k, SDecide k) => [SingMap k f] -> SingMap k f
unions ts
= foldlStrict union empty ts
unionsWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> [SingMap k f] -> SingMap k f
unionsWithKey f ts
= foldlStrict (unionWithKey f) empty ts
union :: (SOrd k, SDecide k) => SingMap k f -> SingMap k f -> SingMap k f
union Tip t2 = t2
union t1 Tip = t1
union t1 t2 = hedgeUnionL (const LT) (const GT) t1 t2
hedgeUnionL :: (SOrd k, SDecide k)
=> (SomeSing k -> Ordering) -> (SomeSing k -> Ordering) -> SingMap k f -> SingMap k f
-> SingMap k f
hedgeUnionL _ _ t1 Tip
= t1
hedgeUnionL cmplo cmphi Tip (Bin _ kx x l r)
= combine kx x (filterGt cmplo l) (filterLt cmphi r)
hedgeUnionL cmplo cmphi (Bin _ kx x l r) t2
= combine kx x (hedgeUnionL cmplo cmpkx l (trim cmplo cmpkx t2))
(hedgeUnionL cmpkx cmphi r (trim cmpkx cmphi t2))
where
cmpkx k = compareSome (SomeSing kx) k
unionWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap k f -> SingMap k f -> SingMap k f
unionWithKey _ Tip t2 = t2
unionWithKey _ t1 Tip = t1
unionWithKey f t1 t2 = hedgeUnionWithKey f (const LT) (const GT) t1 t2
hedgeUnionWithKey :: forall k f. (SOrd k, SDecide k)
=> (forall v. Sing v -> f v -> f v -> f v)
-> (SomeSing k -> Ordering) -> (SomeSing k -> Ordering)
-> SingMap k f -> SingMap k f
-> SingMap k f
hedgeUnionWithKey _ _ _ t1 Tip
= t1
hedgeUnionWithKey _ cmplo cmphi Tip (Bin _ kx x l r)
= combine kx x (filterGt cmplo l) (filterLt cmphi r)
hedgeUnionWithKey f cmplo cmphi (Bin _ (kx :: Sing tx) x l r) t2
= combine kx newx (hedgeUnionWithKey f cmplo cmpkx l lt)
(hedgeUnionWithKey f cmpkx cmphi r gt)
where
cmpkx k = compareSome (SomeSing kx) k
lt = trim cmplo cmpkx t2
(found,gt) = trimLookupLo (SomeSing kx) cmphi t2
newx :: f tx
newx = case found of
Nothing -> x
Just (SomeSingWith1 ky y) -> case kx %:== ky of
STrue -> unifyOnEq kx ky (f kx x y)
SFalse -> error "SingMap.union: inconsistent SEq instance"
difference :: (SOrd k, SDecide k) => SingMap k f -> SingMap k g -> SingMap k f
difference Tip _ = Tip
difference t1 Tip = t1
difference t1 t2 = hedgeDiff (const LT) (const GT) t1 t2
hedgeDiff :: (SOrd k, SDecide k)
=> (SomeSing k -> Ordering) -> (SomeSing k -> Ordering) -> SingMap k f -> SingMap k g
-> SingMap k f
hedgeDiff _ _ Tip _
= Tip
hedgeDiff cmplo cmphi (Bin _ kx x l r) Tip
= combine kx x (filterGt cmplo l) (filterLt cmphi r)
hedgeDiff cmplo cmphi t (Bin _ kx _ l r)
= merge (hedgeDiff cmplo cmpkx (trim cmplo cmpkx t) l)
(hedgeDiff cmpkx cmphi (trim cmpkx cmphi t) r)
where
cmpkx k = compareSome (SomeSing kx) k
differenceWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> g v -> Maybe (f v)) -> SingMap k f -> SingMap k g -> SingMap k f
differenceWithKey _ Tip _ = Tip
differenceWithKey _ t1 Tip = t1
differenceWithKey f t1 t2 = hedgeDiffWithKey f (const LT) (const GT) t1 t2
hedgeDiffWithKey :: (SOrd k, SDecide k)
=> (forall v. Sing v -> f v -> g v -> Maybe (f v))
-> (SomeSing k -> Ordering) -> (SomeSing k -> Ordering)
-> SingMap k f -> SingMap k g
-> SingMap k f
hedgeDiffWithKey _ _ _ Tip _
= Tip
hedgeDiffWithKey _ cmplo cmphi (Bin _ kx x l r) Tip
= combine kx x (filterGt cmplo l) (filterLt cmphi r)
hedgeDiffWithKey f cmplo cmphi t (Bin _ kx x l r)
= case found of
Nothing -> merge tl tr
Just (SomeSingWith1 ky y) ->
case kx %:== ky of
SFalse -> error "SingMap.difference: inconsistent SEq instance"
STrue -> unifyOnEq kx ky $
case f ky y x of
Nothing -> merge tl tr
Just z -> combine ky z tl tr
where
cmpkx k = compareSome (SomeSing kx) k
lt = trim cmplo cmpkx t
(found,gt) = trimLookupLo (SomeSing kx) cmphi t
tl = hedgeDiffWithKey f cmplo cmpkx lt l
tr = hedgeDiffWithKey f cmpkx cmphi gt r
intersection :: (SOrd k, SDecide k) => SingMap k f -> SingMap k f -> SingMap k f
intersection m1 m2
= intersectionWithKey (\_ x _ -> x) m1 m2
intersectionWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> g v -> h v) -> SingMap k f -> SingMap k g -> SingMap k h
intersectionWithKey _ Tip _ = Tip
intersectionWithKey _ _ Tip = Tip
intersectionWithKey f t1@(Bin s1 k1 x1 l1 r1) t2@(Bin s2 k2 x2 l2 r2) =
if s1 >= s2 then
let (lt,found,gt) = splitLookupWithKey k2 t1
tl = intersectionWithKey f lt l2
tr = intersectionWithKey f gt r2
in case found of
Just (k,x) -> combine k (f k x x2) tl tr
Nothing -> merge tl tr
else let (lt,found,gt) = splitLookup k1 t2
tl = intersectionWithKey f l1 lt
tr = intersectionWithKey f r1 gt
in case found of
Just x -> combine k1 (f k1 x1 x) tl tr
Nothing -> merge tl tr
filterWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> Bool) -> SingMap k f -> SingMap k f
filterWithKey p = go
where
go Tip = Tip
go (Bin _ kx x l r)
| p kx x = combine kx x (go l) (go r)
| otherwise = merge (go l) (go r)
partitionWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> Bool) -> SingMap k f -> (SingMap k f, SingMap k f)
partitionWithKey _ Tip = (Tip,Tip)
partitionWithKey p (Bin _ kx x l r)
| p kx x = (combine kx x l1 r1,merge l2 r2)
| otherwise = (merge l1 r1,combine kx x l2 r2)
where
(l1,l2) = partitionWithKey p l
(r1,r2) = partitionWithKey p r
mapMaybeWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> Maybe (g v)) -> SingMap k f -> SingMap k g
mapMaybeWithKey f = go
where
go Tip = Tip
go (Bin _ kx x l r) = case f kx x of
Just y -> combine kx y (go l) (go r)
Nothing -> merge (go l) (go r)
mapEitherWithKey :: (SOrd k, SDecide k) =>
(forall v. Sing v -> f v -> Either (g v) (h v)) -> SingMap k f -> (SingMap k g, SingMap k h)
mapEitherWithKey _ Tip = (Tip, Tip)
mapEitherWithKey f (Bin _ kx x l r) = case f kx x of
Left y -> (combine kx y l1 r1, merge l2 r2)
Right z -> (merge l1 r1, combine kx z l2 r2)
where
(l1,l2) = mapEitherWithKey f l
(r1,r2) = mapEitherWithKey f r
mapWithKey :: (forall v. Sing v -> f v -> g v) -> SingMap k f -> SingMap k g
mapWithKey f = go
where
go Tip = Tip
go (Bin sx kx x l r) = Bin sx kx (f kx x) (go l) (go r)
mapAccumLWithKey :: (forall v. a -> Sing v -> f v -> (a, g v)) -> a -> SingMap k f -> (a, SingMap k g)
mapAccumLWithKey f = go
where
go a Tip = (a,Tip)
go a (Bin sx kx x l r) =
let (a1,l') = go a l
(a2,x') = f a1 kx x
(a3,r') = go a2 r
in (a3,Bin sx kx x' l' r')
mapAccumRWithKey :: (forall v. a -> Sing v -> f v -> (a, g v)) -> a -> SingMap k f -> (a, SingMap k g)
mapAccumRWithKey f = go
where
go a Tip = (a,Tip)
go a (Bin sx kx x l r) =
let (a1,r') = go a r
(a2,x') = f a1 kx x
(a3,l') = go a2 l
in (a3,Bin sx kx x' l' r')
foldWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap k f -> b
foldWithKey = foldrWithKey
foldrWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap k f -> b
foldrWithKey f = go
where
go z Tip = z
go z (Bin _ kx x l r) = go (f kx x (go z r)) l
foldlWithKey :: (forall v. b -> Sing v -> f v -> b) -> b -> SingMap k f -> b
foldlWithKey f = go
where
go z Tip = z
go z (Bin _ kx x l r) = go (f (go z l) kx x) r
keys :: SingMap k f -> [SomeSing k]
keys m
= [SomeSing k | (SomeSingWith1 k _) <- assocs m]
assocs :: SingMap k f -> [SomeSingWith1 k f]
assocs m
= toList m
fromList :: (SOrd k, SDecide k) => [SomeSingWith1 k f] -> SingMap k f
fromList xs
= foldlStrict ins empty xs
where
ins :: (SOrd k, SDecide k) => SingMap k f -> SomeSingWith1 k f -> SingMap k f
ins t (SomeSingWith1 k x) = insert k x t
fromListWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 k f] -> SingMap k f
fromListWithKey f xs
= foldlStrict (ins f) empty xs
where
ins :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap k f -> SomeSingWith1 k f -> SingMap k f
ins f t (SomeSingWith1 k x) = insertWithKey f k x t
toList :: SingMap k f -> [SomeSingWith1 k f]
toList t = toAscList t
toAscList :: SingMap k f -> [SomeSingWith1 k f]
toAscList t = foldrWithKey (\k x xs -> (SomeSingWith1 k x):xs) [] t
toDescList :: SingMap k f -> [SomeSingWith1 k f]
toDescList t = foldlWithKey (\xs k x -> (SomeSingWith1 k x):xs) [] t
fromAscList :: (SEq k, SDecide k) => [SomeSingWith1 k f] -> SingMap k f
fromAscList xs
= fromAscListWithKey (\_ x _ -> x) xs
fromAscListWithKey :: (SEq k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 k f] -> SingMap k f
fromAscListWithKey f xs
= fromDistinctAscList (combineEq f xs)
where
combineEq _ xs'
= case xs' of
[] -> []
[x] -> [x]
(x:xx) -> combineEq' f x xx
combineEq' :: (SEq k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> SomeSingWith1 k f -> [SomeSingWith1 k f] -> [SomeSingWith1 k f]
combineEq' f z [] = [z]
combineEq' f z@(SomeSingWith1 kz zz) (x@(SomeSingWith1 kx xx):xs') =
case kx %:== kz of
STrue -> unifyOnEq kx kz (let yy = f kx xx zz in combineEq' f (SomeSingWith1 kx yy) xs')
SFalse -> z : combineEq' f x xs'
fromDistinctAscList :: [SomeSingWith1 k f] -> SingMap k f
fromDistinctAscList xs
= build const (length xs) xs
where
build :: (SingMap k f -> [SomeSingWith1 k f] -> b) -> Int -> [SomeSingWith1 k f] -> b
build c 0 xs' = c Tip xs'
build c 5 xs' = case xs' of
((SomeSingWith1 k1 x1):(SomeSingWith1 k2 x2):(SomeSingWith1 k3 x3):(SomeSingWith1 k4 x4):(SomeSingWith1 k5 x5):xx)
-> c (bin k4 x4 (bin k2 x2 (singleton k1 x1) (singleton k3 x3)) (singleton k5 x5)) xx
_ -> error "fromDistinctAscList build"
build c n xs' = seq nr $ build (buildR nr c) nl xs'
where
nl = n `div` 2
nr = n nl 1
buildR :: Int -> (SingMap k f -> [SomeSingWith1 k f] -> b) -> SingMap k f -> [SomeSingWith1 k f] -> b
buildR n c l (SomeSingWith1 k x : ys) = build (buildB l k x c) n ys
buildR _ _ _ [] = error "fromDistinctAscList buildR []"
buildB :: SingMap k f -> Sing v -> f v -> (SingMap k f -> a -> b) -> SingMap k f -> a -> b
buildB l k x c r zs = c (bin k x l r) zs
split :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> (SingMap k f, SingMap k f)
split k = go
where
go :: SingMap k f -> (SingMap k f, SingMap k f)
go Tip = (Tip, Tip)
go (Bin _ kx x l r) = case sCompare k kx of
SLT -> let (lt,gt) = go l in (lt,combine kx x gt r)
SGT -> let (lt,gt) = go r in (combine kx x l lt,gt)
SEQ -> unifyOnCompareEQ k kx (l,r)
splitLookup :: forall k f v. (SOrd k, SDecide k) => Sing v -> SingMap k f -> (SingMap k f, Maybe (f v), SingMap k f)
splitLookup k = go
where
go :: SingMap k f -> (SingMap k f, Maybe (f v), SingMap k f)
go Tip = (Tip,Nothing,Tip)
go (Bin _ kx x l r) = case sCompare k kx of
SLT -> let (lt,z,gt) = go l in (lt,z,combine kx x gt r)
SGT -> let (lt,z,gt) = go r in (combine kx x l lt,z,gt)
SEQ -> unifyOnCompareEQ k kx (l,Just x,r)
splitLookupWithKey :: forall k f v. (SOrd k, SDecide k) => Sing v -> SingMap k f -> (SingMap k f, Maybe (Sing v, f v), SingMap k f)
splitLookupWithKey k = go
where
go :: SingMap k f -> (SingMap k f, Maybe (Sing v, f v), SingMap k f)
go Tip = (Tip,Nothing,Tip)
go (Bin _ kx x l r) = case sCompare k kx of
SLT -> let (lt,z,gt) = go l in (lt,z,combine kx x gt r)
SGT -> let (lt,z,gt) = go r in (combine kx x l lt,z,gt)
SEQ -> unifyOnCompareEQ k kx (l,Just (kx, x),r)
showTreeWith :: (forall v. Sing v -> f v -> String) -> Bool -> Bool -> SingMap k f -> String
showTreeWith showelem hang wide t
| hang = (showsTreeHang showelem wide [] t) ""
| otherwise = (showsTree showelem wide [] [] t) ""
showsTree :: (forall v. Sing v -> f v -> String) -> Bool -> [String] -> [String] -> SingMap k f -> ShowS
showsTree showelem wide lbars rbars t
= case t of
Tip -> showsBars lbars . showString "|\n"
Bin _ kx x Tip Tip
-> showsBars lbars . showString (showelem kx x) . showString "\n"
Bin _ kx x l r
-> showsTree showelem wide (withBar rbars) (withEmpty rbars) r .
showWide wide rbars .
showsBars lbars . showString (showelem kx x) . showString "\n" .
showWide wide lbars .
showsTree showelem wide (withEmpty lbars) (withBar lbars) l
showsTreeHang :: (forall v. Sing v -> f v -> String) -> Bool -> [String] -> SingMap k f -> ShowS
showsTreeHang showelem wide bars t
= case t of
Tip -> showsBars bars . showString "|\n"
Bin _ kx x Tip Tip
-> showsBars bars . showString (showelem kx x) . showString "\n"
Bin _ kx x l r
-> showsBars bars . showString (showelem kx x) . showString "\n" .
showWide wide bars .
showsTreeHang showelem wide (withBar bars) l .
showWide wide bars .
showsTreeHang showelem wide (withEmpty bars) r
showWide :: Bool -> [String] -> String -> String
showWide wide bars
| wide = showString (concat (reverse bars)) . showString "|\n"
| otherwise = id
showsBars :: [String] -> ShowS
showsBars bars
= case bars of
[] -> id
_ -> showString (concat (reverse (tail bars))) . showString node
node :: String
node = "+--"
withBar, withEmpty :: [String] -> [String]
withBar bars = "| ":bars
withEmpty bars = " ":bars
valid :: (SOrd k, SDecide k) => SingMap k f -> Bool
valid t
= balanced t && ordered t && validsize t
ordered :: (SOrd k, SDecide k) => SingMap k f -> Bool
ordered t
= bounded (const True) (const True) t
where
bounded :: (SOrd k, SDecide k) => (SomeSing k -> Bool) -> (SomeSing k -> Bool) -> SingMap k f -> Bool
bounded lo hi t'
= case t' of
Tip -> True
Bin _ kx _ l r -> (lo (SomeSing kx))
&& (hi (SomeSing kx))
&& bounded lo (`ltSome` SomeSing kx) l
&& bounded (`gtSome` SomeSing kx) hi r
balanced :: SingMap k f -> Bool
balanced t
= case t of
Tip -> True
Bin _ _ _ l r -> (size l + size r <= 1 || (size l <= delta*size r && size r <= delta*size l)) &&
balanced l && balanced r
validsize :: SingMap k f -> Bool
validsize t
= (realsize t == Just (size t))
where
realsize t'
= case t' of
Tip -> Just 0
Bin sz _ _ l r -> case (realsize l,realsize r) of
(Just n,Just m) | n+m+1 == sz -> Just sz
_ -> Nothing
foldlStrict :: (a -> b -> a) -> a -> [b] -> a
foldlStrict f = go
where
go z [] = z
go z (x:xs) = z `seq` go (f z x) xs
ltSome :: SOrd k => SomeSing k -> SomeSing k -> Bool
ltSome (SomeSing a) (SomeSing b) = fromSing (a %:< b)
gtSome :: SOrd k => SomeSing k -> SomeSing k -> Bool
gtSome (SomeSing a) (SomeSing b) = fromSing (a %:> b)
unifyOnCompareEQ :: forall k (a :: k) (b :: k) x.
(SDecide k, Compare a b ~ 'EQ)
=> Sing a -> Sing b -> (a ~ b => x) -> x
unifyOnCompareEQ a b x =
case testEquality a b of
Nothing -> error "unifyOnCompareEQ: inconsistent SOrd and SDecide instances"
Just Refl -> x
unifyOnEq :: forall k (a :: k) (b :: k) x.
(SDecide k, (a :== b) ~ 'True)
=> Sing a -> Sing b -> (a ~ b => x) -> x
unifyOnEq a b x =
case testEquality a b of
Nothing -> error "unifyOnEq: inconsistent SEq and SDecide instances"
Just Refl -> x
fromRec :: (SOrd k, SDecide k) => Rec (SingWith1 k f) rs -> SingMap k f
fromRec r = insertRec r empty
insertRec :: (SOrd k, SDecide k) => Rec (SingWith1 k f) rs -> SingMap k f -> SingMap k f
insertRec RNil m = m
insertRec (SingWith1 s v :& rs) m = insert s v (insertRec rs m)