-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Safe type-level dimensionality for multidimensional data.
--   
--   Safe type-level dimensionality for multidimensional data.
@package dimensions
@version 0.3.2.0


-- | This modules is based on <a>TypeLits</a> and re-exports its
--   functionality. It provides <a>KnownDim</a> class that is similar to
--   <a>KnownNat</a>, but keeps <a>Int</a>s instead of <a>Integer</a>s. A
--   set of utility functions provide inference functionality, so that
--   <a>KnownDim</a> can be preserved over some type-level operations.
module Numeric.TypeLits

-- | Either known or unknown at compile-time natural number
data XNat
XN :: Nat -> XNat
N :: Nat -> XNat

-- | Unknown natural number, known to be not smaller than the given Nat
type XN (n :: Nat) = XN n

-- | Known natural number
type N (n :: Nat) = N n

-- | Same as SomeNat, but for Dimensions: Hide all information about
--   Dimensions inside
data SomeIntNat
SomeIntNat :: (Proxy n) -> SomeIntNat

-- | Similar to <a>someNatVal</a>, but for a single dimension
someIntNatVal :: Int -> Maybe SomeIntNat

-- | Similar to <a>natVal</a> from <a>TypeLits</a>, but returns <a>Int</a>.
intNatVal :: forall n proxy. KnownDim n => proxy n -> Int

