module TypeUnary.Vec
(
Z, S, (:+:)
, N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16
, Nat(..), zero, one, two, three, four
, withIsNat, natSucc, natIsNat
, natToZ, natEq, natAdd, (:<:)
, Index(..), succI, index0, index1, index2, index3
, Vec(..), IsNat(..), (<+>), indices
, Vec0,Vec1,Vec2,Vec3,Vec4,Vec5,Vec6,Vec7,Vec8,Vec9
, Vec10,Vec11,Vec12,Vec13,Vec14,Vec15,Vec16
, vec1, vec2, vec3, vec4
, un1, un2, un3, un4
, get0, get1, get2, get3
, get, swizzle, split
, ToVec(..)
) where
import Prelude hiding (foldr,sum)
import Control.Applicative (Applicative(..),liftA2,(<$>))
import Data.Foldable (Foldable(..),toList,sum)
import Data.Traversable (Traversable(..))
import Data.Maybe (isJust)
import Foreign.Storable
import Foreign.Ptr (Ptr,plusPtr,castPtr)
import Data.VectorSpace
import Data.Proof.EQ
data Z
data S n
infixl 6 :+:
type family a :+: b
type instance Z :+: b = b
type instance S a :+: b = S (a :+: b)
type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
type N9 = S N8
type N10 = S N9
type N11 = S N10
type N12 = S N11
type N13 = S N12
type N14 = S N13
type N15 = S N14
type N16 = S N15
data Nat :: * -> * where
Zero :: Nat Z
Succ :: IsNat n => Nat n -> Nat (S n)
instance Show (Nat n) where show = show . natToZ
withIsNat :: (IsNat n => Nat n -> a) -> (Nat n -> a)
withIsNat p Zero = p Zero
withIsNat p (Succ n) = p (Succ n)
natSucc :: Nat n -> Nat (S n)
natSucc = withIsNat Succ
natIsNat :: Nat n -> (IsNat n => Nat n)
natIsNat Zero = Zero
natIsNat (Succ n) = Succ n
natToZ :: Nat n -> Integer
natToZ Zero = 0
natToZ (Succ n) = (succ . natToZ) n
natEq :: Nat m -> Nat n -> Maybe (m :=: n)
Zero `natEq` Zero = Just Refl
Succ m `natEq` Succ n = liftEq <$> (m `natEq` n)
_ `natEq` _ = Nothing
natAdd :: Nat m -> Nat n -> Nat (m :+: n)
Zero `natAdd` n = n
Succ m `natAdd` n = natSucc (m `natAdd` n)
zero :: Nat N0
zero = Zero
one :: Nat N1
one = Succ zero
two :: Nat N2
two = Succ one
three :: Nat N3
three = Succ two
four :: Nat N4
four = Succ three
infix 4 :<:
data m :<: n where
ZLess :: Z :<: S n
SLess :: m :<: n -> S m :<: S n
data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n)
instance Eq (Index lim) where
Index _ n == Index _ n' = isJust (n `natEq` n')
succI :: Index m -> Index (S m)
succI (Index p n) = Index (SLess p) (Succ n)
index0 :: Index (S m)
index0 = Index ZLess Zero
index1 :: Index (S (S m))
index1 = succI index0
index2 :: Index (S (S (S m)))
index2 = succI index1
index3 :: Index (S (S (S (S m))))
index3 = succI index2
infixr 5 :<
data Vec :: * -> * -> * where
ZVec :: Vec Z a
(:<) :: a -> Vec n a -> Vec (S n) a
instance Eq a => Eq (Vec n a) where
ZVec == ZVec = True
a :< as == b :< bs = a==b && as==bs
instance Ord a => Ord (Vec n a) where
ZVec `compare` ZVec = EQ
(a :< as) `compare` (b :< bs) =
case a `compare` b of
LT -> LT
GT -> GT
EQ -> as `compare` bs
instance Show a => Show (Vec n a) where
show v = "elemsV " ++ show (toList v)
instance Functor (Vec n) where
fmap _ ZVec = ZVec
fmap f (a :< u) = f a :< fmap f u
instance IsNat n => Applicative (Vec n) where
pure = pureV
(<*>) = applyV
applyV :: Vec n (a -> b) -> Vec n a -> Vec n b
ZVec `applyV` ZVec = ZVec
(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)
instance Foldable (Vec n) where
foldr _ b ZVec = b
foldr h b (a :< as) = a `h` foldr h b as
instance Traversable (Vec n) where
traverse _ ZVec = pure ZVec
traverse f (a :< as) = liftA2 (:<) (f a) (traverse f as)
instance (IsNat n, Num a) => AdditiveGroup (Vec n a) where
{ zeroV = pure 0; (^+^) = liftA2 (+) ; negateV = fmap negate }
instance (IsNat n, Num a) => VectorSpace (Vec n a) where
type Scalar (Vec n a) = Vec1 a
(*^) (s :< ZVec) = fmap (s *)
instance (IsNat n, Num a) => InnerSpace (Vec n a) where
(<.>) = (result.result) (vec1 . sum) (liftA2 (*))
instance (IsNat n, Storable a) => Storable (Vec n a) where
sizeOf = const (fromIntegral (natToZ (nat :: Nat n))
* sizeOf (undefined :: a))
alignment = const (alignment (undefined :: a))
peek = peekV . castPtr
poke = pokeV . castPtr
instance IsNat Z where
nat = Zero
pureV _ = ZVec
elemsV [] = ZVec
elemsV (_:_) = error "elemsV: too many elements"
peekV = const (return ZVec)
pokeV = const (const (return ()))
instance IsNat n => IsNat (S n) where
nat = Succ nat
pureV a = a :< pureV a
elemsV [] = error "elemsV: too few elements"
elemsV (a : as) = a :< elemsV as
peekV p = do a <- peek p
as <- peekV (p `plusPtr` sizeOf a)
return (a :< as)
pokeV p (a :< as) = do poke p a
pokeV (p `plusPtr` sizeOf a) as
infixl 1 <+>
(<+>) :: Vec m a -> Vec n a -> Vec (m :+: n) a
ZVec <+> v = v
(a :< u) <+> v = a :< (u <+> v)
indices :: Nat n -> Vec n (Index n)
indices Zero = ZVec
indices (Succ n) = index0 :< fmap succI (indices n)
class IsNat n where
nat :: Nat n
pureV :: a -> Vec n a
elemsV :: [a] -> Vec n a
peekV :: Storable a => Ptr a -> IO (Vec n a)
pokeV :: Storable a => Ptr a -> Vec n a -> IO ()
type Vec0 = Vec N0
type Vec1 = Vec N1
type Vec2 = Vec N2
type Vec3 = Vec N3
type Vec4 = Vec N4
type Vec5 = Vec N5
type Vec6 = Vec N6
type Vec7 = Vec N7
type Vec8 = Vec N8
type Vec9 = Vec N9
type Vec10 = Vec N10
type Vec11 = Vec N11
type Vec12 = Vec N12
type Vec13 = Vec N13
type Vec14 = Vec N14
type Vec15 = Vec N15
type Vec16 = Vec N16
vec1 :: a -> Vec1 a
vec1 a = a :< ZVec
vec2 :: a -> a -> Vec2 a
vec2 a b = a :< vec1 b
vec3 :: a -> a -> a -> Vec3 a
vec3 a b c = a :< vec2 b c
vec4 :: a -> a -> a -> a -> Vec4 a
vec4 a b c d = a :< vec3 b c d
un1 :: Vec1 a -> a
un1 (a :< ZVec) = a
un2 :: Vec2 a -> (a,a)
un2 (a :< b :< ZVec) = (a,b)
un3 :: Vec3 a -> (a,a,a)
un3 (a :< b :< c :< ZVec) = (a,b,c)
un4 :: Vec4 a -> (a,a,a,a)
un4 (a :< b :< c :< d :< ZVec) = (a,b,c,d)
get :: Index n -> Vec n a -> Vec1 a
get (Index ZLess Zero ) (a :< _) = vec1 a
get (Index (SLess p) (Succ m)) (_ :< as) = get (Index p m) as
get0 :: Vec (S n) a -> Vec1 a
get1 :: Vec (S (S n)) a -> Vec1 a
get2 :: Vec (S (S (S n))) a -> Vec1 a
get3 :: Vec (S (S (S (S n)))) a -> Vec1 a
get0 = get index0
get1 = get index1
get2 = get index2
get3 = get index3
swizzle :: Vec n (Index m) -> Vec m a -> Vec n a
swizzle ZVec _ = ZVec
swizzle (ix :< ixs) v = un1 (get ix v) :< swizzle ixs v
split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a)
split = split' nat
split' :: Nat n -> Vec (n :+: m) a -> (Vec n a, Vec m a)
split' Zero v = (ZVec, v)
split' (Succ n) (a :< as) = (a :< bs, cs)
where
(bs,cs) = split' n as
class ToVec c n a | c -> n a where
toVec :: c -> Vec n a
instance ToVec (Vec n a) n a where toVec = id
result :: (b -> b') -> ((a -> b) -> (a -> b'))
result = (.)