{- |
You can find the properties in the source code.
-}

{-# LANGUAGE ScopedTypeVariables #-}

module Number.Peano.Inf.Test 
    ( test
    ) where

import Number.Peano.Inf
import Test.LazySmallCheck hiding (test)
import Data.List

default (Nat)

------ helper functions

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
(<=>) = (==)


----------- Properties of Nat ------------

-- Note that (n::Nat) means that @n = 0, 1, 2..@ or @n = infinity@, but @inductive_infinity@ will not appear.

test :: IO ()
test = do

-- Eq

    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) ->  xor [n < m, n == m, m < n]


-- (<), (>), (>=), compare

    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

-- min, max

    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


-- diff

    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)

    -- infinity `diff` infinity  is undefined


-- zeroDiff, infDiff, (-), (-|)

    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 $ \(n::Nat) ->  n /= 0 ==>  infinity * n  ==  infinity

--    sm $ \(n::Nat) (m::Nat) ->  n * m  ==  m * n

--    sm $ \(n::Nat) (m::Nat) (k::Nat) ->  n * (m * k)  ==  (n * m) * k



-- minBound, maxBound

    sm $  minBound == (0::Nat)  &&  maxBound == infinity

    sm $ \(n::Nat) ->  minBound <= n

    sm $ \(n::Nat) ->  n <= maxBound


-- toInteger, fromInteger

    sm $ toInteger (0::Nat)  ==  0

    sm $ \(n::Nat) ->  n /= infinity ==>  toInteger (1 + n)  ==  1 + toInteger n

    -- toInteger infinity   is undefined

    sm $ \(n::Nat) ->  n /= infinity ==>  fromInteger (toInteger n)  ==  n

    sm $ \(n::Integer) ->  n >= 0 ==>  toInteger (fromInteger n :: Nat)  ==  n


-- toEnum, fromEnum

    sm $ \(n::Int) ->  n >= 0 ==>  (toEnum n :: Nat) == fromInteger (toInteger n)

    sm $ \(n::Nat) ->  n /= infinity ==>  toInteger (fromEnum n) == toInteger n


-- succ, pred

    sm $ \(n::Nat) ->  succ n  ==  1 + n

    sm $ \(n::Nat) ->  pred (1 + n)  ==  n


-- enumFrom

    sm $ \(n::Nat) ->  head [n.. ] == n

    sm $ \(n::Nat) ->  tail [n.. ] =~= [1+n.. ]

--    sm $ \(n::Nat) ->  [n.. ] =~= [n, 1+n.. ]


-- enumFromTo

    sm $ \(n::Nat) (m::Nat) ->  [n.. m] =~= takeWhile (<= m) [n..]


-- enumFromThen (non-decreasing)

    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.. ]


-- enumFromThen (non-increasing)

    sm $ \(n::Nat) (d::Nat) ->  d /= infinity ==>  tail [d+d+n, d+n.. ] =~= [d+n, n.. ]

--    sm $ \(n::Nat) (d::Nat) ->  tail [d+d+d+n, d+d+n.. ] =~= [d+d+n, d+n.. ]

    sm $ \(n::Nat) (d::Nat) ->  n < d ==>  tail [d+n, n.. ] == [n]


-- enumFromThenTo

    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..]


-- inductive_infininty

    sm $ \(n::Nat) ->  n /= infinity ==>  n < inductive_infinity



------- Lazyness properties of Nat ----------



    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) ->  undefined + n  >= n        -- raises an error

    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) ->  (n + undefined) `min` n == n       -- raises an error

    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