e12af96e482be31e3c938757f674bdc612643581
[packages/containers.git] / tests / IntSetValidity.hs
1 {-# LANGUAGE CPP #-}
2 module IntSetValidity (valid) where
3
4 import Data.Bits (xor, (.&.))
5 import Data.IntSet.Internal
6 import Test.QuickCheck (Property, counterexample, property, (.&&.))
7 import Utils.Containers.Internal.BitUtil (bitcount)
8
9 {--------------------------------------------------------------------
10 Assertions
11 --------------------------------------------------------------------}
12 -- | Returns true iff the internal structure of the IntSet is valid.
13 valid :: IntSet -> Property
14 valid t =
15 counterexample "nilNeverChildOfBin" (nilNeverChildOfBin t) .&&.
16 counterexample "maskPowerOfTwo" (maskPowerOfTwo t) .&&.
17 counterexample "commonPrefix" (commonPrefix t) .&&.
18 counterexample "markRespected" (maskRespected t) .&&.
19 counterexample "tipsValid" (tipsValid t)
20
21 -- Invariant: Nil is never found as a child of Bin.
22 nilNeverChildOfBin :: IntSet -> Bool
23 nilNeverChildOfBin t =
24 case t of
25 Nil -> True
26 Tip _ _ -> True
27 Bin _ _ l r -> noNilInSet l && noNilInSet r
28 where
29 noNilInSet t' =
30 case t' of
31 Nil -> False
32 Tip _ _ -> True
33 Bin _ _ l' r' -> noNilInSet l' && noNilInSet r'
34
35 -- Invariant: The Mask is a power of 2. It is the largest bit position at which
36 -- two elements of the set differ.
37 maskPowerOfTwo :: IntSet -> Bool
38 maskPowerOfTwo t =
39 case t of
40 Nil -> True
41 Tip _ _ -> True
42 Bin _ m l r ->
43 bitcount 0 (fromIntegral m) == 1 && maskPowerOfTwo l && maskPowerOfTwo r
44
45 -- Invariant: Prefix is the common high-order bits that all elements share to
46 -- the left of the Mask bit.
47 commonPrefix :: IntSet -> Bool
48 commonPrefix t =
49 case t of
50 Nil -> True
51 Tip _ _ -> True
52 b@(Bin p _ l r) -> all (sharedPrefix p) (elems b) && commonPrefix l && commonPrefix r
53 where
54 sharedPrefix :: Prefix -> Int -> Bool
55 sharedPrefix p a = p == p .&. a
56
57 -- Invariant: In Bin prefix mask left right, left consists of the elements that
58 -- don't have the mask bit set; right is all the elements that do.
59 maskRespected :: IntSet -> Bool
60 maskRespected t =
61 case t of
62 Nil -> True
63 Tip _ _ -> True
64 Bin _ binMask l r ->
65 all (\x -> zero x binMask) (elems l) &&
66 all (\x -> not (zero x binMask)) (elems r) &&
67 maskRespected l &&
68 maskRespected r
69
70 -- Invariant: The Prefix is zero for the last 5 (on 32 bit arches) or 6 bits
71 -- (on 64 bit arches). The values of the set represented by a tip
72 -- are the prefix plus the indices of the set bits in the bit map.
73 --
74 -- Note: Valid entries stored in tip omitted.
75 tipsValid :: IntSet -> Bool
76 tipsValid t =
77 case t of
78 Nil -> True
79 tip@(Tip p b) -> validTipPrefix p
80 Bin _ _ l r -> tipsValid l && tipsValid r
81
82 validTipPrefix :: Prefix -> Bool
83 #if WORD_SIZE_IN_BITS==32
84 -- Last 5 bits of the prefix must be zero for 32 bit arches.
85 validTipPrefix p = (0x0000001F .&. p) == 0
86 #else
87 -- Last 6 bits of the prefix must be zero 64 bit anches.
88 validTipPrefix p = (0x000000000000003F .&. p) == 0
89 #endif