liquidhaskell-0.8.10.7: benchmarks/containers-0.5.0.0/Data/Map/Base0.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
#if __GLASGOW_HASKELL__
-- LIQUID {- LANGUAGE DeriveDataTypeable, StandaloneDeriving -}
#endif
#if !defined(TESTING) && __GLASGOW_HASKELL__ >= 703
{-# LANGUAGE Trustworthy #-}
#endif
module Data.Map.Base where
import Language.Haskell.Liquid.Prelude
import Prelude hiding (lookup,map,filter,foldr,foldl,null)
import Data.Monoid (Monoid(..))
import Data.Traversable (Traversable(traverse))
import qualified Data.Foldable as Foldable
import Control.DeepSeq (NFData(rnf))
#if __GLASGOW_HASKELL__
import GHC.Exts ( build )
import Text.Read
import Data.Data
#endif
#define STRICT_1_OF_2(fn) fn arg _ | arg `seq` False = undefined
#define STRICT_1_OF_3(fn) fn arg _ _ | arg `seq` False = undefined
#define STRICT_2_OF_3(fn) fn _ arg _ | arg `seq` False = undefined
#define STRICT_1_OF_4(fn) fn arg _ _ _ | arg `seq` False = undefined
#define STRICT_2_OF_4(fn) fn _ arg _ _ | arg `seq` False = undefined
data Map k a = Bin Size k a (Map k a) (Map k a)
| Tip
type Size = Int
data MaybeS a = NothingS | JustS a
{-@ include <Base.hquals> @-}
{-@
data Map k a <l :: root:k -> k -> Bool, r :: root:k -> k -> Bool>
= Bin (sz :: Size)
(key :: k)
(value :: a)
(left :: Map <l, r> (k <l key>) a)
(right :: Map <l, r> (k <r key>) a)
| Tip
@-}
{-@ measure isJustS :: forall a. MaybeS a -> Bool
isJustS (JustS x) = true
isJustS (NothingS) = false
@-}
{-@ measure fromJustS :: forall a. MaybeS a -> a
fromJustS (JustS x) = x
@-}
{-@ type OMap k a = Map <{v:k | v < root}, {v:k | v > root}> k a @-}
{-@ measure isBin :: Map k a -> Bool
isBin (Bin sz kx x l r) = true
isBin (Tip) = false
@-}
{-@ measure key :: Map k a -> k
key (Bin sz kx x l r) = kx
@-}
---------------------------------------------------------------------
{-@ trim :: (Ord k) => lo:MaybeS k -> hi:MaybeS k -> OMap k a -> {v: OMap k a | (((isBin(v) && isJustS(lo)) => (fromJustS(lo) < key(v))) && ((isBin(v) && isJustS(hi)) => (fromJustS(hi) > key(v)))) } @-}
trim :: Ord k => MaybeS k -> MaybeS k -> Map k a -> Map k a
trim = error "GOO"
--trim NothingS NothingS t = t
--trim (JustS lk) NothingS t = greater lk t
-- where greater lo t@(Bin _ k _ _ r) | k <= lo = greater lo r
-- | otherwise = t
-- greater _ t'@Tip = t'
--trim NothingS (JustS hk) t = lesser hk t
-- where lesser hi t'@(Bin _ k _ l _) | k >= hi = lesser hi l
-- | otherwise = t'
-- lesser _ t'@Tip = t'
--trim (JustS lk) (JustS hk) t = middle lk hk t
-- where middle lo hi t'@(Bin _ k _ l r) | k <= lo = middle lo hi r
-- | k >= hi = middle lo hi l
-- | otherwise = t'
-- middle _ _ t'@Tip = t'
{-@ filterGt :: (Ord k) -> x:MaybeS k -> OMap k v -> OMap {v:k | ((isJustS(x)) => (v > fromJustS(x))) } v @-}
filterGt :: Ord k => MaybeS k -> Map k v -> Map k v
filterGt = error "GOO"
{-@ filterLt :: (Ord k) -> x:MaybeS k -> OMap k v -> OMap {v:k | ((isJustS(x)) => (v < fromJustS(x))) } v @-}
filterLt :: Ord k => MaybeS k -> Map k v -> Map k v
filterLt = error "GOO"
{-@ join :: kcut:k -> a -> OMap {v:k | v < kcut} a -> OMap {v:k| v > kcut} a -> OMap k a @-}
join :: k -> a -> Map k a -> Map k a -> Map k a
join kx x l r = Bin 1 kx x l r
{-@ merge :: kcut:k -> OMap {v:k | v < kcut} a -> OMap {v:k| v > kcut} a -> OMap k a @-}
merge :: k -> Map k a -> Map k a -> Map k a
merge = error "gOO"
{-@ member :: Ord k => k -> OMap k a -> Bool @-}
member :: Ord k => k -> Map k a -> Bool
member kx t = error "TODO"
{-@ insertR :: Ord k => k -> a -> OMap k a -> OMap k a @-}
insertR :: Ord k => k -> a -> Map k a -> Map k a
insertR kx x t = error "TODO"
{-@ singleton :: k -> a -> OMap k a @-}
singleton :: k -> a -> Map k a
singleton = error "GOO"
{-@ assert lookup :: (Ord k) => k -> OMap k a -> Maybe a @-}
lookup :: Ord k => k -> Map k a -> Maybe a
lookup = error "TDA"
{-@ hedgeDiff :: (Ord k) => lo0:MaybeS k -> lo: {v: MaybeS {v: k | (isJustS(lo0) && (v = fromJustS(lo0))) } | v = lo0 }
-> hi0:MaybeS k -> hi:{v: MaybeS {v: k | ( isJustS(hi0) && (v = fromJustS(hi0))) }
| (((isJustS(lo) && isJustS(v)) => (fromJustS(v) >= fromJustS(lo))) && (v = hi0)) }
-> {v: OMap k a | (((isBin(v) && isJustS(lo)) => (fromJustS(lo) < key(v))) && ((isBin(v) && isJustS(hi)) => (fromJustS(hi) > key(v)))) }
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } b
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } a @-}
hedgeDiff :: Ord a => MaybeS a -> MaybeS a -> MaybeS a -> MaybeS a -> Map a b -> Map a c -> Map a b
hedgeDiff _ _ _ _ Tip _ = Tip
hedgeDiff blo0 blo bhi0 bhi (Bin _ kx x l r) Tip = join kx x (filterGt blo l) (filterLt bhi r)
hedgeDiff blo0 blo bhi0 bhi t (Bin _ kx _ l r) = merge kx (hedgeDiff blo0 blo bmi bmi (trim blo bmi t) l)
(hedgeDiff bmi bmi bhi0 bhi (trim bmi bhi t) r)
where bmi = JustS kx
------------------------------------------------------------------------------
-- {- hedgeUnion :: (Ord k) => lo0:MaybeS k -> lo: {v: MaybeS {v: k | (isJustS(lo0) && (v = fromJustS(lo0))) } | v = lo0 }
-- -> hi0:MaybeS k -> hi:{v: MaybeS {v: k | ( isJustS(hi0) && (v = fromJustS(hi0))) }
-- | (((isJustS(lo) && isJustS(v)) => (fromJustS(v) >= fromJustS(lo))) && (v = hi0)) }
-- -> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } a
-- -> {v: OMap k a | (((isBin(v) && isJustS(lo)) => (fromJustS(lo) < key(v))) && ((isBin(v) && isJustS(hi)) => (fromJustS(hi) > key(v)))) }
-- -> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } a @-}
--
-- hedgeUnion :: Ord k => MaybeS k -> MaybeS k -> MaybeS k -> MaybeS k -> Map k b -> Map k b -> Map k b
-- hedgeUnion _ _ _ _ t1 Tip = t1
-- hedgeUnion blo0 blo bhi0 bhi Tip (Bin _ kx x l r) = join kx x (filterGt blo l) (filterLt bhi r)
-- hedgeUnion _ _ _ _ t1 (Bin _ kx x Tip Tip) = insertR kx x t1 -- According to benchmarks, this special case increases
-- -- performance up to 30%. It does not help in difference or intersection.
-- hedgeUnion blo0 blo bhi0 bhi (Bin _ kx x l r) t2 = join kx x (hedgeUnion blo blo bmi bmi l (trim blo bmi t2))
-- (hedgeUnion bmi bmi bhi0 bhi r (trim bmi bhi t2))
-- where bmi = JustS kx
--
-- {- hedgeInt :: (Ord k) => lo0:MaybeS k -> lo: {v: MaybeS {v: k | (isJustS(lo0) && (v = fromJustS(lo0))) } | v = lo0 }
-- -> hi0:MaybeS k -> hi:{v: MaybeS {v: k | ( isJustS(hi0) && (v = fromJustS(hi0))) }
-- | (((isJustS(lo) && isJustS(v)) => (fromJustS(v) >= fromJustS(lo))) && (v = hi0)) }
-- -> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } a
-- -> {v: OMap k b | (((isBin(v) && isJustS(lo)) => (fromJustS(lo) < key(v))) && ((isBin(v) && isJustS(hi)) => (fromJustS(hi) > key(v)))) }
-- -> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } a @-}
-- hedgeInt :: Ord k => MaybeS k -> MaybeS k -> MaybeS k -> MaybeS k -> Map k a -> Map k b -> Map k a
-- hedgeInt _ _ _ _ _ Tip = Tip
-- hedgeInt _ _ _ _ Tip _ = Tip
-- hedgeInt blo0 blo bhi0 bhi (Bin _ kx x l r) t2 = let l' = hedgeInt blo0 blo bmi bmi l (trim blo bmi t2)
-- r' = hedgeInt bmi bmi bhi0 bhi r (trim bmi bhi t2)
-- in if kx `member` t2 then join kx x l' r' else merge kx l' r'
-- where bmi = JustS kx
----------------------------------------------------------------------------------
{- mergeWithKey :: (Ord k) => (k -> a -> b -> Maybe c)
-> (lo:MaybeS k -> hi: MaybeS k
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } a
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } c)
-> (lo:MaybeS k -> hi: MaybeS k
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } b
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } c)
-> OMap k a -> OMap k b -> OMap k c @-}
--mergeWithKey :: Ord k => (k -> a -> b -> Maybe c) -> (MaybeS k -> MaybeS k -> Map k a -> Map k c) -> (MaybeS k -> MaybeS k -> Map k b -> Map k c)
-- -> Map k a -> Map k b -> Map k c
--mergeWithKey f g1 g2 = go
-- where
-- go Tip t2 = g2 NothingS NothingS t2
-- go t1 Tip = g1 NothingS NothingS t1
-- go t1 t2 = hedgeMerge f g1 g2 NothingS NothingS NothingS NothingS t1 t2
{-@ hedgeMerge :: (Ord k) => (k -> a -> b -> Maybe c)
-> (lo:MaybeS k -> hi: MaybeS k
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } a
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } c)
-> (lo:MaybeS k -> hi: MaybeS k
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } b
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } c)
-> lo0:MaybeS k -> lo: {v: MaybeS {v: k | (isJustS(lo0) && (v = fromJustS(lo0))) } | v = lo0 }
-> hi0:MaybeS k -> hi:{v: MaybeS {v: k | ( isJustS(hi0) && (v = fromJustS(hi0))) }
| (((isJustS(lo) && isJustS(v)) => (fromJustS(v) >= fromJustS(lo))) && (v = hi0)) }
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } a
-> {v: OMap k b | (((isBin(v) && isJustS(lo)) => (fromJustS(lo) < key(v))) && ((isBin(v) && isJustS(hi)) => (fromJustS(hi) > key(v)))) }
-> OMap {v: k | (((isJustS(lo)) => (v > fromJustS(lo))) && (((isJustS(hi)) => (v < fromJustS(hi))))) } c @-}
hedgeMerge :: Ord k => (k -> a -> b -> Maybe c)
-> (MaybeS k -> MaybeS k -> Map k a -> Map k c)
-> (MaybeS k -> MaybeS k -> Map k b -> Map k c)
-> MaybeS k -> MaybeS k -> MaybeS k -> MaybeS k
-> Map k a -> Map k b -> Map k c
hedgeMerge f g1 g2 _ blo _ bhi t1 Tip
= g1 blo bhi t1
hedgeMerge f g1 g2 blo0 blo bhi0 bhi Tip (Bin _ kx x l r)
= g2 blo bhi $ join kx x (filterGt blo l) (filterLt bhi r)
hedgeMerge f g1 g2 blo0 blo bhi0 bhi (Bin _ kx x l r) t2
= let bmi = JustS kx
l' = hedgeMerge f g1 g2 blo0 blo bmi bmi l (trim blo bmi t2)
(found, trim_t2) = trimLookupLo kx bhi t2
r' = hedgeMerge f g1 g2 bmi bmi bhi0 bhi r trim_t2
in case found of
Nothing -> case g1 blo bhi (singleton kx x) of
Tip -> merge kx l' r'
(Bin _ _ x' Tip Tip) -> join kx x' l' r'
_ -> error "mergeWithKey: Given function only1 does not fulfil required conditions (see documentation)"
Just x2 -> case f kx x x2 of
Nothing -> merge kx l' r'
Just x' -> join kx x' l' r'
{-@ trimLookupLo :: (Ord k)
=> lo:k
-> bhi:{v: MaybeS k | (isJustS(v) => (lo < fromJustS(v)))}
-> OMap k a
-> (Maybe a, {v: OMap k a | ((isBin(v) => (lo < key(v))) && ((isBin(v) && isJustS(bhi)) => (fromJustS(bhi) > key(v)))) }) @-}
trimLookupLo :: Ord k => k -> MaybeS k -> Map k a -> (Maybe a, Map k a)
trimLookupLo lk NothingS t = greater lk t
where greater :: Ord k => k -> Map k a -> (Maybe a, Map k a)
greater lo t'@(Bin _ kx x l r) = case compare lo kx of LT -> (lookup lo l, {-`strictPair`-} t')
EQ -> (Just x, (case r of {r'@(Bin _ _ _ _ _) -> r' ; r'@Tip -> r'}))
GT -> greater lo r
greater _ Tip = (Nothing, Tip)
trimLookupLo lk (JustS hk) t = middle lk hk t
where middle :: Ord k => k -> k -> Map k a -> (Maybe a, Map k a)
middle lo hi t'@(Bin _ kx x l r) = case compare lo kx of LT | kx < hi -> (lookup lo l, {- `strictPair` -} t')
| otherwise -> middle lo hi l
EQ -> (Just x, {-`strictPair`-} lesser lo hi (case r of {r'@(Bin _ _ _ _ _) -> r' ; r'@Tip -> r'}))
GT -> middle lo hi r
middle _ _ Tip = (Nothing, Tip)
lesser :: Ord k => k -> k -> Map k a -> Map k a
lesser lo hi t'@(Bin _ k _ l _) | k >= hi = lesser lo hi l
| otherwise = t'
lesser _ _ t'@Tip = t'
#if __GLASGOW_HASKELL__ >= 700
{-# INLINABLE trimLookupLo #-}
#endif