Last active
August 3, 2020 09:05
-
-
Save minoki/b9a9ebaa70d99ac223232e85b01fb50e to your computer and use it in GitHub Desktop.
A code that exhibits "Impossible case alternative"
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE MagicHash #-} | |
module IntegerToInt where | |
import GHC.Integer.GMP.Internals (Integer (S#)) | |
-- import GHC.Num.Integer (Integer (IS)) | |
import GHC.Exts (Int (I#)) | |
-- Like Data.Bits.toIntegralSized, but optimized for Integer and Int | |
integerToIntMaybe :: Integer -> Maybe Int | |
integerToIntMaybe (S# x) = Just (I# x) | |
-- integerToIntMaybe (IS x) = Just (I# x) | |
integerToIntMaybe _ = Nothing -- relies on Integer's invariant | |
{-# INLINE [0] integerToIntMaybe #-} -- --> Impossible case alternative | |
-- {-# NOINLINE integerToIntMaybe #-} -- --> Segmentation fault | |
minBoundIntAsInteger :: Integer | |
minBoundIntAsInteger = fromIntegral (minBound :: Int) | |
{-# INLINE minBoundIntAsInteger #-} | |
maxBoundIntAsInteger :: Integer | |
maxBoundIntAsInteger = fromIntegral (maxBound :: Int) | |
{-# INLINE maxBoundIntAsInteger #-} | |
-- Helper function | |
integerToIntMaybe2 :: Bool -> Integer -> Maybe Int | |
integerToIntMaybe2 _ x = integerToIntMaybe x | |
-- No error with | |
-- integerToIntMaybe2 _ = integerToIntMaybe | |
{-# INLINE [0] integerToIntMaybe2 #-} | |
{-# RULES | |
"integerToIntMaybe" [~0] forall x. | |
integerToIntMaybe x = integerToIntMaybe2 (minBoundIntAsInteger <= x && x <= maxBoundIntAsInteger) x | |
"integerToIntMaybe2/small" forall x. | |
integerToIntMaybe2 True x = Just (fromIntegral x) | |
"integerToIntMaybe2/large" forall x. | |
integerToIntMaybe2 False x = Nothing | |
#-} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import IntegerToInt | |
noinline :: a -> a | |
noinline x = x | |
{-# NOINLINE noinline #-} | |
main = do | |
print (noinline integerToIntMaybe 3141) -- Just 3141 (at runtime) | |
print (integerToIntMaybe (2^20)) -- Just 1048576 (at runtime) | |
print (integerToIntMaybe 314159265398979323846264338327950) -- Nothing (at compile time) | |
print (integerToIntMaybe 3141) -- Just 3141 (at compile time) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment