{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE NoStarIsType #-}
#endif
module Numeric.Dimensions.Dim
(
XNat (..), XN, N, XNatType (..)
, Dim ( D, Dn, Dx
, D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, D10, D11, D12, D13
, D14, D15, D16, D17, D18, D19, D20, D21, D22, D23, D24, D25
)
, SomeDim
, KnownDim (..), BoundedDim (..), minDim, KnownXNatType (..), FixedDim
, dimVal, dimVal', typeableDim, someDimVal
, sameDim, sameDim'
, compareDim, compareDim'
, constrainBy, relax
, plusDim, minusDim, minusDimM, timesDim, powerDim, divDim, modDim, log2Dim
, Nat, CmpNat, SOrdering (..), type (+), type (-), type (*), type (^), type (<=)
, KnownDimKind (..), DimKind (..)
, Dims, SomeDims (..), Dimensions (..), BoundedDims (..), minDims
, TypedList ( Dims, XDims, AsXDims, KnownDims
, U, (:*), Empty, TypeList, Cons, Snoc, Reverse)
, typeableDims, inferTypeableDims
, listDims, someDimsVal, totalDim, totalDim'
, sameDims, sameDims'
, inSpaceOf, asSpaceOf
, xDims, xDims'
, stripPrefixDims, stripSuffixDims
, AsXDims, AsDims, FixedDims, KnownXNatTypes
, RepresentableList (..), TypeList, types
, order, order'
) where
import Data.Bits (countLeadingZeros, finiteBitSize)
import Data.Coerce
import Data.Constraint
import Data.Data hiding (TypeRep, typeRep, typeRepTyCon)
import Data.Kind (Constraint, Type)
import qualified Data.List (stripPrefix)
import Data.Type.List
import Data.Type.Lits
import GHC.Exts (Proxy#, proxy#, unsafeCoerce#)
import qualified GHC.Generics as G
import Numeric.Natural (Natural)
import Numeric.TypedList
import qualified Text.Read as Read
import qualified Text.Read.Lex as Read
import Type.Reflection
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
deriving ( Typeable )
type Dims (xs :: [k]) = TypedList Dim xs
pattern D :: forall (n :: Nat) . () => KnownDim n => Dim n
pattern D <- (dimEv -> Dict)
where
D = dim @n
{-# COMPLETE D #-}
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 = coerce k
pattern Dx :: forall (xn :: XNat) . KnownXNatType xn
=> forall (n :: Nat) (m :: Nat)
. (KnownDim n, m <= n, xn ~ 'XN m) => Dim n -> Dim xn
pattern Dx k <- (dimXNEv (xNatType @xn) -> PatXN k)
where
Dx k = coerce k
{-# COMPLETE Dn, Dx #-}
class KnownDim (n :: Nat) where
dim :: Dim n
class KnownDimKind k => BoundedDim (n :: k) where
type family DimBound n :: Nat
dimBound :: Dim (DimBound n)
constrainDim :: forall (l :: Type) (y :: l) . Dim y -> Maybe (Dim n)
instance KnownDim n => BoundedDim (n :: Nat) where
type DimBound n = n
dimBound = dim @n
{-# INLINE dimBound #-}
constrainDim (DimSing y)
| dimVal' @n == y = Just (DimSing y)
| otherwise = Nothing
{-# INLINE constrainDim #-}
instance KnownDim n => BoundedDim ('N n) where
type DimBound ('N n) = n
dimBound = dim @n
{-# INLINE dimBound #-}
constrainDim (DimSing y)
| dimVal' @n == y = Just (DimSing y)
| otherwise = Nothing
{-# INLINE constrainDim #-}
instance KnownDim m => BoundedDim ('XN m) where
type DimBound ('XN m) = m
dimBound = dim @m
{-# INLINE dimBound #-}
constrainDim (DimSing y)
| dimVal' @m <= y = Just (DimSing y)
| otherwise = Nothing
{-# INLINE constrainDim #-}
minDim :: forall (k :: Type) (d :: k) . BoundedDim d => Dim d
minDim = coerce (dimBound @k @d)
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 :: forall (k :: Type) (x :: k) . Dim (x :: k) -> Word
dimVal = coerce
{-# INLINE dimVal #-}
dimVal' :: forall (n :: Nat) . KnownDim n => Word
dimVal' = coerce (dim @n)
{-# INLINE dimVal' #-}
typeableDim :: forall (n :: Nat) . Typeable n => Dim n
typeableDim = DimSing . read . tyConName . typeRepTyCon $ typeRep @n
{-# INLINE typeableDim #-}
type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where
FixedDim ('N a) b = a ~ b
FixedDim ('XN m) b = m <= b
instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where
{-# INLINE dim #-}
dim = DimSing (fromIntegral (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 {-# OVERLAPPING #-} KnownDim 21 where
{ {-# INLINE dim #-}; dim = DimSing 21 }
instance {-# OVERLAPPING #-} KnownDim 22 where
{ {-# INLINE dim #-}; dim = DimSing 22 }
instance {-# OVERLAPPING #-} KnownDim 23 where
{ {-# INLINE dim #-}; dim = DimSing 23 }
instance {-# OVERLAPPING #-} KnownDim 24 where
{ {-# INLINE dim #-}; dim = DimSing 24 }
instance {-# OVERLAPPING #-} KnownDim 25 where
{ {-# INLINE dim #-}; dim = DimSing 25 }
instance Class (KnownNat n) (KnownDim n) where
cls = Sub $ reifyNat @_ @n (fromIntegral $ dimVal' @n) Dict
someDimVal :: Word -> SomeDim
someDimVal = coerce
{-# INLINE someDimVal #-}
constrainBy :: forall (k :: Type) (x :: k) (p :: k -> Type) (l :: Type) (y :: l)
. BoundedDim x => p x -> Dim y -> Maybe (Dim x)
constrainBy = const (constrainDim @k @x @l @y)
{-# INLINE constrainBy #-}
relax :: forall (m :: Nat) (n :: Nat) . (<=) m n => Dim (XN n) -> Dim (XN m)
relax = coerce
{-# INLINE relax #-}
sameDim :: forall (x :: Nat) (y :: Nat)
. Dim x -> Dim y -> Maybe (Dict (x ~ y))
sameDim (DimSing a) (DimSing b)
| a == b = Just (unsafeCoerceDict @(x ~ x) Dict)
| otherwise = Nothing
{-# INLINE sameDim #-}
sameDim' :: forall (x :: Nat) (y :: Nat) (p :: Nat -> Type) (q :: Nat -> Type)
. (KnownDim x, KnownDim y)
=> p x -> q y -> Maybe (Dict (x ~ y))
sameDim' = const . const $ sameDim (dim @x) (dim @y)
{-# INLINE sameDim' #-}
compareDim :: forall (a :: Nat) (b :: Nat)
. Dim a -> Dim b -> SOrdering (CmpNat a b)
compareDim a b
= case coerce (compare :: Word -> Word -> Ordering) a b of
LT -> unsafeCoerce# SLT
EQ -> unsafeCoerce# SEQ
GT -> unsafeCoerce# SGT
{-# INLINE compareDim #-}
compareDim' :: forall (a :: Nat) (b :: Nat) (p :: Nat -> Type) (q :: Nat -> Type)
. (KnownDim a, KnownDim b) => p a -> q b -> SOrdering (CmpNat a b)
compareDim' = const . const $ compareDim (dim @a) (dim @b)
{-# INLINE compareDim' #-}
plusDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (n + m)
plusDim = coerce ((+) :: Word -> Word -> Word)
{-# INLINE plusDim #-}
minusDim :: forall (n :: Nat) (m :: Nat) . (<=) m n => Dim n -> Dim m -> Dim (n - m)
minusDim = coerce ((-) :: Word -> Word -> Word)
{-# INLINE minusDim #-}
minusDimM :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Maybe (Dim (n - m))
minusDimM (DimSing a) (DimSing b)
| a >= b = Just (coerce (a - b))
| otherwise = Nothing
{-# INLINE minusDimM #-}
timesDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((*) n m)
timesDim = coerce ((*) :: Word -> Word -> Word)
{-# INLINE timesDim #-}
powerDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((^) n m)
powerDim = coerce ((^) :: Word -> Word -> Word)
{-# INLINE powerDim #-}
divDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Div n m)
divDim = coerce (div :: Word -> Word -> Word)
modDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Mod n m)
modDim = coerce (mod :: Word -> Word -> Word)
log2Dim :: forall (n :: Nat) . Dim n -> Dim (Log2 n)
log2Dim (DimSing 0) = undefined
log2Dim (DimSing x) = DimSing . fromIntegral $ finiteBitSize x - 1 - countLeadingZeros x
data DimKind :: Type -> Type where
DimNat :: DimKind Nat
DimXNat :: DimKind XNat
class KnownDimKind (k :: Type) where
dimKind :: DimKind k
instance KnownDimKind Nat where
dimKind = DimNat
instance KnownDimKind XNat where
dimKind = DimXNat
pattern D0 :: forall (n :: Nat) . () => n ~ 0 => Dim n
pattern D0 <- (sameDim (D @0) -> Just Dict)
where D0 = DimSing 0
pattern D1 :: forall (n :: Nat) . () => n ~ 1 => Dim n
pattern D1 <- (sameDim (D @1) -> Just Dict)
where D1 = DimSing 1
pattern D2 :: forall (n :: Nat) . () => n ~ 2 => Dim n
pattern D2 <- (sameDim (D @2) -> Just Dict)
where D2 = DimSing 2
pattern D3 :: forall (n :: Nat) . () => n ~ 3 => Dim n
pattern D3 <- (sameDim (D @3) -> Just Dict)
where D3 = DimSing 3
pattern D4 :: forall (n :: Nat) . () => n ~ 4 => Dim n
pattern D4 <- (sameDim (D @4) -> Just Dict)
where D4 = DimSing 4
pattern D5 :: forall (n :: Nat) . () => n ~ 5 => Dim n
pattern D5 <- (sameDim (D @5) -> Just Dict)
where D5 = DimSing 5
pattern D6 :: forall (n :: Nat) . () => n ~ 6 => Dim n
pattern D6 <- (sameDim (D @6) -> Just Dict)
where D6 = DimSing 6
pattern D7 :: forall (n :: Nat) . () => n ~ 7 => Dim n
pattern D7 <- (sameDim (D @7) -> Just Dict)
where D7 = DimSing 7
pattern D8 :: forall (n :: Nat) . () => n ~ 8 => Dim n
pattern D8 <- (sameDim (D @8) -> Just Dict)
where D8 = DimSing 8
pattern D9 :: forall (n :: Nat) . () => n ~ 9 => Dim n
pattern D9 <- (sameDim (D @9) -> Just Dict)
where D9 = DimSing 9
pattern D10 :: forall (n :: Nat) . () => n ~ 10 => Dim n
pattern D10 <- (sameDim (D @10) -> Just Dict)
where D10 = DimSing 10
pattern D11 :: forall (n :: Nat) . () => n ~ 11 => Dim n
pattern D11 <- (sameDim (D @11) -> Just Dict)
where D11 = DimSing 11
pattern D12 :: forall (n :: Nat) . () => n ~ 12 => Dim n
pattern D12 <- (sameDim (D @12) -> Just Dict)
where D12 = DimSing 12
pattern D13 :: forall (n :: Nat) . () => n ~ 13 => Dim n
pattern D13 <- (sameDim (D @13) -> Just Dict)
where D13 = DimSing 13
pattern D14 :: forall (n :: Nat) . () => n ~ 14 => Dim n
pattern D14 <- (sameDim (D @14) -> Just Dict)
where D14 = DimSing 14
pattern D15 :: forall (n :: Nat) . () => n ~ 15 => Dim n
pattern D15 <- (sameDim (D @15) -> Just Dict)
where D15 = DimSing 15
pattern D16 :: forall (n :: Nat) . () => n ~ 16 => Dim n
pattern D16 <- (sameDim (D @16) -> Just Dict)
where D16 = DimSing 16
pattern D17 :: forall (n :: Nat) . () => n ~ 17 => Dim n
pattern D17 <- (sameDim (D @17) -> Just Dict)
where D17 = DimSing 17
pattern D18 :: forall (n :: Nat) . () => n ~ 18 => Dim n
pattern D18 <- (sameDim (D @18) -> Just Dict)
where D18 = DimSing 18
pattern D19 :: forall (n :: Nat) . () => n ~ 19 => Dim n
pattern D19 <- (sameDim (D @19) -> Just Dict)
where D19 = DimSing 19
pattern D20 :: forall (n :: Nat) . () => n ~ 20 => Dim n
pattern D20 <- (sameDim (D @20) -> Just Dict)
where D20 = DimSing 20
pattern D21 :: forall (n :: Nat) . () => n ~ 21 => Dim n
pattern D21 <- (sameDim (D @21) -> Just Dict)
where D21 = DimSing 21
pattern D22 :: forall (n :: Nat) . () => n ~ 22 => Dim n
pattern D22 <- (sameDim (D @22) -> Just Dict)
where D22 = DimSing 22
pattern D23 :: forall (n :: Nat) . () => n ~ 23 => Dim n
pattern D23 <- (sameDim (D @23) -> Just Dict)
where D23 = DimSing 23
pattern D24 :: forall (n :: Nat) . () => n ~ 24 => Dim n
pattern D24 <- (sameDim (D @24) -> Just Dict)
where D24 = DimSing 24
pattern D25 :: forall (n :: Nat) . () => n ~ 25 => Dim n
pattern D25 <- (sameDim (D @25) -> Just Dict)
where D25 = DimSing 25
pattern Dims :: forall (ds :: [Nat]) . () => Dimensions ds => Dims ds
pattern Dims <- (dimsEv -> Dict)
where
Dims = dims @ds
{-# COMPLETE Dims #-}
pattern KnownDims :: forall (ds :: [Nat]) . ()
=> ( All KnownDim ds, All BoundedDim ds
, RepresentableList ds, Dimensions ds)
=> Dims ds
pattern KnownDims <- (patKDims -> PatKDims)
where
KnownDims = dims @ds
{-# COMPLETE KnownDims #-}
pattern XDims :: forall (xns :: [XNat]) . KnownXNatTypes xns
=> forall (ns :: [Nat]) . (FixedDims xns ns, Dimensions ns)
=> Dims ns -> Dims xns
pattern XDims ns <- (patXDims -> PatXDims ns)
where
XDims ns = unsafeCoerce# ns
{-# COMPLETE XDims #-}
pattern AsXDims :: forall (ns :: [Nat]) . ()
=> (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))
=> Dims (AsXDims ns) -> Dims ns
pattern AsXDims xns <- (patAsXDims -> PatAsXDims xns)
where
AsXDims xns = unsafeCoerce# xns
{-# COMPLETE AsXDims #-}
data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)
class Dimensions (ds :: [Nat]) where
dims :: Dims ds
instance Dimensions '[] where
dims = U
{-# INLINE dims #-}
instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds) where
dims = dim :* dims
{-# INLINE dims #-}
class KnownDimKind k => BoundedDims (ds :: [k]) where
type family DimsBound ds :: [Nat]
dimsBound :: Dims (DimsBound ds)
constrainDims :: forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds)
inferAllBoundedDims :: Dict (All BoundedDim ds, RepresentableList ds)
instance Dimensions ns => BoundedDims (ns :: [Nat]) where
type DimsBound ns = ns
dimsBound = dims @ns
{-# INLINE dimsBound #-}
constrainDims ys
| listDims ys == listDims (dims @ns)
= Just (unsafeCoerce# ys)
| otherwise = Nothing
{-# INLINE constrainDims #-}
inferAllBoundedDims = go (dims @ns)
where
go :: forall (ds :: [Nat]) . Dims ds
-> Dict (All BoundedDim ds, RepresentableList ds)
go U = Dict
go (D :* ds)
| Dict <- go ds = Dict
instance BoundedDims ('[] :: [XNat]) where
type DimsBound '[] = '[]
dimsBound = U
constrainDims = const $ Just U
inferAllBoundedDims = Dict
instance (BoundedDim n, BoundedDims ns) => BoundedDims ((n ': ns) :: [XNat]) where
type DimsBound (n ': ns) = DimBound n ': DimsBound ns
dimsBound = dimBound @XNat @n :* dimsBound @XNat @ns
constrainDims U = Nothing
constrainDims (y :* ys) = (:*) <$> constrainDim y <*> constrainDims ys
inferAllBoundedDims = case inferAllBoundedDims @XNat @ns of Dict -> Dict
minDims :: forall (k :: Type) (ds :: [k])
. BoundedDims ds => Dims ds
minDims = unsafeCoerce# (dimsBound @k @ds)
typeableDims :: forall (ds :: [Nat]) . Typeable ds => Dims ds
typeableDims = case typeRep @ds of
App (App _ (tx :: TypeRep (n :: k1))) (txs :: TypeRep (ns :: k2))
-> case unsafeCoerceDict @(Nat ~ Nat, [Nat] ~ [Nat])
@(Nat ~ k1 , [Nat] ~ k2) Dict of
Dict -> case unsafeCoerceDict @(ds ~ ds)
@(ds ~ (n ': ns)) Dict of
Dict -> withTypeable tx (typeableDim @n)
:* withTypeable txs (typeableDims @ns)
Con _
-> unsafeCoerce# U
r -> error ("typeableDims -- impossible typeRep: " ++ show r)
{-# INLINE typeableDims #-}
inferTypeableDims :: forall (ds :: [Nat]) . Dims ds -> Dict (Typeable ds)
inferTypeableDims U = Dict
inferTypeableDims ((D :: Dim d) :* ds)
| Dict <- mapDict cls (Dict @(KnownDim d))
, Dict <- inferTypeableDims ds
= Dict
listDims :: forall (k :: Type) (xs :: [k]) . Dims xs -> [Word]
listDims = unsafeCoerce#
{-# INLINE listDims #-}
someDimsVal :: [Word] -> SomeDims
someDimsVal = SomeDims . unsafeCoerce#
{-# INLINE someDimsVal #-}
totalDim :: forall (k :: Type) (xs :: [k]) . Dims xs -> Word
totalDim = product . listDims
{-# INLINE totalDim #-}
totalDim' :: forall (xs :: [Nat]) . Dimensions xs => Word
totalDim' = totalDim (dims @xs)
{-# INLINE totalDim' #-}
xDims :: forall (xns :: [XNat]) (ns :: [Nat])
. FixedDims xns ns => Dims ns -> Dims xns
xDims = unsafeCoerce#
{-# INLINE xDims #-}
xDims' :: forall (xns :: [XNat]) (ns :: [Nat])
. (FixedDims xns ns, Dimensions ns) => Dims xns
xDims' = xDims @xns (dims @ns)
{-# INLINE xDims' #-}
stripPrefixDims :: forall (xs :: [Nat]) (ys :: [Nat])
. Dims xs -> Dims ys
-> Maybe (Dims (StripPrefix xs ys))
stripPrefixDims = unsafeCoerce# (Data.List.stripPrefix :: [Word] -> [Word] -> Maybe [Word])
{-# INLINE stripPrefixDims #-}
stripSuffixDims :: forall (xs :: [Nat]) (ys :: [Nat])
. Dims xs -> Dims ys
-> Maybe (Dims (StripSuffix xs ys))
stripSuffixDims = unsafeCoerce# stripSuf
where
stripSuf :: [Word] -> [Word] -> Maybe [Word]
stripSuf suf whole = go pref whole
where
pref = getPref suf whole
getPref (_:as) (_:bs) = getPref as bs
getPref [] bs = zipWith const whole bs
getPref _ [] = []
go (_:as) (_:bs) = go as bs
go [] bs = if suf == bs then Just pref else Nothing
go _ [] = Nothing
{-# INLINE stripSuffixDims #-}
sameDims :: forall (as :: [Nat]) (bs :: [Nat])
. Dims as -> Dims bs -> Maybe (Dict (as ~ bs))
sameDims as bs
| listDims as == listDims bs
= Just (unsafeCoerceDict @(as ~ as) Dict)
| otherwise = Nothing
{-# INLINE sameDims #-}
sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) (p :: [Nat] -> Type) (q :: [Nat] -> Type)
. (Dimensions as, Dimensions bs)
=> p as -> q bs -> Maybe (Dict (as ~ bs))
sameDims' = const . const $ sameDims (dims @as) (dims @bs)
{-# INLINE sameDims' #-}
inSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] -> Type) (q :: [k] -> Type)
. p ds -> q ds -> p ds
inSpaceOf = const
{-# INLINE inSpaceOf #-}
asSpaceOf :: forall (k :: Type) (ds :: [k])
(p :: [k] -> Type) (q :: [k] -> Type) (r :: Type)
. p ds -> (q ds -> r) -> (q ds -> r)
asSpaceOf = const id
{-# INLINE asSpaceOf #-}
type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where
AsXDims '[] = '[]
AsXDims (n ': ns) = N n ': AsXDims ns
type family AsDims (xns::[XNat]) = (ns :: [Nat]) | ns -> xns where
AsDims '[] = '[]
AsDims (N x ': xs) = x ': AsDims xs
type family FixedDims (xns::[XNat]) (ns :: [Nat]) :: Constraint where
FixedDims '[] ns = (ns ~ '[])
FixedDims (xn ': xns) ns
= ( ns ~ (Head ns ': Tail ns)
, FixedDim xn (Head ns)
, FixedDims xns (Tail ns))
type KnownXNatTypes xns = All KnownXNatType xns
instance Typeable d => Data (Dim (d :: Nat)) where
gfoldl _ = id
gunfold _ z = const (z (typeableDim @d))
toConstr = const $ dimNatConstr (dimVal (typeableDim @d))
dataTypeOf = const $ dimDataType (dimVal (typeableDim @d))
dimDataType :: Word -> DataType
dimDataType = mkDataType "Numeric.Dim.Dim" . (:[]) . dimNatConstr
dimNatConstr :: Word -> Constr
dimNatConstr d = mkConstr (dimDataType d) ("D" ++ show d) [] Prefix
instance KnownDim d => G.Generic (Dim (d :: Nat)) where
type Rep (Dim d) = G.D1
('G.MetaData "Dim" "Numeric.Dim" "dimensions" 'False)
(G.C1 ('G.MetaCons (AppendSymbol "D" (ShowNat d)) 'G.PrefixI 'False) G.U1)
from D = G.M1 (G.M1 G.U1)
to = const (dim @d)
instance Eq (Dim (n :: Nat)) where
(==) = const (const True)
{-# INLINE (==) #-}
(/=) = const (const False)
{-# INLINE (/=) #-}
instance Eq (Dim (x :: XNat)) where
(==) = coerce ((==) :: Word -> Word -> Bool)
{-# INLINE (==) #-}
(/=) = coerce ((/=) :: Word -> Word -> Bool)
{-# INLINE (/=) #-}
instance Eq (Dims (ds :: [Nat])) where
(==) = const (const True)
{-# INLINE (==) #-}
(/=) = const (const False)
{-# INLINE (/=) #-}
instance Eq (Dims (ds :: [XNat])) where
(==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)
{-# INLINE (==) #-}
(/=) = unsafeCoerce# ((/=) :: [Word] -> [Word] -> Bool)
{-# INLINE (/=) #-}
instance Eq SomeDims where
SomeDims as == SomeDims bs = listDims as == listDims bs
{-# INLINE (==) #-}
SomeDims as /= SomeDims bs = listDims as /= listDims bs
{-# INLINE (/=) #-}
instance Ord (Dim (n :: Nat)) where
compare = const (const EQ)
{-# INLINE compare #-}
instance Ord (Dim (x :: XNat)) where
compare = coerce (compare :: Word -> Word -> Ordering)
{-# INLINE compare #-}
instance Ord (Dims (ds :: [Nat])) where
compare = const (const EQ)
{-# INLINE compare #-}
instance Ord (Dims (ds :: [XNat])) where
compare = unsafeCoerce# (compare :: [Word] -> [Word] -> Ordering)
{-# INLINE compare #-}
instance Ord SomeDims where
compare (SomeDims as) (SomeDims bs) = compare (listDims as) (listDims bs)
{-# INLINE compare #-}
instance Show (Dim (x :: k)) where
showsPrec _ d = showChar 'D' . shows (dimVal d)
{-# INLINE showsPrec #-}
instance Show (Dims (xs :: [k])) where
showsPrec = typedListShowsPrec @k @Dim @xs showsPrec
instance Show SomeDims where
showsPrec p (SomeDims ds)
= showParen (p >= 10)
$ showString "SomeDims " . showsPrec 10 ds
instance BoundedDim x => Read (Dim (x :: k)) where
readPrec = Read.lexP >>= \case
Read.Ident ('D':s)
| Just d <- Read.readMaybe s
>>= constrainDim @k @x @XNat @(XN 0) . DimSing
-> return d
_ -> Read.pfail
readList = Read.readListDefault
readListPrec = Read.readListPrecDefault
instance BoundedDims xs => Read (Dims (xs :: [k])) where
readPrec = case inferAllBoundedDims @k @xs of
Dict -> typedListReadPrec @k @BoundedDim ":*" Read.readPrec (tList @k @xs)
readList = Read.readListDefault
readListPrec = Read.readListPrecDefault
instance Read SomeDims where
readPrec = Read.parens . Read.prec 10 $ do
Read.lift . Read.expect $ Read.Ident "SomeDims"
withTypedListReadPrec @Nat @Dim @SomeDims
(\g -> (\(Dx d) -> g d) <$> Read.readPrec @(Dim (XN 0)))
SomeDims
reifyDim :: forall (r :: Type) (d :: Nat) . Dim d -> (KnownDim d => r) -> r
reifyDim d k = unsafeCoerce# (MagicDim k :: MagicDim d r) d
{-# INLINE reifyDim #-}
newtype MagicDim (d :: Nat) (r :: Type) = MagicDim (KnownDim d => r)
reifyNat :: forall (r :: Type) (d :: Nat) . Natural -> (KnownNat d => r) -> r
reifyNat d k = unsafeCoerce# (MagicNat k :: MagicNat d r) d
{-# INLINE reifyNat #-}
newtype MagicNat (d :: Nat) (r :: Type) = MagicNat (KnownNat d => r)
dimEv :: forall (d :: Nat) . Dim d -> Dict (KnownDim d)
dimEv d = reifyDim d Dict
{-# INLINE dimEv #-}
reifyDims :: forall (r :: Type) (ds :: [Nat]) . Dims ds -> (Dimensions ds => r) -> r
reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds
{-# INLINE reifyDims #-}
newtype MagicDims (ds :: [Nat]) (r :: Type) = MagicDims (Dimensions ds => r)
dimsEv :: forall (ds :: [Nat]) . Dims ds -> Dict (Dimensions ds)
dimsEv ds = reifyDims ds Dict
{-# INLINE dimsEv #-}
data PatXDim (xn :: XNat) where
PatN :: KnownDim n => Dim n -> PatXDim ('N n)
PatXN :: (KnownDim n, 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 unsafeCoerceDict @(m <= m) @(m <= d) Dict of
Dict -> const (PatXN d)
{-# INLINE dimXNEv #-}
data PatXDims (xns :: [XNat])
= forall (ns :: [Nat])
. (FixedDims xns ns, Dimensions ns) => PatXDims (Dims ns)
patXDims :: forall (xns :: [XNat])
. All KnownXNatType xns => Dims xns -> PatXDims xns
patXDims U = PatXDims U
patXDims (Dn n :* xns) = case patXDims xns of
PatXDims ns -> PatXDims (n :* ns)
patXDims (Dx n :* xns) = case patXDims xns of
PatXDims ns -> PatXDims (n :* ns)
{-# INLINE patXDims #-}
data PatAsXDims (ns :: [Nat])
= (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))
=> PatAsXDims (Dims (AsXDims ns))
patAsXDims :: forall (ns :: [Nat]) . Dims ns -> PatAsXDims ns
patAsXDims U = PatAsXDims U
patAsXDims (n@D :* ns) = case patAsXDims ns of
PatAsXDims xns -> PatAsXDims (Dn n :* xns)
{-# INLINE patAsXDims #-}
data PatKDims (ns :: [Nat])
= (All KnownDim ns, All BoundedDim ns, RepresentableList ns, Dimensions ns) => PatKDims
patKDims :: forall (ns :: [Nat]) . Dims ns -> PatKDims ns
patKDims U = PatKDims
patKDims (D :* ns) = case patKDims ns of
PatKDims -> PatKDims
{-# INLINE patKDims #-}
unsafeCoerceDict :: forall (a :: Constraint) (b :: Constraint)
. Dict a -> Dict b
unsafeCoerceDict = unsafeCoerce#