9e92ba631e6ba0007ab5aeb016bfffa81112c778
1 module IntMapValidity (valid) where
3 import Data.Bits (xor, (.&.))
4 import Data.IntMap.Internal
5 import Test.QuickCheck (Property, counterexample, property, (.&&.))
6 import Utils.Containers.Internal.BitUtil (bitcount)
8 {--------------------------------------------------------------------
9 Assertions
10 --------------------------------------------------------------------}
11 -- | Returns true iff the internal structure of the IntMap is valid.
12 valid :: IntMap a -> Property
13 valid t =
14 counterexample "nilNeverChildOfBin" (nilNeverChildOfBin t) .&&.
15 counterexample "commonPrefix" (commonPrefix t) .&&.
18 -- Invariant: Nil is never found as a child of Bin.
19 nilNeverChildOfBin :: IntMap a -> Bool
20 nilNeverChildOfBin t =
21 case t of
22 Nil -> True
23 Tip _ _ -> True
24 Bin _ _ l r -> noNilInSet l && noNilInSet r
25 where
26 noNilInSet t' =
27 case t' of
28 Nil -> False
29 Tip _ _ -> True
30 Bin _ _ l' r' -> noNilInSet l' && noNilInSet r'
32 -- Invariant: The Mask is a power of 2. It is the largest bit position at which
33 -- two keys of the map differ.
34 maskPowerOfTwo :: IntMap a -> Bool
36 case t of
37 Nil -> True
38 Tip _ _ -> True
39 Bin _ m l r ->
40 bitcount 0 (fromIntegral m) == 1 && maskPowerOfTwo l && maskPowerOfTwo r
42 -- Invariant: Prefix is the common high-order bits that all elements share to
43 -- the left of the Mask bit.
44 commonPrefix :: IntMap a -> Bool
45 commonPrefix t =
46 case t of
47 Nil -> True
48 Tip _ _ -> True
49 b@(Bin p _ l r) -> all (sharedPrefix p) (keys b) && commonPrefix l && commonPrefix r
50 where
51 sharedPrefix :: Prefix -> Int -> Bool
52 sharedPrefix p a = p == p .&. a
54 -- Invariant: In Bin prefix mask left right, left consists of the elements that
55 -- don't have the mask bit set; right is all the elements that do.
56 maskRespected :: IntMap a -> Bool