-- Copyright (c) 2018-2019  Herbert Valerio Riedel <hvr@gnu.org>
--
--  This file is free software: you may copy, redistribute and/or modify it
--  under the terms of the GNU General Public License as published by the
--  Free Software Foundation, either version 2 of the License, or (at your
--  option) any later version.
--
--  This file is distributed in the hope that it will be useful, but
--  WITHOUT ANY WARRANTY; without even the implied warranty of
--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
--  General Public License for more details.
--
--  You should have received a copy of the GNU General Public License
--  along with this program (see `LICENSE`).  If not, see
--  <https://www.gnu.org/licenses/old-licenses/gpl-2.0.html>.

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Int.Subtypes
    ( UInt(..), toUInt, fromUInt, uintFromInteger
    , SInt(..), toSInt, fromSInt, sintFromInteger

    , UIntBounds
    , SIntBounds

      -- helpers
    , IsBelowMaxBound
    , IsAboveMinBoundNeg
    ) where

import           Common

import           Data.Coerce (coerce)

-- | Unsigned integer sub-type
newtype UInt (lb :: Nat) (ub :: Nat) t = UInt t
  deriving (UInt lb ub t -> UInt lb ub t -> Bool
(UInt lb ub t -> UInt lb ub t -> Bool)
-> (UInt lb ub t -> UInt lb ub t -> Bool) -> Eq (UInt lb ub t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (lb :: Nat) (ub :: Nat) t.
Eq t =>
UInt lb ub t -> UInt lb ub t -> Bool
/= :: UInt lb ub t -> UInt lb ub t -> Bool
$c/= :: forall (lb :: Nat) (ub :: Nat) t.
Eq t =>
UInt lb ub t -> UInt lb ub t -> Bool
== :: UInt lb ub t -> UInt lb ub t -> Bool
$c== :: forall (lb :: Nat) (ub :: Nat) t.
Eq t =>
UInt lb ub t -> UInt lb ub t -> Bool
Eq,Eq (UInt lb ub t)
Eq (UInt lb ub t) =>
(UInt lb ub t -> UInt lb ub t -> Ordering)
-> (UInt lb ub t -> UInt lb ub t -> Bool)
-> (UInt lb ub t -> UInt lb ub t -> Bool)
-> (UInt lb ub t -> UInt lb ub t -> Bool)
-> (UInt lb ub t -> UInt lb ub t -> Bool)
-> (UInt lb ub t -> UInt lb ub t -> UInt lb ub t)
-> (UInt lb ub t -> UInt lb ub t -> UInt lb ub t)
-> Ord (UInt lb ub t)
UInt lb ub t -> UInt lb ub t -> Bool
UInt lb ub t -> UInt lb ub t -> Ordering
UInt lb ub t -> UInt lb ub t -> UInt lb ub t
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (lb :: Nat) (ub :: Nat) t. Ord t => Eq (UInt lb ub t)
forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> Bool
forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> Ordering
forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> UInt lb ub t
min :: UInt lb ub t -> UInt lb ub t -> UInt lb ub t
$cmin :: forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> UInt lb ub t
max :: UInt lb ub t -> UInt lb ub t -> UInt lb ub t
$cmax :: forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> UInt lb ub t
>= :: UInt lb ub t -> UInt lb ub t -> Bool
$c>= :: forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> Bool
> :: UInt lb ub t -> UInt lb ub t -> Bool
$c> :: forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> Bool
<= :: UInt lb ub t -> UInt lb ub t -> Bool
$c<= :: forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> Bool
< :: UInt lb ub t -> UInt lb ub t -> Bool
$c< :: forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> Bool
compare :: UInt lb ub t -> UInt lb ub t -> Ordering
$ccompare :: forall (lb :: Nat) (ub :: Nat) t.
Ord t =>
UInt lb ub t -> UInt lb ub t -> Ordering
$cp1Ord :: forall (lb :: Nat) (ub :: Nat) t. Ord t => Eq (UInt lb ub t)
Ord)

-- | Signed integer sub-type
--
-- __NOTE__: Due to lack of negative type-level integer literals the
-- lower bound is negated, i.e. it expresses a negative magnitude
newtype SInt (nlb :: Nat) (ub :: Nat) t = SInt t
  deriving (SInt nlb ub t -> SInt nlb ub t -> Bool
(SInt nlb ub t -> SInt nlb ub t -> Bool)
-> (SInt nlb ub t -> SInt nlb ub t -> Bool) -> Eq (SInt nlb ub t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (nlb :: Nat) (ub :: Nat) t.
Eq t =>
SInt nlb ub t -> SInt nlb ub t -> Bool
/= :: SInt nlb ub t -> SInt nlb ub t -> Bool
$c/= :: forall (nlb :: Nat) (ub :: Nat) t.
Eq t =>
SInt nlb ub t -> SInt nlb ub t -> Bool
== :: SInt nlb ub t -> SInt nlb ub t -> Bool
$c== :: forall (nlb :: Nat) (ub :: Nat) t.
Eq t =>
SInt nlb ub t -> SInt nlb ub t -> Bool
Eq,Eq (SInt nlb ub t)
Eq (SInt nlb ub t) =>
(SInt nlb ub t -> SInt nlb ub t -> Ordering)
-> (SInt nlb ub t -> SInt nlb ub t -> Bool)
-> (SInt nlb ub t -> SInt nlb ub t -> Bool)
-> (SInt nlb ub t -> SInt nlb ub t -> Bool)
-> (SInt nlb ub t -> SInt nlb ub t -> Bool)
-> (SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t)
-> (SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t)
-> Ord (SInt nlb ub t)
SInt nlb ub t -> SInt nlb ub t -> Bool
SInt nlb ub t -> SInt nlb ub t -> Ordering
SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (nlb :: Nat) (ub :: Nat) t. Ord t => Eq (SInt nlb ub t)
forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> Bool
forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> Ordering
forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
min :: SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
$cmin :: forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
max :: SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
$cmax :: forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
>= :: SInt nlb ub t -> SInt nlb ub t -> Bool
$c>= :: forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> Bool
> :: SInt nlb ub t -> SInt nlb ub t -> Bool
$c> :: forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> Bool
<= :: SInt nlb ub t -> SInt nlb ub t -> Bool
$c<= :: forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> Bool
< :: SInt nlb ub t -> SInt nlb ub t -> Bool
$c< :: forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> Bool
compare :: SInt nlb ub t -> SInt nlb ub t -> Ordering
$ccompare :: forall (nlb :: Nat) (ub :: Nat) t.
Ord t =>
SInt nlb ub t -> SInt nlb ub t -> Ordering
$cp1Ord :: forall (nlb :: Nat) (ub :: Nat) t. Ord t => Eq (SInt nlb ub t)
Ord)

-- | Coerce integer sub-type into its base-type
fromUInt :: UInt lb ub t -> t
fromUInt :: UInt lb ub t -> t
fromUInt (UInt i :: t
i) = t
i

-- | Coerce integer sub-type into its base-type
fromSInt :: SInt nlb ub t -> t
fromSInt :: SInt nlb ub t -> t
fromSInt (SInt i :: t
i) = t
i

instance forall lb ub t . NFData t => NFData (UInt lb ub t) where
  rnf :: UInt lb ub t -> ()
rnf = (t -> ()) -> UInt lb ub t -> ()
forall a b. Coercible a b => a -> b
coerce (t -> ()
forall a. NFData a => a -> ()
rnf :: t -> ())

instance forall lb ub t . NFData t => NFData (SInt lb ub t) where
  rnf :: SInt lb ub t -> ()
rnf = (t -> ()) -> SInt lb ub t -> ()
forall a b. Coercible a b => a -> b
coerce (t -> ()
forall a. NFData a => a -> ()
rnf :: t -> ())

instance forall lb ub t . Show t => Show (UInt lb ub t) where
  show :: UInt lb ub t -> String
show      = (t -> String) -> UInt lb ub t -> String
forall a b. Coercible a b => a -> b
coerce (t -> String
forall a. Show a => a -> String
show :: t -> String)
  showsPrec :: Int -> UInt lb ub t -> ShowS
showsPrec = (Int -> t -> ShowS) -> Int -> UInt lb ub t -> ShowS
forall a b. Coercible a b => a -> b
coerce (Int -> t -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec :: Int -> t -> ShowS)

instance forall nlb ub t . Show t => Show (SInt nlb ub t) where
  show :: SInt nlb ub t -> String
show      = (t -> String) -> SInt nlb ub t -> String
forall a b. Coercible a b => a -> b
coerce (t -> String
forall a. Show a => a -> String
show :: t -> String)
  showsPrec :: Int -> SInt nlb ub t -> ShowS
showsPrec = (Int -> t -> ShowS) -> Int -> SInt nlb ub t -> ShowS
forall a b. Coercible a b => a -> b
coerce (Int -> t -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec :: Int -> t -> ShowS)

-- | Constraint encoding type-level invariants for 'UInt'
type UIntBounds lb ub t = ( KnownNat lb, KnownNat ub, lb <= ub
                          , IsBelowMaxBound ub (IntBaseType t) ~ 'True)

-- | Constraint encoding type-level invariants for 'SInt'
type SIntBounds nlb ub t = ( KnownNat nlb, KnownNat ub
                          , IsAboveMinBoundNeg nlb (IntBaseType t) ~ 'True
                          , IsBelowMaxBound ub (IntBaseType t) ~ 'True)

type family IsBelowMaxBound (n :: Nat) (t :: IntBaseTypeK) :: Bool where
  IsBelowMaxBound n ('FixedWordTag b) = n+1 <=? (2^b)
  IsBelowMaxBound n ('FixedIntTag b)  = n+1 <=? (2^(b-1))
  IsBelowMaxBound n 'BigIntTag        = 'True
  IsBelowMaxBound n 'BigWordTag       = 'True

type family IsAboveMinBoundNeg (n :: Nat) (t :: IntBaseTypeK) :: Bool where
  IsAboveMinBoundNeg n ('FixedWordTag b) = n <=? 0
  IsAboveMinBoundNeg n ('FixedIntTag b)  = n <=? (2^(b-1))
  IsAboveMinBoundNeg n 'BigIntTag        = 'True
  IsAboveMinBoundNeg n 'BigWordTag       = n <=? 0

instance forall lb ub t . (UIntBounds lb ub t, Num t) => Bounded (UInt lb ub t) where
  minBound :: UInt lb ub t
minBound = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t. t -> UInt lb ub t
UInt (t -> UInt lb ub t) -> t -> UInt lb ub t
forall a b. (a -> b) -> a -> b
$ Integer -> t
forall a. Num a => Integer -> a
fromInteger (Proxy lb -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy lb
forall k (t :: k). Proxy t
Proxy :: Proxy lb))
  maxBound :: UInt lb ub t
maxBound = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t. t -> UInt lb ub t
UInt (t -> UInt lb ub t) -> t -> UInt lb ub t
forall a b. (a -> b) -> a -> b
$ Integer -> t
forall a. Num a => Integer -> a
fromInteger (Proxy ub -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy ub
forall k (t :: k). Proxy t
Proxy :: Proxy ub))

instance forall nlb ub t . (SIntBounds nlb ub t, Num t) => Bounded (SInt nlb ub t) where
  minBound :: SInt nlb ub t
minBound = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t. t -> SInt nlb ub t
SInt (t -> SInt nlb ub t) -> t -> SInt nlb ub t
forall a b. (a -> b) -> a -> b
$ Integer -> t
forall a. Num a => Integer -> a
fromInteger (-Proxy nlb -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy nlb
forall k (t :: k). Proxy t
Proxy :: Proxy nlb))
  maxBound :: SInt nlb ub t
maxBound = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t. t -> SInt nlb ub t
SInt (t -> SInt nlb ub t) -> t -> SInt nlb ub t
forall a b. (a -> b) -> a -> b
$ Integer -> t
forall a. Num a => Integer -> a
fromInteger (Proxy ub -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy ub
forall k (t :: k). Proxy t
Proxy :: Proxy ub))

----------------------------------------------------------------------------

uintFromInteger :: forall lb ub t . (UIntBounds lb ub t, Num t) => Integer -> Either ArithException (UInt lb ub t)
uintFromInteger :: Integer -> Either ArithException (UInt lb ub t)
uintFromInteger i :: Integer
i
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Proxy lb -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy lb
forall k (t :: k). Proxy t
Proxy :: Proxy lb) = ArithException -> Either ArithException (UInt lb ub t)
forall a b. a -> Either a b
Left ArithException
Underflow
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Proxy ub -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy ub
forall k (t :: k). Proxy t
Proxy :: Proxy ub) = ArithException -> Either ArithException (UInt lb ub t)
forall a b. a -> Either a b
Left ArithException
Overflow
  | Bool
otherwise                      = UInt lb ub t -> Either ArithException (UInt lb ub t)
forall a b. b -> Either a b
Right UInt lb ub t
i'
  where
    i' :: UInt lb ub t
i' = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t. t -> UInt lb ub t
UInt (Integer -> t
forall a. Num a => Integer -> a
fromInteger Integer
i) :: UInt lb ub t

-- | Try to coerce a base-type into its 'UInt' sub-type
--
-- If out of range, @'Left' 'Underflow'@ or @'Right' 'Overflow'@ will be returned.
toUInt :: forall lb ub t . (UIntBounds lb ub t, Num t, Ord t) => t -> Either ArithException (UInt lb ub t)
toUInt :: t -> Either ArithException (UInt lb ub t)
toUInt i :: t
i
  | UInt lb ub t
i' UInt lb ub t -> UInt lb ub t -> Bool
forall a. Ord a => a -> a -> Bool
< UInt lb ub t
forall a. Bounded a => a
minBound = ArithException -> Either ArithException (UInt lb ub t)
forall a b. a -> Either a b
Left ArithException
Underflow
  | UInt lb ub t
i' UInt lb ub t -> UInt lb ub t -> Bool
forall a. Ord a => a -> a -> Bool
> UInt lb ub t
forall a. Bounded a => a
maxBound = ArithException -> Either ArithException (UInt lb ub t)
forall a b. a -> Either a b
Left ArithException
Overflow
  | Bool
otherwise     = UInt lb ub t -> Either ArithException (UInt lb ub t)
forall a b. b -> Either a b
Right UInt lb ub t
i'
  where
    i' :: UInt lb ub t
i' = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t. t -> UInt lb ub t
UInt t
i :: UInt lb ub t

toUInt' :: forall lb ub t . (UIntBounds lb ub t, Num t, Ord t) => t -> UInt lb ub t
toUInt' :: t -> UInt lb ub t
toUInt' = (ArithException -> UInt lb ub t)
-> (UInt lb ub t -> UInt lb ub t)
-> Either ArithException (UInt lb ub t)
-> UInt lb ub t
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ArithException -> UInt lb ub t
forall a e. Exception e => e -> a
throw UInt lb ub t -> UInt lb ub t
forall a. a -> a
id (Either ArithException (UInt lb ub t) -> UInt lb ub t)
-> (t -> Either ArithException (UInt lb ub t)) -> t -> UInt lb ub t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Either ArithException (UInt lb ub t)
forall (lb :: Nat) (ub :: Nat) t.
(UIntBounds lb ub t, Num t, Ord t) =>
t -> Either ArithException (UInt lb ub t)
toUInt

instance forall lb ub t . (UIntBounds lb ub t, Integral t, Ord t) => Num (UInt lb ub t) where
  fromInteger :: Integer -> UInt lb ub t
fromInteger     = (ArithException -> UInt lb ub t)
-> (UInt lb ub t -> UInt lb ub t)
-> Either ArithException (UInt lb ub t)
-> UInt lb ub t
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ArithException -> UInt lb ub t
forall a e. Exception e => e -> a
throw UInt lb ub t -> UInt lb ub t
forall a. a -> a
id (Either ArithException (UInt lb ub t) -> UInt lb ub t)
-> (Integer -> Either ArithException (UInt lb ub t))
-> Integer
-> UInt lb ub t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Either ArithException (UInt lb ub t)
forall (lb :: Nat) (ub :: Nat) t.
(UIntBounds lb ub t, Num t) =>
Integer -> Either ArithException (UInt lb ub t)
uintFromInteger

  UInt 0 * :: UInt lb ub t -> UInt lb ub t -> UInt lb ub t
* _      = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t. t -> UInt lb ub t
UInt 0
  UInt 1 * y :: UInt lb ub t
y      = UInt lb ub t
y
  _      * UInt 0 = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t. t -> UInt lb ub t
UInt 0
  x :: UInt lb ub t
x      * UInt 1 = UInt lb ub t
x
  UInt x :: t
x * UInt y :: t
y = Integer -> UInt lb ub t
forall a. Num a => Integer -> a
fromInteger (t -> Integer
forall a. Integral a => a -> Integer
toInteger t
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* t -> Integer
forall a. Integral a => a -> Integer
toInteger t
y)

  UInt 0 + :: UInt lb ub t -> UInt lb ub t -> UInt lb ub t
+ y :: UInt lb ub t
y      = UInt lb ub t
y
  x :: UInt lb ub t
x      + UInt 0 = UInt lb ub t
x
  UInt x :: t
x + UInt y :: t
y = Integer -> UInt lb ub t
forall a. Num a => Integer -> a
fromInteger (t -> Integer
forall a. Integral a => a -> Integer
toInteger t
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ t -> Integer
forall a. Integral a => a -> Integer
toInteger t
y)

  x :: UInt lb ub t
x      - :: UInt lb ub t -> UInt lb ub t -> UInt lb ub t
- UInt 0 = UInt lb ub t
x
  UInt 0 - y :: UInt lb ub t
y      = UInt lb ub t -> UInt lb ub t
forall a. Num a => a -> a
negate UInt lb ub t
y
  UInt x :: t
x - UInt y :: t
y = Integer -> UInt lb ub t
forall a. Num a => Integer -> a
fromInteger (t -> Integer
forall a. Integral a => a -> Integer
toInteger t
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- t -> Integer
forall a. Integral a => a -> Integer
toInteger t
y)

  negate :: UInt lb ub t -> UInt lb ub t
negate (UInt 0) = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t. t -> UInt lb ub t
UInt 0
  negate (UInt _) = ArithException -> UInt lb ub t
forall a e. Exception e => e -> a
throw ArithException
Underflow

  abs :: UInt lb ub t -> UInt lb ub t
abs             = UInt lb ub t -> UInt lb ub t
forall a. a -> a
id

  signum :: UInt lb ub t -> UInt lb ub t
signum (UInt 0) = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t. t -> UInt lb ub t
UInt 0
  signum (UInt _) = t -> UInt lb ub t
forall (lb :: Nat) (ub :: Nat) t.
(UIntBounds lb ub t, Num t, Ord t) =>
t -> UInt lb ub t
toUInt' 1

----------------------------------------------------------------------------

sintFromInteger :: forall nlb ub t . (SIntBounds nlb ub t, Num t) => Integer -> Either ArithException (SInt nlb ub t)
sintFromInteger :: Integer -> Either ArithException (SInt nlb ub t)
sintFromInteger i :: Integer
i
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< -Proxy nlb -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy nlb
forall k (t :: k). Proxy t
Proxy :: Proxy nlb) = ArithException -> Either ArithException (SInt nlb ub t)
forall a b. a -> Either a b
Left ArithException
Underflow
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>  Proxy ub -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy ub
forall k (t :: k). Proxy t
Proxy :: Proxy ub)  = ArithException -> Either ArithException (SInt nlb ub t)
forall a b. a -> Either a b
Left ArithException
Overflow
  | Bool
