{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# 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
{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
module Numeric.Dimensions.Dim
(
Nat, XNat (..), XN, N
, DimType (..), KnownDimType(..), DimKind (..), KnownDimKind(..)
, 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 (..), withKnownXDim
, BoundedDim (..), minimalDim, ExactDim, FixedDim
, dimVal, dimVal', typeableDim, someDimVal
, sameDim, sameDim'
, lessOrEqDim, lessOrEqDim'
, compareDim, compareDim'
, constrainBy, relax
, plusDim, minusDim, minusDimM, timesDim, powerDim, divDim, modDim, log2Dim
, minDim, maxDim
, CmpNat, SOrdering (..), type (+), type (-), type (*), type (^), type (<=)
, Min, Max
, Dims, SomeDims (..), Dimensions (..), withKnownXDims
, BoundedDims (..), DimsBound, minimalDims
, ExactDims, FixedDims, inferFixedDims, inferExactFixedDims
, TypedList ( Dims, XDims, KnownDims
, U, (:*), Empty, TypeList, Cons, Snoc, Reverse)
, typeableDims, inferTypeableDims
, listDims, someDimsVal, totalDim, totalDim'
, sameDims, sameDims'
, inSpaceOf
, stripPrefixDims, stripSuffixDims
, RepresentableList (..), TypeList, types
, order, order'
, KindOf, KindOfEl
#if !(defined(__HADDOCK__) || defined(__HADDOCK_VERSION__))
, incohInstBoundedDims
#endif
) where
import Data.Bits (countLeadingZeros, finiteBitSize)
import Data.Coerce
import Data.Constraint
import Data.Constraint.Bare
import Data.Constraint.Deriving
import Data.Data hiding (TypeRep, typeRep,
typeRepTyCon)
import Data.Kind (Type)
import qualified Data.List (stripPrefix)
import Data.Type.List
import Data.Type.List.Internal
import Data.Type.Lits
import GHC.Exts (Proxy#, RuntimeRep, TYPE, proxy#)
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
import Unsafe.Coerce (unsafeCoerce)
data XNat = XN Nat | N Nat
type XN = 'XN
type N = 'N
data DimType (d :: k) where
DimTNat :: DimType (n :: Nat)
DimTXNatN :: DimType (N n)
DimTXNatX :: DimType (XN m)
data DimKind (k :: Type) where
DimKNat :: DimKind Nat
DimKXNat :: DimKind XNat
class KnownDimType d where
dimType :: DimType d
class KnownDimKind k where
dimKind :: DimKind k
instance KnownDimType (n :: Nat) where
dimType = DimTNat
{-# INLINE dimType #-}
instance KnownDimType ('N n :: XNat) where
dimType = DimTXNatN
{-# INLINE dimType #-}
instance KnownDimType ('XN n :: XNat) where
dimType = DimTXNatX
{-# INLINE dimType #-}
instance KnownDimKind Nat where
dimKind = DimKNat
{-# INLINE dimKind #-}
instance KnownDimKind XNat where
dimKind = DimKXNat
{-# INLINE dimKind #-}
instance Class (KnownDimKind k) (KnownDimType (n :: k)) where
cls = Sub $ case dimType @n of
DimTNat -> Dict
DimTXNatN -> Dict
DimTXNatX -> Dict
newtype Dim (x :: k) = DimSing Word
deriving ( Typeable )
type SomeDim = Dim (XN 0)
type Dims = (TypedList Dim :: [k] -> Type)
#define PLEASE_STYLISH_HASKELL \
forall d . KnownDimType d => \
(KindOf d ~ Nat, KnownDim d) => \
Dim d
pattern D :: PLEASE_STYLISH_HASKELL
pattern D <- (patDim (dimType @d) -> PatNat)
where
D = dim @d
#undef PLEASE_STYLISH_HASKELL
#define PLEASE_STYLISH_HASKELL \
forall d . KnownDimType d => \
forall (n :: Nat) . (KindOf d ~ XNat, d ~ N n) => \
Dim n -> Dim d
pattern Dn :: PLEASE_STYLISH_HASKELL
pattern Dn k <- (patDim (dimType @d) -> PatXNatN k)
where
Dn k = coerce k
#undef PLEASE_STYLISH_HASKELL
#define PLEASE_STYLISH_HASKELL \
forall d . KnownDimType d => \
forall (m :: Nat) (n :: Nat) . (KindOf d ~ XNat, d ~ XN m, m <= n) => \
Dim n -> Dim d
pattern Dx :: PLEASE_STYLISH_HASKELL
pattern Dx k <- (patDim (dimType @d) -> PatXNatX k)
where
Dx k = coerce k
#undef PLEASE_STYLISH_HASKELL
{-# COMPLETE D #-}
{-# COMPLETE Dn, Dx #-}
{-# COMPLETE D, Dn, Dx #-}
class KnownDim n where
dim :: Dim n
class (KnownDimKind (KindOf d), KnownDimType d, KnownDim (DimBound d))
=> BoundedDim d where
type family DimBound d :: Nat
dimBound :: Dim (DimBound d)
constrainDim :: forall y . Dim y -> Maybe (Dim d)
minimalDim :: forall n . BoundedDim n => Dim n
minimalDim = coerce (dimBound @n)
{-# INLINE minimalDim #-}
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 #-}
dimVal :: forall x . Dim x -> Word
dimVal = coerce
{-# INLINE dimVal #-}
dimVal' :: forall n . 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
type family ExactDim (d :: k) :: Constraint where
ExactDim (_ :: Nat) = ()
ExactDim (x :: XNat) = (x ~ N (DimBound x))
instance 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 KnownDim n => KnownDim (N n) where
{-# INLINE dim #-}
dim = coerce (dim @n)
withKnownXDim :: forall (d :: XNat) (rep :: RuntimeRep) (r :: TYPE rep)
. KnownDim d
=> ( (KnownDim (DimBound d), ExactDim d
, KnownDimType d, FixedDim d (DimBound d)) => r)
-> r
withKnownXDim
| Dict <- unsafeEqTypes @d @(N (DimBound d))
= reifyDim @Nat @(DimBound d) (coerce (dim @d))
{-# INLINE withKnownXDim #-}
instance Class (KnownNat n) (KnownDim n) where
cls = Sub $ reifyNat @_ @n (fromIntegral $ dimVal' @n) Dict
someDimVal :: Word -> SomeDim
someDimVal = coerce
{-# INLINE someDimVal #-}
constrainBy :: forall x p y
. BoundedDim x => p x -> Dim y -> Maybe (Dim x)
constrainBy = const (constrainDim @x @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 (unsafeEqTypes @x @y)
| otherwise = Nothing
{-# INLINE sameDim #-}
sameDim' :: forall (x :: Nat) (y :: Nat)
. (KnownDim x, KnownDim y) => Maybe (Dict (x ~ y))
sameDim' = sameDim (dim @x) (dim @y)
{-# INLINE sameDim' #-}
lessOrEqDim :: forall (x :: Nat) (y :: Nat)
. Dim x -> Dim y -> Maybe (Dict (x <= y))
lessOrEqDim a b = case compareDim a b of
SLT -> Just Dict
SEQ -> Just Dict
SGT -> Nothing
{-# INLINE lessOrEqDim #-}
lessOrEqDim' :: forall (x :: Nat) (y :: Nat)
. (KnownDim x, KnownDim y) => Maybe (Dict (x <= y))
lessOrEqDim' = lessOrEqDim (dim @x) (dim @y)
{-# INLINE lessOrEqDim' #-}
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)
. (KnownDim a, KnownDim b) => SOrdering (CmpNat a b)
compareDim' = 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
minDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Min n m)
minDim = coerce (min :: Word -> Word -> Word)
maxDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Max n m)
maxDim = coerce (max :: Word -> Word -> Word)
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
#define PLEASE_STYLISH_HASKELL \
forall ds . KnownDimKind (KindOfEl ds) => \
(KindOfEl ds ~ Nat, Dimensions ds) => \
Dims ds
pattern Dims :: PLEASE_STYLISH_HASKELL
pattern Dims <- (patDims (dimKind @(KindOfEl ds)) -> PatNats)
where
Dims = dims @ds
#undef PLEASE_STYLISH_HASKELL
#define PLEASE_STYLISH_HASKELL \
forall ds . KnownDimKind (KindOfEl ds) => \
forall (ns :: [Nat]) . (KindOfEl ds ~ XNat, FixedDims ds ns) => \
Dims ns -> Dims ds
pattern XDims :: PLEASE_STYLISH_HASKELL
pattern XDims ns <- (patDims (dimKind @(KindOfEl ds)) -> PatXNats ns)
where
XDims = unsafeCastTL
#undef PLEASE_STYLISH_HASKELL
{-# COMPLETE Dims #-}
{-# COMPLETE XDims #-}
{-# COMPLETE Dims, XDims #-}
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 #-}
data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)
class Dimensions ds 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 #-}
withKnownXDims :: forall (ds :: [XNat]) (rep :: RuntimeRep) (r :: TYPE rep)
. Dimensions ds
=> (( Dimensions (DimsBound ds), ExactDims ds
, All KnownDimType ds, FixedDims ds (DimsBound ds)) => r)
-> r
withKnownXDims f
| Dict <- unsafeEqTypes @ds @(Map 'N (DimsBound ds))
= reifyDims @Nat @(DimsBound ds) dsN
(withBareConstraint (dictToBare (inferExactFixedDims @ds dsN)) (\_ -> f) ())
where
dsN :: Dims (DimsBound ds)
dsN = unsafeCastTL (dims @ds)
{-# INLINE withKnownXDims #-}
type family DimsBound (ds :: [k]) :: [Nat] where
DimsBound (ns :: [Nat]) = ns
DimsBound ('[] :: [XNat]) = '[]
DimsBound (n ': ns) = DimBound n ': DimsBound ns
type family ExactDims (d :: [k]) :: Constraint where
ExactDims (_ :: [Nat]) = ()
ExactDims (xs :: [XNat]) = xs ~ Map 'N (DimsBound xs)
type family BoundedDimsTail (ds :: [k]) where
BoundedDimsTail '[] = UnreachableConstraint (BoundedDims (Tail '[]))
"BoundDimsTail '[] -- BoundedDims (Tail '[])"
BoundedDimsTail (_ ': ns) = BoundedDims ns
class ( KnownDimKind (KindOfEl ds), All BoundedDim ds, RepresentableList ds
, Dimensions (DimsBound ds), BoundedDimsTail ds)
=> BoundedDims ds where
dimsBound :: Dims (DimsBound ds)
constrainDims :: forall ys . Dims ys -> Maybe (Dims ds)
minimalDims :: forall ds . BoundedDims ds => Dims ds
minimalDims = unsafeCastTL (dimsBound @ds)
{-# ANN defineBoundedDims ClassDict #-}
defineBoundedDims ::
forall (k :: Type) (ds :: [k])
. ( KnownDimKind (KindOfEl ds), All BoundedDim ds, RepresentableList ds
, Dimensions (DimsBound ds), BoundedDimsTail ds)
=> Dims (DimsBound ds)
-> (forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds))
-> Dict (BoundedDims ds)
defineBoundedDims = defineBoundedDims
{-# ANN incohInstBoundedDims (ToInstance Incoherent) #-}
incohInstBoundedDims ::
forall (k :: Type) (ds :: [k])
. (Dimensions ds, KnownDimKind k) => Dict (BoundedDims ds)
incohInstBoundedDims
= incohInstBoundedDims' @k @ds dims (inferAllBoundedDims ds)
where
ds = dims @ds
incohInstBoundedDims' ::
forall (k :: Type) (ds :: [k])
. KnownDimKind k
=> Dims ds
-> Dict (All BoundedDim ds, RepresentableList ds)
-> Dict (BoundedDims ds)
incohInstBoundedDims' ds Dict = case dimsBound' of
Dims -> case ds of
U -> defineBoundedDims dimsBound' constrainDims'
_ :* ds'
| _ :* TypeList <- tList @ds
, Dict <- incohInstBoundedDims' ds' Dict
-> defineBoundedDims dimsBound' constrainDims'
_ -> error "incohInstBoundedDims': impossible pattern"
where
dimsBound' :: Dims (DimsBound ds)
dimsBound' = unsafeCastTL ds
constrainDims' :: forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds)
constrainDims' ys
| listDims ys == listDims dimsBound'
= Just (unsafeCastTL ys)
| otherwise = Nothing
#if defined(__HADDOCK__) || defined(__HADDOCK_VERSION__)
instance Dimensions ns => BoundedDims (ns :: [Nat]) where
dimsBound = undefined
constrainDims = undefined
#endif
instance BoundedDims ('[] :: [XNat]) where
dimsBound = U
constrainDims U = Just U
constrainDims (_ :* _) = Nothing
instance (BoundedDim n, BoundedDims ns) => BoundedDims ((n ': ns) :: [XNat]) where
dimsBound = dimBound @n :* dimsBound @ns
constrainDims U = Nothing
constrainDims (y :* ys) = (:*) <$> constrainDim y <*> constrainDims ys
typeableDims :: forall (ds :: [Nat]) . Typeable ds => Dims ds
typeableDims = case typeRep @ds of
App (App _ (tx :: TypeRep (n :: k1))) (txs :: TypeRep (ns :: k2))
| Dict <- unsafeEqTypes @k1 @Nat
, Dict <- unsafeEqTypes @k2 @[Nat]
, Dict <- unsafeEqTypes @ds @(n ': ns)
-> 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 xs . Dims xs -> [Word]
listDims = unsafeCoerce
{-# INLINE listDims #-}
someDimsVal :: [Word] -> SomeDims
someDimsVal = SomeDims . unsafeCoerce
{-# INLINE someDimsVal #-}
totalDim :: forall xs . Dims xs -> Word
totalDim = product . listDims
{-# INLINE totalDim #-}
totalDim' :: forall xs . Dimensions xs => Word
totalDim' = totalDim (dims @xs)
{-# INLINE totalDim' #-}
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 (unsafeEqTypes @as @bs)
| 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 ds p q
. p ds -> q ds -> p ds
inSpaceOf = const
{-# INLINE inSpaceOf #-}
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))
inferFixedDims :: forall (xns :: [XNat]) (ns :: [Nat])
. All KnownDimType xns
=> Dims xns -> Dims ns -> Maybe (Dict (FixedDims xns ns))
inferFixedDims U U = Just Dict
inferFixedDims (Dx (a :: Dim n) :* xns) (b :* ns)
| Dict <- unsafeEqTypes @n @(DimBound (Head xns))
, Just Dict <- lessOrEqDim a b
, Just Dict <- inferFixedDims xns ns
= Just Dict
inferFixedDims (Dn a :* xns) (b :* ns)
| Just Dict <- sameDim a b
, Just Dict <- inferFixedDims xns ns
= Just Dict
inferFixedDims _ _ = Nothing
unsafeInferFixedDims :: forall (xns :: [XNat]) (ns :: [Nat])
. Dims ns -> Dict (FixedDims xns ns)
unsafeInferFixedDims U
| Dict <- unsafeEqTypes @xns @'[] = Dict
unsafeInferFixedDims ((D :: Dim n) :* ns)
| Dict <- unsafeEqTypes @xns @(N n ': Tail xns)
, Dict <- unsafeInferFixedDims @(Tail xns) ns = Dict
{-# INLINE unsafeInferFixedDims #-}
inferExactFixedDims :: forall (ds :: [XNat]) . ExactDims ds
=> Dims (DimsBound ds)
-> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
inferExactFixedDims U = Dict
inferExactFixedDims (_ :* ns)
| Dict <- inferExactFixedDims @(Tail ds) ns = Dict
{-# INLINE inferExactFixedDims #-}
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 @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 @x @(XN 0) . DimSing
-> return d
_ -> Read.pfail
readList = Read.readListDefault
readListPrec = Read.readListPrecDefault
instance BoundedDims xs => Read (Dims (xs :: [k])) where
readPrec = typedListReadPrec @BoundedDim ":*" Read.readPrec (tList @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 @Dim @SomeDims
(\g -> (\(Dx d) -> g d) <$> Read.readPrec @(Dim (XN 0)))
SomeDims
reifyDim :: forall (k :: Type) (d :: k) (rep :: RuntimeRep) (r :: TYPE rep)
. Dim d -> (KnownDim d => r) -> r
reifyDim d k = unsafeCoerce (MagicDim k :: MagicDim d r) d
{-# INLINE reifyDim #-}
newtype MagicDim (d :: k) (r :: TYPE rep) = 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)
reifyDims :: forall (k :: Type) (ds :: [k]) (rep :: RuntimeRep) (r :: TYPE rep)
. Dims ds -> (Dimensions ds => r) -> r
reifyDims ds k = unsafeCoerce (MagicDims k :: MagicDims ds r) ds
{-# INLINE reifyDims #-}
newtype MagicDims (ds :: [k]) (r :: TYPE rep) = MagicDims (Dimensions ds => r)
data PatDim (d :: k) where
PatNat :: KnownDim n => PatDim (n :: Nat)
PatXNatN :: Dim n -> PatDim (N n)
PatXNatX :: (m <= n) => Dim n -> PatDim (XN m)
patDim :: forall (k :: Type) (d :: k) . DimType d -> Dim d -> PatDim d
patDim DimTNat d = reifyDim d PatNat
patDim DimTXNatN d = PatXNatN (coerce d)
patDim DimTXNatX d = f (coerce d) d
where
f :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim (XN m) -> PatDim (XN m)
f n = case unsafeCoerceDict @(m <= m) @(m <= n) Dict of
Dict -> const (PatXNatX n)
{-# INLINE patDim #-}
data PatDims (ds :: [k]) where
PatNats :: Dimensions ds => PatDims (ds :: [Nat])
PatXNats :: FixedDims ds ns => Dims ns -> PatDims (ds :: [XNat])
patDims :: forall (k :: Type) (ds :: [k]) . DimKind k -> Dims ds -> PatDims ds
patDims DimKNat ds = reifyDims ds PatNats
patDims DimKXNat ds = withBareConstraint
(dictToBare (unsafeInferFixedDims @ds ds')) (PatXNats ds')
where
ds' = unsafeCastTL ds
{-# INLINE patDims #-}
inferAllBoundedDims :: forall (k :: Type) (ds :: [k])
. (Dimensions ds, KnownDimKind k)
=> Dims ds -> Dict (All BoundedDim ds, RepresentableList ds)
inferAllBoundedDims = go
where
reifyBoundedDim :: forall (d :: k) . Dim d -> Dict (BoundedDim d)
reifyBoundedDim = case dimKind @k of
DimKNat -> \d -> reifyDim d Dict
DimKXNat
| Dict <- unsafeEqTypes @d @(N (DimBound d))
-> \d -> reifyDim (coerce d :: Dim (DimBound d)) Dict
go :: forall (xs :: [k]) . Dims xs
-> Dict (All BoundedDim xs, RepresentableList xs)
go U = Dict
go (d :* ds)
| Dict <- reifyBoundedDim d
, Dict <- go ds = Dict
{-# INLINE inferAllBoundedDims #-}
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
unsafeCastTL :: TypedList f (xs :: [k]) -> TypedList g (ys :: [l])
unsafeCastTL = unsafeCoerce