type-unary 0.2.5 → 0.2.8

raw patch · 2 files changed

+39/−4 lines, 2 files

Files

• src/TypeUnary/Vec.hs +38/−3
• type-unary.cabal +1/−1

@@ -6,7 +6,8 @@            , RankNTypes            , MultiParamTypeClasses, FunctionalDependencies   #-}-{-# OPTIONS_GHC -Wall -fno-warn-incomplete-patterns #-}+{-# OPTIONS_GHC -Wall #-}+ ---------------------------------------------------------------------- -- | -- Module      :  TypeUnary.Vec@@ -23,7 +24,7 @@   (     module TypeUnary.Nat   -- * Vectors-  , Vec(..), headV, tailV, joinV, (<+>), indices, iota+  , Vec(..), unConsV, headV, tailV, joinV, (<+>), indices, iota   , Vec0,Vec1,Vec2,Vec3,Vec4,Vec5,Vec6,Vec7,Vec8,Vec9   , Vec10,Vec11,Vec12,Vec13,Vec14,Vec15,Vec16   , vec1, vec2, vec3, vec4, vec5, vec6, vec7, vec8@@ -32,7 +33,7 @@   , update   , set, set0, set1, set2, set3   , getI, setI-  , flattenV, swizzle, split, deleteV, elemsV+  , flattenV, chunkV, swizzle, split, deleteV, elemsV   , zipV , zipWithV , unzipV   , zipV3, zipWithV3, unzipV3   , transpose, cross@@ -70,6 +71,10 @@   ZVec :: Vec Z a    (:<) :: a -> Vec n a -> Vec (S n) a +-- | Type-safe un-cons for vectors+unConsV :: Vec (S n) a -> (a, Vec n a)+unConsV (a :< as) = (a,as)+ -- | Type-safe head for vectors headV :: Vec (S n) a -> a headV (a :< _) = a@@ -105,6 +110,12 @@  -} +cant :: String -> a+cant str = error $ str ++ ": GHC doesn't know this case can't happen."++cantV :: String -> a+cantV str = cant (str ++ " on Vec")+ {--------------------------------------------------------------------     Instances for standard classes --------------------------------------------------------------------}@@ -112,11 +123,13 @@ instance Eq a => Eq (Vec n a) where   ZVec    == ZVec    = True   a :< as == b :< bs = a==b && as==bs+  _ == _ = cantV "(==)"  instance Ord a => Ord (Vec n a) where   ZVec      `compare` ZVec      = EQ   (a :< as) `compare` (b :< bs) =     (a `compare` b) `mappend` (as `compare` bs)+  _ `compare` _ = cantV "compare"  -- Equivalently, -- @@ -168,6 +181,7 @@ 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)+_ `applyV` _ = cant "applyV"  -- Without -fno-warn-incomplete-patterns above, -- the previous two instances lead to warnings about non-exhaustive@@ -187,6 +201,7 @@ joinV :: Vec n (Vec n a) -> Vec n a joinV ZVec = ZVec joinV ((a :< _) :< vs) = a :< joinV (tailV <$> vs)+joinV _ = cant "joinV"  instance Foldable (Vec n) where   foldr _  b ZVec     = b@@ -203,6 +218,7 @@ instance (IsNat n, Num a) => VectorSpace (Vec n a) where   type Scalar (Vec n a) = Vec1 a   (*^) (s :< ZVec) = fmap (s *)+  (*^) _ = cantV "(*^)"  instance (IsNat n, Num a) => InnerSpace (Vec n a) where    -- u <.> v = vec1 (sum (liftA2 (*) u v))@@ -248,6 +264,7 @@ pokeV' Zero     _ ZVec      = return () pokeV' (Succ n) p (a :< as) = do poke p a                                  pokeV' n (p `plusPtr` sizeOf a) as+pokeV' _ _ _ = cant "pokeV"  -- -- Experiment toward simplifying away the plusPtr calls. -- succPtr :: forall a. Storable a => Ptr a -> Ptr a@@ -324,18 +341,22 @@ -- | Extract element un1 :: Vec1 a -> a un1 (a :< ZVec) = a+un1 _ = cant "un1"  -- | Extract elements un2 :: Vec2 a -> (a,a) un2 (a :< b :< ZVec) = (a,b)+un2 _ = cant "un2"  -- | Extract elements un3 :: Vec3 a -> (a,a,a) un3 (a :< b :< c :< ZVec) = (a,b,c)+un3 _ = cant "un3"  -- | Extract elements un4 :: Vec4 a -> (a,a,a,a) un4 (a :< b :< c :< d :< ZVec) = (a,b,c,d)+un4 _ = cant "un4"  -- TODO: consider this notation: --@@ -355,6 +376,7 @@ get :: Index n -> Vec n a -> a get (Index ZLess     Zero    ) (a :< _)  = a get (Index (SLess p) (Succ m)) (_ :< as) = get (Index p m) as+get _ _ = cant "get"  get0 :: Vec (N1 :+: n) a -> a   -- ^ Get first  element get1 :: Vec (N2 :+: n) a -> a   -- ^ Get second element@@ -370,6 +392,7 @@ update :: Index n -> (a -> a) -> Vec n a -> Vec n a update (Index ZLess     Zero    ) f (a :< as) = f a :< as update (Index (SLess p) (Succ m)) f (a :< as) =   a :< update (Index p m) f as+update _ _ _ = cantV "update"  -- | Replace a vector element, taking a proof that the index is within bounds. set :: Index n -> a -> Vec n a -> Vec n a@@ -408,6 +431,15 @@ flattenV' (Succ n') (v :< vs') = v <+> flattenV' n' vs' flattenV' _ _ = error "flattenV': GHC doesn't know this case can't happen." +-- | Chunk a vector into a vector of vectors (a 2D array)+chunkV :: (IsNat n, IsNat m) => Vec (n :*: m) a -> Vec n (Vec m a)+chunkV = chunkV' nat++chunkV' :: IsNat m => Nat n -> Vec (n :*: m) a -> Vec n (Vec m a)+chunkV' Zero     ZVec = ZVec+chunkV' (Succ n) as   = v :< chunkV' n as' where (v,as') = split as+chunkV' _ _ = cant "chunkV"+ -- | Swizzling.  Extract multiple elements simultaneously. swizzle :: Vec n (Index m) -> Vec m a -> Vec n a swizzle is v = flip get v <$> is@@ -426,6 +458,7 @@ split' (Succ n) (a :< as) = (a :< bs, cs)  where    (bs,cs) = split' n as+split' _ _ = cantV "split"  -- For instance, -- @@ -551,12 +584,14 @@ zipWithV :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c zipWithV _ ZVec      ZVec      = ZVec zipWithV f (a :< as) (b :< bs) = f a b :< zipWithV f as bs+zipWithV _ _ _ = cant "zipWithV"  -- | Unzip one vector into two. Like 'liftA2', but the former requires -- @IsNat n@. zipWithV3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d zipWithV3 _ ZVec      ZVec      ZVec      = ZVec zipWithV3 f (a :< as) (b :< bs) (c :< cs) = f a b c :< zipWithV3 f as bs cs+zipWithV3 _ _ _ _ = cant "zipWithV3"  -- | Unzip a vector of pairs into a pair of vectors unzipV :: Vec n (a,b) -> (Vec n a, Vec n b)

@@ -1,5 +1,5 @@ Name:                type-unary-Version:             0.2.5+Version:             0.2.8 Cabal-Version:       >= 1.6 Synopsis:               Type-level and typed unary natural numbers, inequality proofs, vectors