otherwise                        = SInt nlb ub t -> Either ArithException (SInt nlb ub t)
forall a b. b -> Either a b
Right SInt nlb ub t
i'
  where
    i' :: SInt nlb ub t
i' = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t. t -> SInt nlb ub t
SInt (Integer -> t
forall a. Num a => Integer -> a
fromInteger Integer
i) :: SInt nlb ub t

-- | Try to coerce a base-type into its 'SInt' sub-type
--
-- If out of range, @'Left' 'Underflow'@ or @'Right' 'Overflow'@ will be returned.
toSInt :: forall nlb ub t . (SIntBounds nlb ub t, Num t, Ord t) => t -> Either ArithException (SInt nlb ub t)
toSInt :: t -> Either ArithException (SInt nlb ub t)
toSInt i :: t
i
  | SInt nlb ub t
i' SInt nlb ub t -> SInt nlb ub t -> Bool
forall a. Ord a => a -> a -> Bool
< SInt nlb ub t
forall a. Bounded a => a
minBound = ArithException -> Either ArithException (SInt nlb ub t)
forall a b. a -> Either a b
Left ArithException
Underflow
  | SInt nlb ub t
i' SInt nlb ub t -> SInt nlb ub t -> Bool
forall a. Ord a => a -> a -> Bool
> SInt nlb ub t
forall a. Bounded a => a
maxBound = ArithException -> Either ArithException (SInt nlb ub t)
forall a b. a -> Either a b
Left ArithException
Overflow
  | Bool
