{-# LANGUAGE DataKinds, TypeOperators #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}

import Data.List (isInfixOf)
import Data.Proxy
import Data.Type.Bool
import Control.Exception
import Test.Tasty
import Test.Tasty.HUnit

import ErrorTests

import GHC.TypeLits
import GHC.TypeLits.Extra

test1 :: Proxy (GCD 6 8) -> Proxy 2
test1 = id

test2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 10 8))
test2 = id

test3 :: Proxy (CLog 3 10) -> Proxy 3
test3 = id

test4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 7))
test4 = id

test5 :: Proxy (CLog x (x^y)) -> Proxy y
test5 = id

test6 :: Integer
test6 = natVal (Proxy :: Proxy (CLog 6 8))

test7 :: Integer
test7 = natVal (Proxy :: Proxy (CLog 3 10))

test8 :: Integer
test8 = natVal (Proxy :: Proxy ((CLog 2 4) * (3 ^ (CLog 2 4))))

test9 :: Integer
test9 = natVal (Proxy :: Proxy (Max (CLog 2 4) (CLog 4 20)))

test10 :: Proxy (Div 9 3) -> Proxy 3
test10 = id

test11 :: Proxy (Div 9 4) -> Proxy 2
test11 = id

test12 :: Proxy (Mod 9 3) -> Proxy 0
test12 = id

test13 :: Proxy (Mod 9 4) -> Proxy 1
test13 = id

test14 :: Integer
test14 = natVal (Proxy :: Proxy (Div 9 3))

test15 :: Integer
test15 = natVal (Proxy :: Proxy (Mod 9 4))

test16 :: Proxy (LCM 18 7) -> Proxy 126
test16 = id

test17 :: Integer
test17 = natVal (Proxy :: Proxy (LCM 18 7))

test18 :: Proxy ((LCM 6 4) + x) -> Proxy (x + (LCM 3 4))
test18 = id

test19 :: Integer
test19 = natVal (Proxy :: Proxy (FLog 3 1))

test20 :: Proxy (FLog 3 1) -> Proxy 0
test20 = id

test21 :: Integer
test21 = natVal (Proxy :: Proxy (CLog 3 1))

test22 :: Proxy (CLog 3 1) -> Proxy 0
test22 = id

test23 :: Integer
test23 = natVal (Proxy :: Proxy (Log 3 1))

test24 :: Integer
test24 = natVal (Proxy :: Proxy (Log 3 9))

test25 :: Proxy (Log 3 9) -> Proxy 2
test25 = id

test26 :: Proxy (b ^ (Log b y)) -> Proxy y
test26 = id

test27 :: Proxy (Max n n) -> Proxy n
test27 = id

test28 :: Proxy (Min n n) -> Proxy n
test28 = id

test29 :: Proxy (Max n n + 1) -> Proxy (1 + n)
test29 = id

test30 :: Proxy n -> Proxy (1 + Max n n) -> Proxy (Min n n + 1)
test30 _ = id

main :: IO ()
main = defaultMain tests

