module Number.Peano.Inf.Test
( test
) where
import Number.Peano.Inf
import Test.LazySmallCheck hiding (test)
import Data.List
default (Nat)
sm :: Testable a => a -> IO ()
sm = smallCheck 10
(=~=) :: Eq a => [a] -> [a] -> Bool
as =~= bs = take 15 as == take 15 bs
infix 1 <=>
(<=>) :: Bool -> Bool -> Bool
(<=>) = (==)
test :: IO ()
test = do
sm $ \(n::Nat) -> n == n
sm $ \(n::Nat) (m::Nat) -> n == m <=> m == n
sm $ \(n::Nat) (m::Nat) (k::Nat) -> n == m && m == k ==> n == k
sm $ \(n::Nat) (m::Nat) (k::Nat) -> n <= m && m <= k ==> n <= k
sm $ \(n::Nat) (m::Nat) -> n <= m && m <= n <=> n == m
sm $ \(n::Nat) (m::Nat) -> n <= m || m <= n
sm $ \(n::Nat) (m::Nat) -> n < m <=> n <= m && n /= m
sm $ \(n::Nat) (m::Nat) -> n > m <=> m < n
sm $ \(n::Nat) (m::Nat) -> n >= m <=> m <= n
sm $ \(n::Nat) (m::Nat) -> n `compare` m == case () of
_ | n < m -> LT
| n == m -> EQ
| n > m -> GT
sm $ \(n::Nat) (m::Nat) -> (n `min` m, n `max` m) `elem` [(n, m), (m, n)]
sm $ \(n::Nat) (m::Nat) -> n `min` m <= n && n `min` m <= m
sm $ \(n::Nat) (m::Nat) -> n `max` m >= n && n `max` m >= m
sm $ \(n::Nat) (m::Nat) -> n + m == m + n
sm $ \(n::Nat) (m::Nat) (k::Nat) -> n + (m + k) == (n + m) + k
sm $ \(n::Nat) -> 0 + n == n
sm $ \(n::Nat) -> infinity + n == infinity
sm $ \(n::Nat) -> n == infinity || n `elem` iterate (1+) 0
sm $ \(n::Nat) -> n /= infinity ==> n < 1 + n
sm $ \(n::Nat) (d::Nat) -> n /= infinity ==> (d + n) `diff` n == Left d
sm $ \(n::Nat) (d::Nat) -> n /= infinity ==> n `diff` (1 + d + n) == Right (1 + d)
sm $ \(n::Nat) (m::Nat) -> m /= infinity ==> n `zeroDiff` m == n `diff` m
sm $ infinity `zeroDiff` infinity == Left 0
sm $ \(n::Nat) (m::Nat) -> m /= infinity ==> n `infDiff` m == n `diff` m
sm $ infinity `infDiff` infinity == Left infinity
sm $ \(n::Nat) (m::Nat) -> n >= m && m /= infinity ==> Left (n m) == n `diff` m
sm $ \(n::Nat) (m::Nat) -> n >= m && m /= infinity ==> n -| m == n m
sm $ \(n::Nat) (m::Nat) -> n <= m && m /= infinity ==> n -| m == 0
sm $ \(n::Nat) -> 0 * n == 0
sm $ \(n::Nat) (m::Nat) -> (1 + n) * m == m + n * m
sm $ minBound == (0::Nat) && maxBound == infinity
sm $ \(n::Nat) -> minBound <= n
sm $ \(n::Nat) -> n <= maxBound
sm $ toInteger (0::Nat) == 0
sm $ \(n::Nat) -> n /= infinity ==> toInteger (1 + n) == 1 + toInteger n
sm $ \(n::Nat) -> n /= infinity ==> fromInteger (toInteger n) == n
sm $ \(n::Integer) -> n >= 0 ==> toInteger (fromInteger n :: Nat) == n
sm $ \(n::Int) -> n >= 0 ==> (toEnum n :: Nat) == fromInteger (toInteger n)
sm $ \(n::Nat) -> n /= infinity ==> toInteger (fromEnum n) == toInteger n
sm $ \(n::Nat) -> succ n == 1 + n
sm $ \(n::Nat) -> pred (1 + n) == n
sm $ \(n::Nat) -> head [n.. ] == n
sm $ \(n::Nat) -> tail [n.. ] =~= [1+n.. ]
sm $ \(n::Nat) (m::Nat) -> [n.. m] =~= takeWhile (<= m) [n..]
sm $ \(n::Nat) (m::Nat) -> take 2 [n, m.. ] == [n, m]
sm $ \(n::Nat) (d::Nat) -> tail [n, d+n.. ] =~= [d+n, d+d+n.. ]
sm $ \(n::Nat) (d::Nat) -> d /= infinity ==> tail [d+d+n, d+n.. ] =~= [d+n, n.. ]
sm $ \(n::Nat) (d::Nat) -> n < d ==> tail [d+n, n.. ] == [n]
sm $ \(n::Nat) (m::Nat) (k::Nat) -> [n, m.. k] =~= case n `compare` m of
LT -> takeWhile (<= k) [n, m..]
EQ -> [n, m..]
GT -> takeWhile (>= k) [n, m..]
sm $ \(n::Nat) -> n /= infinity ==> n < inductive_infinity
sm $ (0::Nat) <= undefined
sm $ infinity + undefined == infinity
sm $ \(n::Nat) -> n /= infinity ==> inductive_infinity + undefined > n
sm $ \(n::Nat) -> n + undefined >= n
sm $ \(n::Nat) -> n /= infinity ==> 1 + n + undefined > n
sm $ \(n::Nat) -> n `min` (n + undefined) == n
sm $ \(n::Nat) -> (1 + n + undefined) `min` n == n
sm $ \(n::Nat) (m::Nat) -> (n + undefined) `min` (m + undefined) >= n `min` m
sm $ \(n::Nat) (m::Nat) -> n `max` (m + undefined) >= m
sm $ \(n::Nat) (m::Nat) -> (m + undefined) `max` n >= m
sm $ \(n::Nat) (m::Nat) -> (n + undefined) `max` (m + undefined) >= n `min` m
sm $ \(n::Nat) -> (1 + undefined) * n >= n
sm $ \(n::Nat) -> n /= infinity ==> (1 + undefined) * inductive_infinity > n