dimensions 0.3.2.0 → 1.0.0.0

raw patch · 24 files changed

+3107/−2203 lines, 24 filesdep −ghc-primdep ~CabalPVP ok

version bump matches the API change (PVP)

Dependencies removed: ghc-prim

Dependency ranges changed: Cabal

API changes (from Hackage documentation)

Files

• dimensions.cabal +26/−16
• src/Numeric/Dim.hs +446/−0
• src/Numeric/Dimensions.hs +13/−9
• src/Numeric/Dimensions/Dim.hs +0/−582
• src/Numeric/Dimensions/Dims.hs +405/−0
• src/Numeric/Dimensions/Fold.hs +334/−0
• src/Numeric/Dimensions/Idx.hs +0/−209
• src/Numeric/Dimensions/Idxs.hs +427/−0
• src/Numeric/Dimensions/List.hs +0/−436
• src/Numeric/Dimensions/Traverse.hs +0/−289
• src/Numeric/Dimensions/Traverse/IO.hs +0/−113
• src/Numeric/Dimensions/Traverse/ST.hs +0/−113
• src/Numeric/Dimensions/XDim.hs +0/−118
• src/Numeric/Tuple.hs +35/−0
• src/Numeric/Tuple/Lazy.hs +320/−0
• src/Numeric/Tuple/Strict.hs +320/−0
• src/Numeric/Type/Evidence.hs +59/−0
• src/Numeric/Type/List.hs +222/−0
• src/Numeric/TypeLits.hs +0/−192
• src/Numeric/TypedList.hs +343/−0
• test/Numeric/DimTest.hs +86/−0
• test/Numeric/Dimensions/DimsTest.hs +67/−0
• test/Numeric/Dimensions/ListTest.hs +0/−124
• test/Spec.hs +4/−2

@@ -1,6 +1,6 @@ name: dimensions-version: 0.3.2.0-cabal-version: >=1.20+version: 1.0.0.0+cabal-version: >=1.22 build-type: Simple license: BSD3 license-file: LICENSE@@ -19,24 +19,33 @@     subdir: dimensions  +flag unsafeindices+    description:+        Disable bound checks on Idx and Idxs types.+    default: False++ library +    if flag(unsafeindices)+        cpp-options: -DUNSAFE_INDICES     exposed-modules:+        Numeric.Dim+        Numeric.Tuple+        Numeric.Tuple.Lazy+        Numeric.Tuple.Strict+        Numeric.Type.Evidence+        Numeric.Type.List+        Numeric.TypedList         Numeric.Dimensions-        Numeric.Dimensions.Dim-        Numeric.Dimensions.XDim-        Numeric.Dimensions.Idx-        Numeric.Dimensions.List-        Numeric.Dimensions.Traverse-        Numeric.Dimensions.Traverse.IO-        Numeric.Dimensions.Traverse.ST-        Numeric.TypeLits+        Numeric.Dimensions.Dims+        Numeric.Dimensions.Idxs+        Numeric.Dimensions.Fold     build-depends:-        base >=4.9 && <5,-        ghc-prim >= 0.5+        base >=4.9 && <5     default-language: Haskell2010     hs-source-dirs: src-    ghc-options: -Wall -fwarn-tabs -O2+    ghc-options: -Wall   test-suite dimensions-test@@ -44,12 +53,13 @@     type: exitcode-stdio-1.0     main-is: Spec.hs     other-modules:-        Numeric.Dimensions.ListTest+        Numeric.DimTest+        Numeric.Dimensions.DimsTest     build-depends:         base -any,-        Cabal >=1.20,+        Cabal -any,         QuickCheck -any,         dimensions -any     default-language: Haskell2010     hs-source-dirs: test-    ghc-options: -Wall -fwarn-tabs -O2+    ghc-options: -Wall

