diff --git a/explore/arith-pat/lib/ArithmeticPattern.hs b/explore/arith-pat/lib/ArithmeticPattern.hs index 48ed7b9b..ddb800b7 100644 --- a/explore/arith-pat/lib/ArithmeticPattern.hs +++ b/explore/arith-pat/lib/ArithmeticPattern.hs @@ -1,5 +1,6 @@ module ArithmeticPattern where +import Prelude hiding (elem, null, subtract) import SemilinearSet type Pattern = SS @@ -18,46 +19,59 @@ mkIntPattern x p = SS [LS x p, LS x (-p)] mkConstPattern :: Int -> Pattern mkConstPattern x = SS [LS x 0] -emptyPattern :: Pattern -emptyPattern = SS [] +-- | The pattern covering nothing. +empty :: Pattern +empty = SS [] -allNatsPattern :: Pattern -allNatsPattern = mkNatPattern 0 1 +-- | The pattern covering all natural numbers; i.e. the nonnegative integers. +nats :: Pattern +nats = mkNatPattern 0 1 -allIntsPattern :: Pattern -allIntsPattern = mkIntPattern 0 1 +-- | The pattern covering all integers. +ints :: Pattern +ints = mkIntPattern 0 1 --- Coverage Checking ----------------------------------------------------------- +-- Pattern Operations ---------------------------------------------------------- + +-- | Lists all numbers covered by this pattern, in ascending order by absolute +-- value. +toList :: Pattern -> [Int] +toList = toListSS + +-- | Checks if a pattern covers nothing. +null :: Pattern -> Bool +null (SS []) = True +null _ = False -- | 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 +elem :: Int -> Pattern -> Bool +elem e (SS lss) = any (not . null . intersectWithSingle e) lss + +-- | Determines equality of patterns by checking if they are both a subset of +-- the other. +equal :: Pattern -> Pattern -> Bool +equal a b = subset a b && subset b a + +-- | Unions two patterns. +union :: Pattern -> Pattern -> Pattern +union = unionSS + +-- | Intersects two patterns. +intersect :: Pattern -> Pattern -> Pattern +intersect = intersectSS + +-- | Complements a pattern, inverting its coverage. +complement :: Pattern -> Pattern +complement = complementSS + +-- | Checks if the first pattern is entirely covered by the second. +subset :: Pattern -> Pattern -> Bool +subset a b = null $ subtract a b + +-- | Checks if the first pattern entirely covers the second. +superset :: Pattern -> Pattern -> Bool +superset = flip subset + +-- | Subtracts the second pattern from the first. +subtract :: Pattern -> Pattern -> Pattern +subtract a b = intersect a $ complement b diff --git a/explore/arith-pat/lib/SemilinearSet.hs b/explore/arith-pat/lib/SemilinearSet.hs index 93198397..553f2a4a 100644 --- a/explore/arith-pat/lib/SemilinearSet.hs +++ b/explore/arith-pat/lib/SemilinearSet.hs @@ -4,7 +4,7 @@ module SemilinearSet where data LS = LS Int Int deriving (Show, Eq) -- (initial, period) -newtype SS = SS [LS] deriving (Show, Eq) -- union +newtype SS = SS [LS] deriving (Show, Eq) -- union -- List Representation --------------------------------------------------------- @@ -121,7 +121,7 @@ intersectSS (SS as) (SS bs) = case intersectLS <$> as <*> bs of -- | Unions two semilinear sets; a trivial operation due to their structure. unionSS :: SS -> SS -> SS -unionSS (SS a) (SS b) = SS $ a ++ b +unionSS (SS a) (SS b) = SS (a ++ b) -- | Returns the set complement of the given linear set, which is semilinear. complementLS :: LS -> SS @@ -137,11 +137,6 @@ 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)` diff --git a/explore/arith-pat/test/Main.hs b/explore/arith-pat/test/Main.hs index c8cb6161..dfb8d38f 100644 --- a/explore/arith-pat/test/Main.hs +++ b/explore/arith-pat/test/Main.hs @@ -1,11 +1,11 @@ module Main (main) where import qualified TestSemilinearSet -import qualified TestPatternChecker +import qualified TestArithmeticPattern main :: IO () main = do putStrLn "Running tests for SemilinearSet..." TestSemilinearSet.runTests - putStrLn "Running tests for PatternChecker..." - TestPatternChecker.runTests + putStrLn "Running tests for ArithmeticPattern..." + TestArithmeticPattern.runTests diff --git a/explore/arith-pat/test/TestArithmeticPattern.hs b/explore/arith-pat/test/TestArithmeticPattern.hs index b7988f59..69569f96 100644 --- a/explore/arith-pat/test/TestArithmeticPattern.hs +++ b/explore/arith-pat/test/TestArithmeticPattern.hs @@ -1,53 +1,48 @@ -module TestPatternChecker (runTests) where +module TestArithmeticPattern (runTests) where import Control.Monad (unless) -import PatternChecker +import qualified ArithmeticPattern as P import Test.QuickCheck -- Property Tests -------------------------------------------------------------- -- | Tests that the patterns `2n` and `2n+1` cover all natural numbers. testEvenOddN :: Bool -testEvenOddN = null $ missingNats [evens, odds] +testEvenOddN = P.equal P.nats $ P.union evens odds where - evens = mkNatPattern 0 2 - odds = mkNatPattern 1 2 + evens = P.mkNatPattern 0 2 + odds = P.mkNatPattern 1 2 -- | Tests that the patterns `2x` and `2x+1` cover all the integers. testEvenOddZ :: Bool -testEvenOddZ = null $ missingInts [evens, odds] +testEvenOddZ = P.equal P.ints $ P.union 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] + evens = P.mkIntPattern 0 2 + odds = P.mkIntPattern 1 2 -- | 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 +testMissingN x = (== [0..k-1]) . P.toList . P.subtract P.nats $ nPlusK + where + k = abs x + nPlusK = P.mkNatPattern k 1 -- | Tests that no single natural number pattern can cover all integers. testIntsNeedMultipleNatPatterns :: Int -> Int -> Bool -testIntsNeedMultipleNatPatterns x p = not $ coversInts [mkNatPattern x p] +testIntsNeedMultipleNatPatterns x p + = not . null . P.toList . P.subtract P.ints $ P.mkNatPattern x p -- | Tests that all integer patterns with period 1 cover all integers. testWildcardIntPattern :: Int -> Bool -testWildcardIntPattern x = coversInts [mkIntPattern x 1] +testWildcardIntPattern x = P.equal P.ints $ P.mkIntPattern x 1 -- | Tests that constant patterns contain the number they represent. testConstantPatternContains :: Int -> Bool -testConstantPatternContains x = elemPattern x $ mkConstPattern x +testConstantPatternContains x = P.elem x $ P.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)) +testConstantContainsOne x y = (x == y) || not (P.elem x (P.mkConstPattern y)) -- Run Tests ------------------------------------------------------------------- @@ -55,13 +50,11 @@ 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 + , withMaxSuccess 200 testMissingN + , withMaxSuccess 200 testIntsNeedMultipleNatPatterns + , withMaxSuccess 200 testWildcardIntPattern + , withMaxSuccess 200 testConstantPatternContains + , withMaxSuccess 200 testConstantContainsOne ] runTests :: IO () diff --git a/explore/arith-pat/test/TestSemilinearSet.hs b/explore/arith-pat/test/TestSemilinearSet.hs index 15982362..3d610348 100644 --- a/explore/arith-pat/test/TestSemilinearSet.hs +++ b/explore/arith-pat/test/TestSemilinearSet.hs @@ -12,7 +12,7 @@ instance Arbitrary LS where arbitrary = do x <- chooseInt (-maxTestSize, maxTestSize) p <- chooseInt (-maxTestSize, maxTestSize) - return $ LS (x, p) + return $ LS x p instance Arbitrary SS where arbitrary = do @@ -25,20 +25,36 @@ instance Arbitrary SS where maxTestSize :: Int maxTestSize = 40 +-- | The empty set. +emptySS :: SS +emptySS = SS [] + +-- | The set containing all integers. +allSS :: SS +allSS = SS [LS 0 1, LS 0 (-1)] + +-- | The set containing all natural numbers. +natSS :: SS +natSS = SS [LS 0 1] + -- | 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 empty. +isEmptySS :: SS -> Bool +isEmptySS (SS []) = True +isEmptySS _ = False + -- | 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) +coversNats ss = isEmptySS $ intersectSS natSS (complementSS ss) -- | Checks if the second set is a subset of the first. isSubsetOf :: SS -> SS -> Bool @@ -100,7 +116,7 @@ testSamePeriodAllOffsets :: Int -> Bool testSamePeriodAllOffsets n = coversNats offsets where p = abs n + 1 - offsets = SS $ LS (0, p) : [LS (x, p) | x <- [1..p-1]] + offsets = SS $ LS 0 p : [LS x p | x <- [1..p-1]] -- Run Tests ------------------------------------------------------------------- @@ -109,13 +125,13 @@ 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 + , withMaxSuccess 200 testIntersectWithComplement + , withMaxSuccess 200 testUnionWithComplement + , withMaxSuccess 40 testUnionIsSuperset + , withMaxSuccess 200 testIntersectIsSubset + , withMaxSuccess 200 testEmptyIsAlwaysSubset + , withMaxSuccess 200 testAllIsAlwaysSuperset + , withMaxSuccess 40 testSamePeriodAllOffsets ] runTests :: IO ()