{-# LANGUAGE ScopedTypeVariables #-}

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

import Number.Peano.Inf

import Test.LazySmallCheck hiding (test)

default (Nat)

test :: IO ()
test = do

-- Several lazyness properties

    smallCheck 10 $

        undefined >= (0::Nat)        

    smallCheck 10 $ \(n::Nat) -> and

        [   n + undefined >= n      -- but @undefined + n@ raises an error.

        ,   n /= infinity  ==>  (1 + n + undefined) `compare` n == GT       -- but @compare (n + undefined) n@ raises an error.

        ,   n `min` (n + undefined) == n

        ,   (1 + n + undefined) `min` n == n    -- but @min (n + undefined) n@ raises an error.
        ]

    smallCheck 10 $ \(m::Nat) (n::Nat) -> and

        [   (m + n) `min` (m + undefined) >= m

        ,   (m + undefined) `min` (m + n) >= m

        ,   n `max` (m + undefined) >= m

        ,   (m + undefined) `max` n >= m

        ]

-- Properties of infinity

    smallCheck 10 $ and 

        [   infinity == infinity

        ,   0 * infinity == 0

        ,   infinity * 0 == 0

        ]

    smallCheck 10 $ \(n::Nat) -> and

        [   n /= infinity ==>  n < infinity

        ,   n + infinity == infinity

        ,   infinity + n == infinity

        ,   n /= 0 ==>  n * infinity == infinity

        ,   n /= 0 ==>  infinity * n == infinity

        ,   n /= infinity ==>  infinity - n == infinity

        ]


{-
The following values raise error messages:

* @infinity - infinity@,

* @fromEnum infinity@,

* @toInteger infinity@.
-}