-- | This function does GHC's magic to convert user-supplied <a>dimVal'</a>
--   function to create an instance of KnownDim typeclass at runtime. The
--   trick is taken from Edward Kmett's reflection library explained in
--   <a>https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection</a>
reifyDim :: forall r. Int -> (forall (n :: Nat). KnownDim n => Proxy# n -> r) -> r

-- | This class gives the int associated with a type-level natural. Valid
--   known dim must be not less than 0.
class KnownDim (n :: Nat)

-- | Get value of type-level dim at runtime
dimVal' :: KnownDim n => Int

-- | A constraint family that makes sure all subdimensions are known.

-- | A variant of <a>dimVal'</a> that gets <a>Proxy#</a> as an argument.
dimVal# :: forall (n :: Nat). KnownDim n => Proxy# n -> Int

-- | The type constructor <tt>Proxy#</tt> is used to bear witness to some
--   type variable. It's used when you want to pass around proxy values for
--   doing things like modelling type applications. A <tt>Proxy#</tt> is
--   not only unboxed, it also has a polymorphic kind, and has no runtime
--   representation, being totally free.
data Proxy# :: forall k. k -> TYPE VoidRep

-- | Witness for an unboxed <tt>Proxy#</tt> value, which has no runtime
--   representation.
proxy# :: Proxy# k a

-- | Bring an instance of certain class or constaint satisfaction evidence
--   into scope.
data Evidence :: Constraint -> Type
[Evidence] :: a => Evidence a
withEvidence :: Evidence a -> (a => r) -> r
sumEvs :: Evidence a -> Evidence b -> Evidence (a, b)
(+!+) :: Evidence a -> Evidence b -> Evidence (a, b)
infixl 4 +!+
inferPlusKnownDim :: forall n m. (KnownDim n, KnownDim m) => Evidence (KnownDim (n + m))
inferMinusKnownDim :: forall n m. (KnownDim n, KnownDim m, m <= n) => Evidence (KnownDim (n - m))
inferMinusKnownDimM :: forall n m. (KnownDim n, KnownDim m) => Maybe (Evidence (KnownDim (n - m)))
inferTimesKnownDim :: forall n m. (KnownDim n, KnownDim m) => Evidence (KnownDim (n * m))

-- | A concrete, poly-kinded proxy type
data Proxy k (t :: k) :: forall k. k -> *
Proxy :: Proxy k
instance GHC.TypeLits.KnownNat n => Numeric.TypeLits.KnownDim n
instance Numeric.TypeLits.KnownDim 0
instance Numeric.TypeLits.KnownDim 1
instance Numeric.TypeLits.KnownDim 2
instance Numeric.TypeLits.KnownDim 3
instance Numeric.TypeLits.KnownDim 4
instance Numeric.TypeLits.KnownDim 5
instance Numeric.TypeLits.KnownDim 6
instance Numeric.TypeLits.KnownDim 7
instance Numeric.TypeLits.KnownDim 8
instance Numeric.TypeLits.KnownDim 9
instance Numeric.TypeLits.KnownDim 10
instance Numeric.TypeLits.KnownDim 11
instance Numeric.TypeLits.KnownDim 12
instance Numeric.TypeLits.KnownDim 13
instance Numeric.TypeLits.KnownDim 14
instance Numeric.TypeLits.KnownDim 15
instance Numeric.TypeLits.KnownDim 16
instance Numeric.TypeLits.KnownDim 17
instance Numeric.TypeLits.KnownDim 18
instance Numeric.TypeLits.KnownDim 19
instance Numeric.TypeLits.KnownDim 20
instance GHC.Classes.Eq Numeric.TypeLits.SomeIntNat
instance GHC.Classes.Ord Numeric.TypeLits.SomeIntNat
instance GHC.Show.Show Numeric.TypeLits.SomeIntNat
instance GHC.Read.Read Numeric.TypeLits.SomeIntNat


-- | Provides type-level operations on lists.
--   
--   <ul>
--   <li>Note for GHC 8.0 Due to <a>GHC issue #13538</a> some complex type
--   families could not be truly kind-polymorphic before GHC 8.2, thus I
--   specialized them to work only on `[Nat]` and `[XNat]`.</li>
--   </ul>
module Numeric.Dimensions.List

-- | List concatenation

-- | Synonym for a type-level cons (injective, since this is just a synonym
--   for the list constructor)
type (:+) (a :: k) (as :: [k]) = a : as

-- | Synonym for a type-level snoc (injective!)
type (+:) (ns :: [k]) (n :: k) = Snoc ns n

-- | Synonym for an empty type-level list
type Empty = '[]

-- | Prefix-style synonym for cons
type Cons (n :: k) (ns :: [k]) = n :+ ns

-- | Prefix-style synonym for snoc
type Snoc (ns :: [k]) (n :: k) = GetSnoc (DoSnoc ns n)

-- | Prefix-style synonym for concatenation
type Concat (as :: [k]) (bs :: [k]) = as ++ bs

-- | Reverse a type-level list (injective!)
type Reverse (xs :: [k]) = Reversed (DoReverse xs)

-- | Represent a triple of lists forming a relation `as ++ bs ~ asbs`
class (asbs ~ Concat as bs, as ~ Prefix bs asbs, bs ~ Suffix as asbs, IsSuffix bs asbs ~ True, IsPrefix as asbs ~ True) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) | as bs -> asbs, as asbs -> bs, bs asbs -> as
tlPrefix :: ConcatList as bs asbs => ConcatEvidence as bs asbs -> Proxy as
tlSuffix :: ConcatList as bs asbs => ConcatEvidence as bs asbs -> Proxy bs
tlConcat :: ConcatList as bs asbs => ConcatEvidence as bs asbs -> Proxy asbs

-- | Type-level list that is known to be finite. Basically, provides means
--   to get its length and term-level rep (via TypeList)
class FiniteList (xs :: [k]) where type Length xs :: Nat where {
    type family Length xs :: Nat;
}

-- | Length of a type-level list at term level
order :: FiniteList xs => Int

-- | Get type-level constructed list
tList :: FiniteList xs => TypeList xs

