{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
module Numeric.Dimensions.Dims
( Dims, SomeDims (..), Dimensions (..), XDimensions (..)
, TypedList ( Dims, XDims, AsXDims, KnownDims
, U, (:*), Empty, TypeList, Cons, Snoc, Reverse)
, listDims, someDimsVal, totalDim, totalDim'
, sameDims, sameDims'
, compareDims, compareDims'
, inSpaceOf, asSpaceOf
, xDims, xDims'
, AsXDims, AsDims, FixedDims, KnownXNatTypes, type (:<), type (>:)
, RepresentableList (..), TypeList, types
, order, order'
, module Numeric.Dim
) where
import GHC.Exts (unsafeCoerce#, Constraint)
import qualified Text.Read as Read
import Numeric.Dim
import Numeric.Type.Evidence
import Numeric.Type.List
import Numeric.TypedList (RepresentableList (..), TypeList,
TypedList (..), order, order', types)
type Dims (xs :: [k]) = TypedList Dim xs
#if __GLASGOW_HASKELL__ >= 802
{-# COMPLETE Dims #-}
{-# COMPLETE XDims #-}
{-# COMPLETE AsXDims #-}
{-# COMPLETE KnownDims #-}
#endif
pattern Dims :: forall ds . () => Dimensions ds => Dims ds
pattern Dims <- (dimsEv -> E)
where
Dims = dims @_ @ds
pattern KnownDims :: forall ds . ()
=> (All KnownDim ds, Dimensions ds) => Dims ds
pattern KnownDims <- (patKDims -> PatKDims)
where
KnownDims = dims @_ @ds
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
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
data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)
class Dimensions (ds :: [k]) where
dims :: Dims ds
instance Dimensions ('[] :: [k]) where
dims = U
{-# INLINE dims #-}
instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds :: [k]) where
dims = dim :* dims
{-# INLINE dims #-}
class KnownXNatTypes xds => XDimensions (xds :: [XNat]) where
constrainDims :: Dims (ds :: [k]) -> Maybe (Dims xds)
instance XDimensions '[] where
constrainDims U = Just U
constrainDims _ = Nothing
{-# INLINE constrainDims #-}
instance (XDimensions xs, KnownDim m) => XDimensions (XN m ': xs) where
constrainDims (d :* ds) = case constrain d of
Nothing -> Nothing
Just xd -> (xd :*) <$> constrainDims ds
constrainDims Empty = Nothing
instance (XDimensions xs, KnownDim n) => XDimensions (N n ': xs) where
constrainDims (d :* ds)
| unsafeCoerce# d == dimVal' @n = (Dn D :*) <$> constrainDims ds
| otherwise = Nothing
constrainDims Empty = Nothing
listDims :: Dims xs -> [Word]
listDims = unsafeCoerce#
{-# INLINE listDims #-}
someDimsVal :: [Word] -> SomeDims
someDimsVal = SomeDims . unsafeCoerce#
{-# INLINE someDimsVal #-}
totalDim :: Dims xs -> Word
totalDim = product . listDims
{-# INLINE totalDim #-}
totalDim' :: forall xs . Dimensions xs => Word
totalDim' = totalDim (dims @_ @xs)
{-# INLINE totalDim' #-}
xDims :: FixedDims xns ns => Dims ns -> Dims xns
xDims = unsafeCoerce#
{-# INLINE xDims #-}
xDims' :: forall xns ns . (FixedDims xns ns, Dimensions ns) => Dims xns
xDims' = xDims @xns (dims @Nat @ns)
{-# INLINE xDims' #-}
sameDims :: Dims (as :: [Nat]) -> Dims (bs :: [Nat]) -> Maybe (Evidence (as ~ bs))
sameDims as bs
| listDims as == listDims bs
= Just (unsafeCoerce# (E @('[] ~ '[])))
| otherwise = Nothing
{-# INLINE sameDims #-}
sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) p q
. (Dimensions as, Dimensions bs)
=> p as -> q bs -> Maybe (Evidence (as ~ bs))
sameDims' _ _ = sameDims (dims @Nat @as) (dims @Nat @bs)
{-# INLINE sameDims' #-}
compareDims :: Dims as -> Dims bs -> Ordering
compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)
{-# INLINE compareDims #-}
compareDims' :: forall as bs p q
. (Dimensions as, Dimensions bs)
=> p as -> q bs -> Ordering
compareDims' _ _ = compareDims (dims @_ @as) (dims @_ @bs)
{-# INLINE compareDims' #-}
inSpaceOf :: a ds -> b ds -> a ds
inSpaceOf x _ = x
{-# INLINE inSpaceOf #-}
asSpaceOf :: a ds -> (b ds -> c) -> (b ds -> c)
asSpaceOf _ = id
{-# INLINE asSpaceOf #-}
instance Eq (Dims (ds :: [Nat])) where
(==) _ _ = True
instance Eq (Dims (ds :: [XNat])) where
(==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)
instance Eq SomeDims where
SomeDims as == SomeDims bs = listDims as == listDims bs
instance Ord (Dims (ds :: [Nat])) where
compare _ _ = EQ
instance Ord (Dims (ds :: [XNat])) where
compare = compareDims
instance Ord SomeDims where
compare (SomeDims as) (SomeDims bs) = compareDims as bs
instance Show (Dims xs) where
show ds = "Dims " ++ show (listDims ds)
showsPrec p ds
= showParen (p >= 10)
$ showString "Dims " . showsPrec p (listDims ds)
instance Show SomeDims where
show (SomeDims ds) = "SomeDims " ++ show (listDims ds)
showsPrec p (SomeDims ds)
= showParen (p >= 10)
$ showString "SomeDims " . showsPrec p (listDims ds)
instance Read SomeDims where
readPrec = Read.parens $ Read.prec 10 $ do
s <- Read.lexP
if s == Read.Ident "SomeDims"
then someDimsVal <$> Read.readPrec
else Read.pfail
instance Dimensions ds => Bounded (Dims ds) where
maxBound = dims
{-# INLINE maxBound #-}
minBound = dims
{-# INLINE minBound #-}
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
type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where
0 :< _ = '[]
1 :< ns = ns
n :< ns = n :+ ns
infixr 6 :<
type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where
_ >: 0 = '[]
ns >: 1 = ns
ns >: n = ns +: n
infixl 6 >:
reifyDims :: forall r ds . Dims ds -> ( Dimensions ds => r) -> r
reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds
{-# INLINE reifyDims #-}
newtype MagicDims ds r = MagicDims (Dimensions ds => r)
dimsEv :: Dims ds -> Evidence (Dimensions ds)
dimsEv ds = reifyDims ds E
{-# INLINE dimsEv #-}
data PatXDims (xns :: [XNat])
= forall (ns :: [Nat])
. (FixedDims xns ns, Dimensions ns) => PatXDims (Dims ns)
patXDims :: 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)
#if __GLASGOW_HASKELL__ >= 802
#else
patXDims _ = error "XDims/patXDims: impossible argument"
#endif
{-# INLINE patXDims #-}
data PatAsXDims (ns :: [Nat])
= (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))
=> PatAsXDims (Dims (AsXDims ns))
patAsXDims :: Dims ns -> PatAsXDims ns
patAsXDims U = PatAsXDims U
patAsXDims (n@D :* ns) = case patAsXDims ns of
PatAsXDims xns -> PatAsXDims (Dn n :* xns)
#if __GLASGOW_HASKELL__ >= 802
#else
patAsXDims _ = error "AsXDims/patAsXDims: impossible argument"
#endif
{-# INLINE patAsXDims #-}
data PatKDims (ns :: [k])
= (All KnownDim ns, Dimensions ns) => PatKDims
patKDims :: Dims ns -> PatKDims ns
patKDims U = PatKDims
patKDims (Dim :* ns) = case patKDims ns of
PatKDims -> PatKDims
#if __GLASGOW_HASKELL__ >= 802
#else
patKDims _ = error "Dims/patKDims: impossible argument"
#endif
{-# INLINE patKDims #-}