dimensions (empty) → 0.1.0.0
raw patch · 14 files changed
+2304/−0 lines, 14 filesdep +Cabaldep +QuickCheckdep +basesetup-changed
Dependencies added: Cabal, QuickCheck, base, dimensions, ghc-prim
Files
- LICENSE +24/−0
- Setup.hs +2/−0
- dimensions.cabal +55/−0
- src/Numeric/Dimensions.hs +28/−0
- src/Numeric/Dimensions/Dim.hs +585/−0
- src/Numeric/Dimensions/Idx.hs +209/−0
- src/Numeric/Dimensions/List.hs +436/−0
- src/Numeric/Dimensions/Traverse.hs +289/−0
- src/Numeric/Dimensions/Traverse/IO.hs +113/−0
- src/Numeric/Dimensions/Traverse/ST.hs +113/−0
- src/Numeric/Dimensions/XDim.hs +110/−0
- src/Numeric/TypeLits.hs +192/−0
- test/Numeric/Dimensions/ListTest.hs +124/−0
- test/Spec.hs +24/−0
+ LICENSE view
@@ -0,0 +1,24 @@+Copyright (c) 2017, Artem M. Chirkin+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:+ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+ * Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+ * Neither the name of the copyright holder nor the+ names of its contributors may be used to endorse or promote products+ derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL COPYRIGHT HOLDER BE LIABLE FOR ANY+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ dimensions.cabal view
@@ -0,0 +1,55 @@+name: dimensions+version: 0.1.0.0+cabal-version: >=1.20+build-type: Simple+license: BSD3+license-file: LICENSE+copyright: (c) Artem Chirkin+maintainer: chirkin@arch.ethz.ch+homepage: https://github.com/achirkin/easytensor#readme+synopsis: Safe type-level dimensionality for multidimensional data+description:+ Safe type-level dimensionality for multidimensional data.+category: Math, Geometry+author: Artem Chirkin++source-repository head+ type: git+ location: https://github.com/achirkin/easytensor.git+ subdir: dimensions+++library++ exposed-modules:+ 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+ build-depends:+ base >=4.9 && <5,+ ghc-prim >= 0.5+ default-language: Haskell2010+ hs-source-dirs: src+ ghc-options: -Wall -fwarn-tabs -O2+++test-suite dimensions-test++ type: detailed-0.9+ test-module: Spec+ other-modules:+ Numeric.Dimensions.ListTest+ build-depends:+ base -any,+ Cabal >=1.20,+ QuickCheck -any,+ dimensions -any+ default-language: Haskell2010+ hs-source-dirs: test+ ghc-options: -Wall -fwarn-tabs -O2
+ src/Numeric/Dimensions.hs view
@@ -0,0 +1,28 @@+-----------------------------------------------------------------------------+-- |+-- Module : Numeric.Dimensions+-- Copyright : (c) Artem Chirkin+-- License : BSD3+--+-- 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.+--+-- 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+ ( module Numeric.Dimensions.List+ , module Numeric.Dimensions.Dim+ , module Numeric.Dimensions.Idx+ , Evidence (..), withEvidence, sumEvs, (+!+)+ ) where++import Numeric.Dimensions.List+import Numeric.Dimensions.Dim+import Numeric.Dimensions.Idx+import Numeric.TypeLits
+ src/Numeric/Dimensions/Dim.hs view
@@ -0,0 +1,585 @@+{-# 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 is 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 is 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 #-}
+ src/Numeric/Dimensions/Idx.hs view
@@ -0,0 +1,209 @@+{-# 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 #-}
+ src/Numeric/Dimensions/List.hs view
@@ -0,0 +1,436 @@+{-# 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
+ src/Numeric/Dimensions/Traverse.hs view
@@ -0,0 +1,289 @@+{-# 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'
+ src/Numeric/Dimensions/Traverse/IO.hs view
@@ -0,0 +1,113 @@+{-# 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 #-}
+ src/Numeric/Dimensions/Traverse/ST.hs view
@@ -0,0 +1,113 @@+{-# 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 #-}
+ src/Numeric/Dimensions/XDim.hs view
@@ -0,0 +1,110 @@+{-# 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 :: FixedXDim xds ds ~ xds => Dim ds -> Dim xds+++instance XDimensions '[] where+ wrapDim D = D+ {-# INLINE wrapDim #-}++instance XDimensions xs => XDimensions (XN m ': xs) where+ wrapDim ((d@Dn :: Dim d) :* ds)+ | Evidence <- unsafeEqEvidence @(m <=? d) @'True+ = Dx d :* wrapDim ds++instance XDimensions xs => XDimensions (N n ': xs) where+ wrapDim ((Dn :: Dim d) :* ds)+ | Evidence <- unsafeEqEvidence @n @d+ = Dn @d :* wrapDim ds+++-- | Loose compile-time information about dimensionalities+xdim :: forall (ds :: [Nat]) (xds :: [XNat])+ . ( Dimensions ds+ , XDimensions xds+ , FixedXDim xds ds ~ xds) => 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 #-}
+ src/Numeric/TypeLits.hs view
@@ -0,0 +1,192 @@+{-# 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 #-}
+ test/Numeric/Dimensions/ListTest.hs view
@@ -0,0 +1,124 @@+{-# 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
+ test/Spec.hs view
@@ -0,0 +1,24 @@+module Spec (tests) where++import Distribution.TestSuite++import qualified Numeric.Dimensions.ListTest++tests :: IO [Test]+tests = return+ [ test "Dimensions.List" Numeric.Dimensions.ListTest.runTests+ ]+++test :: String -> IO Bool -> Test+test tName propOp = Test testI+ where+ testI = TestInstance+ { run = fromBool <$> propOp+ , name = tName+ , tags = []+ , options = []+ , setOption = \_ _ -> Right testI+ }+ fromBool False = Finished (Fail "Property does not hold!")+ fromBool True = Finished Pass