From 4832a5ec97c7bf47a6f4ef1e6ba6b48e89da16a3 Mon Sep 17 00:00:00 2001 From: Katherine Reid Date: Wed, 3 Jul 2024 13:01:15 -0500 Subject: [PATCH] moved local code to disco branch --- explore/arith-pat/ArithPat.agda | 16 -- explore/arith-pat/ArithPat.hs | 46 ----- explore/arith-pat/LICENSE | 30 ++++ explore/arith-pat/arith-pat.cabal | 43 +++++ explore/arith-pat/lib/ArithmeticPattern.hs | 63 +++++++ explore/arith-pat/lib/SemilinearSet.hs | 164 ++++++++++++++++++ explore/arith-pat/test/Main.hs | 11 ++ .../arith-pat/test/TestArithmeticPattern.hs | 70 ++++++++ explore/arith-pat/test/TestSemilinearSet.hs | 124 +++++++++++++ 9 files changed, 505 insertions(+), 62 deletions(-) delete mode 100644 explore/arith-pat/ArithPat.agda delete mode 100644 explore/arith-pat/ArithPat.hs create mode 100644 explore/arith-pat/LICENSE create mode 100644 explore/arith-pat/arith-pat.cabal create mode 100644 explore/arith-pat/lib/ArithmeticPattern.hs create mode 100644 explore/arith-pat/lib/SemilinearSet.hs create mode 100644 explore/arith-pat/test/Main.hs create mode 100644 explore/arith-pat/test/TestArithmeticPattern.hs create mode 100644 explore/arith-pat/test/TestSemilinearSet.hs diff --git a/explore/arith-pat/ArithPat.agda b/explore/arith-pat/ArithPat.agda deleted file mode 100644 index 17128ff3..00000000 --- a/explore/arith-pat/ArithPat.agda +++ /dev/null @@ -1,16 +0,0 @@ -open import Data.Nat -open import Data.Nat.DivMod -open import Data.Nat.LCM -open import Data.Fin -open import Data.Sum -open import Data.Product - -Sub : ℕ → Set₁ -Sub n = Fin n → Set - -ℤSet : Set₁ -ℤSet = Σ[ m ∈ ℕ ] (NonZero m × Sub m) - -_∪_ : ℤSet → ℤSet → ℤSet -(m₁ , (pf₁ , B₁)) ∪ (m₂ , (pf₂ , B₂)) = lcm m₁ m₂ , {!!} , λ x → B₁ (toℕ x mod m₁) ⊎ B₂ (toℕ x mod m₂) - diff --git a/explore/arith-pat/ArithPat.hs b/explore/arith-pat/ArithPat.hs deleted file mode 100644 index d41f0698..00000000 --- a/explore/arith-pat/ArithPat.hs +++ /dev/null @@ -1,46 +0,0 @@ -import Prelude hiding (elem) -import Prelude qualified as P - -import Control.Applicative - --- Key insight: of course we could simply use (Integer -> Bool) to --- represent sets of integers; then interpreting patterns, taking --- unions, etc. would be very easy. But testing for equality of such --- sets (e.g. testing for complete coverage by testing equality with Z --- itself) would be undecidable! So the name of the game is to add a --- bit more first-order information to represent the structure of the --- specific kinds of sets we can get, so that we can decide equality. - -data ZSet = ZSet Integer (Integer -> Bool) - -- modulus m paired with indicator function on [0..m) - -- ZSet m B represents the set { am + b | a ∈ ℤ, b ∈ B } - -ints :: ZSet -ints = ZSet 1 (const True) - -odds :: ZSet -odds = ZSet 2 (==1) - -evens :: ZSet -evens = ZSet 2 (==0) - -m31 :: ZSet -m31 = ZSet 3 (==1) - -m635 :: ZSet -m635 = ZSet 6 (`P.elem` [3,5]) - -elem :: ZSet -> Integer -> Bool -elem (ZSet m b) = b . (`mod` m) - -expand :: Integer -> ZSet -> ZSet -expand k (ZSet m b) = ZSet (k*m) (\x -> b (x `mod` m)) - -union :: ZSet -> ZSet -> ZSet -union s1@(ZSet m1 _) s2@(ZSet m2 _) = ZSet (lcm m1 m2) (liftA2 (||) (elem s1) (elem s2)) - -instance Eq ZSet where - s1@(ZSet m1 _) == s2@(ZSet m2 _) = all (liftA2 (==) (elem s1) (elem s2)) [0 .. m-1] - where - m = lcm m1 m2 - diff --git a/explore/arith-pat/LICENSE b/explore/arith-pat/LICENSE new file mode 100644 index 00000000..1f227e5b --- /dev/null +++ b/explore/arith-pat/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2024, Katherine Reid + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Katherine Reid nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/explore/arith-pat/arith-pat.cabal b/explore/arith-pat/arith-pat.cabal new file mode 100644 index 00000000..adec1157 --- /dev/null +++ b/explore/arith-pat/arith-pat.cabal @@ -0,0 +1,43 @@ +cabal-version: 3.0 +name: arith-pat +version: 0.1.0.0 +synopsis: Tools for testing completeness of arithmetic patterns +-- description: +license: BSD-3-Clause +license-file: LICENSE +author: Katherine Reid +maintainer: reidst@hendrix.edu +-- copyright: +category: Math +build-type: Simple +-- extra-doc-files: +-- extra-source-files: + +common warnings + ghc-options: -Wall + +library + import: warnings + exposed-modules: + ArithmeticPattern, + SemilinearSet + -- other-modules: + -- other-extensions: + build-depends: base ^>=4.17.2.1 + hs-source-dirs: lib + default-language: Haskell2010 + +test-suite arit-pat-test + import: warnings + default-language: Haskell2010 + other-modules: + TestArithmeticPattern, + TestSemilinearSet, + -- other-extensions: + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Main.hs + build-depends: + base ^>=4.17.2.1, + arith-pat, + QuickCheck diff --git a/explore/arith-pat/lib/ArithmeticPattern.hs b/explore/arith-pat/lib/ArithmeticPattern.hs new file mode 100644 index 00000000..48ed7b9b --- /dev/null +++ b/explore/arith-pat/lib/ArithmeticPattern.hs @@ -0,0 +1,63 @@ +module ArithmeticPattern where + +import SemilinearSet + +type Pattern = SS + +-- Pattern Constructions ------------------------------------------------------- + +-- | Constructs a pattern with a natrual number variable. +mkNatPattern :: Int -> Int -> Pattern +mkNatPattern x p = SS [LS x p] + +-- | Constructs a pattern with an integer variable. +mkIntPattern :: Int -> Int -> Pattern +mkIntPattern x p = SS [LS x p, LS x (-p)] + +-- | Constructs a pattern with no variable, representing a single number. +mkConstPattern :: Int -> Pattern +mkConstPattern x = SS [LS x 0] + +emptyPattern :: Pattern +emptyPattern = SS [] + +allNatsPattern :: Pattern +allNatsPattern = mkNatPattern 0 1 + +allIntsPattern :: Pattern +allIntsPattern = mkIntPattern 0 1 + +-- Coverage Checking ----------------------------------------------------------- + +-- | Checks if a number is covered by a pattern. +elemPattern :: Int -> Pattern -> Bool +elemPattern e (SS lss) = any (notNullSS . intersectWithSingle e) lss + where notNullSS (SS x) = not . null $ x + +-- | Subtracts +subtractPattern :: Pattern -> Pattern -> Pattern +subtractPattern a b = intersectSS a (complementSS b) + +-- | Generates a (potentially infinite) list of natural numbers not covered by +-- any of the given patterns. If the list is empty, then the pattern coverage is +-- complete. +missingNats :: [Pattern] -> [Int] +missingNats pats = toListSS $ intersectSS allNatsPattern $ complementSS unionSet + where unionSet = foldr unionSS (SS []) pats + +-- | Generates a (potentially infinite) list of integers not covered by any of +-- the given patterns. If the list is empty, then the pattern coverage is +-- complete. +missingInts :: [Pattern] -> [Int] +missingInts pats = toListSS $ complementSS unionSet + where unionSet = foldr unionSS emptyPattern pats + +-- | Checks whether a set of patterns covers the natural numbers. Shorthand for +-- `null . missingNats`. +coversNats :: [Pattern] -> Bool +coversNats = null . missingNats + +-- | Checks whether a set of patterns covers the integers. Shorthand for +-- `null . missingInts`. +coversInts :: [Pattern] -> Bool +coversInts = null . missingInts diff --git a/explore/arith-pat/lib/SemilinearSet.hs b/explore/arith-pat/lib/SemilinearSet.hs new file mode 100644 index 00000000..93198397 --- /dev/null +++ b/explore/arith-pat/lib/SemilinearSet.hs @@ -0,0 +1,164 @@ +module SemilinearSet where + +-- Types ----------------------------------------------------------------------- + +data LS = LS Int Int deriving (Show, Eq) -- (initial, period) + +newtype SS = SS [LS] deriving (Show, Eq) -- union + +-- List Representation --------------------------------------------------------- + +-- | Represents a linear set as a list of numbers. +toListLS :: LS -> [Int] +toListLS (LS x p) = if p == 0 then [x] else [x + p * i | i <- [0..]] + +-- | Represents a semilinear set as a list of numbers, sorted by absolute value +-- in ascending order. +toListSS :: SS -> [Int] +toListSS (SS lss) = answer + where + downLSs = filter (\(LS _ p) -> p < 0) lss + upLSs = filter (\(LS _ p) -> p >= 0) lss + downLists = map toListLS downLSs + upLists = map toListLS upLSs + downList = foldr (mergeSortedLists (>)) [] downLists + upList = foldr (mergeSortedLists (<)) [] upLists + (downPositives, downRest) = span (>= 0) downList + (upNegatives, upRest) = span (< 0) upList + allNegatives = mergeSortedLists (>) (reverse upNegatives) downRest + allPositives = mergeSortedLists (<) (reverse downPositives) upRest + answer = mergeSortedLists (\x y -> abs x < abs y) allNegatives allPositives + +-- | Merges two lists together via a selection function. The selection function +-- returning `True` means that the head of the first list will be taken first. +-- If the heads are equal, the first is taken and the second is discarded. +mergeSortedLists :: Eq a => (a -> a -> Bool) -> [a] -> [a] -> [a] +mergeSortedLists cmp (x:xs) (y:ys) + | x == y = x : mergeSortedLists cmp xs ys + | cmp x y = x : mergeSortedLists cmp xs (y:ys) + | otherwise = y : mergeSortedLists cmp (x:xs) ys +mergeSortedLists _ x y = x ++ y + +-- Set Helpers ----------------------------------------------------------------- + +-- | Negates the initial and period of a linear set, effectively mapping +-- negation over the elements of the set. +flipDirLS :: LS -> LS +flipDirLS (LS x p) = LS (-x) (-p) + +-- | Maps `flipDirLS` over the linear sets within a semilinear set. +flipDirSS :: SS -> SS +flipDirSS (SS lss) = SS $ map flipDirLS lss + +-- | Represents a linear set as an equivalent semilinear set. +toSS :: LS -> SS +toSS ls = SS [ls] + +-- | Checks if a number is an element of a linear set. +containsLS :: Int -> LS -> Bool +containsLS n (LS x p) = case compare p 0 of + LT -> n <= x && modEquiv p n x + GT -> n >= x && modEquiv p n x + EQ -> n == x + +-- | Sorts two linear sets by their initial value in descending order. +sort2LS :: LS -> LS -> ((Int, Int), (Int, Int)) +sort2LS (LS x1 p1) (LS x2 p2) = if x1 > x2 + then ((x1, p1), (x2, p2)) + else ((x2, p2), (x1, p1)) + +-- Set Operations -------------------------------------------------------------- + +-- | Intersects two singleton linear sets. +intersectTwoSingles :: Int -> Int -> SS +intersectTwoSingles x y = SS [LS x 0 | x == y] + +-- | Intersects a singleton linear set with a non-singleton one. +intersectWithSingle :: Int -> LS -> SS +intersectWithSingle s ls = SS [LS s 0 | containsLS s ls] + +-- | Intersects two linear sets when both have positive periods. Expects +-- arguments to have been sorted via `sort2LS`. +intersectSameDir :: LS -> LS -> SS +intersectSameDir lsa lsb = answer + where + ((x1, p1), (x2, p2)) = sort2LS lsa lsb + diff = x2 - x1 + p2dg = p2 `div` g + gp = gcd p1 p2 + g = gcd gp $ diff `mod` p2 + i = modInv p2dg (p1 `div` g) + k = mod (i * diff `div` g) p2dg + answer = if g == gp + then SS [LS (p1 * k + x1) (lcm p1 p2)] + else SS [] + +-- | Intersects two linear sets whose periods are opposite in sign. Expects the +-- first linear set to have a negative period, and the second to be positive. +intersectOppDir :: LS -> LS -> SS +intersectOppDir (LS xd pd) (LS xu pu) = answer + where + answer = SS $ map (\n -> LS n 0) filtered + filtered = filter (\n -> modEquiv pd n xd && modEquiv pu n xu) [xu..xd] + +-- | Intersects any two linear sets; the result is semilinear. +intersectLS :: LS -> LS -> SS +intersectLS lsa@(LS x1 p1) lsb@(LS x2 p2) = case (compare p1 0, compare p2 0) of + (EQ, EQ) -> intersectTwoSingles x1 x2 + (EQ, _) -> intersectWithSingle x1 lsb + ( _, EQ) -> intersectWithSingle x2 lsa + (LT, GT) -> intersectOppDir lsa lsb + (GT, LT) -> intersectOppDir lsb lsa + (GT, GT) -> intersectSameDir lsa lsb + (LT, LT) -> flipDirSS $ intersectSameDir (flipDirLS lsa) (flipDirLS lsb) + +-- | Intersects two semilinear sets. This is done by pairwise intersecting the +-- component linear sets and unioning those intersections. +intersectSS :: SS -> SS -> SS +intersectSS (SS as) (SS bs) = case intersectLS <$> as <*> bs of + [] -> SS [] + (c:cs) -> foldr unionSS c cs + +-- | Unions two semilinear sets; a trivial operation due to their structure. +unionSS :: SS -> SS -> SS +unionSS (SS a) (SS b) = SS $ a ++ b + +-- | Returns the set complement of the given linear set, which is semilinear. +complementLS :: LS -> SS +complementLS (LS x p) = case compare p 0 of + GT -> SS $ LS (x - 1) (-1) : [LS (x + i) p | i <- [1 .. p - 1]] + LT -> SS $ LS (x + 1) 1 : [LS (x + i) p | i <- [p + 1 .. -1]] + EQ -> SS [LS (x - 1) (-1), LS (x + 1) 1] + +-- | Returns the set complement of the given semilinear set. This is done by +-- complementing the component linear sets and intersecting them. +complementSS :: SS -> SS +complementSS (SS lss) = case map complementLS lss of + [] -> SS [LS 0 1, LS (-1) (-1)] + (x:xs) -> foldr intersectSS x xs + +-- | Returns the set difference of two linear sets; i.e. the intersection of A +-- with the complement of B. +subtractSS :: SS -> SS -> SS +subtractSS ssa ssb = intersectSS ssa (complementSS ssb) + +-- Math Helpers ---------------------------------------------------------------- + +-- | Runs the Extended Euclidean Algorithm. `egcd a b` returns `(gcd a b, x, y)` +-- such that `a*x + b*y == gcd a b`. +egcd :: Int -> Int -> (Int, Int, Int) +egcd 0 b = (b, 0, 1) +egcd a b = (g, t - d * s, s) + where + (g, s, t) = egcd m a + (d, m) = divMod b a + +-- | Calculates the multiplicative inverse for a given modulus. +-- `modInv m a = x` such that `mod (a*x) m == gcd a m`. +modInv :: Int -> Int -> Int +modInv m a = mod x m + where (_, x, _) = egcd a m + +-- | Determines whether two numbers are equivalent under a modulus. +modEquiv :: Int -> Int -> Int -> Bool +modEquiv m a b = mod a m == mod b m diff --git a/explore/arith-pat/test/Main.hs b/explore/arith-pat/test/Main.hs new file mode 100644 index 00000000..c8cb6161 --- /dev/null +++ b/explore/arith-pat/test/Main.hs @@ -0,0 +1,11 @@ +module Main (main) where + +import qualified TestSemilinearSet +import qualified TestPatternChecker + +main :: IO () +main = do + putStrLn "Running tests for SemilinearSet..." + TestSemilinearSet.runTests + putStrLn "Running tests for PatternChecker..." + TestPatternChecker.runTests diff --git a/explore/arith-pat/test/TestArithmeticPattern.hs b/explore/arith-pat/test/TestArithmeticPattern.hs new file mode 100644 index 00000000..b7988f59 --- /dev/null +++ b/explore/arith-pat/test/TestArithmeticPattern.hs @@ -0,0 +1,70 @@ +module TestPatternChecker (runTests) where + +import Control.Monad (unless) +import PatternChecker +import Test.QuickCheck + +-- Property Tests -------------------------------------------------------------- + +-- | Tests that the patterns `2n` and `2n+1` cover all natural numbers. +testEvenOddN :: Bool +testEvenOddN = null $ missingNats [evens, odds] + where + evens = mkNatPattern 0 2 + odds = mkNatPattern 1 2 + +-- | Tests that the patterns `2x` and `2x+1` cover all the integers. +testEvenOddZ :: Bool +testEvenOddZ = null $ missingInts [evens, odds] + where + evens = mkIntPattern 0 2 + odds = mkIntPattern 1 2 + +-- | Tests that `allNatsPattern` satisfies `coversNats`. +testNatsCover :: Bool +testNatsCover = coversNats [allNatsPattern] + +-- | Tests that `allIntsPattern` satisfies `coversInts`. +testIntsCover :: Bool +testIntsCover = coversInts [allIntsPattern] + +-- | Tests that an `n+k` pattern misses exactly the first k natural numbers. +testMissingN :: Int -> Bool +testMissingN x = missingNats [mkNatPattern n 1] == [0..n-1] + where n = abs x + +-- | Tests that no single natural number pattern can cover all integers. +testIntsNeedMultipleNatPatterns :: Int -> Int -> Bool +testIntsNeedMultipleNatPatterns x p = not $ coversInts [mkNatPattern x p] + +-- | Tests that all integer patterns with period 1 cover all integers. +testWildcardIntPattern :: Int -> Bool +testWildcardIntPattern x = coversInts [mkIntPattern x 1] + +-- | Tests that constant patterns contain the number they represent. +testConstantPatternContains :: Int -> Bool +testConstantPatternContains x = elemPattern x $ mkConstPattern x + +-- | Tests that constant patterns do not contain any other number. +testConstantContainsOne :: Int -> Int -> Bool +testConstantContainsOne x y = (x == y) || not (elemPattern x (mkConstPattern y)) + +-- Run Tests ------------------------------------------------------------------- + +tests :: [Property] +tests = + [ once testEvenOddN + , once testEvenOddZ + , once testNatsCover + , once testIntsCover + , withMaxSuccess 500 testMissingN + , withMaxSuccess 500 testIntsNeedMultipleNatPatterns + , withMaxSuccess 500 testWildcardIntPattern + , withMaxSuccess 500 testConstantPatternContains + , withMaxSuccess 500 testConstantContainsOne + ] + +runTests :: IO () +runTests = do + results <- mapM quickCheckResult tests + unless (all isSuccess results) $ fail "Not all tests passed" diff --git a/explore/arith-pat/test/TestSemilinearSet.hs b/explore/arith-pat/test/TestSemilinearSet.hs new file mode 100644 index 00000000..15982362 --- /dev/null +++ b/explore/arith-pat/test/TestSemilinearSet.hs @@ -0,0 +1,124 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module TestSemilinearSet (runTests) where + +import Control.Monad (unless) +import SemilinearSet +import Test.QuickCheck + +-- Typeclasses ----------------------------------------------------------------- + +instance Arbitrary LS where + arbitrary = do + x <- chooseInt (-maxTestSize, maxTestSize) + p <- chooseInt (-maxTestSize, maxTestSize) + return $ LS (x, p) + +instance Arbitrary SS where + arbitrary = do + lss <- scale (`div` 20) $ listOf arbitrary + return $ SS lss + +-- Test Helpers ---------------------------------------------------------------- + +-- | The absolute value limit up to which infinite lists should be tested. +maxTestSize :: Int +maxTestSize = 40 + +-- | Determines whether two semilinear sets consist of the same values up to +-- `maxTestSize`. +listEquivalent :: SS -> SS -> Bool +listEquivalent a b = toList' a == toList' b + where toList' = takeWhile ((<= maxTestSize) . abs) . toListSS + +-- | Checks if a set is equivalent to the set of all numbers. +isAllSS :: SS -> Bool +isAllSS = listEquivalent allSS + +-- | Checks if a set covers all natural numbers. +coversNats :: SS -> Bool +coversNats ss + = isEmptySS $ intersectSS natSS (complementSS ss) + +-- | Checks if the second set is a subset of the first. +isSubsetOf :: SS -> SS -> Bool +isSubsetOf sup sub = isEmptySS $ intersectSS sub (complementSS sup) + +-- | Checks if the second set is a superset of the first. +isSupersetOf :: SS -> SS -> Bool +isSupersetOf = flip isSubsetOf + +-- Property Tests -------------------------------------------------------------- + +-- | Tests that an empty semilinear set contains no values. +testEmptySS :: Bool +testEmptySS = null $ toListSS emptySS + +-- | Tests that the complement of an empty semilinear set contains all numbers. +testEmptyComplement :: Bool +testEmptyComplement + = isAllSS (complementSS emptySS) + && isEmptySS (complementSS allSS) + +-- | Tests that taking the complement of a semilinear set twice results in the +-- same set. +testDoubleComplement :: SS -> Bool +testDoubleComplement ss = listEquivalent ss $ (complementSS . complementSS) ss + +-- | Tests that intersecting a semilinear set with its complement results in the +-- empty set. +testIntersectWithComplement :: SS -> Bool +testIntersectWithComplement ss + = isEmptySS $ intersectSS ss (complementSS ss) + +-- | Tests that unioning a semilinear set with its complement contains all +-- numbers. +testUnionWithComplement :: SS -> Bool +testUnionWithComplement ss = isAllSS $ unionSS ss (complementSS ss) + +-- | Tests that the union of two sets is a superset of both. +testUnionIsSuperset :: SS -> SS -> Bool +testUnionIsSuperset ssa ssb = all (isSubsetOf ssu) [ssa, ssb] + where ssu = unionSS ssa ssb + +-- | Tests that the intersection of two sets is a subset of both. +testIntersectIsSubset :: SS -> SS -> Bool +testIntersectIsSubset ssa ssb = all (isSupersetOf ssi) [ssa, ssb] + where ssi = intersectSS ssa ssb + +-- | Tests that all sets are a superset of the empty set. +testEmptyIsAlwaysSubset :: SS -> Bool +testEmptyIsAlwaysSubset = isSupersetOf emptySS + +-- | Tests that the set of all numbers is a superset of all sets. +testAllIsAlwaysSuperset :: SS -> Bool +testAllIsAlwaysSuperset = isSubsetOf allSS + +-- | Tests that the union of all equivalence classes for a given modulus/period +-- covers all numbers. +testSamePeriodAllOffsets :: Int -> Bool +testSamePeriodAllOffsets n = coversNats offsets + where + p = abs n + 1 + offsets = SS $ LS (0, p) : [LS (x, p) | x <- [1..p-1]] + +-- Run Tests ------------------------------------------------------------------- + +tests :: [Property] +tests = + [ once testEmptySS + , once testEmptyComplement + , withMaxSuccess 10 testDoubleComplement + , withMaxSuccess 500 testIntersectWithComplement + , withMaxSuccess 500 testUnionWithComplement + , withMaxSuccess 50 testUnionIsSuperset + , withMaxSuccess 500 testIntersectIsSubset + , withMaxSuccess 500 testEmptyIsAlwaysSubset + , withMaxSuccess 500 testAllIsAlwaysSuperset + , withMaxSuccess 50 testSamePeriodAllOffsets + ] + +runTests :: IO () +runTests = do + results <- mapM quickCheckResult tests + unless (all isSuccess results) $ fail "Not all tests passed"