-- | Type level list, used together with FiniteList typeclass
data TypeList (xs :: [k])
[TLEmpty] :: TypeList '[]
[TLCons] :: FiniteList xs => !(Proxy# x) -> !(TypeList xs) -> TypeList (x :+ xs)

-- | Any two type-level lists can be concatenated, so we just fool the
--   compiler by unsafeCoercing proxy-like data type.
inferConcat :: forall as bs. ConcatEvidence as bs (as ++ bs)

-- | <tt>as</tt> being prefix of <tt>asbs</tt> is enough to infer some
--   concatenation relations so we just fool the compiler by unsafeCoercing
--   proxy-like data type.
inferSuffix :: forall as asbs. IsPrefix as asbs ~ True => ConcatEvidence as (Suffix as asbs) asbs

-- | <tt>bs</tt> being suffix of <tt>asbs</tt> is enough to infer some
--   concatenation relations so we just fool the compiler by unsafeCoercing
--   proxy-like data type.
inferPrefix :: forall bs asbs. IsSuffix bs asbs ~ True => ConcatEvidence (Prefix bs asbs) bs asbs

-- | Pattern-matching on the constructor of this type brings an evidence
--   that `as ++ bs ~ asbs`
type ConcatEvidence (as :: [k]) (bs :: [k]) (asbs :: [k]) = Evidence (asbs ~ Concat as bs, as ~ Prefix bs asbs, bs ~ Suffix as asbs, IsSuffix bs asbs ~ True, IsPrefix as asbs ~ True)

-- | Pattern-matching on the constructor of this type brings an evidence
--   that the type-level parameter list is finite
type FiniteListEvidence (xs :: [k]) = Evidence (FiniteList xs)

-- | Length of a finite list is known and equal to <a>order</a> of the list
inferKnownLength :: forall xs. FiniteList xs => Evidence (KnownDim (Length xs))

-- | Tail of the list is also known list
inferTailFiniteList :: forall xs. FiniteList xs => Maybe (Evidence (FiniteList (Tail xs)))

-- | Infer that concatenation is also finite
inferConcatFiniteList :: forall as bs. (FiniteList as, FiniteList bs) => Evidence (FiniteList (as ++ bs))

-- | Infer that prefix is also finite
inferPrefixFiniteList :: forall bs asbs. (IsSuffix bs asbs ~ True, FiniteList bs, FiniteList asbs) => Evidence (FiniteList (Prefix bs asbs))

-- | Infer that suffix is also finite
inferSuffixFiniteList :: forall as asbs. (IsPrefix as asbs ~ True, FiniteList as, FiniteList asbs) => Evidence (FiniteList (Suffix as asbs))

-- | Make snoc almost as good as cons
inferSnocFiniteList :: forall xs z. FiniteList xs => Evidence (FiniteList (xs +: z))

-- | Init of the list is also known list
inferInitFiniteList :: forall xs. FiniteList xs => Maybe (Evidence (FiniteList (Init xs)))

-- | Take KnownDim of the list is also known list
inferTakeNFiniteList :: forall n xs. (KnownDim n, FiniteList xs) => Evidence (FiniteList (Take n xs))

-- | Drop KnownDim of the list is also known list
inferDropNFiniteList :: forall n xs. (KnownDim n, FiniteList xs) => Evidence (FiniteList (Drop n xs))

-- | Reverse of the list is also known list
inferReverseFiniteList :: forall xs. FiniteList xs => Evidence (FiniteList (Reverse xs))
instance forall k (asbs :: [k]) (as :: [k]) (bs :: [k]). (asbs ~ Numeric.Dimensions.List.Concat as bs, as ~ Numeric.Dimensions.List.Prefix bs asbs, bs ~ Numeric.Dimensions.List.Suffix as asbs, Numeric.Dimensions.List.IsSuffix bs asbs ~ 'GHC.Types.True, Numeric.Dimensions.List.IsPrefix as asbs ~ 'GHC.Types.True) => Numeric.Dimensions.List.ConcatList as bs asbs
instance forall k (xs :: [k]). GHC.Show.Show (Numeric.Dimensions.List.TypeList xs)
instance Numeric.Dimensions.List.FiniteList '[]
instance forall k (xs :: [k]) (x :: k). Numeric.Dimensions.List.FiniteList xs => Numeric.Dimensions.List.FiniteList (x Numeric.Dimensions.List.:+ xs)


-- | Provides a data type `Dim ds` to keep dimension sizes for
--   multiple-dimensional data. Lower indices go first, i.e. assumed
--   enumeration is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1).
module Numeric.Dimensions.Dim

-- | (Kind) This is the kind of type-level natural numbers.
data Nat :: *

