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
data SingMap (kproxy :: KProxy j) (f :: j -> *) where
Tip :: SingMap kproxy f
Bin :: !Int
-> !(Sing v)
-> !(f v)
-> !(SingMap kproxy f)
-> !(SingMap kproxy f)
-> SingMap kproxy f
type SingMap' = SingMap 'KProxy
instance (SEq kproxy, SDecide kproxy, EqSing1 f) => Eq (SingMap kproxy f) where
t1 == t2 = (size t1 == size t2) && (toAscList t1 == toAscList t2)
instance (HashableKind kproxy, HashableSing1 f) => Hashable (SingMap kproxy f) where
hashWithSalt i m = hashWithSalt i (toAscList m)
instance (ToJSONKeyKind kproxy, ToJSONSing1 f) => ToJSON (SingMap kproxy f) where
toJSON = Object . foldrWithKey (\s f -> HashMap.insert (toJSONKeyKind s) (toJSONSing1 s f)) HashMap.empty
instance (SOrd kproxy, SDecide kproxy, FromJSONKeyKind kproxy, FromJSONSing1 f) => FromJSON (SingMap kproxy f) where
parseJSON = withObject "SingMap kproxy a" $ fmap fromList . mapM parseSingWith . HashMap.toList
where
parseSingWith :: (Text,Value) -> Parser (SomeSingWith1 kproxy f)
parseSingWith (t,v) = do
SomeSing s :: SomeSing kproxy <- parseJSONKeyKind t
pv <- parseJSONSing1 s v
return (SomeSingWith1 s pv)
empty :: SingMap kproxy f
empty = Tip
singleton :: Sing v -> f v -> SingMap kproxy f
singleton k x = Bin 1 k x Tip Tip
null :: SingMap kproxy f -> Bool
null Tip = True
null Bin{} = False
size :: SingMap kproxy f -> Int
size Tip = 0
size (Bin n _ _ _ _) = n
lookup :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Maybe (f v)
lookup k = k `seq` go
where
go :: SingMap kproxy 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 kproxy f v. (SOrd kproxy, SDecide kproxy) => SomeSing kproxy -> SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f)
lookupAssoc (SomeSing k) = k `seq` go
where
go :: SingMap kproxy f -> Maybe (SomeSingWith1 kproxy 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 kproxy, SDecide kproxy) => Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy 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 kproxy f -> SingMap kproxy 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 kproxy => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy 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 :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy 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 :: (kproxy ~ 'KProxy) => SingMap kproxy f -> (SomeSingWith1 kproxy f, SingMap kproxy 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 :: (kproxy ~ 'KProxy) => SingMap kproxy f -> (SomeSingWith1 kproxy f, SingMap kproxy 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 kproxy f -> SingMap kproxy f -> SingMap kproxy 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 kproxy f -> SingMap kproxy f -> SingMap kproxy 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 kproxy f -> SingMap kproxy f -> SingMap kproxy 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 kproxy f -> SingMap kproxy f -> SingMap kproxy 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 kproxy f -> SingMap kproxy f -> SingMap kproxy 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 kproxy f -> SingMap kproxy f -> SingMap kproxy f
bin k x l r
= Bin (size l + size r + 1) k x l r
trim :: SOrd kproxy => (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy 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 kproxy, SDecide kproxy) => SomeSing kproxy -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> (Maybe (SomeSingWith1 kproxy f), SingMap kproxy 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 kproxy, SDecide kproxy) => (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy 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 kproxy, SDecide kproxy) => (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy 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 kproxy, SDecide kproxy) => SingMap kproxy f -> Sing v -> f v
(!) m k = find k m
(\\) :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
m1 \\ m2 = difference m1 m2
member :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Bool
member k = isJust . lookup k
notMember :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Bool
notMember k m = not (member k m)
find :: (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy 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 kproxy, SDecide kproxy) => f v -> Sing v -> SingMap kproxy f -> f v
findWithDefault def k m = case lookup k m of
Nothing -> def
Just v -> v
insert :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
insert kx x = kx `seq` go
where
go :: SingMap kproxy f -> SingMap kproxy 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 kproxy, SDecide kproxy) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
insertWith f = insertWithKey (\_ x' y' -> f x' y')
insertWith' :: (SOrd kproxy, SDecide kproxy) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
insertWith' f = insertWithKey' (\_ x' y' -> f x' y')
insertWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
insertWithKey f kx x = kx `seq` go
where
go :: SingMap kproxy f -> SingMap kproxy 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 kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
insertWithKey' f kx x = kx `seq` go
where
go :: SingMap kproxy f -> SingMap kproxy 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 kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f
-> (Maybe (f v), SingMap kproxy f)
insertLookupWithKey f kx x = kx `seq` go
where
go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy 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 kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f
-> (Maybe (f v), SingMap kproxy f)
insertLookupWithKey' f kx x = kx `seq` go
where
go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy 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 (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> SingMap kproxy f
delete k = k `seq` go
where
go :: SingMap kproxy f -> SingMap kproxy 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 kproxy, SDecide kproxy) => (f v -> f v) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
adjust f = adjustWithKey (\_ x -> f x)
adjustWithKey :: (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
adjustWithKey f = updateWithKey (\k' x' -> Just (f k' x'))
update :: (SOrd kproxy, SDecide kproxy) => (f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
update f = updateWithKey (\_ x -> f x)
updateWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
updateWithKey f k = k `seq` go
where
go :: SingMap kproxy f -> SingMap kproxy 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 kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)
updateLookupWithKey f k = k `seq` go
where
go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy 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 kproxy f v. (SOrd kproxy, SDecide kproxy) => (Maybe (f v) -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
alter f k = k `seq` go
where
go :: SingMap kproxy f -> SingMap kproxy 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 (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy 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 (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Maybe Int
lookupIndex k = k `seq` go 0
where
go :: Int -> SingMap kproxy 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 :: (kproxy ~ 'KProxy) => Int -> SingMap kproxy f -> SomeSingWith1 kproxy 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 :: (kproxy ~ 'KProxy) => (forall v. Sing v -> f v -> Maybe (f v)) -> Int -> SingMap kproxy f -> SingMap kproxy 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 :: (kproxy ~ 'KProxy) => Int -> SingMap kproxy f -> SingMap kproxy f
deleteAt i m
= updateAt (\_ _ -> Nothing) i m
findMin :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SomeSingWith1 kproxy 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 :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SomeSingWith1 kproxy 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 :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy f
deleteMin (Bin _ _ _ Tip r) = r
deleteMin (Bin _ kx x l r) = balance kx x (deleteMin l) r
deleteMin Tip = Tip
deleteMax :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy 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 kproxy f -> SingMap kproxy 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 kproxy f -> SingMap kproxy 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 :: (kproxy ~ 'KProxy) => SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f, SingMap kproxy f)
minViewWithKey Tip = Nothing
minViewWithKey x = Just (deleteFindMin x)
maxViewWithKey :: (kproxy ~ 'KProxy) => SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f, SingMap kproxy f)
maxViewWithKey Tip = Nothing
maxViewWithKey x = Just (deleteFindMax x)
unions :: (SOrd kproxy, SDecide kproxy) => [SingMap kproxy f] -> SingMap kproxy f
unions ts
= foldlStrict union empty ts
unionsWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SingMap kproxy f] -> SingMap kproxy f
unionsWithKey f ts
= foldlStrict (unionWithKey f) empty ts
union :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
union Tip t2 = t2
union t1 Tip = t1
union t1 t2 = hedgeUnionL (const LT) (const GT) t1 t2
hedgeUnionL :: (SOrd kproxy, SDecide kproxy)
=> (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f
-> SingMap kproxy 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 kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
unionWithKey _ Tip t2 = t2
unionWithKey _ t1 Tip = t1
unionWithKey f t1 t2 = hedgeUnionWithKey f (const LT) (const GT) t1 t2
hedgeUnionWithKey :: forall kproxy f. (SOrd kproxy, SDecide kproxy)
=> (forall v. Sing v -> f v -> f v -> f v)
-> (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering)
-> SingMap kproxy f -> SingMap kproxy f
-> SingMap kproxy 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 kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy f
difference Tip _ = Tip
difference t1 Tip = t1
difference t1 t2 = hedgeDiff (const LT) (const GT) t1 t2
hedgeDiff :: (SOrd kproxy, SDecide kproxy)
=> (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy g
-> SingMap kproxy 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 kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> g v -> Maybe (f v)) -> SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy f
differenceWithKey _ Tip _ = Tip
differenceWithKey _ t1 Tip = t1
differenceWithKey f t1 t2 = hedgeDiffWithKey f (const LT) (const GT) t1 t2
hedgeDiffWithKey :: (SOrd kproxy, SDecide kproxy)
=> (forall v. Sing v -> f v -> g v -> Maybe (f v))
-> (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering)
-> SingMap kproxy f -> SingMap kproxy g
-> SingMap kproxy 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 kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
intersection m1 m2
= intersectionWithKey (\_ x _ -> x) m1 m2
intersectionWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> g v -> h v) -> SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy 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 kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Bool) -> SingMap kproxy f -> SingMap kproxy 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 kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Bool) -> SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy 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 kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Maybe (g v)) -> SingMap kproxy f -> SingMap kproxy 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 kproxy, SDecide kproxy) =>
(forall v. Sing v -> f v -> Either (g v) (h v)) -> SingMap kproxy f -> (SingMap kproxy g, SingMap kproxy 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 kproxy f -> SingMap kproxy 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 kproxy f -> (a, SingMap kproxy 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 kproxy f -> (a, SingMap kproxy 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 kproxy f -> b
foldWithKey = foldrWithKey
foldrWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap kproxy 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 kproxy 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 :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSing kproxy]
keys m
= [SomeSing k | (SomeSingWith1 k _) <- assocs m]
assocs :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]
assocs m
= toList m
fromList :: (SOrd kproxy, SDecide kproxy) => [SomeSingWith1 kproxy f] -> SingMap kproxy f
fromList xs
= foldlStrict ins empty xs
where
ins :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SomeSingWith1 kproxy f -> SingMap kproxy f
ins t (SomeSingWith1 k x) = insert k x t
fromListWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 kproxy f] -> SingMap kproxy f
fromListWithKey f xs
= foldlStrict (ins f) empty xs
where
ins :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap kproxy f -> SomeSingWith1 kproxy f -> SingMap kproxy f
ins f t (SomeSingWith1 k x) = insertWithKey f k x t
toList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]
toList t = toAscList t
toAscList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]
toAscList t = foldrWithKey (\k x xs -> (SomeSingWith1 k x):xs) [] t
toDescList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]
toDescList t = foldlWithKey (\xs k x -> (SomeSingWith1 k x):xs) [] t
fromAscList :: (SEq kproxy, SDecide kproxy) => [SomeSingWith1 kproxy f] -> SingMap kproxy f
fromAscList xs
= fromAscListWithKey (\_ x _ -> x) xs
fromAscListWithKey :: (SEq kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 kproxy f] -> SingMap kproxy f
fromAscListWithKey f xs
= fromDistinctAscList (combineEq f xs)
where
combineEq _ xs'
= case xs' of
[] -> []
[x] -> [x]
(x:xx) -> combineEq' f x xx
combineEq' :: (SEq kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SomeSingWith1 kproxy f -> [SomeSingWith1 kproxy f] -> [SomeSingWith1 kproxy 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 kproxy f] -> SingMap kproxy f
fromDistinctAscList xs
= build const (length xs) xs
where
build :: (SingMap kproxy f -> [SomeSingWith1 kproxy f] -> b) -> Int -> [SomeSingWith1 kproxy 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 kproxy f -> [SomeSingWith1 kproxy f] -> b) -> SingMap kproxy f -> [SomeSingWith1 kproxy f] -> b
buildR n c l (SomeSingWith1 k x : ys) = build (buildB l k x c) n ys
buildR _ _ _ [] = error "fromDistinctAscList buildR []"
buildB :: SingMap kproxy f -> Sing v -> f v -> (SingMap kproxy f -> a -> b) -> SingMap kproxy f -> a -> b
buildB l k x c r zs = c (bin k x l r) zs
split :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy f)
split k = go
where
go :: SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy 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 kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, Maybe (f v), SingMap kproxy f)
splitLookup k = go
where
go :: SingMap kproxy f -> (SingMap kproxy f, Maybe (f v), SingMap kproxy 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 kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, Maybe (Sing v, f v), SingMap kproxy f)
splitLookupWithKey k = go
where
go :: SingMap kproxy f -> (SingMap kproxy f, Maybe (Sing v, f v), SingMap kproxy 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 kproxy 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 kproxy 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 kproxy 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 kproxy, SDecide kproxy) => SingMap kproxy f -> Bool
valid t
= balanced t && ordered t && validsize t
ordered :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> Bool
ordered t
= bounded (const True) (const True) t
where
bounded :: (SOrd kproxy, SDecide kproxy) => (SomeSing kproxy -> Bool) -> (SomeSing kproxy -> Bool) -> SingMap kproxy 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 kproxy 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 kproxy 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
compareSome :: SOrd kproxy => SomeSing kproxy -> SomeSing kproxy -> Ordering
compareSome (SomeSing a) (SomeSing b) = fromSing (sCompare a b)
ltSome :: SOrd kproxy => SomeSing kproxy -> SomeSing kproxy -> Bool
ltSome (SomeSing a) (SomeSing b) = fromSing (a %:< b)
gtSome :: SOrd kproxy => SomeSing kproxy -> SomeSing kproxy -> Bool
gtSome (SomeSing a) (SomeSing b) = fromSing (a %:> b)
unifyOnCompareEQ :: forall (kproxy :: KProxy k) (a :: k) (b :: k) x.
(SDecide kproxy, 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 (kproxy :: KProxy k) (a :: k) (b :: k) x.
(SDecide kproxy, (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