{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Numeric.Dim
(
XNat (..), XN, N, XNatType (..)
, Dim (Dim, D, Dn, Dx), SomeDim
, KnownDim (..), KnownXNatType (..)
, dimVal, dimVal', someDimVal
, sameDim, sameDim'
, compareDim, compareDim'
, constrain, constrainBy, relax
, plusDim, minusDim, minusDimM, timesDim, powerDim
, Nat, CmpNat, type (+), type (-), type (*), type (^)
, MinDim, FixedDim, inferDimLE
, KnownDimKind (..), DimKind (..)
) where
import Data.Type.Bool
import Data.Type.Equality
import GHC.Base (Type)
import GHC.Exts (Constraint, Proxy#, proxy#, unsafeCoerce#)
import GHC.TypeLits
import Numeric.Type.Evidence
data XNat = XN Nat | N Nat
type XN (n::Nat) = 'XN n
type N (n::Nat) = 'N n
data XNatType :: XNat -> Type where
Nt :: XNatType ('N n)
XNt :: XNatType ('XN m)
type SomeDim = Dim ('XN 0)
newtype Dim (x :: k) = DimSing Word
#if __GLASGOW_HASKELL__ >= 802
{-# COMPLETE D #-}
{-# COMPLETE Dn, Dx #-}
{-# COMPLETE Dim #-}
#endif
pattern Dim :: forall (n :: k) . () => KnownDim n => Dim n
pattern Dim <- (dimEv -> E)
where
Dim = dim @_ @n
pattern D :: forall (n :: Nat) . () => KnownDim n => Dim n
pattern D <- (dimEv -> E)
where
D = dim @_ @n
pattern Dn :: forall (xn :: XNat) . KnownXNatType xn
=> forall (n :: Nat) . (KnownDim n, xn ~ 'N n) => Dim n -> Dim xn
pattern Dn k <- (dimXNEv (xNatType @xn) -> PatN k)
where
Dn k = unsafeCoerce# k
pattern Dx :: forall (xn :: XNat) . KnownXNatType xn
=> forall (n :: Nat) (m :: Nat)
. (KnownDim n, MinDim m n, xn ~ 'XN m) => Dim n -> Dim xn
pattern Dx k <- (dimXNEv (xNatType @xn) -> PatXN k)
where
Dx k = unsafeCoerce# k
class KnownDim (n :: k) where
dim :: Dim n
class KnownXNatType (n :: XNat) where
xNatType :: XNatType n
instance KnownXNatType ('N n) where
xNatType = Nt
{-# INLINE xNatType #-}
instance KnownXNatType ('XN n) where
xNatType = XNt
{-# INLINE xNatType #-}
dimVal :: Dim (x :: k) -> Word
dimVal = unsafeCoerce#
{-# INLINE dimVal #-}
dimVal' :: forall n . KnownDim n => Word
dimVal' = unsafeCoerce# (dim @_ @n)
{-# INLINE dimVal' #-}
type family MinDim (m :: Nat) (n :: Nat) :: Constraint where
MinDim m n =
If (CmpNat m n == 'GT)
(TypeError
('Text "Minimum Dim size constraint ("
':<>: 'ShowType m
':<>: 'Text " <= "
':<>: 'ShowType n
':<>: 'Text ") is not satisfied."
':$$: 'Text "Minimum Dim: " ':<>: 'ShowType m
':$$: 'Text " Actual Dim: " ':<>: 'ShowType n
) :: Constraint
)
(m <= n)
type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where
FixedDim ('N a) b = a ~ b
FixedDim ('XN m) b = MinDim m b
instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where
{-# INLINE dim #-}
dim = DimSing (fromInteger (natVal' (proxy# :: Proxy# n)))
instance {-# OVERLAPPING #-} KnownDim 0 where
{ {-# INLINE dim #-}; dim = DimSing 0 }
instance {-# OVERLAPPING #-} KnownDim 1 where
{ {-# INLINE dim #-}; dim = DimSing 1 }
instance {-# OVERLAPPING #-} KnownDim 2 where
{ {-# INLINE dim #-}; dim = DimSing 2 }
instance {-# OVERLAPPING #-} KnownDim 3 where
{ {-# INLINE dim #-}; dim = DimSing 3 }
instance {-# OVERLAPPING #-} KnownDim 4 where
{ {-# INLINE dim #-}; dim = DimSing 4 }
instance {-# OVERLAPPING #-} KnownDim 5 where
{ {-# INLINE dim #-}; dim = DimSing 5 }
instance {-# OVERLAPPING #-} KnownDim 6 where
{ {-# INLINE dim #-}; dim = DimSing 6 }
instance {-# OVERLAPPING #-} KnownDim 7 where
{ {-# INLINE dim #-}; dim = DimSing 7 }
instance {-# OVERLAPPING #-} KnownDim 8 where
{ {-# INLINE dim #-}; dim = DimSing 8 }
instance {-# OVERLAPPING #-} KnownDim 9 where
{ {-# INLINE dim #-}; dim = DimSing 9 }
instance {-# OVERLAPPING #-} KnownDim 10 where
{ {-# INLINE dim #-}; dim = DimSing 10 }
instance {-# OVERLAPPING #-} KnownDim 11 where
{ {-# INLINE dim #-}; dim = DimSing 11 }
instance {-# OVERLAPPING #-} KnownDim 12 where
{ {-# INLINE dim #-}; dim = DimSing 12 }
instance {-# OVERLAPPING #-} KnownDim 13 where
{ {-# INLINE dim #-}; dim = DimSing 13 }
instance {-# OVERLAPPING #-} KnownDim 14 where
{ {-# INLINE dim #-}; dim = DimSing 14 }
instance {-# OVERLAPPING #-} KnownDim 15 where
{ {-# INLINE dim #-}; dim = DimSing 15 }
instance {-# OVERLAPPING #-} KnownDim 16 where
{ {-# INLINE dim #-}; dim = DimSing 16 }
instance {-# OVERLAPPING #-} KnownDim 17 where
{ {-# INLINE dim #-}; dim = DimSing 17 }
instance {-# OVERLAPPING #-} KnownDim 18 where
{ {-# INLINE dim #-}; dim = DimSing 18 }
instance {-# OVERLAPPING #-} KnownDim 19 where
{ {-# INLINE dim #-}; dim = DimSing 19 }
instance {-# OVERLAPPING #-} KnownDim 20 where
{ {-# INLINE dim #-}; dim = DimSing 20 }
instance KnownDim n => KnownDim ('N n) where
{-# INLINE dim #-}
dim = unsafeCoerce# (dim @Nat @n)
someDimVal :: Word -> SomeDim
someDimVal = unsafeCoerce#
{-# INLINE someDimVal #-}
constrain :: forall (m :: Nat) x . KnownDim m
=> Dim x -> Maybe (Dim (XN m))
constrain (DimSing x) | dimVal' @m > x = Nothing
| otherwise = Just (unsafeCoerce# x)
{-# INLINE constrain #-}
constrainBy :: forall m x . Dim m -> Dim x -> Maybe (Dim (XN m))
constrainBy D = constrain @m
#if __GLASGOW_HASKELL__ < 802
constrainBy _ = error "Dim: Impossible pattern."
#endif
relax :: forall (m :: Nat) (n :: Nat) . (MinDim m n) => Dim (XN n) -> Dim (XN m)
relax = unsafeCoerce#
{-# INLINE relax #-}
sameDim :: forall (x :: Nat) (y :: Nat)
. Dim x -> Dim y -> Maybe (Evidence (x ~ y))
sameDim (DimSing a) (DimSing b)
| a == b = Just (unsafeCoerce# (E @(x ~ x)))
| otherwise = Nothing
{-# INLINE sameDim #-}
sameDim' :: forall (x :: Nat) (y :: Nat) p q
. (KnownDim x, KnownDim y)
=> p x -> q y -> Maybe (Evidence (x ~ y))
sameDim' _ _ = sameDim' (dim @Nat @x) (dim @Nat @y)
{-# INLINE sameDim' #-}
compareDim :: Dim a -> Dim b -> Ordering
compareDim = unsafeCoerce# (compare :: Word -> Word -> Ordering)
{-# INLINE compareDim #-}
compareDim' :: forall a b p q
. (KnownDim a, KnownDim b) => p a -> q b -> Ordering
compareDim' _ _ = compareDim (dim @_ @a) (dim @_ @b)
{-# INLINE compareDim' #-}
instance Eq (Dim (n :: Nat)) where
_ == _ = True
{-# INLINE (==) #-}
instance Eq (Dim (x :: XNat)) where
DimSing a == DimSing b = a == b
{-# INLINE (==) #-}
instance Ord (Dim (n :: Nat)) where
compare _ _ = EQ
{-# INLINE compare #-}
instance Ord (Dim (x :: XNat)) where
compare = compareDim
{-# INLINE compare #-}
instance Show (Dim x) where
showsPrec p = showsPrec p . dimVal
{-# INLINE showsPrec #-}
instance KnownDim m => Read (Dim ('XN m)) where
readsPrec p xs = do (a,ys) <- readsPrec p xs
case constrain (someDimVal a) of
Nothing -> []
Just n -> [(n,ys)]
plusDim :: Dim n -> Dim m -> Dim (n + m)
plusDim (DimSing a) (DimSing b) = unsafeCoerce# (a + b)
{-# INLINE plusDim #-}
minusDim :: MinDim m n => Dim n -> Dim m -> Dim (n - m)
minusDim (DimSing a) (DimSing b) = unsafeCoerce# (a - b)
{-# INLINE minusDim #-}
minusDimM :: Dim n -> Dim m -> Maybe (Dim (n - m))
minusDimM (DimSing a) (DimSing b)
| a >= b = Just (unsafeCoerce# (a - b))
| otherwise = Nothing
{-# INLINE minusDimM #-}
timesDim :: Dim n -> Dim m -> Dim ((*) n m)
timesDim (DimSing a) (DimSing b) = unsafeCoerce# (a * b)
{-# INLINE timesDim #-}
powerDim :: Dim n -> Dim m -> Dim ((^) n m)
powerDim (DimSing a) (DimSing b) = unsafeCoerce# (a ^ b)
{-# INLINE powerDim #-}
inferDimLE :: forall m n . MinDim m n => Evidence (m <= n)
inferDimLE = unsafeCoerce# (E @(n <= n))
data DimKind :: Type -> Type where
DimNat :: DimKind Nat
DimXNat :: DimKind XNat
class KnownDimKind k where
dimKind :: DimKind k
instance KnownDimKind Nat where
dimKind = DimNat
instance KnownDimKind XNat where
dimKind = DimXNat
reifyDim :: forall r d . Dim d -> (KnownDim d => r) -> r
reifyDim d k = unsafeCoerce# (MagicDim k :: MagicDim d r) d
{-# INLINE reifyDim #-}
newtype MagicDim d r = MagicDim (KnownDim d => r)
dimEv :: Dim d -> Evidence (KnownDim d)
dimEv d = reifyDim d E
{-# INLINE dimEv #-}
data PatXDim (xn :: XNat) where
PatN :: KnownDim n => Dim n -> PatXDim ('N n)
PatXN :: (KnownDim n, MinDim m n) => Dim n -> PatXDim ('XN m)
dimXNEv :: forall (xn :: XNat) . XNatType xn -> Dim xn -> PatXDim xn
dimXNEv Nt (DimSing k) = reifyDim dd (PatN dd)
where
dd = DimSing @Nat @_ k
dimXNEv XNt xn@(DimSing k) = reifyDim dd (f dd xn)
where
dd = DimSing @Nat @_ k
f :: forall (d :: Nat) (m :: Nat)
. KnownDim d => Dim d -> Dim ('XN m) -> PatXDim ('XN m)
f d _ = case ( unsafeCoerce# (E @((CmpNat m m == 'GT) ~ 'False, m <= m))
:: Evidence ((CmpNat m d == 'GT) ~ 'False, m <= d)
) of
E -> PatXN d
{-# INLINE dimXNEv #-}