{- |
Adapted from 'Data.SafeInt' to perform saturating arithmetic (i.e. returning max or min bounds) instead of throwing on overflow.

This is not quite as fast as using 'Int' or 'Int64' directly, but we need the safety.
-}
{-# LANGUAGE BangPatterns       #-}
{-# LANGUAGE CPP                #-}
{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE MagicHash          #-}
{-# LANGUAGE UnboxedTuples      #-}
module Data.SatInt (SatInt) where

import Control.DeepSeq (NFData)
import Data.Aeson (FromJSON, ToJSON)
import Data.Bits
import Data.Csv
import Data.Primitive (Prim)
import GHC.Base
import GHC.Generics
#if MIN_VERSION_base(4,16,0)
import GHC.Integer (smallInteger)
#endif
import GHC.Num
import GHC.Real
import Language.Haskell.TH.Syntax (Lift)
import NoThunks.Class

newtype SatInt = SI { SatInt -> Int
unSatInt :: Int }
    deriving newtype (SatInt -> ()
(SatInt -> ()) -> NFData SatInt
forall a. (a -> ()) -> NFData a
rnf :: SatInt -> ()
$crnf :: SatInt -> ()
NFData, Eq SatInt
SatInt
Eq SatInt
-> (SatInt -> SatInt -> SatInt)
-> (SatInt -> SatInt -> SatInt)
-> (SatInt -> SatInt -> SatInt)
-> (SatInt -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> SatInt
-> (Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> Bool)
-> (SatInt -> Maybe Int)
-> (SatInt -> Int)
-> (SatInt -> Bool)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int -> SatInt)
-> (SatInt -> Int)
-> Bits SatInt
Int -> SatInt
SatInt -> Bool
SatInt -> Int
SatInt -> Maybe Int
SatInt -> SatInt
SatInt -> Int -> Bool
SatInt -> Int -> SatInt
SatInt -> SatInt -> SatInt
forall a.
Eq a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> a
-> (Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> Bool)
-> (a -> Maybe Int)
-> (a -> Int)
-> (a -> Bool)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int)
-> Bits a
popCount :: SatInt -> Int
$cpopCount :: SatInt -> Int
rotateR :: SatInt -> Int -> SatInt
$crotateR :: SatInt -> Int -> SatInt
rotateL :: SatInt -> Int -> SatInt
$crotateL :: SatInt -> Int -> SatInt
unsafeShiftR :: SatInt -> Int -> SatInt
$cunsafeShiftR :: SatInt -> Int -> SatInt
shiftR :: SatInt -> Int -> SatInt
$cshiftR :: SatInt -> Int -> SatInt
unsafeShiftL :: SatInt -> Int -> SatInt
$cunsafeShiftL :: SatInt -> Int -> SatInt
shiftL :: SatInt -> Int -> SatInt
$cshiftL :: SatInt -> Int -> SatInt
isSigned :: SatInt -> Bool
$cisSigned :: SatInt -> Bool
bitSize :: SatInt -> Int
$cbitSize :: SatInt -> Int
bitSizeMaybe :: SatInt -> Maybe Int
$cbitSizeMaybe :: SatInt -> Maybe Int
testBit :: SatInt -> Int -> Bool
$ctestBit :: SatInt -> Int -> Bool
complementBit :: SatInt -> Int -> SatInt
$ccomplementBit :: SatInt -> Int -> SatInt
clearBit :: SatInt -> Int -> SatInt
$cclearBit :: SatInt -> Int -> SatInt
setBit :: SatInt -> Int -> SatInt
$csetBit :: SatInt -> Int -> SatInt
bit :: Int -> SatInt
$cbit :: Int -> SatInt
zeroBits :: SatInt
$czeroBits :: SatInt
rotate :: SatInt -> Int -> SatInt
$crotate :: SatInt -> Int -> SatInt
shift :: SatInt -> Int -> SatInt
$cshift :: SatInt -> Int -> SatInt
complement :: SatInt -> SatInt
$ccomplement :: SatInt -> SatInt
xor :: SatInt -> SatInt -> SatInt
$cxor :: SatInt -> SatInt -> SatInt
.|. :: SatInt -> SatInt -> SatInt
$c.|. :: SatInt -> SatInt -> SatInt
.&. :: SatInt -> SatInt -> SatInt
$c.&. :: SatInt -> SatInt -> SatInt
$cp1Bits :: Eq SatInt
Bits, Bits SatInt
Bits SatInt
-> (SatInt -> Int)
-> (SatInt -> Int)
-> (SatInt -> Int)
-> FiniteBits SatInt
SatInt -> Int
forall b.
Bits b -> (b -> Int) -> (b -> Int) -> (b -> Int) -> FiniteBits b
countTrailingZeros :: SatInt -> Int
$ccountTrailingZeros :: SatInt -> Int
countLeadingZeros :: SatInt -> Int
$ccountLeadingZeros :: SatInt -> Int
finiteBitSize :: SatInt -> Int
$cfiniteBitSize :: SatInt -> Int
$cp1FiniteBits :: Bits SatInt
FiniteBits, Addr# -> Int# -> SatInt
Addr# -> Int# -> Int# -> SatInt -> State# s -> State# s
Addr# -> Int# -> State# s -> (# State# s, SatInt #)
Addr# -> Int# -> SatInt -> State# s -> State# s
ByteArray# -> Int# -> SatInt
MutableByteArray# s -> Int# -> State# s -> (# State# s, SatInt #)
MutableByteArray# s -> Int# -> SatInt -> State# s -> State# s
MutableByteArray# s
-> Int# -> Int# -> SatInt -> State# s -> State# s
SatInt -> Int#
(SatInt -> Int#)
-> (SatInt -> Int#)
-> (ByteArray# -> Int# -> SatInt)
-> (forall s.
    MutableByteArray# s -> Int# -> State# s -> (# State# s, SatInt #))
-> (forall s.
    MutableByteArray# s -> Int# -> SatInt -> State# s -> State# s)
-> (forall s.
    MutableByteArray# s
    -> Int# -> Int# -> SatInt -> State# s -> State# s)
-> (Addr# -> Int# -> SatInt)
-> (forall s. Addr# -> Int# -> State# s -> (# State# s, SatInt #))
-> (forall s. Addr# -> Int# -> SatInt -> State# s -> State# s)
-> (forall s.
    Addr# -> Int# -> Int# -> SatInt -> State# s -> State# s)
-> Prim SatInt
forall s. Addr# -> Int# -> Int# -> SatInt -> State# s -> State# s
forall s. Addr# -> Int# -> State# s -> (# State# s, SatInt #)
forall s. Addr# -> Int# -> SatInt -> State# s -> State# s
forall s.
MutableByteArray# s
-> Int# -> Int# -> SatInt -> State# s -> State# s
forall s.
MutableByteArray# s -> Int# -> State# s -> (# State# s, SatInt #)
forall s.
MutableByteArray# s -> Int# -> SatInt -> State# s -> State# s
forall a.
(a -> Int#)
-> (a -> Int#)
-> (ByteArray# -> Int# -> a)
-> (forall s.
    MutableByteArray# s -> Int# -> State# s -> (# State# s, a #))
-> (forall s.
    MutableByteArray# s -> Int# -> a -> State# s -> State# s)
-> (forall s.
    MutableByteArray# s -> Int# -> Int# -> a -> State# s -> State# s)
-> (Addr# -> Int# -> a)
-> (forall s. Addr# -> Int# -> State# s -> (# State# s, a #))
-> (forall s. Addr# -> Int# -> a -> State# s -> State# s)
-> (forall s. Addr# -> Int# -> Int# -> a -> State# s -> State# s)
-> Prim a
setOffAddr# :: Addr# -> Int# -> Int# -> SatInt -> State# s -> State# s
$csetOffAddr# :: forall s. Addr# -> Int# -> Int# -> SatInt -> State# s -> State# s
writeOffAddr# :: Addr# -> Int# -> SatInt -> State# s -> State# s
$cwriteOffAddr# :: forall s. Addr# -> Int# -> SatInt -> State# s -> State# s
readOffAddr# :: Addr# -> Int# -> State# s -> (# State# s, SatInt #)
$creadOffAddr# :: forall s. Addr# -> Int# -> State# s -> (# State# s, SatInt #)
indexOffAddr# :: Addr# -> Int# -> SatInt
$cindexOffAddr# :: Addr# -> Int# -> SatInt
setByteArray# :: MutableByteArray# s
-> Int# -> Int# -> SatInt -> State# s -> State# s
$csetByteArray# :: forall s.
MutableByteArray# s
-> Int# -> Int# -> SatInt -> State# s -> State# s
writeByteArray# :: MutableByteArray# s -> Int# -> SatInt -> State# s -> State# s
$cwriteByteArray# :: forall s.
MutableByteArray# s -> Int# -> SatInt -> State# s -> State# s
readByteArray# :: MutableByteArray# s -> Int# -> State# s -> (# State# s, SatInt #)
$creadByteArray# :: forall s.
MutableByteArray# s -> Int# -> State# s -> (# State# s, SatInt #)
indexByteArray# :: ByteArray# -> Int# -> SatInt
$cindexByteArray# :: ByteArray# -> Int# -> SatInt
alignment# :: SatInt -> Int#
$calignment# :: SatInt -> Int#
sizeOf# :: SatInt -> Int#
$csizeOf# :: SatInt -> Int#
Prim)
    deriving stock (SatInt -> Q Exp
SatInt -> Q (TExp SatInt)
(SatInt -> Q Exp) -> (SatInt -> Q (TExp SatInt)) -> Lift SatInt
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: SatInt -> Q (TExp SatInt)
$cliftTyped :: SatInt -> Q (TExp SatInt)
lift :: SatInt -> Q Exp
$clift :: SatInt -> Q Exp
Lift, (forall x. SatInt -> Rep SatInt x)
-> (forall x. Rep SatInt x -> SatInt) -> Generic SatInt
forall x. Rep SatInt x -> SatInt
forall x. SatInt -> Rep SatInt x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SatInt x -> SatInt
$cfrom :: forall x. SatInt -> Rep SatInt x
Generic)
    deriving (Value -> Parser [SatInt]
Value -> Parser SatInt
(Value -> Parser SatInt)
-> (Value -> Parser [SatInt]) -> FromJSON SatInt
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [SatInt]
$cparseJSONList :: Value -> Parser [SatInt]
parseJSON :: Value -> Parser SatInt
$cparseJSON :: Value -> Parser SatInt
FromJSON, [SatInt] -> Encoding
[SatInt] -> Value
SatInt -> Encoding
SatInt -> Value
(SatInt -> Value)
-> (SatInt -> Encoding)
-> ([SatInt] -> Value)
-> ([SatInt] -> Encoding)
-> ToJSON SatInt
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [SatInt] -> Encoding
$ctoEncodingList :: [SatInt] -> Encoding
toJSONList :: [SatInt] -> Value
$ctoJSONList :: [SatInt] -> Value
toEncoding :: SatInt -> Encoding
$ctoEncoding :: SatInt -> Encoding
toJSON :: SatInt -> Value
$ctoJSON :: SatInt -> Value
ToJSON) via Int
    deriving Field -> Parser SatInt
(Field -> Parser SatInt) -> FromField SatInt
forall a. (Field -> Parser a) -> FromField a
parseField :: Field -> Parser SatInt
$cparseField :: Field -> Parser SatInt
FromField via Int  -- For reading cost model data from CSV input
    deriving anyclass Context -> SatInt -> IO (Maybe ThunkInfo)
Proxy SatInt -> String
(Context -> SatInt -> IO (Maybe ThunkInfo))
-> (Context -> SatInt -> IO (Maybe ThunkInfo))
-> (Proxy SatInt -> String)
-> NoThunks SatInt
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy SatInt -> String
$cshowTypeOf :: Proxy SatInt -> String
wNoThunks :: Context -> SatInt -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> SatInt -> IO (Maybe ThunkInfo)
noThunks :: Context -> SatInt -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> SatInt -> IO (Maybe ThunkInfo)
NoThunks

instance Show SatInt where
  showsPrec :: Int -> SatInt -> ShowS
showsPrec Int
p SatInt
x = Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (SatInt -> Int
unSatInt SatInt
x)

instance Read SatInt where
  readsPrec :: Int -> ReadS SatInt
readsPrec Int
p String
xs = [ (Int -> SatInt
SI Int
x, String
r) | (Int
x, String
r) <- Int -> ReadS Int
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs ]

instance Eq SatInt where
  SI Int
x == :: SatInt -> SatInt -> Bool
== SI Int
y = Int -> Int -> Bool
eqInt Int
x Int
y
  SI Int
x /= :: SatInt -> SatInt -> Bool
/= SI Int
y = Int -> Int -> Bool
neInt Int
x Int
y

instance Ord SatInt where
  SI Int
x < :: SatInt -> SatInt -> Bool
<  SI Int
y = Int -> Int -> Bool
ltInt Int
x Int
y
  SI Int
x <= :: SatInt -> SatInt -> Bool
<= SI Int
y = Int -> Int -> Bool
leInt Int
x Int
y
  SI Int
x > :: SatInt -> SatInt -> Bool
>  SI Int
y = Int -> Int -> Bool
gtInt Int
x Int
y
  SI Int
x >= :: SatInt -> SatInt -> Bool
>= SI Int
y = Int -> Int -> Bool
geInt Int
x Int
y

-- | In the `Num' instance, we plug in our own addition, multiplication
-- and subtraction function that perform overflow-checking.
instance Num SatInt where
  + :: SatInt -> SatInt -> SatInt
(+)               = SatInt -> SatInt -> SatInt
plusSI
  * :: SatInt -> SatInt -> SatInt
(*)               = SatInt -> SatInt -> SatInt
timesSI
  (-)               = SatInt -> SatInt -> SatInt
minusSI
  negate :: SatInt -> SatInt
negate (SI Int
y)
    | Int
y Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
minBound = SatInt
forall a. Bounded a => a
maxBound
    | Bool
otherwise     = Int -> SatInt
SI (Int -> Int
forall a. Num a => a -> a
negate Int
y)
  abs :: SatInt -> SatInt
abs SatInt
x
    | SatInt
x SatInt -> SatInt -> Bool
forall a. Ord a => a -> a -> Bool
>= SatInt
0        = SatInt
x
    | Bool
otherwise     = SatInt -> SatInt
forall a. Num a => a -> a
negate SatInt
x
  signum :: SatInt -> SatInt
signum (SI Int
x)     = Int -> SatInt
SI (Int -> Int
forall a. Num a => a -> a
signum Int
x)
  fromInteger :: Integer -> SatInt
fromInteger Integer
x
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
maxBoundInteger  = SatInt
forall a. Bounded a => a
maxBound
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
minBoundInteger  = SatInt
forall a. Bounded a => a
minBound
    | Bool
otherwise            = Int -> SatInt
SI (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
x)

maxBoundInteger :: Integer
maxBoundInteger :: Integer
maxBoundInteger = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
maxInt

minBoundInteger :: Integer
minBoundInteger :: Integer
minBoundInteger = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
minInt

instance Bounded SatInt where

  minBound :: SatInt
minBound = Int -> SatInt
SI Int
minInt
  maxBound :: SatInt
maxBound = Int -> SatInt
SI Int
maxInt

instance Enum SatInt where
  succ :: SatInt -> SatInt
succ (SI Int
x) = Int -> SatInt
SI (Int -> Int
forall a. Enum a => a -> a
succ Int
x)
  pred :: SatInt -> SatInt
pred (SI Int
x) = Int -> SatInt
SI (Int -> Int
forall a. Enum a => a -> a
pred Int
x)
  toEnum :: Int -> SatInt
toEnum                = Int -> SatInt
SI
  fromEnum :: SatInt -> Int
fromEnum              = SatInt -> Int
unSatInt

  {-# INLINE enumFrom #-}
  enumFrom :: SatInt -> [SatInt]
enumFrom (SI (I# Int#
x)) = Int# -> Int# -> [SatInt]
eftInt Int#
x Int#
maxInt#
      where !(I# Int#
maxInt#) = Int
maxInt

  {-# INLINE enumFromTo #-}
  enumFromTo :: SatInt -> SatInt -> [SatInt]
enumFromTo (SI (I# Int#
x)) (SI (I# Int#
y)) = Int# -> Int# -> [SatInt]
eftInt Int#
x Int#
y

  {-# INLINE enumFromThen #-}
  enumFromThen :: SatInt -> SatInt -> [SatInt]
enumFromThen (SI (I# Int#
x1)) (SI (I# Int#
x2)) = Int# -> Int# -> [SatInt]
efdInt Int#
x1 Int#
x2

  {-# INLINE enumFromThenTo #-}
  enumFromThenTo :: SatInt -> SatInt -> SatInt -> [SatInt]
enumFromThenTo (SI (I# Int#
x1)) (SI (I# Int#
x2)) (SI (I# Int#
y)) = Int# -> Int# -> Int# -> [SatInt]
efdtInt Int#
x1 Int#
x2 Int#
y

-- The following code is copied/adapted from GHC.Enum.

{-# RULES
"eftInt"        [~1] forall x y. eftInt x y = build (\ c n -> eftIntFB c n x y)
"eftIntList"    [1] eftIntFB  (:) [] = eftInt
 #-}

{-# NOINLINE [1] eftInt #-}
eftInt :: Int# -> Int# -> [SatInt]
-- [x1..x2]
eftInt :: Int# -> Int# -> [SatInt]
eftInt Int#
x0 Int#
y | Int# -> Bool
isTrue# (Int#
x0 Int# -> Int# -> Int#
># Int#
y) = []
            | Bool
otherwise = Int# -> [SatInt]
go Int#
x0
               where
                 go :: Int# -> [SatInt]
go Int#
x = Int -> SatInt
SI (Int# -> Int
I# Int#
x) SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: if Int# -> Bool
isTrue# (Int#
x Int# -> Int# -> Int#
==# Int#
y) then [] else Int# -> [SatInt]
go (Int#
x Int# -> Int# -> Int#
+# Int#
1#)

{-# INLINE [0] eftIntFB #-}
eftIntFB :: (SatInt -> r -> r) -> r -> Int# -> Int# -> r
eftIntFB :: (SatInt -> r -> r) -> r -> Int# -> Int# -> r
eftIntFB SatInt -> r -> r
c r
n Int#
x0 Int#
y | Int# -> Bool
isTrue# (Int#
x0 Int# -> Int# -> Int#
># Int#
y) = r
n
                  | Bool
otherwise = Int# -> r
go Int#
x0
                 where
                   go :: Int# -> r
go Int#
x = Int -> SatInt
SI (Int# -> Int
I# Int#
x) SatInt -> r -> r
`c` if Int# -> Bool
isTrue# (Int#
x Int# -> Int# -> Int#
==# Int#
y) then r
n else Int# -> r
go (Int#
x Int# -> Int# -> Int#
+# Int#
1#)
                        -- Watch out for y=maxBound; hence ==, not >
        -- Be very careful not to have more than one "c"
        -- so that when eftInfFB is inlined we can inline
        -- whatever is bound to "c"

{-# RULES
"efdtInt"       [~1] forall x1 x2 y.
                     efdtInt x1 x2 y = build (\ c n -> efdtIntFB c n x1 x2 y)
"efdtIntUpList" [1]  efdtIntFB (:) [] = efdtInt
 #-}

efdInt :: Int# -> Int# -> [SatInt]
-- [x1,x2..maxInt]
efdInt :: Int# -> Int# -> [SatInt]
efdInt Int#
x1 Int#
x2
 | Int# -> Bool
isTrue# (Int#
x2 Int# -> Int# -> Int#
>=# Int#
x1) = case Int
maxInt of I# Int#
y -> Int# -> Int# -> Int# -> [SatInt]
efdtIntUp Int#
x1 Int#
x2 Int#
y
 | Bool
otherwise = case Int
minInt of I# Int#
y -> Int# -> Int# -> Int# -> [SatInt]
efdtIntDn Int#
x1 Int#
x2 Int#
y

{-# NOINLINE [1] efdtInt #-}
efdtInt :: Int# -> Int# -> Int# -> [SatInt]
-- [x1,x2..y]
efdtInt :: Int# -> Int# -> Int# -> [SatInt]
efdtInt Int#
x1 Int#
x2 Int#
y
 | Int# -> Bool
isTrue# (Int#
x2 Int# -> Int# -> Int#
>=# Int#
x1) = Int# -> Int# -> Int# -> [SatInt]
efdtIntUp Int#
x1 Int#
x2 Int#
y
 | Bool
otherwise = Int# -> Int# -> Int# -> [SatInt]
efdtIntDn Int#
x1 Int#
x2 Int#
y

{-# INLINE [0] efdtIntFB #-}
efdtIntFB :: (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
efdtIntFB :: (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
efdtIntFB SatInt -> r -> r
c r
n Int#
x1 Int#
x2 Int#
y
 | Int# -> Bool
isTrue# (Int#
x2 Int# -> Int# -> Int#
>=# Int#
x1) = (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
forall r. (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
efdtIntUpFB SatInt -> r -> r
c r
n Int#
x1 Int#
x2 Int#
y
 | Bool
otherwise  = (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
forall r. (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
efdtIntDnFB SatInt -> r -> r
c r
n Int#
x1 Int#
x2 Int#
y

-- Requires x2 >= x1
efdtIntUp :: Int# -> Int# -> Int# -> [SatInt]
efdtIntUp :: Int# -> Int# -> Int# -> [SatInt]
efdtIntUp Int#
x1 Int#
x2 Int#
y    -- Be careful about overflow!
 | Int# -> Bool
isTrue# (Int#
y Int# -> Int# -> Int#
<# Int#
x2) = if Int# -> Bool
isTrue# (Int#
y Int# -> Int# -> Int#
<# Int#
x1) then [] else [Int -> SatInt
SI (Int# -> Int
I# Int#
x1)]
 | Bool
otherwise = -- Common case: x1 <= x2 <= y
               let !delta :: Int#
delta = Int#
x2 Int# -> Int# -> Int#
-# Int#
x1 -- >= 0
                   !y' :: Int#
y' = Int#
y Int# -> Int# -> Int#
-# Int#
delta  -- x1 <= y' <= y; hence y' is representable

                   -- Invariant: x <= y
                   -- Note that: z <= y' => z + delta won't overflow
                   -- so we are guaranteed not to overflow if/when we recurse
                   go_up :: Int# -> [SatInt]
go_up Int#
x | Int# -> Bool
isTrue# (Int#
x Int# -> Int# -> Int#
># Int#
y') = [Int -> SatInt
SI (Int# -> Int
I# Int#
x)]
                           | Bool
otherwise = Int -> SatInt
SI (Int# -> Int
I# Int#
x) SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: Int# -> [SatInt]
go_up (Int#
x Int# -> Int# -> Int#
+# Int#
delta)
               in Int -> SatInt
SI (Int# -> Int
I# Int#
x1) SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: Int# -> [SatInt]
go_up Int#
x2

-- Requires x2 >= x1
{-# INLINE [0] efdtIntUpFB #-}
efdtIntUpFB :: (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
efdtIntUpFB :: (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
efdtIntUpFB SatInt -> r -> r
c r
n Int#
x1 Int#
x2 Int#
y    -- Be careful about overflow!
 | Int# -> Bool
isTrue# (Int#
y Int# -> Int# -> Int#
<# Int#
x2) = if Int# -> Bool
isTrue# (Int#
y Int# -> Int# -> Int#
<# Int#
x1) then r
n else Int -> SatInt
SI (Int# -> Int
I# Int#
x1) SatInt -> r -> r
`c` r
n
 | Bool
otherwise = -- Common case: x1 <= x2 <= y
               let !delta :: Int#
delta = Int#
x2 Int# -> Int# -> Int#
-# Int#
x1 -- >= 0
                   !y' :: Int#
y' = Int#
y Int# -> Int# -> Int#
-# Int#
delta  -- x1 <= y' <= y; hence y' is representable

                   -- Invariant: x <= y
                   -- Note that: z <= y' => z + delta won't overflow
                   -- so we are guaranteed not to overflow if/when we recurse
                   go_up :: Int# -> r
go_up Int#
x | Int# -> Bool
isTrue# (Int#
x Int# -> Int# -> Int#
># Int#
y') = Int -> SatInt
SI (Int# -> Int
I# Int#
x) SatInt -> r -> r
`c` r
n
                           | Bool
otherwise = Int -> SatInt
SI (Int# -> Int
I# Int#
x) SatInt -> r -> r
`c` Int# -> r
go_up (Int#
x Int# -> Int# -> Int#
+# Int#
delta)
               in Int -> SatInt
SI (Int# -> Int
I# Int#
x1) SatInt -> r -> r
`c` Int# -> r
go_up Int#
x2

-- Requires x2 <= x1
efdtIntDn :: Int# -> Int# -> Int# -> [SatInt]
efdtIntDn :: Int# -> Int# -> Int# -> [SatInt]
efdtIntDn Int#
x1 Int#
x2 Int#
y    -- Be careful about underflow!
 | Int# -> Bool
isTrue# (Int#
y Int# -> Int# -> Int#
># Int#
x2) = if Int# -> Bool
isTrue# (Int#
y Int# -> Int# -> Int#
># Int#
x1) then [] else [Int -> SatInt
SI (Int# -> Int
I# Int#
x1)]
 | Bool
otherwise = -- Common case: x1 >= x2 >= y
               let !delta :: Int#
delta = Int#
x2 Int# -> Int# -> Int#
-# Int#
x1 -- <= 0
                   !y' :: Int#
y' = Int#
y Int# -> Int# -> Int#
-# Int#
delta  -- y <= y' <= x1; hence y' is representable

                   -- Invariant: x >= y
                   -- Note that: z >= y' => z + delta won't underflow
                   -- so we are guaranteed not to underflow if/when we recurse
                   go_dn :: Int# -> [SatInt]
go_dn Int#
x | Int# -> Bool
isTrue# (Int#
x Int# -> Int# -> Int#
<# Int#
y') = [Int -> SatInt
SI (Int# -> Int
I# Int#
x)]
                           | Bool
otherwise = Int -> SatInt
SI (Int# -> Int
I# Int#
x) SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: Int# -> [SatInt]
go_dn (Int#
x Int# -> Int# -> Int#
+# Int#
delta)
   in Int -> SatInt
SI (Int# -> Int
I# Int#
x1) SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: Int# -> [SatInt]
go_dn Int#
x2


-- Requires x2 <= x1
{-# INLINE [0] efdtIntDnFB #-}
efdtIntDnFB :: (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
efdtIntDnFB :: (SatInt -> r -> r) -> r -> Int# -> Int# -> Int# -> r
efdtIntDnFB SatInt -> r -> r
c r
n Int#
x1 Int#
x2 Int#
y    -- Be careful about underflow!
 | Int# -> Bool
isTrue# (Int#
y Int# -> Int# -> Int#
># Int#
x2) = if Int# -> Bool
isTrue# (Int#
y Int# -> Int# -> Int#
># Int#
x1) then r
n else Int -> SatInt
SI (Int# -> Int
I# Int#
x1) SatInt -> r -> r
`c` r
n
 | Bool
otherwise = -- Common case: x1 >= x2 >= y
               let !delta :: Int#
delta = Int#
x2 Int# -> Int# -> Int#
-# Int#
x1 -- <= 0
                   !y' :: Int#
y' = Int#
y Int# -> Int# -> Int#
-# Int#
delta  -- y <= y' <= x1; hence y' is representable

                   -- Invariant: x >= y
                   -- Note that: z >= y' => z + delta won't underflow
                   -- so we are guaranteed not to underflow if/when we recurse
                   go_dn :: Int# -> r
go_dn Int#
x | Int# -> Bool
isTrue# (Int#
x Int# -> Int# -> Int#
<# Int#
y') = Int -> SatInt
SI (Int# -> Int
I# Int#
x) SatInt -> r -> r
`c` r
n
                           | Bool
otherwise = Int -> SatInt
SI (Int# -> Int
I# Int#
x) SatInt -> r -> r
`c` Int# -> r
go_dn (Int#
x Int# -> Int# -> Int#
+# Int#
delta)
               in Int -> SatInt
SI (Int# -> Int
I# Int#
x1) SatInt -> r -> r
`c` Int# -> r
go_dn Int#
x2

-- The following code is copied/adapted from GHC.Real.

instance Real SatInt where
  toRational :: SatInt -> Rational
toRational (SI Int
x) = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

instance Integral SatInt where
    toInteger :: SatInt -> Integer
toInteger (SI (I# Int#
i)) = Int# -> Integer
smallInteger Int#
i

    SI Int
a quot :: SatInt -> SatInt -> SatInt
`quot` SI Int
b
     | Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0                     = SatInt
forall a. a
divZeroError
     -- a/-1 = -a, -minBound = maxBound
     -- We can't just fall though since `quotInt` would overflow instead
     | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (-Int
1) = SatInt
forall a. Bounded a => a
maxBound
     | Bool
otherwise                  = Int -> SatInt
SI (Int
a Int -> Int -> Int
`quotInt` Int
b)

    SI Int
a rem :: SatInt -> SatInt -> SatInt
`rem` SI Int
b
     | Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0                     = SatInt
forall a. a
divZeroError
     -- a/-1 = -a, with no remainder
     -- We can't just fall though since `remInt` would overflow instead
     | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (-Int
1) = SatInt
0
     | Bool
otherwise                  = Int -> SatInt
SI (Int
a Int -> Int -> Int
`remInt` Int
b)

    SI Int
a div :: SatInt -> SatInt -> SatInt
`div` SI Int
b
     | Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0                     = SatInt
forall a. a
divZeroError
     -- a/-1 = -a, -minBound = maxBound
     -- We can't just fall though since `divInt` would overflow instead
     | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (-Int
1) = SatInt
forall a. Bounded a => a
maxBound
     | Bool
otherwise                  = Int -> SatInt
SI (Int
a Int -> Int -> Int
`divInt` Int
b)

    SI Int
a mod :: SatInt -> SatInt -> SatInt
`mod` SI Int
b
     | Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0                     = SatInt
forall a. a
divZeroError
     -- a/-1 = -a, with no remainder
     -- We can't just fall though since `modInt` would overflow instead
     | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (-Int
1) = SatInt
0
     | Bool
otherwise                  = Int -> SatInt
SI (Int
a Int -> Int -> Int
`modInt` Int
b)

    SI Int
a quotRem :: SatInt -> SatInt -> (SatInt, SatInt)
`quotRem` SI Int
b
     | Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0                     = (SatInt, SatInt)
forall a. a
divZeroError
     -- See cases for `quot` and `rem`
     | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (-Int
1) = (SatInt
forall a. Bounded a => a
maxBound, SatInt
0)
     | Bool
otherwise                  =  Int
a Int -> Int -> (SatInt, SatInt)
`quotRemSI` Int
b

    SI Int
a divMod :: SatInt -> SatInt -> (SatInt, SatInt)
`divMod` SI Int
b
     | Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0                     = (SatInt, SatInt)
forall a. a
divZeroError
     -- See cases for `div` and `mod`
     | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (-Int
1) = (SatInt
forall a. Bounded a => a
maxBound, SatInt
0)
     | Bool
otherwise                  =  Int
a Int -> Int -> (SatInt, SatInt)
`divModSI` Int
b

quotRemSI :: Int -> Int -> (SatInt, SatInt)
quotRemSI :: Int -> Int -> (SatInt, SatInt)
quotRemSI a :: Int
a@(I# Int#
_) b :: Int
b@(I# Int#
_) = (Int -> SatInt
SI (Int
a Int -> Int -> Int
`quotInt` Int
b), Int -> SatInt
SI (Int
a Int -> Int -> Int
`remInt` Int
b))

divModSI ::  Int -> Int -> (SatInt, SatInt)
divModSI :: Int -> Int -> (SatInt, SatInt)
divModSI x :: Int
x@(I# Int#
_) y :: Int
y@(I# Int#
_) = (Int -> SatInt
SI (Int
x Int -> Int -> Int
`divInt` Int
y), Int -> SatInt
SI (Int
x Int -> Int -> Int
`modInt` Int
y))

{-
'addIntC#', 'subIntC#', and 'mulIntMayOflow#' have tricky returns:
all of them return non-zero (*not* necessarily 1) in the case of an overflow,
so we can't use 'isTrue#'; and the first two return a truncated value in
case of overflow, but this is *not* the same as the saturating result,
but rather a bitwise truncation that is typically not what we want.

So we have to case on the result, and then do some logic to work out what
kind of overflow we're facing, and pick the correct result accordingly.
-}

plusSI :: SatInt -> SatInt -> SatInt
plusSI :: SatInt -> SatInt -> SatInt
plusSI (SI (I# Int#
x#)) (SI (I# Int#
y#)) =
  case Int# -> Int# -> (# Int#, Int# #)
addIntC# Int#
x# Int#
y#  of
    (# Int#
r#, Int#
0# #) -> Int -> SatInt
SI (Int# -> Int
I# Int#
r#)
    -- Overflow
    (# Int#, Int# #)
_ ->
      if      Int# -> Bool
isTrue# ((Int#
x# Int# -> Int# -> Int#
># Int#
0#) Int# -> Int# -> Int#
`andI#` (Int#
y# Int# -> Int# -> Int#
># Int#
0#)) then SatInt
forall a. Bounded a => a
maxBound
      else if Int# -> Bool
isTrue# ((Int#
x# Int# -> Int# -> Int#
<# Int#
0#) Int# -> Int# -> Int#
`andI#` (Int#
y# Int# -> Int# -> Int#
<# Int#
0#)) then SatInt
forall a. Bounded a => a
minBound
      -- x and y have opposite signs, and yet we've overflowed, should
      -- be impossible
      else SatInt
forall a. a
overflowError

minusSI :: SatInt -> SatInt -> SatInt
minusSI :: SatInt -> SatInt -> SatInt
minusSI (SI (I# Int#
x#)) (SI (I# Int#
y#)) =
  case Int# -> Int# -> (# Int#, Int# #)
subIntC# Int#
x# Int#
y# of
    (# Int#
r#, Int#
0# #) -> Int -> SatInt
SI (Int# -> Int
I# Int#
r#)
    -- Overflow
    (# Int#, Int# #)
_ ->
      if      Int# -> Bool
isTrue# ((Int#
x# Int# -> Int# -> Int#
>=# Int#
0#) Int# -> Int# -> Int#
`andI#` (Int#
y# Int# -> Int# -> Int#
<# Int#
0#)) then SatInt
forall a. Bounded a => a
maxBound
      else if Int# -> Bool
isTrue# ((Int#
x# Int# -> Int# -> Int#
<=# Int#
0#) Int# -> Int# -> Int#
`andI#` (Int#
y# Int# -> Int# -> Int#
># Int#
0#)) then SatInt
forall a. Bounded a => a
minBound
      -- x and y have the same sign, and yet we've overflowed, should
      -- be impossible
      else SatInt
forall a. a
overflowError

timesSI :: SatInt -> SatInt -> SatInt
timesSI :: SatInt -> SatInt -> SatInt
timesSI (SI (I# Int#
x#)) (SI (I# Int#
y#)) =
  case Int# -> Int# -> Int#
mulIntMayOflo# Int#
x# Int#
y# of
      Int#
0# -> Int -> SatInt
SI (Int# -> Int
I# (Int#
x# Int# -> Int# -> Int#
*# Int#
y#))
      -- Overflow
      Int#
_ ->
          if      Int# -> Bool
isTrue# ((Int#
x# Int# -> Int# -> Int#
># Int#
0#) Int# -> Int# -> Int#
`andI#` (Int#
y# Int# -> Int# -> Int#
># Int#
0#)) then SatInt
forall a. Bounded a => a
maxBound
          else if Int# -> Bool
isTrue# ((Int#
x# Int# -> Int# -> Int#
># Int#
0#) Int# -> Int# -> Int#
`andI#` (Int#
y# Int# -> Int# -> Int#
<# Int#
0#)) then SatInt
forall a. Bounded a => a
minBound
          else if Int# -> Bool
isTrue# ((Int#
x# Int# -> Int# -> Int#
<# Int#
0#) Int# -> Int# -> Int#
`andI#` (Int#
y# Int# -> Int# -> Int#
># Int#
0#)) then SatInt
forall a. Bounded a => a
minBound
          else if Int# -> Bool
isTrue# ((Int#
x# Int# -> Int# -> Int#
<# Int#
0#) Int# -> Int# -> Int#
`andI#` (Int#
y# Int# -> Int# -> Int#
<# Int#
0#)) then SatInt
forall a. Bounded a => a
maxBound
          -- Logically unreachable unless x or y is 0, in which case
          -- it should be impossible to overflow
          else SatInt
forall a. a
overflowError

{-# RULES
"fromIntegral/Int->SatInt"     fromIntegral = SI
"fromIntegral/SatInt->SatInt" fromIntegral = id :: SatInt -> SatInt
  #-}

-- Specialized versions of several functions. They're specialized for
-- Int in the GHC base libraries. We try to get the same effect by
-- including specialized code and adding a rewrite rule.

sumSI :: [SatInt] -> SatInt
sumSI :: [SatInt] -> SatInt
sumSI     [SatInt]
l       = [SatInt] -> SatInt -> SatInt
forall t. Num t => [t] -> t -> t
sum' [SatInt]
l SatInt
0
  where
    sum' :: [t] -> t -> t
sum' []     t
a = t
a
    sum' (t
x:[t]
xs) t
a = [t] -> t -> t
sum' [t]
xs (t
a t -> t -> t
forall a. Num a => a -> a -> a
+ t
x)

productSI :: [SatInt] -> SatInt
productSI :: [SatInt] -> SatInt
productSI [SatInt]
l       = [SatInt] -> SatInt -> SatInt
forall t. Num t => [t] -> t -> t
prod [SatInt]
l SatInt
1
  where
    prod :: [t] -> t -> t
prod []     t
a = t
a
    prod (t
x:[t]
xs) t
a = [t] -> t -> t
prod [t]
xs (t
at -> t -> t
forall a. Num a => a -> a -> a
*t
x)

{-# RULES
  "sum/SatInt"          sum = sumSI;
  "product/SatInt"      product = productSI
  #-}