module Numeric.Dimensions.Dim
(
Nat, XNat, XN, N, Dim (..), dimVal, totalDim, fromInt
, SomeDims (..), SomeDim (..), someDimVal, someDimsVal, sameDim, compareDim
, inSpaceOf, asSpaceOf
, Dimensions (..), KnownDim (..), KnownDims
, AsXDims, AsDims, WrapDims, UnwrapDims
, ConsDim, NatKind
, FixedDim, FixedXDim, WrapNat, type (:<), type (>:)
, inferDimensions, inferDimKnownDims, inferDimFiniteList
, inferTailDimensions, inferConcatDimensions
, inferPrefixDimensions, inferSuffixDimensions
, inferSnocDimensions, inferInitDimensions
, inferTakeNDimensions, inferDropNDimensions
, inferReverseDimensions, reifyDimensions
, inferUnSnocDimensions, SnocDimensions
, inferUnConsDimensions, ConsDimensions
) where
import Data.Maybe (isJust)
import GHC.Exts (Constraint, unsafeCoerce#)
import Data.Type.Equality ((:~:)(..))
import Numeric.Dimensions.List
import Numeric.TypeLits
data Dim (ns :: k) where
D :: Dim '[]
(:*) :: forall (n::l) (ns::[k]) . NatKind [k] l
=> !(Dim n) -> !(Dim ns) -> Dim (ConsDim n ns)
Dn :: forall (n :: Nat) . KnownDim n => Dim (n :: Nat)
Dx :: forall (n :: Nat) (m :: Nat) . n <= m
=> !(Dim m) -> Dim (XN n)
infixr 5 :*
fromInt :: forall m . KnownDim m => Int -> Maybe (Dim (XN m))
fromInt i | i < dimVal' @m = Nothing
| otherwise = do
SomeDim (dn :: Dim n) <- someDimVal i
return $ case unsafeEqEvidence @(m <=? n) @'True of
Evidence -> Dx dn
data SomeDim = forall (n :: Nat) . SomeDim (Dim n)
data SomeDims = forall (ns :: [Nat]) . SomeDims (Dim ns)
dimVal :: Dim x -> Int
dimVal D = 1
dimVal (d :* ds) = dimVal d * dimVal ds
dimVal (Dn :: Dim m) = dimVal' @m
dimVal (Dx (Dn :: Dim m)) = dimVal' @m
totalDim :: forall ds proxy . Dimensions ds => proxy ds -> Int
totalDim _ = dimVal (dim @ds)
someDimVal :: Int -> Maybe SomeDim
someDimVal x | 0 > x = Nothing
| otherwise = Just (reifyDim x f)
where
f :: forall (n :: Nat) . KnownDim n => Proxy# n -> SomeDim
f _ = SomeDim (Dn @n)
someDimsVal :: [Int] -> Maybe SomeDims
someDimsVal [] = Just $ SomeDims D
someDimsVal (x:xs) | 0 > x = Nothing
| otherwise = do
SomeDim p <- someDimVal x
SomeDims ps <- someDimsVal xs
return $ SomeDims (p :* ps)
dimList :: Dim ds -> String
dimList D = ""
dimList d@Dn = show (dimVal d)
dimList (Dx d@Dn) = show (dimVal d)
dimList (d :* D) = show (dimVal d)
dimList (d :* ds) = show (dimVal d) ++ ' ':dimList ds
sameDim :: Dim as -> Dim bs -> Maybe (Evidence (as ~ bs))
sameDim D D = Just Evidence
sameDim (a :* as) (b :* bs) | dimVal a == dimVal b = (unsafeCoerce# (Evidence @())) <$ sameDim as bs
| otherwise = Nothing
sameDim _ _ = Nothing
compareDim :: Dim as -> Dim bs -> Ordering
compareDim D D = EQ
compareDim _ D = GT
compareDim D _ = LT
compareDim (a :* as) (b :* bs) = compareDim as bs `mappend` compare (dimVal a) (dimVal b)
compareDim a@Dn b@Dn = compare (dimVal a) (dimVal b)
compareDim (Dx a) (Dx b) = compare (dimVal a) (dimVal b)
compareDim a@Dn (Dx b) = compare (dimVal a) (dimVal b)
compareDim (Dx a) b@Dn = compare (dimVal a) (dimVal b)
compareDim a@Dn (b :* bs) = compareDim D bs `mappend` compare (dimVal a) (dimVal b)
compareDim (Dx a) (b :* bs) = compareDim D bs `mappend` compare (dimVal a) (dimVal b)
compareDim (a :* as) b@Dn = compareDim as D `mappend` compare (dimVal a) (dimVal b)
compareDim (a :* as) (Dx b) = compareDim as D `mappend` compare (dimVal a) (dimVal b)
inSpaceOf :: a ds -> b ds -> a ds
inSpaceOf x _ = x
asSpaceOf :: a ds -> (b ds -> c) -> (b ds -> c)
asSpaceOf _ = id
instance Show (Dim ds) where
show D = "Dim Ø"
show ds = "Dim " ++ dimList ds
instance Show SomeDims where
show (SomeDims p) = "Some" ++ show p
instance Eq (Dim ds) where
a == b = isJust $ sameDim a b
instance Eq SomeDims where
SomeDims as == SomeDims bs = isJust $ sameDim as bs
instance Ord (Dim ds) where
compare = compareDim
instance Ord SomeDims where
compare (SomeDims as) (SomeDims bs) = compareDim as bs
class Dimensions (ds :: [Nat]) where
dim :: Dim ds
instance Dimensions '[] where
dim = D
instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds) where
dim = Dn :* dim
instance Dimensions ds => Bounded (Dim ds) where
maxBound = dim
minBound = dim
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 WrapDims (x::[k]) :: [XNat] where
WrapDims ('[] :: [Nat]) = '[]
WrapDims ('[] :: [XNat]) = '[]
WrapDims (n ': ns :: [Nat]) = N n ': WrapDims ns
WrapDims (xns :: [XNat]) = xns
type family UnwrapDims (xns::[k]) :: [Nat] where
UnwrapDims ('[] :: [Nat]) = '[]
UnwrapDims ('[] :: [XNat]) = '[]
UnwrapDims (N x ': xs) = x ': UnwrapDims xs
UnwrapDims (XN _ ': _) = TypeError (
'Text "Cannot unwrap dimension XN into Nat"
':$$: 'Text "(dimension is not known at compile time)"
)
type family ConsDim (x :: l) (xs :: [k]) = (ys :: [k]) | ys -> x xs l where
ConsDim (x :: Nat) (xs :: [Nat]) = x ': xs
ConsDim (x :: Nat) (xs :: [XNat]) = N x ': xs
ConsDim (XN m) (xs :: [XNat]) = XN m ': xs
type family NatKind ks k :: Constraint where
NatKind [Nat] l = l ~ Nat
NatKind [XNat] Nat = ()
NatKind [XNat] XNat = ()
NatKind ks k = ks ~ [k]
type family FixedDim (xns :: [XNat]) (ns :: [Nat]) :: [Nat] where
FixedDim '[] _ = '[]
FixedDim (N n ': xs) ns = n ': FixedDim xs (Tail ns)
FixedDim (XN _ ': xs) ns = Head ns ': FixedDim xs (Tail ns)
type family FixedXDim (xns :: [XNat]) (ns :: [Nat]) :: [XNat] where
FixedXDim _ '[] = '[]
FixedXDim xs (n ': ns) = WrapNat (Head xs) n ': FixedXDim (Tail xs) ns
type family WrapNat (xn :: XNat) (n :: Nat) :: XNat where
WrapNat (XN m) n = XN m
WrapNat _ n = N n
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 >:
inferDimensions :: forall (ds :: [Nat])
. (KnownDims ds, FiniteList ds)
=> Evidence (Dimensions ds)
inferDimensions = case tList @Nat @ds of
TLEmpty -> Evidence
TLCons _ (_ :: TypeList ds') -> case inferDimensions @ds' of
Evidence -> Evidence
inferDimKnownDims :: forall (ds :: [Nat])
. Dimensions ds
=> Evidence (KnownDims ds)
inferDimKnownDims = inferDimKnownDims' (dim @ds)
where
inferDimKnownDims' :: forall (ns :: [Nat]) . Dim ns -> Evidence (KnownDims ns)
inferDimKnownDims' D = Evidence
inferDimKnownDims' (Dn :* ds) = case inferDimKnownDims' ds of Evidence -> Evidence
inferDimFiniteList :: forall (ds :: [Nat])
. Dimensions ds
=> Evidence (FiniteList ds)
inferDimFiniteList = inferDimFiniteList' (dim @ds)
where
inferDimFiniteList' :: forall (ns :: [Nat]) . Dim ns -> Evidence (FiniteList ns)
inferDimFiniteList' D = Evidence
inferDimFiniteList' (Dn :* ds) = case inferDimFiniteList' ds of Evidence -> Evidence
inferTailDimensions :: forall (ds :: [Nat])
. Dimensions ds
=> Maybe (Evidence (Dimensions (Tail ds)))
inferTailDimensions = case dim @ds of
D -> Nothing
Dn :* ds' -> Just $ reifyDimensions ds'
inferConcatDimensions :: forall as bs
. (Dimensions as, Dimensions bs)
=> Evidence (Dimensions (as ++ bs))
inferConcatDimensions = reifyDimensions $ magic (dim @as) (unsafeCoerce# $ dim @bs)
where
magic :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim ys
magic D ys = ys
magic xs D = unsafeCoerce# xs
magic (x :* xs) ys = unsafeCoerce# $ x :* magic xs ys
inferPrefixDimensions :: forall bs asbs
. (IsSuffix bs asbs ~ 'True, Dimensions bs, Dimensions asbs)
=> Evidence (Dimensions (Prefix bs asbs))
inferPrefixDimensions = reifyDimensions $ magic (len dasbs len (dim @bs)) (unsafeCoerce# dasbs)
where
dasbs = dim @asbs
len :: forall (ns :: [Nat]) . Dim ns -> Int
len D = 0
len (_ :* ds) = 1 + len ds
magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim ns
magic _ D = D
magic 0 _ = unsafeCoerce# D
magic n (d :* ds) = d :* magic (n1) ds
inferSuffixDimensions :: forall as asbs
. (IsPrefix as asbs ~ 'True, Dimensions as, Dimensions asbs)
=> Evidence (Dimensions (Suffix as asbs))
inferSuffixDimensions = reifyDimensions $ magic (dim @as) (unsafeCoerce# $ dim @asbs)
where
magic :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim ys
magic D ys = ys
magic _ D = D
magic (_ :* xs) (_ :* ys) = unsafeCoerce# $ magic xs ys
inferSnocDimensions :: forall xs z
. (KnownDim z, Dimensions xs)
=> Evidence (Dimensions (xs +: z))
inferSnocDimensions = reifyDimensions $ magic (dim @xs)
where
magic :: forall (ns :: [Nat]) . Dim ns -> Dim (ns +: z)
magic D = Dn :* D
magic (d :* ds) = unsafeCoerce# (d :* magic ds)
inferUnSnocDimensions :: forall ds
. Dimensions ds
=> Maybe (Evidence (SnocDimensions ds))
inferUnSnocDimensions = case dim @ds of
D -> Nothing
ds -> Just $ case magic ds of
(ys, Dn) -> case unsafeSnocDims' @ds of
Evidence -> case reifyDimensions @(Init ds) (unsafeCoerce# ys) of
Evidence -> Evidence
where
magic :: forall (ns :: [Nat]) . Dim ns -> (Dim ns, Dim (Last ns))
magic D = (D, undefined)
magic (d :* D) = (unsafeCoerce# D, d)
magic (d :* ds) = case magic ds of
(ds', z) -> (d :* ds', unsafeCoerce# z)
inferUnConsDimensions :: forall ds
. Dimensions ds
=> Maybe (Evidence (ConsDimensions ds))
inferUnConsDimensions = case dim @ds of
D -> Nothing
Dn :* ds' -> Just $ case reifyDimensions ds' +!+ unsafeConsDims' @ds of
Evidence -> Evidence
type SnocDimensions (xs :: [Nat]) =
( xs ~ (Init xs +: Last xs)
, xs ~ (Init xs ++ '[Last xs])
, IsPrefix (Init xs) xs ~ 'True
, IsSuffix '[Last xs] xs ~ 'True
, Suffix (Init xs) xs ~ '[Last xs]
, Prefix '[Last xs] xs ~ Init xs
, Dimensions (Init xs)
, KnownDim (Last xs)
)
type ConsDimensions (xs :: [Nat]) =
( xs ~ ( Head xs :+ Tail xs)
, xs ~ ('[Head xs] ++ Tail xs)
, IsPrefix '[Head xs] xs ~ 'True
, IsSuffix (Tail xs) xs ~ 'True
, Suffix '[Head xs] xs ~ Tail xs
, Prefix (Tail xs) xs ~ '[Head xs]
, Dimensions (Tail xs)
, KnownDim (Head xs)
)
unsafeSnocDims' :: forall (xs :: [Nat]) . Evidence
( xs ~ (Init xs +: Last xs)
, xs ~ (Init xs ++ '[Last xs])
, IsPrefix (Init xs) xs ~ 'True
, IsSuffix '[Last xs] xs ~ 'True
, Suffix (Init xs) xs ~ '[Last xs]
, Prefix '[Last xs] xs ~ Init xs
)
unsafeSnocDims' = case unsafeEqEvidence @xs @(Init xs +: Last xs)
+!+ unsafeEqEvidence @xs @(Init xs ++ '[Last xs])
+!+ unsafeEqEvidence @(IsPrefix (Init xs) xs) @'True
+!+ unsafeEqEvidence @(IsSuffix '[Last xs] xs) @'True
+!+ unsafeEqEvidence @(Suffix (Init xs) xs) @'[Last xs]
+!+ unsafeEqEvidence @(Prefix '[Last xs] xs) @(Init xs) of
Evidence -> Evidence
unsafeConsDims' :: forall (xs :: [Nat]) . Evidence
( xs ~ ( Head xs :+ Tail xs)
, xs ~ ('[Head xs] ++ Tail xs)
, IsPrefix '[Head xs] xs ~ 'True
, IsSuffix (Tail xs) xs ~ 'True
, Suffix '[Head xs] xs ~ Tail xs
, Prefix (Tail xs) xs ~ '[Head xs]
)
unsafeConsDims' = case unsafeEqEvidence @xs @( Head xs :+ Tail xs)
+!+ unsafeEqEvidence @xs @('[Head xs] ++ Tail xs)
+!+ unsafeEqEvidence @(IsPrefix '[Head xs] xs) @'True
+!+ unsafeEqEvidence @(IsSuffix (Tail xs) xs) @'True
+!+ unsafeEqEvidence @(Suffix '[Head xs] xs) @(Tail xs)
+!+ unsafeEqEvidence @(Prefix (Tail xs) xs) @'[Head xs] of
Evidence -> Evidence
inferInitDimensions :: forall xs
. Dimensions xs
=> Maybe (Evidence (Dimensions (Init xs)))
inferInitDimensions = case dim @xs of
D -> Nothing
ds -> Just . reifyDimensions $ magic (unsafeCoerce# ds)
where
magic :: forall (ns :: [Nat]) . Dim ns -> Dim ns
magic D = D
magic (_ :* D) = unsafeCoerce# D
magic (d :* ds) = d :* magic ds
inferTakeNDimensions :: forall n xs
. (KnownDim n, Dimensions xs)
=> Evidence (Dimensions (Take n xs))
inferTakeNDimensions = reifyDimensions $ magic (dimVal' @n) (dim @xs)
where
magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim (Take n ns)
magic _ D = D
magic 0 _ = unsafeCoerce# D
magic n (d :* ds) = unsafeCoerce# $ d :* (unsafeCoerce# $ magic (n1) ds :: Dim (Tail ns))
inferDropNDimensions :: forall n xs
. (KnownDim n, Dimensions xs)
=> Evidence (Dimensions (Drop n xs))
inferDropNDimensions = reifyDimensions $ magic (dimVal' @n) (dim @xs)
where
magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim (Drop n ns)
magic _ D = D
magic 0 ds = unsafeCoerce# ds
magic n (_ :* ds) = unsafeCoerce# $ magic (n1) ds
inferReverseDimensions :: forall xs . Dimensions xs => Evidence (Dimensions (Reverse xs))
inferReverseDimensions = reifyDimensions $ magic (dim @xs) (unsafeCoerce# D)
where
magic :: forall (ns :: [Nat]) . Dim ns -> Dim (Reverse ns) -> Dim (Reverse ns)
magic D xs = xs
magic (p:*sx) xs = magic (unsafeCoerce# sx :: Dim ns)
(unsafeCoerce# (p:*xs) :: Dim (Reverse ns))
reifyDimensions :: forall (ds :: [Nat]) . Dim ds -> Evidence (Dimensions ds)
reifyDimensions ds = reifyDims ds Evidence
reifyDims :: forall r (ds :: [Nat]) . Dim ds -> ( Dimensions ds => r) -> r
reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds
newtype MagicDims ds r = MagicDims (Dimensions ds => r)
unsafeEqEvidence :: forall x y . Evidence (x ~ y)
unsafeEqEvidence = case (unsafeCoerce# Refl :: x :~: y) of Refl -> Evidence