@@ -0,0 +1,446 @@+{-# LANGUAGE AllowAmbiguousTypes   #-}+{-# LANGUAGE CPP                   #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE ExplicitNamespaces    #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE MagicHash             #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE Rank2Types            #-}+{-# LANGUAGE RoleAnnotations       #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE Strict                #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE ViewPatterns          #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Dim+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+-- This module is based on `GHC.TypeLits` and re-exports its functionality.+-- It provides `KnownDim` class that is similar to `KnownNat`, but keeps+-- `Int`s instead of `Integer`s;+-- Also it provides `Dim` data family serving as a customized `Proxy` type+-- and 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.+--+-----------------------------------------------------------------------------+module Numeric.Dim+  ( -- * Type level numbers that can be unknown.+    XNat (..), XN, N, XNatType (..)+    -- * Term level dimension+  , Dim (Dim, D, Dn, Dx), SomeDim+  , KnownDim (..), KnownXNatType (..)+  , dimVal, dimVal', someDimVal+  , sameDim, sameDim'+  , compareDim, compareDim'+  , constrain, 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+    -- * Re-export part of `GHC.TypeLits` for convenience+  , Nat, CmpNat, type (+), type (-), type (*), type (^)+  , MinDim, FixedDim, inferDimLE+    -- * Inferring kind of type-level dimension+  , KnownDimKind (..), DimKind (..)+  ) where+++import           Data.Type.Bool+import           Data.Type.Equality+import           GHC.Base           (Type)+import           GHC.Exts           (Constraint, Proxy#, proxy#, unsafeCoerce#)+import           GHC.TypeLits++import           Numeric.Type.Evidence+++-- | 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 (n::Nat) = 'XN n+-- | Known natural number+type N (n::Nat) = 'N n++-- | Find out whether @XNat@ is of known or constrained type.+data XNatType :: XNat -> Type where+  -- | Given @XNat@ is known+  Nt  :: XNatType ('N n)+  -- | Given @XNat@ is constrained unknown+  XNt :: XNatType ('XN m)++-- | Same as `SomeNat`+type SomeDim = Dim ('XN 0)++-- | 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+-- Starting from GHC 8.2, compiler supports specifying lists of complete+-- pattern synonyms.+#if __GLASGOW_HASKELL__ >= 802+{-# COMPLETE D #-}+{-# COMPLETE Dn, Dx #-}+{-# COMPLETE Dim #-}+#endif+++-- | Independently of the kind of type-level number,+--   construct an instance of `KnownDim` from it.+--+--   Match against this pattern to bring `KnownDim` instance into scope+--   when you don't know the kind of the @Dim@ parameter.+pattern Dim :: forall (n :: k) . () => KnownDim n => Dim n+pattern Dim <- (dimEv -> E)+  where+    Dim = dim @_ @n+++-- | Same as @Dim@ pattern, but constrained to @Nat@ kind.+pattern D :: forall (n :: Nat) . () => KnownDim n => Dim n+pattern D <- (dimEv -> E)+  where+    D = dim @_ @n++-- | Statically known `XNat`+pattern Dn :: forall (xn :: XNat) . KnownXNatType xn+           => forall (n :: Nat) . (KnownDim n, xn ~ 'N n) => Dim n -> Dim xn+pattern Dn k <- (dimXNEv (xNatType @xn) -> PatN k)+  where+    Dn k = unsafeCoerce# k++-- | `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 :: forall (xn :: XNat) . KnownXNatType xn+           => forall (n :: Nat) (m :: Nat)+            . (KnownDim n, MinDim m n, xn ~ 'XN m) => Dim n -> Dim xn+pattern Dx k <- (dimXNEv (xNatType @xn) -> PatXN k)+  where+    Dx k = unsafeCoerce# k++-- | This class provides the `Dim` associated with a type-level natural.+class KnownDim (n :: k) where+    -- | Get value of type-level dim at runtime.+    --+    --   Note, this function is supposed to be used with @TypeApplications@,+    --   and the @KnownDim@ class has varying kind of the parameter;+    --   thus, the function has two type paremeters (kind and type of @n@).+    --   For example, you can type:+    --+    --   >>>:set -XTypeApplications+    --   >>>:set -XDataKinds+    --   >>>:t dim @Nat @3+    --   dim @Nat @3 :: Dim 3+    --+    --   >>>:set -XTypeOperators+    --   >>>:t dim @_ @(13 - 6)+    --   dim @_ @(13 - 6) :: Dim 7+    --+    --+    --   >>>:t dim @_ @(N 17)+    --   dim @_ @(N 17) :: Dim (N 17)+    --+    dim :: Dim n+++-- | Find out the type of `XNat` constructor+class KnownXNatType (n :: XNat) where+  -- | Pattern-match against this to out the type of `XNat` constructor+  xNatType :: XNatType n++instance KnownXNatType ('N n) where+  xNatType = Nt+  {-# INLINE xNatType #-}++instance KnownXNatType ('XN n) where+  xNatType = XNt+  {-# INLINE xNatType #-}+++-- | Similar to `natVal` from `GHC.TypeLits`, but returns `Word`.+dimVal :: Dim (x :: k) -> Word+dimVal = unsafeCoerce#+{-# INLINE dimVal #-}++-- | Similar to `natVal` from `GHC.TypeLits`, but returns `Word`.+dimVal' :: forall n . KnownDim n => Word+dimVal' = unsafeCoerce# (dim @_ @n)+{-# INLINE dimVal' #-}++-- | Friendly error message if `m <= n` constraint is not satisfied.+--   Use this type family instead of @(<=)@ if possible+--   or try `inferDimLE` function as the last resort.+type family MinDim (m :: Nat) (n :: Nat) :: Constraint where+  MinDim m n =+    If (CmpNat m n == 'GT)+       (TypeError+         ('Text "Minimum Dim size constraint ("+            ':<>: 'ShowType m+            ':<>: 'Text " <= "+            ':<>: 'ShowType n+            ':<>: 'Text ") is not satisfied."+         ':$$: 'Text "Minimum Dim: " ':<>: 'ShowType m+         ':$$: 'Text " Actual Dim: " ':<>: 'ShowType n+         ) :: Constraint+       )+       (m <= n)++-- | 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 = MinDim m b++instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where+    {-# INLINE dim #-}+    dim = DimSing (fromInteger (natVal' (proxy# :: Proxy# n)))++instance {-# OVERLAPPING #-} KnownDim 0  where+  { {-# INLINE dim #-}; dim = DimSing 0 }+instance {-# OVERLAPPING #-} KnownDim 1  where+  { {-# INLINE dim #-}; dim = DimSing 1 }+instance {-# OVERLAPPING #-} KnownDim 2  where+  { {-# INLINE dim #-}; dim = DimSing 2 }+instance {-# OVERLAPPING #-} KnownDim 3  where+  { {-# INLINE dim #-}; dim = DimSing 3 }+instance {-# OVERLAPPING #-} KnownDim 4  where+  { {-# INLINE dim #-}; dim = DimSing 4 }+instance {-# OVERLAPPING #-} KnownDim 5  where+  { {-# INLINE dim #-}; dim = DimSing 5 }+instance {-# OVERLAPPING #-} KnownDim 6  where+  { {-# INLINE dim #-}; dim = DimSing 6 }+instance {-# OVERLAPPING #-} KnownDim 7  where+  { {-# INLINE dim #-}; dim = DimSing 7 }+instance {-# OVERLAPPING #-} KnownDim 8  where+  { {-# INLINE dim #-}; dim = DimSing 8 }+instance {-# OVERLAPPING #-} KnownDim 9  where+  { {-# INLINE dim #-}; dim = DimSing 9 }+instance {-# OVERLAPPING #-} KnownDim 10 where+  { {-# INLINE dim #-}; dim = DimSing 10 }+instance {-# OVERLAPPING #-} KnownDim 11 where+  { {-# INLINE dim #-}; dim = DimSing 11 }+instance {-# OVERLAPPING #-} KnownDim 12 where+  { {-# INLINE dim #-}; dim = DimSing 12 }+instance {-# OVERLAPPING #-} KnownDim 13 where+  { {-# INLINE dim #-}; dim = DimSing 13 }+instance {-# OVERLAPPING #-} KnownDim 14 where+  { {-# INLINE dim #-}; dim = DimSing 14 }+instance {-# OVERLAPPING #-} KnownDim 15 where+  { {-# INLINE dim #-}; dim = DimSing 15 }+instance {-# OVERLAPPING #-} KnownDim 16 where+  { {-# INLINE dim #-}; dim = DimSing 16 }+instance {-# OVERLAPPING #-} KnownDim 17 where+  { {-# INLINE dim #-}; dim = DimSing 17 }+instance {-# OVERLAPPING #-} KnownDim 18 where+  { {-# INLINE dim #-}; dim = DimSing 18 }+instance {-# OVERLAPPING #-} KnownDim 19 where+  { {-# INLINE dim #-}; dim = DimSing 19 }+instance {-# OVERLAPPING #-} KnownDim 20 where+  { {-# INLINE dim #-}; dim = DimSing 20 }++instance KnownDim n => KnownDim ('N n) where+    {-# INLINE dim #-}+    dim = unsafeCoerce# (dim @Nat @n)++-- | Similar to `someNatVal` from `GHC.TypeLits`.+someDimVal :: Word -> SomeDim+someDimVal = unsafeCoerce#+{-# INLINE someDimVal #-}+++-- | Change the minimum allowed size of a @Dim (XN x)@,+--   while testing if the value inside satisfies it.+constrain :: forall (m :: Nat) x . KnownDim m+          => Dim x -> Maybe (Dim (XN m))+constrain (DimSing x) | dimVal' @m > x = Nothing+                      | otherwise      = Just (unsafeCoerce# x)+{-# INLINE constrain #-}++-- | `constrain` with explicitly-passed constraining @Dim@+--   to avoid @AllowAmbiguousTypes@.+constrainBy :: forall m x . Dim m -> Dim x -> Maybe (Dim (XN m))+constrainBy D = constrain @m+#if __GLASGOW_HASKELL__ < 802+constrainBy _ = error "Dim: Impossible pattern."+#endif++-- | Decrease minimum allowed size of a @Dim (XN x)@.+relax :: forall (m :: Nat) (n :: Nat) . (MinDim m n) => Dim (XN n) -> Dim (XN m)+relax = unsafeCoerce#+{-# 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 (Evidence (x ~ y))+sameDim (DimSing a) (DimSing b)+  | a == b    = Just (unsafeCoerce# (E @(x ~ x)))+  | otherwise = 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) p q+          . (KnownDim x, KnownDim y)+         => p x -> q y -> Maybe (Evidence (x ~ y))+sameDim' _ _ = sameDim' (dim @Nat @x) (dim @Nat @y)+{-# INLINE sameDim' #-}++-- | Ordering of dimension values.+compareDim :: Dim a -> Dim b -> Ordering+compareDim = unsafeCoerce# (compare :: Word -> Word -> Ordering)+{-# INLINE compareDim #-}+++-- | Ordering of dimension values.+compareDim' :: forall a b p q+             . (KnownDim a, KnownDim b) => p a -> q b -> Ordering+compareDim' _ _ = compareDim (dim @_ @a)  (dim @_ @b)+{-# INLINE compareDim' #-}+++instance Eq (Dim (n :: Nat)) where+    _ == _ = True+    {-# INLINE (==) #-}++instance Eq (Dim (x :: XNat)) where+    DimSing a == DimSing b = a == b+    {-# INLINE (==) #-}++instance Ord (Dim (n :: Nat)) where+    compare _ _ = EQ+    {-# INLINE compare #-}++instance Ord (Dim (x :: XNat)) where+    compare = compareDim+    {-# INLINE compare #-}++instance Show (Dim x) where+    showsPrec p = showsPrec p . dimVal+    {-# INLINE showsPrec #-}++instance KnownDim m => Read (Dim ('XN m)) where+    readsPrec p xs = do (a,ys) <- readsPrec p xs+                        case constrain (someDimVal a) of+                          Nothing -> []+                          Just n  -> [(n,ys)]+++++plusDim :: Dim n -> Dim m -> Dim (n + m)+plusDim (DimSing a) (DimSing b) = unsafeCoerce# (a + b)+{-# INLINE plusDim #-}++minusDim :: MinDim m n => Dim n -> Dim m -> Dim (n - m)+minusDim (DimSing a) (DimSing b) = unsafeCoerce# (a - b)+{-# INLINE minusDim #-}++minusDimM :: Dim n -> Dim m -> Maybe (Dim (n - m))+minusDimM (DimSing a) (DimSing b)+  | a >= b    = Just (unsafeCoerce# (a - b))+  | otherwise = Nothing+{-# INLINE minusDimM #-}++timesDim :: Dim n -> Dim m -> Dim ((*) n m)+timesDim (DimSing a) (DimSing b) = unsafeCoerce# (a * b)+{-# INLINE timesDim #-}++powerDim :: Dim n -> Dim m -> Dim ((^) n m)+powerDim (DimSing a) (DimSing b) = unsafeCoerce# (a ^ b)+{-# INLINE powerDim #-}+++-- | @MinDim@ implies @(<=)@, but this fact is not so clear to GHC.+--   This function assures the type system that the relation takes place.+inferDimLE :: forall m n . MinDim m n => Evidence (m <= n)+inferDimLE = unsafeCoerce# (E @(n <= n))+++-- | GADT to support `KnownDimKind` type class.+--   Match against its constructors to know if @k@ is @Nat@ or @XNat@+data DimKind :: Type -> Type where+    -- | Working on @Nat@.+    DimNat  :: DimKind Nat+    -- | Working on @XNat@.+    DimXNat :: DimKind XNat++-- | Figure out whether the type-level dimension is `Nat` or `XNat`.+--   Useful for generalized inference functions.+class KnownDimKind k where+    dimKind :: DimKind k++instance KnownDimKind Nat where+    dimKind = DimNat++instance KnownDimKind XNat where+    dimKind = DimXNat++--------------------------------------------------------------------------------++-- | 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 r d . Dim d -> (KnownDim d => r) -> r+reifyDim d k = unsafeCoerce# (MagicDim k :: MagicDim d r) d+{-# INLINE reifyDim #-}+newtype MagicDim d r = MagicDim (KnownDim d => r)++dimEv :: Dim d -> Evidence (KnownDim d)+dimEv d = reifyDim d E+{-# INLINE dimEv #-}++data PatXDim (xn :: XNat) where+  PatN :: KnownDim n => Dim n -> PatXDim ('N n)+  PatXN :: (KnownDim n, MinDim m n) => Dim n -> PatXDim ('XN m)++dimXNEv :: forall (xn :: XNat) . XNatType xn -> Dim xn -> PatXDim xn+dimXNEv Nt (DimSing k) = reifyDim dd (PatN dd)+  where+    dd = DimSing @Nat @_ k+dimXNEv XNt xn@(DimSing k) = reifyDim dd (f dd xn)+  where+    dd = DimSing @Nat @_ k+    f :: forall (d :: Nat) (m :: Nat)+       . KnownDim d => Dim d -> Dim ('XN m) -> PatXDim ('XN m)+    f d _ = case ( unsafeCoerce# (E @((CmpNat m m == 'GT) ~ 'False, m <= m))+                :: Evidence ((CmpNat m d == 'GT) ~ 'False, m <= d)+               ) of+      E -> PatXN d+{-# INLINE dimXNEv #-}

@@ -7,7 +7,7 @@ -- Maintainer  :  chirkin@arch.ethz.ch -- -- 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.+-- The core types are `Dims ds` and `Idxs 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).@@ -16,13 +16,17 @@ -----------------------------------------------------------------------------  module Numeric.Dimensions-  ( module Numeric.Dimensions.List-  , module Numeric.Dimensions.Dim-  , module Numeric.Dimensions.Idx-  , Evidence (..), withEvidence, sumEvs, (+!+)+  ( module Numeric.Dim+  , module Numeric.Dimensions.Dims+  , module Numeric.Dimensions.Idxs+  , module Numeric.Dimensions.Fold+  , module Numeric.Type.Evidence+  , module Numeric.Type.List   ) where -import Numeric.Dimensions.List-import Numeric.Dimensions.Dim-import Numeric.Dimensions.Idx-import Numeric.TypeLits+import Numeric.Dim+import Numeric.Dimensions.Dims+import Numeric.Dimensions.Idxs+import Numeric.Dimensions.Fold+import Numeric.Type.Evidence+import Numeric.Type.List

@@ -1,582 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes       #-}-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces        #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE FlexibleInstances         #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE MagicHash                 #-}-{-# LANGUAGE MultiParamTypeClasses     #-}-{-# LANGUAGE PolyKinds                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE RoleAnnotations           #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeFamilies              #-}-{-# LANGUAGE TypeFamilyDependencies    #-}-{-# LANGUAGE TypeInType                #-}-{-# LANGUAGE TypeOperators             #-}-{-# LANGUAGE UndecidableInstances      #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.Dim--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ 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-  ( -- * Dimension data types-    Nat, XNat, XN, N, Dim (..), dimVal, totalDim, fromInt-  , SomeDims (..), SomeDim (..), someDimVal, someDimsVal, sameDim, compareDim-  , inSpaceOf, asSpaceOf-    -- * Dimension constraints-  , Dimensions (..), KnownDim (..), KnownDims-    -- * Type-level programming-    --   Provide type families to work with lists of dimensions (`[Nat]` or `[XNat]`)-  , AsXDims, AsDims, WrapDims, UnwrapDims-  , ConsDim, NatKind-  , FixedDim, FixedXDim, WrapNat, type (:<), type (>:)-    -- * Inference of dimension evidence-  , inferDimensions, inferDimKnownDims, inferDimFiniteList-  , inferTailDimensions, inferConcatDimensions-  , inferPrefixDimensions, inferSuffixDimensions-  , inferSnocDimensions, inferInitDimensions-  , inferTakeNDimensions, inferDropNDimensions-  , inferReverseDimensions, reifyDimensions-    -- * Cons and Snoc inference-    --   Very useful functions when you need some evidence for contraction ops.-  , inferUnSnocDimensions, SnocDimensions-  , inferUnConsDimensions, ConsDimensions-  ) where--import           Data.Maybe              (isJust)-import           GHC.Exts                (Constraint, unsafeCoerce#)-import           Data.Type.Equality      ((:~:)(..))--import           Numeric.Dimensions.List-import           Numeric.TypeLits----- | Type-level dimensionality-data Dim (ns :: k) where-  -- | 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)-infixr 5 :*---- | 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))-fromInt i | i < dimVal' @m = Nothing-          | otherwise      = do-  SomeDim (dn :: Dim n) <- someDimVal i-  return $ case unsafeEqEvidence @(m <=? n) @'True of-      Evidence -> Dx dn-{-# INLINE fromInt #-}------ | Same as SomeNat, but for Dimension:---   Hide all information about Dimension inside-data SomeDim = forall (n :: Nat) . SomeDim (Dim n)---- | Same as SomeNat, but for Dimensions:---   Hide all information about Dimensions inside-data SomeDims = forall (ns :: [Nat]) . SomeDims (Dim ns)---- | Get value of type-level dim at runtime.---   Gives a product of all dimensions if is a list.-dimVal :: Dim x -> Int-dimVal D                  = 1-dimVal (d :* ds)          = dimVal d * dimVal ds-dimVal (Dn :: Dim m)      = dimVal' @m-dimVal (Dx (Dn :: Dim m)) = dimVal' @m-{-# INLINE dimVal #-}---- | Product of all dimension sizes.-totalDim :: forall ds proxy . Dimensions ds => proxy ds -> Int-totalDim _ = dimVal (dim @ds)-{-# INLINE totalDim #-}---- | Similar to `someNatVal`, but for a single dimension-someDimVal :: Int -> Maybe SomeDim-someDimVal x | 0 > x     = Nothing-             | otherwise = Just (reifyDim x f)-  where-    f :: forall (n :: Nat) . KnownDim n => Proxy# n -> SomeDim-    f _ = SomeDim (Dn @n)-{-# INLINE someDimVal #-}---- | Convert a list of ints into unknown type-level Dimensions list-someDimsVal :: [Int] -> Maybe SomeDims-someDimsVal []             = Just $ SomeDims D-someDimsVal (x:xs) | 0 > x = Nothing-                   | otherwise = do-  SomeDim p <- someDimVal x-  SomeDims ps <- someDimsVal xs-  return $ SomeDims (p :* ps)-{-# INLINE someDimsVal #-}--dimList :: Dim ds -> String-dimList  D        = ""-dimList d@Dn      = show (dimVal d)-dimList (Dx d@Dn) = show (dimVal d)-dimList (d :* D)  = show (dimVal d)-dimList (d :* ds) = show (dimVal d) ++ ' ':dimList ds---- | We either get evidence that this function was instantiated with the--- same type-level Dimensions, or 'Nothing'.-sameDim :: Dim as -> Dim bs -> Maybe (Evidence (as ~ bs))-sameDim D D                 = Just Evidence-sameDim (a :* as) (b :* bs) | dimVal a == dimVal b = (unsafeCoerce# (Evidence @())) <$ sameDim as bs-                            | otherwise            = Nothing-sameDim _ _ = Nothing----- | 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-compareDim D D = EQ-compareDim _ D = GT-compareDim D _ = LT-compareDim (a :* as) (b :* bs) = compareDim as bs `mappend` compare (dimVal a) (dimVal b)-compareDim a@Dn b@Dn = compare (dimVal a) (dimVal b)-compareDim (Dx a) (Dx b) = compare (dimVal a) (dimVal b)-compareDim a@Dn (Dx b) = compare (dimVal a) (dimVal b)-compareDim (Dx a) b@Dn = compare (dimVal a) (dimVal b)-compareDim a@Dn (b :* bs) = compareDim D bs `mappend` compare (dimVal a) (dimVal b)-compareDim (Dx a) (b :* bs) = compareDim D bs `mappend` compare (dimVal a) (dimVal b)-compareDim (a :* as) b@Dn = compareDim as D `mappend` compare (dimVal a) (dimVal b)-compareDim (a :* as) (Dx b) = compareDim as D `mappend` compare (dimVal a) (dimVal b)----- | Similar to `const` or `asProxyTypeOf`;---   to be used on such implicit functions as `dim`, `dimMax`, etc.-inSpaceOf :: a ds -> b ds -> a ds-inSpaceOf x _ = x-{-# INLINE inSpaceOf #-}---- | Similar to `asProxyTypeOf`,---   Give a hint to type checker to fix the type of a function argument.-asSpaceOf :: a ds -> (b ds -> c) -> (b ds -> c)-asSpaceOf _ = id-{-# INLINE asSpaceOf #-}---instance Show (Dim ds) where-    show D  = "Dim Ø"-    show ds = "Dim " ++ dimList ds--instance Show SomeDims where-    show (SomeDims p) = "Some" ++ show p--instance Eq (Dim ds) where-    a == b = isJust $ sameDim a b--instance Eq SomeDims where-    SomeDims as == SomeDims bs = isJust $ sameDim as bs--instance Ord (Dim ds) where-    compare = compareDim--instance Ord SomeDims where-    compare (SomeDims as) (SomeDims bs) = compareDim as bs--class Dimensions (ds :: [Nat]) where-    -- | Dimensionality of our space-    dim :: Dim ds--instance Dimensions '[] where-    dim = D-    {-# INLINE dim #-}--instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds) where-    dim = Dn :* dim-    {-# INLINE dim #-}--instance Dimensions ds => Bounded (Dim ds) where-    maxBound = dim-    {-# INLINE maxBound #-}-    minBound = dim-    {-# INLINE minBound #-}-------------------------------------------------------------------------------------- * Type-level programming-------------------------------------------------------------------------------------- | Map Dims onto XDims (injective)-type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where-    AsXDims '[] = '[]-    AsXDims (n ': ns) = N n ': AsXDims ns---- | Map XDims onto Dims (injective)-type family AsDims (xns::[XNat]) = (ns :: [Nat]) | ns -> xns where-    AsDims '[] = '[]-    AsDims (N x ': xs) = x ': AsDims xs---- | Treat Dims or XDims uniformly as XDims-type family WrapDims (x::[k]) :: [XNat] where-    WrapDims ('[] :: [Nat])     = '[]-    WrapDims ('[] :: [XNat])    = '[]-    WrapDims (n ': ns :: [Nat]) = N n ': WrapDims ns-    WrapDims (xns :: [XNat])    = xns---- | Treat Dims or XDims uniformly as Dims-type family UnwrapDims (xns::[k]) :: [Nat] where-    UnwrapDims ('[] :: [Nat])  = '[]-    UnwrapDims ('[] :: [XNat]) = '[]-    UnwrapDims (N x ': xs)     = x ': UnwrapDims xs-    UnwrapDims (XN _ ': _)       = TypeError (-           'Text "Cannot unwrap dimension XN into Nat"-     ':$$: 'Text "(dimension is not known at compile time)"-     )---- | Unify usage of XNat and Nat.---   This is useful in function and type definitions.---   Mainly used in the definition of Dim.-type family ConsDim (x :: l) (xs :: [k]) = (ys :: [k]) | ys -> x xs l where-    ConsDim (x :: Nat) (xs :: [Nat])  = x    ': xs-    ConsDim (x :: Nat) (xs :: [XNat]) = N x  ': xs-    ConsDim (XN m)     (xs :: [XNat]) = XN m ': xs---- | Constraint on kinds;---   makes sure that the second argument kind is Nat if the first is a list of Nats.-type family NatKind ks k :: Constraint where-    NatKind [Nat]  l    = l ~ Nat-    NatKind [XNat] Nat  = ()-    NatKind [XNat] XNat = ()-    NatKind  ks    k    = ks ~ [k]---- | FixedDim tries not to inspect content of `ns` and construct it---   based only on `xns` when it is possible.---   This means it does not check if `XN m <= n`.-type family FixedDim (xns :: [XNat]) (ns :: [Nat]) :: [Nat] where-    FixedDim '[]          _  = '[]-    FixedDim (N n  ': xs) ns = n ': FixedDim xs (Tail ns)-    FixedDim (XN _ ': xs) ns = Head ns ': FixedDim xs (Tail ns)---- | FixedXDim tries not to inspect content of `xns` and construct it---   based only on `ns` when it is possible.---   This means it does not check if `XN m <= n`.-type family FixedXDim (xns :: [XNat]) (ns :: [Nat]) :: [XNat] where-    FixedXDim _  '[]       = '[]-    FixedXDim xs (n ': ns) = WrapNat (Head xs) n ': FixedXDim (Tail xs) ns---- | WrapNat tries not to inspect content of `xn` and construct it---   based only on `n` when it is possible.---   This means it does not check if `XN m <= n`.-type family WrapNat (xn :: XNat) (n :: Nat) :: XNat where-    WrapNat (XN m) n = XN m-    WrapNat  _     n = N 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.-type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where-    0 :< _  = '[]-    1 :< ns = ns-    n :< ns = n :+ ns-infixr 6 :<---- | Synonym for (+:) that treats Nat values 0 and 1 in a special way:---   it preserves the property that all dimensions are greater than 1.-type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where-    _  >: 0 = '[]-    ns >: 1 = ns-    ns >: n = ns +: n-infixl 6 >:---------------------------------------------------------------------------------------- * Inference of evidence------------------------------------------------------------------------------------- | Infer `Dimensions` given that the list is KnownDims and finite-inferDimensions :: forall (ds :: [Nat])-                 . (KnownDims ds, FiniteList ds)-                => Evidence (Dimensions ds)-inferDimensions = case tList @Nat @ds of-  TLEmpty -> Evidence-  TLCons _ (_ :: TypeList ds') -> case inferDimensions @ds' of-    Evidence -> Evidence-{-# INLINE inferDimensions #-}---- | `Dimensions` implies `KnownDims`-inferDimKnownDims :: forall (ds :: [Nat])-                   . Dimensions ds-                  => Evidence (KnownDims ds)-inferDimKnownDims = inferDimKnownDims' (dim @ds)-  where-    inferDimKnownDims' :: forall (ns :: [Nat]) . Dim ns -> Evidence (KnownDims ns)-    inferDimKnownDims' D = Evidence-    inferDimKnownDims' (Dn :* ds) = case inferDimKnownDims' ds of Evidence -> Evidence-{-# INLINE inferDimKnownDims #-}----- | `Dimensions` implies `FiniteList`-inferDimFiniteList :: forall (ds :: [Nat])-                    . Dimensions ds-                   => Evidence (FiniteList ds)-inferDimFiniteList = inferDimFiniteList' (dim @ds)-  where-    inferDimFiniteList' :: forall (ns :: [Nat]) . Dim ns -> Evidence (FiniteList ns)-    inferDimFiniteList' D = Evidence-    inferDimFiniteList' (Dn :* ds) = case inferDimFiniteList' ds of Evidence -> Evidence-{-# INLINE inferDimFiniteList #-}----- | Infer that tail list is also Dimensions-inferTailDimensions :: forall (ds :: [Nat])-                    . Dimensions ds-                    => Maybe (Evidence (Dimensions (Tail ds)))-inferTailDimensions = case dim @ds of-    D         -> Nothing-    Dn :* ds' -> Just $ reifyDimensions ds'-{-# INLINE inferTailDimensions #-}----- | Infer that concatenation is also Dimensions-inferConcatDimensions :: forall as bs-                       . (Dimensions as, Dimensions bs)-                      => Evidence (Dimensions (as ++ bs))-inferConcatDimensions = reifyDimensions $ magic (dim @as) (unsafeCoerce# $ dim @bs)-  where-    magic :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim ys-    magic D ys         = ys-    magic xs D         = unsafeCoerce# xs-    magic (x :* xs) ys = unsafeCoerce# $ x :* magic xs ys-    {-# NOINLINE magic #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882-{-# INLINE inferConcatDimensions #-}----- | Infer that prefix is also Dimensions-inferPrefixDimensions :: forall bs asbs-                       . (IsSuffix bs asbs ~ 'True, Dimensions bs, Dimensions asbs)-                      => Evidence (Dimensions (Prefix bs asbs))-inferPrefixDimensions = reifyDimensions $ magic (len dasbs - len (dim @bs)) (unsafeCoerce# dasbs)-  where-    dasbs = dim @asbs-    len :: forall (ns :: [Nat]) . Dim ns -> Int-    len D         = 0-    len (_ :* ds) = 1 + len ds-    magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim ns-    magic _ D         = D-    magic 0 _         = unsafeCoerce# D-    magic n (d :* ds) = d :* magic (n-1) ds-    {-# NOINLINE magic #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882-{-# INLINE inferPrefixDimensions #-}---- | Infer that suffix is also Dimensions-inferSuffixDimensions :: forall as asbs-                       . (IsPrefix as asbs ~ 'True, Dimensions as, Dimensions asbs)-                      => Evidence (Dimensions (Suffix as asbs))-inferSuffixDimensions = reifyDimensions $ magic (dim @as) (unsafeCoerce# $ dim @asbs)-  where-    magic :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim ys-    magic D ys                = ys-    magic _ D                 = D-    magic (_ :* xs) (_ :* ys) = unsafeCoerce# $ magic xs ys-{-# INLINE inferSuffixDimensions #-}---- | Make snoc almost as good as cons-inferSnocDimensions :: forall xs z-                     . (KnownDim z, Dimensions xs)-                    => Evidence (Dimensions (xs +: z))-inferSnocDimensions = reifyDimensions $ magic (dim @xs)-  where-    magic :: forall (ns :: [Nat]) . Dim ns -> Dim (ns +: z)-    magic D         = Dn :* D-    magic (d :* ds) = unsafeCoerce# (d :* magic ds)-{-# INLINE inferSnocDimensions #-}---- | Init of the dimension list is also Dimensions,---   and the last dimension is KnownDim.-inferUnSnocDimensions :: forall ds-                       . Dimensions ds-                      => Maybe (Evidence (SnocDimensions ds))-inferUnSnocDimensions = case dim @ds of-      D  -> Nothing-      ds -> Just $ case magic ds of-          (ys, Dn) -> case unsafeSnocDims' @ds of-            Evidence -> case reifyDimensions  @(Init ds) (unsafeCoerce# ys) of-              Evidence -> Evidence-    where-      magic :: forall (ns :: [Nat]) . Dim ns -> (Dim ns, Dim (Last ns))-      magic D         = (D, undefined)-      magic (d :* D)  = (unsafeCoerce# D, d)-      magic (d :* ds) = case magic ds of-          (ds', z) -> (d :* ds', unsafeCoerce# z)-{-# INLINE inferUnSnocDimensions #-}----- | Tail of the dimension list is also Dimensions,---   and the head dimension is KnownDim.-inferUnConsDimensions :: forall ds-                       . Dimensions ds-                      => Maybe (Evidence (ConsDimensions ds))-inferUnConsDimensions = case dim @ds of-      D  -> Nothing-      Dn :* ds' -> Just $ case reifyDimensions ds' +!+ unsafeConsDims' @ds of-            Evidence -> Evidence-{-# INLINE inferUnConsDimensions #-}---- | 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)-    )---- | 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)-    )---unsafeSnocDims' :: forall (xs :: [Nat]) . Evidence-    ( xs ~ (Init xs +: Last xs)-    , xs ~ (Init xs ++ '[Last xs])-    , IsPrefix  (Init xs) xs ~ 'True-    , IsSuffix '[Last xs] xs ~ 'True-    , Suffix    (Init xs) xs ~ '[Last xs]-    , Prefix   '[Last xs] xs ~   Init xs-    )-unsafeSnocDims' = case  unsafeEqEvidence @xs @(Init xs +: Last xs)-                    +!+ unsafeEqEvidence @xs @(Init xs ++ '[Last xs])-                    +!+ unsafeEqEvidence @(IsPrefix  (Init xs) xs) @'True-                    +!+ unsafeEqEvidence @(IsSuffix '[Last xs] xs) @'True-                    +!+ unsafeEqEvidence @(Suffix    (Init xs) xs) @'[Last xs]-                    +!+ unsafeEqEvidence @(Prefix   '[Last xs] xs) @(Init xs) of-    Evidence -> Evidence-{-# INLINE unsafeSnocDims' #-}--unsafeConsDims' :: forall (xs :: [Nat]) . Evidence-    ( xs ~ (  Head xs  :+ Tail xs)-    , xs ~ ('[Head xs] ++ Tail xs)-    , IsPrefix '[Head xs] xs ~ 'True-    , IsSuffix  (Tail xs) xs ~ 'True-    , Suffix   '[Head xs] xs ~   Tail xs-    , Prefix    (Tail xs) xs ~ '[Head xs]-    )-unsafeConsDims' = case  unsafeEqEvidence @xs @(  Head xs  :+ Tail xs)-                    +!+ unsafeEqEvidence @xs @('[Head xs] ++ Tail xs)-                    +!+ unsafeEqEvidence @(IsPrefix '[Head xs] xs) @'True-                    +!+ unsafeEqEvidence @(IsSuffix  (Tail xs) xs) @'True-                    +!+ unsafeEqEvidence @(Suffix   '[Head xs] xs) @(Tail xs)-                    +!+ unsafeEqEvidence @(Prefix    (Tail xs) xs) @'[Head xs] of-    Evidence -> Evidence-{-# INLINE unsafeConsDims' #-}----- | Init of the list is also Dimensions-inferInitDimensions :: forall xs-                     . Dimensions xs-                    => Maybe (Evidence (Dimensions (Init xs)))-inferInitDimensions = case dim @xs of-      D  -> Nothing-      ds -> Just . reifyDimensions $ magic (unsafeCoerce# ds)-    where-      magic :: forall (ns :: [Nat]) . Dim ns -> Dim ns-      magic D         = D-      magic (_ :* D)  = unsafeCoerce# D-      magic (d :* ds) = d :* magic ds-{-# INLINE inferInitDimensions #-}---- | Take KnownDim of the list is also Dimensions-inferTakeNDimensions :: forall n xs-                      . (KnownDim n, Dimensions xs)-                     => Evidence (Dimensions (Take n xs))-inferTakeNDimensions = reifyDimensions $ magic (dimVal' @n) (dim @xs)-    where-      magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim (Take n ns)-      magic _ D = D-      magic 0 _ = unsafeCoerce# D-      magic n (d :* ds) = unsafeCoerce# $ d :* (unsafeCoerce# $ magic (n-1) ds :: Dim (Tail ns))-      {-# NOINLINE magic #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882-{-# INLINE inferTakeNDimensions #-}---- | Drop KnownDim of the list is also Dimensions-inferDropNDimensions :: forall n xs-                      . (KnownDim n, Dimensions xs)-                     => Evidence (Dimensions (Drop n xs))-inferDropNDimensions = reifyDimensions $ magic (dimVal' @n) (dim @xs)-    where-      magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim (Drop n ns)-      magic _ D         = D-      magic 0 ds        = unsafeCoerce# ds-      magic n (_ :* ds) = unsafeCoerce# $ magic (n-1) ds-      {-# NOINLINE magic #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882-{-# INLINE inferDropNDimensions #-}---- | Reverse of the list is also Dimensions-inferReverseDimensions :: forall xs . Dimensions xs => Evidence (Dimensions (Reverse xs))-inferReverseDimensions = reifyDimensions $ magic (dim @xs) (unsafeCoerce# D)-    where-      magic :: forall (ns :: [Nat]) . Dim ns -> Dim (Reverse ns) -> Dim (Reverse ns)-      magic D xs = xs-      magic (p:*sx) xs = magic (unsafeCoerce# sx :: Dim ns)-                               (unsafeCoerce# (p:*xs) :: Dim (Reverse ns))-{-# INLINE inferReverseDimensions #-}----------------------------------------------------------------------------------------- * Utility functions--------------------------------------------------------------------------------------- | Use the given `Dim ds` to create an instance of `Dimensions ds` dynamically.-reifyDimensions :: forall (ds :: [Nat]) . Dim ds -> Evidence (Dimensions ds)-reifyDimensions ds = reifyDims ds Evidence-{-# INLINE reifyDimensions #-}----- | This function does GHC's magic to convert user-supplied `dimVal'` 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-reifyDims :: forall r (ds :: [Nat]) . Dim ds -> ( Dimensions ds => r) -> r-reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds-{-# INLINE reifyDims #-}-newtype MagicDims ds r = MagicDims (Dimensions ds => r)---unsafeEqEvidence :: forall x y . Evidence (x ~ y)-unsafeEqEvidence = case (unsafeCoerce# Refl :: x :~: y) of Refl -> Evidence-{-# INLINE unsafeEqEvidence #-}

@@ -0,0 +1,405 @@+{-# OPTIONS_GHC -fno-warn-orphans      #-}+{-# LANGUAGE AllowAmbiguousTypes       #-}+{-# LANGUAGE CPP                       #-}+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE ExplicitNamespaces        #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE FlexibleInstances         #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE KindSignatures            #-}+{-# LANGUAGE MagicHash                 #-}+{-# LANGUAGE MultiParamTypeClasses     #-}+{-# LANGUAGE PatternSynonyms           #-}+{-# LANGUAGE PolyKinds                 #-}+{-# LANGUAGE Rank2Types                #-}+{-# LANGUAGE RoleAnnotations           #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TypeApplications          #-}+{-# LANGUAGE TypeFamilies              #-}+{-# LANGUAGE TypeFamilyDependencies    #-}+{-# LANGUAGE TypeInType                #-}+{-# LANGUAGE TypeOperators             #-}+{-# LANGUAGE UndecidableInstances      #-}+{-# LANGUAGE ViewPatterns              #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Dimensions.Dims+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+-- Provides a data type `Dims 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.Dims+  ( Dims, SomeDims (..), Dimensions (..)+  , TypedList ( Dims, XDims, AsXDims, KnownDims+              , U, (:*), Empty, TypeList, Cons, Snoc, Reverse)+  , listDims, someDimsVal, totalDim, totalDim'+  , sameDims, sameDims'+  , compareDims, compareDims'+  , inSpaceOf, asSpaceOf+  , xDims, xDims'+    -- * Type-level programming+    --   Provide type families to work with lists of dimensions (`[Nat]` or `[XNat]`)+  , AsXDims, AsDims, FixedDims, KnownXNatTypes, type (:<), type (>:)+    -- * Re-export type list+  , RepresentableList (..), TypeList, types+  , order, order'+    -- * Re-export single dimension type and functions+  , module Numeric.Dim+  ) where++++import           GHC.Exts              (unsafeCoerce#, Constraint)+import qualified Text.Read             as Read++import           Numeric.Dim+import           Numeric.Type.Evidence+import           Numeric.Type.List+import           Numeric.TypedList     (RepresentableList (..), TypeList,+                                        TypedList (..), order, order', types)+++-- | Type-level dimensionality O(1).+type Dims (xs :: [k]) = TypedList Dim xs++-- Starting from GHC 8.2, compiler supports specifying lists of complete+-- pattern synonyms.+#if __GLASGOW_HASKELL__ >= 802+{-# COMPLETE Dims #-}+{-# COMPLETE XDims #-}+{-# COMPLETE AsXDims #-}+{-# COMPLETE KnownDims #-}+#endif++-- | @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 :: forall ds . () => Dimensions ds => Dims ds+pattern Dims <- (dimsEv -> E)+  where+    Dims = dims @_ @ds++-- | @O(Length ds)@ `Dimensions` and `KnownDim` for each individual dimension.+pattern KnownDims :: forall ds . ()+                  => (All KnownDim ds, Dimensions ds) => Dims ds+pattern KnownDims <- (patKDims -> PatKDims)+  where+    KnownDims = dims @_ @ds+++-- | 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.+--+--   In order to use this pattern, one must know @XNat@ type constructors in+--   each dimension at compile time.+pattern XDims :: forall (xns :: [XNat]) . KnownXNatTypes xns+              => forall (ns :: [Nat]) . (FixedDims xns ns, Dimensions ns)+              => Dims ns -> Dims xns+pattern XDims ns <- (patXDims -> PatXDims ns)+  where+    XDims ns = unsafeCoerce# ns++-- | An easy way to convert Nat-indexed dims into XNat-indexed dims.+pattern AsXDims :: forall (ns :: [Nat]) . ()+                => (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))+                => Dims (AsXDims ns) -> Dims ns+pattern AsXDims xns <- (patAsXDims -> PatAsXDims xns)+  where+    AsXDims xns = unsafeCoerce# xns++-- | Same as SomeNat, but for Dimensions:+--   Hide all information about Dimensions inside+data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)++class Dimensions (ds :: [k]) where+    -- | Get dimensionality of a space at runtime,+    --   represented as a list of `Dim`.+    --+    --   Note, this function is supposed to be used with @TypeApplications@,+    --   and the @Dimensions@ class has varying kind of the parameter;+    --   thus, the function has two type paremeters (kind and type of @ds@).+    --   For example, you can type:+    --+    --   >>>:set -XTypeApplications+    --   >>>:set -XDataKinds+    --   >>>:t dims @_ @'[N 17, N 12]+    --   dims @_ @'[N 17, N 12] :: Dims '[N 17, N 12]+    --+    --   >>>:t dims @XNat @'[]+    --   dims @XNat @'[] :: 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 = U+    {-# INLINE dims #-}++instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds :: [k]) where+    dims = dim :* dims+    {-# INLINE dims #-}+++-- | Convert `Dims xs` to a plain haskell list of dimension sizes @O(1)@.+listDims :: Dims xs -> [Word]+listDims = unsafeCoerce#+{-# INLINE listDims #-}++-- | Convert a plain haskell list of dimension sizes into an unknown+--   type-level dimensionality  @O(1)@.+someDimsVal :: [Word] -> SomeDims+someDimsVal = SomeDims . unsafeCoerce#+{-# INLINE someDimsVal #-}++-- | Product of all dimension sizes @O(Length xs)@.+totalDim :: Dims xs -> Word+totalDim = product . listDims+{-# INLINE totalDim #-}++-- | Product of all dimension sizes @O(Length xs)@.+totalDim' :: forall xs . Dimensions xs => Word+totalDim' = totalDim (dims @_ @xs)+{-# INLINE totalDim' #-}++-- | Get XNat-indexed dims given their fixed counterpart.+xDims :: FixedDims xns ns => Dims ns -> Dims xns+xDims = unsafeCoerce#+{-# INLINE xDims #-}++-- | Get XNat-indexed dims given their fixed counterpart.+xDims' :: forall xns ns . (FixedDims xns ns, Dimensions ns) => Dims xns+xDims' = xDims @xns (dims @Nat @ns)+{-# INLINE xDims' #-}+++-- | We either get evidence that this function was instantiated with the+--   same type-level Dimensions, or 'Nothing' @O(Length xs)@.+--+--   Note, this function works on @Nat@-indexed dimensions only,+--   because @Dims '[XN x]@ does not have runtime evidence to infer @x@+--   and `KnownDim x` does not imply `KnownDim (XN x)`.+sameDims :: Dims (as :: [Nat]) -> Dims (bs :: [Nat]) -> Maybe (Evidence (as ~ bs))+sameDims as bs+  | listDims as == listDims bs+    = Just (unsafeCoerce# (E @('[] ~ '[])))+  | otherwise = 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 q+           . (Dimensions as, Dimensions bs)+          => p as -> q bs -> Maybe (Evidence (as ~ bs))+sameDims' _ _ = sameDims (dims @Nat @as) (dims @Nat @bs)+{-# INLINE sameDims' #-}++-- | Compare dimensions by their size in lexicorgaphic order+--   from the last dimension to the first dimension+--   (the last dimension is the most significant one).+--+--   Literally,+--+--   > compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)+compareDims :: Dims as -> Dims bs -> Ordering+compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)+{-# INLINE compareDims #-}++-- | Compare dimensions by their size in lexicorgaphic order+--   from the last dimension to the first dimension+--   (the last dimension is the most significant one) @O(Length xs)@.+--+--   Literally,+--+--   > compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)+--+--   This is the same @compare@ rule, as for `Idxs`.+compareDims' :: forall as bs p q+              . (Dimensions as, Dimensions bs)+             => p as -> q bs -> Ordering+compareDims' _ _ = compareDims (dims @_ @as) (dims @_ @bs)+{-# INLINE compareDims' #-}+++-- | Similar to `const` or `asProxyTypeOf`;+--   to be used on such implicit functions as `dim`, `dimMax`, etc.+inSpaceOf :: a ds -> b ds -> a ds+inSpaceOf x _ = x+{-# INLINE inSpaceOf #-}++-- | Similar to `asProxyTypeOf`,+--   Give a hint to type checker to fix the type of a function argument.+asSpaceOf :: a ds -> (b ds -> c) -> (b ds -> c)+asSpaceOf _ = id+{-# INLINE asSpaceOf #-}+++instance Eq (Dims (ds :: [Nat])) where+    (==) _ _ = True++instance Eq (Dims (ds :: [XNat])) where+    (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)++instance Eq SomeDims where+    SomeDims as == SomeDims bs = listDims as == listDims bs++instance Ord (Dims (ds :: [Nat])) where+    compare _ _ = EQ++instance Ord (Dims (ds :: [XNat])) where+    compare = compareDims++instance Ord SomeDims where+    compare (SomeDims as) (SomeDims bs) = compareDims as bs++instance Show (Dims xs) where+    show ds = "Dims " ++ show (listDims ds)+    showsPrec p ds+      = showParen (p >= 10)+      $ showString "Dims " . showsPrec p (listDims ds)++instance Show SomeDims where+    show (SomeDims ds) = "SomeDims " ++ show (listDims ds)+    showsPrec p (SomeDims ds)+      = showParen (p >= 10)+      $ showString "SomeDims " . showsPrec p (listDims ds)++instance Read SomeDims where+    readPrec = Read.parens $ Read.prec 10 $ do+      s <- Read.lexP+      if s == Read.Ident "SomeDims"+      then someDimsVal <$> Read.readPrec+      else Read.pfail++instance Dimensions ds => Bounded (Dims ds) where+    maxBound = dims+    {-# INLINE maxBound #-}+    minBound = dims+    {-# INLINE minBound #-}++++-- | Map Dims onto XDims (injective)+type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where+    AsXDims '[] = '[]+    AsXDims (n ': ns) = N n ': AsXDims ns++-- | Map XDims onto Dims (injective)+type family AsDims (xns::[XNat]) = (ns :: [Nat]) | ns -> xns where+    AsDims '[] = '[]+    AsDims (N x ': xs) = x ': AsDims xs++-- | Constrain @Nat@ dimensions hidden behind @XNat@s.+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))++-- | Know the structure of each dimension+type KnownXNatTypes xns = All KnownXNatType xns+++-- | Synonym for (:+) that treats Nat values 0 and 1 in a special way:+--   it preserves the property that all dimensions are greater than 1.+type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where+    0 :< _  = '[]+    1 :< ns = ns+    n :< ns = n :+ ns+infixr 6 :<++-- | Synonym for (+:) that treats Nat values 0 and 1 in a special way:+--   it preserves the property that all dimensions are greater than 1.+type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where+    _  >: 0 = '[]+    ns >: 1 = ns+    ns >: n = ns +: n+infixl 6 >:+++++++--------------------------------------------------------------------------------++-- | This function does GHC's magic to convert user-supplied `dims` function+--   to create an instance of `Dimensions` typeclass at runtime.+--   The trick is taken from Edward Kmett's reflection library explained+--   in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection+reifyDims :: forall r ds . Dims ds -> ( Dimensions ds => r) -> r+reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds+{-# INLINE reifyDims #-}+newtype MagicDims ds r = MagicDims (Dimensions ds => r)++dimsEv :: Dims ds -> Evidence (Dimensions ds)+dimsEv ds = reifyDims ds E+{-# INLINE dimsEv #-}+++data PatXDims (xns :: [XNat])+  = forall (ns :: [Nat])+  . (FixedDims xns ns, Dimensions ns) => PatXDims (Dims ns)+++patXDims :: All KnownXNatType xns => Dims xns -> PatXDims xns+patXDims U = PatXDims U+patXDims (Dn n :* xns) = case patXDims xns of+  PatXDims ns -> PatXDims (n :* ns)+patXDims (Dx n :* xns) = case patXDims xns of+  PatXDims ns -> PatXDims (n :* ns)+#if __GLASGOW_HASKELL__ >= 802+#else+patXDims _ = error "XDims/patXDims: impossible argument"+#endif+{-# INLINE patXDims #-}+++data PatAsXDims (ns :: [Nat])+  = (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))+  => PatAsXDims (Dims (AsXDims ns))+++patAsXDims :: Dims ns -> PatAsXDims ns+patAsXDims U = PatAsXDims U+patAsXDims (n@D :* ns) = case patAsXDims ns of+  PatAsXDims xns -> PatAsXDims (Dn n :* xns)+#if __GLASGOW_HASKELL__ >= 802+#else+patAsXDims _ = error "AsXDims/patAsXDims: impossible argument"+#endif+{-# INLINE patAsXDims #-}++++data PatKDims (ns :: [k])+  = (All KnownDim ns, Dimensions ns) => PatKDims+++patKDims :: Dims ns -> PatKDims ns+patKDims U = PatKDims+patKDims (Dim :* ns) = case patKDims ns of+  PatKDims -> PatKDims+#if __GLASGOW_HASKELL__ >= 802+#else+patKDims _ = error "Dims/patKDims: impossible argument"+#endif+{-# INLINE patKDims #-}

@@ -0,0 +1,334 @@+{-# LANGUAGE PolyKinds #-}+-- Workaround weird behavior of GHC 8.4+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Dimensions.Fold+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+-- Fold a function over all dimensions provided dimension indices or offsets.+-- The main purpose of this module is to fold or traverse flat data arrays+-- following the shape of dimensions associated with them.+--+-----------------------------------------------------------------------------+module Numeric.Dimensions.Fold+  ( overDim, overDim_, overDimIdx, overDimIdx_+  , overDimOff, overDimOff_+  , overDimReverse, overDimReverseIdx+  , foldDim, foldDimIdx, foldDimOff+  , foldDimReverse, foldDimReverseIdx+  , overDimPart, overDimPartIdx+  ) where+++import           Control.Monad           ((>=>))+import           Numeric.Dimensions.Idxs++-- | Go over all dimensions keeping track of index and offset+overDim :: Monad m+        => Dims ds -- ^ Shape of a space+        -> (Idxs ds -> Int -> a -> m a) -- ^ Function to call on each dimension+        -> Int -- ^ Initial offset+        -> Int -- ^ Offset step+        -> a -- ^ Initial value+        -> m a+overDim U k offset _step = k U offset+overDim (d :* ds) k offset step = overDim ds k' offset (di * step)+  where+    dw = dimVal d+    di = fromIntegral dw+    k' is = go 1+      where+        go i off+          | i > dw = return+          | otherwise = k (Idx i :* is) off >=> go (i+1) (off+step)+{-# INLINE overDim #-}++-- | Go over all dimensions in reverse order keeping track of index and offset+overDimReverse :: Monad m+               => Dims ds -- ^ Shape of a space+               -> (Idxs ds -> Int -> a -> m a) -- ^ Function to call on each dimension+               -> Int -- ^ Initial offset+               -> Int -- ^ Offset step (substracted from initial offset)+               -> a -- ^ Initial value+               -> m a+overDimReverse U k offset _step = k U offset+overDimReverse (d :* ds) k offset step = overDimReverse ds k' offset (di * step)+  where+    dw = dimVal d+    di = fromIntegral dw+    k' is = go dw+      where+        go i off+          | i <= 0 = return+          | otherwise = k (Idx i :* is) off >=> go (i-1) (off-step)+{-# INLINE overDimReverse #-}++-- | Go over all dimensions keeping track of index and offset+overDim_ :: Monad m+         => Dims ds -- ^ Shape of a space+         -> (Idxs ds -> Int -> m ()) -- ^ Function to call on each dimension+         -> Int -- ^ Initial offset+         -> Int -- ^ Offset step+         -> m ()+overDim_ U k offset _step = k U offset+overDim_ (d :* ds) k offset step = overDim_ ds k' offset (di * step)+  where+    dw = dimVal d+    di = fromIntegral dw+    k' is = go 1+      where+        go i off+          | i > dw = return ()+          | otherwise = k (Idx i :* is) off >> go (i+1) (off+step)+{-# INLINE overDim_ #-}++-- | Go over all dimensions keeping track of index+overDimIdx :: Monad m+           => Dims ds -- ^ Shape of a space+           -> (Idxs ds -> a -> m a) -- ^ Function to call on each dimension+           -> a -- ^ Initial value+           -> m a+overDimIdx U k = k U+overDimIdx (d :* ds) k = overDimIdx ds k'+  where+    dw = dimVal d+    k' is = go 1+      where+        go i+          | i > dw = return+          | otherwise = k (Idx i :* is) >=> go (i+1)+{-# INLINE overDimIdx #-}++-- | Go over all dimensions keeping track of index+overDimIdx_ :: Monad m+            => Dims ds -- ^ Shape of a space+            -> (Idxs ds -> m ()) -- ^ Function to call on each dimension+            -> m ()+overDimIdx_ U k = k U+overDimIdx_ (d :* ds) k = overDimIdx_ ds k'+  where+    dw = dimVal d+    k' is = go 1+      where+        go i+          | i > dw = return ()+          | otherwise = k (Idx i :* is) >> go (i+1)+{-# INLINE overDimIdx_ #-}+++-- | Go over all dimensions keeping track of total offset+overDimOff :: Monad m+           => Dims ds -- ^ Shape of a space+           -> (Int -> a -> m a) -- ^ Function to call with each offset value+           -> Int -- ^ Initial offset+           -> Int -- ^ Offset step+           -> a -- ^ Initial value+           -> m a+overDimOff ds k offset step = go (totalDim ds) offset+  where+    go i off+          | i == 0 = return+          | otherwise = k off >=> go (i-1) (off+step)+{-# INLINE overDimOff #-}++-- | Go over all dimensions keeping track of total offset+overDimOff_ :: Monad m+            => Dims ds -- ^ Shape of a space+            -> (Int -> m ()) -- ^ Function to call with each offset value+            -> Int -- ^ Initial offset+            -> Int -- ^ Offset step+            -> m ()+overDimOff_ ds k offset step = go (totalDim ds) offset+  where+    go i off+          | i == 0 = return ()+          | otherwise = k off >> go (i-1) (off+step)+{-# INLINE overDimOff_ #-}+++-- | Go over all dimensions in reverse order keeping track of index+overDimReverseIdx :: Monad m+                  => Dims ds -- ^ Shape of a space+                  -> (Idxs ds -> a -> m a) -- ^ Function to call on each dimension+                  -> a -- ^ Initial value+                  -> m a+overDimReverseIdx U k = k U+overDimReverseIdx (d :* ds) k = overDimReverseIdx ds k'+  where+    dw = dimVal d+    k' is = go dw+      where+        go i+          | i <= 0 = return+          | otherwise = k (Idx i :* is) >=> go (i-1)+{-# INLINE overDimReverseIdx #-}++++-- | Fold over all dimensions keeping track of index and offset+foldDim :: Dims ds -- ^ Shape of a space+        -> (Idxs ds -> Int -> a -> a) -- ^ Function to call on each dimension+        -> Int -- ^ Initial offset+        -> Int -- ^ Offset step+        -> a -- ^ Initial value+        -> a+foldDim U k offset _step = k U offset+foldDim (d :* ds) k offset step = foldDim ds k' offset (di * step)+  where+    dw = dimVal d+    di = fromIntegral dw+    k' is = go 1+      where+        go i off+          | i > dw = id+          | otherwise = go (i+1) (off+step) . k (Idx i :* is) off+{-# INLINE foldDim #-}++-- | Fold over all dimensions in reverse order keeping track of index and offset+foldDimReverse :: Dims ds -- ^ Shape of a space+               -> (Idxs ds -> Int -> a -> a) -- ^ Function to call on each dimension+               -> Int -- ^ Initial offset+               -> Int -- ^ Offset step (substracted from initial offset)+               -> a -- ^ Initial value+               -> a+foldDimReverse U k offset _step = k U offset+foldDimReverse (d :* ds) k offset step = foldDimReverse ds k' offset (di * step)+  where+    dw = dimVal d+    di = fromIntegral dw+    k' is = go dw+      where+        go i off+          | i <= 0 = id+          | otherwise = go (i-1) (off-step) . k (Idx i :* is) off+{-# INLINE foldDimReverse #-}++++-- | Fold over all dimensions keeping track of index+foldDimIdx :: Dims ds -- ^ Shape of a space+           -> (Idxs ds -> a -> a) -- ^ Function to call on each dimension+           -> a -- ^ Initial value+           -> a+foldDimIdx U k = k U+foldDimIdx (d :* ds) k = foldDimIdx ds k'+  where+    dw = dimVal d+    k' is = go 1+      where+        go i+          | i > dw = id+          | otherwise = go (i+1) . k (Idx i :* is)+{-# INLINE foldDimIdx #-}+++-- | Fold over all dimensions keeping track of total offset+foldDimOff :: Dims ds -- ^ Shape of a space+           -> (Int -> a -> a) -- ^ Function to call on each dimension+           -> Int -- ^ Initial offset+           -> Int -- ^ Offset step+           -> a -- ^ Initial value+           -> a+foldDimOff ds k offset step = go (totalDim ds) offset+  where+    go i off+          | i == 0 = id+          | otherwise = go (i-1) (off+step) . k off+{-# INLINE foldDimOff #-}+++-- | Fold over all dimensions in reverse order keeping track of index+foldDimReverseIdx :: Dims ds -- ^ Shape of a space+                  -> (Idxs ds -> a -> a) -- ^ Function to call on each dimension+                  -> a -- ^ Initial value+                  -> a+foldDimReverseIdx U k = k U+foldDimReverseIdx (d :* ds) k = foldDimReverseIdx ds k'+  where+    dw = dimVal d+    k' is = go dw+      where+        go i+          | i <= 0 = id+          | otherwise = go (i-1) . k (Idx i :* is)+{-# INLINE foldDimReverseIdx #-}+++-- | Traverse from the first index to the second index in each dimension.+--   You can combine positive and negative traversal directions+--   along different dimensions.+--+--   Note, initial and final indices are included in the range;+--   the argument function is guaranteed to execute at least once.+overDimPart :: (Dimensions ds, Monad m)+            => Idxs ds -- ^ Initial indices+            -> Idxs ds -- ^ Final indices+            -> (Idxs ds -> Int -> a -> m a)+                       -- ^ Function to call on each dimension+            -> Int     -- ^ Initial offset (at index @minBound :: Idxs ds@)+                       --   Note, this is not an offset value at initial indices.+            -> Int     -- ^ Offset step+            -> a       -- ^ initial value+            -> m a+overDimPart imin imax f offset step = overDimPart' stepSizes imin imax f offset+    where+      stepSizes = createStepSizes (dims `inSpaceOf` imin) step++      createStepSizes :: Dims ns -> Int -> TypedList StepSize ns+      createStepSizes U _ = U+      createStepSizes (d :* ds) k+        = StepSize k :* createStepSizes ds (k * fromIntegral (dimVal d))++overDimPart' :: Monad m+             => TypedList StepSize ns+             -> Idxs ds -> Idxs ds+             -> (Idxs ds -> Int -> a -> m a)+             -> Int+             -> a -> m a+overDimPart' U U U k off0 = k U off0+overDimPart' (siW :* iws) (Idx iStart :* starts) (Idx iEnd :* ends) k off0+  | iEnd >= iStart = overDimPart' iws starts ends (loop iStart) (off0 + headOff)+  | otherwise      = overDimPart' iws starts ends (looi iStart) (off0 + headOff)+  where+    StepSize iW = siW+    headOff = iW * (fromIntegral iStart - 1)+    loop i js off+      | i > iEnd = return+      | otherwise = k (Idx i :* js) off >=> loop (i+1) js (off + iW)+    looi i js off+      | i < iEnd = return+      | otherwise = k (Idx i :* js) off >=> looi (i-1) js (off - iW)+++newtype StepSize n = StepSize Int++-- | Traverse from the first index to the second index in each dimension.+--   You can combine positive and negative traversal directions+--   along different dimensions.+--+--   Note, initial and final indices are included in the range;+--   the argument function is guaranteed to execute at least once.+overDimPartIdx :: Monad m+               => Idxs ds -- ^ Initial indices+               -> Idxs ds -- ^ Final indices+               -> (Idxs ds -> a -> m a)+                          -- ^ Function to call on each dimension+               -> a       -- ^ initial value+               -> m a+overDimPartIdx U U k = k U+overDimPartIdx (start :* starts) (end :* ends) k+  | iEnd >= iStart = overDimPartIdx starts ends (loop iStart)+  | otherwise      = overDimPartIdx starts ends (looi iStart)+  where+    Idx iStart = start+    Idx iEnd   = end+    loop i is+      | i > iEnd = return+      | otherwise = k (Idx i :* is) >=> loop (i+1) is+    looi i is+      | i < iEnd = return+      | otherwise = k (Idx i :* is) >=> looi (i-1) is

@@ -1,209 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes       #-}-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces        #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE FlexibleInstances         #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE MagicHash                 #-}-{-# LANGUAGE MultiParamTypeClasses     #-}-{-# LANGUAGE PolyKinds                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeFamilies              #-}-{-# LANGUAGE TypeFamilyDependencies    #-}-{-# LANGUAGE TypeInType                #-}-{-# LANGUAGE TypeOperators             #-}-{-# LANGUAGE UndecidableInstances      #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.Idx--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ 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-  ( -- * Data types-    Idx (..)-  , appendIdx, splitIdx-  ) where---import           Control.Arrow           (first)-import           GHC.Exts                (IsList (..))-import           Unsafe.Coerce           (unsafeCoerce)--import           Numeric.Dimensions.Dim-import           Numeric.Dimensions.List------ | Type-level dimensional indexing with arbitrary Int values inside-data Idx (ds :: [Nat]) where-   -- | Zero-rank dimensionality - scalar-   Z :: Idx '[]-   -- | List-like concatenation of indices-   (:!) :: {-# UNPACK #-} !Int -> !(Idx ds) -> Idx (d ': ds)-infixr 5 :!--idxToList :: Idx ds -> [Int]-idxToList Z         = []-idxToList (x :! xs) = x : idxToList xs--idxFromList :: [Int] -> Idx ds-idxFromList []     = unsafeCoerce Z-idxFromList (x:xs) = unsafeCoerce $ x :! unsafeCoerce (idxFromList xs)--succIdx :: Dim xs -> Idx xs -> Idx xs-succIdx _ Z = Z-succIdx ((Dn :: Dim d) :* ds) (i :! is) | i >= dimVal' @d = 1 :! succIdx ds is-                                        | otherwise       = succ i :! is-{-# INLINE succIdx #-}--predIdx :: Dim xs -> Idx xs -> Idx xs-predIdx _ Z = Z-predIdx ((Dn :: Dim d) :* ds) (i :! is) | i <= 1    = dimVal' @d :! predIdx ds is-                                        | otherwise = pred i :! is-{-# INLINE predIdx #-}---- | Convert zero-based offset into Idx in a given space-toIdx :: Dim xs -> Int -> Idx xs-toIdx D _ = Z-toIdx ((Dn :: Dim d) :* ds) off = case divMod off (dimVal' @d) of-      (off', i) -> i+1 :! toIdx ds off'-{-# NOINLINE toIdx #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882---- | Get zero-based offset of current index-fromIdx :: Dim xs -> Idx xs -> Int-fromIdx _ Z                             = 0-fromIdx ((Dn :: Dim d) :* ds) (i :! is) = i - 1 + dimVal' @d * fromIdx ds is-{-# INLINE fromIdx #-}---- | Offset difference of two indices (first idx - second idx)-diffIdx :: Dim xs -> Idx xs -> Idx xs -> Int-diffIdx _ Z _ = 0-diffIdx ((Dn :: Dim d) :* ds) (i1:!is1) (i2:!is2) = i1 - i2-          + dimVal' @d * diffIdx ds is1 is2-{-# INLINE diffIdx #-}---- | Step dimension index by an Integer offset-stepIdx :: Dim ds -> Int -> Idx ds -> Idx ds-stepIdx _ _ Z = Z-stepIdx ((Dn :: Dim d) :* ds) di (i:!is)-      = case divMod (di + i - 1) (dimVal' @d) of-         (0  , i') -> i'+1 :! is-         (di', i') -> i'+1 :! stepIdx ds di' is-{-# INLINE stepIdx #-}---- | Append index dimension-appendIdx :: forall (as :: [Nat]) (b :: Nat)-           . Idx as -> Int -> Idx (as +: b)-appendIdx Z i = i :! Z-appendIdx (j :! js) i = unsafeCoerce $ j :! (unsafeCoerce (appendIdx js i) :: Idx (Tail (as +: b)))-{-# INLINE appendIdx #-}---- | Split index into prefix and suffix dimensioned indices-splitIdx :: forall (as :: [Nat]) (bs :: [Nat])-          . FiniteList as => Idx (as ++ bs) -> (Idx as, Idx bs)-splitIdx = splitN (order @_ @as)-  where-    splitN :: Int -> Idx (as ++ bs) -> (Idx as, Idx bs)-    splitN 0 js = unsafeCoerce (Z, js)-    splitN n (j :! js) = first (unsafeCoerce . (j :!))-                       $ splitN (n-1) (unsafeCoerce js)-    splitN _ Z  = unsafeCoerce (Z, Z)-{-# INLINE splitIdx #-}---instance Show (Idx ds) where-    show Z  = "Idx Ø"-    show xs = "Idx" ++ foldr (\i s -> " " ++ show i ++ s) "" (idxToList xs)--instance Eq (Idx ds) where-    Z == Z = True-    (a:!as) == (b:!bs) = a == b && as == bs-    Z /= Z = False-    (a:!as) /= (b:!bs) = a /= b || as /= bs----- | With this instance we can slightly reduce indexing expressions---   e.g. x ! (1 :! 2 :! 4) == x ! (1 :! 2 :! 4 :! Z)-instance Num (Idx '[n]) where-    (a:!Z) + (b:!Z) = (a+b) :! Z-    (a:!Z) - (b:!Z) = (a-b) :! Z-    (a:!Z) * (b:!Z) = (a*b) :! Z-    signum (a:!Z)   = signum a :! Z-    abs (a:!Z)      = abs a :! Z-    fromInteger i   = fromInteger i :! Z---instance Ord (Idx ds) where-    compare Z Z             = EQ-    compare (a:!as) (b:!bs) = compare as bs `mappend` compare a b--instance Dimensions ds => Bounded (Idx ds) where-    maxBound = f (dim @ds)-      where-        f :: forall ns . Dim ns -> Idx ns-        f D                     = Z-        f ((Dn :: Dim n) :* ds) = dimVal' @n :! f ds-    {-# INLINE maxBound #-}-    minBound = f (dim @ds)-      where-        f :: forall (ns :: [Nat]) . Dim ns -> Idx ns-        f D          = Z-        f (Dn :* ds) = 1 :! f ds-    {-# INLINE minBound #-}--instance IsList (Idx ds) where-    type Item (Idx ds) = Int-    -- | Very unsafe way to convert Haskell list into Idx.-    --   If the length of a list is not equal to the length of type-level-    --   dimensions, behavior is undefined (going to crash likely).-    fromList = idxFromList-    toList = idxToList--instance Dimensions ds => Enum (Idx ds) where-    succ = succIdx (dim @ds)-    {-# INLINE succ #-}-    pred = predIdx (dim @ds)-    {-# INLINE pred #-}-    toEnum = toIdx (dim @ds)-    {-# INLINE toEnum #-}-    fromEnum = fromIdx (dim @ds)-    {-# INLINE fromEnum #-}-    enumFrom x = take (diffIdx ds maxBound x + 1) $ iterate (succIdx ds) x-      where-        ds = dim @ds-    {-# INLINE enumFrom #-}-    enumFromTo x y | x >= y    = take (diffIdx ds x y + 1) $ iterate (predIdx ds) x-                   | otherwise = take (diffIdx ds y x + 1) $ iterate (succIdx ds) x-      where-        ds = dim @ds-    {-# INLINE enumFromTo #-}-    enumFromThen x x' = take n $ iterate (stepIdx ds dn) x-      where-        ds = dim @ds-        dn = diffIdx ds x' x-        n  = 1 + if dn == 0 then 0-                            else if dn > 0 then diffIdx ds maxBound x `div` dn-                                           else diffIdx ds x minBound `div` negate dn-    {-# INLINE enumFromThen #-}-    enumFromThenTo x x' y = take n $ iterate (stepIdx ds dn) x-      where-        ds = dim @ds-        dn = diffIdx ds x' x-        n  = 1 + if dn == 0 then 0-                            else diffIdx ds y x `div` dn-    {-# INLINE enumFromThenTo #-}

@@ -0,0 +1,427 @@+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE ConstraintKinds            #-}+{-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE DeriveDataTypeable         #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE ExistentialQuantification  #-}+{-# LANGUAGE ExplicitNamespaces         #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GADTs                      #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures             #-}+{-# LANGUAGE MagicHash                  #-}+{-# LANGUAGE PolyKinds                  #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE Strict                     #-}+{-# LANGUAGE TypeApplications           #-}+#if __GLASGOW_HASKELL__ >= 802+#else+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+#endif+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Dimensions.Idxs+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+-- 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.Idxs+  ( -- * Data types+    Idx (..), Idxs+  , idxFromWord, unsafeIdxFromWord, idxToWord+  , listIdxs, idxsFromWords+    -- * Re-export dimensions types+  , module Numeric.Dimensions.Dims+  ) where+++import           Control.Arrow           (first)+import           Data.Data               (Data)+import           Foreign.Storable        (Storable)+import           GHC.Base+import           GHC.Enum+import           GHC.Generics            (Generic, Generic1)++import           Numeric.Dimensions.Dims+++-- | This type is used to index a single dimension;+--   the range of indices is from @1@ to @n@.+--+--   Note, this type has a weird `Enum` instance:+--+--   >>>fromEnum (Idx 7)+--   6+--+--   The logic behind this is that the `Enum` class is used to transform+--   indices to offsets. That is, element of an array at index @k :: Idx n@+--   is the element taken by an offset `k - 1 :: Int`.+newtype Idx n = Idx { unIdx :: Word }+  deriving ( Data, Generic, Generic1, Integral, Real, Storable, Eq, Ord )++instance Read (Idx n) where+    readsPrec d = fmap (first Idx) . readsPrec d++instance Show (Idx n) where+    showsPrec d = showsPrec d . unIdx+++instance KnownDim n => Bounded (Idx n) where+    minBound = 1+    {-# INLINE minBound #-}+    maxBound = unsafeCoerce# (dim @_ @n)+    {-# INLINE maxBound #-}++--   This is a weird `Enum` instance:+--+--   >>>fromEnum (Idx 7)+--   6+--+--   The logic behind this is that the `Enum` class is used to transform+--   indices to offsets. That is, element of an array at index @k :: Idx n@+--   is the element taken by an offset `k - 1 :: Int`.+instance KnownDim n => Enum (Idx n) where++#ifdef UNSAFE_INDICES+    succ = unsafeCoerce# ((+ 1) :: Word -> Word)+#else+    succ x@(Idx i)+      | x /= maxBound = Idx (i + 1)+      | otherwise = succError $ "Idx " ++ show (dim @_ @n)+#endif+    {-# INLINE succ #-}++#ifdef UNSAFE_INDICES+    pred = unsafeCoerce# ((+ (-1)) :: Word -> Word)+#else+    pred x@(Idx i)+      | x /= maxBound = Idx (i + 1)+      | otherwise = predError $ "Idx " ++ show (dim @_ @n)+#endif+    {-# INLINE pred #-}++#ifdef UNSAFE_INDICES+    toEnum (I# i#) = unsafeCoerce# (W# (int2Word# (i# +# 1#)))+#else+    toEnum i@(I# i#)+        | i >= 0 && i < dm = unsafeCoerce# (W# (int2Word# (i# +# 1#) ))+        | otherwise        = toEnumError ("Idx " ++ show d) i (0, dm)+      where+        d = unsafeCoerce# (dim @_ @n) :: Word+        dm = fromIntegral d - 1+#endif+    {-# INLINE toEnum #-}++#ifdef UNSAFE_INDICES+    fromEnum (Idx (W# w#)) = I# (word2Int# w# -# 1#)+#else+    fromEnum (Idx x@(W# w#))+        | x <= maxIntWord = I# (word2Int# w# -# 1#)+        | otherwise       = fromEnumError ("Idx " ++ show (dim @_ @n)) x+        where+          maxIntWord = W# (case maxInt of I# i -> int2Word# i)+#endif+    {-# INLINE fromEnum #-}++    enumFrom (Idx n)+      = unsafeCoerce# (enumFromTo n (unsafeCoerce# (dim @_ @n)))+    {-# INLINE enumFrom #-}+    enumFromThen (Idx n0) (Idx n1)+      = case compare n0 n1 of+          LT -> unsafeCoerce# (enumFromThenTo n0 n1 (unsafeCoerce# (dim @_ @n)))+          EQ -> unsafeCoerce# (repeat n0)+          GT -> unsafeCoerce# (enumFromThenTo n0 n1 1)+    {-# INLINE enumFromThen #-}+    enumFromTo+      = unsafeCoerce# (enumFromTo :: Word -> Word -> [Word])+    {-# INLINE enumFromTo #-}+    enumFromThenTo+      = unsafeCoerce# (enumFromThenTo :: Word -> Word -> Word -> [Word])+    {-# INLINE enumFromThenTo #-}++instance KnownDim n => Num (Idx n) where++#ifdef UNSAFE_INDICES+    (+) = unsafeCoerce# ((+) :: Word -> Word -> Word)+#else+    (Idx a) + (Idx b)+        | r > d || r < a || r < b+          = errorWithoutStackTrace+          $ "Num.(+){Idx " ++ show d ++ "}: sum of "+            ++ show a ++ " and " ++ show b+            ++ " is outside of index bounds."+        | otherwise = Idx r+      where+        r = a + b+        d = unsafeCoerce# (dim @_ @n)+#endif+    {-# INLINE (+) #-}++#ifdef UNSAFE_INDICES+    (-) = unsafeCoerce# ((-) :: Word -> Word -> Word)+#else+    (Idx a) - (Idx b)+        | b >= a+          = errorWithoutStackTrace+          $ "Num.(-){Idx " ++ show (dim @_ @n) ++ "}: difference of "+            ++ show a ++ " and " ++ show b+            ++ " is not positive."+        | otherwise = Idx (a - b)+#endif+    {-# INLINE (-) #-}++#ifdef UNSAFE_INDICES+    (*) = unsafeCoerce# ((*) :: Word -> Word -> Word)+#else+    (Idx a) * (Idx b)+        | r > d || r < a || r < b+          = errorWithoutStackTrace+          $ "Num.(*){Idx " ++ show d ++ "}: product of "+            ++ show a ++ " and " ++ show b+            ++ " is outside of index bounds."+        | otherwise = Idx r+      where+        r = a * b+        d = unsafeCoerce# (dim @_ @n)+#endif+    {-# INLINE (*) #-}++    negate = errorWithoutStackTrace+           $ "Num.(*){Idx " ++ show (dim @_ @n) ++ "}: cannot negate index."+    {-# INLINE negate #-}+    abs = id+    {-# INLINE abs #-}+    signum _ = Idx 1+    {-# INLINE signum #-}++#ifdef UNSAFE_INDICES+    fromInteger = unsafeCoerce# (fromInteger :: Integer -> Word)+#else+    fromInteger i+      | i > 0 && i <= d = Idx $ fromInteger i+      | otherwise       = errorWithoutStackTrace+                        $ "Num.fromInteger{Idx "+                        ++ show d ++ "}: integer "+                        ++ show i ++ " is outside of index bounds."+      where+        d = toInteger (unsafeCoerce# (dim @_ @n) :: Word)+#endif+    {-# INLINE fromInteger #-}+++unsafeIdxFromWord :: forall d . KnownDim d => Word -> Idx d+#ifdef UNSAFE_INDICES+unsafeIdxFromWord = unsafeCoerce#+#else+unsafeIdxFromWord w+  | w > 0 && w <= d = Idx w+  | otherwise       = errorWithoutStackTrace+                    $ "idxFromWord{Idx "+                    ++ show d ++ "}: word "+                    ++ show w ++ " is outside of index bounds."+  where+    d = unsafeCoerce# (dim @_ @d)+#endif+{-# INLINE unsafeIdxFromWord #-}++idxFromWord :: forall d . KnownDim d => Word -> Maybe (Idx d)+idxFromWord w+  | w > 0 && w <= unsafeCoerce# (dim @_ @d) = Just (Idx w)+  | otherwise                                 = Nothing+{-# INLINE idxFromWord #-}+++idxToWord :: Idx d -> Word+idxToWord = unsafeCoerce#+{-# INLINE idxToWord #-}++{-# RULES+"fromIntegral/idxToWord"+  fromIntegral = idxToWord+  #-}+++-- | Type-level dimensional indexing with arbitrary Word values inside.+--   Most of the operations on it require `Dimensions` constraint,+--   because the @Idxs@ itself does not store info about dimension bounds.+--+--   Note, this type has a special `Enum` instance:+--   `fromEnum` gives an offset of the index in a flat 1D array;+--   this is in line with a weird `Enum` instance of `Idx` type.+type Idxs (xs :: [k]) = TypedList Idx xs+++listIdxs :: Idxs xs -> [Word]+listIdxs = unsafeCoerce#+{-# INLINE listIdxs #-}+++idxsFromWords :: forall ds . Dimensions ds => [Word] -> Maybe (Idx ds)+idxsFromWords = unsafeCoerce# . go (listDims (dims @_ @ds))+  where+    go [] [] = Just []+    go (d : ds) (i : is)+      | i > 0 && i <= d = (i:) <$> go ds is+    go _ _   = Nothing++++instance Eq (Idxs xs) where+    (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)+    {-# INLINE (==) #-}++-- | Compare indices by their importance in lexicorgaphic order+--   from the last dimension to the first dimension+--   (the last dimension is the most significant one) @O(Length xs)@.+--+--   Literally,+--+--   > compare a b = compare (reverse $ listIdxs a) (reverse $ listIdxs b)+--+--   This is the same @compare@ rule, as for `Dims`.+--   Another reason to reverse the list of indices is to have a consistent+--   behavior when calculating index offsets:+--+--   > sort == sortOn fromEnum+--+instance Ord (Idxs xs) where+    compare a b = compare (reverse $ listIdxs a) (reverse $ listIdxs b)+    {-# INLINE compare #-}+++instance Show (Idxs xs) where+    show ds = "Idxs " ++ show (listIdxs ds)+    showsPrec p ds+      = showParen (p >= 10)+      $ showString "Idxs " . showsPrec p (listIdxs ds)++-- | With this instance we can slightly reduce indexing expressions, e.g.+--+--   > x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U)+--+instance KnownDim n => Num (Idxs '[n]) where+    (a:*U) + (b:*U) = (a+b) :* U+    {-# INLINE (+) #-}+    (a:*U) - (b:*U) = (a-b) :* U+    {-# INLINE (-) #-}+    (a:*U) * (b:*U) = (a*b) :* U+    {-# INLINE (*) #-}+    signum (a:*U)   = signum a :* U+    {-# INLINE signum #-}+    abs (a:*U)      = abs a :* U+    {-# INLINE abs #-}+    fromInteger i   = fromInteger i :* U+    {-# INLINE fromInteger #-}++instance Dimensions ds => Bounded (Idxs ds) where+    maxBound = f (dims @_ @ds)+      where+        f :: forall ns . Dims ns -> Idxs ns+        f U         = U+        f (d :* ds) = Idx (dimVal d) :* f ds+    {-# INLINE maxBound #-}+    minBound = f (dims @_ @ds)+      where+        f :: forall ns . Dims ns -> Idxs ns+        f U         = U+        f (_ :* ds) = Idx 1 :* f ds+    {-# INLINE minBound #-}+++instance Dimensions ds => Enum (Idxs ds) where++    succ = go (dims @_ @ds)+      where+        go :: forall ns . Dims ns -> Idxs ns -> Idxs ns+        go U U = succError $ "Idxs " ++ show (listDims $ dims @_ @ds)+        go (d :* ds) (Idx i :* is)+          | i == dimVal d = Idx 1 :* go ds is+          | otherwise     = Idx (i+1) :* is+    {-# INLINE succ #-}++    pred = go (dims @_ @ds)+      where+        go :: forall ns . Dims ns -> Idxs ns -> Idxs ns+        go U U = predError $ "Idxs " ++ show (listDims $ dims @_ @ds)+        go (d :* ds) (Idx i :* is)+          | i == 1    = Idx (dimVal d) :* go ds is+          | otherwise = Idx (i-1) :* is+    {-# INLINE pred #-}++    toEnum i = go dds $ fromIntegral i+      where+        dds = dims @_ @ds+        go :: forall ns . Dims ns -> Word -> Idxs ns+        go U 0 = U+        go U _ = toEnumError ("Idxs " ++ show (listDims dds))+                             i (0, totalDim dds - 1)+        go (d :* ds) off = case divMod off (dimVal d) of+          (off', j) -> Idx (j+1) :* go ds off'+    {-# INLINE toEnum #-}++    fromEnum = fromIntegral . go 1 (dims @_ @ds)+      where+        go :: forall ns . Word -> Dims ns -> Idxs ns -> Word+        go _ U U                     = 0+        go m (d :* ds) (Idx i :* is) = m * (i - 1) + go (m * dimVal d) ds is+    {-# INLINE fromEnum #-}++    enumFrom x = take (diffIdx (dims @_ @ds) maxBound x + 1) $ iterate succ x+    {-# INLINE enumFrom #-}++    enumFromTo x y | x >= y    = take (diffIdx ds x y + 1) $ iterate pred x+                   | otherwise = take (diffIdx ds y x + 1) $ iterate succ x+      where+        ds = dims @_ @ds+    {-# INLINE enumFromTo #-}++    enumFromThen x x' = take n $ iterate (stepIdx ds dn) x+      where+        ds = dims @_ @ds+        dn = diffIdx ds x' x+        n  = 1 + if dn == 0+                 then 0+                 else if dn > 0+                      then diffIdx ds maxBound x `div` dn+                      else diffIdx ds x minBound `div` negate dn+    {-# INLINE enumFromThen #-}++    enumFromThenTo x x' y = take n $ iterate (stepIdx ds dn) x+      where+        ds = dims @_ @ds+        dn = diffIdx ds x' x+        n  = 1 + if dn == 0 then 0+                            else diffIdx ds y x `div` dn+    {-# INLINE enumFromThenTo #-}++++--------------------------------------------------------------------------------++++-- | Offset difference of two indices @idx1 - idx2@+diffIdx :: Dims xs -> Idxs xs -> Idxs xs -> Int+diffIdx U U U = 0+diffIdx (d :* ds) (Idx i1 :* is1) (Idx i2 :* is2)+  = fromIntegral i1 - fromIntegral i2+  + fromIntegral (dimVal d) * diffIdx ds is1 is2+{-# INLINE diffIdx #-}++-- | Step dimension index by an Int offset+stepIdx :: Dims ds -> Int -> Idxs ds -> Idxs ds+stepIdx U _ U = U+stepIdx (d :* ds) di (Idx i :* is)+      = case divMod (di + fromIntegral i - 1) (fromIntegral (dimVal d)) of+         (0  , i') -> Idx (fromIntegral (i'+1)) :* is+         (di', i') -> Idx (fromIntegral (i'+1)) :* stepIdx ds di' is+{-# INLINE stepIdx #-}

@@ -1,436 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes       #-}-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces        #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE FlexibleInstances         #-}-{-# LANGUAGE FunctionalDependencies    #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE MagicHash                 #-}-{-# LANGUAGE MultiParamTypeClasses     #-}-{-# LANGUAGE PolyKinds                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE RoleAnnotations           #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeFamilies              #-}-{-# LANGUAGE TypeFamilyDependencies    #-}-{-# LANGUAGE TypeOperators             #-}-{-# LANGUAGE UndecidableInstances      #-}-{-# LANGUAGE CPP                       #-}------------------------------------------------------------------------------------ |--- Module      :  Numeric.Dimensions.List--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Provides type-level operations on lists.------ * Note for GHC 8.0--- Due to <https://ghc.haskell.org/trac/ghc/ticket/13538 GHC issue #13538>--- 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]`.--------------------------------------------------------------------------------------module Numeric.Dimensions.List-  ( -- * Basic operations-    type (++), type (:+), type (+:)-  , Empty, Cons, Snoc, Head-  , Tail, Init, Last, Concat, Reverse, Take, Drop-    -- * Working with concatenations-  , Suffix, Prefix, IsPrefix, IsSuffix-    -- * Term level functions-  , ConcatList (..), FiniteList (..), TypeList (..)-    -- * Term level inference of type-level functions-  , inferConcat, inferSuffix, inferPrefix, ConcatEvidence, FiniteListEvidence-  , inferKnownLength-  , inferTailFiniteList, inferConcatFiniteList-  , inferPrefixFiniteList, inferSuffixFiniteList-  , inferSnocFiniteList, inferInitFiniteList-  , inferTakeNFiniteList, inferDropNFiniteList, inferReverseFiniteList-  ) where--import           Data.Proxy       (Proxy (..))-import           Data.Type.Equality      ((:~:)(..))-import           Numeric.TypeLits-import           Unsafe.Coerce    (unsafeCoerce)---- | Synonym for a type-level cons---     (injective, since this is just a synonym for the list constructor)-type (a :: k) :+ (as :: [k]) = a ': as-infixr 5 :+--- | Prefix-style synonym for cons-type Cons (n :: k) (ns :: [k]) = n :+ ns---- | Synonym for a type-level snoc (injective!)-type (ns :: [k]) +: (n :: k) = Snoc ns n-infixl 5 +:--- | Prefix-style synonym for snoc-type Snoc (ns :: [k]) (n :: k) = GetSnoc (DoSnoc ns n)----- | List concatenation-type family (as :: [k]) ++ (bs :: [k]) :: [k] where-    (++) '[] bs = bs-    (++) as '[] = as-    (++) (a :+ as) bs = a :+ (as ++ bs)-infixr 5 ++---- | 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)----- | Synonym for an empty type-level list-type Empty = '[]---type family Take (n::Nat) (xs :: [k]) :: [k] where-    Take _ '[] = '[]-    Take 0 xs = '[]-    Take n (x :+ xs) = x :+ Take (n-1) xs---type family Drop (n::Nat) (xs :: [k]) :: [k] where-    Drop _ '[] = '[]-    Drop 0 xs = xs-    Drop n (x :+ xs) = Drop (n-1) xs--type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where-    Suffix '[] bs = bs-    Suffix as as = '[]-    Suffix (_ :+ as) (_ :+ asbs) = Suffix as asbs--type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where-    Prefix '[] as = as-    Prefix bs bs = '[]-    Prefix bs asbs = Take (Length asbs - Length bs) asbs---type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where-    IsPrefix '[] _ = 'True-    IsPrefix (a :+ as) (a :+ asbs) = IsPrefix as asbs-    IsPrefix as as = 'True-    IsPrefix _ _= 'False--type family IsSuffix (as :: [k]) (asbs :: [k]) :: Bool where-    IsSuffix '[] _ = 'True-    IsSuffix bs bs = 'True-    IsSuffix bs (_ :+ sbs) = IsSuffix bs sbs-    IsSuffix _ _ = 'False---type family Head (xs :: [k]) :: k where-    Head (x :+ xs) = x-    Head '[]       = TypeError ( 'Text-      "Head -- empty type-level list."-     )--type family Tail (xs :: [k]) :: [k] where-    Tail (x :+ xs) = xs-    Tail '[]       = TypeError ( 'Text-      "Tail -- empty type-level list."-     )--type family Init (xs :: [k]) :: [k] where-    Init '[x] = '[]-    Init (x :+ xs) = x :+ Init xs-    Init '[]       = TypeError ( 'Text-      "Init -- empty type-level list."-     )--type family Last (xs :: [k]) :: k where-    Last '[x] = x-    Last (x :+ xs) = Last xs-    Last '[]       = TypeError ( 'Text-      "Last -- empty type-level list."-     )----- | 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 where-    tlPrefix :: ConcatEvidence as bs asbs -> Proxy as-    tlSuffix :: ConcatEvidence as bs asbs -> Proxy bs-    tlConcat :: ConcatEvidence as bs asbs -> Proxy asbs--instance ( 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]) where-    tlPrefix _ = Proxy-    {-# INLINE tlPrefix #-}-    tlSuffix _ = Proxy-    {-# INLINE tlSuffix #-}-    tlConcat _ = Proxy-    {-# INLINE tlConcat #-}----- | Type level list, used together with FiniteList typeclass-data TypeList (xs :: [k]) where-    TLEmpty :: TypeList '[]-    TLCons  :: FiniteList xs => !(Proxy# x) -> !(TypeList xs) -> TypeList (x :+ xs)--instance Show (TypeList xs) where-    show TLEmpty = "TLEmpty"-    show (TLCons _ xs) = "TLCons " ++ show xs---- | 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-    -- | Length of a type-level list at type level-    type Length xs :: Nat-    -- | Length of a type-level list at term level-    order :: Int-    -- | Get type-level constructed list-    tList :: TypeList xs----instance FiniteList ('[] :: [k]) where-    type Length '[] = 0-    order = 0-    {-# INLINE order #-}-    tList = TLEmpty-    {-# INLINE tList #-}--instance FiniteList xs => FiniteList (x :+ xs :: [k]) where-    type Length (x :+ xs) = Length xs + 1-    order = 1 + order @k @xs-    {-# INLINE order #-}-    tList = TLCons proxy# (tList @k @xs)-    {-# INLINE tList #-}----unsafeEqEvidence :: forall x y . Evidence (x ~ y)-unsafeEqEvidence = case (unsafeCoerce Refl :: x :~: y) of Refl -> Evidence-{-# INLINE unsafeEqEvidence #-}---- | Length of a finite list is known and equal to `order` of the list-inferKnownLength :: forall xs . FiniteList xs => Evidence (KnownDim (Length xs))-inferKnownLength = reifyDim (order @_ @xs) f-  where-    f :: forall n . KnownDim n => Proxy# n -> Evidence (KnownDim (Length xs))-    f _ = unsafeCoerce (Evidence @(KnownDim n))-{-# INLINE inferKnownLength #-}----- | Tail of the list is also known list-inferTailFiniteList :: forall xs . FiniteList xs => Maybe (Evidence (FiniteList (Tail xs)))-inferTailFiniteList = case tList @_ @xs of-  TLEmpty    -> Nothing-  TLCons _ _ -> Just Evidence-{-# INLINE inferTailFiniteList #-}---- | Infer that concatenation is also finite-inferConcatFiniteList :: forall as bs-                       . (FiniteList as, FiniteList bs)-                      => Evidence (FiniteList (as ++ bs))-inferConcatFiniteList = case tList @_ @as of-  TLEmpty -> Evidence-  TLCons _ (_ :: TypeList as') -> case inferConcatFiniteList @as' @bs of-      Evidence -> case unsafeEqEvidence @(as ++ bs) @(Head as ': (as' ++ bs)) of-        Evidence -> Evidence-{-# INLINE inferConcatFiniteList #-}----- | Infer that prefix is also finite-inferPrefixFiniteList :: forall bs asbs-                       . (IsSuffix bs asbs ~ 'True, FiniteList bs, FiniteList asbs)-                      => Evidence (FiniteList (Prefix bs asbs))-inferPrefixFiniteList = reifyDim (order @_ @asbs - order @_ @bs) f-  where-    f :: forall n . KnownDim n => Proxy# n -> Evidence (FiniteList (Prefix bs asbs))-    f _ = unsafeCoerce (inferTakeNFiniteList @n @asbs)-{-# INLINE inferPrefixFiniteList #-}---- | Infer that suffix is also finite-inferSuffixFiniteList :: forall as asbs-                       . (IsPrefix as asbs ~ 'True, FiniteList as, FiniteList asbs)-                      => Evidence (FiniteList (Suffix as asbs))-inferSuffixFiniteList = case tList @_ @as of-  TLEmpty -> Evidence-  TLCons _ (_ :: TypeList as') -> case tList @_ @asbs of-    TLCons _ (_ :: TypeList asbs') -> case unsafeEqEvidence @(IsPrefix as' asbs') @'True-                                  `sumEvs` unsafeEqEvidence @(Suffix as' asbs') @(Suffix as asbs) of-      Evidence -> inferSuffixFiniteList @as' @asbs'-{-# INLINE inferSuffixFiniteList #-}---- | Make snoc almost as good as cons-inferSnocFiniteList :: forall xs z-                     . FiniteList xs-                    => Evidence (FiniteList (xs +: z))-inferSnocFiniteList = case tList @_ @xs of-  TLEmpty -> Evidence-  TLCons _ (_ :: TypeList xs') -> case inferSnocFiniteList @xs' @z-                              `sumEvs` unsafeEqEvidence @(Head xs :+ (xs' +: z)) @(xs +: z) of-    Evidence -> Evidence-{-# INLINE inferSnocFiniteList #-}---- | Init of the list is also known list-inferInitFiniteList :: forall xs-                     . FiniteList xs-                    => Maybe (Evidence (FiniteList (Init xs)))-inferInitFiniteList = case tList @_ @xs of-  TLEmpty -> Nothing-  TLCons _ TLEmpty -> Just Evidence-  TLCons _ (TLCons _ _ :: TypeList xs') -> case inferInitFiniteList @xs' of-    Just Evidence -> Just Evidence-    Nothing -> Nothing-{-# INLINE inferInitFiniteList #-}---- | Take KnownDim of the list is also known list-inferTakeNFiniteList :: forall n xs-                      . (KnownDim n, FiniteList xs)-                     => Evidence (FiniteList (Take n xs))-inferTakeNFiniteList = magic @n @xs (dimVal' @n) (tList @_ @xs)-    where-      magic :: forall m ns . Int -> TypeList ns -> Evidence (FiniteList (Take m ns))-      magic _ TLEmpty = Evidence-      magic 0 _ = case unsafeEqEvidence @(Take m ns) @'[] of-              Evidence -> Evidence-      magic n (TLCons _ tl) = case unsafeEqEvidence @(Head ns ': Take (m-1) (Tail ns)) @(Take m ns) of-              Evidence -> case magic @(m-1) @(Tail ns) (n-1) tl of-                Evidence -> Evidence-{-# INLINE inferTakeNFiniteList #-}---- | Drop KnownDim of the list is also known list-inferDropNFiniteList :: forall n xs-                      . (KnownDim n, FiniteList xs)-                     => Evidence (FiniteList (Drop n xs))-inferDropNFiniteList = case magic (dimVal' @n) (tList @_ @xs) of-      TLEmpty    -> Evidence-      TLCons _ _ -> Evidence-    where-      magic :: forall ns . Int -> TypeList ns -> TypeList (Drop n ns)-      magic _ TLEmpty       = TLEmpty-      magic 0 tl            = unsafeCoerce tl-      magic n (TLCons _ tl) = unsafeCoerce $ magic (n-1) tl-{-# INLINE inferDropNFiniteList #-}---- | Reverse of the list is also known list-inferReverseFiniteList :: forall xs . FiniteList xs => Evidence (FiniteList (Reverse xs))-inferReverseFiniteList = case magic (tList @_ @xs) TLEmpty of-      TLEmpty    -> Evidence-      TLCons _ _ -> Evidence-    where-      magic :: forall (ns :: [k]) (bs :: [k])-             . FiniteList bs-            => TypeList ns -> TypeList bs -> TypeList (Reverse ns)-      magic TLEmpty xs = unsafeCoerce xs-      magic (TLCons p sx) xs = magic (unsafeCoerce sx :: TypeList ns) (TLCons p xs)-{-# INLINE inferReverseFiniteList #-}---------------------------------------------------------------------------------------- Constructing evidence for our constraints------------------------------------------------------------------------------------- | 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)----- | 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)-inferConcat = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()]))-{-# INLINE inferConcat #-}----- | `as` being prefix of `asbs` 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-inferSuffix = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()]))-{-# INLINE inferSuffix #-}----- | `bs` being suffix of `asbs` 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-inferPrefix = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()]))-{-# INLINE inferPrefix #-}---------------------------------------------------------------------------------------- Tricks to make some type-level operations injective-------------------------------------------------------------------------------------- | A special data type that can have either a single element,---   or more than two.---   This feature is not enforced in the type system - this is just a way to make injective Snoc.-data Snocing k = SSingle k | Snocing [k]--type family DoSnoc (xs :: [k]) (z::k) = (ys :: Snocing k) | ys -> xs z where-    DoSnoc '[]       x = 'SSingle x-#if __GLASGOW_HASKELL__ >= 802-    DoSnoc (x :+ xs :: [k]) (y :: k) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [k]) :: Snocing k)-#else-    DoSnoc (x :+ xs :: [Nat]) (y :: Nat) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [Nat]) :: Snocing Nat)-    DoSnoc (x :+ xs :: [XNat]) (y :: XNat) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [XNat]) :: Snocing XNat)-#endif--type family GetSnoc (xs :: Snocing k) = (ys :: [k]) | ys -> xs where-    GetSnoc ('SSingle x) = '[x]-#if __GLASGOW_HASKELL__ >= 802-    GetSnoc ('Snocing (y :+ x :+ xs)) = y :+ x :+ xs-#else-    GetSnoc ('Snocing (y :+ x :+ xs) :: Snocing Nat) = (y :+ x :+ xs :: [Nat])-    GetSnoc ('Snocing (y :+ x :+ xs) :: Snocing XNat) = (y :+ x :+ xs :: [XNat])-#endif---- | Another data type to make Reverse injective.-data Reversing k = REmpty | Reversing [k]--type family Reversed (ts :: Reversing k) = (rs :: [k]) | rs -> ts where-    Reversed 'REmpty = '[]-#if __GLASGOW_HASKELL__ >= 802-    Reversed ('Reversing (x :+ xs)) = x :+ xs-#else-    Reversed ('Reversing (x :+ xs) :: Reversing Nat) = (x :+ xs :: [Nat])-    Reversed ('Reversing (x :+ xs) :: Reversing XNat) = (x :+ xs :: [XNat])-#endif---type family DoReverse (as :: [k]) = (rs :: Reversing k) | rs -> as where-    DoReverse '[]  = 'REmpty-#if __GLASGOW_HASKELL__ >= 802-    DoReverse (a :+ as) = 'Reversing (Reversed (DoReverse as) +: a)-#else-    DoReverse (a :+ as :: [Nat]) = ('Reversing (Reversed (DoReverse as) +: a :: [Nat]) :: Reversing Nat)-    DoReverse (a :+ as :: [XNat]) = ('Reversing (Reversed (DoReverse as) +: a :: [XNat]) :: Reversing XNat)-#endif

@@ -1,289 +0,0 @@-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE MagicHash                 #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE UnboxedTuples             #-}-{-# LANGUAGE BangPatterns              #-}-{-# LANGUAGE Strict                    #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.Traverse--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Map a function over all dimensions provided dimension indices or offsets.-----------------------------------------------------------------------------------module Numeric.Dimensions.Traverse-  ( overDim#, overDim_#, overDimIdx#, overDimIdx_#, overDimOff#, overDimOff_#-  , overDimPart#-  , foldDim, foldDimIdx, foldDimOff-  , foldDimReverse, foldDimReverseIdx-  ) where---import           GHC.Exts--import           Numeric.Dimensions.Dim-import           Numeric.Dimensions.Idx------ | Traverse over all dimensions keeping track of index and offset-overDim# :: Dim (ds :: [Nat])-         -> (Idx ds -> Int# -> a -> State# s -> (# State# s, a #)) -- ^ function to map over each dimension-         -> Int# -- ^ Initial offset-         -> Int# -- ^ offset step-         -> a-         -> State# s-         -> (# State# s, a #)-overDim# ds f off0# step# a0 s0 = case overDim'# ds g off0# a0 s0 of-                              (# s1, _, a1 #) -> (# s1, a1 #)-  where-    g i off# a s = case f i off# a s of-                    (# t, b #) -> (# t, off# +# step#, b #)-{-# INLINE overDim# #-}---- | Fold over all dimensions keeping track of index and offset-foldDim :: Dim (ds :: [Nat])-        -> (Idx ds -> Int# -> a -> a) -- ^ function to map over each dimension-        -> Int# -- ^ Initial offset-        -> Int# -- ^ offset step-        -> a -> a-foldDim ds f off0# step# a0 = case foldDim' ds g off0# a0 of-                              (# _, a1 #) -> a1-  where-    g i off# a = (# off# +# step#, f i off# a #)-{-# INLINE foldDim #-}---- | Fold over all dimensions in reverse order keeping track of index and offset-foldDimReverse :: Dim (ds :: [Nat])-               -> (Idx ds -> Int# -> a -> a) -- ^ function to map over each dimension-               -> Int# -- ^ Initial offset-               -> Int# -- ^ offset step (substracted from initial offset)-               -> a -> a-foldDimReverse ds f off0# step# a0 = case foldDimReverse' ds g (off0# +# n# *# step# -# step#) a0 of-                              (# _, a1 #) -> a1-  where-    !(I# n#) = dimVal ds-    g i off# a = (# off# -# step#, f i off# a #)-{-# INLINE foldDimReverse #-}------ | Same as overDim#, but with no return value-overDim_# :: Dim (ds :: [Nat])-          -> (Idx ds -> Int# -> State# s -> State# s) -- ^ function to map over each dimension-          -> Int# -- ^ Initial offset-          -> Int# -- ^ offset step-          -> State# s-          -> State# s-overDim_# ds f off0# step# s0 = case overDim_'# ds g off0# s0 of-                              (# s1, _ #) -> s1-  where-    g i off# s = (# f i off# s, off# +# step# #)-{-# INLINE overDim_# #-}---- | 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 #)-overDimIdx# D f = f Z-overDimIdx# ((Dn :: Dim n) :* (!ds)) f = overDimIdx# ds (loop 1)-  where-    n = dimVal' @n-    loop i js a s | i > n = (# s,  a #)-                  | otherwise = case f (i:!js) a s of-                            (# s', b #) -> loop (i+1) js b s'---- | Fold all dimensions keeping track of indices-foldDimIdx :: Dim (ds :: [Nat])-            -> (Idx ds -> a -> a)-            -> a -> a-foldDimIdx D f = f Z-foldDimIdx ((Dn :: Dim n) :* (!ds)) f = foldDimIdx ds (loop 1)-  where-    n = dimVal' @n-    loop i js a | i > n = a-                | otherwise = loop (i+1) js $! f (i:!js) a---- | Fold all dimensions in reverse order keeping track of indices-foldDimReverseIdx :: Dim (ds :: [Nat])-                  -> (Idx ds -> a -> a)-                  -> a -> a-foldDimReverseIdx D f = f Z-foldDimReverseIdx ((Dn :: Dim n) :* (!ds)) f = foldDimReverseIdx ds (loop n)-  where-    n = dimVal' @n-    loop i js a | i > n = a-                | otherwise = loop (i-1) js $! f (i:!js) 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-overDimIdx_# D f = f Z-overDimIdx_# ((Dn :: Dim n) :* (!ds)) f = overDimIdx_# ds (loop 1)-  where-    n = dimVal' @n-    loop i js s | i > n = s-                | otherwise =  loop (i+1) js (f (i:!js) s)---- | Traverse over all dimensions keeping track of total offset-overDimOff# :: Dim (ds :: [Nat])-            -> (Int# -> a -> State# s -> (# State# s, a #)) -- ^ function to map over each dimension-            -> Int# -- ^ Initial offset-            -> Int# -- ^ offset step-            -> a -> State# s -> (# State# s, a #)-overDimOff# ds f off0# step# = loop off0#-  where-    off1# = case dimVal ds of I# n# -> n# *# step# +# off0#-    cond# = if isTrue# (off1# >=# off0#)-             then \off -> isTrue# (off >=# off1#)-             else \off -> isTrue# (off <=# off1#)-    loop off# a s | cond# off# = (# s,  a #)-                  | otherwise = case f off# a s of-                                  (# s', b #) -> loop (off# +# step#) b s'---- | Fold over all dimensions keeping track of total offset-foldDimOff :: Dim (ds :: [Nat])-           -> (Int# -> a -> a) -- ^ function to map over each dimension-           -> Int# -- ^ Initial offset-           -> Int# -- ^ offset step-           -> a -> a-foldDimOff ds f off0# step# = loop off0#-  where-    off1# = case dimVal ds of I# n# -> n# *# step# +# off0#-    cond# = if isTrue# (off1# >=# off0#)-             then \off -> isTrue# (off >=# off1#)-             else \off -> isTrue# (off <=# off1#)-    loop off# a | cond# off# = a-                | otherwise  = loop (off# +# step#) $! f off# a----- | Traverse over all dimensions keeping track of total offset, with not return value-overDimOff_# :: Dim (ds :: [Nat])-             -> (Int# -> State# s -> State# s) -- ^ function to map over each dimension-             -> Int# -- ^ Initial offset-             -> Int# -- ^ offset step-             -> State# s -> State# s-overDimOff_# ds f off0# step# = loop off0#-  where-    off1# = case dimVal ds of I# n# -> n# *# step# +# off0#-    cond# = if isTrue# (off1# >=# off0#)-            then \off -> isTrue# (off >=# off1#)-            else \off -> isTrue# (off <=# off1#)-    loop off# s | cond# off# = s-                | otherwise = loop (off# +# step#) (f off# 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 #)) -- ^ function to map over each dimension-             -> Int# -- ^ Initial offset-             -> Int# -- ^ offset step-             -> a-             -> State# s-             -> (# State# s, a #)-overDimPart# imin imax f off0 step = overDimPart'# offs imin imax f off0-    where-      offs = createOffsets (dim @ds) (I# step)-      createOffsets :: forall (ns :: [Nat]) . Dim ns -> Int -> Idx ns-      createOffsets D _ = Z-      createOffsets ((Dn :: Dim n) :* (!ds)) k = k :! createOffsets ds (k * dimVal' @n)-------overDim'# :: Dim (ds :: [Nat])-          -> (Idx ds -> Int# -> a -> State# s -> (# State# s, Int#, a #)) -- ^ function to map over each dimension-          -> Int# -- ^ Initial offset-          -> a-          -> State# s-          -> (# State# s, Int#,  a #)-overDim'# D f = f Z-overDim'# ((Dn :: Dim n) :* (!ds)) f = overDim'# ds (loop 1)-  where-    n = dimVal' @n-    loop i js off# a s | i > n = (# s , off# , a #)-                       | otherwise = case f (i:!js) off# a s of-                                 (# s', off1#, b #) -> loop (i+1) js off1# b s'----foldDim' :: Dim (ds :: [Nat])-         -> (Idx ds -> Int# -> a -> (# Int#, a #)) -- ^ function to map over each dimension-         -> Int# -- ^ Initial offset-         -> a -> (# Int#,  a #)-foldDim' D f = f Z-foldDim' ((Dn :: Dim n) :* (!ds)) f = foldDim' ds (loop 1)-  where-    n = dimVal' @n-    loop i js off# a | i > n = (#  off#, a #)-                     | otherwise = case f (i:!js) off# a of-                               (# off1#, b #) -> loop (i+1) js off1# b--foldDimReverse' :: Dim (ds :: [Nat])-                -> (Idx ds -> Int# -> a -> (# Int#, a #)) -- ^ function to map over each dimension-                -> Int# -- ^ Initial offset-                -> a -> (# Int#,  a #)-foldDimReverse' D f = f Z-foldDimReverse' ((Dn :: Dim n) :* (!ds)) f = foldDimReverse' ds (loop n)-  where-    n = dimVal' @n-    loop i js off# a | i <= 0 = (#  off#, a #)-                     | otherwise = case f (i:!js) off# a of-                                (# off1#, b #) -> loop (i-1) js off1# b----overDim_'# :: Dim (ds :: [Nat])-           -> (Idx ds -> Int# -> State# s -> (# State# s, Int# #)) -- ^ function to map over each dimension-           -> Int# -- ^ Initial offset-           -> State# s-           -> (# State# s, Int# #)-overDim_'# D f = f Z-overDim_'# ((Dn :: Dim n) :* (!ds)) f = overDim_'# ds (loop 1)-  where-    n = dimVal' @n-    loop i js off# s | i > n = (# s , off#  #)-                     | otherwise = case f (i:!js) off# s of-                               (# s', off1# #) -> loop (i+1) js off1# s'---overDimPart'# :: Idx (ds :: [Nat])-              -> Idx (ds :: [Nat])-              -> Idx (ds :: [Nat])-              -> (Idx ds -> Int# -> a -> State# s -> (# State# s, a #)) -- ^ function to map over each dimension-              -> Int# -- ^ Initial offset-              -> a-              -> State# s-              -> (# State# s, a #)-overDimPart'# _ Z Z f off0# = f Z off0#-overDimPart'# (I# iW:!iws) (iMin:!mins) (iMax:!maxs) f off0#-    | iMax >= iMin = overDimPart'# iws mins maxs (loop iMin) (off0# +# minOff#)-    | otherwise    = overDimPart'# iws mins maxs (looi iMin) (off0# +# minOff#)-  where-    minOff# = case iMin of I# i -> iW *# (i -# 1#)-    loop i js off# a s | i > iMax = (# s, a #)-                       | otherwise = case f (i:!js) off# a s of-                               (# s', b #) -> loop (i+1) js (off# +# iW) b s'-    looi i js off# a s | i < iMax = (# s, a #)-                       | otherwise = case f (i:!js) off# a s of-                               (# s', b #) -> looi (i-1) js (off# -# iW) b s'

@@ -1,113 +0,0 @@-{-# LANGUAGE DataKinds           #-}-{-# LANGUAGE KindSignatures      #-}-{-# LANGUAGE MagicHash           #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE UnboxedTuples       #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.Traverse.IO--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ 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-  ( overDim, overDim_, overDimIdx, overDimIdx_, overDimOff, overDimOff_, overDimPart-  , foldDim, foldDimIdx, foldDimOff-  ) where---import           GHC.Exts-import           GHC.IO                      (IO (..))--import           Numeric.Dimensions.Dim-import           Numeric.Dimensions.Idx-import           Numeric.Dimensions.Traverse------ | Traverse over all dimensions keeping track of index and offset-overDim :: Dim (ds :: [Nat])-        -> (Idx ds -> Int# -> a -> IO a) -- ^ function to map over each dimension-        -> Int# -- ^ Initial offset-        -> Int# -- ^ offset step-        -> a -> IO a-overDim ds stf off0# step# = IO . overDim# ds (\i off# a -> case stf i off# a of-                                                           IO f -> f-                                         ) off0# step#-{-# INLINE overDim #-}---- | Traverse over all dimensions keeping track of indices-overDimIdx :: Dim (ds :: [Nat])-           -> (Idx ds -> a -> IO a)-           -> a -> IO a-overDimIdx ds stf = IO . overDimIdx# ds (\i a -> case stf i a of IO f -> f)-{-# INLINE overDimIdx #-}---- | Traverse over all dimensions keeping track of total offset-overDimOff :: Dim (ds :: [Nat])-        -> (Idx ds -> Int# -> a -> IO a) -- ^ function to map over each dimension-        -> Int# -- ^ Initial offset-        -> Int# -- ^ offset step-        -> a -> IO a-overDimOff ds stf off0# step# = IO . overDim# ds (\i off# a -> case stf i off# a of-                                                           IO f -> f-                                         ) off0# step#-{-# INLINE overDimOff #-}------ | Same as overDim#, but with no return value-overDim_ :: Dim (ds :: [Nat])-         -> (Idx ds -> Int# -> IO ()) -- ^ function to map over each dimension-         -> Int# -- ^ Initial offset-         -> Int# -- ^ offset step-         -> IO ()-overDim_ ds stf off0# step# = fst'# $ overDim_# ds (\i off# -> fst# (stf i off#)-                                          ) off0# step#-{-# INLINE overDim_ #-}---- | Traverse over all dimensions keeping track of indices, with no return value-overDimIdx_ :: Dim (ds :: [Nat])-            -> (Idx ds -> IO ())-            -> IO ()-overDimIdx_ ds stf = fst'# $ overDimIdx_# ds (\i -> fst# (stf i))-{-# INLINE overDimIdx_ #-}----- | Traverse over all dimensions keeping track of total offset, with not return value-overDimOff_ :: Dim (ds :: [Nat])-            -> (Int# -> IO ()) -- ^ function to map over each dimension-            -> Int# -- ^ Initial offset-            -> Int# -- ^ offset step-            -> IO ()-overDimOff_ ds stf off0# step# = fst'# $ overDimOff_# ds (\off#-> fst# (stf off#)-                                         ) off0# step#-{-# INLINE overDimOff_ #-}--fst# :: IO () -> State# RealWorld -> State# RealWorld-fst# (IO f) s = case f s of (# t, _ #) -> t-{-# INLINE fst# #-}--fst'# :: (State# RealWorld -> State# RealWorld) -> IO ()-fst'# f = IO $ \s -> case f s of t -> (# t, () #)---- | 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) -- ^ function to map over each dimension-            -> Int# -- ^ Initial offset-            -> Int# -- ^ offset step-            -> a -> IO a-overDimPart iMin iMax stf off0# step# = IO . overDimPart# iMin iMax (\i off# a -> case stf i off# a of-                                                                   IO f -> f-                                                              ) off0# step#-{-# INLINE overDimPart #-}

@@ -1,113 +0,0 @@-{-# LANGUAGE DataKinds           #-}-{-# LANGUAGE KindSignatures      #-}-{-# LANGUAGE MagicHash           #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE UnboxedTuples       #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.Traverse.ST--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ 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-  ( overDim, overDim_, overDimIdx, overDimIdx_, overDimOff, overDimOff_, overDimPart-  , foldDim, foldDimIdx, foldDimOff-  ) where---import           GHC.Exts-import           GHC.ST                      (ST (..))--import           Numeric.Dimensions.Dim-import           Numeric.Dimensions.Idx-import           Numeric.Dimensions.Traverse------ | Traverse over all dimensions keeping track of index and offset-overDim :: Dim (ds :: [Nat])-        -> (Idx ds -> Int# -> a -> ST s a) -- ^ function to map over each dimension-        -> Int# -- ^ Initial offset-        -> Int# -- ^ offset step-        -> a -> ST s a-overDim ds stf off0# step# = ST . overDim# ds (\i off# a -> case stf i off# a of-                                                           ST f -> f-                                         ) off0# step#-{-# INLINE overDim #-}---- | Traverse over all dimensions keeping track of indices-overDimIdx :: Dim (ds :: [Nat])-           -> (Idx ds -> a -> ST s a)-           -> a -> ST s a-overDimIdx ds stf = ST . overDimIdx# ds (\i a -> case stf i a of ST f -> f)-{-# INLINE overDimIdx #-}---- | Traverse over all dimensions keeping track of total offset-overDimOff :: Dim (ds :: [Nat])-        -> (Idx ds -> Int# -> a -> ST s a) -- ^ function to map over each dimension-        -> Int# -- ^ Initial offset-        -> Int# -- ^ offset step-        -> a -> ST s a-overDimOff ds stf off0# step# = ST . overDim# ds (\i off# a -> case stf i off# a of-                                                           ST f -> f-                                         ) off0# step#-{-# INLINE overDimOff #-}------ | Same as overDim#, but with no return value-overDim_ :: Dim (ds :: [Nat])-         -> (Idx ds -> Int# -> ST s ()) -- ^ function to map over each dimension-         -> Int# -- ^ Initial offset-         -> Int# -- ^ offset step-         -> ST s ()-overDim_ ds stf off0# step# = fst'# $ overDim_# ds (\i off# -> fst# (stf i off#)-                                          ) off0# step#-{-# INLINE overDim_ #-}---- | Traverse over all dimensions keeping track of indices, with no return value-overDimIdx_ :: Dim (ds :: [Nat])-            -> (Idx ds -> ST s ())-            -> ST s ()-overDimIdx_ ds stf = fst'# $ overDimIdx_# ds (\i -> fst# (stf i))-{-# INLINE overDimIdx_ #-}----- | Traverse over all dimensions keeping track of total offset, with not return value-overDimOff_ :: Dim (ds :: [Nat])-            -> (Int# -> ST s ()) -- ^ function to map over each dimension-            -> Int# -- ^ Initial offset-            -> Int# -- ^ offset step-            -> ST s ()-overDimOff_ ds stf off0# step# = fst'# $ overDimOff_# ds (\off#-> fst# (stf off#)-                                         ) off0# step#-{-# INLINE overDimOff_ #-}--fst# :: ST s () -> State# s -> State# s-fst# (ST f) s = case f s of (# t, _ #) -> t-{-# INLINE fst# #-}--fst'# :: (State# s -> State# s) -> ST s ()-fst'# f = ST $ \s -> case f s of t -> (# t, () #)---- | 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) -- ^ function to map over each dimension-            -> Int# -- ^ Initial offset-            -> Int# -- ^ offset step-            -> a -> ST s a-overDimPart iMin iMax stf off0# step# = ST . overDimPart# iMin iMax (\i off# a -> case stf i off# a of-                                                                   ST f -> f-                                                              ) off0# step#-{-# INLINE overDimPart #-}

@@ -1,118 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes       #-}-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces        #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE FlexibleInstances         #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE MagicHash                 #-}-{-# LANGUAGE MultiParamTypeClasses     #-}-{-# LANGUAGE PolyKinds                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE RoleAnnotations           #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeFamilies              #-}-{-# LANGUAGE TypeFamilyDependencies    #-}-{-# LANGUAGE TypeInType                #-}-{-# LANGUAGE TypeOperators             #-}-{-# LANGUAGE UndecidableInstances      #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.XDim--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Some dimensions in a type-level dimension list may by not known at compile time.-----------------------------------------------------------------------------------module Numeric.Dimensions.XDim-  ( -- * Data types-    XDim (..), xdim, xDimVal-    -- * Constraints-  , XDimensions (..)-  ) where---import           Data.Maybe              (isJust)-import           Data.Type.Equality      ((:~:)(..))-import           GHC.Exts                (unsafeCoerce#)--import           Numeric.Dimensions.Dim-import           Numeric.TypeLits----- | 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])-  = forall ns . ( FixedDim xns ns ~ ns-                , FixedXDim xns ns ~ xns-                ) => XDim (Dim ns)---class XDimensions (xds :: [XNat]) where-    wrapDim :: Dim (ds :: [Nat]) -> Maybe (Dim xds)---instance XDimensions '[] where-    wrapDim D = Just D-    wrapDim _ = Nothing-    {-# INLINE wrapDim #-}--instance (XDimensions xs, KnownDim m) => XDimensions (XN m ': xs) where-    wrapDim D = Nothing-    wrapDim ((d@Dn :: Dim d) :* ds) =-      if dimVal d >= dimVal' @m-      then case (wrapDim @xs ds, unsafeEqEvidence @(m <=? d) @'True) of-            (Just xds, Evidence) -> Just (Dx d :* xds)-            (Nothing, _) -> Nothing-      else Nothing--instance (XDimensions xs, KnownDim n) => XDimensions (N n ': xs) where-  wrapDim D = Nothing-  wrapDim ((Dn :: Dim d) :* ds) =-    if dimVal' @d == dimVal' @n-    then case (wrapDim @xs ds, unsafeEqEvidence @n @d) of-          (Just xds, Evidence) -> Just (Dn @d :* xds)-          (Nothing, _) -> Nothing-    else Nothing----- | Loose compile-time information about dimensionalities-xdim :: forall (ds :: [Nat]) (xds :: [XNat])-      . ( Dimensions ds-        , XDimensions xds) => Maybe (Dim xds)-xdim = wrapDim @xds @ds (dim @ds)-{-# INLINE xdim #-}------ | Construct dimensionality at runtime-xDimVal :: Dim (xns :: [XNat]) -> XDim xns-xDimVal D = XDim D-xDimVal ((Dn :: Dim n) :* ds) = case xDimVal ds of-  XDim ps -> XDim (Dn @n :* ps)-xDimVal (Dx d :* ds) = case xDimVal ds of-  XDim ps -> XDim (d :* ps)---instance Show (XDim xns) where-    show (XDim p) = 'X' : show p--instance Eq (XDim xds) where-    XDim as == XDim bs = isJust $ sameDim as bs--instance Ord (XDim xds) where-    compare (XDim as) (XDim bs) = compareDim as bs---unsafeEqEvidence :: forall x y . Evidence (x ~ y)-unsafeEqEvidence = case (unsafeCoerce# Refl :: x :~: y) of Refl -> Evidence-{-# INLINE unsafeEqEvidence #-}

@@ -0,0 +1,35 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Tuple+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+--+-----------------------------------------------------------------------------+module Numeric.Tuple+    ( module TS+    , toStrict, fromStrict+    ) where++import Numeric.Tuple.Strict as TS+import qualified Numeric.Tuple.Lazy as TL+import Unsafe.Coerce (unsafeCoerce)++toStrict :: TL.Tuple xs -> TS.Tuple xs+toStrict U = U+toStrict (TL.Id x :* xs)+  = let !y = x `seq` TS.Id x+        !ys = toStrict xs+    in y :* ys+#if __GLASGOW_HASKELL__ >= 802+#else+toStrict _ = error "Tuple.toStrict: impossible argument"+#endif++fromStrict :: TS.Tuple xs -> TL.Tuple xs+fromStrict = unsafeCoerce+{-# INLINE fromStrict #-}

@@ -0,0 +1,320 @@+{-# LANGUAGE AllowAmbiguousTypes        #-}+{-# LANGUAGE BangPatterns               #-}+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE DeriveDataTypeable         #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE DeriveTraversable          #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GADTs                      #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE IncoherentInstances        #-}+{-# LANGUAGE KindSignatures             #-}+{-# LANGUAGE MagicHash                  #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE PatternSynonyms            #-}+{-# LANGUAGE PolyKinds                  #-}+{-# LANGUAGE Rank2Types                 #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE TypeFamilyDependencies     #-}+{-# LANGUAGE TypeOperators              #-}+{-# LANGUAGE UndecidableInstances       #-}+{-# LANGUAGE ViewPatterns               #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Tuple.Lazy+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+--+-----------------------------------------------------------------------------+module Numeric.Tuple.Lazy+    ( Id (..), Tuple+    , TypedList (U, (:*), (:$), (:!), Empty, TypeList, Cons, Snoc, Reverse)+    , (*$), ($*), (*!), (!*)+    ) where+++import           Control.Arrow         (first)+import           Control.Monad.Fix+import           Control.Monad.Zip+import           Data.Bits             (Bits, FiniteBits)+import           Data.Coerce+import           Data.Data             (Data)+import           Data.Foldable+import           Data.Ix               (Ix)+import           Data.Monoid           (Monoid (..))+import           Data.Semigroup        (Semigroup (..))+import           Data.String           (IsString)+import           Foreign.Storable      (Storable)+import           GHC.Base              (Type)+import           GHC.Exts+import           GHC.Generics          (Generic, Generic1)+import qualified GHC.Read              as Read+import qualified Text.Read             as Read++import           Numeric.Type.List+import           Numeric.TypedList++-- | This is an almost complete copy of `Data.Functor.Identity`+--   by (c) Andy Gill 2001.+newtype Id a = Id { runId :: a }+    deriving ( Bits, Bounded, Data, Enum, Eq, FiniteBits, Floating, Fractional+             , Generic, Generic1, Integral, IsString, Ix, Monoid, Num, Ord+             , Real, RealFrac, RealFloat , Semigroup, Storable, Traversable)+++instance (Read a) => Read (Id a) where+    readsPrec d = fmap (first Id) . readsPrec d++instance (Show a) => Show (Id a) where+    showsPrec d = showsPrec d . runId++instance Foldable Id where+    foldMap          = coerce+    elem             = (. runId) #. (==)+    foldl            = coerce+    foldl'           = coerce+    foldl1 _         = runId+    foldr f z (Id x) = f x z+    foldr'           = foldr+    foldr1 _         = runId+    length _         = 1+    maximum          = runId+    minimum          = runId+    null _           = False+    product          = runId+    sum              = runId+    toList (Id x)    = [x]++instance Functor Id where+    fmap     = coerce++instance Applicative Id where+    pure     = Id+    (<*>)    = coerce++instance Monad Id where+    m >>= k  = k (runId m)++instance MonadFix Id where+    mfix f   = Id (fix (runId . f))++instance MonadZip Id where+    mzipWith = coerce+    munzip   = coerce+++++-- | A tuple indexed by a list of types+type Tuple (xs :: [Type]) = TypedList Id xs+++-- Starting from GHC 8.2, compiler supports specifying lists of complete+-- pattern synonyms.+#if __GLASGOW_HASKELL__ >= 802+{-# COMPLETE U, (:$) #-}+{-# COMPLETE U, (:!) #-}+{-# COMPLETE Empty, (:$) #-}+{-# COMPLETE Empty, (:!) #-}+#endif+++-- | Constructing a type-indexed list+pattern (:$) :: forall (xs :: [Type])+              . ()+             => forall (y :: Type) (ys :: [Type])+              . (xs ~ (y ': ys)) => y -> Tuple ys -> Tuple xs+pattern (:$) x xs <- (Id x :* xs)+  where+    (:$) = (*$)+infixr 5 :$++-- | Constructing a type-indexed list+pattern (:!) :: forall (xs :: [Type])+              . ()+             => forall (y :: Type) (ys :: [Type])+              . (xs ~ (y ': ys)) => y -> Tuple ys -> Tuple xs+pattern (:!) x xs <- (forceCons -> Id x :* xs)+  where+    (:!) = (*!)+infixr 5 :!+++-- | Grow a tuple on the left O(1).+(*$) :: x -> Tuple xs -> Tuple (x :+ xs)+(*$) x xs = unsafeCoerce# (unsafeCoerce# x : unsafeCoerce# xs :: [Any])+{-# INLINE (*$) #-}+infixr 5 *$++-- | Grow a tuple on the left while evaluating arguments to WHNF O(1).+(*!) :: x -> Tuple xs -> Tuple (x :+ xs)+(*!) !x !xs = let !r = unsafeCoerce# x : unsafeCoerce# xs :: [Any]+              in unsafeCoerce# r+{-# INLINE (*!) #-}+infixr 5 *!++-- | Grow a tuple on the right.+--   Note, it traverses an element list inside O(n).+($*) :: Tuple xs -> x -> Tuple (xs +: x)+($*) xs x = unsafeCoerce# (unsafeCoerce# xs ++ [unsafeCoerce# x] :: [Any])+{-# INLINE ($*) #-}+infixl 5 $*++-- | Grow a tuple on the right while evaluating arguments to WHNF.+--   Note, it traverses an element list inside O(n).+(!*) :: Tuple xs -> x -> Tuple (xs +: x)+(!*) !xs !x = let !r = go (unsafeCoerce# x) (unsafeCoerce# xs) :: [Any]+                  go :: Any -> [Any] -> [Any]+                  go z []       = z `seq` [z]+                  go z (y : ys) = y `seq` y : go z ys+              in unsafeCoerce# r+{-# INLINE (!*) #-}+infixl 5 !*+++instance (All Semigroup xs) => Semigroup (Tuple xs) where+    U <> U = U+    (x :$ xs) <> (y :$ ys)+      = (x <> y) *$ ( xs <> ys)+#if __GLASGOW_HASKELL__ >= 802+#else+    _ <> _ = error "(<>): impossible combination of arguments"+#endif++instance ( Semigroup (Tuple xs)+         , RepresentableList xs+         , All Monoid xs) => Monoid (Tuple xs) where+    mempty = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Monoid ys => TypeList ys -> Tuple ys+        go U         = U+        go (_ :* xs) = mempty *$ go xs+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ = error "mempty/go: impossible combination of arguments"+#endif+    mappend = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Monoid ys+            => TypeList ys+            -> Tuple ys+            -> Tuple ys+            -> Tuple ys+        go U _ _ = U+        go (_ :* ts) (x :$ xs) (y :$ ys) = mappend x y *$ go ts xs ys+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ _ _ = error "mappend/go: impossible combination of arguments"+#endif+++instance (RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) where+    minBound = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Bounded ys => TypeList ys -> Tuple ys+        go U         = U+        go (_ :* xs) = minBound *$ go xs+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ = error "minBound/go: impossible combination of arguments"+#endif+    maxBound = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Bounded ys => TypeList ys -> Tuple ys+        go U         = U+        go (_ :* xs) = maxBound *$ go xs+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ = error "maxBound/go: impossible combination of arguments"+#endif++instance All Eq xs => Eq (Tuple xs) where+    (==) U U                 = True+    (==) (x :* tx) (y :* ty) = x == y && tx == ty+#if __GLASGOW_HASKELL__ >= 802+#else+    (==) _ _ = error "(==): impossible combination of arguments"+#endif+    (/=) U U                 = False+    (/=) (x :* tx) (y :* ty) = x /= y || tx /= ty+#if __GLASGOW_HASKELL__ >= 802+#else+    (/=) _ _ = error "(/=): impossible combination of arguments"+#endif++-- | Ord instance of the Tuple implements inverse lexicorgaphic ordering.+--   That is, the last element in the tuple is the most significant one.+--+--   Note, this will never work on infinite-dimensional tuples!+instance (All Eq xs, All Ord xs) => Ord (Tuple xs) where+    compare U U                 = EQ+    compare (x :* tx) (y :* ty) = compare tx ty <> compare x y+#if __GLASGOW_HASKELL__ >= 802+#else+    compare _ _ = error "compare: impossible combination of arguments"+#endif++instance All Show xs => Show (Tuple xs) where+    show U         = "U"+    show (x :* xs) = show x ++ " :* " ++ show xs+#if __GLASGOW_HASKELL__ >= 802+#else+    show _ = error "show: impossible combination of arguments"+#endif+    showsPrec _ U = showString "U"+    showsPrec p (x :* xs) = showParen (p >= 5)+                          $ showsPrec 5 x+                          . showString " :* "+                          . showsPrec 5 xs+#if __GLASGOW_HASKELL__ >= 802+#else+    showsPrec _ _ = error "showsPrec: impossible combination of arguments"+#endif++instance (RepresentableList xs, All Read xs) => Read (Tuple xs) where+    readPrec = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Read ys => TypeList ys -> Read.ReadPrec (Tuple ys)+        go U = U <$ Read.expectP (Read.Symbol "U")+        go (_ :* ts) = Read.parens $ Read.prec 5 $ do+          x <- Read.step Read.readPrec+          Read.expectP (Read.Symbol ":*")+          xs <- Read.step $ go ts+          return (x :* xs)+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ = error "readPrec/go: impossible combination of arguments"+#endif++++--------------------------------------------------------------------------------+-- internal+--------------------------------------------------------------------------------+++-- | Internal (non-exported) 'Coercible' helper for 'elem'+--+-- See Note [Function coercion] in "Data.Foldable" for more details.+(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c+(#.) _f = coerce++forceCons :: Tuple xs -> Tuple xs+forceCons U = U+forceCons (Id x :* xs) = x `seq` xs `seq` (Id x :* xs)+#if __GLASGOW_HASKELL__ >= 802+#else+forceCons _ = error "forceCons: impossible combination of arguments"+#endif

@@ -0,0 +1,320 @@+{-# LANGUAGE AllowAmbiguousTypes        #-}+{-# LANGUAGE BangPatterns               #-}+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE DeriveDataTypeable         #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE DeriveTraversable          #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GADTs                      #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE IncoherentInstances        #-}+{-# LANGUAGE KindSignatures             #-}+{-# LANGUAGE MagicHash                  #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE PatternSynonyms            #-}+{-# LANGUAGE PolyKinds                  #-}+{-# LANGUAGE Rank2Types                 #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE TypeFamilyDependencies     #-}+{-# LANGUAGE TypeOperators              #-}+{-# LANGUAGE UndecidableInstances       #-}+{-# LANGUAGE ViewPatterns               #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Tuple.Strict+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+--+-----------------------------------------------------------------------------+module Numeric.Tuple.Strict+    ( Id (..), Tuple+    , TypedList (U, (:*), (:$), (:!), Empty, TypeList, Cons, Snoc, Reverse)+    , (*$), ($*), (*!), (!*)+    ) where+++import           Control.Arrow         (first)+import           Control.Monad.Fix+import           Control.Monad.Zip+import           Data.Bits             (Bits, FiniteBits)+import           Data.Coerce+import           Data.Data             (Data)+import           Data.Foldable+import           Data.Ix               (Ix)+import           Data.Monoid           (Monoid (..))+import           Data.Semigroup        (Semigroup (..))+import           Data.String           (IsString)+import           Foreign.Storable      (Storable)+import           GHC.Base              (Type)+import           GHC.Exts+import           GHC.Generics          (Generic, Generic1)+import qualified GHC.Read              as Read+import qualified Text.Read             as Read++import           Numeric.Type.List+import           Numeric.TypedList++-- | This is an almost complete copy of `Data.Functor.Identity`+--   by (c) Andy Gill 2001.+newtype Id a = Id { runId :: a }+    deriving ( Bits, Bounded, Data, Enum, Eq, FiniteBits, Floating, Fractional+             , Generic, Generic1, Integral, IsString, Ix, Monoid, Num, Ord+             , Real, RealFrac, RealFloat , Semigroup, Storable, Traversable)+++instance (Read a) => Read (Id a) where+    readsPrec d = fmap (first Id) . readsPrec d++instance (Show a) => Show (Id a) where+    showsPrec d = showsPrec d . runId++instance Foldable Id where+    foldMap          = coerce+    elem             = (. runId) #. (==)+    foldl            = coerce+    foldl'           = coerce+    foldl1 _         = runId+    foldr f z (Id x) = f x z+    foldr'           = foldr+    foldr1 _         = runId+    length _         = 1+    maximum          = runId+    minimum          = runId+    null _           = False+    product          = runId+    sum              = runId+    toList (Id x)    = [x]++instance Functor Id where+    fmap     = coerce++instance Applicative Id where+    pure     = Id+    (<*>)    = coerce++instance Monad Id where+    m >>= k  = k (runId m)++instance MonadFix Id where+    mfix f   = Id (fix (runId . f))++instance MonadZip Id where+    mzipWith = coerce+    munzip   = coerce+++++-- | A tuple indexed by a list of types+type Tuple (xs :: [Type]) = TypedList Id xs+++-- Starting from GHC 8.2, compiler supports specifying lists of complete+-- pattern synonyms.+#if __GLASGOW_HASKELL__ >= 802+{-# COMPLETE U, (:$) #-}+{-# COMPLETE U, (:!) #-}+{-# COMPLETE Empty, (:$) #-}+{-# COMPLETE Empty, (:!) #-}+#endif+++-- | Constructing a type-indexed list+pattern (:$) :: forall (xs :: [Type])+              . ()+             => forall (y :: Type) (ys :: [Type])+              . (xs ~ (y ': ys)) => y -> Tuple ys -> Tuple xs+pattern (:$) x xs <- (Id x :* xs)+  where+    (:$) = (*$)+infixr 5 :$++-- | Constructing a type-indexed list+pattern (:!) :: forall (xs :: [Type])+              . ()+             => forall (y :: Type) (ys :: [Type])+              . (xs ~ (y ': ys)) => y -> Tuple ys -> Tuple xs+pattern (:!) x xs <- (forceCons -> Id x :* xs)+  where+    (:!) = (*!)+infixr 5 :!+++-- | Grow a tuple on the left O(1).+(*$) :: x -> Tuple xs -> Tuple (x :+ xs)+(*$) x xs = unsafeCoerce# (unsafeCoerce# x : unsafeCoerce# xs :: [Any])+{-# INLINE (*$) #-}+infixr 5 *$++-- | Grow a tuple on the left while evaluating arguments to WHNF O(1).+(*!) :: x -> Tuple xs -> Tuple (x :+ xs)+(*!) !x !xs = let !r = unsafeCoerce# x : unsafeCoerce# xs :: [Any]+              in unsafeCoerce# r+{-# INLINE (*!) #-}+infixr 5 *!++-- | Grow a tuple on the right.+--   Note, it traverses an element list inside O(n).+($*) :: Tuple xs -> x -> Tuple (xs +: x)+($*) xs x = unsafeCoerce# (unsafeCoerce# xs ++ [unsafeCoerce# x] :: [Any])+{-# INLINE ($*) #-}+infixl 5 $*++-- | Grow a tuple on the right while evaluating arguments to WHNF.+--   Note, it traverses an element list inside O(n).+(!*) :: Tuple xs -> x -> Tuple (xs +: x)+(!*) !xs !x = let !r = go (unsafeCoerce# x) (unsafeCoerce# xs) :: [Any]+                  go :: Any -> [Any] -> [Any]+                  go z []       = z `seq` [z]+                  go z (y : ys) = y `seq` y : go z ys+              in unsafeCoerce# r+{-# INLINE (!*) #-}+infixl 5 !*+++instance (All Semigroup xs) => Semigroup (Tuple xs) where+    U <> U = U+    (x :! xs) <> (y :! ys)+      = (x <> y) *! ( xs <> ys)+#if __GLASGOW_HASKELL__ >= 802+#else+    _ <> _ = error "(<>): impossible combination of arguments"+#endif++instance ( Semigroup (Tuple xs)+         , RepresentableList xs+         , All Monoid xs) => Monoid (Tuple xs) where+    mempty = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Monoid ys => TypeList ys -> Tuple ys+        go U         = U+        go (_ :* xs) = mempty *! go xs+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ = error "mempty/go: impossible combination of arguments"+#endif+    mappend = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Monoid ys+            => TypeList ys+            -> Tuple ys+            -> Tuple ys+            -> Tuple ys+        go U _ _ = U+        go (_ :* ts) (x :! xs) (y :! ys) = mappend x y *! go ts xs ys+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ _ _ = error "mappend/go: impossible combination of arguments"+#endif+++instance (RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) where+    minBound = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Bounded ys => TypeList ys -> Tuple ys+        go U         = U+        go (_ :* xs) = minBound *! go xs+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ = error "minBound/go: impossible combination of arguments"+#endif+    maxBound = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Bounded ys => TypeList ys -> Tuple ys+        go U         = U+        go (_ :* xs) = maxBound *! go xs+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ = error "maxBound/go: impossible combination of arguments"+#endif++instance All Eq xs => Eq (Tuple xs) where+    (==) U U                 = True+    (==) (x :* tx) (y :* ty) = x == y && tx == ty+#if __GLASGOW_HASKELL__ >= 802+#else+    (==) _ _ = error "(==): impossible combination of arguments"+#endif+    (/=) U U                 = False+    (/=) (x :* tx) (y :* ty) = x /= y || tx /= ty+#if __GLASGOW_HASKELL__ >= 802+#else+    (/=) _ _ = error "(/=): impossible combination of arguments"+#endif++-- | Ord instance of the Tuple implements inverse lexicorgaphic ordering.+--   That is, the last element in the tuple is the most significant one.+--+--   Note, this will never work on infinite-dimensional tuples!+instance (All Eq xs, All Ord xs) => Ord (Tuple xs) where+    compare U U                 = EQ+    compare (x :* tx) (y :* ty) = compare tx ty <> compare x y+#if __GLASGOW_HASKELL__ >= 802+#else+    compare _ _ = error "compare: impossible combination of arguments"+#endif++instance All Show xs => Show (Tuple xs) where+    show U         = "U"+    show (x :* xs) = show x ++ " :* " ++ show xs+#if __GLASGOW_HASKELL__ >= 802+#else+    show _ = error "show: impossible combination of arguments"+#endif+    showsPrec _ U = showString "U"+    showsPrec p (x :* xs) = showParen (p >= 5)+                          $ showsPrec 5 x+                          . showString " :* "+                          . showsPrec 5 xs+#if __GLASGOW_HASKELL__ >= 802+#else+    showsPrec _ _ = error "showsPrec: impossible combination of arguments"+#endif++instance (RepresentableList xs, All Read xs) => Read (Tuple xs) where+    readPrec = go (tList @Type @xs)+      where+        go :: forall (ys :: [Type])+            . All Read ys => TypeList ys -> Read.ReadPrec (Tuple ys)+        go U = U <$ Read.expectP (Read.Symbol "U")+        go (_ :* ts) = Read.parens $ Read.prec 5 $ do+          x <- Read.step Read.readPrec+          Read.expectP (Read.Symbol ":*")+          xs <- Read.step $ go ts+          return (x :* xs)+#if __GLASGOW_HASKELL__ >= 802+#else+        go _ = error "readPrec/go: impossible combination of arguments"+#endif++++--------------------------------------------------------------------------------+-- internal+--------------------------------------------------------------------------------+++-- | Internal (non-exported) 'Coercible' helper for 'elem'+--+-- See Note [Function coercion] in "Data.Foldable" for more details.+(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c+(#.) _f = coerce++forceCons :: Tuple xs -> Tuple xs+forceCons U = U+forceCons (Id x :* xs) = x `seq` xs `seq` (Id x :* xs)+#if __GLASGOW_HASKELL__ >= 802+#else+forceCons _ = error "forceCons: impossible combination of arguments"+#endif

@@ -0,0 +1,59 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds       #-}+{-# LANGUAGE GADTs           #-}+{-# LANGUAGE KindSignatures  #-}+{-# LANGUAGE Rank2Types      #-}+{-# LANGUAGE PolyKinds       #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Type.Evidence+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+-- Construct type-level evidence at runtime+--+-----------------------------------------------------------------------------+module Numeric.Type.Evidence+  ( Evidence (..), withEvidence, sumEvs, (+!+)+  , Evidence' (..), toEvidence, toEvidence'+  ) where+++import           GHC.Base (Type)+import           GHC.Exts (Constraint)+++-- | Bring an instance of certain class or constaint satisfaction evidence into scope.+data Evidence :: Constraint -> Type where+    E :: a => Evidence a++-- | Combine evidence+sumEvs :: Evidence a -> Evidence b -> Evidence (a,b)+sumEvs E E = E+{-# INLINE sumEvs #-}++infixl 4 +!++-- | Combine evidence+(+!+) :: Evidence a -> Evidence b -> Evidence (a,b)+(+!+) = sumEvs+{-# INLINE (+!+) #-}++-- | Pattern match agains evidence to get constraints info+withEvidence :: Evidence a -> (a => r) -> r+withEvidence d r = case d of E -> r+{-# INLINE withEvidence #-}++-- | Same as @Evidence@, but allows to separate constraint function from+--   the type it is applied to.+data Evidence' :: (k -> Constraint) -> k -> Type where+    E' :: c a => Evidence' c a++toEvidence :: Evidence' c a -> Evidence (c a)+toEvidence E' = E+{-# INLINE toEvidence #-}++toEvidence' :: Evidence (c a) -> Evidence' c a+toEvidence' E = E'+{-# INLINE toEvidence' #-}

@@ -0,0 +1,222 @@+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE ExplicitNamespaces     #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures         #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Type.List+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+-- Provides type-level operations on lists.+--+--+--------------------------------------------------------------------------------++module Numeric.Type.List+  ( -- * Basic operations+    type (++), type (+:), type (:+)+  , Empty, Cons, Snoc, Head+  , Tail, Init, Last, Concat, Reverse, Take, Drop, Length+  , All, Map+    -- * Working with concatenations+  , Suffix, Prefix, IsPrefix, IsSuffix+    -- * Term level functions+  , ConcatList+  ) where++import           GHC.Exts+import           GHC.TypeLits+++-- | Synonym for a type-level cons+--     (injective, since this is just a synonym for the list constructor)+type (a :: k) :+ (as :: [k]) = a ': as+infixr 5 :++-- | Prefix-style synonym for cons+type Cons (n :: k) (ns :: [k]) = n :+ ns++-- | Synonym for a type-level snoc (injective!)+type (ns :: [k]) +: (n :: k) = Snoc ns n+infixl 5 +:+-- | Prefix-style synonym for snoc+type Snoc (ns :: [k]) (n :: k) = GetSnoc k (DoSnoc k ns n)+++-- | List concatenation+type family (as :: [k]) ++ (bs :: [k]) :: [k] where+    (++) '[] bs = bs+    (++) as '[] = as+    (++) (a :+ as) bs = a :+ (as ++ bs)+infixr 5 ++++-- | Prefix-style synonym for concatenation+type Concat (as :: [k]) (bs :: [k]) = as ++ bs+++-- | Reverse a type-level list (injective!)+type Reverse (xs :: [k]) = Reversed k (DoReverse k xs)+++-- | Synonym for an empty type-level list+type Empty = '[]+++type family Take (n::Nat) (xs :: [k]) :: [k] where+    Take _ '[] = '[]+    Take 0 xs = '[]+    Take n (x :+ xs) = x :+ Take (n-1) xs+++type family Drop (n::Nat) (xs :: [k]) :: [k] where+    Drop _ '[] = '[]+    Drop 0 xs = xs+    Drop n (x :+ xs) = Drop (n-1) xs++type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where+    Suffix '[] bs = bs+    Suffix as as = '[]+    Suffix (_ :+ as) (_ :+ asbs) = Suffix as asbs++type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where+    Prefix '[] as = as+    Prefix bs bs = '[]+    Prefix bs asbs = Take (Length asbs - Length bs) asbs+++type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where+    IsPrefix '[] _ = 'True+    IsPrefix (a :+ as) (a :+ asbs) = IsPrefix as asbs+    IsPrefix as as = 'True+    IsPrefix _ _= 'False++type family IsSuffix (as :: [k]) (asbs :: [k]) :: Bool where+    IsSuffix '[] _ = 'True+    IsSuffix bs bs = 'True+    IsSuffix bs (_ :+ sbs) = IsSuffix bs sbs+    IsSuffix _ _ = 'False+++type family Head (xs :: [k]) :: k where+    Head (x :+ xs)  = x+    Head (KEmpty k) = TypeError ( 'Text+      "Head: empty type-level list."+      ':$$: FamErrMsg k+     )++type family Tail (xs :: [k]) :: [k] where+    Tail (x :+ xs)  = xs+    Tail (KEmpty k) = TypeError ( 'Text+      "Tail: empty type-level list."+      ':$$: FamErrMsg k+     )++type family Init (xs :: [k]) :: [k] where+    Init '[x]       = '[]+    Init (x :+ xs)  = x :+ Init xs+    Init (KEmpty k) = TypeError ( 'Text+      "Init: empty type-level list."+      ':$$: FamErrMsg k+     )++type family Last (xs :: [k]) :: k where+    Last '[x]       = x+    Last (x :+ xs)  = Last xs+    Last (KEmpty k) = TypeError ( 'Text+      "Last: empty type-level list."+      ':$$: FamErrMsg k+     )++type family Length (xs :: [k]) :: Nat where+    Length '[] = 0+    Length (_ ': xs) = 1 + Length xs+++type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where+    All _ '[] = ()+    All f (x ': xs) = (f x, All f xs)++type family Map (f :: a -> b) (xs :: [a]) :: [b] where+    Map f '[] = '[]+    Map f (x ': xs) = f x ': Map f 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++instance ( 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])++++type FamErrMsg k+  = 'Text "Type-level error occured when operating on a list of kind "+    ':<>: 'ShowType [k] ':<>: 'Text "."++--------------------------------------------------------------------------------+---- Tricks to make some type-level operations injective+--------------------------------------------------------------------------------++++-- | A special data type that can have either a single element,+--   or more than two.+--   This feature is not enforced in the type system - this is just a way to make injective Snoc.+data Snocing k    = SSingle k | SCons [k]+type SSingle k x  = 'SSingle (x :: k)+type SCons k xs   = 'SCons (xs :: [k])+type KCons k x xs = (x :: k) ': (xs :: [k])+type KEmpty k     = ('[] :: [k])+type KSingle k x  = ('[x] :: [k])++type family DoSnoc k (xs :: [k]) (z::k) = (ys :: Snocing k) | ys -> xs z where+    DoSnoc k '[]       x      = SSingle k x+    DoSnoc k (KCons k x xs) y =+      (SCons k (KCons k x (GetSnoc k (DoSnoc k xs y)) :: [k]) :: Snocing k)+++type family GetSnoc k (xs :: Snocing k) = (ys :: [k]) | ys -> xs where+    GetSnoc k (SSingle k x) = KSingle k x+    GetSnoc k (SCons k (KCons k y (KCons k x xs))) =+      KCons k y (KCons k x xs)++-- | Another data type to make Reverse injective.+data Reversing k    = REmpty | RReverse [k]+type REmpty    k    = 'REmpty+type RReverse  k xs = 'RReverse (xs :: [k])++++type family Reversed k (ts :: Reversing k) = (rs :: [k]) | rs -> ts where+    Reversed k (REmpty k) = KEmpty k+    Reversed k (RReverse k (KCons k x xs)) = KCons k x xs+++type family DoReverse k (as :: [k]) = (rs :: Reversing k) | rs -> as where+    DoReverse k '[]  = REmpty k+    DoReverse k (KCons k a as) =+      RReverse k (GetSnoc k (DoSnoc k (Reversed k (DoReverse k as)) a))

@@ -1,192 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes       #-}-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE FlexibleInstances         #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE MagicHash                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE RoleAnnotations           #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeFamilies              #-}-{-# LANGUAGE TypeOperators             #-}-{-# LANGUAGE UndecidableInstances      #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.TypeLits--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ This modules is based on `GHC.TypeLits` and re-exports its functionality.--- It provides `KnownDim` class that is similar to `KnownNat`, but keeps--- `Int`s instead of `Integer`s.--- A set of utility functions provide inference functionality, so--- that `KnownDim` can be preserved over some type-level operations.-----------------------------------------------------------------------------------module Numeric.TypeLits-  ( XNat (..), XN, N-    -- * Nats backed by Int-  , SomeIntNat (..), someIntNatVal, intNatVal, reifyDim-  , KnownDim (..), KnownDims, dimVal#, Proxy#, proxy#-    -- * Dynamically constructing evidence-  , Evidence (..), withEvidence, sumEvs, (+!+)-  , inferPlusKnownDim, inferMinusKnownDim, inferMinusKnownDimM-  , inferTimesKnownDim-    -- * Re-export original GHC TypeLits-  , module GHC.TypeLits-  , Proxy (..)-  ) where---import           Data.Proxy    (Proxy(..))-import           GHC.Exts      (Constraint, Proxy#, proxy#)-import           GHC.TypeLits-import           GHC.Types     (Type)-import           Unsafe.Coerce (unsafeCoerce)------ | 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 (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 = forall (n :: Nat) . KnownDim n => SomeIntNat (Proxy n)------ | This class gives the int associated with a type-level natural.---   Valid known dim must be not less than 0.-class KnownDim (n :: Nat) where-    -- | Get value of type-level dim at runtime-    dimVal' :: Int---- | A constraint family that makes sure all subdimensions are known.-type family KnownDims (ns :: [Nat]) :: Constraint where-    KnownDims '[] = ()-    KnownDims (x ': xs) = ( KnownDim x, KnownDims xs )---- | A variant of `dimVal'` that gets `Proxy#` as an argument.-dimVal# :: forall (n :: Nat) . KnownDim n => Proxy# n -> Int-dimVal# _ = dimVal' @n-{-# INLINE dimVal# #-}---- | Similar to `natVal` from `GHC.TypeLits`, but returns `Int`.-intNatVal :: forall n proxy . KnownDim n => proxy n -> Int-intNatVal _ = dimVal' @n--instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where-    {-# INLINE dimVal' #-}-    dimVal' = fromInteger (natVal' (proxy# :: Proxy# n))--instance {-# OVERLAPPING #-} KnownDim 0  where { {-# INLINE dimVal' #-}; dimVal' = 0 }-instance {-# OVERLAPPING #-} KnownDim 1  where { {-# INLINE dimVal' #-}; dimVal' = 1 }-instance {-# OVERLAPPING #-} KnownDim 2  where { {-# INLINE dimVal' #-}; dimVal' = 2 }-instance {-# OVERLAPPING #-} KnownDim 3  where { {-# INLINE dimVal' #-}; dimVal' = 3 }-instance {-# OVERLAPPING #-} KnownDim 4  where { {-# INLINE dimVal' #-}; dimVal' = 4 }-instance {-# OVERLAPPING #-} KnownDim 5  where { {-# INLINE dimVal' #-}; dimVal' = 5 }-instance {-# OVERLAPPING #-} KnownDim 6  where { {-# INLINE dimVal' #-}; dimVal' = 6 }-instance {-# OVERLAPPING #-} KnownDim 7  where { {-# INLINE dimVal' #-}; dimVal' = 7 }-instance {-# OVERLAPPING #-} KnownDim 8  where { {-# INLINE dimVal' #-}; dimVal' = 8 }-instance {-# OVERLAPPING #-} KnownDim 9  where { {-# INLINE dimVal' #-}; dimVal' = 9 }-instance {-# OVERLAPPING #-} KnownDim 10 where { {-# INLINE dimVal' #-}; dimVal' = 10 }-instance {-# OVERLAPPING #-} KnownDim 11 where { {-# INLINE dimVal' #-}; dimVal' = 11 }-instance {-# OVERLAPPING #-} KnownDim 12 where { {-# INLINE dimVal' #-}; dimVal' = 12 }-instance {-# OVERLAPPING #-} KnownDim 13 where { {-# INLINE dimVal' #-}; dimVal' = 13 }-instance {-# OVERLAPPING #-} KnownDim 14 where { {-# INLINE dimVal' #-}; dimVal' = 14 }-instance {-# OVERLAPPING #-} KnownDim 15 where { {-# INLINE dimVal' #-}; dimVal' = 15 }-instance {-# OVERLAPPING #-} KnownDim 16 where { {-# INLINE dimVal' #-}; dimVal' = 16 }-instance {-# OVERLAPPING #-} KnownDim 17 where { {-# INLINE dimVal' #-}; dimVal' = 17 }-instance {-# OVERLAPPING #-} KnownDim 18 where { {-# INLINE dimVal' #-}; dimVal' = 18 }-instance {-# OVERLAPPING #-} KnownDim 19 where { {-# INLINE dimVal' #-}; dimVal' = 19 }-instance {-# OVERLAPPING #-} KnownDim 20 where { {-# INLINE dimVal' #-}; dimVal' = 20 }----- | Similar to `someNatVal`, but for a single dimension-someIntNatVal :: Int -> Maybe SomeIntNat-someIntNatVal x | 0 > x     = Nothing-                | otherwise = Just (reifyDim x f)-  where-    f :: forall (n :: Nat) . KnownDim n => Proxy# n -> SomeIntNat-    f _ = SomeIntNat (Proxy @n)-{-# INLINE someIntNatVal #-}----- | This function does GHC's magic to convert user-supplied `dimVal'` 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 r . Int -> (forall (n :: Nat) . KnownDim n => Proxy# n -> r) -> r-reifyDim n k = unsafeCoerce (MagicDim k :: MagicDim r) n proxy#-{-# INLINE reifyDim #-}-newtype MagicDim r = MagicDim (forall (n :: Nat) . KnownDim n => Proxy# n -> r)---instance Eq SomeIntNat where-  SomeIntNat x == SomeIntNat y = intNatVal x == intNatVal y--instance Ord SomeIntNat where-  compare (SomeIntNat x) (SomeIntNat y) = compare (intNatVal x) (intNatVal y)--instance Show SomeIntNat where-  showsPrec p (SomeIntNat x) = showsPrec p (intNatVal x)--instance Read SomeIntNat where-  readsPrec p xs = do (a,ys) <- readsPrec p xs-                      case someIntNatVal a of-                        Nothing -> []-                        Just n  -> [(n,ys)]----- | Bring an instance of certain class or constaint satisfaction evidence into scope.-data Evidence :: Constraint -> Type where-    Evidence :: a => Evidence a--sumEvs :: Evidence a -> Evidence b -> Evidence (a,b)-sumEvs Evidence Evidence = Evidence-{-# INLINE sumEvs #-}--infixl 4 +!+-(+!+) :: Evidence a -> Evidence b -> Evidence (a,b)-(+!+) = sumEvs-{-# INLINE (+!+) #-}---withEvidence :: Evidence a -> (a => r) -> r-withEvidence d r = case d of Evidence -> r-{-# INLINE withEvidence #-}--mkKDEv :: forall (m :: Nat) (n :: Nat) . KnownDim n => Proxy# n -> Evidence (KnownDim m)-mkKDEv _ = unsafeCoerce $ Evidence @(KnownDim n)-{-# INLINE mkKDEv #-}--inferPlusKnownDim :: forall n m . (KnownDim n, KnownDim m) => Evidence (KnownDim (n + m))-inferPlusKnownDim = reifyDim (dimVal' @n + dimVal' @m) (mkKDEv @(n + m))-{-# INLINE inferPlusKnownDim #-}--inferMinusKnownDim :: forall n m . (KnownDim n, KnownDim m, m <= n) => Evidence (KnownDim (n - m))-inferMinusKnownDim = reifyDim (dimVal' @n - dimVal' @m) (mkKDEv @(n - m))-{-# INLINE inferMinusKnownDim #-}--inferMinusKnownDimM :: forall n m . (KnownDim n, KnownDim m) => Maybe (Evidence (KnownDim (n - m)))-inferMinusKnownDimM = if v >= 0 then Just $ reifyDim v (mkKDEv @(n - m))-                                else Nothing-  where-    v = dimVal' @n - dimVal' @m-{-# INLINE inferMinusKnownDimM #-}--inferTimesKnownDim :: forall n m . (KnownDim n, KnownDim m) => Evidence (KnownDim (n * m))-inferTimesKnownDim = reifyDim (dimVal' @n * dimVal' @m) (mkKDEv @(n * m))-{-# INLINE inferTimesKnownDim #-}

@@ -0,0 +1,343 @@+{-# LANGUAGE AllowAmbiguousTypes    #-}+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE KindSignatures         #-}+{-# LANGUAGE MagicHash              #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE PatternSynonyms        #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE Rank2Types             #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE ViewPatterns           #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.TypedList+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Maintainer  :  chirkin@arch.ethz.ch+--+--+-- Provide a type-indexed heterogeneous list type @TypedList@.+-- Behind the facade, @TypedList@ is just a plain list of haskell pointers.+-- It is used to represent dimension lists, indices, and just flexible tuples.+--+-- Most of type-level functionality is implemented using GADT-like pattern synonyms.+-- Import this module qualified to use list-like functionality.+--+-----------------------------------------------------------------------------+module Numeric.TypedList+    ( TypedList (U, (:*), Empty, TypeList, EvList, Cons, Snoc, Reverse)+    , RepresentableList (..)+    , TypeList, types, order, order'+    , cons, snoc+    , Numeric.TypedList.reverse+    , Numeric.TypedList.take+    , Numeric.TypedList.drop+    , Numeric.TypedList.head+    , Numeric.TypedList.tail+    , Numeric.TypedList.last+    , Numeric.TypedList.init+    , Numeric.TypedList.splitAt+    , Numeric.TypedList.concat+    , Numeric.TypedList.length+    , Numeric.TypedList.map+    , module Numeric.Type.List+    ) where++import           Control.Arrow         (first)+import           Data.Proxy+import           GHC.Base              (Type)+import           GHC.Exts++import           Numeric.Dim+import           Numeric.Type.Evidence+import           Numeric.Type.List+++-- | Type-indexed list+newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any]+++-- Starting from GHC 8.2, compiler supports specifying lists of complete+-- pattern synonyms.+#if __GLASGOW_HASKELL__ >= 802+{-# COMPLETE TypeList #-}+{-# COMPLETE EvList #-}+{-# COMPLETE U, (:*) #-}+{-# COMPLETE U, Cons #-}+{-# COMPLETE U, Snoc #-}+{-# COMPLETE Empty, (:*) #-}+{-# COMPLETE Empty, Cons #-}+{-# COMPLETE Empty, Snoc #-}+{-# COMPLETE Reverse #-}+#endif++-- | A list of type proxies+type TypeList (xs :: [k]) = TypedList Proxy xs+++-- | A list of evidence for constraints+type EvidenceList (c :: k -> Constraint) (xs :: [k])+  = TypedList (Evidence' c) xs+++-- | Pattern matching against this causes `RepresentableList` instance+--   come into scope.+--   Also it allows constructing a term-level list out of a constraint.+pattern TypeList :: forall (xs :: [k])+                  . () => RepresentableList xs => TypeList xs+pattern TypeList <- (mkRTL -> E)+  where+    TypeList = tList @k @xs++-- | Pattern matching against this allows manipulating lists of constraints.+--   Useful when creating functions that change the shape of dimensions.+pattern EvList :: forall (c :: k -> Constraint) (xs :: [k])+                . () => (All c xs, RepresentableList xs) => EvidenceList c xs+pattern EvList <- (mkEVL -> E)+  where+    EvList = _evList (tList @k @xs)++-- | Zero-length type list+pattern U :: forall (f :: k -> Type) (xs :: [k])+           . () => (xs ~ '[]) => TypedList f xs+pattern U <- (patTL @f @xs -> PatCNil)+  where+    U = unsafeCoerce# []++-- | Zero-length type list; synonym to `U`.+pattern Empty :: forall (f :: k -> Type) (xs :: [k])+               . () => (xs ~ '[]) => TypedList f xs+pattern Empty = U++-- | Constructing a type-indexed list+pattern (:*) :: forall (f :: k -> Type) (xs :: [k])+              . ()+             => forall (y :: k) (ys :: [k])+              . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs+pattern (:*) x xs = Cons x xs+infixr 5 :*++-- | Constructing a type-indexed list in the canonical way+pattern Cons :: forall (f :: k -> Type) (xs :: [k])+              . ()+             => forall (y :: k) (ys :: [k])+              . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs+pattern Cons x xs <- (patTL @f @xs -> PatCons x xs)+  where+    Cons = Numeric.TypedList.cons++-- | Constructing a type-indexed list from the other end+pattern Snoc :: forall (f :: k -> Type) (xs :: [k])+              . ()+             => forall (sy :: [k]) (y :: k)+              . (xs ~ (sy +: y)) => TypedList f sy -> f y -> TypedList f xs+pattern Snoc sx x <- (unsnocTL @f @xs -> PatSnoc sx x)+  where+    Snoc = Numeric.TypedList.snoc++-- | Reverse a typed list+pattern Reverse :: forall (f :: k -> Type) (xs :: [k])+                 . ()+                => forall (sx :: [k])+                 . (xs ~ Reverse sx, sx ~ Reverse xs)+                => TypedList f sx -> TypedList f xs+pattern Reverse sx <- (unreverseTL @f @xs -> PatReverse sx)+  where+    Reverse = Numeric.TypedList.reverse++cons :: f x -> TypedList f xs -> TypedList f (x :+ xs)+cons x xs = TypedList (unsafeCoerce# x : unsafeCoerce# xs)+{-# INLINE cons #-}++snoc :: TypedList f xs -> f x -> TypedList f (xs +: x)+snoc xs x = TypedList (unsafeCoerce# xs ++ [unsafeCoerce# x])+{-# INLINE snoc #-}++reverse :: TypedList f xs -> TypedList f (Reverse xs)+reverse (TypedList sx) = unsafeCoerce# (Prelude.reverse sx)+{-# INLINE reverse #-}++take :: Dim n -> TypedList f xs -> TypedList f (Take n xs)+take d (TypedList xs) = unsafeCoerce# (Prelude.take (intD d) xs)+{-# INLINE take #-}++drop :: Dim n -> TypedList f xs -> TypedList f (Drop n xs)+drop d (TypedList xs) = unsafeCoerce# (Prelude.drop (intD d) xs)+{-# INLINE drop #-}++head :: TypedList f xs -> f (Head xs)+head (TypedList xs) = unsafeCoerce# (Prelude.head xs)+{-# INLINE head #-}++tail :: TypedList f xs -> TypedList f (Tail xs)+tail (TypedList xs) = unsafeCoerce# (Prelude.tail xs)+{-# INLINE tail #-}++init :: TypedList f xs -> TypedList f (Init xs)+init (TypedList xs) = unsafeCoerce# (Prelude.init xs)+{-# INLINE init #-}++last :: TypedList f xs -> f (Last xs)+last (TypedList xs) = unsafeCoerce# (Prelude.last xs)+{-# INLINE last #-}++length :: TypedList f xs -> Dim (Length xs)+length = order+{-# INLINE length #-}++splitAt :: Dim n+        -> TypedList f xs+        -> (TypedList f (Take n xs), TypedList f (Drop n xs))+splitAt d (TypedList xs) = unsafeCoerce# (Prelude.splitAt (intD d) xs)+{-# INLINE splitAt #-}++concat :: TypedList f xs+       -> TypedList f ys+       -> TypedList f (xs ++ ys)+concat (TypedList xs) (TypedList ys) = unsafeCoerce# (xs ++ ys)+{-# INLINE concat #-}++-- | Map a function over contents of a typed list+map :: (forall a . f a -> g a)+    -> TypedList f xs+    -> TypedList g xs+map k (TypedList xs) = unsafeCoerce# (Prelude.map k' xs)+  where+    k' :: Any -> Any+    k' = unsafeCoerce# . k . unsafeCoerce#+{-# INLINE map #-}++-- | Get a constructible `TypeList` from any other `TypedList`;+--   Pattern matching agains the result brings `RepresentableList` constraint+--   into the scope:+--+--   > case types ts of TypeList -> ...+--+types :: TypedList f xs -> TypeList xs+types (TypedList xs) = unsafeCoerce# (Prelude.map (const Proxy) xs)+{-# INLINE types #-}++-- | Representable type lists.+--   Allows getting type information about list structure at runtime.+class RepresentableList (xs :: [k]) where+  -- | Get type-level constructed list+  tList :: TypeList xs++instance RepresentableList ('[] :: [k]) where+  tList = U++instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where+  tList = Proxy @x :* tList @k @xs+++order' :: forall xs . RepresentableList xs => Dim (Length xs)+order' = order (tList @_ @xs)+{-# INLINE order' #-}++order :: TypedList f xs -> Dim (Length xs)+order (TypedList xs) = unsafeCoerce# (fromIntegral (Prelude.length xs) :: Word)+{-# INLINE order #-}+++++--------------------------------------------------------------------------------+-- internal+--------------------------------------------------------------------------------+++-- | This function does GHC's magic to convert user-supplied `tList` function+--   to create an instance of `RepresentableList` typeclass at runtime.+--   The trick is taken from Edward Kmett's reflection library explained+--   in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection+reifyRepList :: forall xs r+              . TypeList xs+             -> (RepresentableList xs => r)+             -> r+reifyRepList tl k = unsafeCoerce# (MagicRepList k :: MagicRepList xs r) tl+{-# INLINE reifyRepList #-}+newtype MagicRepList xs r = MagicRepList (RepresentableList xs => r)++data PatReverse f xs+  = forall (sx :: [k]) . (xs ~ Reverse sx, sx ~ Reverse xs)+  => PatReverse (TypedList f sx)++unreverseTL :: forall f xs . TypedList f xs -> PatReverse f xs+unreverseTL (TypedList xs)+  = case (unsafeCoerce# (E @(xs ~ xs, xs ~ xs))+           :: Evidence (xs ~ Reverse sx, sx ~ Reverse xs)+         ) of+      E -> PatReverse (unsafeCoerce# (Prelude.reverse xs))+{-# INLINE unreverseTL #-}+++mkRTL :: forall (xs :: [k])+       . TypeList xs+      -> Evidence (RepresentableList xs)+mkRTL xs = reifyRepList xs E+{-# INLINE mkRTL #-}+++data PatSnoc f xs where+  PatSNil :: PatSnoc f '[]+  PatSnoc :: TypedList f ys -> f y -> PatSnoc f (ys +: y)++unsnocTL :: forall f xs . TypedList f xs -> PatSnoc f xs+unsnocTL (TypedList [])+  = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ '[])) of+      E -> PatSNil+unsnocTL (TypedList (x:xs))+  = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ (Init xs +: Last xs))) of+      E -> PatSnoc (unsafeCoerce# sy) (unsafeCoerce# y)+  where+    (sy, y) = unsnoc x xs+    unsnoc t []     = ([], t)+    unsnoc t (z:zs) = first (t:) (unsnoc z zs)+{-# INLINE unsnocTL #-}+++data PatCons f xs where+  PatCNil :: PatCons f '[]+  PatCons :: f y -> TypedList f ys -> PatCons f (y ': ys)++patTL :: forall f xs . TypedList f xs -> PatCons f xs+patTL (TypedList [])+  = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ '[])) of+      E -> PatCNil+patTL (TypedList (x : xs))+  = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ (Head xs ': Tail xs))) of+      E -> PatCons (unsafeCoerce# x) (unsafeCoerce# xs)+{-# INLINE patTL #-}++intD :: Dim n -> Int+intD = (fromIntegral :: Word -> Int) . unsafeCoerce#+++mkEVL :: forall (c :: k -> Constraint) (xs :: [k])+       . EvidenceList c xs -> Evidence (All c xs, RepresentableList xs)+mkEVL U = E+mkEVL (E' :* evs) = case mkEVL evs of E -> E+#if __GLASGOW_HASKELL__ >= 802+#else+mkEVL _ = error "EvList/mkEVL: impossible argument"+#endif+++_evList :: forall (c :: k -> Constraint) (xs :: [k])+        . All c xs => TypeList xs -> EvidenceList c xs+_evList U = U+_evList (_ :* xs) = case _evList xs of evs -> E' :* evs+#if __GLASGOW_HASKELL__ >= 802+#else+_evList _ = error "EvList/_evList: impossible argument"+#endif

@@ -0,0 +1,86 @@+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE ExplicitNamespaces        #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE KindSignatures            #-}+{-# LANGUAGE PolyKinds                 #-}+{-# LANGUAGE Rank2Types                #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TemplateHaskell           #-}+{-# LANGUAGE TypeApplications          #-}+{-# LANGUAGE TypeOperators             #-}++-- | Some GHC versions show incorrect warnings here:+--+--   GHC 8.2 says "Pattern match has inaccessible right hand side"+--    if our GADT-like patterns are matched nested:+--    https://ghc.haskell.org/trac/ghc/ticket/14253+--+--   GHC 8.0 says "Pattern match(es) are non-exhaustive"+--    because it does not support COMPLETE pragmas yet.+--+module Numeric.DimTest (runTests) where++import           Test.QuickCheck       (quickCheckAll)++import           Numeric.Dim+import           Numeric.Type.Evidence+++-- | Try inference of type-level natural values via term-level binary functions.+testBinaryOp :: forall (a :: Nat) (b :: Nat) (c :: Nat)+              . (Word -> Word -> Word)+             -> (Dim a -> Dim b -> Dim c)+             -> Dim a -> Dim b -> Bool+testBinaryOp fTerm fType da db+  | a <- dimVal da+  , b <- dimVal db+  , Dx dr <- someDimVal (fTerm a b)+      -- pattern-match against @SomeDim@ to extract a type-level natural Dim.+  , True  <- fTerm a b == dimVal (fType da db)+      -- compare the term-level function and the type-level function results+      -- as regular word values.+  , Just E <- sameDim dr (fType da db)+      -- now the type system knows that @c ~ fType a b@ and+      -- we can use ordinary equality function (which is @const True@).+  = dr == fType da db+testBinaryOp _ _ _ _ = False++++prop_plusDim :: Word -> Word -> Bool+prop_plusDim a b = case (someDimVal a, someDimVal b) of+  (Dx da, Dx db) -> testBinaryOp (+) plusDim da db+++prop_timesDim :: Word -> Word -> Bool+prop_timesDim a b = case (someDimVal a, someDimVal b) of+  (Dx da, Dx db) -> testBinaryOp (*) timesDim da db+++prop_powerDim :: Word -> Word -> Bool+prop_powerDim a b = case ( someDimVal a+                         , someDimVal b+                         ) of+  (Dx da, Dx db) -> testBinaryOp (^) powerDim da db++prop_minusDim :: Word -> Word -> Bool+prop_minusDim a' b'+  | a <- max a' b'+  , b <- min a' b'+  , xda <- someDimVal a -- this is an unknown (Dim (XN 0))+  , Dx db <- someDimVal b+  , Just (Dx da) <- constrainBy db xda -- here da >= db+  = a - b == dimVal (minusDim da db)+prop_minusDim _ _ = False+++++++return []+runTests :: IO Bool+runTests = $quickCheckAll

@@ -0,0 +1,67 @@+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE ExplicitNamespaces        #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE KindSignatures            #-}+{-# LANGUAGE PolyKinds                 #-}+{-# LANGUAGE Rank2Types                #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TemplateHaskell           #-}+{-# LANGUAGE TypeApplications          #-}+{-# LANGUAGE TypeOperators             #-}++++module Numeric.Dimensions.DimsTest (runTests) where++import           Test.QuickCheck         (quickCheckAll)++import           Numeric.Dim+import           Numeric.Dimensions.Dims+import qualified Numeric.TypedList as TL+++-- | Matching against @Reverse@ pattern lets GHC know the reversion relation+--   at the type level.+--   That means the type system knows that reverse of reverse is the same list!+prop_reverseDims :: [Word] -> Bool+prop_reverseDims xs+  | SomeDims ds <- someDimsVal xs+  = case ds of+      Reverse rds -> case rds of+        Reverse rrds -> ds == rrds+++prop_concatDims :: [Word] -> [Word] -> Bool+prop_concatDims xs ys+  | SomeDims dxs <- someDimsVal xs+  , SomeDims dys <- someDimsVal ys+  = case TL.concat dxs dys of+      dxsys -> listDims dxsys == xs ++ ys+++-- | TODO: bring more evidence about list equality+prop_splitDims :: Word -> [Word] -> Bool+prop_splitDims n xsys+  | SomeDims dxsys <- someDimsVal xsys+  , Dx dn <- someDimVal n -- TODO: why this causes non-exhaustive patterns in GHC 8.2?+  , (xs, ys) <- splitAt (fromIntegral n) xsys+  = case TL.splitAt dn dxsys of+      (dxs, dys) -> and+        [ listDims dxs == xs+        , listDims dys == ys+        -- , dxsys == TL.concat dxs dys+        ]+++++++++return []+runTests :: IO Bool+runTests = $quickCheckAll

@@ -1,124 +0,0 @@-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces        #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TemplateHaskell           #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeOperators             #-}-{-# LANGUAGE UndecidableInstances      #-}-{-# LANGUAGE MagicHash                 #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.ListTest--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Testing type-level Lists and the inference plugin------------------------------------------------------------------------------------module Numeric.Dimensions.ListTest (runTests) where--import           Test.QuickCheck    (quickCheckAll)--import           Numeric.TypeLits-import           Numeric.Dimensions---- * Test simple binary nat ops--natSum :: Dim a -> Dim b -> Proxy (a+b)-natSum _ _ = Proxy-natMul :: Dim a -> Dim b -> Proxy (a*b)-natMul _ _ = Proxy-natRem :: Dim a -> Dim b -> Proxy (a-b)-natRem _ _ = Proxy-natSucc :: Dim a -> Proxy (a + 1)-natSucc _ = Proxy-natPred :: Dim a -> Proxy (a - 1)-natPred _ = Proxy--prop_KnownNats :: Int -> Int -> Bool-prop_KnownNats a b-  | x <- max (abs a) (abs b)-  , y <- min (abs a) (abs b)-  , z <- y `mod` 50-  , Just (SomeDim (px@Dn :: Dim x)) <- someDimVal x-  , Just (SomeDim (py@Dn :: Dim y)) <- someDimVal y-  , Just (SomeDim (px1@Dn :: Dim x1)) <- someDimVal (x+1)-  , Just (SomeDim (Dn :: Dim z)) <- someDimVal z-  , Just Evidence <- (\e1 e2 e3 -> e1 `sumEvs` e2 `sumEvs` e3)-        <$> inferMinusKnownDimM @x @y-        <*> inferMinusKnownDimM @x1 @1-        <*> Just ( inferPlusKnownDim @x @y-          `sumEvs` inferTimesKnownDim @x @y-          `sumEvs` inferPlusKnownDim @y @1-         )-  = and-    [ x + y == intNatVal (natSum px py)-    , x * y == intNatVal (natMul px py)-    , x - y == intNatVal (natRem px py)-    , x == intNatVal (natPred px1)-    , y + 1 == intNatVal (natSucc py)-    ]-prop_KnownNats _ _ = True------ * Test props on a single type-level list--prop_FiniteList :: Int -> [Int] -> Bool-prop_FiniteList a xs'-  | n <- (abs a)-  , xs <- (2+) . abs <$> xs'-  , Just (SomeDim (Dn :: Dim n)) <- someDimVal n-  , Just (SomeDims (pxs :: Dim xs)) <- someDimsVal xs-  , Evidence <- reifyDimensions pxs-  , Evidence <- inferDimFiniteList @xs-  = and [ order @_ @xs == length xs-        , case inferTakeNFiniteList @n @xs of-            Evidence -> order @_ @(Take n xs) == length (take n xs)-        , case inferDropNFiniteList @n @xs of-            Evidence -> order @_ @(Drop n xs) == length (drop n xs)-        , case inferReverseFiniteList @xs of-            Evidence -> order @_ @(Reverse xs) == length (reverse xs)-        ]-prop_FiniteList _ _ = False------- * Inference properties--prop_ListInference :: [Int] -> [Int] -> Bool-prop_ListInference xs' ys'-  | xs <- (2+) . abs <$> xs'-  , ys <- (2+) . abs <$> ys'-  , Just (SomeDims (dxs :: Dim xs)) <- someDimsVal xs-  , Just (SomeDims (dys :: Dim ys)) <- someDimsVal ys-  , Evidence <- reifyDimensions dxs-  , Evidence <- reifyDimensions dys-  , Evidence <- inferDimFiniteList @xs-       `sumEvs` inferDimFiniteList @ys-  = and [ case inferConcatFiniteList @xs @ys of-            Evidence -> order @_ @(xs ++ ys) == length xs + length ys-        , case inferConcat @xs @ys `sumEvs`-               inferConcatFiniteList @xs @ys of-            Evidence -> case inferPrefixFiniteList @ys @(xs ++ ys) of-              Evidence -> order @_ @(Prefix ys (xs ++ ys)) == length xs-        , case inferConcat @xs @ys `sumEvs`-               inferConcatFiniteList @xs @ys of-            Evidence -> case inferSuffixFiniteList @xs @(xs ++ ys) of-              Evidence -> order @_ @(Suffix xs (xs ++ ys)) == length ys-        ]-prop_ListInference _ _ = False--return []-runTests :: IO Bool-runTests = $quickCheckAll

@@ -3,13 +3,15 @@ import           System.Exit import           Distribution.TestSuite -import qualified Numeric.Dimensions.ListTest+import qualified Numeric.DimTest+import qualified Numeric.Dimensions.DimsTest   -- | Collection of tests in detailed-0.9 format tests :: IO [Test] tests = return-  [ test "Dimensions.List"    Numeric.Dimensions.ListTest.runTests+  [ test "Dim"    Numeric.DimTest.runTests+  , test "Dims"   Numeric.Dimensions.DimsTest.runTests   ]