{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.TypeNums.Ints
(
TInt(..)
, KnownInt
, intVal
, intVal'
) where
import GHC.Exts (Proxy#, proxy#)
import GHC.TypeLits (KnownNat, Nat, natVal')
newtype SInt (n :: k) =
SInt Integer
data TInt = Pos Nat
| Neg Nat
class KnownInt (n :: k) where
intSing :: SInt n
instance forall n. KnownNat n => KnownInt n where
intSing = SInt $! natVal' (proxy# @Nat @n)
instance forall n. KnownNat n => KnownInt ('Pos n) where
intSing = SInt $! natVal' (proxy# @Nat @n)
instance forall n. KnownNat n => KnownInt ('Neg n) where
intSing = SInt $! negate (natVal' (proxy# @Nat @n))
intVal ::
forall n proxy. KnownInt n
=> proxy n
-> Integer
intVal _ =
case intSing :: SInt n of
SInt x -> x
intVal' ::
forall n. KnownInt n
=> Proxy# n
-> Integer
intVal' _ =
case intSing :: SInt n of
SInt x -> x