{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
module Data.TypedDigits.Internal (
module Data.TypedDigits.Internal
, KnownNat
)
where
import Data.Maybe
import Data.Proxy
import Data.Singletons.TypeLits (Nat, Sing(..), KnownNat )
import Data.Singletons (singByProxy, SingI(..), fromSing )
newtype Digit (base :: Nat) = Digit { getVal :: Int }
getBaseT :: forall a base . (KnownNat base) => a base -> Int
getBaseT _ = fromIntegral $ fromSing s
where
s :: Sing base
s = singByProxy (Proxy :: Proxy base)
digit :: forall base . (KnownNat base) => Int -> Maybe (Digit base)
digit x =
if x >= 0 && x < fromIntegral (getBaseT (Proxy :: Proxy base))
then Just $ Digit x
else Nothing
digit' :: KnownNat base => Int -> Digit base
digit' x = fromMaybe (error "bad value for base") (digit x)
digitSing :: KnownNat base => Digit base -> Sing base
digitSing Digit{} =
sing
getBase :: KnownNat base => Digit base -> Int
getBase d = fromIntegral $ fromSing (digitSing d)
deriving instance Eq (Digit base)
deriving instance Ord (Digit base)
instance (KnownNat base) => Show (Digit base) where
show d = show (getVal d) ++ " (base " ++ show (getBase d) ++ ")"
instance KnownNat base => Enum (Digit base) where
toEnum = digit'
fromEnum = getVal
instance (KnownNat base) => Bounded (Digit base) where
minBound = digit' 0
maxBound = digit' $ n - 1
where
n = getBaseT (Proxy :: Proxy base)
(<+>) :: KnownNat base => Digit base -> Digit base -> Digit base
a <+> b = digit' $ getVal a + getVal b
(<->) :: KnownNat base => Digit base -> Digit base -> Digit base
a <-> b = digit' $ getVal a - getVal b