diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/dimensions.cabal b/dimensions.cabal new file mode 100644 --- /dev/null +++ b/dimensions.cabal @@ -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 diff --git a/src/Numeric/Dimensions.hs b/src/Numeric/Dimensions.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions.hs @@ -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 diff --git a/src/Numeric/Dimensions/Dim.hs b/src/Numeric/Dimensions/Dim.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Dim.hs @@ -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 #-} diff --git a/src/Numeric/Dimensions/Idx.hs b/src/Numeric/Dimensions/Idx.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Idx.hs @@ -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 #-} diff --git a/src/Numeric/Dimensions/List.hs b/src/Numeric/Dimensions/List.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/List.hs @@ -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 +-- 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 diff --git a/src/Numeric/Dimensions/Traverse.hs b/src/Numeric/Dimensions/Traverse.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Traverse.hs @@ -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' diff --git a/src/Numeric/Dimensions/Traverse/IO.hs b/src/Numeric/Dimensions/Traverse/IO.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Traverse/IO.hs @@ -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 #-} diff --git a/src/Numeric/Dimensions/Traverse/ST.hs b/src/Numeric/Dimensions/Traverse/ST.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Traverse/ST.hs @@ -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 #-} diff --git a/src/Numeric/Dimensions/XDim.hs b/src/Numeric/Dimensions/XDim.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/XDim.hs @@ -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 #-} diff --git a/src/Numeric/TypeLits.hs b/src/Numeric/TypeLits.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/TypeLits.hs @@ -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 #-} diff --git a/test/Numeric/Dimensions/ListTest.hs b/test/Numeric/Dimensions/ListTest.hs new file mode 100644 --- /dev/null +++ b/test/Numeric/Dimensions/ListTest.hs @@ -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 diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -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