tests :: TestTree
tests = testGroup "ghc-typelits-natnormalise"
  [ testGroup "Basic functionality"
    [ testCase "GCD 6 8 ~ 2" $
      show (test1 Proxy) @?=
      "Proxy"
    , testCase "forall x . GCD 6 8 + x ~ x + GCD 10 8" $
      show (test2 Proxy) @?=
      "Proxy"
    , testCase "CLog 3 10 ~ 3" $
      show (test3 Proxy) @?=
      "Proxy"
    , testCase "forall x . CLog 3 10 + x ~ x + CLog 2 7" $
      show (test4 Proxy) @?=
      "Proxy"
    , testCase "forall x>1 . CLog x (x^y) ~ y" $
      show (test5 Proxy) @?=
      "Proxy"
    , testCase "KnownNat (CLog 6 8) ~ 2" $
      show test6 @?=
      "2"
    , testCase "KnownNat (CLog 3 10) ~ 3" $
      show test7 @?=
      "3"
    , testCase "KnownNat ((CLog 2 4) * (3 ^ (CLog 2 4)))) ~ 18" $
      show test8 @?=
      "18"
    , testCase "KnownNat (Max (CLog 2 4) (CLog 4 20)) ~ 3" $
      show test9 @?=
      "3"
    , testCase "Div 9 3 ~ 3" $
      show (test10 Proxy) @?=
      "Proxy"
    , testCase "Div 9 4 ~ 2" $
      show (test11 Proxy) @?=
      "Proxy"
    , testCase "Mod 9 3 ~ 0" $
      show (test12 Proxy) @?=
      "Proxy"
    , testCase "Mod 9 4 ~ 1" $
      show (test13 Proxy) @?=
      "Proxy"
    , testCase "KnownNat (Div 9 3) ~ 3" $
      show test14 @?=
      "3"
    , testCase "KnownNat (Mod 9 4) ~ 1" $
      show test15 @?=
      "1"
    , testCase "LCM 18 7 ~ 126" $
      show (test16 Proxy) @?=
      "Proxy"
    , testCase "KnownNat (LCM 18 7) ~ 126" $
      show test17 @?=
      "126"
    , testCase "forall x . LCM 3 4 + x ~ x + LCM 6 4" $
      show (test18 Proxy) @?=
      "Proxy"
    , testCase "KnownNat (FLog 3 1) ~ 0" $
      show test19 @?=
      "0"
    , testCase "FLog 3 1 ~ 0" $
      show (test20 Proxy) @?=
      "Proxy"
    , testCase "KnownNat (CLog 3 1) ~ 0" $
      show test21 @?=
      "0"
    , testCase "CLog 3 1 ~ 0" $
      show (test22 Proxy) @?=
      "Proxy"
    , testCase "KnownNat (Log 3 1) ~ 0" $
      show test23 @?=
      "0"
    , testCase "KnownNat (Log 3 9) ~ 2" $
      show test24 @?=
      "2"
    , testCase "Log 3 9 ~ 2" $
      show (test25 Proxy) @?=
      "Proxy"
    , testCase "forall x>1 . x ^ (Log x y) ~ y" $
      show (test26 Proxy) @?=
      "Proxy"
    , testCase "forall x . Max x x ~ x" $
      show (test27 Proxy) @?=
      "Proxy"
    , testCase "forall x . Min x x ~ x" $
      show (test28 Proxy) @?=
      "Proxy"
    , testCase "forall x . (Max x x + 1) ~ (1 + x)" $
      show (test29 Proxy) @?=
      "Proxy"
    , testCase "forall x . (Min x x + 1) ~ (1 + Max x x)" $
      show (test30 Proxy Proxy) @?=
      "Proxy"
    ]
  , testGroup "errors"
    [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors
    , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail2 `throws` testFail2Errors
    , testCase "CLog 3 10 /~ 2" $ testFail3 `throws` testFail3Errors
    , testCase "CLog 3 10 + x /~ x + CLog 2 9" $ testFail4 `throws` testFail4Errors
    , testCase "CLog 0 4 /~ 100" $ testFail5 `throws` testFail5Errors
    , testCase "CLog 1 4 /~ 100" $ testFail5 `throws` testFail5Errors
    , testCase "CLog 4 0 /~ 0" $ testFail7 `throws` testFail7Errors
    , testCase "CLog 1 (1^y) /~ y" $ testFail8 `throws` testFail8Errors
    , testCase "CLog 0 (0^y) /~ y" $ testFail9 `throws` testFail9Errors
    , testCase "No instance (KnownNat (CLog 1 4))" $ testFail10 `throws` testFail10Errors
    , testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ testFail11 `throws` testFail11Errors
    , testCase "Div 4 0 /~ 4" $ testFail12 `throws` testFail12Errors
    , testCase "Mod 4 0 /~ 4" $ testFail13 `throws` testFail13Errors
    , testCase "FLog 0 4 /~ 100" $ testFail14 `throws` testFail14Errors
    , testCase "FLog 1 4 /~ 100" $ testFail15 `throws` testFail15Errors
    , testCase "FLog 4 0 /~ 0" $ testFail16 `throws` testFail16Errors
    , testCase "GCD 6 8 /~ 4" $ testFail17 `throws` testFail17Errors
    , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors
    , testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors
    , testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors
    ]
  ]

-- | Assert that evaluation of the first argument (to WHNF) will throw
-- an exception whose string representation contains the given
-- substrings.
throws :: a -> [String] -> Assertion
throws v xs = do
  result <- try (evaluate v)
  case result of
    Right _ -> assertFailure "No exception!"
    Left (TypeError msg) ->
      if all (`isInfixOf` msg) xs
         then return ()
         else assertFailure msg