-- | Either known or unknown at compile-time natural number
data XNat

-- | Unknown natural number, known to be not smaller than the given Nat
type XN (n :: Nat) = XN n

-- | Known natural number
type N (n :: Nat) = N n

-- | Type-level dimensionality
data Dim (ns :: k)

-- | Zero-rank dimensionality - scalar
[D] :: Dim '[]

-- | List-like concatenation of dimensionality. NatKind constraint is
--   needed here to infer that
[:*] :: forall (n :: l) (ns :: [k]). NatKind [k] l => !(Dim n) -> !(Dim ns) -> Dim (ConsDim n ns)

-- | Proxy-like constructor
[Dn] :: forall (n :: Nat). KnownDim n => Dim (n :: Nat)

-- | Nat known at runtime packed into existential constructor
[Dx] :: forall (n :: Nat) (m :: Nat). n <= m => !(Dim m) -> Dim (XN n)

-- | Get value of type-level dim at runtime. Gives a product of all
--   dimensions if is a list.
dimVal :: Dim x -> Int

-- | Product of all dimension sizes.
totalDim :: forall ds proxy. Dimensions ds => proxy ds -> Int

-- | Get runtime-known dim and make sure it is not smaller than the given
--   Nat.
fromInt :: forall m. KnownDim m => Int -> Maybe (Dim (XN m))

-- | Same as SomeNat, but for Dimensions: Hide all information about
--   Dimensions inside
data SomeDims
SomeDims :: (Dim ns) -> SomeDims

-- | Same as SomeNat, but for Dimension: Hide all information about
--   Dimension inside
data SomeDim
SomeDim :: (Dim n) -> SomeDim

-- | Similar to <a>someNatVal</a>, but for a single dimension
someDimVal :: Int -> Maybe SomeDim

-- | Convert a list of ints into unknown type-level Dimensions list
someDimsVal :: [Int] -> Maybe SomeDims

-- | We either get evidence that this function was instantiated with the
--   same type-level Dimensions, or <a>Nothing</a>.
sameDim :: Dim as -> Dim bs -> Maybe (Evidence (as ~ bs))

-- | Compare dimensions by their size in lexicorgaphic order from the last
--   dimension to the first dimension (the last dimension is the most
--   significant one).
compareDim :: Dim as -> Dim bs -> Ordering

-- | Similar to <a>const</a> or <tt>asProxyTypeOf</tt>; to be used on such
--   implicit functions as <a>dim</a>, <tt>dimMax</tt>, etc.
inSpaceOf :: a ds -> b ds -> a ds

-- | Similar to <tt>asProxyTypeOf</tt>, Give a hint to type checker to fix
--   the type of a function argument.
asSpaceOf :: a ds -> (b ds -> c) -> (b ds -> c)
class Dimensions (ds :: [Nat])

-- | Dimensionality of our space
dim :: Dimensions ds => Dim ds

-- | This class gives the int associated with a type-level natural. Valid
--   known dim must be not less than 0.
class KnownDim (n :: Nat)

-- | Get value of type-level dim at runtime
dimVal' :: KnownDim n => Int

-- | A constraint family that makes sure all subdimensions are known.

-- | Map Dims onto XDims (injective)

-- | Map XDims onto Dims (injective)

-- | Treat Dims or XDims uniformly as XDims

-- | Treat Dims or XDims uniformly as Dims

-- | Unify usage of XNat and Nat. This is useful in function and type
--   definitions. Mainly used in the definition of Dim.

-- | Constraint on kinds; makes sure that the second argument kind is Nat
--   if the first is a list of Nats.

-- | FixedDim tries not to inspect content of <tt>ns</tt> and construct it
--   based only on <tt>xns</tt> when it is possible. This means it does not
--   check if `XN m &lt;= n`.

-- | FixedXDim tries not to inspect content of <tt>xns</tt> and construct
--   it based only on <tt>ns</tt> when it is possible. This means it does
--   not check if `XN m &lt;= n`.

