type-unary 0.1.2 → 0.1.3

raw patch · 2 files changed

+39/−15 lines, 2 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

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

@@ -35,8 +35,8 @@   , Vec10,Vec11,Vec12,Vec13,Vec14,Vec15,Vec16   , vec1, vec2, vec3, vec4   , un1, un2, un3, un4-  , get0, get1, get2, get3-  , get, swizzle, split+  , get, get0, get1, get2, get3+  , swizzle, split   , ToVec(..)   ) where @@ -190,16 +190,16 @@ succI :: Index m -> Index (S m) succI (Index p n) = Index (SLess p) (Succ n) -index0 :: Index (S m)+index0 :: Index (N1 :+: m) index0 = Index ZLess Zero -index1 :: Index (S (S m))+index1 :: Index (N2 :+: m) index1 = succI index0 -index2 :: Index (S (S (S m)))+index2 :: Index (N3 :+: m) index2 = succI index1 -index3 :: Index (S (S (S (S m))))+index3 :: Index (N4 :+: m) index3 = succI index2  @@ -259,6 +259,11 @@ instance Show a => Show (Vec n a) where   show v = "elemsV " ++ show (toList v) +-- 2011-10-26: There was an orphan Show Vec instance in shady-gen's+-- Shady.Language.Type, which conflicted with the Show instance above. To+-- do: check whether this change broke Shady's code generation. Maybe not,+-- if the code generation uses Pretty instead of Show.+ instance Functor (Vec n) where   fmap _ ZVec     = ZVec   fmap f (a :< u) = f a :< fmap f u@@ -431,15 +436,14 @@ --------------------------------------------------------------------}  -- | General indexing, taking a proof that the index is within bounds.-get :: Index n -> Vec n a -> Vec1 a-get (Index ZLess     Zero    ) (a :< _)  = vec1 a+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 --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 :: Vec (N1 :+: n) a -> a   -- ^ Get first  element+get1 :: Vec (N2 :+: n) a -> a   -- ^ Get second element+get2 :: Vec (N3 :+: n) a -> a   -- ^ Get third  element+get3 :: Vec (N4 :+: n) a -> a   -- ^ Get fourth element  get0 = get index0 get1 = get index1@@ -450,7 +454,7 @@ -- | Swizzling.  Extract multiple elements simultaneously. 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+swizzle (ix :< ixs) v = get ix v :< swizzle ixs v  {- -- 'a' :< 'b' :< 'c' :< ZVec@@ -496,6 +500,26 @@ --                TypeUnary.Vec.take :: IsNat n => Vec (n :+: m) a -> Vec n a --     at /Users/conal/Haskell/type-unary/src/TypeUnary/Vec.hs:488:1-18 --   NB: `:+:' is a type function, and may not be injective++{-++-- Reversal. Thinking about this one. Currently thwarted by missing+-- knowledge about numbers in the type-checker. Would be easy with+-- built-in type-level naturals.++-- | Reverse a vector+reverseV :: Vec n a -> Vec n a+reverseV = reverse' nat ZVec++--  Couldn't match type `n' with `n :+: Z'++-- Reverse na and append to ma+reverse' :: Nat n -> Vec m a -> Vec n a -> Vec (n :+: m) a+reverse' Zero     ma ZVec      = ma+reverse' (Succ n) ma (a :< as) = reverse' n (a :< ma) as++-- Could not deduce ((n1 :+: S m) ~ S (n1 :+: m))+-}  {--------------------------------------------------------------------     Conversion to vectors

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