ADPfusion-0.4.0.0: ADP/Fusion/QuickCheck/Set.hs
{-# Options_GHC -O0 #-}
module ADP.Fusion.QuickCheck.Set where
import Data.Bits
import Data.Vector.Fusion.Util
import Debug.Trace
import qualified Data.List as L
import qualified Data.Vector.Fusion.Stream as S
import qualified Data.Vector.Unboxed as VU
import Test.QuickCheck hiding (NonEmpty)
import Test.QuickCheck.All
import Test.QuickCheck.Monadic
import Data.Bits.Ordered
import Data.PrimitiveArray
import ADP.Fusion
import ADP.Fusion.QuickCheck.Common
-- * BitSets without interfaces
-- ** Inside checks
prop_b_ii ix@(BitSet _) = zs == ls where
tia = ITbl 0 0 EmptyOk xsB (\ _ _ -> Id 1)
tib = ITbl 0 0 EmptyOk xsB (\ _ _ -> Id 1)
zs = ((,) <<< tia % tib ... S.toList) highestB ix
ls = [ ( xsB ! kk , xsB ! (ix `xor` kk) )
| k <- VU.toList . popCntSorted $ popCount ix -- [ 0 .. 2^(popCount ix) -1 ]
, let kk = popShiftL ix (BitSet k)
]
prop_b_ii_nn ix@(BitSet _) = zs == ls where
tia = ITbl 0 0 NonEmpty xsB (\ _ _ -> Id 1)
tib = ITbl 0 0 NonEmpty xsB (\ _ _ -> Id 1)
zs = ((,) <<< tia % tib ... S.toList) highestB ix
ls = [ ( xsB ! kk , xsB ! (ix `xor` kk) )
| k <- VU.toList . popCntSorted $ popCount ix -- [ 0 .. 2^(popCount ix) -1 ]
, let kk = popShiftL ix (BitSet k)
, popCount kk > 0
, popCount (ix `xor` kk) > 0
]
prop_b_iii ix@(BitSet _) = zs == ls where
tia = ITbl 0 0 EmptyOk xsB (\ _ _ -> Id 1)
tib = ITbl 0 0 EmptyOk xsB (\ _ _ -> Id 1)
tic = ITbl 0 0 EmptyOk xsB (\ _ _ -> Id 1)
zs = ((,,) <<< tia % tib % tic ... S.toList) highestB ix
ls = [ ( xsB ! kk , xsB ! ll , xsB ! mm )
| k <- VU.toList . popCntSorted $ popCount ix
, l <- VU.toList . popCntSorted $ popCount ix - popCount k
, let kk = popShiftL ix (BitSet k)
, let ll = popShiftL (ix `xor` kk) (BitSet l)
, let mm = (ix `xor` (kk .|. ll))
]
prop_b_iii_nnn ix@(BitSet _) = zs == ls where
tia = ITbl 0 0 NonEmpty xsB (\ _ _ -> Id 1)
tib = ITbl 0 0 NonEmpty xsB (\ _ _ -> Id 1)
tic = ITbl 0 0 NonEmpty xsB (\ _ _ -> Id 1)
zs = ((,,) <<< tia % tib % tic ... S.toList) highestB ix
ls = [ ( xsB ! kk , xsB ! ll , xsB ! mm )
| k <- VU.toList . popCntSorted $ popCount ix
, l <- VU.toList . popCntSorted $ popCount ix - popCount k
, let kk = popShiftL ix (BitSet k)
, let ll = popShiftL (ix `xor` kk) (BitSet l)
, let mm = (ix `xor` (kk .|. ll))
, popCount kk > 0, popCount ll > 0, popCount mm > 0
]
-- * Outside checks
-- These checks are very similar to those in the @Subword@ module. We just
-- need to be a bit more careful, as indexed sets have overlap.
-- ** Two non-terminals.
--
-- @A_s -> B_(s\t) C_t (s\t) ++ t == s@
-- @s = 111 , s\t = 101, t = 010@
--
-- with @Z@ the full set.
-- @Z = 1111@
-- @B*_Z\(s\t) -> A*_Z\s C_t@
-- @Z\(s\t) = 1010, Z\s = 1000, t = 010@
-- * BitSets with two interfaces
-- ** Inside checks
prop_bii_i :: BS2I First Last -> Bool
prop_bii_i ix@(s:>i:>j) = zs == ls where
tia = ITbl 0 0 EmptyOk xsBII (\ _ _ -> Id 1)
zs = (id <<< tia ... S.toList) highestBII ix
ls = [ xsBII ! ix ]
prop_bii_i_n :: BS2I First Last -> Bool
prop_bii_i_n ix@(s:>i:>j) = zs == ls where
tia = ITbl 0 0 NonEmpty xsBII (\ _ _ -> Id 1)
zs = (id <<< tia ... S.toList) highestBII ix
ls = [ xsBII ! ix | popCount s > 0 ]
-- | Edges should never work as a single terminal element.
prop_bii_e :: BS2I First Last -> Bool
prop_bii_e ix@(s:>Iter i:>Iter j) = zs == ls where
e = Edge (\ i j -> (i,j)) :: Edge (Int,Int)
zs = (id <<< e ... S.toList) highestBII ix
ls = [] :: [ (Int,Int) ]
-- | Edges extend only in cases where in @i -> j@, @i@ actually happens to
-- be a true interface.
prop_bii_ie :: BS2I First Last -> Bool
prop_bii_ie ix@(s:>i:>Iter j) = zs == ls where
tia = ITbl 0 0 EmptyOk xsBII (\ _ _ -> Id 1)
e = Edge (\ i j -> (i,j)) :: Edge (Int,Int)
zs = ((,) <<< tia % e ... S.toList) highestBII ix
ls = [ ( xsBII ! (t:>i:>(Iter k :: Interface Last)) , (k,j) )
| let t = s `clearBit` j
, k <- activeBitsL t ]
prop_bii_ie_n :: BS2I First Last -> Bool
prop_bii_ie_n ix@(s:>i:>Iter j) = zs == ls where
tia = ITbl 0 0 NonEmpty xsBII (\ _ _ -> Id 1)
e = Edge (\ i j -> (i,j)) :: Edge (Int,Int)
zs = ((,) <<< tia % e ... S.toList) highestBII ix
ls = [ ( xsBII ! (t:>i:>(Iter k :: Interface Last)) , (k,j) )
| let t = s `clearBit` j
, popCount t >= 2
, k <- activeBitsL t
, k /= getIter i
]
prop_bii_iee :: BS2I First Last -> Bool
prop_bii_iee ix@(s:>i:>Iter j) = L.sort zs == L.sort ls where
tia = ITbl 0 0 EmptyOk xsBII (\ _ _ -> Id 1)
e = Edge (\ i j -> (i,j)) :: Edge (Int,Int)
zs = ((,,) <<< tia % e % e ... S.toList) highestBII ix
ls = [ ( xsBII ! (t:>i:>kk) , (k,l) , (l,j) )
| let tmp = (s `clearBit` j)
, l <- activeBitsL tmp
, l /= getIter i
, let t = tmp `clearBit` l
, k <- activeBitsL t
, let kk = Iter k
]
prop_bii_ieee :: BS2I First Last -> Bool
prop_bii_ieee ix@(s:>i:>Iter j) = L.sort zs == L.sort ls where
tia = ITbl 0 0 EmptyOk xsBII (\ _ _ -> Id 1)
e = Edge (\ i j -> (i,j)) :: Edge (Int,Int)
zs = ((,,,) <<< tia % e % e % e ... S.toList) highestBII ix
ls = [ ( xsBII ! (t:>i:>kk) , (k,l) , (l,m) , (m,j) )
| let tmpM = (s `clearBit` j)
, m <- activeBitsL tmpM
, m /= getIter i
, let tmpL = (tmpM `clearBit` m)
, l <- activeBitsL tmpL
, l /= getIter i
, let t = tmpL `clearBit` l
, k <- activeBitsL t
, let kk = Iter k
]
prop_bii_iee_n :: BS2I First Last -> Bool
prop_bii_iee_n ix@(s:>i:>Iter j) = L.sort zs == L.sort ls where
tia = ITbl 0 0 NonEmpty xsBII (\ _ _ -> Id 1)
e = Edge (\ i j -> (i,j)) :: Edge (Int,Int)
zs = ((,,) <<< tia % e % e ... S.toList) highestBII ix
ls = [ ( xsBII ! (t:>i:>kk) , (k,l) , (l,j) )
| let tmp = (s `clearBit` j)
, l <- activeBitsL tmp
, l /= getIter i
, let t = tmp `clearBit` l
, popCount t >= 2
, k <- activeBitsL t
, k /= getIter i
, let kk = Iter k
]
prop_bii_ieee_n :: BS2I First Last -> Bool
prop_bii_ieee_n ix@(s:>i:>Iter j) = L.sort zs == L.sort ls where
tia = ITbl 0 0 NonEmpty xsBII (\ _ _ -> Id 1)
e = Edge (\ i j -> (i,j)) :: Edge (Int,Int)
zs = ((,,,) <<< tia % e % e % e ... S.toList) highestBII ix
ls = [ ( xsBII ! (t:>i:>kk) , (k,l) , (l,m) , (m,j) )
| let tmpM = (s `clearBit` j)
, m <- activeBitsL tmpM
, m /= getIter i
, let tmpL = (tmpM `clearBit` m)
, l <- activeBitsL tmpL
, l /= getIter i
, let t = tmpL `clearBit` l
, popCount t >= 2
, k <- activeBitsL t
, k /= getIter i
, let kk = Iter k
]
-- prop_bii_ii (ix@(s:>i:>j) :: (BitSet:>Interface First:>Interface Last)) = tr zs ls $ zs == ls where
-- tia = ITbl 0 0 EmptyOk xsBII (\ _ _ -> Id 1)
-- tib = ITbl 0 0 EmptyOk xsBII (\ _ _ -> Id 1)
-- zs = ((,) <<< tia % tib ... S.toList) highestBII ix
-- ls = [ ( xsBII ! kk , xsBII ! ll )
-- | k <- VU.toList . popCntSorted $ popCount s
-- , ki <- if k==0 then [0] else activeBitsL k
-- , kj <- if | k==0 -> [0] | popCount k==1 -> [ki] | otherwise -> activeBitsL (k `clearBit` ki)
-- , let kk = (BitSet k:>Iter ki:>Iter kj)
-- , let l = s `xor` BitSet k
-- , li <- if l==0 then [0] else activeBitsL l
-- , lj <- if | l==0 -> [0] | popCount l==1 -> [li] | otherwise -> activeBitsL (l `clearBit` li)
-- , let ll = (l:>Iter li:>Iter lj)
-- ]
-- * Helper functions
highBit = fromIntegral arbitraryBitSetMax -- should be the same as the highest bit in Index.Set.arbitrary
highestB = BitSet $ 2^(highBit+1) -1
highestBII = highestB :> Iter (highBit-1) :> Iter (highBit-1) -- assuming @highBit >= 1@
xsB :: Unboxed BitSet Int
xsB = fromList (BitSet 0) highestB [ 0 .. ]
xoB :: Unboxed (Outside BitSet) Int
xoB = fromList (O (BitSet 0)) (O highestB) [ 0 .. ]
xsBII :: Unboxed (BitSet:>Interface First:>Interface Last) Int
xsBII = fromList (BitSet 0:>Iter 0:>Iter 0) highestBII [ 0 .. ]
-- * general quickcheck stuff
options = stdArgs {maxSuccess = 1000}
customCheck = quickCheckWithResult options
return []
allProps = $forAllProperties customCheck