{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Main
  (main)
  where

import           Data.Function
import           Data.Int
import           Data.Proxy
import           Data.Word
import           GHC.TypeLits
import           Numeric.Natural
import           Numeric.Sized.IntOfSize
import           Numeric.Sized.WordOfSize
import           Test.DocTest
import           Test.QuickCheck          hiding (generate)
import qualified Test.SmallCheck          as SmallCheck
import           Test.SmallCheck.Series

instance KnownNat n =>
         Arbitrary (IntOfSize n) where
    arbitrary = arbitraryBoundedEnum

instance KnownNat n =>
         Arbitrary (WordOfSize n) where
    arbitrary = arbitraryBoundedEnum

instance (KnownNat n, Monad m) =>
         Serial m (IntOfSize n) where
    series = generate (`take` allIntsOfSize)

instance (KnownNat n, Monad m) =>
         Serial m (WordOfSize n) where
    series = generate (`take` allWordsOfSize)

type family IntType (n :: Nat) :: * where
        IntType 8  = Int8
        IntType 16 = Int16
        IntType 32 = Int32
        IntType 64 = Int64

type family WordType (n :: Nat) :: * where
        WordType 8  = Word8
        WordType 16 = Word16
        WordType 32 = Word32
        WordType 64 = Word64

sameConvAs
    :: (Integral n, Integral m, Integral i, Show i)
    => Proxy n -> Proxy m -> i -> Property
sameConvAs (_ :: Proxy n) (_ :: Proxy m) (x :: i) =
    ((fromIntegral :: n -> i) . (fromIntegral :: i -> n)) x ===
    ((fromIntegral :: m -> i) . (fromIntegral :: i -> m)) x

sameConvI
    :: (KnownNat n, Integral (IntType n))
    => Proxy n -> Integer -> Property
sameConvI (_ :: Proxy n) =
    sameConvAs (Proxy :: Proxy (IntOfSize n)) (Proxy :: Proxy (IntType n))

sameConvW
    :: (KnownNat n, Integral (WordType n))
    => Proxy n -> Natural -> Property
sameConvW (_ :: Proxy n) =
    sameConvAs (Proxy :: Proxy (WordOfSize n)) (Proxy :: Proxy (WordType n))

sameFncAs
    :: (Integral n, Integral m, Integral i, Show i)
    => (forall a. Integral a =>
                  a -> a -> a)
    -> Proxy n
    -> Proxy m
    -> i
    -> i
    -> Property
sameFncAs f (_ :: Proxy n) (_ :: Proxy m) (x :: i) (y :: i) =
    (fromIntegral :: n -> i) ((f `on` (fromIntegral :: i -> n)) x y) ===
    (fromIntegral :: m -> i) ((f `on` (fromIntegral :: i -> m)) x y)

sameFncI, sameFncINZRhs
    :: (KnownNat n, Integral (IntType n))
    => (forall a. Integral a =>
                  a -> a -> a)
    -> Proxy n
    -> Integer
    -> Integer
    -> Property
sameFncI f (_ :: Proxy n) =
    sameFncAs f (Proxy :: Proxy (IntOfSize n)) (Proxy :: Proxy (IntType n))

sameFncINZRhs f n x y = y /= 0 ==> sameFncI f n x y

sameFncW, sameFncWNZRhs
    :: (KnownNat n, Integral (WordType n))
    => (forall a. Integral a =>
                  a -> a -> a)
    -> Proxy n
    -> Natural
    -> Natural
    -> Property
sameFncW f (_ :: Proxy n) =
    sameFncAs f (Proxy :: Proxy (WordOfSize n)) (Proxy :: Proxy (WordType n))

sameFncWNZRhs f n x y = y /= 0 ==> sameFncW f n x y

sameFncAsS
    :: (Integral n, Integral m, Show n)
    => (forall a. Integral a =>
                  a -> a -> a)
    -> Proxy n
    -> Proxy m
    -> n
    -> n
    -> Either String String
sameFncAsS f (_ :: Proxy n) (_ :: Proxy m) x y =
    if (fromIntegral :: n -> m) (f x y) ==
       (f `on` (fromIntegral :: n -> m)) x y
        then Right ""
        else Left (show x ++ " " ++ show y)

sameFncWS
    :: (KnownNat n, Integral (WordType n))
    => (forall a. Integral a =>
                  a -> a -> a)
    -> Proxy n
    -> WordOfSize n
    -> WordOfSize n
    -> Either String String
sameFncWS f (_ :: Proxy n) =
    sameFncAsS f (Proxy :: Proxy (WordOfSize n)) (Proxy :: Proxy (WordType n))

sameFncWNZRhsS
    :: (KnownNat n, Integral (WordType n), Monad m)
    => (forall a. Integral a =>
                  a -> a -> a)
    -> Proxy n
    -> WordOfSize n
    -> WordOfSize n
    -> SmallCheck.Property m
sameFncWNZRhsS f n x y = y /= 0 SmallCheck.==> sameFncWS f n x y

sameFncIS
    :: (KnownNat n, Integral (IntType n))
    => (forall a. Integral a =>
                  a -> a -> a)
    -> Proxy n
    -> IntOfSize n
    -> IntOfSize n
    -> Either String String
sameFncIS f (_ :: Proxy n) =
    sameFncAsS f (Proxy :: Proxy (IntOfSize n)) (Proxy :: Proxy (IntType n))

sameFncINZRhsS
    :: (KnownNat n, Integral (IntType n), Monad m, Bounded (IntOfSize n))
    => (forall a. Integral a =>
                  a -> a -> a)
    -> Proxy n
    -> IntOfSize n
    -> IntOfSize n
    -> SmallCheck.Property m
sameFncINZRhsS f n x y =
    y /= 0 && (x /= minBound || y /= -1) SmallCheck.==> sameFncIS f n x y

testAll
    :: Testable a
    => (forall n. (KnownNat n, Integral (WordType n), Integral (IntType n)) =>
                  Proxy n -> a)
    -> IO ()
testAll prop = do
    quickCheck (prop (Proxy :: Proxy 8))
    quickCheck (prop (Proxy :: Proxy 16))
    quickCheck (prop (Proxy :: Proxy 32))
    quickCheck (prop (Proxy :: Proxy 64))

main :: IO ()
main = do
    testAll sameConvI
    testAll sameConvW
    testAll (sameFncI (+))
    testAll (sameFncW (+))
    testAll (sameFncI (*))
    testAll (sameFncW (*))
    testAll (sameFncI (-))
    testAll (sameFncW (-))
    testAll (sameFncINZRhs div)
    testAll (sameFncWNZRhs div)
    testAll (sameFncINZRhs mod)
    testAll (sameFncWNZRhs mod)
    testAll (sameFncINZRhs rem)
    testAll (sameFncWNZRhs rem)
    testAll (sameFncINZRhs quot)
    testAll (sameFncWNZRhs quot)
    SmallCheck.smallCheck 100000 (sameFncWS (+) (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncIS (+) (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncWS (*) (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncIS (*) (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncWS (-) (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncIS (-) (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncWNZRhsS div (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncINZRhsS div (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncWNZRhsS mod (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncINZRhsS mod (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncWNZRhsS rem (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncINZRhsS rem (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncWNZRhsS quot (Proxy :: Proxy 8))
    SmallCheck.smallCheck 100000 (sameFncINZRhsS quot (Proxy :: Proxy 8))
    doctest ["-isrc", "src/"]