-- | WrapNat tries not to inspect content of <tt>xn</tt> and construct it
--   based only on <tt>n</tt> when it is possible. This means it does not
--   check if `XN m &lt;= n`.

-- | Synonym for (:+) that treats Nat values 0 and 1 in a special way: it
--   preserves the property that all dimensions are greater than 1.

-- | Synonym for (+:) that treats Nat values 0 and 1 in a special way: it
--   preserves the property that all dimensions are greater than 1.

-- | Infer <a>Dimensions</a> given that the list is KnownDims and finite
inferDimensions :: forall (ds :: [Nat]). (KnownDims ds, FiniteList ds) => Evidence (Dimensions ds)

-- | <a>Dimensions</a> implies <a>KnownDims</a>
inferDimKnownDims :: forall (ds :: [Nat]). Dimensions ds => Evidence (KnownDims ds)

-- | <a>Dimensions</a> implies <a>FiniteList</a>
inferDimFiniteList :: forall (ds :: [Nat]). Dimensions ds => Evidence (FiniteList ds)

-- | Infer that tail list is also Dimensions
inferTailDimensions :: forall (ds :: [Nat]). Dimensions ds => Maybe (Evidence (Dimensions (Tail ds)))

-- | Infer that concatenation is also Dimensions
inferConcatDimensions :: forall as bs. (Dimensions as, Dimensions bs) => Evidence (Dimensions (as ++ bs))

-- | Infer that prefix is also Dimensions
inferPrefixDimensions :: forall bs asbs. (IsSuffix bs asbs ~ True, Dimensions bs, Dimensions asbs) => Evidence (Dimensions (Prefix bs asbs))

-- | Infer that suffix is also Dimensions
inferSuffixDimensions :: forall as asbs. (IsPrefix as asbs ~ True, Dimensions as, Dimensions asbs) => Evidence (Dimensions (Suffix as asbs))

-- | Make snoc almost as good as cons
inferSnocDimensions :: forall xs z. (KnownDim z, Dimensions xs) => Evidence (Dimensions (xs +: z))

-- | Init of the list is also Dimensions
inferInitDimensions :: forall xs. Dimensions xs => Maybe (Evidence (Dimensions (Init xs)))

-- | Take KnownDim of the list is also Dimensions
inferTakeNDimensions :: forall n xs. (KnownDim n, Dimensions xs) => Evidence (Dimensions (Take n xs))

-- | Drop KnownDim of the list is also Dimensions
inferDropNDimensions :: forall n xs. (KnownDim n, Dimensions xs) => Evidence (Dimensions (Drop n xs))

-- | Reverse of the list is also Dimensions
inferReverseDimensions :: forall xs. Dimensions xs => Evidence (Dimensions (Reverse xs))

-- | Use the given `Dim ds` to create an instance of `Dimensions ds`
--   dynamically.
reifyDimensions :: forall (ds :: [Nat]). Dim ds -> Evidence (Dimensions ds)

-- | Init of the dimension list is also Dimensions, and the last dimension
--   is KnownDim.
inferUnSnocDimensions :: forall ds. Dimensions ds => Maybe (Evidence (SnocDimensions ds))

