----------------------------------------------------------------------------- -- | -- Module : TestSuite.Basics.ArithNoSolver -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Test suite for basic concrete arithmetic, i.e., testing all -- the constant folding based arithmetic implementation in SBV ----------------------------------------------------------------------------- {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TupleSections #-} module TestSuite.Basics.ArithNoSolver(tests) where import qualified Data.Numbers.CrackNum as CN (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.SBV.Internals import Utils.SBVTestFramework import Data.Maybe (fromJust, isJust, fromMaybe) import Data.List (genericIndex, isInfixOf, isPrefixOf, isSuffixOf, genericTake, genericDrop, genericLength) import qualified Data.Char as C import qualified Data.SBV.Char as SC import qualified Data.SBV.String as SS import qualified Data.SBV.List as SL -- Test suite tests :: TestTree tests = testGroup "Arith.NoSolver" $ genReals ++ genFloats ++ genQRems ++ genBinTest "+" (+) ++ genBinTest "-" (-) ++ genBinTest "*" (*) ++ genUnTest "negate" negate ++ genUnTest "abs" abs ++ genUnTest "signum" signum ++ genBinTest ".&." (.&.) ++ genBinTest ".|." (.|.) ++ genBoolTest "<" (<) (.<) ++ genBoolTest "<=" (<=) (.<=) ++ genBoolTest ">" (>) (.>) ++ genBoolTest ">=" (>=) (.>=) ++ genBoolTest "==" (==) (.==) ++ genBoolTest "/=" (/=) (./=) ++ genBinTest "xor" xor ++ genUnTest "complement" complement ++ genIntTest False "setBit" setBit ++ genIntTest False "clearBit" clearBit ++ genIntTest False "complementBit" complementBit ++ genIntTest True "shift" shift ++ genIntTest True "shiftL" shiftL ++ genIntTest True "shiftR" shiftR ++ genIntTest True "rotate" rotate ++ genIntTest True "rotateL" rotateL ++ genIntTest True "rotateR" rotateR ++ genShiftRotTest "shiftL_gen" sShiftLeft ++ genShiftRotTest "shiftR_gen" sShiftRight ++ genShiftRotTest "rotateL_gen" sRotateLeft ++ genShiftRotTest "rotateR_gen" sRotateRight ++ genShiftMixSize ++ genBlasts ++ genCounts ++ genIntCasts ++ genChars ++ genStrings ++ genLists genBinTest :: String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree] genBinTest nm op = map mkTest $ zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `op` y | x <- sw8s, y <- sw8s ] ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `op` y | x <- sw16s, y <- sw16s] ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `op` y | x <- sw32s, y <- sw32s] ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `op` y | x <- sw64s, y <- sw64s] ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `op` y | x <- si8s, y <- si8s ] ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `op` y | x <- si16s, y <- si16s] ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `op` y | x <- si32s, y <- si32s] ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `op` y | x <- si64s, y <- si64s] ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `op` y | x <- siUBs, y <- siUBs] where pair (x, y, a) b = (x, y, show (fromIntegral a `asTypeOf` b) == show b) mkTest (x, y, s) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True") genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [TestTree] genBoolTest nm op opS = map mkTest $ zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `opS` y | x <- sw8s, y <- sw8s ] ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `opS` y | x <- sw16s, y <- sw16s] ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `opS` y | x <- sw32s, y <- sw32s] ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `opS` y | x <- sw64s, y <- sw64s] ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `opS` y | x <- si8s, y <- si8s ] ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `opS` y | x <- si16s, y <- si16s] ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `opS` y | x <- si32s, y <- si32s] ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `opS` y | x <- si64s, y <- si64s] ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `opS` y | x <- siUBs, y <- siUBs] ++ zipWith pair [(show x, show y, x `op` y) | x <- iCs, y <- iCs ] [x `opS` y | x <- siCs, y <- siCs ] ++ zipWith pair [(show x, show y, x `op` y) | x <- ss, y <- ss ] [x `opS` y | x <- sss, y <- sss ] ++ zipWith pair [(show x, show y, toL x `op` toL y) | x <- ssl, y <- ssl ] [x `opS` y | x <- ssl, y <- ssl ] where pair (x, y, a) b = (x, y, Just a == unliteral b) mkTest (x, y, s) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True") toL x = fromMaybe (error "genBoolTest: Cannot extract a literal!") (unliteral x) genUnTest :: String -> (forall a. (Num a, Bits a) => a -> a) -> [TestTree] genUnTest nm op = map mkTest $ zipWith pair [(show x, op x) | x <- w8s ] [op x | x <- sw8s ] ++ zipWith pair [(show x, op x) | x <- w16s] [op x | x <- sw16s] ++ zipWith pair [(show x, op x) | x <- w32s] [op x | x <- sw32s] ++ zipWith pair [(show x, op x) | x <- w64s] [op x | x <- sw64s] ++ zipWith pair [(show x, op x) | x <- i8s ] [op x | x <- si8s ] ++ zipWith pair [(show x, op x) | x <- i16s] [op x | x <- si16s] ++ zipWith pair [(show x, op x) | x <- i32s] [op x | x <- si32s] ++ zipWith pair [(show x, op x) | x <- i64s] [op x | x <- si64s] ++ zipWith pair [(show x, op x) | x <- iUBs] [op x | x <- siUBs] where pair (x, a) b = (x, show (fromIntegral a `asTypeOf` b) == show b) mkTest (x, s) = testCase ("arithCF-" ++ nm ++ "." ++ x) (s `showsAs` "True") genIntTest :: Bool -> String -> (forall a. (Num a, Bits a) => (a -> Int -> a)) -> [TestTree] genIntTest overSized nm op = map mkTest $ zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- is (intSizeOf x)] [x `op` y | x <- sw8s, y <- is (intSizeOf x)] ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- is (intSizeOf x)] [x `op` y | x <- sw16s, y <- is (intSizeOf x)] ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- is (intSizeOf x)] [x `op` y | x <- sw32s, y <- is (intSizeOf x)] ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- is (intSizeOf x)] [x `op` y | x <- sw64s, y <- is (intSizeOf x)] ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- is (intSizeOf x)] [x `op` y | x <- si8s, y <- is (intSizeOf x)] ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- is (intSizeOf x)] [x `op` y | x <- si16s, y <- is (intSizeOf x)] ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- is (intSizeOf x)] [x `op` y | x <- si32s, y <- is (intSizeOf x)] ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- is (intSizeOf x)] [x `op` y | x <- si64s, y <- is (intSizeOf x)] ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0..10]] [x `op` y | x <- siUBs, y <- [0..10]] where is sz = [0 .. sz - 1] ++ extras where extras | overSized = map (sz +) ([0 .. 1] ++ [sz, sz+1]) | True = [] pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b) mkTest (t, x, y, a, b, s) = testCase ("arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b) (s `showsAs` "True") genShiftRotTest :: String -> (forall a. (SIntegral a, SDivisible (SBV a)) => (SBV a -> SBV a -> SBV a)) -> [TestTree] genShiftRotTest nm op = map mkTest $ zipWith pair [("u8", show x, show y, literal x `op` y) | x <- w8s, y <- is (intSizeOf x)] [x `op` y | x <- sw8s, y <- is (intSizeOf x)] ++ zipWith pair [("u16", show x, show y, literal x `op` y) | x <- w16s, y <- is (intSizeOf x)] [x `op` y | x <- sw16s, y <- is (intSizeOf x)] ++ zipWith pair [("u32", show x, show y, literal x `op` y) | x <- w32s, y <- is (intSizeOf x)] [x `op` y | x <- sw32s, y <- is (intSizeOf x)] ++ zipWith pair [("u64", show x, show y, literal x `op` y) | x <- w64s, y <- is (intSizeOf x)] [x `op` y | x <- sw64s, y <- is (intSizeOf x)] ++ zipWith pair [("s8", show x, show y, literal x `op` y) | x <- i8s, y <- is (intSizeOf x)] [x `op` y | x <- si8s, y <- is (intSizeOf x)] ++ zipWith pair [("s16", show x, show y, literal x `op` y) | x <- i16s, y <- is (intSizeOf x)] [x `op` y | x <- si16s, y <- is (intSizeOf x)] ++ zipWith pair [("s32", show x, show y, literal x `op` y) | x <- i32s, y <- is (intSizeOf x)] [x `op` y | x <- si32s, y <- is (intSizeOf x)] ++ zipWith pair [("s64", show x, show y, literal x `op` y) | x <- i64s, y <- is (intSizeOf x)] [x `op` y | x <- si64s, y <- is (intSizeOf x)] -- NB. No generic shift/rotate for SMTLib unbounded integers where is sz = let b :: Word32 b = fromIntegral sz in map (sFromIntegral . literal) $ [0 .. b - 1] ++ [b, b+1, 2*b, 2*b+1] pair (t, x, y, a) b = (t, x, y, show a, show b, isJust (unliteral a) && isJust (unliteral b) && unliteral a == unliteral b) mkTest (t, x, y, a, b, s) = testCase ("arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b) (s `showsAs` "True") -- A few tests for mixed-size shifts genShiftMixSize :: [TestTree] genShiftMixSize = map mkTest $ [pair (show x, show y, "shl_w8_w16", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- w8s, y <- yw16s] ++ [pair (show x, show y, "shr_w8_w16", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- w8s, y <- yw16s] ++ [pair (show x, show y, "shl_w16_w8", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- w16s, y <- w8s] ++ [pair (show x, show y, "shr_w16_w8", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- w16s, y <- w8s] ++ [pair (show x, show y, "shl_i8_i16", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- i8s, y <- yi16s] ++ [pair (show x, show y, "shr_i8_i16", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- i8s, y <- yi16s] ++ [pair (show x, show y, "shl_i16_i8", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- i16s, y <- i8s, y >= 0] ++ [pair (show x, show y, "shr_i16_i8", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- i16s, y <- i8s, y >= 0] ++ [pair (show x, show y, "shl_w8_i16", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- w8s, y <- yi16s] ++ [pair (show x, show y, "shr_w8_i16", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- w8s, y <- yi16s] ++ [pair (show x, show y, "shl_w16_i8", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- w16s, y <- i8s, y >= 0] ++ [pair (show x, show y, "shr_w16_i8", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- w16s, y <- i8s, y >= 0] ++ [pair (show x, show y, "shl_i8_w16", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- i8s, y <- yw16s] ++ [pair (show x, show y, "shr_i8_w16", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- i8s, y <- yw16s] ++ [pair (show x, show y, "shl_i16_w8", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- i16s, y <- w8s] ++ [pair (show x, show y, "shr_i16_w8", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- i16s, y <- w8s] where pair :: (Eq a, SymVal a, Show a) => (String, String, String, SBV a, a) -> (String, Bool) pair (x, y, l, sr, lr) = (l ++ "." ++ x ++ "_" ++ y ++ "_" ++ show (unliteral sr) ++ "_" ++ show lr, isJust (unliteral sr) && unliteral sr == Just lr) mkTest (l, s) = testCase ("arithCF-genShiftMixSize" ++ l) (s `showsAs` "True") yi16s :: [Int16] yi16s = [0, 255, 256, 257, maxBound] yw16s :: [Word16] yw16s = [0, 255, 256, 257, maxBound] genBlasts :: [TestTree] genBlasts = map mkTest $ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw8s ] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw8s ] ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si8s ] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si8s ] ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw16s] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw16s] ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si16s] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si16s] ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw32s] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw32s] ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si32s] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si32s] ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw64s] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw64s] ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si64s] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si64s] where mkTest (x, r) = testCase ("blast-" ++ x) (r `showsAs` "True") genCounts :: [TestTree] genCounts = map mkTest $ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SWord8 )) | x <- sw8s ] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SWord8 )) | x <- sw8s ] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SInt8 )) | x <- si8s ] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SInt8 )) | x <- si8s ] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SWord16)) | x <- sw16s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SWord16)) | x <- sw16s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SInt16 )) | x <- si16s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SInt16 )) | x <- si16s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SWord32)) | x <- sw32s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SWord32)) | x <- sw32s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SInt32 )) | x <- si32s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SInt32 )) | x <- si32s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SWord64)) | x <- sw64s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SWord64)) | x <- sw64s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SInt64 )) | x <- si64s] ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SInt64 )) | x <- si64s] where mkTest (x, r) = testCase ("count-" ++ x) (r `showsAs` "True") genIntCasts :: [TestTree] genIntCasts = map mkTest $ cast w8s ++ cast w16s ++ cast w32s ++ cast w64s ++ cast i8s ++ cast i16s ++ cast i32s ++ cast i64s ++ cast iUBs where mkTest (x, r) = testCase ("intCast-" ++ x) (r `showsAs` "True") lhs x = sFromIntegral (literal x) rhs x = literal (fromIntegral x) cast :: forall a. (Show a, Integral a, SymVal a) => [a] -> [(String, SBool)] cast xs = toWords xs ++ toInts xs toWords xs = [(show x, lhs x .== (rhs x :: SWord8 )) | x <- xs] ++ [(show x, lhs x .== (rhs x :: SWord16)) | x <- xs] ++ [(show x, lhs x .== (rhs x :: SWord32)) | x <- xs] ++ [(show x, lhs x .== (rhs x :: SWord64)) | x <- xs] toInts xs = [(show x, lhs x .== (rhs x :: SInt8 )) | x <- xs] ++ [(show x, lhs x .== (rhs x :: SInt16)) | x <- xs] ++ [(show x, lhs x .== (rhs x :: SInt32)) | x <- xs] ++ [(show x, lhs x .== (rhs x :: SInt64)) | x <- xs] ++ [(show x, lhs x .== (rhs x :: SInteger)) | x <- xs] genQRems :: [TestTree] genQRems = map mkTest $ zipWith pair [("divMod", show x, show y, x `divMod0` y) | x <- w8s, y <- w8s ] [x `sDivMod` y | x <- sw8s, y <- sw8s ] ++ zipWith pair [("divMod", show x, show y, x `divMod0` y) | x <- w16s, y <- w16s] [x `sDivMod` y | x <- sw16s, y <- sw16s] ++ zipWith pair [("divMod", show x, show y, x `divMod0` y) | x <- w32s, y <- w32s] [x `sDivMod` y | x <- sw32s, y <- sw32s] ++ zipWith pair [("divMod", show x, show y, x `divMod0` y) | x <- w64s, y <- w64s] [x `sDivMod` y | x <- sw64s, y <- sw64s] ++ zipWith pair [("divMod", show x, show y, x `divMod1` y) | x <- i8s, y <- i8s ] [x `sDivMod` y | x <- si8s, y <- si8s ] ++ zipWith pair [("divMod", show x, show y, x `divMod1` y) | x <- i16s, y <- i16s] [x `sDivMod` y | x <- si16s, y <- si16s] ++ zipWith pair [("divMod", show x, show y, x `divMod1` y) | x <- i32s, y <- i32s] [x `sDivMod` y | x <- si32s, y <- si32s] ++ zipWith pair [("divMod", show x, show y, x `divMod1` y) | x <- i64s, y <- i64s] [x `sDivMod` y | x <- si64s, y <- si64s] ++ zipWith pair [("divMod", show x, show y, x `divMod0` y) | x <- iUBs, y <- iUBs] [x `sDivMod` y | x <- siUBs, y <- siUBs] ++ zipWith pair [("quotRem", show x, show y, x `quotRem0` y) | x <- w8s, y <- w8s ] [x `sQuotRem` y | x <- sw8s, y <- sw8s ] ++ zipWith pair [("quotRem", show x, show y, x `quotRem0` y) | x <- w16s, y <- w16s] [x `sQuotRem` y | x <- sw16s, y <- sw16s] ++ zipWith pair [("quotRem", show x, show y, x `quotRem0` y) | x <- w32s, y <- w32s] [x `sQuotRem` y | x <- sw32s, y <- sw32s] ++ zipWith pair [("quotRem", show x, show y, x `quotRem0` y) | x <- w64s, y <- w64s] [x `sQuotRem` y | x <- sw64s, y <- sw64s] ++ zipWith pair [("quotRem", show x, show y, x `quotRem1` y) | x <- i8s, y <- i8s ] [x `sQuotRem` y | x <- si8s, y <- si8s ] ++ zipWith pair [("quotRem", show x, show y, x `quotRem1` y) | x <- i16s, y <- i16s] [x `sQuotRem` y | x <- si16s, y <- si16s] ++ zipWith pair [("quotRem", show x, show y, x `quotRem1` y) | x <- i32s, y <- i32s] [x `sQuotRem` y | x <- si32s, y <- si32s] ++ zipWith pair [("quotRem", show x, show y, x `quotRem1` y) | x <- i64s, y <- i64s] [x `sQuotRem` y | x <- si64s, y <- si64s] ++ zipWith pair [("quotRem", show x, show y, x `quotRem0` y) | x <- iUBs, y <- iUBs] [x `sQuotRem` y | x <- siUBs, y <- siUBs] where pair (nm, x, y, (r1, r2)) (e1, e2) = (nm, x, y, show (fromIntegral r1 `asTypeOf` e1, fromIntegral r2 `asTypeOf` e2) == show (e1, e2)) mkTest (nm, x, y, s) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True") -- Haskell's divMod and quotRem differs from SBV's in two ways: -- - when y is 0, Haskell throws an exception, SBV sets the result to 0; like in division -- - Haskell overflows if x == minBound and y == -1 for bounded signed types; but SBV returns minBound, 0; which is more meaningful -- NB. There was a ticket filed against the second anomaly above, See: http://ghc.haskell.org/trac/ghc/ticket/8695 -- But the Haskell folks decided not to fix it. Sigh.. overflow x y = x == minBound && y == -1 divMod0 x y = if y == 0 then (0, x) else x `divMod` y divMod1 x y = if overflow x y then (x, 0) else x `divMod0` y quotRem0 x y = if y == 0 then (0, x) else x `quotRem` y quotRem1 x y = if overflow x y then (x, 0) else x `quotRem0` y genReals :: [TestTree] genReals = map mkTest $ map ("+",) (zipWith pair [(show x, show y, x + y) | x <- rs, y <- rs ] [x + y | x <- srs, y <- srs ]) ++ map ("-",) (zipWith pair [(show x, show y, x - y) | x <- rs, y <- rs ] [x - y | x <- srs, y <- srs ]) ++ map ("*",) (zipWith pair [(show x, show y, x * y) | x <- rs, y <- rs ] [x * y | x <- srs, y <- srs ]) ++ map ("<",) (zipWith pair [(show x, show y, x < y) | x <- rs, y <- rs ] [x .< y | x <- srs, y <- srs ]) ++ map ("<=",) (zipWith pair [(show x, show y, x <= y) | x <- rs, y <- rs ] [x .<= y | x <- srs, y <- srs ]) ++ map (">",) (zipWith pair [(show x, show y, x > y) | x <- rs, y <- rs ] [x .> y | x <- srs, y <- srs ]) ++ map (">=",) (zipWith pair [(show x, show y, x >= y) | x <- rs, y <- rs ] [x .>= y | x <- srs, y <- srs ]) ++ map ("==",) (zipWith pair [(show x, show y, x == y) | x <- rs, y <- rs ] [x .== y | x <- srs, y <- srs ]) ++ map ("/=",) (zipWith pair [(show x, show y, x /= y) | x <- rs, y <- rs ] [x ./= y | x <- srs, y <- srs ]) ++ map ("/",) (zipWith pair [(show x, show y, x / y) | x <- rs, y <- rs, y /= 0] [x / y | x <- srs, y <- srs, unliteral y /= Just 0]) where pair (x, y, a) b = (x, y, Just a == unliteral b) mkTest (nm, (x, y, s)) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True") genFloats :: [TestTree] genFloats = bTests ++ uTests ++ fpTests1 ++ fpTests2 ++ converts where bTests = map mkTest2 $ floatRun2 "+" (+) (+) comb ++ doubleRun2 "+" (+) (+) comb ++ floatRun2 "-" (-) (-) comb ++ doubleRun2 "-" (-) (-) comb ++ floatRun2 "*" (*) (*) comb ++ doubleRun2 "*" (*) (*) comb ++ floatRun2 "/" (/) (/) comb ++ doubleRun2 "/" (/) (/) comb ++ floatRun2 "<" (<) (.<) combB ++ doubleRun2 "<" (<) (.<) combB ++ floatRun2 "<=" (<=) (.<=) combB ++ doubleRun2 "<=" (<=) (.<=) combB ++ floatRun2 ">" (>) (.>) combB ++ doubleRun2 ">" (>) (.>) combB ++ floatRun2 ">=" (>=) (.>=) combB ++ doubleRun2 ">=" (>=) (.>=) combB ++ floatRun2 "==" (==) (.==) combB ++ doubleRun2 "==" (==) (.==) combB ++ floatRun2 "/=" (/=) (./=) combN ++ doubleRun2 "/=" (/=) (./=) combN fpTests1 = map mkTest1 $ floatRun1 "abs" abs abs comb1 ++ floatRun1 "fpAbs" abs fpAbs comb1 ++ doubleRun1 "abs" abs abs comb1 ++ doubleRun1 "fpAbs" abs fpAbs comb1 ++ floatRun1 "negate" negate negate comb1 ++ floatRun1 "fpNeg" negate fpNeg comb1 ++ doubleRun1 "negate" negate negate comb1 ++ doubleRun1 "fpNeg" negate fpNeg comb1 ++ floatRun1M "fpSqrt" sqrt fpSqrt comb1 ++ doubleRun1M "fpSqrt" sqrt fpSqrt comb1 ++ floatRun1M "fpRoundToIntegral" fpRoundToIntegralH fpRoundToIntegral comb1 ++ doubleRun1M "fpRoundToIntegral" fpRoundToIntegralH fpRoundToIntegral comb1 ++ floatRun1 "signum" signum signum comb1 ++ doubleRun1 "signum" signum signum comb1 -- TODO. Can't possibly test fma, unless we FFI out to C. Leave it out for the time being fpTests2 = map mkTest2 $ floatRun2M "fpAdd" (+) fpAdd comb ++ doubleRun2M "fpAdd" (+) fpAdd comb ++ floatRun2M "fpSub" (-) fpSub comb ++ doubleRun2M "fpSub" (-) fpSub comb ++ floatRun2M "fpMul" (*) fpMul comb ++ doubleRun2M "fpMul" (*) fpMul comb ++ floatRun2M "fpDiv" (/) fpDiv comb ++ doubleRun2M "fpDiv" (/) fpDiv comb ++ floatRunMM "fpMin" fpMinH fpMin comb ++ doubleRunMM "fpMin" fpMinH fpMin comb ++ floatRunMM "fpMax" fpMaxH fpMax comb ++ doubleRunMM "fpMax" fpMaxH fpMax comb ++ floatRun2 "fpRem" fpRemH fpRem comb ++ doubleRun2 "fpRem" fpRemH fpRem comb ++ floatRun2 "fpIsEqualObject" fpIsEqualObjectH fpIsEqualObject combE ++ doubleRun2 "fpIsEqualObject" fpIsEqualObjectH fpIsEqualObject combE converts = [cvtTest ("toFP_Int8_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- i8s ] ++ [cvtTest ("toFP_Int16_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- i16s] ++ [cvtTest ("toFP_Int32_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- i32s] ++ [cvtTest ("toFP_Int64_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- i64s] ++ [cvtTest ("toFP_Word8_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- w8s ] ++ [cvtTest ("toFP_Word16_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- w16s] ++ [cvtTest ("toFP_Word32_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- w32s] ++ [cvtTest ("toFP_Word64_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- w64s] ++ [cvtTest ("toFP_Float_ToFloat", show x, toSFloat sRNE (literal x), literal x ) | x <- fs ] ++ [cvtTest ("toFP_Double_ToFloat", show x, toSFloat sRNE (literal x), literal (fp2fp x)) | x <- ds ] ++ [cvtTest ("toFP_Integer_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- iUBs] ++ [cvtTest ("toFP_Real_ToFloat", show x, toSFloat sRNE (literal x), fromRational (toRational x)) | x <- rs ] ++ [cvtTest ("toFP_Int8_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- i8s ] ++ [cvtTest ("toFP_Int16_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- i16s] ++ [cvtTest ("toFP_Int32_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- i32s] ++ [cvtTest ("toFP_Int64_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- i64s] ++ [cvtTest ("toFP_Word8_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- w8s ] ++ [cvtTest ("toFP_Word16_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- w16s] ++ [cvtTest ("toFP_Word32_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- w32s] ++ [cvtTest ("toFP_Word64_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- w64s] ++ [cvtTest ("toFP_Float_ToDouble", show x, toSDouble sRNE (literal x), literal (fp2fp x)) | x <- fs ] ++ [cvtTest ("toFP_Double_ToDouble", show x, toSDouble sRNE (literal x), literal x) | x <- ds ] ++ [cvtTest ("toFP_Integer_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- iUBs] ++ [cvtTest ("toFP_Real_ToDouble", show x, toSDouble sRNE (literal x), fromRational (toRational x)) | x <- rs ] -- NB. We don't constant fold float/double conversions, so we skip these -- ++ [cvtTest ("reinterp_Word32_Float", show x, sWord32AsSFloat (literal x), literal (CN.wordToFloat x)) | x <- w32s] ++ [cvtTest ("reinterp_Word64_Double", show x, sWord64AsSDouble (literal x), literal (CN.wordToDouble x)) | x <- w64s] ++ [cvtTestI ("reinterp_Float_Word32", show x, sFloatAsSWord32 (literal x), CN.floatToWord x) | x <- fs, not (isNaN x)] -- Not unique for NaN ++ [cvtTestI ("reinterp_Double_Word64", show x, sDoubleAsSWord64 (literal x), CN.doubleToWord x) | x <- ds, not (isNaN x)] -- Not unique for NaN floatRun1 nm f g cmb = [(nm, cmb (x, f x, extract (g (literal x)))) | x <- fs] doubleRun1 nm f g cmb = [(nm, cmb (x, f x, extract (g (literal x)))) | x <- ds] floatRun1M nm f g cmb = [(nm, cmb (x, f x, extract (g sRNE (literal x)))) | x <- fs] doubleRun1M nm f g cmb = [(nm, cmb (x, f x, extract (g sRNE (literal x)))) | x <- ds] floatRun2 nm f g cmb = [(nm, cmb (x, y, f x y, extract (g (literal x) (literal y)))) | x <- fs, y <- fs] doubleRun2 nm f g cmb = [(nm, cmb (x, y, f x y, extract (g (literal x) (literal y)))) | x <- ds, y <- ds] floatRun2M nm f g cmb = [(nm, cmb (x, y, f x y, extract (g sRNE (literal x) (literal y)))) | x <- fs, y <- fs] doubleRun2M nm f g cmb = [(nm, cmb (x, y, f x y, extract (g sRNE (literal x) (literal y)))) | x <- ds, y <- ds] floatRunMM nm f g cmb = [(nm, cmb (x, y, f x y, extract (g (literal x) (literal y)))) | x <- fs, y <- fs, not (alt0 x y || alt0 y x)] doubleRunMM nm f g cmb = [(nm, cmb (x, y, f x y, extract (g (literal x) (literal y)))) | x <- ds, y <- ds, not (alt0 x y || alt0 y x)] -- fpMin/fpMax: skip +0/-0 case as this is underspecified alt0 x y = isNegativeZero x && y == 0 && not (isNegativeZero y) uTests = map mkTest1 $ concatMap (checkPred fs sfs) predicates ++ concatMap (checkPred ds sds) predicates extract :: SymVal a => SBV a -> a extract = fromJust . unliteral comb (x, y, a, b) = (show x, show y, same a b) combB (x, y, a, b) = (show x, show y, checkNaN f x y a b) where f v w = not (v || w) -- All comparisons except /=: Both should be False if we have a NaN argument combN (x, y, a, b) = (show x, show y, checkNaN f x y a b) where f v w = v && w -- /=: Both should be True combE (x, y, a, b) = (show x, show y, a == b) comb1 (x, a, b) = (show x, same a b) same a b = (isNaN a && isNaN b) || (a == b) checkNaN f x y a b | isNaN x || isNaN y = f a b | True = a == b cvtTest (nm, x, a, b) = testCase ("fpConverts.arithmetic-CF-" ++ nm ++ "." ++ x) (same (extract a) (extract b) `showsAs` "True") cvtTestI (nm, x, a, b) = testCase ("fpConverts.arithmetic-CF-" ++ nm ++ "." ++ x) ((a .== literal b) `showsAs` "True") mkTest1 (nm, (x, s)) = testCase ("arithCF-" ++ nm ++ "." ++ x) (s `showsAs` "True") mkTest2 (nm, (x, y, s)) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True") checkPred :: Show a => [a] -> [SBV a] -> (String, SBV a -> SBool, a -> Bool) -> [(String, (String, Bool))] checkPred xs sxs (n, ps, p) = zipWith (chk n) (map (\x -> (x, p x)) xs) (map ps sxs) where chk nm (x, v) sv = (nm, (show x, Just v == unliteral sv)) predicates :: IEEEFloating a => [(String, SBV a -> SBool, a -> Bool)] predicates = [ ("fpIsNormal", fpIsNormal, fpIsNormalizedH) , ("fpIsSubnormal", fpIsSubnormal, isDenormalized) , ("fpIsZero", fpIsZero, (== 0)) , ("fpIsInfinite", fpIsInfinite, isInfinite) , ("fpIsNaN", fpIsNaN, isNaN) , ("fpIsNegative", fpIsNegative, \x -> x < 0 || isNegativeZero x) , ("fpIsPositive", fpIsPositive, \x -> x >= 0 && not (isNegativeZero x)) , ("fpIsNegativeZero", fpIsNegativeZero, isNegativeZero) , ("fpIsPositiveZero", fpIsPositiveZero, \x -> x == 0 && not (isNegativeZero x)) , ("fpIsPoint", fpIsPoint, \x -> not (isNaN x || isInfinite x)) ] genChars :: [TestTree] genChars = map mkTest $ [("ord", show c, check SC.ord cord c) | c <- cs] ++ [("toLower", show c, check SC.toLower C.toLower c) | c <- cs] ++ [("toUpper", show c, check SC.toUpper C.toUpper c) | c <- cs, toUpperExceptions c] ++ [("digitToInt", show c, check SC.digitToInt dig2Int c) | c <- cs, digitToIntRange c] ++ [("intToDigit", show c, check SC.intToDigit int2Dig c) | c <- [0 .. 15]] ++ [("isControl", show c, check SC.isControl C.isControl c) | c <- cs] ++ [("isSpace", show c, check SC.isSpace C.isSpace c) | c <- cs] ++ [("isLower", show c, check SC.isLower C.isLower c) | c <- cs] ++ [("isUpper", show c, check SC.isUpper C.isUpper c) | c <- cs] ++ [("isAlpha", show c, check SC.isAlpha C.isAlpha c) | c <- cs] ++ [("isAlphaNum", show c, check SC.isAlphaNum C.isAlphaNum c) | c <- cs] ++ [("isPrint", show c, check SC.isPrint C.isPrint c) | c <- cs] ++ [("isDigit", show c, check SC.isDigit C.isDigit c) | c <- cs] ++ [("isOctDigit", show c, check SC.isOctDigit C.isOctDigit c) | c <- cs] ++ [("isHexDigit", show c, check SC.isHexDigit C.isHexDigit c) | c <- cs] ++ [("isLetter", show c, check SC.isLetter C.isLetter c) | c <- cs] ++ [("isMark", show c, check SC.isMark C.isMark c) | c <- cs] ++ [("isNumber", show c, check SC.isNumber C.isNumber c) | c <- cs] ++ [("isPunctuation", show c, check SC.isPunctuation C.isPunctuation c) | c <- cs] ++ [("isSymbol", show c, check SC.isSymbol C.isSymbol c) | c <- cs] ++ [("isSeparator", show c, check SC.isSeparator C.isSeparator c) | c <- cs] ++ [("isAscii", show c, check SC.isAscii C.isAscii c) | c <- cs] ++ [("isLatin1", show c, check SC.isLatin1 C.isLatin1 c) | c <- cs] ++ [("isAsciiUpper", show c, check SC.isAsciiUpper C.isAsciiUpper c) | c <- cs] ++ [("isAsciiLower", show c, check SC.isAsciiLower C.isAsciiLower c) | c <- cs] where toUpperExceptions = (`notElem` "\181\255") digitToIntRange = (`elem` "0123456789abcdefABCDEF") cord :: Char -> Integer cord = fromIntegral . C.ord dig2Int :: Char -> Integer dig2Int = fromIntegral . C.digitToInt int2Dig :: Integer -> Char int2Dig = C.intToDigit . fromIntegral mkTest (nm, x, t) = testCase ("genChars-" ++ nm ++ "." ++ x) (assert t) check sop cop arg = case unliteral (sop (literal arg)) of Nothing -> False Just x -> x == cop arg genStrings :: [TestTree] genStrings = map mkTest1 ( [("length", show s, check1 SS.length strLen s ) | s <- ss ] ++ [("null", show s, check1 SS.null null s ) | s <- ss ] ++ [("head", show s, check1 SS.head head s ) | s <- ss, not (null s) ] ++ [("tail", show s, check1 SS.tail tail s ) | s <- ss, not (null s) ] ++ [("singleton", show c, check1 SS.singleton (: []) c ) | c <- cs ] ++ [("implode", show s, checkI SS.implode s ) | s <- ss ] ++ [("strToNat", show s, check1 SS.strToNat strToNat s ) | s <- ss ] ++ [("natToStr", show i, check1 SS.natToStr natToStr i ) | i <- iUBs ]) ++ map mkTest2 ( [("strToStrAt", show s, show i, check2 SS.strToStrAt strToStrAt s i ) | s <- ss, i <- range s ] ++ [("strToCharAt", show s, show i, check2 SS.strToCharAt strToCharAt s i ) | s <- ss, i <- range s ] ++ [("concat", show s, show s1, check2 SS.concat (++) s s1 ) | s <- ss, s1 <- ss ] ++ [("isInfixOf", show s, show s1, check2 SS.isInfixOf isInfixOf s s1 ) | s <- ss, s1 <- ss ] ++ [("isSuffixOf", show s, show s1, check2 SS.isSuffixOf isSuffixOf s s1 ) | s <- ss, s1 <- ss ] ++ [("isPrefixOf", show s, show s1, check2 SS.isPrefixOf isPrefixOf s s1 ) | s <- ss, s1 <- ss ] ++ [("take", show s, show i, check2 SS.take genericTake i s ) | s <- ss, i <- iUBs ] ++ [("drop", show s, show i, check2 SS.drop genericDrop i s ) | s <- ss, i <- iUBs ] ++ [("indexOf", show s, show s1, check2 SS.indexOf indexOf s s1 ) | s <- ss, s1 <- ss ]) ++ map mkTest3 ( [("subStr", show s, show i, show j, check3 SS.subStr subStr s i j ) | s <- ss, i <- range s, j <- range s, i + j <= genericLength s] ++ [("replace", show s, show s1, show s2, check3 SS.replace replace s s1 s2) | s <- ss, s1 <- ss, s2 <- ss ] ++ [("offsetIndexOf", show s, show s1, show i, check3 SS.offsetIndexOf offsetIndexOf s s1 i ) | s <- ss, s1 <- ss, i <- range s ]) where strLen :: String -> Integer strLen = fromIntegral . length strToNat :: String -> Integer strToNat s | all C.isDigit s && not (null s) = read s | True = -1 natToStr :: Integer -> String natToStr i | i >= 0 = show i | True = "" range :: String -> [Integer] range s = map fromIntegral [0 .. length s - 1] indexOf :: String -> String -> Integer indexOf s1 s2 = go 0 s1 where go i x | s2 `isPrefixOf` x = i | True = case x of "" -> -1 (_:r) -> go (i+1) r strToStrAt :: String -> Integer -> String s `strToStrAt` i = [s `strToCharAt` i] strToCharAt :: String -> Integer -> Char s `strToCharAt` i = s `genericIndex` i subStr :: String -> Integer -> Integer -> String subStr s i j = genericTake j (genericDrop i s) replace :: String -> String -> String -> String replace s "" y = y ++ s replace s x y = go s where go "" = "" go h@(c:rest) | x `isPrefixOf` h = y ++ drop (length x) h | True = c : go rest offsetIndexOf :: String -> String -> Integer -> Integer offsetIndexOf x y i = case indexOf (genericDrop i x) y of -1 -> -1 r -> r+i mkTest1 (nm, x, t) = testCase ("genStrings-" ++ nm ++ "." ++ x) (assert t) mkTest2 (nm, x, y, t) = testCase ("genStrings-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t) mkTest3 (nm, x, y, z, t) = testCase ("genStrings-" ++ nm ++ "." ++ x ++ "_" ++ y ++ "_" ++ z) (assert t) checkI sop s = case unliteral (sop (map literal s)) of Nothing -> False Just x -> s == x check1 sop cop arg = case unliteral (sop (literal arg)) of Nothing -> False Just x -> x == cop arg check2 sop cop arg1 arg2 = case unliteral (sop (literal arg1) (literal arg2)) of Nothing -> False Just x -> x == cop arg1 arg2 check3 sop cop arg1 arg2 arg3 = case unliteral (sop (literal arg1) (literal arg2) (literal arg3)) of Nothing -> False Just x -> x == cop arg1 arg2 arg3 genLists :: [TestTree] genLists = map mkTest1 ( [("length", show l, check1 SL.length llen l ) | l <- sl ] ++ [("null", show l, check1 SL.null null l ) | l <- sl ] ++ [("head", show l, check1 SL.head head l ) | l <- sl, not (null l) ] ++ [("tail", show l, check1 SL.tail tail l ) | l <- sl, not (null l) ] ++ [("singleton", show i, check1 SL.singleton (: []) i ) | i <- iUBs ] ++ [("implode", show l, checkI SL.implode id l ) | l <- sl ]) ++ map mkTest2 ( [("listToListAt", show l, show i, check2 SL.listToListAt listToListAt l i ) | l <- sl, i <- range l ] ++ [("elemAt", show l, show i, check2 SL.elemAt elemAt l i ) | l <- sl, i <- range l ] ++ [("concat", show l, show l1, check2 SL.concat (++) l l1 ) | l <- sl, l1 <- sl ] ++ [("isInfixOf", show l, show l1, check2 SL.isInfixOf isInfixOf l l1 ) | l <- sl, l1 <- sl ] ++ [("isSuffixOf", show l, show l1, check2 SL.isSuffixOf isSuffixOf l l1 ) | l <- sl, l1 <- sl ] ++ [("isPrefixOf", show l, show l1, check2 SL.isPrefixOf isPrefixOf l l1 ) | l <- sl, l1 <- sl ] ++ [("take", show l, show i, check2 SL.take genericTake i l ) | l <- sl, i <- iUBs ] ++ [("drop", show l, show i, check2 SL.drop genericDrop i l ) | l <- sl, i <- iUBs ] ++ [("indexOf", show l, show l1, check2 SL.indexOf indexOf l l1 ) | l <- sl, l1 <- sl ]) ++ map mkTest3 ( [("subList", show l, show i, show j, check3 SL.subList subList l i j ) | l <- sl, i <- range l, j <- range l, i + j <= genericLength l] ++ [("replace", show l, show l1, show l2, check3 SL.replace replace l l1 l2) | l <- sl, l1 <- sl, l2 <- sl ] ++ [("offsetIndexOf", show l, show l1, show i, check3 SL.offsetIndexOf offsetIndexOf l l1 i ) | l <- sl, l1 <- sl, i <- range l ]) where llen :: [Integer] -> Integer llen = fromIntegral . length range :: [Integer] -> [Integer] range l = map fromIntegral [0 .. length l - 1] indexOf :: [Integer] -> [Integer] -> Integer indexOf s1 s2 = go 0 s1 where go i x | s2 `isPrefixOf` x = i | True = case x of [] -> -1 (_:r) -> go (i+1) r listToListAt :: [Integer] -> Integer -> [Integer] s `listToListAt` i = [s `elemAt` i] elemAt :: [Integer] -> Integer -> Integer l `elemAt` i = l `genericIndex` i subList :: [Integer] -> Integer -> Integer -> [Integer] subList s i j = genericTake j (genericDrop i s) replace :: [Integer] -> [Integer] -> [Integer] -> [Integer] replace s [] y = y ++ s replace s x y = go s where go [] = [] go h@(c:rest) | x `isPrefixOf` h = y ++ drop (length x) h | True = c : go rest offsetIndexOf :: [Integer] -> [Integer] -> Integer -> Integer offsetIndexOf x y i = case indexOf (genericDrop i x) y of -1 -> -1 r -> r+i mkTest1 (nm, x, t) = testCase ("genLists-" ++ nm ++ "." ++ x) (assert t) mkTest2 (nm, x, y, t) = testCase ("genLists-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t) mkTest3 (nm, x, y, z, t) = testCase ("genLists-" ++ nm ++ "." ++ x ++ "_" ++ y ++ "_" ++ z) (assert t) checkI sop cop arg = case unliteral (sop (map literal arg)) of Nothing -> False Just x -> x == cop arg check1 sop cop arg = case unliteral (sop (literal arg)) of Nothing -> False Just x -> x == cop arg check2 sop cop arg1 arg2 = case unliteral (sop (literal arg1) (literal arg2)) of Nothing -> False Just x -> x == cop arg1 arg2 check3 sop cop arg1 arg2 arg3 = case unliteral (sop (literal arg1) (literal arg2) (literal arg3)) of Nothing -> False Just x -> x == cop arg1 arg2 arg3 -- Concrete test data xsUnsigned :: (Num a, Bounded a) => [a] xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound) xsSigned :: (Num a, Enum a, Bounded a) => [a] xsSigned = xsUnsigned ++ [-5 .. 5] w8s :: [Word8] w8s = xsUnsigned sw8s :: [SWord8] sw8s = xsUnsigned w16s :: [Word16] w16s = xsUnsigned sw16s :: [SWord16] sw16s = xsUnsigned w32s :: [Word32] w32s = xsUnsigned sw32s :: [SWord32] sw32s = xsUnsigned w64s :: [Word64] w64s = xsUnsigned sw64s :: [SWord64] sw64s = xsUnsigned i8s :: [Int8] i8s = xsSigned si8s :: [SInt8] si8s = xsSigned i16s :: [Int16] i16s = xsSigned si16s :: [SInt16] si16s = xsSigned i32s :: [Int32] i32s = xsSigned si32s :: [SInt32] si32s = xsSigned i64s :: [Int64] i64s = xsSigned si64s :: [SInt64] si64s = xsSigned iUBs :: [Integer] iUBs = [-1000000 .. -999995] ++ [-5 .. 5] ++ [999995 .. 1000000] siUBs :: [SInteger] siUBs = map literal iUBs rs :: [AlgReal] rs = [fromRational (i % d) | i <- nums, d <- dens] where nums = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 .. 1000001] dens = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000] srs :: [SReal] srs = map literal rs fs :: [Float] fs = xs ++ map (* (-1)) (filter (not . isNaN) xs) -- -nan is the same as nan where xs = [nan, infinity, 0, 0.5, 0.68302244, 0.5268265, 0.10283524, 5.8336496e-2, 1.0e-45] sfs :: [SFloat] sfs = map literal fs ds :: [Double] ds = xs ++ map (* (-1)) (filter (not . isNaN) xs) -- -nan is the same as nan where xs = [nan, infinity, 0, 0.5, 2.516632060108026e-2, 0.8601891300751106, 7.518897767550192e-2, 1.1656043286207285e-2, 5.0e-324] sds :: [SDouble] sds = map literal ds -- Currently we test over all latin-1 characters. But when Unicode comes along, we'll have to be more selective. cs :: String cs = map C.chr [0..255] -- For pair character ops, just take a subset iCs :: String iCs = map C.chr $ [0..5] ++ [98..102] ++ [250..255] siCs :: [SChar] siCs = map literal iCs -- Ditto for strings, just a few things ss :: [String] ss = ["", "palTRY", "teSTing", "SBV", "sTRIngs", "123", "surely", "thIS", "hI", "ly", "0"] sss :: [SString] sss = map literal ss -- Lists are the worst in coverage! sl :: [[Integer]] sl = [[], [0], [-1, 1], [-10, 0, 10], [3, 4, 5, 4, 5, 3]] -- Lists are the worst in coverage! ssl :: [SList Integer] ssl = map literal sl {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}