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