-- | Various evidence for the Snoc operation.
type SnocDimensions (xs :: [Nat]) = (xs ~ (Init xs +: Last xs), xs ~ (Init xs ++ '[Last xs]), IsPrefix (Init xs) xs ~ True, IsSuffix '[Last xs] xs ~ True, Suffix (Init xs) xs ~ '[Last xs], Prefix '[Last xs] xs ~ Init xs, Dimensions (Init xs), KnownDim (Last xs))

-- | Tail of the dimension list is also Dimensions, and the head dimension
--   is KnownDim.
inferUnConsDimensions :: forall ds. Dimensions ds => Maybe (Evidence (ConsDimensions ds))

-- | Various evidence for the Snoc operation.
type ConsDimensions (xs :: [Nat]) = (xs ~ (Head xs :+ Tail xs), xs ~ ('[Head xs] ++ Tail xs), IsPrefix '[Head xs] xs ~ True, IsSuffix (Tail xs) xs ~ True, Suffix '[Head xs] xs ~ Tail xs, Prefix (Tail xs) xs ~ '[Head xs], Dimensions (Tail xs), KnownDim (Head xs))
instance forall k (ds :: k). GHC.Show.Show (Numeric.Dimensions.Dim.Dim ds)
instance GHC.Show.Show Numeric.Dimensions.Dim.SomeDims
instance forall k (ds :: k). GHC.Classes.Eq (Numeric.Dimensions.Dim.Dim ds)
instance GHC.Classes.Eq Numeric.Dimensions.Dim.SomeDims
instance forall k (ds :: k). GHC.Classes.Ord (Numeric.Dimensions.Dim.Dim ds)
instance GHC.Classes.Ord Numeric.Dimensions.Dim.SomeDims
instance Numeric.Dimensions.Dim.Dimensions '[]
instance (Numeric.TypeLits.KnownDim d, Numeric.Dimensions.Dim.Dimensions ds) => Numeric.Dimensions.Dim.Dimensions (d : ds)
instance Numeric.Dimensions.Dim.Dimensions ds => GHC.Enum.Bounded (Numeric.Dimensions.Dim.Dim ds)


-- | Provides a data type Idx that enumerates through multiple dimensions.
--   Lower indices go first, i.e. assumed enumeration is i = i1 + i2*n1 +
--   i3*n1*n2 + ... + ik*n1*n2*...*n(k-1). This is also to encourage
--   column-first matrix enumeration and array layout.
module Numeric.Dimensions.Idx

-- | Type-level dimensional indexing with arbitrary Int values inside
data Idx (ds :: [Nat])

-- | Zero-rank dimensionality - scalar
[Z] :: Idx '[]

-- | List-like concatenation of indices
[:!] :: {-# UNPACK #-} !Int -> !(Idx ds) -> Idx (d : ds)

-- | Append index dimension
appendIdx :: forall (as :: [Nat]) (b :: Nat). Idx as -> Int -> Idx (as +: b)

-- | Split index into prefix and suffix dimensioned indices
splitIdx :: forall (as :: [Nat]) (bs :: [Nat]). FiniteList as => Idx (as ++ bs) -> (Idx as, Idx bs)
instance GHC.Show.Show (Numeric.Dimensions.Idx.Idx ds)
instance GHC.Classes.Eq (Numeric.Dimensions.Idx.Idx ds)
instance GHC.Num.Num (Numeric.Dimensions.Idx.Idx '[n])
instance GHC.Classes.Ord (Numeric.Dimensions.Idx.Idx ds)
instance Numeric.Dimensions.Dim.Dimensions ds => GHC.Enum.Bounded (Numeric.Dimensions.Idx.Idx ds)
instance GHC.Exts.IsList (Numeric.Dimensions.Idx.Idx ds)
instance Numeric.Dimensions.Dim.Dimensions ds => GHC.Enum.Enum (Numeric.Dimensions.Idx.Idx ds)


-- | Map a function over all dimensions provided dimension indices or
--   offsets.
module Numeric.Dimensions.Traverse

-- | Traverse over all dimensions keeping track of index and offset
overDim# :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> State# s -> (# State# s, a #)) -> Int# -> Int# -> a -> State# s -> (# State# s, a #)

-- | Same as overDim#, but with no return value
overDim_# :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> State# s -> State# s) -> Int# -> Int# -> State# s -> State# s

-- | Traverse over all dimensions keeping track of indices
overDimIdx# :: Dim (ds :: [Nat]) -> (Idx ds -> a -> State# s -> (# State# s, a #)) -> a -> State# s -> (# State# s, a #)

-- | Traverse over all dimensions keeping track of indices, with no return
--   value
overDimIdx_# :: Dim (ds :: [Nat]) -> (Idx ds -> State# s -> State# s) -> State# s -> State# s

-- | Traverse over all dimensions keeping track of total offset
overDimOff# :: Dim (ds :: [Nat]) -> (Int# -> a -> State# s -> (# State# s, a #)) -> Int# -> Int# -> a -> State# s -> (# State# s, a #)

-- | Traverse over all dimensions keeping track of total offset, with not
--   return value
overDimOff_# :: Dim (ds :: [Nat]) -> (Int# -> State# s -> State# s) -> Int# -> Int# -> State# s -> State# s

-- | Traverse from the first index to the second index in each dimension.
--   Indices must be within Dim range, which is not checked. You can
--   combine positive and negative traversal directions along different
--   dimensions.
overDimPart# :: forall (ds :: [Nat]) a s. Dimensions ds => Idx ds -> Idx ds -> (Idx ds -> Int# -> a -> State# s -> (# State# s, a #)) -> Int# -> Int# -> a -> State# s -> (# State# s, a #)

-- | Fold over all dimensions keeping track of index and offset
foldDim :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> a) -> Int# -> Int# -> a -> a

-- | Fold all dimensions keeping track of indices
foldDimIdx :: Dim (ds :: [Nat]) -> (Idx ds -> a -> a) -> a -> a

-- | Fold over all dimensions keeping track of total offset
foldDimOff :: Dim (ds :: [Nat]) -> (Int# -> a -> a) -> Int# -> Int# -> a -> a

-- | Fold over all dimensions in reverse order keeping track of index and
--   offset
foldDimReverse :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> a) -> Int# -> Int# -> a -> a

-- | Fold all dimensions in reverse order keeping track of indices
foldDimReverseIdx :: Dim (ds :: [Nat]) -> (Idx ds -> a -> a) -> a -> a


-- | Map a function over all dimensions provided dimension indices or
--   offsets. This module provides a variant of traversal that lives in IO
--   monad.
module Numeric.Dimensions.Traverse.IO

-- | Traverse over all dimensions keeping track of index and offset
overDim :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> IO a) -> Int# -> Int# -> a -> IO a

-- | Same as overDim#, but with no return value
overDim_ :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> IO ()) -> Int# -> Int# -> IO ()

-- | Traverse over all dimensions keeping track of indices
overDimIdx :: Dim (ds :: [Nat]) -> (Idx ds -> a -> IO a) -> a -> IO a

-- | Traverse over all dimensions keeping track of indices, with no return
--   value
overDimIdx_ :: Dim (ds :: [Nat]) -> (Idx ds -> IO ()) -> IO ()

-- | Traverse over all dimensions keeping track of total offset
overDimOff :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> IO a) -> Int# -> Int# -> a -> IO a

