module Data.Tensor.Type where
import Data.List (foldl')
import Data.Proxy
import Data.Singletons
import Data.Singletons.Prelude.List
import GHC.TypeLits
import Unsafe.Coerce
type Shape = [Int]
type Index = [Int]
toNat :: KnownNat s => Proxy s -> Int
toNat = unsafeCoerce . natVal
natsVal :: forall proxy (s::[Nat]). SingI s => proxy s -> Index
natsVal _ = case (sing :: Sing s) of
SNil -> []
(SCons x xs) -> unsafeCoerce <$> (fromSing x: fromSing xs)
viToti :: Index -> Int -> Index
viToti s i = snd $ foldl' go (i,[]) (reverse s)
where
{-# INLINE go #-}
go (i',x) n = let (d,r) = divMod i' n in (d,r:x)
tiTovi :: Index -> Index -> Int
tiTovi = go 0
where
{-# INLINE go #-}
go i (n:ns) (ind:inds) = go (i * n + ind) ns inds
go i _ _ = i
mult :: (Eq a, Num a) => a -> a -> a
mult a b = case a of
0 -> 0
c -> c * b
i0 = Proxy :: Proxy 0
i1 = Proxy :: Proxy 1
i2 = Proxy :: Proxy 2
i3 = Proxy :: Proxy 3
i4 = Proxy :: Proxy 4
i5 = Proxy :: Proxy 5
i6 = Proxy :: Proxy 6
i7 = Proxy :: Proxy 7
i8 = Proxy :: Proxy 8
i9 = Proxy :: Proxy 9