otherwise     = SInt nlb ub t -> Either ArithException (SInt nlb ub t)
forall a b. b -> Either a b
Right SInt nlb ub t
i'
  where
    i' :: SInt nlb ub t
i' = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t. t -> SInt nlb ub t
SInt t
i :: SInt nlb ub t

toSInt' :: forall nlb ub t . (SIntBounds nlb ub t, Num t, Ord t) => t -> SInt nlb ub t
toSInt' :: t -> SInt nlb ub t
toSInt' = (ArithException -> SInt nlb ub t)
-> (SInt nlb ub t -> SInt nlb ub t)
-> Either ArithException (SInt nlb ub t)
-> SInt nlb ub t
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ArithException -> SInt nlb ub t
forall a e. Exception e => e -> a
throw SInt nlb ub t -> SInt nlb ub t
forall a. a -> a
id (Either ArithException (SInt nlb ub t) -> SInt nlb ub t)
-> (t -> Either ArithException (SInt nlb ub t))
-> t
-> SInt nlb ub t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Either ArithException (SInt nlb ub t)
forall (nlb :: Nat) (ub :: Nat) t.
(SIntBounds nlb ub t, Num t, Ord t) =>
t -> Either ArithException (SInt nlb ub t)
toSInt

instance forall nlb ub t . (SIntBounds nlb ub t, Integral t, Ord t) => Num (SInt nlb ub t) where
  fromInteger :: Integer -> SInt nlb ub t