-- | Traverse over all dimensions keeping track of total offset, with not
--   return value
overDimOff_ :: Dim (ds :: [Nat]) -> (Int# -> IO ()) -> Int# -> Int# -> IO ()

-- | Traverse from the first index to the second index in each dimension.
--   Indices must be within Dim range, which is not checked. You can
--   combine positive and negative traversal directions along different
--   dimensions.
overDimPart :: forall (ds :: [Nat]) a. Dimensions ds => Idx ds -> Idx ds -> (Idx ds -> Int# -> a -> IO a) -> Int# -> Int# -> a -> IO a

-- | Fold over all dimensions keeping track of index and offset
foldDim :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> a) -> Int# -> Int# -> a -> a

-- | Fold all dimensions keeping track of indices
foldDimIdx :: Dim (ds :: [Nat]) -> (Idx ds -> a -> a) -> a -> a

-- | Fold over all dimensions keeping track of total offset
foldDimOff :: Dim (ds :: [Nat]) -> (Int# -> a -> a) -> Int# -> Int# -> a -> a


-- | Map a function over all dimensions provided dimension indices or
--   offsets. This module provides a variant of traversal that lives in ST
--   monad.
module Numeric.Dimensions.Traverse.ST

-- | Traverse over all dimensions keeping track of index and offset
overDim :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> ST s a) -> Int# -> Int# -> a -> ST s a

-- | Same as overDim#, but with no return value
overDim_ :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> ST s ()) -> Int# -> Int# -> ST s ()

-- | Traverse over all dimensions keeping track of indices
overDimIdx :: Dim (ds :: [Nat]) -> (Idx ds -> a -> ST s a) -> a -> ST s a

