1{-# LANGUAGE CPP #-}
2{-# LANGUAGE ScopedTypeVariables #-}
3module ReifyNatSpec where
4
5#if __GLASGOW_HASKELL__ >= 708
6import Control.Exception (ArithException(..), evaluate)
7import Data.Reflection
8import Test.Hspec.QuickCheck
9import Test.QuickCheck (Negative(..), NonNegative(..))
10
11# if MIN_VERSION_base(4,10,0)
12import GHC.TypeNats (natVal)
13import Numeric.Natural (Natural)
14# endif
15#endif
16
17import Test.Hspec
18
19main :: IO ()
20main = hspec spec
21
22spec :: Spec
23spec =
24#if __GLASGOW_HASKELL__ >= 708
25  describe "reifyNat" $ do
26    prop "reify positive Integers and reflect them back" $
27      \(NonNegative (i :: Integer)) -> reifyNat i $ \p -> reflect p `shouldBe` i
28    prop "should throw an Underflow exception on negative inputs" $
29      \(Negative (i :: Integer)) ->
30        reifyNat i (evaluate . reflect) `shouldThrow` (== Underflow)
31# if MIN_VERSION_base(4,10,0)
32    it "should reflect very large Naturals correctly" $ do -- #41
33      let d42, d2_63, d2_64 :: Natural
34          d42   = 42
35          d2_63 = 2^(63 :: Natural)
36          d2_64 = 2^(64 :: Natural)
37      reifyNat (toInteger d42)       $ \p -> natVal p `shouldBe` d42
38      reifyNat (toInteger (d2_63-1)) $ \p -> natVal p `shouldBe` d2_63-1
39      reifyNat (toInteger d2_63)     $ \p -> natVal p `shouldBe` d2_63
40      reifyNat (toInteger (d2_64-1)) $ \p -> natVal p `shouldBe` d2_64-1
41      reifyNat (toInteger d2_64)     $ \p -> natVal p `shouldBe` d2_64
42# endif
43#else
44  return ()
45#endif
46