fromInteger     = (ArithException -> SInt nlb ub t)
-> (SInt nlb ub t -> SInt nlb ub t)
-> Either ArithException (SInt nlb ub t)
-> SInt nlb ub t
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ArithException -> SInt nlb ub t
forall a e. Exception e => e -> a
throw SInt nlb ub t -> SInt nlb ub t
forall a. a -> a
id (Either ArithException (SInt nlb ub t) -> SInt nlb ub t)
-> (Integer -> Either ArithException (SInt nlb ub t))
-> Integer
-> SInt nlb ub t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Either ArithException (SInt nlb ub t)
forall (nlb :: Nat) (ub :: Nat) t.
(SIntBounds nlb ub t, Num t) =>
Integer -> Either ArithException (SInt nlb ub t)
sintFromInteger

  SInt 0 * :: SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
* _      = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t. t -> SInt nlb ub t
SInt 0
  SInt 1 * y :: SInt nlb ub t
y      = SInt nlb ub t
y
  _      * SInt 0 = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t. t -> SInt nlb ub t
SInt 0
  x :: SInt nlb ub t
x      * SInt 1 = SInt nlb ub t
x
  SInt x :: t
x * SInt y :: t
y = Integer -> SInt nlb ub t
forall a. Num a => Integer -> a
fromInteger (t -> Integer
forall a. Integral a => a -> Integer
toInteger t
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* t -> Integer
forall a. Integral a => a -> Integer
toInteger t
y)

  SInt 0 + :: SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
