type-unary 0.1.14 → 0.1.15

raw patch · 3 files changed

+47/−20 lines, 3 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• src/TypeUnary/Nat.hs +21/−5
• src/TypeUnary/Vec.hs +25/−14
• type-unary.cabal +1/−1

@@ -23,6 +23,7 @@   , IsNat(..)   -- * Inequality proofs and indices   , (:<:)(..), Index(..), succI, index0, index1, index2, index3+  , coerceToIndex   ) where  import Prelude hiding (foldr,sum)@@ -110,14 +111,14 @@   ZLess :: Z :<: S n   SLess :: m :<: n -> S m :<: S n --- data Index :: * -> * where---   Index :: (n :<: lim) -> Nat n -> Index lim---- or- -- | A number under the given limit, with proof data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n) +-- Equivalently,+-- +--   data Index :: * -> * where+--     Index :: (n :<: lim) -> Nat n -> Index lim+ -- TODO: Consider removing the Nat n field, since it's computable from -- IsNat n or n :<: lim. @@ -138,6 +139,21 @@  index3 :: Index (N4 :+: m) index3 = succI index2++-- | Index generation from integer. Can fail dynamically if the integer is+-- too large.+coerceToIndex :: (Integral i, IsNat m) => i -> Index m+coerceToIndex = coerceToIndex' nat++coerceToIndex' :: Integral i => Nat m -> i -> Index m+coerceToIndex' mOrig niOrig = loop mOrig niOrig+ where+   loop :: Integral i => Nat m -> i -> Index m+   loop Zero _        = error $ "coerceToIndex: out of bounds: "+                                ++ show niOrig ++ " should be less than "+                                ++ show mOrig+   loop (Succ _)   0  = Index ZLess Zero+   loop (Succ m') ni' = succI (loop m' (ni'-1))  {--------------------------------------------------------------------     IsNat

@@ -31,6 +31,7 @@   , get, get0, get1, get2, get3   , update   , set, set0, set1, set2, set3+  , getI, setI   , swizzle, split, deleteV, elemsV   , ToVec(..)   ) where@@ -355,26 +356,22 @@ set2 = set index2 set3 = set index3 +-- | Variant of 'get' in which the index size is checked at run-time+-- instead of compile-time.+getI :: (IsNat n, Integral i) => i -> Vec n a -> a+getI = get . coerceToIndex +-- | Variant of 'set' in which the index size is checked at run-time+-- instead of compile-time.+setI :: (IsNat n, Integral i) => i -> a -> Vec n a -> Vec n a+setI = set . coerceToIndex++ -- | Swizzling.  Extract multiple elements simultaneously. swizzle :: Vec n (Index m) -> Vec m a -> Vec n a swizzle ZVec        _ = ZVec swizzle (ix :< ixs) v = get ix v :< swizzle ixs v -{---- 'a' :< 'b' :< 'c' :< ZVec-t1 :: Three Char-t1 = elemsV "abc"-     -- 'a' :< 'b' :< 'c' :< ZVec--t2 :: Four (Index N3)-t2 = elemsV [index2, index0 ,index1, index2]---- 'c' :< 'a' :< 'b' :< 'c' :< ZVec-t3 :: Four Char-t3 = swizzle t2 t1--}- -- | Split a vector split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a) split = split' nat@@ -443,6 +440,20 @@ elemsV' Zero (_:_)        = error "elemsV: too many elements" elemsV' (Succ _) []       = error "elemsV: too few elements" elemsV' (Succ n) (a : as) = a :< elemsV' n as++{-+-- 'a' :< 'b' :< 'c' :< ZVec+t1 :: Three Char+t1 = elemsV "abc"+     -- 'a' :< 'b' :< 'c' :< ZVec++t2 :: Four (Index N3)+t2 = elemsV [index2, index0 ,index1, index2]++-- 'c' :< 'a' :< 'b' :< 'c' :< ZVec+t3 :: Four Char+t3 = swizzle t2 t1+-}   {--------------------------------------------------------------------

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