{-# 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
-- Copyright   :  (c) Artem Chirkin
-- License     :  BSD3
--
-- This module provides `KnownDim` class that is similar to `KnownNat` from `GHC.TypeNats`,
-- but keeps `Word`s instead of `Natural`s;
-- Also it provides `Dim` data type serving as a singleton
-- suitable for recovering an instance of the `KnownDim` class.
-- A set of utility functions provide inference functionality, so
-- that `KnownDim` can be preserved over some type-level operations.
--
-- Provides a data type @Dims ds@ to keep dimension sizes
-- for multiple-dimensional data.
-- Higher indices go first, i.e. assumed enumeration
--          is i = i1*n1*n2*...*n(k-1) + ... + i(k-2)*n1*n2 + i(k-1)*n1 + ik
-- This corresponds to row-first layout of matrices and multidimenional arrays.
--
-----------------------------------------------------------------------------

module Numeric.Dimensions.Dim
  ( -- * @Dim@: a @Nat@-indexed dimension
    -- ** Type level numbers that can be unknown.
    Nat, XNat (..), XN, N
  , DimType (..), KnownDimType(..), DimKind (..), KnownDimKind(..)
    -- ** Term level dimension
  , 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
    -- ** Simple Dim arithmetics
    --
    --   The functions below create singleton values that work as a witness
    --   of `KnownDim` instance for type-level Nat operations.
    --   For example, to show that @(a + b)@ is a @KnownDim@, one writes:
    --
    --   > case plusDim dA dB of
    --   >   D -> ... -- here we know KnownDim ( a + b )
    --
    --   There is a bug and a feature in these functions though:
    --   they are implemented in terms of @Num Word@, which means that
    --   their results are subject to integer overflow.
    --   The good side is the confidence that they behave exactly as
    --   their @Word@ counterparts.
  , plusDim, minusDim, minusDimM, timesDim, powerDim, divDim, modDim, log2Dim
  , minDim, maxDim
    -- ** Re-export part of `Data.Type.Lits` for convenience
  , CmpNat, SOrdering (..), type (+), type (-), type (*), type (^), type (<=)
  , Min, Max
    -- * @Dims@: a list of dimensions
  , 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
    -- ** Re-export type list
  , RepresentableList (..), TypeList, types
  , order, order'
  , KindOf, KindOfEl
#if !(defined(__HADDOCK__) || defined(__HADDOCK_VERSION__))
    -- hide a plugin-related func
  , 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)

{-
COMPLETE pragmas on Dims and XDims let you avoid the boilerplate of catch-all cases
when pattern-matching only to get the evidence brought by Dims. Unfortunately,
there is a bug the pattern-match checker in GHC 8.10 and 9.0, which warns you incorrectly
about redundant or inacessible patterns in some rare cases.
To workaround those dangerous cases, I disable these pragmas for some compiler versions.
(i.e. it's better to place a redundant wildcard case than to have a partial function at runtime).

https://gitlab.haskell.org/ghc/ghc/-/issues/19622
 -}
#define IS_UNSOUND_MATCHING_810_900 (MIN_VERSION_GLASGOW_HASKELL(8,10,0,0) && !MIN_VERSION_GLASGOW_HASKELL(9,1,0,0))


-- | Either known or unknown at compile-time natural number
data XNat = XN Nat | N Nat
-- | Unknown natural number, known to be not smaller than the given Nat
type XN = 'XN
-- | Known natural number
type N = 'N

-- | GADT to support `KnownDimType` type class.
--   Find out if this type variable is a @Nat@ or @XNat@,
--   and whether @XNat@ is of known or constrained type.
data DimType (d :: k) where
    -- | This is a plain @Nat@
    DimTNat   :: DimType (n :: Nat)
    -- | Given @XNat@ is known
    DimTXNatN :: DimType (N n)
    -- | Given @XNat@ is constrained unknown
    DimTXNatX :: DimType (XN m)

-- | GADT to support `KnownDimKind` type class.
--   Match against its constructors to know if @k@ is @Nat@ or @XNat@
data DimKind (k :: Type) where
    -- | Working on @Nat@.
    DimKNat  :: DimKind Nat
    -- | Working on @XNat@.
    DimKXNat :: DimKind XNat

-- | Figure out whether the type-level dimension is `Nat`, or `N Nat`, or `XN Nat`.
class KnownDimType d where
    -- | Pattern-match against this to out the value (type) of the dim type variable.
    dimType :: DimType d

-- | Figure out whether the type-level dimension is `Nat` or `XNat`.
class KnownDimKind k where
    -- | Pattern-match against this to out the kind of the dim type variable.
    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

-- | Singleton type to store type-level dimension value.
--
--   On the one hand, it can be used to let type-inference system know
--   relations between type-level naturals.
--   On the other hand, this is just a newtype wrapper on the @Word@ type.
--
--   Usually, the type parameter of @Dim@ is either @Nat@ or @XNat@.
--   If dimensionality of your data is known in advance, use @Nat@;
--   if you know the size of some dimensions, but do not know the size
--   of others, use @XNat@s to represent them.
newtype Dim (x :: k) = DimSing Word
  deriving ( Typeable )

type role Dim nominal

-- | Same as `SomeNat`
type SomeDim = Dim (XN 0)

-- | Type-level dimensionality.
type Dims = (TypedList Dim :: [k] -> Type)

#define PLEASE_STYLISH_HASKELL \
  forall d . KnownDimType d => \
  (KindOf d ~ Nat, KnownDim d) => \
  Dim d

-- | Match against this pattern to bring `KnownDim` instance into scope.
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

-- | Statically known `XNat`
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

-- | `XNat` that is unknown at compile time.
--   Same as `SomeNat`, but for a dimension:
--   Hide dimension size inside, but allow specifying its minimum possible value.
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 #-}

-- | This class provides the `Dim` associated with a type-level natural.
--
--   Note, kind of the @KnownDim@ argument is usually @Nat@, because
--     it is impossible to create a unique @KnownDim (XN m)@ instance.
--   Nevertheless, you can have @KnownDim (N n)@, which is useful in some cases.
class KnownDim n where
    -- | Get value of type-level dim at runtime.
    --
    --   Note, this function is supposed to be used with @TypeApplications@.
    --   For example, you can type:
    --
    --   >>>:set -XTypeApplications
    --   >>>:set -XDataKinds
    --   >>>:t dim @3
    --   dim @3 :: Dim 3
    --
    --   >>>:set -XTypeOperators
    --   >>>:t dim @(13 - 6)
    --   dim @(13 - 6) :: Dim 7
    --
    dim :: Dim n

-- | Get a minimal or exact bound of a @Dim@.
--
--   To satisfy the @BoundedDim@ means to be equal to @N n@ or be not less than @XN m@.
class (KnownDimKind (KindOf d), KnownDimType d, KnownDim (DimBound d))
    => BoundedDim d where
    -- | Minimal or exact bound of a @Dim@.
    --   Useful for indexing: it is safe to index something by an index less than
    --   @DimBound n@ (for both @Nat@ and @Xnat@ indexed dims).
    type family DimBound d :: Nat
    -- | Get such a minimal @Dim (DimBound n)@, that @Dim n@ is guaranteed
    --   to be not less than @dimBound@ if @n ~ XN a@,
    --     otherwise, the return @Dim@ is the same as @n@.
    dimBound :: Dim (DimBound d)
    -- | If the runtime value of @Dim y@ satisfies @dimBound @x@,
    --   then coerce to @Dim x@. Otherwise, return @Nothing@.
    --
    --   To satisfy the @dimBound@ means to be equal to @N n@ or be not less than @XN m@.
    constrainDim :: forall y . Dim y -> Maybe (Dim d)

-- | Returns the minimal @Dim@ that satisfies the @BoundedDim@ constraint
--   (this is the exact @dim@ for @Nat@s and the minimal bound for @XNat@s).
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 #-}

-- | Similar to `natVal` from `GHC.TypeNats`, but returns `Word`.
dimVal :: forall x . Dim x -> Word
dimVal :: Dim x -> Word
dimVal = Dim x -> Word
coerce
{-# INLINE dimVal #-}

-- | Similar to `natVal` from `GHC.TypeNats`, but returns `Word`.
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' #-}

-- | Construct a @Dim n@ if there is an instance of @Typeable n@ around.
--
--   Note: we can do this only for @Nat@-indexed dim, because the type @XN m@
--         does not have enough information to create a dim at runtime.
typeableDim :: forall (n :: Nat) . Typeable n => Dim n
{- YES, that's right. TyCon of a Nat is a string containing the Nat value.
   There simply no place in a TyCon to keep the Nat as a number
     (check GHC.Types for the definition of TyCon).

  Here is an excert from Data.Typeable.Internal:

  -- | Used to make `'Typeable' instance for things of kind Nat
  typeNatTypeRep :: KnownNat a => Proxy# a -> TypeRep a
  typeNatTypeRep p = typeLitTypeRep (show (natVal' p)) tcNat

 -}
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 #-}

-- | Constraints given by an XNat type on possible values of a Nat hidden inside.
type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where
    FixedDim ('N a)  b = a ~ b
    FixedDim ('XN m) b = m <= b

-- | This is either @Nat@, or a known @XNat@ (i.e. @N n@).
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)

-- | If you have @KnownDim d@, then @d@ can only be @Nat@ or a known type of
--   @XNat@ (i.e. @N n@).
--   This function assures the type checker that this is indeed the case.
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

-- | Similar to `someNatVal` from `GHC.TypeNats`.
someDimVal :: Word -> SomeDim
someDimVal :: Word -> SomeDim
someDimVal = Word -> SomeDim
coerce
{-# INLINE someDimVal #-}

-- | `constrainDim` with explicitly-passed constraining @Dim@
--   to avoid @AllowAmbiguousTypes@.
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 #-}

-- | Decrease minimum allowed size of a @Dim (XN x)@.
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 #-}

-- | We either get evidence that this function
--   was instantiated with the same type-level numbers, or Nothing.
--
--   Note, this function works on @Nat@-indexed dimensions only,
--   because @Dim (XN x)@ does not have runtime evidence to infer @x@
--   and `KnownDim x` does not imply `KnownDim (XN x)`.
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 #-}

-- | We either get evidence that this function
--   was instantiated with the same type-level numbers, or Nothing.
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' #-}

-- | We either get evidence that @x@ is not greater than @y@, or Nothing.
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 #-}

-- | We either get evidence that @x@ is not greater than @y@, or Nothing.
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' #-}

-- | Ordering of dimension values.
--
--   Note: `CmpNat` forces type parameters to kind `Nat`;
--         if you want to compare unknown `XNat`s, use `Ord` instance of `Dim`.
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 #-}

-- | Ordering of dimension values.
--
--   Note: `CmpNat` forces type parameters to kind `Nat`;
--         if you want to compare unknown `XNat`s, use `Ord` instance of `Dim`.
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' #-}

-- | Same as `Prelude.(+)`.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (n + m)@.
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 #-}

-- | Same as `Prelude.(-)`.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (n - m)@.
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 #-}

-- | Similar to `minusDim`, but returns @Nothing@ if the result would be negative.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (n - m)@.
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 #-}

-- | Same as `Prelude.(*)`.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (n * m)@.
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 #-}

-- | Same as `Prelude.(^)`.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (n ^ m)@.
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 #-}

-- | Same as `Prelude.div`.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (Div n m)@.
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)

-- | Same as `Prelude.mod`.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (Mod n m)@.
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)

-- | Returns log base 2 (round down).
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (Log2 n)@.
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

-- | Same as `Prelude.min`.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (Min n m)@.
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)

-- | Same as `Prelude.max`.
--   Pattern-matching against the result would produce the evindence
--    @KnownDim (Max n m)@.
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)



-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | Match @Dim n@ against a concrete @Nat@
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

-- | @O(1)@ Pattern-matching against this constructor brings a `Dimensions`
--   instance into the scope.
--   Thus, you can do arbitrary operations on your dims and use this pattern
--   at any time to reconstruct the class instance at runtime.
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

-- | @O(n)@
--   Pattern-matching against this constructor reveals Nat-kinded list of dims,
--   pretending the dimensionality is known at compile time within the scope
--   of the pattern match.
--   This is the main recommended way to get `Dims` at runtime;
--   for example, reading a list of dimensions from a file.
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

-- | @O(Length ds)@ A heavy weapon against all sorts of type errors
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 #-}

-- | Same as SomeNat, but for Dimensions:
--   Hide all information about Dimensions inside
data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)

-- | Put runtime evidence of `Dims` value inside function constraints.
--   Similar to `KnownDim` or `KnownNat`, but for lists of numbers.
--
--   Note, kind of the @Dimensions@ list is usually @Nat@, restricted by
--   @KnownDim@ being also @Nat@-indexed
--     (it is impossible to create a unique @KnownDim (XN m)@ instance).
--   Nevertheless, you can have @KnownDim (N n)@, which is useful in some cases.
class Dimensions ds where
    -- | Get dimensionality of a space at runtime,
    --   represented as a list of `Dim`.
    --
    --   Note, this function is supposed to be used with @TypeApplications@.
    --   For example, you can type:
    --
    --   >>>:set -XTypeApplications
    --   >>>:set -XDataKinds
    --   >>>:t dims @'[17, 12]
    --   dims @'[17, 12] :: Dims '[17, 12]
    --
    --   >>>:t dims @'[]
    --   dims @'[] :: Dims '[]
    --
    --   >>>:t dims @(Tail '[3,2,5,7])
    --   dims @(Tail '[3,2,5,7]) :: Dims '[2, 5, 7]
    --
    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 #-}

-- | If you have @Dimensions ds@, then @ds@ can only be @[Nat]@ or a known type of
--   @[XNa]t@ (i.e. all @N n@).
--   This function assures the type checker that this is indeed the case.
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" #-}

-- | Minimal or exact bound of @Dims@.
--   This is a plural form of `DimBound`.
type family DimsBound (ds :: [k]) :: [Nat] where
    DimsBound (ns :: [Nat]) = ns
    DimsBound ('[] :: [XNat]) = '[]
    DimsBound (n ': ns) = DimBound n ': DimsBound ns

-- | Every dim in a list is either @Nat@, or a known @XNat@ (i.e. @N n@).
type family ExactDims (d :: [k]) :: Constraint where
    ExactDims (_  :: [Nat])  = ()
    ExactDims (xs :: [XNat]) = xs ~ Map 'N (DimsBound xs)

-- | This is a technical "helper" family that allows to infer BoundedDims
--   constraint on a tail of a list via the superclass relation.
type family BoundedDimsTail (ds :: [k]) where
    BoundedDimsTail '[] = UnreachableConstraint (BoundedDims (Tail '[]))
                           "BoundDimsTail '[] -- BoundedDims (Tail '[])"
    BoundedDimsTail (_ ': ns) = BoundedDims ns

-- | Get a minimal or exact bound of @Dims@.
--
--   This is a plural form of `BoundedDim`.
--
--   @BoundedDims@ is a somewhat weaker form of @Dimensions@:
--
--    * It is defined for both @[Nat]@ and @[XNat]@;
--    * Instance of @Dimensions ds@ always implies @BoundedDims ds@.
--
--   @BoundedDims@ is a powerful inference tool:
--     its instances do not require much, but it provides a lot via the superclass
--     constraints.
class ( KnownDimKind (KindOfEl ds), All BoundedDim ds, RepresentableList ds
      , Dimensions (DimsBound ds), BoundedDimsTail ds)
   => BoundedDims ds where
    -- | Plural form for `dimBound`
    dimsBound :: Dims (DimsBound ds)
    -- | Plural form for `constrainDim`.
    --
    --   Given a @Dims ys@, test if its runtime value satisfies constraints imposed by
    --   @BoundedDims xs@, and returns it back coerced to @Dims xs@ on success.
    --
    --   This function allows to guess safely individual dimension values,
    --   as well as the length of the dimension list.
    --   It returns @Nothing@ if @xs@ and @ys@ have different length or if any
    --   of the values in @ys@ are less than the corresponding values of @xs@.
    constrainDims :: forall ys . Dims ys -> Maybe (Dims ds)

-- | Minimal runtime @Dims ds@ value that satifies the constraints imposed by
--   the type signature of @Dims ds@
--   (this is the exact @dims@ for @Nat@s and the minimal bound for @XNat@s).
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

-- instance {-# INCOHERENT #-} Dimensions ns => BoundedDims (ns :: [k])
{-# 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



-- | Construct a @Dims ds@ if there is an instance of @Typeable ds@ around.
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 #-}

-- | @Dims (ds :: [Nat])@ is always @Typeable@.
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


-- | @O(1)@ Convert @Dims xs@ to a plain haskell list of dimension sizes.
--
--   Note, for @XNat@-indexed list it returns actual content dimensions,
--   not the constraint numbers (@XN m@)
listDims :: forall xs . Dims xs -> [Word]
listDims :: Dims xs -> [Word]
listDims = Dims xs -> [Word]
forall a b. a -> b
unsafeCoerce
{-# INLINE listDims #-}

-- | Convert a plain haskell list of dimension sizes into an unknown
--   type-level dimensionality  @O(1)@.
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 #-}

-- | Product of all dimension sizes @O(Length xs)@.
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 #-}

-- | Product of all dimension sizes @O(Length xs)@.
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' #-}

-- | Drop the given prefix from a Dims list.
--   It returns Nothing if the list did not start with the prefix given,
--    or Just the Dims after the prefix, if it does.
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 #-}

-- | Drop the given suffix from a Dims list.
--   It returns Nothing if the list did not end with the suffix given,
--    or Just the Dims before the suffix, if it does.
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 #-}

-- | We either get evidence that this function was instantiated with the
--   same type-level Dimensions, or 'Nothing' @O(Length xs)@.
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 #-}

-- | We either get evidence that this function was instantiated with the
--   same type-level Dimensions, or 'Nothing' @O(Length xs)@.
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' #-}


-- | Restricted version of `const`, similar to `asProxyTypeOf`;
--   to be used on such implicit functions as `dims`, `dimsBound` etc.
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 #-}

-- | Constrain @Nat@ dimensions hidden behind @XNat@s.
--   This is a link connecting the two types of type-level dims;
--   you often need it to convert @Dims@, @Idxs@, and data.
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))

-- | Try to instantiate the `FixedDims` constraint given two @Dims@ lists.
--
--   The first @Dims@ is assumed to be the output of @minimalDims@,
--   i.e. @listDims xns == toList (listDims xns)@.
--
--   If you input a list that is not equal to its type-level @DimsBound@,
--   you will just have a lower chance to get @Just Dict@ result.
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

-- | A very unsafe function that bypasses all type-level checks and constructs
--   the evidence from 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)
    {-
    Very unsafe operation.
    I rely here on the fact that FixedDim xn n has the same
    runtime rep as a single type equality.
    If that changes, then the code is broken.
     -}
  | 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 #-}

-- | Infer `FixedDims` if you know that all of dims are exact (@d ~ N n@).
--   This function is totally safe and faithful.
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



-- | This function does GHC's magic to convert user-supplied `dim` function
--   to create an instance of `KnownDim` typeclass at runtime.
--   The trick is taken from Edward Kmett's reflection library explained
--   in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection
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 -- convert to *some* [Nat]
{-# INLINE patDims #-}

{-
I know that Dimensions can be either Nats or N-known XNats.
Therefore, inside the worker function I can (un)safely pick up a BoundedDim
instance for (d ~ N n)
 -}
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