{-# 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
{-# 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#, type (~~))
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)
#define IS_UNSOUND_MATCHING_810_900 (MIN_VERSION_GLASGOW_HASKELL(8,10,0,0) && !MIN_VERSION_GLASGOW_HASKELL(9,1,0,0))
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 :: DimType n
dimType = DimType n
forall (n :: Nat). DimType n
DimTNat
{-# INLINE dimType #-}
instance KnownDimType ('N n :: XNat) where
dimType :: DimType ('N n)
dimType = DimType ('N n)
forall (n :: Nat). DimType ('N n)
DimTXNatN
{-# INLINE dimType #-}
instance KnownDimType ('XN n :: XNat) where
dimType :: DimType ('XN n)
dimType = DimType ('XN n)
forall (n :: Nat). DimType ('XN n)
DimTXNatX
{-# INLINE dimType #-}
instance KnownDimKind Nat where
dimKind :: DimKind Nat
dimKind = DimKind Nat
DimKNat
{-# INLINE dimKind #-}
instance KnownDimKind XNat where
dimKind :: DimKind XNat
dimKind = DimKind XNat
DimKXNat
{-# INLINE dimKind #-}
instance Class (KnownDimKind k) (KnownDimType (n :: k)) where
cls :: KnownDimType n :- KnownDimKind k
cls = (KnownDimType n => Dict (KnownDimKind k))
-> KnownDimType n :- KnownDimKind k
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownDimType n => Dict (KnownDimKind k))
-> KnownDimType n :- KnownDimKind k)
-> (KnownDimType n => Dict (KnownDimKind k))
-> KnownDimType n :- KnownDimKind k
forall a b. (a -> b) -> a -> b
$ case KnownDimType n => DimType n
forall k (d :: k). KnownDimType d => DimType d
dimType @n of
DimType n
DimTNat -> Dict (KnownDimKind k)
forall (a :: Constraint). a => Dict a
Dict
DimType n
DimTXNatN -> Dict (KnownDimKind k)
forall (a :: Constraint). a => Dict a
Dict
DimType n
DimTXNatX -> Dict (KnownDimKind k)
forall (a :: Constraint). a => Dict a
Dict
newtype Dim (x :: k) = DimSing Word
deriving ( Typeable )
type role Dim nominal
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 $bD :: Dim d
$mD :: forall r k (d :: k).
KnownDimType d =>
Dim d -> ((k ~ Nat, KnownDim d) => r) -> (Void# -> r) -> r
D <- (patDim (dimType @d) -> PatNat)
where
D = KnownDim d => Dim d
forall k (n :: k). KnownDim n => Dim n
dim @d
#undef PLEASE_STYLISH_HASKELL
#define PLEASE_STYLISH_HASKELL \
forall d . KnownDimType d => \
forall (n :: Nat) . (d ~~ N n) => \
Dim n -> Dim d
pattern Dn :: PLEASE_STYLISH_HASKELL
pattern $bDn :: Dim n -> Dim d
$mDn :: forall r k (d :: k).
KnownDimType d =>
Dim d
-> (forall (n :: Nat). (d ~~ N n) => Dim n -> r)
-> (Void# -> r)
-> r
Dn k <- (patDim (dimType @d) -> PatXNatN k)
where
Dn Dim n
k = Dim n -> Dim d
coerce Dim n
k
#undef PLEASE_STYLISH_HASKELL
#define PLEASE_STYLISH_HASKELL \
forall d . KnownDimType d => \
forall (m :: Nat) (n :: Nat) . (d ~~ XN m, m <= n) => \
Dim n -> Dim d
pattern Dx :: PLEASE_STYLISH_HASKELL
pattern $bDx :: Dim n -> Dim d
$mDx :: forall r k (d :: k).
KnownDimType d =>
Dim d
-> (forall (m :: Nat) (n :: Nat).
(d ~~ XN m, m <= n) =>
Dim n -> r)
-> (Void# -> r)
-> r
Dx k <- (patDim (dimType @d) -> PatXNatX k)
where
Dx Dim n
k = Dim n -> Dim d
coerce Dim n
k
#undef PLEASE_STYLISH_HASKELL
#if !IS_UNSOUND_MATCHING_810_900
{-# COMPLETE D #-}
{-# COMPLETE Dn, Dx #-}
#endif
{-# 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 :: Dim n
minimalDim = Dim (DimBound n) -> Dim n
coerce (BoundedDim n => Dim (DimBound n)
forall k (d :: k). BoundedDim d => Dim (DimBound d)
dimBound @n)
{-# INLINE minimalDim #-}
instance KnownDim n => BoundedDim (n :: Nat) where
type DimBound n = n
dimBound :: Dim (DimBound n)
dimBound = KnownDim n => Dim n
forall k (n :: k). KnownDim n => Dim n
dim @n
{-# INLINE dimBound #-}
constrainDim :: Dim y -> Maybe (Dim n)
constrainDim (DimSing Word
y)
| KnownDim n => Word
forall k (n :: k). KnownDim n => Word
dimVal' @n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
y = Dim n -> Maybe (Dim n)
forall a. a -> Maybe a
Just (Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
y)
| Bool
otherwise = Maybe (Dim n)
forall a. Maybe a
Nothing
{-# INLINE constrainDim #-}
instance KnownDim n => BoundedDim (N n) where
type DimBound (N n) = n
dimBound :: Dim (DimBound (N n))
dimBound = KnownDim n => Dim n
forall k (n :: k). KnownDim n => Dim n
dim @n
{-# INLINE dimBound #-}
constrainDim :: Dim y -> Maybe (Dim (N n))
constrainDim (DimSing Word
y)
| KnownDim n => Word
forall k (n :: k). KnownDim n => Word
dimVal' @n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
y = Dim (N n) -> Maybe (Dim (N n))
forall a. a -> Maybe a
Just (Word -> Dim (N n)
forall k (x :: k). Word -> Dim x
DimSing Word
y)
| Bool
otherwise = Maybe (Dim (N n))
forall a. Maybe a
Nothing
{-# INLINE constrainDim #-}
instance KnownDim m => BoundedDim (XN m) where
type DimBound ('XN m) = m
dimBound :: Dim (DimBound (XN m))
dimBound = KnownDim m => Dim m
forall k (n :: k). KnownDim n => Dim n
dim @m
{-# INLINE dimBound #-}
constrainDim :: Dim y -> Maybe (Dim (XN m))
constrainDim (DimSing Word
y)
| KnownDim m => Word
forall k (n :: k). KnownDim n => Word
dimVal' @m Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
<= Word
y = Dim (XN m) -> Maybe (Dim (XN m))
forall a. a -> Maybe a
Just (Word -> Dim (XN m)
forall k (x :: k). Word -> Dim x
DimSing Word
y)
| Bool
otherwise = Maybe (Dim (XN m))
forall a. Maybe a
Nothing
{-# INLINE constrainDim #-}
dimVal :: forall x . Dim x -> Word
dimVal :: Dim x -> Word
dimVal = Dim x -> Word
coerce
{-# INLINE dimVal #-}
dimVal' :: forall n . KnownDim n => Word
dimVal' :: Word
dimVal' = Dim n -> Word
coerce (KnownDim n => Dim n
forall k (n :: k). KnownDim n => Dim n
dim @n)
{-# INLINE dimVal' #-}
typeableDim :: forall (n :: Nat) . Typeable n => Dim n
typeableDim :: Dim n
typeableDim = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing (Word -> Dim n) -> (TypeRep n -> Word) -> TypeRep n -> Dim n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Word
forall a. Read a => String -> a
read (String -> Word) -> (TypeRep n -> String) -> TypeRep n -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> String
tyConName (TyCon -> String) -> (TypeRep n -> TyCon) -> TypeRep n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep n -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon (TypeRep n -> Dim n) -> TypeRep n -> Dim n
forall a b. (a -> b) -> a -> b
$ Typeable n => TypeRep n
forall k (a :: k). Typeable a => TypeRep a
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 :: Dim n
dim = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing (Natural -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy# n -> Natural
forall (n :: Nat). KnownNat n => Proxy# n -> Natural
natVal' (Proxy# n
forall k (a :: k). Proxy# a
proxy# :: Proxy# n)))
instance {-# OVERLAPPING #-} KnownDim 0 where
{ {-# INLINE dim #-}; dim :: Dim 0
dim = Word -> Dim 0
forall k (x :: k). Word -> Dim x
DimSing Word
0 }
instance {-# OVERLAPPING #-} KnownDim 1 where
{ {-# INLINE dim #-}; dim :: Dim 1
dim = Word -> Dim 1
forall k (x :: k). Word -> Dim x
DimSing Word
1 }
instance {-# OVERLAPPING #-} KnownDim 2 where
{ {-# INLINE dim #-}; dim :: Dim 2
dim = Word -> Dim 2
forall k (x :: k). Word -> Dim x
DimSing Word
2 }
instance {-# OVERLAPPING #-} KnownDim 3 where
{ {-# INLINE dim #-}; dim :: Dim 3
dim = Word -> Dim 3
forall k (x :: k). Word -> Dim x
DimSing Word
3 }
instance {-# OVERLAPPING #-} KnownDim 4 where
{ {-# INLINE dim #-}; dim :: Dim 4
dim = Word -> Dim 4
forall k (x :: k). Word -> Dim x
DimSing Word
4 }
instance {-# OVERLAPPING #-} KnownDim 5 where
{ {-# INLINE dim #-}; dim :: Dim 5
dim = Word -> Dim 5
forall k (x :: k). Word -> Dim x
DimSing Word
5 }
instance {-# OVERLAPPING #-} KnownDim 6 where
{ {-# INLINE dim #-}; dim :: Dim 6
dim = Word -> Dim 6
forall k (x :: k). Word -> Dim x
DimSing Word
6 }
instance {-# OVERLAPPING #-} KnownDim 7 where
{ {-# INLINE dim #-}; dim :: Dim 7
dim = Word -> Dim 7
forall k (x :: k). Word -> Dim x
DimSing Word
7 }
instance {-# OVERLAPPING #-} KnownDim 8 where
{ {-# INLINE dim #-}; dim :: Dim 8
dim = Word -> Dim 8
forall k (x :: k). Word -> Dim x
DimSing Word
8 }
instance {-# OVERLAPPING #-} KnownDim 9 where
{ {-# INLINE dim #-}; dim :: Dim 9
dim = Word -> Dim 9
forall k (x :: k). Word -> Dim x
DimSing Word
9 }
instance {-# OVERLAPPING #-} KnownDim 10 where
{ {-# INLINE dim #-}; dim :: Dim 10
dim = Word -> Dim 10
forall k (x :: k). Word -> Dim x
DimSing Word
10 }
instance {-# OVERLAPPING #-} KnownDim 11 where
{ {-# INLINE dim #-}; dim :: Dim 11
dim = Word -> Dim 11
forall k (x :: k). Word -> Dim x
DimSing Word
11 }
instance {-# OVERLAPPING #-} KnownDim 12 where
{ {-# INLINE dim #-}; dim :: Dim 12
dim = Word -> Dim 12
forall k (x :: k). Word -> Dim x
DimSing Word
12 }
instance {-# OVERLAPPING #-} KnownDim 13 where
{ {-# INLINE dim #-}; dim :: Dim 13
dim = Word -> Dim 13
forall k (x :: k). Word -> Dim x
DimSing Word
13 }
instance {-# OVERLAPPING #-} KnownDim 14 where
{ {-# INLINE dim #-}; dim :: Dim 14
dim = Word -> Dim 14
forall k (x :: k). Word -> Dim x
DimSing Word
14 }
instance {-# OVERLAPPING #-} KnownDim 15 where
{ {-# INLINE dim #-}; dim :: Dim 15
dim = Word -> Dim 15
forall k (x :: k). Word -> Dim x
DimSing Word
15 }
instance {-# OVERLAPPING #-} KnownDim 16 where
{ {-# INLINE dim #-}; dim :: Dim 16
dim = Word -> Dim 16
forall k (x :: k). Word -> Dim x
DimSing Word
16 }
instance {-# OVERLAPPING #-} KnownDim 17 where
{ {-# INLINE dim #-}; dim :: Dim 17
dim = Word -> Dim 17
forall k (x :: k). Word -> Dim x
DimSing Word
17 }
instance {-# OVERLAPPING #-} KnownDim 18 where
{ {-# INLINE dim #-}; dim :: Dim 18
dim = Word -> Dim 18
forall k (x :: k). Word -> Dim x
DimSing Word
18 }
instance {-# OVERLAPPING #-} KnownDim 19 where
{ {-# INLINE dim #-}; dim :: Dim 19
dim = Word -> Dim 19
forall k (x :: k). Word -> Dim x
DimSing Word
19 }
instance {-# OVERLAPPING #-} KnownDim 20 where
{ {-# INLINE dim #-}; dim :: Dim 20
dim = Word -> Dim 20
forall k (x :: k). Word -> Dim x
DimSing Word
20 }
instance {-# OVERLAPPING #-} KnownDim 21 where
{ {-# INLINE dim #-}; dim :: Dim 21
dim = Word -> Dim 21
forall k (x :: k). Word -> Dim x
DimSing Word
21 }
instance {-# OVERLAPPING #-} KnownDim 22 where
{ {-# INLINE dim #-}; dim :: Dim 22
dim = Word -> Dim 22
forall k (x :: k). Word -> Dim x
DimSing Word
22 }
instance {-# OVERLAPPING #-} KnownDim 23 where
{ {-# INLINE dim #-}; dim :: Dim 23
dim = Word -> Dim 23
forall k (x :: k). Word -> Dim x
DimSing Word
23 }
instance {-# OVERLAPPING #-} KnownDim 24 where
{ {-# INLINE dim #-}; dim :: Dim 24
dim = Word -> Dim 24
forall k (x :: k). Word -> Dim x
DimSing Word
24 }
instance {-# OVERLAPPING #-} KnownDim 25 where
{ {-# INLINE dim #-}; dim :: Dim 25
dim = Word -> Dim 25
forall k (x :: k). Word -> Dim x
DimSing Word
25 }
instance KnownDim n => KnownDim (N n) where
{-# INLINE dim #-}
dim :: Dim (N n)
dim = Dim n -> Dim (N n)
coerce (KnownDim n => Dim n
forall k (n :: k). KnownDim n => Dim n
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 :: ((KnownDim (DimBound d), ExactDim d, KnownDimType d,
FixedDim d (DimBound d)) =>
r)
-> r
withKnownXDim (KnownDim (DimBound d), ExactDim d, KnownDimType d,
FixedDim d (DimBound d)) =>
r
x
| Dict (d ~ N (DimBound d))
Dict <- Dict (d ~ N (DimBound d))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @d @(N (DimBound d))
= Dim (DimBound d) -> (KnownDim (DimBound d) => r) -> r
forall k (d :: k) r. Dim d -> (KnownDim d => r) -> r
reifyDim @Nat @(DimBound d) @rep @r (Dim d -> Dim (DimBound d)
coerce (KnownDim d => Dim d
forall k (n :: k). KnownDim n => Dim n
dim @d)) KnownDim (DimBound d) => r
(KnownDim (DimBound d), ExactDim d, KnownDimType d,
FixedDim d (DimBound d)) =>
r
x
{-# INLINE withKnownXDim #-}
instance Class (KnownNat n) (KnownDim n) where
cls :: KnownDim n :- KnownNat n
cls = (KnownDim n => Dict (KnownNat n)) -> KnownDim n :- KnownNat n
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownDim n => Dict (KnownNat n)) -> KnownDim n :- KnownNat n)
-> (KnownDim n => Dict (KnownNat n)) -> KnownDim n :- KnownNat n
forall a b. (a -> b) -> a -> b
$ Natural -> (KnownNat n => Dict (KnownNat n)) -> Dict (KnownNat n)
forall r (d :: Nat). Natural -> (KnownNat d => r) -> r
reifyNat @_ @n (Word -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Natural) -> Word -> Natural
forall a b. (a -> b) -> a -> b
$ KnownDim n => Word
forall k (n :: k). KnownDim n => Word
dimVal' @n) KnownNat n => Dict (KnownNat n)
forall (a :: Constraint). a => Dict a
Dict
someDimVal :: Word -> SomeDim
someDimVal :: Word -> SomeDim
someDimVal = Word -> SomeDim
coerce
{-# INLINE someDimVal #-}
constrainBy :: forall x p y
. BoundedDim x => p x -> Dim y -> Maybe (Dim x)
constrainBy :: p x -> Dim y -> Maybe (Dim x)
constrainBy = (Dim y -> Maybe (Dim x)) -> p x -> Dim y -> Maybe (Dim x)
forall a b. a -> b -> a
const (Dim y -> Maybe (Dim x)
forall k (d :: k) k (y :: k).
BoundedDim d =>
Dim y -> Maybe (Dim d)
constrainDim @x @y)
{-# INLINE constrainBy #-}
relax :: forall (m :: Nat) (n :: Nat) . (<=) m n => Dim (XN n) -> Dim (XN m)
relax :: Dim (XN n) -> Dim (XN m)
relax = Dim (XN n) -> Dim (XN m)
coerce
{-# INLINE relax #-}
sameDim :: forall (x :: Nat) (y :: Nat)
. Dim x -> Dim y -> Maybe (Dict (x ~ y))
sameDim :: Dim x -> Dim y -> Maybe (Dict (x ~ y))
sameDim (DimSing Word
a) (DimSing Word
b)
| Word
a Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
b = Dict (x ~ y) -> Maybe (Dict (x ~ y))
forall a. a -> Maybe a
Just (Dict (x ~ y)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @x @y)
| Bool
otherwise = Maybe (Dict (x ~ y))
forall a. Maybe a
Nothing
{-# INLINE sameDim #-}
sameDim' :: forall (x :: Nat) (y :: Nat)
. (KnownDim x, KnownDim y) => Maybe (Dict (x ~ y))
sameDim' :: Maybe (Dict (x ~ y))
sameDim' = Dim x -> Dim y -> Maybe (Dict (x ~ y))
forall (x :: Nat) (y :: Nat).
Dim x -> Dim y -> Maybe (Dict (x ~ y))
sameDim (KnownDim x => Dim x
forall k (n :: k). KnownDim n => Dim n
dim @x) (KnownDim y => Dim y
forall k (n :: k). KnownDim n => Dim n
dim @y)
{-# INLINE sameDim' #-}
lessOrEqDim :: forall (x :: Nat) (y :: Nat)
. Dim x -> Dim y -> Maybe (Dict (x <= y))
lessOrEqDim :: Dim x -> Dim y -> Maybe (Dict (x <= y))
lessOrEqDim Dim x
a Dim y
b = case Dim x -> Dim y -> SOrdering (CmpNat x y)
forall (a :: Nat) (b :: Nat).
Dim a -> Dim b -> SOrdering (CmpNat a b)
compareDim Dim x
a Dim y
b of
SOrdering (CmpNat x y)
SLT -> Dict ('LT ~ 'LT) -> Maybe (Dict ('LT ~ 'LT))
forall a. a -> Maybe a
Just Dict ('LT ~ 'LT)
forall (a :: Constraint). a => Dict a
Dict
SOrdering (CmpNat x y)
SEQ -> Dict ('EQ ~ 'EQ) -> Maybe (Dict ('EQ ~ 'EQ))
forall a. a -> Maybe a
Just Dict ('EQ ~ 'EQ)
forall (a :: Constraint). a => Dict a
Dict
SOrdering (CmpNat x y)
SGT -> Maybe (Dict (x <= y))
forall a. Maybe a
Nothing
{-# INLINE lessOrEqDim #-}
lessOrEqDim' :: forall (x :: Nat) (y :: Nat)
. (KnownDim x, KnownDim y) => Maybe (Dict (x <= y))
lessOrEqDim' :: Maybe (Dict (x <= y))
lessOrEqDim' = Dim x -> Dim y -> Maybe (Dict (x <= y))
forall (x :: Nat) (y :: Nat).
Dim x -> Dim y -> Maybe (Dict (x <= y))
lessOrEqDim (KnownDim x => Dim x
forall k (n :: k). KnownDim n => Dim n
dim @x) (KnownDim y => Dim y
forall k (n :: k). KnownDim n => Dim n
dim @y)
{-# INLINE lessOrEqDim' #-}
compareDim :: forall (a :: Nat) (b :: Nat)
. Dim a -> Dim b -> SOrdering (CmpNat a b)
compareDim :: Dim a -> Dim b -> SOrdering (CmpNat a b)
compareDim Dim a
a Dim b
b
= case (Word -> Word -> Ordering) -> Dim a -> Dim b -> Ordering
coerce (Word -> Word -> Ordering
forall a. Ord a => a -> a -> Ordering
compare :: Word -> Word -> Ordering) Dim a
a Dim b
b of
Ordering
LT -> SOrdering 'LT -> SOrdering (CmpNat a b)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpNat a b)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
Ordering
GT -> SOrdering 'GT -> SOrdering (CmpNat a b)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT
{-# INLINE compareDim #-}
compareDim' :: forall (a :: Nat) (b :: Nat)
. (KnownDim a, KnownDim b) => SOrdering (CmpNat a b)
compareDim' :: SOrdering (CmpNat a b)
compareDim' = Dim a -> Dim b -> SOrdering (CmpNat a b)
forall (a :: Nat) (b :: Nat).
Dim a -> Dim b -> SOrdering (CmpNat a b)
compareDim (KnownDim a => Dim a
forall k (n :: k). KnownDim n => Dim n
dim @a) (KnownDim b => Dim b
forall k (n :: k). KnownDim n => Dim n
dim @b)
{-# INLINE compareDim' #-}
plusDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (n + m)
plusDim :: Dim n -> Dim m -> Dim (n + m)
plusDim = (Word -> Word -> Word) -> Dim n -> Dim m -> Dim (n + m)
coerce (Word -> Word -> Word
forall a. Num a => a -> a -> a
(+) :: Word -> Word -> Word)
{-# INLINE plusDim #-}
minusDim :: forall (n :: Nat) (m :: Nat) . (<=) m n => Dim n -> Dim m -> Dim (n - m)
minusDim :: Dim n -> Dim m -> Dim (n - m)
minusDim = (Word -> Word -> Word) -> Dim n -> Dim m -> Dim (n - m)
coerce ((-) :: Word -> Word -> Word)
{-# INLINE minusDim #-}
minusDimM :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Maybe (Dim (n - m))
minusDimM :: Dim n -> Dim m -> Maybe (Dim (n - m))
minusDimM (DimSing Word
a) (DimSing Word
b)
| Word
a Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
>= Word
b = Dim (n - m) -> Maybe (Dim (n - m))
forall a. a -> Maybe a
Just (Word -> Dim (n - m)
coerce (Word
a Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
b))
| Bool
otherwise = Maybe (Dim (n - m))
forall a. Maybe a
Nothing
{-# INLINE minusDimM #-}
timesDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((*) n m)
timesDim :: Dim n -> Dim m -> Dim (n * m)
timesDim = (Word -> Word -> Word) -> Dim n -> Dim m -> Dim (n * m)
coerce (Word -> Word -> Word
forall a. Num a => a -> a -> a
(*) :: Word -> Word -> Word)
{-# INLINE timesDim #-}
powerDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((^) n m)
powerDim :: Dim n -> Dim m -> Dim (n ^ m)
powerDim = (Word -> Word -> Word) -> Dim n -> Dim m -> Dim (n ^ m)
coerce (Word -> Word -> Word
forall a b. (Num a, Integral b) => a -> b -> a
(^) :: Word -> Word -> Word)
{-# INLINE powerDim #-}
divDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Div n m)
divDim :: Dim n -> Dim m -> Dim (Div n m)
divDim = (Word -> Word -> Word) -> Dim n -> Dim m -> Dim (Div n m)
coerce (Word -> Word -> Word
forall a. Integral a => a -> a -> a
div :: Word -> Word -> Word)
modDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Mod n m)
modDim :: Dim n -> Dim m -> Dim (Mod n m)
modDim = (Word -> Word -> Word) -> Dim n -> Dim m -> Dim (Mod n m)
coerce (Word -> Word -> Word
forall a. Integral a => a -> a -> a
mod :: Word -> Word -> Word)
log2Dim :: forall (n :: Nat) . Dim n -> Dim (Log2 n)
log2Dim :: Dim n -> Dim (Log2 n)
log2Dim (DimSing Word
0) = Dim (Log2 n)
forall a. HasCallStack => a
undefined
log2Dim (DimSing Word
x) = Word -> Dim (Log2 n)
forall k (x :: k). Word -> Dim x
DimSing (Word -> Dim (Log2 n)) -> (Int -> Word) -> Int -> Dim (Log2 n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Dim (Log2 n)) -> Int -> Dim (Log2 n)
forall a b. (a -> b) -> a -> b
$ Word -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize Word
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Word -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros Word
x
minDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Min n m)
minDim :: Dim n -> Dim m -> Dim (Min n m)
minDim = (Word -> Word -> Word) -> Dim n -> Dim m -> Dim (Min n m)
coerce (Word -> Word -> Word
forall a. Ord a => a -> a -> a
min :: Word -> Word -> Word)
maxDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Max n m)
maxDim :: Dim n -> Dim m -> Dim (Max n m)
maxDim = (Word -> Word -> Word) -> Dim n -> Dim m -> Dim (Max n m)
coerce (Word -> Word -> Word
forall a. Ord a => a -> a -> a
max :: Word -> Word -> Word)
pattern D0 :: forall (n :: Nat) . () => n ~ 0 => Dim n
pattern $bD0 :: Dim n
$mD0 :: forall r (n :: Nat). Dim n -> ((n ~ 0) => r) -> (Void# -> r) -> r
D0 <- (sameDim (D @0) -> Just Dict)
where D0 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
0
pattern D1 :: forall (n :: Nat) . () => n ~ 1 => Dim n
pattern $bD1 :: Dim n
$mD1 :: forall r (n :: Nat). Dim n -> ((n ~ 1) => r) -> (Void# -> r) -> r
D1 <- (sameDim (D @1) -> Just Dict)
where D1 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
1
pattern D2 :: forall (n :: Nat) . () => n ~ 2 => Dim n
pattern $bD2 :: Dim n
$mD2 :: forall r (n :: Nat). Dim n -> ((n ~ 2) => r) -> (Void# -> r) -> r
D2 <- (sameDim (D @2) -> Just Dict)
where D2 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
2
pattern D3 :: forall (n :: Nat) . () => n ~ 3 => Dim n
pattern $bD3 :: Dim n
$mD3 :: forall r (n :: Nat). Dim n -> ((n ~ 3) => r) -> (Void# -> r) -> r
D3 <- (sameDim (D @3) -> Just Dict)
where D3 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
3
pattern D4 :: forall (n :: Nat) . () => n ~ 4 => Dim n
pattern $bD4 :: Dim n
$mD4 :: forall r (n :: Nat). Dim n -> ((n ~ 4) => r) -> (Void# -> r) -> r
D4 <- (sameDim (D @4) -> Just Dict)
where D4 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
4
pattern D5 :: forall (n :: Nat) . () => n ~ 5 => Dim n
pattern $bD5 :: Dim n
$mD5 :: forall r (n :: Nat). Dim n -> ((n ~ 5) => r) -> (Void# -> r) -> r
D5 <- (sameDim (D @5) -> Just Dict)
where D5 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
5
pattern D6 :: forall (n :: Nat) . () => n ~ 6 => Dim n
pattern $bD6 :: Dim n
$mD6 :: forall r (n :: Nat). Dim n -> ((n ~ 6) => r) -> (Void# -> r) -> r
D6 <- (sameDim (D @6) -> Just Dict)
where D6 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
6
pattern D7 :: forall (n :: Nat) . () => n ~ 7 => Dim n
pattern $bD7 :: Dim n
$mD7 :: forall r (n :: Nat). Dim n -> ((n ~ 7) => r) -> (Void# -> r) -> r
D7 <- (sameDim (D @7) -> Just Dict)
where D7 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
7
pattern D8 :: forall (n :: Nat) . () => n ~ 8 => Dim n
pattern $bD8 :: Dim n
$mD8 :: forall r (n :: Nat). Dim n -> ((n ~ 8) => r) -> (Void# -> r) -> r
D8 <- (sameDim (D @8) -> Just Dict)
where D8 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
8
pattern D9 :: forall (n :: Nat) . () => n ~ 9 => Dim n
pattern $bD9 :: Dim n
$mD9 :: forall r (n :: Nat). Dim n -> ((n ~ 9) => r) -> (Void# -> r) -> r
D9 <- (sameDim (D @9) -> Just Dict)
where D9 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
9
pattern D10 :: forall (n :: Nat) . () => n ~ 10 => Dim n
pattern $bD10 :: Dim n
$mD10 :: forall r (n :: Nat). Dim n -> ((n ~ 10) => r) -> (Void# -> r) -> r
D10 <- (sameDim (D @10) -> Just Dict)
where D10 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
10
pattern D11 :: forall (n :: Nat) . () => n ~ 11 => Dim n
pattern $bD11 :: Dim n
$mD11 :: forall r (n :: Nat). Dim n -> ((n ~ 11) => r) -> (Void# -> r) -> r
D11 <- (sameDim (D @11) -> Just Dict)
where D11 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
11
pattern D12 :: forall (n :: Nat) . () => n ~ 12 => Dim n
pattern $bD12 :: Dim n
$mD12 :: forall r (n :: Nat). Dim n -> ((n ~ 12) => r) -> (Void# -> r) -> r
D12 <- (sameDim (D @12) -> Just Dict)
where D12 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
12
pattern D13 :: forall (n :: Nat) . () => n ~ 13 => Dim n
pattern $bD13 :: Dim n
$mD13 :: forall r (n :: Nat). Dim n -> ((n ~ 13) => r) -> (Void# -> r) -> r
D13 <- (sameDim (D @13) -> Just Dict)
where D13 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
13
pattern D14 :: forall (n :: Nat) . () => n ~ 14 => Dim n
pattern $bD14 :: Dim n
$mD14 :: forall r (n :: Nat). Dim n -> ((n ~ 14) => r) -> (Void# -> r) -> r
D14 <- (sameDim (D @14) -> Just Dict)
where D14 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
14
pattern D15 :: forall (n :: Nat) . () => n ~ 15 => Dim n
pattern $bD15 :: Dim n
$mD15 :: forall r (n :: Nat). Dim n -> ((n ~ 15) => r) -> (Void# -> r) -> r
D15 <- (sameDim (D @15) -> Just Dict)
where D15 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
15
pattern D16 :: forall (n :: Nat) . () => n ~ 16 => Dim n
pattern $bD16 :: Dim n
$mD16 :: forall r (n :: Nat). Dim n -> ((n ~ 16) => r) -> (Void# -> r) -> r
D16 <- (sameDim (D @16) -> Just Dict)
where D16 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
16
pattern D17 :: forall (n :: Nat) . () => n ~ 17 => Dim n
pattern $bD17 :: Dim n
$mD17 :: forall r (n :: Nat). Dim n -> ((n ~ 17) => r) -> (Void# -> r) -> r
D17 <- (sameDim (D @17) -> Just Dict)
where D17 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
17
pattern D18 :: forall (n :: Nat) . () => n ~ 18 => Dim n
pattern $bD18 :: Dim n
$mD18 :: forall r (n :: Nat). Dim n -> ((n ~ 18) => r) -> (Void# -> r) -> r
D18 <- (sameDim (D @18) -> Just Dict)
where D18 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
18
pattern D19 :: forall (n :: Nat) . () => n ~ 19 => Dim n
pattern $bD19 :: Dim n
$mD19 :: forall r (n :: Nat). Dim n -> ((n ~ 19) => r) -> (Void# -> r) -> r
D19 <- (sameDim (D @19) -> Just Dict)
where D19 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
19
pattern D20 :: forall (n :: Nat) . () => n ~ 20 => Dim n
pattern $bD20 :: Dim n
$mD20 :: forall r (n :: Nat). Dim n -> ((n ~ 20) => r) -> (Void# -> r) -> r
D20 <- (sameDim (D @20) -> Just Dict)
where D20 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
20
pattern D21 :: forall (n :: Nat) . () => n ~ 21 => Dim n
pattern $bD21 :: Dim n
$mD21 :: forall r (n :: Nat). Dim n -> ((n ~ 21) => r) -> (Void# -> r) -> r
D21 <- (sameDim (D @21) -> Just Dict)
where D21 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
21
pattern D22 :: forall (n :: Nat) . () => n ~ 22 => Dim n
pattern $bD22 :: Dim n
$mD22 :: forall r (n :: Nat). Dim n -> ((n ~ 22) => r) -> (Void# -> r) -> r
D22 <- (sameDim (D @22) -> Just Dict)
where D22 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
22
pattern D23 :: forall (n :: Nat) . () => n ~ 23 => Dim n
pattern $bD23 :: Dim n
$mD23 :: forall r (n :: Nat). Dim n -> ((n ~ 23) => r) -> (Void# -> r) -> r
D23 <- (sameDim (D @23) -> Just Dict)
where D23 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
23
pattern D24 :: forall (n :: Nat) . () => n ~ 24 => Dim n
pattern $bD24 :: Dim n
$mD24 :: forall r (n :: Nat). Dim n -> ((n ~ 24) => r) -> (Void# -> r) -> r
D24 <- (sameDim (D @24) -> Just Dict)
where D24 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
24
pattern D25 :: forall (n :: Nat) . () => n ~ 25 => Dim n
pattern $bD25 :: Dim n
$mD25 :: forall r (n :: Nat). Dim n -> ((n ~ 25) => r) -> (Void# -> r) -> r
D25 <- (sameDim (D @25) -> Just Dict)
where D25 = Word -> Dim n
forall k (x :: k). Word -> Dim x
DimSing Word
25
#define PLEASE_STYLISH_HASKELL \
forall ds . KnownDimKind (KindOfEl ds) => \
forall (ns :: [Nat]) . (ds ~~ ns, Dimensions ns) => \
Dims ds
pattern Dims :: PLEASE_STYLISH_HASKELL
pattern $bDims :: Dims ds
$mDims :: forall r k (ds :: [k]).
KnownDimKind k =>
Dims ds
-> (forall (ns :: [Nat]). (ds ~~ ns, Dimensions ns) => r)
-> (Void# -> r)
-> r
Dims <- (patDims (dimKind @(KindOfEl ds)) -> PatNats)
where
Dims = Dimensions ds => Dims ds
forall k (ds :: [k]). Dimensions ds => Dims ds
dims @ds
#undef PLEASE_STYLISH_HASKELL
#define PLEASE_STYLISH_HASKELL \
forall ds . KnownDimKind (KindOfEl ds) => \
forall (ns :: [Nat]) . (FixedDims ds ns) => \
Dims ns -> Dims ds
pattern XDims :: PLEASE_STYLISH_HASKELL
pattern $bXDims :: Dims ns -> Dims ds
$mXDims :: forall r (ds :: [XNat]).
KnownDimKind XNat =>
Dims ds
-> (forall (ns :: [Nat]). FixedDims ds ns => Dims ns -> r)
-> (Void# -> r)
-> r
XDims ns <- (patDims (dimKind @(KindOfEl ds)) -> PatXNats ns)
where
XDims = Dims ns -> Dims ds
forall k (f :: k -> Type) (xs :: [k]) l (g :: l -> Type)
(ys :: [l]).
TypedList f xs -> TypedList g ys
unsafeCastTL
#undef PLEASE_STYLISH_HASKELL
pattern KnownDims :: forall (ds :: [Nat]) . ()
=> ( All KnownDim ds, All BoundedDim ds
, RepresentableList ds, Dimensions ds)
=> Dims ds
pattern $bKnownDims :: Dims ds
$mKnownDims :: forall r (ds :: [Nat]).
Dims ds
-> ((All KnownDim ds, All BoundedDim ds, RepresentableList ds,
Dimensions ds) =>
r)
-> (Void# -> r)
-> r
KnownDims <- (patKDims -> PatKDims)
where
KnownDims = Dimensions ds => Dims ds
forall k (ds :: [k]). Dimensions ds => Dims ds
dims @ds
#if !IS_UNSOUND_MATCHING_810_900
{-# COMPLETE Dims #-}
{-# COMPLETE XDims #-}
#endif
{-# COMPLETE Dims, XDims #-}
{-# COMPLETE KnownDims #-}
data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)
class Dimensions ds where
dims :: Dims ds
instance Dimensions ('[] :: [k]) where
dims :: Dims '[]
dims = Dims '[]
forall k (f :: k -> Type) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
{-# INLINE dims #-}
instance (KnownDim d, Dimensions ds) => Dimensions ((d ': ds) :: [k]) where
dims :: Dims (d : ds)
dims = Dim d
forall k (n :: k). KnownDim n => Dim n
dim Dim d -> TypedList Dim ds -> Dims (d : ds)
forall k (f :: k -> Type) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:* TypedList Dim ds
forall k (ds :: [k]). Dimensions ds => Dims ds
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 :: ((Dimensions (DimsBound ds), ExactDims ds, All KnownDimType ds,
FixedDims ds (DimsBound ds)) =>
r)
-> r
withKnownXDims (Dimensions (DimsBound ds), ExactDims ds, All KnownDimType ds,
FixedDims ds (DimsBound ds)) =>
r
f
| Dict (ds ~ Map 'N (DimsBound ds))
Dict <- Dict (ds ~ Map 'N (DimsBound ds))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @ds @(Map 'N (DimsBound ds))
= Dims (DimsBound ds) -> (Dimensions (DimsBound ds) => r) -> r
forall k (ds :: [k]) r. Dims ds -> (Dimensions ds => r) -> r
reifyDims @Nat @(DimsBound ds) Dims (DimsBound ds)
dsN
(BareConstraint (All KnownDimType ds, FixedDims ds (DimsBound ds))
-> ((All KnownDimType ds, FixedDims ds (DimsBound ds)) => () -> r)
-> ()
-> r
forall (c :: Constraint) r. BareConstraint c -> (c => r) -> r
withBareConstraint (Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
-> BareConstraint
(All KnownDimType ds, FixedDims ds (DimsBound ds))
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare (Dims (DimsBound ds)
-> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
forall (ds :: [XNat]).
ExactDims ds =>
Dims (DimsBound ds)
-> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
inferExactFixedDims @ds Dims (DimsBound ds)
dsN)) (\()
_ -> r
(Dimensions (DimsBound ds), ExactDims ds, All KnownDimType ds,
FixedDims ds (DimsBound ds)) =>
r
f) ())
where
dsN :: Dims (DimsBound ds)
dsN :: Dims (DimsBound ds)
dsN = TypedList Dim ds -> Dims (DimsBound ds)
forall k (f :: k -> Type) (xs :: [k]) l (g :: l -> Type)
(ys :: [l]).
TypedList f xs -> TypedList g ys
unsafeCastTL (Dimensions ds => TypedList Dim ds
forall k (ds :: [k]). Dimensions ds => Dims ds
dims @ds)
{-# INLINE withKnownXDims #-}
{-# ANN withKnownXDims "HLint: ignore Use const" #-}
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 :: Dims ds
minimalDims = TypedList Dim (DimsBound ds) -> Dims ds
forall k (f :: k -> Type) (xs :: [k]) l (g :: l -> Type)
(ys :: [l]).
TypedList f xs -> TypedList g ys
unsafeCastTL (BoundedDims ds => TypedList Dim (DimsBound ds)
forall k (ds :: [k]). BoundedDims ds => Dims (DimsBound ds)
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 :: Dims (DimsBound ds)
-> (forall l (ys :: [l]). Dims ys -> Maybe (Dims ds))
-> Dict (BoundedDims ds)
defineBoundedDims = Dims (DimsBound ds)
-> (forall l (ys :: [l]). Dims ys -> Maybe (Dims ds))
-> Dict (BoundedDims ds)
forall k (ds :: [k]).
(KnownDimKind k, All BoundedDim ds, RepresentableList ds,
Dimensions (DimsBound ds), BoundedDimsTail ds) =>
Dims (DimsBound ds)
-> (forall l (ys :: [l]). Dims ys -> Maybe (Dims ds))
-> Dict (BoundedDims ds)
defineBoundedDims
{-# ANN incohInstBoundedDims (ToInstance Incoherent) #-}
incohInstBoundedDims ::
forall (k :: Type) (ds :: [k])
. (Dimensions ds, KnownDimKind k) => Dict (BoundedDims ds)
incohInstBoundedDims :: Dict (BoundedDims ds)
incohInstBoundedDims
= Dims ds
-> Dict (All BoundedDim ds, RepresentableList ds)
-> Dict (BoundedDims ds)
forall k (ds :: [k]).
KnownDimKind k =>
Dims ds
-> Dict (All BoundedDim ds, RepresentableList ds)
-> Dict (BoundedDims ds)
incohInstBoundedDims' @k @ds Dims ds
forall k (ds :: [k]). Dimensions ds => Dims ds
dims (Dims ds -> Dict (All BoundedDim ds, RepresentableList ds)
forall k (ds :: [k]).
(Dimensions ds, KnownDimKind k) =>
Dims ds -> Dict (All BoundedDim ds, RepresentableList ds)
inferAllBoundedDims Dims ds
ds)
where
ds :: Dims ds
ds = Dimensions ds => Dims ds
forall k (ds :: [k]). Dimensions ds => Dims ds
dims @ds
incohInstBoundedDims' ::
forall (k :: Type) (ds :: [k])
. KnownDimKind k
=> Dims ds
-> Dict (All BoundedDim ds, RepresentableList ds)
-> Dict (BoundedDims ds)
incohInstBoundedDims' :: Dims ds
-> Dict (All BoundedDim ds, RepresentableList ds)
-> Dict (BoundedDims ds)
incohInstBoundedDims' Dims ds
ds Dict (All BoundedDim ds, RepresentableList ds)
Dict = case Dims (DimsBound ds)
dimsBound' of
Dims (DimsBound ds)
Dims -> case Dims ds
ds of
Dims ds
U -> Dims (DimsBound ds)
-> (forall l (ys :: [l]). Dims ys -> Maybe (Dims ds))
-> Dict (BoundedDims ds)
forall k (ds :: [k]).
(KnownDimKind k, All BoundedDim ds, RepresentableList ds,
Dimensions (DimsBound ds), BoundedDimsTail ds) =>
Dims (DimsBound ds)
-> (forall l (ys :: [l]). Dims ys -> Maybe (Dims ds))
-> Dict (BoundedDims ds)
defineBoundedDims Dims (DimsBound ds)
dimsBound' forall l (ys :: [l]). Dims ys -> Maybe (Dims ds)
constrainDims'
Dim y
_ :* TypedList Dim ys
ds'
| Proxy y
_ :* TypeList ys
TypeList <- RepresentableList ds => TypedList Proxy ds
forall k (xs :: [k]). RepresentableList xs => TypeList xs
tList @ds
, Dict (BoundedDims ys)
Dict <- TypedList Dim ys
-> Dict (All BoundedDim ys, RepresentableList ys)
-> Dict (BoundedDims ys)
forall k (ds :: [k]).
KnownDimKind k =>
Dims ds
-> Dict (All BoundedDim ds, RepresentableList ds)
-> Dict (BoundedDims ds)
incohInstBoundedDims' TypedList Dim ys
ds' Dict (All BoundedDim ys, RepresentableList ys)
forall (a :: Constraint). a => Dict a
Dict
-> Dims (DimsBound ds)
-> (forall l (ys :: [l]). Dims ys -> Maybe (Dims ds))
-> Dict (BoundedDims ds)
forall k (ds :: [k]).
(KnownDimKind k, All BoundedDim ds, RepresentableList ds,
Dimensions (DimsBound ds), BoundedDimsTail ds) =>
Dims (DimsBound ds)
-> (forall l (ys :: [l]). Dims ys -> Maybe (Dims ds))
-> Dict (BoundedDims ds)
defineBoundedDims Dims (DimsBound ds)
dimsBound' forall l (ys :: [l]). Dims ys -> Maybe (Dims ds)
constrainDims'
#if __GLASGOW_HASKELL__ < 810
_ -> error "incohInstBoundedDims': impossible pattern"
#endif
#if IS_UNSOUND_MATCHING_810_900
Dims (DimsBound ds)
_ -> String -> Dict (BoundedDims ds)
forall a. HasCallStack => String -> a
error String
"incohInstBoundedDims': impossible pattern"
#endif
where
dimsBound' :: Dims (DimsBound ds)
dimsBound' :: Dims (DimsBound ds)
dimsBound' = Dims ds -> Dims (DimsBound ds)
forall k (f :: k -> Type) (xs :: [k]) l (g :: l -> Type)
(ys :: [l]).
TypedList f xs -> TypedList g ys
unsafeCastTL Dims ds
ds
constrainDims' :: forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds)
constrainDims' :: Dims ys -> Maybe (Dims ds)
constrainDims' Dims ys
ys
| Dims ys -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims ys
ys [Word] -> [Word] -> Bool
forall a. Eq a => a -> a -> Bool
== Dims (DimsBound ds) -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims (DimsBound ds)
dimsBound'
= Dims ds -> Maybe (Dims ds)
forall a. a -> Maybe a
Just (Dims ys -> Dims ds
forall k (f :: k -> Type) (xs :: [k]) l (g :: l -> Type)
(ys :: [l]).
TypedList f xs -> TypedList g ys
unsafeCastTL Dims ys
ys)
| Bool
otherwise = Maybe (Dims ds)
forall a. Maybe a
Nothing
#if defined(__HADDOCK__) || defined(__HADDOCK_VERSION__)
instance Dimensions ns => BoundedDims (ns :: [Nat]) where
dimsBound :: Dims (DimsBound ns)
dimsBound = Dims (DimsBound ns)
forall a. HasCallStack => a
undefined
constrainDims :: Dims ys -> Maybe (Dims ns)
constrainDims = Dims ys -> Maybe (Dims ns)
forall a. HasCallStack => a
undefined
#endif
instance BoundedDims ('[] :: [XNat]) where
dimsBound :: Dims (DimsBound '[])
dimsBound = Dims (DimsBound '[])
forall k (f :: k -> Type) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
constrainDims :: Dims ys -> Maybe (Dims '[])
constrainDims Dims ys
U = Dims '[] -> Maybe (Dims '[])
forall a. a -> Maybe a
Just Dims '[]
forall k (f :: k -> Type) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
constrainDims (Dim y
_ :* TypedList Dim ys
_) = Maybe (Dims '[])
forall a. Maybe a
Nothing
instance (BoundedDim n, BoundedDims ns) => BoundedDims ((n ': ns) :: [XNat]) where
dimsBound :: Dims (DimsBound (n : ns))
dimsBound = BoundedDim n => Dim (DimBound n)
forall k (d :: k). BoundedDim d => Dim (DimBound d)
dimBound @n Dim (DimBound n)
-> TypedList Dim (DimsBound ns)
-> TypedList Dim (DimBound n : DimsBound ns)
forall k (f :: k -> Type) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:* BoundedDims ns => TypedList Dim (DimsBound ns)
forall k (ds :: [k]). BoundedDims ds => Dims (DimsBound ds)
dimsBound @ns
constrainDims :: Dims ys -> Maybe (Dims (n : ns))
constrainDims Dims ys
U = Maybe (Dims (n : ns))
forall a. Maybe a
Nothing
constrainDims (Dim y
y :* TypedList Dim ys
ys) = Dim n -> TypedList Dim ns -> Dims (n : ns)
forall k (f :: k -> Type) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
(:*) (Dim n -> TypedList Dim ns -> Dims (n : ns))
-> Maybe (Dim n) -> Maybe (TypedList Dim ns -> Dims (n : ns))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Dim y -> Maybe (Dim n)
forall k (d :: k) k (y :: k).
BoundedDim d =>
Dim y -> Maybe (Dim d)
constrainDim Dim y
y Maybe (TypedList Dim ns -> Dims (n : ns))
-> Maybe (TypedList Dim ns) -> Maybe (Dims (n : ns))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypedList Dim ys -> Maybe (TypedList Dim ns)
forall k (ds :: [k]) k (ys :: [k]).
BoundedDims ds =>
Dims ys -> Maybe (Dims ds)
constrainDims TypedList Dim ys
ys
typeableDims :: forall (ds :: [Nat]) . Typeable ds => Dims ds
typeableDims :: Dims ds
typeableDims = case Typeable ds => TypeRep ds
forall k (a :: k). Typeable a => TypeRep a
typeRep @ds of
App (App TypeRep a
_ (TypeRep b
tx :: TypeRep (n :: k1))) (TypeRep b
txs :: TypeRep (ns :: k2))
| Dict (k1 ~ Nat)
Dict <- Dict (k1 ~ Nat)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @k1 @Nat
, Dict (k1 ~ [Nat])
Dict <- Dict (k1 ~ [Nat])
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @k2 @[Nat]
, Dict (ds ~ (b : b))
Dict <- Dict (ds ~ (b : b))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @ds @(n ': ns)
-> TypeRep b -> (Typeable b => Dim b) -> Dim b
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep b
tx (Typeable b => Dim b
forall (n :: Nat). Typeable n => Dim n
typeableDim @n) Dim b -> TypedList Dim b -> Dims ds
forall k (f :: k -> Type) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:* TypeRep b -> (Typeable b => TypedList Dim b) -> TypedList Dim b
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep b
txs (Typeable b => TypedList Dim b
forall (ds :: [Nat]). Typeable ds => Dims ds
typeableDims @ns)
Con TyCon
_
-> TypedList Any '[] -> Dims ds
forall a b. a -> b
unsafeCoerce TypedList Any '[]
forall k (f :: k -> Type) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
TypeRep ds
r -> String -> Dims ds
forall a. HasCallStack => String -> a
error (String
"typeableDims -- impossible typeRep: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep ds -> String
forall a. Show a => a -> String
show TypeRep ds
r)
{-# INLINE typeableDims #-}
inferTypeableDims :: forall (ds :: [Nat]) . Dims ds -> Dict (Typeable ds)
inferTypeableDims :: Dims ds -> Dict (Typeable ds)
inferTypeableDims Dims ds
U = Dict (Typeable ds)
forall (a :: Constraint). a => Dict a
Dict
inferTypeableDims ((Dim y
D :: Dim d) :* TypedList Dim ys
ds)
| Dict (KnownNat y)
Dict <- (KnownDim y :- KnownNat y)
-> Dict (KnownDim y) -> Dict (KnownNat y)
forall (a :: Constraint) (b :: Constraint).
(a :- b) -> Dict a -> Dict b
mapDict KnownDim y :- KnownNat y
forall (b :: Constraint) (h :: Constraint). Class b h => h :- b
cls (KnownDim y => Dict (KnownDim y)
forall (a :: Constraint). a => Dict a
Dict @(KnownDim d))
, Dict (Typeable ys)
Dict <- TypedList Dim ys -> Dict (Typeable ys)
forall (ds :: [Nat]). Dims ds -> Dict (Typeable ds)
inferTypeableDims TypedList Dim ys
ds
= Dict (Typeable ds)
forall (a :: Constraint). a => Dict a
Dict
listDims :: forall xs . Dims xs -> [Word]
listDims :: Dims xs -> [Word]
listDims = Dims xs -> [Word]
forall a b. a -> b
unsafeCoerce
{-# INLINE listDims #-}
someDimsVal :: [Word] -> SomeDims
someDimsVal :: [Word] -> SomeDims
someDimsVal = Dims Any -> SomeDims
forall (ns :: [Nat]). Dims ns -> SomeDims
SomeDims (Dims Any -> SomeDims)
-> ([Word] -> Dims Any) -> [Word] -> SomeDims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word] -> Dims Any
forall a b. a -> b
unsafeCoerce
{-# INLINE someDimsVal #-}
totalDim :: forall xs . Dims xs -> Word
totalDim :: Dims xs -> Word
totalDim = [Word] -> Word
forall (t :: Type -> Type) a. (Foldable t, Num a) => t a -> a
product ([Word] -> Word) -> (Dims xs -> [Word]) -> Dims xs -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dims xs -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims
{-# INLINE totalDim #-}
totalDim' :: forall xs . Dimensions xs => Word
totalDim' :: Word
totalDim' = Dims xs -> Word
forall k (xs :: [k]). Dims xs -> Word
totalDim (Dimensions xs => Dims xs
forall k (ds :: [k]). Dimensions ds => Dims ds
dims @xs)
{-# INLINE totalDim' #-}
stripPrefixDims :: forall (xs :: [Nat]) (ys :: [Nat])
. Dims xs -> Dims ys
-> Maybe (Dims (StripPrefix xs ys))
stripPrefixDims :: Dims xs -> Dims ys -> Maybe (Dims (StripPrefix xs ys))
stripPrefixDims = ([Word] -> [Word] -> Maybe [Word])
-> Dims xs -> Dims ys -> Maybe (Dims (StripPrefix xs ys))
forall a b. a -> b
unsafeCoerce ([Word] -> [Word] -> Maybe [Word]
forall a. Eq a => [a] -> [a] -> Maybe [a]
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 :: Dims xs -> Dims ys -> Maybe (Dims (StripSuffix xs ys))
stripSuffixDims = ([Word] -> [Word] -> Maybe [Word])
-> Dims xs -> Dims ys -> Maybe (Dims (StripSuffix xs ys))
forall a b. a -> b
unsafeCoerce [Word] -> [Word] -> Maybe [Word]
stripSuf
where
stripSuf :: [Word] -> [Word] -> Maybe [Word]
stripSuf :: [Word] -> [Word] -> Maybe [Word]
stripSuf [Word]
suf [Word]
whole = [Word] -> [Word] -> Maybe [Word]
go [Word]
pref [Word]
whole
where
pref :: [Word]
pref = [Word] -> [Word] -> [Word]
getPref [Word]
suf [Word]
whole
getPref :: [Word] -> [Word] -> [Word]
getPref (Word
_:[Word]
as) (Word
_:[Word]
bs) = [Word] -> [Word] -> [Word]
getPref [Word]
as [Word]
bs
getPref [] [Word]
bs = (Word -> Word -> Word) -> [Word] -> [Word] -> [Word]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Word -> Word -> Word
forall a b. a -> b -> a
const [Word]
whole [Word]
bs
getPref [Word]
_ [] = []
go :: [Word] -> [Word] -> Maybe [Word]
go (Word
_:[Word]
as) (Word
_:[Word]
bs) = [Word] -> [Word] -> Maybe [Word]
go [Word]
as [Word]
bs
go [] [Word]
bs = if [Word]
suf [Word] -> [Word] -> Bool
forall a. Eq a => a -> a -> Bool
== [Word]
bs then [Word] -> Maybe [Word]
forall a. a -> Maybe a
Just [Word]
pref else Maybe [Word]
forall a. Maybe a
Nothing
go [Word]
_ [] = Maybe [Word]
forall a. Maybe a
Nothing
{-# INLINE stripSuffixDims #-}
sameDims :: forall (as :: [Nat]) (bs :: [Nat])
. Dims as -> Dims bs -> Maybe (Dict (as ~ bs))
sameDims :: Dims as -> Dims bs -> Maybe (Dict (as ~ bs))
sameDims Dims as
as Dims bs
bs
| Dims as -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims as
as [Word] -> [Word] -> Bool
forall a. Eq a => a -> a -> Bool
== Dims bs -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims bs
bs
= Dict (as ~ bs) -> Maybe (Dict (as ~ bs))
forall a. a -> Maybe a
Just (Dict (as ~ bs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @as @bs)
| Bool
otherwise = Maybe (Dict (as ~ bs))
forall a. Maybe a
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' :: p as -> q bs -> Maybe (Dict (as ~ bs))
sameDims' = (q bs -> Maybe (Dict (as ~ bs)))
-> p as -> q bs -> Maybe (Dict (as ~ bs))
forall a b. a -> b -> a
const ((q bs -> Maybe (Dict (as ~ bs)))
-> p as -> q bs -> Maybe (Dict (as ~ bs)))
-> (Maybe (Dict (as ~ bs)) -> q bs -> Maybe (Dict (as ~ bs)))
-> Maybe (Dict (as ~ bs))
-> p as
-> q bs
-> Maybe (Dict (as ~ bs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Dict (as ~ bs)) -> q bs -> Maybe (Dict (as ~ bs))
forall a b. a -> b -> a
const (Maybe (Dict (as ~ bs)) -> p as -> q bs -> Maybe (Dict (as ~ bs)))
-> Maybe (Dict (as ~ bs)) -> p as -> q bs -> Maybe (Dict (as ~ bs))
forall a b. (a -> b) -> a -> b
$ Dims as -> Dims bs -> Maybe (Dict (as ~ bs))
forall (as :: [Nat]) (bs :: [Nat]).
Dims as -> Dims bs -> Maybe (Dict (as ~ bs))
sameDims (Dimensions as => Dims as
forall k (ds :: [k]). Dimensions ds => Dims ds
dims @as) (Dimensions bs => Dims bs
forall k (ds :: [k]). Dimensions ds => Dims ds
dims @bs)
{-# INLINE sameDims' #-}
inSpaceOf :: forall ds p q
. p ds -> q ds -> p ds
inSpaceOf :: p ds -> q ds -> p ds
inSpaceOf = p ds -> q ds -> p ds
forall a b. a -> b -> a
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 :: Dims xns -> Dims ns -> Maybe (Dict (FixedDims xns ns))
inferFixedDims Dims xns
U Dims ns
U = Dict ('[] ~ '[]) -> Maybe (Dict ('[] ~ '[]))
forall a. a -> Maybe a
Just Dict ('[] ~ '[])
forall (a :: Constraint). a => Dict a
Dict
inferFixedDims (Dx (Dim n
a :: Dim n) :* TypedList Dim ys
xns) (Dim y
b :* TypedList Dim ys
ns)
| Dict (n ~ DimBound (Head xns))
Dict <- Dict (n ~ DimBound (Head xns))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @n @(DimBound (Head xns))
, Just Dict (n <= y)
Dict <- Dim n -> Dim y -> Maybe (Dict (n <= y))
forall (x :: Nat) (y :: Nat).
Dim x -> Dim y -> Maybe (Dict (x <= y))
lessOrEqDim Dim n
a Dim y
b
, Just Dict (FixedDims ys ys)
Dict <- TypedList Dim ys
-> TypedList Dim ys -> Maybe (Dict (FixedDims ys ys))
forall (xns :: [XNat]) (ns :: [Nat]).
All KnownDimType xns =>
Dims xns -> Dims ns -> Maybe (Dict (FixedDims xns ns))
inferFixedDims TypedList Dim ys
xns TypedList Dim ys
ns
= Dict ((y : ys) ~ (y : ys), LE m y (CmpNat m y), FixedDims ys ys)
-> Maybe
(Dict ((y : ys) ~ (y : ys), LE m y (CmpNat m y), FixedDims ys ys))
forall a. a -> Maybe a
Just Dict ((y : ys) ~ (y : ys), LE m y (CmpNat m y), FixedDims ys ys)
forall (a :: Constraint). a => Dict a
Dict
inferFixedDims (Dn Dim n
a :* TypedList Dim ys
xns) (Dim y
b :* TypedList Dim ys
ns)
| Just Dict (n ~ y)
Dict <- Dim n -> Dim y -> Maybe (Dict (n ~ y))
forall (x :: Nat) (y :: Nat).
Dim x -> Dim y -> Maybe (Dict (x ~ y))
sameDim Dim n
a Dim y
b
, Just Dict (FixedDims ys ys)
Dict <- TypedList Dim ys
-> TypedList Dim ys -> Maybe (Dict (FixedDims ys ys))
forall (xns :: [XNat]) (ns :: [Nat]).
All KnownDimType xns =>
Dims xns -> Dims ns -> Maybe (Dict (FixedDims xns ns))
inferFixedDims TypedList Dim ys
xns TypedList Dim ys
ns
= Dict ((n : ys) ~ (n : ys), n ~ n, FixedDims ys ys)
-> Maybe (Dict ((n : ys) ~ (n : ys), n ~ n, FixedDims ys ys))
forall a. a -> Maybe a
Just Dict ((n : ys) ~ (n : ys), n ~ n, FixedDims ys ys)
forall (a :: Constraint). a => Dict a
Dict
inferFixedDims Dims xns
_ Dims ns
_ = Maybe (Dict (FixedDims xns ns))
forall a. Maybe a
Nothing
unsafeInferFixedDims :: forall (xns :: [XNat]) (ns :: [Nat])
. Dims ns -> Dict (FixedDims xns ns)
unsafeInferFixedDims :: Dims ns -> Dict (FixedDims xns ns)
unsafeInferFixedDims Dims ns
U
| Dict (xns ~ '[])
Dict <- Dict (xns ~ '[])
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xns @'[] = Dict (FixedDims xns ns)
forall (a :: Constraint). a => Dict a
Dict
unsafeInferFixedDims ((Dim y
D :: Dim n) :* TypedList Dim ys
ns)
| Dict (xns ~ (N y : Tail xns))
Dict <- Dict (xns ~ (N y : Tail xns))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xns @(N n ': Tail xns)
, Dict (FixedDims (Tail xns) ys)
Dict <- TypedList Dim ys -> Dict (FixedDims (Tail xns) ys)
forall (xns :: [XNat]) (ns :: [Nat]).
Dims ns -> Dict (FixedDims xns ns)
unsafeInferFixedDims @(Tail xns) TypedList Dim ys
ns = Dict (FixedDims xns ns)
forall (a :: Constraint). a => Dict a
Dict
{-# INLINE unsafeInferFixedDims #-}
inferExactFixedDims :: forall (ds :: [XNat]) . ExactDims ds
=> Dims (DimsBound ds)
-> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
inferExactFixedDims :: Dims (DimsBound ds)
-> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
inferExactFixedDims Dims (DimsBound ds)
U = Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
forall (a :: Constraint). a => Dict a
Dict
inferExactFixedDims (_ :* ns)
| Dict
(All KnownDimType (Tail ds),
FixedDims (Tail ds) (DimsBound (Tail ds)))
Dict <- Dims (DimsBound (Tail ds))
-> Dict
(All KnownDimType (Tail ds),
FixedDims (Tail ds) (DimsBound (Tail ds)))
forall (ds :: [XNat]).
ExactDims ds =>
Dims (DimsBound ds)
-> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
inferExactFixedDims @(Tail ds) TypedList Dim ys
Dims (DimsBound (Tail ds))
ns = Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
forall (a :: Constraint). a => Dict a
Dict
{-# INLINE inferExactFixedDims #-}
instance Typeable d => Data (Dim (d :: Nat)) where
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Dim d -> c (Dim d)
gfoldl forall d b. Data d => c (d -> b) -> d -> c b
_ forall g. g -> c g
f = Dim d -> c (Dim d)
forall g. g -> c g
f
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Dim d)
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
z = c (Dim d) -> Constr -> c (Dim d)
forall a b. a -> b -> a
const (Dim d -> c (Dim d)
forall r. r -> c r
z (Typeable d => Dim d
forall (n :: Nat). Typeable n => Dim n
typeableDim @d))
toConstr :: Dim d -> Constr
toConstr = Constr -> Dim d -> Constr
forall a b. a -> b -> a
const (Constr -> Dim d -> Constr) -> Constr -> Dim d -> Constr
forall a b. (a -> b) -> a -> b
$ Word -> Constr
dimNatConstr (Dim d -> Word
forall k (x :: k). Dim x -> Word
dimVal (Typeable d => Dim d
forall (n :: Nat). Typeable n => Dim n
typeableDim @d))
dataTypeOf :: Dim d -> DataType
dataTypeOf = DataType -> Dim d -> DataType
forall a b. a -> b -> a
const (DataType -> Dim d -> DataType) -> DataType -> Dim d -> DataType
forall a b. (a -> b) -> a -> b
$ Word -> DataType
dimDataType (Dim d -> Word
forall k (x :: k). Dim x -> Word
dimVal (Typeable d => Dim d
forall (n :: Nat). Typeable n => Dim n
typeableDim @d))
dimDataType :: Word -> DataType
dimDataType :: Word -> DataType
dimDataType = String -> [Constr] -> DataType
mkDataType String
"Numeric.Dim.Dim" ([Constr] -> DataType) -> (Word -> [Constr]) -> Word -> DataType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
:[]) (Constr -> [Constr]) -> (Word -> Constr) -> Word -> [Constr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Constr
dimNatConstr
dimNatConstr :: Word -> Constr
dimNatConstr :: Word -> Constr
dimNatConstr Word
d = DataType -> String -> [String] -> Fixity -> Constr
mkConstr (Word -> DataType
dimDataType Word
d) (String
"D" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word -> String
forall a. Show a => a -> String
show Word
d) [] Fixity
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 :: Dim d -> Rep (Dim d) x
from Dim d
D = M1
C ('MetaCons (AppendSymbol "D" (ShowNat d)) 'PrefixI 'False) U1 x
-> M1
D
('MetaData "Dim" "Numeric.Dim" "dimensions" 'False)
(M1
C ('MetaCons (AppendSymbol "D" (ShowNat d)) 'PrefixI 'False) U1)
x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
G.M1 (U1 x
-> M1
C ('MetaCons (AppendSymbol "D" (ShowNat d)) 'PrefixI 'False) U1 x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
G.M1 U1 x
forall k (p :: k). U1 p
G.U1)
to :: Rep (Dim d) x -> Dim d
to = Dim d
-> M1
D
('MetaData "Dim" "Numeric.Dim" "dimensions" 'False)
(M1
C ('MetaCons (AppendSymbol "D" (ShowNat d)) 'PrefixI 'False) U1)
x
-> Dim d
forall a b. a -> b -> a
const (KnownDim d => Dim d
forall k (n :: k). KnownDim n => Dim n
dim @d)
instance Eq (Dim (n :: Nat)) where
== :: Dim n -> Dim n -> Bool
(==) = (Dim n -> Bool) -> Dim n -> Dim n -> Bool
forall a b. a -> b -> a
const (Bool -> Dim n -> Bool
forall a b. a -> b -> a
const Bool
True)
{-# INLINE (==) #-}
/= :: Dim n -> Dim n -> Bool
(/=) = (Dim n -> Bool) -> Dim n -> Dim n -> Bool
forall a b. a -> b -> a
const (Bool -> Dim n -> Bool
forall a b. a -> b -> a
const Bool
False)
{-# INLINE (/=) #-}
instance Eq (Dim (x :: XNat)) where
== :: Dim x -> Dim x -> Bool
(==) = (Word -> Word -> Bool) -> Dim x -> Dim x -> Bool
coerce (Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Word -> Word -> Bool)
{-# INLINE (==) #-}
/= :: Dim x -> Dim x -> Bool
(/=) = (Word -> Word -> Bool) -> Dim x -> Dim x -> Bool
coerce (Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
(/=) :: Word -> Word -> Bool)
{-# INLINE (/=) #-}
instance Eq (Dims (ds :: [Nat])) where
== :: Dims ds -> Dims ds -> Bool
(==) = (Dims ds -> Bool) -> Dims ds -> Dims ds -> Bool
forall a b. a -> b -> a
const (Bool -> Dims ds -> Bool
forall a b. a -> b -> a
const Bool
True)
{-# INLINE (==) #-}
/= :: Dims ds -> Dims ds -> Bool
(/=) = (Dims ds -> Bool) -> Dims ds -> Dims ds -> Bool
forall a b. a -> b -> a
const (Bool -> Dims ds -> Bool
forall a b. a -> b -> a
const Bool
False)
{-# INLINE (/=) #-}
instance Eq (Dims (ds :: [XNat])) where
== :: Dims ds -> Dims ds -> Bool
(==) = ([Word] -> [Word] -> Bool) -> Dims ds -> Dims ds -> Bool
forall a b. a -> b
unsafeCoerce ([Word] -> [Word] -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: [Word] -> [Word] -> Bool)
{-# INLINE (==) #-}
/= :: Dims ds -> Dims ds -> Bool
(/=) = ([Word] -> [Word] -> Bool) -> Dims ds -> Dims ds -> Bool
forall a b. a -> b
unsafeCoerce ([Word] -> [Word] -> Bool
forall a. Eq a => a -> a -> Bool
(/=) :: [Word] -> [Word] -> Bool)
{-# INLINE (/=) #-}
instance Eq SomeDims where
SomeDims Dims ns
as == :: SomeDims -> SomeDims -> Bool
== SomeDims Dims ns
bs = Dims ns -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims ns
as [Word] -> [Word] -> Bool
forall a. Eq a => a -> a -> Bool
== Dims ns -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims ns
bs
{-# INLINE (==) #-}
SomeDims Dims ns
as /= :: SomeDims -> SomeDims -> Bool
/= SomeDims Dims ns
bs = Dims ns -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims ns
as [Word] -> [Word] -> Bool
forall a. Eq a => a -> a -> Bool
/= Dims ns -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims ns
bs
{-# INLINE (/=) #-}
instance Ord (Dim (n :: Nat)) where
compare :: Dim n -> Dim n -> Ordering
compare = (Dim n -> Ordering) -> Dim n -> Dim n -> Ordering
forall a b. a -> b -> a
const (Ordering -> Dim n -> Ordering
forall a b. a -> b -> a
const Ordering
EQ)
{-# INLINE compare #-}
instance Ord (Dim (x :: XNat)) where
compare :: Dim x -> Dim x -> Ordering
compare = (Word -> Word -> Ordering) -> Dim x -> Dim x -> Ordering
coerce (Word -> Word -> Ordering
forall a. Ord a => a -> a -> Ordering
compare :: Word -> Word -> Ordering)
{-# INLINE compare #-}
instance Ord (Dims (ds :: [Nat])) where
compare :: Dims ds -> Dims ds -> Ordering
compare = (Dims ds -> Ordering) -> Dims ds -> Dims ds -> Ordering
forall a b. a -> b -> a
const (Ordering -> Dims ds -> Ordering
forall a b. a -> b -> a
const Ordering
EQ)
{-# INLINE compare #-}
instance Ord (Dims (ds :: [XNat])) where
compare :: Dims ds -> Dims ds -> Ordering
compare = ([Word] -> [Word] -> Ordering) -> Dims ds -> Dims ds -> Ordering
forall a b. a -> b
unsafeCoerce ([Word] -> [Word] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare :: [Word] -> [Word] -> Ordering)
{-# INLINE compare #-}
instance Ord SomeDims where
compare :: SomeDims -> SomeDims -> Ordering
compare (SomeDims Dims ns
as) (SomeDims Dims ns
bs) = [Word] -> [Word] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Dims ns -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims ns
as) (Dims ns -> [Word]
forall k (xs :: [k]). Dims xs -> [Word]
listDims Dims ns
bs)
{-# INLINE compare #-}
instance Show (Dim (x :: k)) where
showsPrec :: Int -> Dim x -> String -> String
showsPrec Int
_ Dim x
d = Char -> String -> String
showChar Char
'D' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> String -> String
forall a. Show a => a -> String -> String
shows (Dim x -> Word
forall k (x :: k). Dim x -> Word
dimVal Dim x
d)
{-# INLINE showsPrec #-}
instance Show (Dims (xs :: [k])) where
showsPrec :: Int -> Dims xs -> String -> String
showsPrec = (forall (x :: k). Int -> Dim x -> String -> String)
-> Int -> Dims xs -> String -> String
forall k (f :: k -> Type) (xs :: [k]).
(forall (x :: k). Int -> f x -> String -> String)
-> Int -> TypedList f xs -> String -> String
typedListShowsPrec @Dim @xs forall (x :: k). Int -> Dim x -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec
instance Show SomeDims where
showsPrec :: Int -> SomeDims -> String -> String
showsPrec Int
p (SomeDims Dims ns
ds)
= Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
10)
((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
showString String
"SomeDims " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Dims ns -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
10 Dims ns
ds
instance BoundedDim x => Read (Dim (x :: k)) where
readPrec :: ReadPrec (Dim x)
readPrec = ReadPrec Lexeme
Read.lexP ReadPrec Lexeme -> (Lexeme -> ReadPrec (Dim x)) -> ReadPrec (Dim x)
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Read.Ident (Char
'D':String
s)
| Just Dim x
d <- String -> Maybe Word
forall a. Read a => String -> Maybe a
Read.readMaybe String
s
Maybe Word -> (Word -> Maybe (Dim x)) -> Maybe (Dim x)
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= SomeDim -> Maybe (Dim x)
forall k (d :: k) k (y :: k).
BoundedDim d =>
Dim y -> Maybe (Dim d)
constrainDim @x @(XN 0) (SomeDim -> Maybe (Dim x))
-> (Word -> SomeDim) -> Word -> Maybe (Dim x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> SomeDim
forall k (x :: k). Word -> Dim x
DimSing
-> Dim x -> ReadPrec (Dim x)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Dim x
d
Lexeme
_ -> ReadPrec (Dim x)
forall a. ReadPrec a
Read.pfail
readList :: ReadS [Dim x]
readList = ReadS [Dim x]
forall a. Read a => ReadS [a]
Read.readListDefault
readListPrec :: ReadPrec [Dim x]
readListPrec = ReadPrec [Dim x]
forall a. Read a => ReadPrec [a]
Read.readListPrecDefault
instance BoundedDims xs => Read (Dims (xs :: [k])) where
readPrec :: ReadPrec (Dims xs)
readPrec = String
-> (forall (x :: k). BoundedDim x => ReadPrec (Dim x))
-> TypedList Proxy xs
-> ReadPrec (Dims xs)
forall k (c :: k -> Constraint) (f :: k -> Type) (xs :: [k])
(g :: k -> Type).
All c xs =>
String
-> (forall (x :: k). c x => ReadPrec (f x))
-> TypedList g xs
-> ReadPrec (TypedList f xs)
typedListReadPrec @BoundedDim String
":*" forall (x :: k). BoundedDim x => ReadPrec (Dim x)
forall a. Read a => ReadPrec a
Read.readPrec (RepresentableList xs => TypedList Proxy xs
forall k (xs :: [k]). RepresentableList xs => TypeList xs
tList @xs)
readList :: ReadS [Dims xs]
readList = ReadS [Dims xs]
forall a. Read a => ReadS [a]
Read.readListDefault
readListPrec :: ReadPrec [Dims xs]
readListPrec = ReadPrec [Dims xs]
forall a. Read a => ReadPrec [a]
Read.readListPrecDefault
instance Read SomeDims where
readPrec :: ReadPrec SomeDims
readPrec = ReadPrec SomeDims -> ReadPrec SomeDims
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadPrec SomeDims -> ReadPrec SomeDims)
-> (ReadPrec SomeDims -> ReadPrec SomeDims)
-> ReadPrec SomeDims
-> ReadPrec SomeDims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ReadPrec SomeDims -> ReadPrec SomeDims
forall a. Int -> ReadPrec a -> ReadPrec a
Read.prec Int
10 (ReadPrec SomeDims -> ReadPrec SomeDims)
-> ReadPrec SomeDims -> ReadPrec SomeDims
forall a b. (a -> b) -> a -> b
$ do
ReadP () -> ReadPrec ()
forall a. ReadP a -> ReadPrec a
Read.lift (ReadP () -> ReadPrec ())
-> (Lexeme -> ReadP ()) -> Lexeme -> ReadPrec ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lexeme -> ReadP ()
Read.expect (Lexeme -> ReadPrec ()) -> Lexeme -> ReadPrec ()
forall a b. (a -> b) -> a -> b
$ String -> Lexeme
Read.Ident String
"SomeDims"
(forall z. (forall (x :: Nat). Dim x -> z) -> ReadPrec z)
-> (forall (ns :: [Nat]). Dims ns -> SomeDims) -> ReadPrec SomeDims
forall k (f :: k -> Type) r.
(forall z. (forall (x :: k). f x -> z) -> ReadPrec z)
-> (forall (xs :: [k]). TypedList f xs -> r) -> ReadPrec r
withTypedListReadPrec @Dim @SomeDims
(\forall (x :: Nat). Dim x -> z
g -> (\(Dx Dim n
d) -> Dim n -> z
forall (x :: Nat). Dim x -> z
g Dim n
d) (SomeDim -> z) -> ReadPrec SomeDim -> ReadPrec z
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Read SomeDim => ReadPrec SomeDim
forall a. Read a => ReadPrec a
Read.readPrec @(Dim (XN 0)))
forall (ns :: [Nat]). Dims ns -> SomeDims
SomeDims
reifyDim :: forall (k :: Type) (d :: k) (rep :: RuntimeRep) (r :: TYPE rep)
. Dim d -> (KnownDim d => r) -> r
reifyDim :: Dim d -> (KnownDim d => r) -> r
reifyDim Dim d
d KnownDim d => r
k = MagicDim d r -> Dim d -> r
forall a b. a -> b
unsafeCoerce ((KnownDim d => r) -> MagicDim d r
forall k (d :: k) r. (KnownDim d => r) -> MagicDim d r
MagicDim KnownDim d => r
k :: MagicDim d r) Dim d
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 :: Natural -> (KnownNat d => r) -> r
reifyNat Natural
d KnownNat d => r
k = MagicNat d r -> Natural -> r
forall a b. a -> b
unsafeCoerce ((KnownNat d => r) -> MagicNat d r
forall (d :: Nat) r. (KnownNat d => r) -> MagicNat d r
MagicNat KnownNat d => r
k :: MagicNat d r) Natural
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 :: Dims ds -> (Dimensions ds => r) -> r
reifyDims Dims ds
ds Dimensions ds => r
k = MagicDims ds r -> Dims ds -> r
forall a b. a -> b
unsafeCoerce ((Dimensions ds => r) -> MagicDims ds r
forall k (ds :: [k]) r. (Dimensions ds => r) -> MagicDims ds r
MagicDims Dimensions ds => r
k :: MagicDims ds r) Dims ds
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 :: DimType d -> Dim d -> PatDim d
patDim DimType d
DimTNat Dim d
d = Dim d -> (KnownDim d => PatDim d) -> PatDim d
forall k (d :: k) r. Dim d -> (KnownDim d => r) -> r
reifyDim Dim d
d KnownDim d => PatDim d
forall (n :: Nat). KnownDim n => PatDim n
PatNat
patDim DimType d
DimTXNatN Dim d
d = Dim n -> PatDim (N n)
forall (n :: Nat). Dim n -> PatDim (N n)
PatXNatN (Dim d -> Dim n
coerce Dim d
d)
patDim DimType d
DimTXNatX Dim d
d = Dim Any -> Dim (XN m) -> PatDim (XN m)
forall (n :: Nat) (m :: Nat). Dim n -> Dim (XN m) -> PatDim (XN m)
f (Dim d -> Dim Any
coerce Dim d
d) Dim d
Dim (XN m)
d
where
f :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim (XN m) -> PatDim (XN m)
f :: Dim n -> Dim (XN m) -> PatDim (XN m)
f Dim n
n = case Dict (m <= m) -> Dict (m <= n)
forall (a :: Constraint) (b :: Constraint). Dict a -> Dict b
unsafeCoerceDict @(m <= m) @(m <= n) Dict (m <= m)
forall (a :: Constraint). a => Dict a
Dict of
Dict (m <= n)
Dict -> PatDim (XN m) -> Dim (XN m) -> PatDim (XN m)
forall a b. a -> b -> a
const (Dim n -> PatDim (XN m)
forall (m :: Nat) (n :: Nat). (m <= n) => Dim n -> PatDim (XN m)
PatXNatX Dim n
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 :: DimKind k -> Dims ds -> PatDims ds
patDims DimKind k
DimKNat Dims ds
ds = Dims ds -> (Dimensions ds => PatDims ds) -> PatDims ds
forall k (ds :: [k]) r. Dims ds -> (Dimensions ds => r) -> r
reifyDims Dims ds
ds Dimensions ds => PatDims ds
forall (ds :: [Nat]). Dimensions ds => PatDims ds
PatNats
patDims DimKind k
DimKXNat Dims ds
ds = BareConstraint (FixedDims ds Any)
-> (FixedDims ds Any => PatDims ds) -> PatDims ds
forall (c :: Constraint) r. BareConstraint c -> (c => r) -> r
withBareConstraint
(Dict (FixedDims ds Any) -> BareConstraint (FixedDims ds Any)
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare (Dims Any -> Dict (FixedDims ds Any)
forall (xns :: [XNat]) (ns :: [Nat]).
Dims ns -> Dict (FixedDims xns ns)
unsafeInferFixedDims @ds Dims Any
ds')) (Dims Any -> PatDims ds
forall (ds :: [XNat]) (ns :: [Nat]).
FixedDims ds ns =>
Dims ns -> PatDims ds
PatXNats Dims Any
ds')
where
ds' :: Dims Any
ds' = Dims ds -> Dims Any
forall k (f :: k -> Type) (xs :: [k]) l (g :: l -> Type)
(ys :: [l]).
TypedList f xs -> TypedList g ys
unsafeCastTL Dims ds
ds
{-# INLINE patDims #-}
inferAllBoundedDims :: forall (k :: Type) (ds :: [k])
. (Dimensions ds, KnownDimKind k)
=> Dims ds -> Dict (All BoundedDim ds, RepresentableList ds)
inferAllBoundedDims :: Dims ds -> Dict (All BoundedDim ds, RepresentableList ds)
inferAllBoundedDims = Dims ds -> Dict (All BoundedDim ds, RepresentableList ds)
forall (xs :: [k]).
Dims xs -> Dict (All BoundedDim xs, RepresentableList xs)
go
where
reifyBoundedDim :: forall (d :: k) . Dim d -> Dict (BoundedDim d)
reifyBoundedDim :: Dim d -> Dict (BoundedDim d)
reifyBoundedDim = case KnownDimKind k => DimKind k
forall k. KnownDimKind k => DimKind k
dimKind @k of
DimKind k
DimKNat -> (Dim d -> (KnownDim d => Dict (BoundedDim d)) -> Dict (BoundedDim d)
forall k (d :: k) r. Dim d -> (KnownDim d => r) -> r
`reifyDim` KnownDim d => Dict (BoundedDim d)
forall (a :: Constraint). a => Dict a
Dict)
DimKind k
DimKXNat
| Dict (d ~ N (DimBound d))
Dict <- Dict (d ~ N (DimBound d))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @d @(N (DimBound d))
-> \Dim d
d -> Dim (DimBound d)
-> (KnownDim (DimBound d) => Dict (BoundedDim d))
-> Dict (BoundedDim d)
forall k (d :: k) r. Dim d -> (KnownDim d => r) -> r
reifyDim (Dim d -> Dim (DimBound d)
coerce Dim d
d :: Dim (DimBound d)) KnownDim (DimBound d) => Dict (BoundedDim d)
forall (a :: Constraint). a => Dict a
Dict
go :: forall (xs :: [k]) . Dims xs
-> Dict (All BoundedDim xs, RepresentableList xs)
go :: Dims xs -> Dict (All BoundedDim xs, RepresentableList xs)
go Dims xs
U = Dict (All BoundedDim xs, RepresentableList xs)
forall (a :: Constraint). a => Dict a
Dict
go (Dim y
d :* TypedList Dim ys
ds)
| Dict (BoundedDim y)
Dict <- Dim y -> Dict (BoundedDim y)
forall (d :: k). Dim d -> Dict (BoundedDim d)
reifyBoundedDim Dim y
d
, Dict (All BoundedDim ys, RepresentableList ys)
Dict <- TypedList Dim ys -> Dict (All BoundedDim ys, RepresentableList ys)
forall (xs :: [k]).
Dims xs -> Dict (All BoundedDim xs, RepresentableList xs)
go TypedList Dim ys
ds = Dict (All BoundedDim xs, RepresentableList xs)
forall (a :: Constraint). a => Dict a
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 :: Dims ns -> PatKDims ns
patKDims Dims ns
U = PatKDims ns
forall (ns :: [Nat]).
(All KnownDim ns, All BoundedDim ns, RepresentableList ns,
Dimensions ns) =>
PatKDims ns
PatKDims
patKDims (Dim y
D :* TypedList Dim ys
ns) = case TypedList Dim ys -> PatKDims ys
forall (ns :: [Nat]). Dims ns -> PatKDims ns
patKDims TypedList Dim ys
ns of
PatKDims ys
PatKDims -> PatKDims ns
forall (ns :: [Nat]).
(All KnownDim ns, All BoundedDim ns, RepresentableList ns,
Dimensions ns) =>
PatKDims ns
PatKDims
{-# INLINE patKDims #-}
unsafeCoerceDict :: forall (a :: Constraint) (b :: Constraint)
. Dict a -> Dict b
unsafeCoerceDict :: Dict a -> Dict b
unsafeCoerceDict = Dict a -> Dict b
forall a b. a -> b
unsafeCoerce
unsafeCastTL :: TypedList f (xs :: [k]) -> TypedList g (ys :: [l])
unsafeCastTL :: TypedList f xs -> TypedList g ys
unsafeCastTL = TypedList f xs -> TypedList g ys
forall a b. a -> b
unsafeCoerce