+ y :: SInt nlb ub t
y      = SInt nlb ub t
y
  x :: SInt nlb ub t
x      + SInt 0 = SInt nlb ub t
x
  SInt x :: t
x + SInt y :: t
y = Integer -> SInt nlb ub t
forall a. Num a => Integer -> a
fromInteger (t -> Integer
forall a. Integral a => a -> Integer
toInteger t
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ t -> Integer
forall a. Integral a => a -> Integer
toInteger t
y)

  x :: SInt nlb ub t
x      - :: SInt nlb ub t -> SInt nlb ub t -> SInt nlb ub t
- SInt 0 = SInt nlb ub t
x
  SInt 0 - y :: SInt nlb ub t
y      = SInt nlb ub t -> SInt nlb ub t
forall a. Num a => a -> a
negate SInt nlb ub t
y
  SInt x :: t
x - SInt y :: t
y = Integer -> SInt nlb ub t
forall a. Num a => Integer -> a
fromInteger (t -> Integer
forall a. Integral a => a -> Integer
toInteger t
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- t -> Integer
forall a. Integral a => a -> Integer
toInteger t
y)

  negate :: SInt nlb ub t -> SInt nlb ub t
negate (SInt 0) = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t. t -> SInt nlb ub t
SInt 0
  negate (SInt x :: t
x) = Integer -> SInt nlb ub t
forall a. Num a => Integer -> a
fromInteger (t -> Integer
forall a. Integral a => a -> Integer
toInteger t
x)

  abs :: SInt nlb ub t -> SInt nlb ub t
abs    (SInt x :: t
x) = Integer -> SInt nlb ub t
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
abs (t -> Integer
forall a. Integral a => a -> Integer
toInteger t
x))

  signum :: SInt nlb ub t -> SInt nlb ub t
signum (SInt 0) = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t. t -> SInt nlb ub t
SInt 0
  signum (SInt x :: t
x) = t -> SInt nlb ub t
forall (nlb :: Nat) (ub :: Nat) t.
(SIntBounds nlb ub t, Num t, Ord t) =>
t -> SInt nlb ub t
toSInt' (t -> t
forall a. Num a => a -> a
signum t
x)