module Numeric.TypeLits
( XNat (..), XN, N
, SomeIntNat (..), someIntNatVal, intNatVal, reifyDim
, KnownDim (..), KnownDims, dimVal#, Proxy#, proxy#
, Evidence (..), withEvidence, sumEvs, (+!+)
, inferPlusKnownDim, inferMinusKnownDim, inferMinusKnownDimM
, inferTimesKnownDim
, module GHC.TypeLits
, Proxy (..)
) where
import Data.Proxy (Proxy(..))
import GHC.Exts (Constraint, Proxy#, proxy#)
import GHC.TypeLits
import GHC.Types (Type)
import Unsafe.Coerce (unsafeCoerce)
data XNat = XN Nat | N Nat
type XN (n::Nat) = 'XN n
type N (n::Nat) = 'N n
data SomeIntNat = forall (n :: Nat) . KnownDim n => SomeIntNat (Proxy n)
class KnownDim (n :: Nat) where
dimVal' :: Int
type family KnownDims (ns :: [Nat]) :: Constraint where
KnownDims '[] = ()
KnownDims (x ': xs) = ( KnownDim x, KnownDims xs )
dimVal# :: forall (n :: Nat) . KnownDim n => Proxy# n -> Int
dimVal# _ = dimVal' @n
intNatVal :: forall n proxy . KnownDim n => proxy n -> Int
intNatVal _ = dimVal' @n
instance KnownNat n => KnownDim n where
dimVal' = fromInteger (natVal' (proxy# :: Proxy# n))
instance KnownDim 0 where { ; dimVal' = 0 }
instance KnownDim 1 where { ; dimVal' = 1 }
instance KnownDim 2 where { ; dimVal' = 2 }
instance KnownDim 3 where { ; dimVal' = 3 }
instance KnownDim 4 where { ; dimVal' = 4 }
instance KnownDim 5 where { ; dimVal' = 5 }
instance KnownDim 6 where { ; dimVal' = 6 }
instance KnownDim 7 where { ; dimVal' = 7 }
instance KnownDim 8 where { ; dimVal' = 8 }
instance KnownDim 9 where { ; dimVal' = 9 }
instance KnownDim 10 where { ; dimVal' = 10 }
instance KnownDim 11 where { ; dimVal' = 11 }
instance KnownDim 12 where { ; dimVal' = 12 }
instance KnownDim 13 where { ; dimVal' = 13 }
instance KnownDim 14 where { ; dimVal' = 14 }
instance KnownDim 15 where { ; dimVal' = 15 }
instance KnownDim 16 where { ; dimVal' = 16 }
instance KnownDim 17 where { ; dimVal' = 17 }
instance KnownDim 18 where { ; dimVal' = 18 }
instance KnownDim 19 where { ; dimVal' = 19 }
instance KnownDim 20 where { ; dimVal' = 20 }
someIntNatVal :: Int -> Maybe SomeIntNat
someIntNatVal x | 0 > x = Nothing
| otherwise = Just (reifyDim x f)
where
f :: forall (n :: Nat) . KnownDim n => Proxy# n -> SomeIntNat
f _ = SomeIntNat (Proxy @n)
reifyDim :: forall r . Int -> (forall (n :: Nat) . KnownDim n => Proxy# n -> r) -> r
reifyDim n k = unsafeCoerce (MagicDim k :: MagicDim r) n proxy#
newtype MagicDim r = MagicDim (forall (n :: Nat) . KnownDim n => Proxy# n -> r)
instance Eq SomeIntNat where
SomeIntNat x == SomeIntNat y = intNatVal x == intNatVal y
instance Ord SomeIntNat where
compare (SomeIntNat x) (SomeIntNat y) = compare (intNatVal x) (intNatVal y)
instance Show SomeIntNat where
showsPrec p (SomeIntNat x) = showsPrec p (intNatVal x)
instance Read SomeIntNat where
readsPrec p xs = do (a,ys) <- readsPrec p xs
case someIntNatVal a of
Nothing -> []
Just n -> [(n,ys)]
data Evidence :: Constraint -> Type where
Evidence :: a => Evidence a
sumEvs :: Evidence a -> Evidence b -> Evidence (a,b)
sumEvs Evidence Evidence = Evidence
infixl 4 +!+
(+!+) :: Evidence a -> Evidence b -> Evidence (a,b)
(+!+) = sumEvs
withEvidence :: Evidence a -> (a => r) -> r
withEvidence d r = case d of Evidence -> r
mkKDEv :: forall (m :: Nat) (n :: Nat) . KnownDim n => Proxy# n -> Evidence (KnownDim m)
mkKDEv _ = unsafeCoerce $ Evidence @(KnownDim n)
inferPlusKnownDim :: forall n m . (KnownDim n, KnownDim m) => Evidence (KnownDim (n + m))
inferPlusKnownDim = reifyDim (dimVal' @n + dimVal' @m) (mkKDEv @(n + m))
inferMinusKnownDim :: forall n m . (KnownDim n, KnownDim m, m <= n) => Evidence (KnownDim (n m))
inferMinusKnownDim = reifyDim (dimVal' @n dimVal' @m) (mkKDEv @(n m))
inferMinusKnownDimM :: forall n m . (KnownDim n, KnownDim m) => Maybe (Evidence (KnownDim (n m)))
inferMinusKnownDimM = if v >= 0 then Just $ reifyDim v (mkKDEv @(n m))
else Nothing
where
v = dimVal' @n dimVal' @m
inferTimesKnownDim :: forall n m . (KnownDim n, KnownDim m) => Evidence (KnownDim (n * m))
inferTimesKnownDim = reifyDim (dimVal' @n * dimVal' @m) (mkKDEv @(n * m))