-- | Traverse over all dimensions keeping track of indices, with no return
--   value
overDimIdx_ :: Dim (ds :: [Nat]) -> (Idx ds -> ST s ()) -> ST s ()

-- | Traverse over all dimensions keeping track of total offset
overDimOff :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> ST s a) -> Int# -> Int# -> a -> ST s a

-- | Traverse over all dimensions keeping track of total offset, with not
--   return value
overDimOff_ :: Dim (ds :: [Nat]) -> (Int# -> ST s ()) -> Int# -> Int# -> ST s ()

-- | Traverse from the first index to the second index in each dimension.
--   Indices must be within Dim range, which is not checked. You can
--   combine positive and negative traversal directions along different
--   dimensions.
overDimPart :: forall (ds :: [Nat]) a s. Dimensions ds => Idx ds -> Idx ds -> (Idx ds -> Int# -> a -> ST s a) -> Int# -> Int# -> a -> ST s a

-- | Fold over all dimensions keeping track of index and offset
foldDim :: Dim (ds :: [Nat]) -> (Idx ds -> Int# -> a -> a) -> Int# -> Int# -> a -> a

-- | Fold all dimensions keeping track of indices
foldDimIdx :: Dim (ds :: [Nat]) -> (Idx ds -> a -> a) -> a -> a

-- | Fold over all dimensions keeping track of total offset
foldDimOff :: Dim (ds :: [Nat]) -> (Int# -> a -> a) -> Int# -> Int# -> a -> a


-- | Some dimensions in a type-level dimension list may by not known at
--   compile time.
module Numeric.Dimensions.XDim

-- | Similar to SomeNat, hide some dimensions under an existential
--   constructor. In contrast to SomeDim, it preserves the order of
--   dimensions, and it can keep some of the dimensions in the list static
--   while making other dimensions known only at runtime.
data XDim (xns :: [XNat])
XDim :: (Dim ns) -> XDim

-- | Loose compile-time information about dimensionalities
xdim :: forall (ds :: [Nat]) (xds :: [XNat]). (Dimensions ds, XDimensions xds) => Maybe (Dim xds)

-- | Construct dimensionality at runtime
xDimVal :: Dim (xns :: [XNat]) -> XDim xns
class XDimensions (xds :: [XNat])
wrapDim :: XDimensions xds => Dim (ds :: [Nat]) -> Maybe (Dim xds)
instance Numeric.Dimensions.XDim.XDimensions '[]
instance (Numeric.Dimensions.XDim.XDimensions xs, Numeric.TypeLits.KnownDim m) => Numeric.Dimensions.XDim.XDimensions (Numeric.TypeLits.XN m : xs)
instance (Numeric.Dimensions.XDim.XDimensions xs, Numeric.TypeLits.KnownDim n) => Numeric.Dimensions.XDim.XDimensions (Numeric.TypeLits.N n : xs)
instance GHC.Show.Show (Numeric.Dimensions.XDim.XDim xns)
instance GHC.Classes.Eq (Numeric.Dimensions.XDim.XDim xds)
instance GHC.Classes.Ord (Numeric.Dimensions.XDim.XDim xds)


-- | Provides a set of data types to define and traverse through multiple
--   dimensions. The core types are `Dim ds` and `Idx ds`, which fix
--   dimension sizes at compile time.
--   
--   Lower indices go first, i.e. assumed enumeration is i = i1 + i2*n1 +
--   i3*n1*n2 + ... + ik*n1*n2*...*n(k-1). This is also to encourage
--   column-first matrix enumeration and array layout.
module Numeric.Dimensions

-- | Bring an instance of certain class or constaint satisfaction evidence
--   into scope.
data Evidence :: Constraint -> Type
[Evidence] :: a => Evidence a
withEvidence :: Evidence a -> (a => r) -> r
sumEvs :: Evidence a -> Evidence b -> Evidence (a, b)
(+!+) :: Evidence a -> Evidence b -> Evidence (a, b)
infixl 4 +!+