hvect 0.2.0.0 → 0.3.0.0

raw patch · 4 files changed

+107/−35 lines, 4 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• README.md +33/−0
• hvect.cabal +6/−3
• src/Data/HVect.hs +60/−32
• test/Data/HVectTest.hs +8/−0

@@ -0,0 +1,33 @@+hvect+=====++[![Build Status](https://travis-ci.org/agrafix/hvect.svg)](https://travis-ci.org/agrafix/hvect)+[![Hackage](https://img.shields.io/hackage/v/hvect.svg)](http://hackage.haskell.org/package/hvect)++## Intro++Hackage: [hvect](http://hackage.haskell.org/package/hvect)+Stackage: [hvect](https://www.stackage.org/package/hvect)++Simple strict heterogeneous lists+++## Install++* Using cabal: `cabal install hvect`+* Using Stack: `stack install hvect`+* From Source (cabal): `git clone https://github.com/agrafix/hvect.git && cd hvect && cabal install`+* From Source (stack): `git clone https://github.com/agrafix/hvect.git && cd hvect && stack build`+++## Misc++### Supported GHC Versions++* 7.8.4+* 7.10.2++### License++Released under the MIT license.+(c) 2014 - 2015 Alexander Thiemann <mail@athiemann.net>, Tim Baumann <tim@timbaumann.info>

@@ -1,5 +1,5 @@ name:                hvect-version:             0.2.0.0+version:             0.3.0.0 synopsis:            Simple strict heterogeneous lists description:         Small, concise and simple implementation of heterogeneous lists with useful utility functions homepage:            https://github.com/agrafix/hvect@@ -12,10 +12,13 @@ category:            Data build-type:          Simple cabal-version:       >=1.10+tested-with:         GHC==7.8.4, GHC==7.10.2+extra-source-files:+    README.md  library   exposed-modules:     Data.HVect-  build-depends:       base >=4.6 && <5+  build-depends:       base >=4.7 && <5   hs-source-dirs:      src   default-language:    Haskell2010 @@ -31,4 +34,4 @@  source-repository head   type:     git-  location: git://github.com/agrafix/hvect.git+  location: https://github.com/agrafix/hvect

@@ -1,19 +1,22 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-}-{-# LANGUAGE UndecidableInstances #-} -- for ReverseLoop type family {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE FlexibleInstances #-}-+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE UndecidableInstances #-} -- for ReverseLoop type family module Data.HVect   ( -- * typesafe strict vector     HVect (..)   , empty, null, head, tail   , singleton   , length, HVectLen (..)+  , findFirst, InList (..), ListContains (..), NotInList(..)   , (!!), HVectIdx (..)   , HVectElim   , Append, (<++>)@@ -28,6 +31,7 @@   , (:<)   ) where +import Data.Proxy import Prelude hiding (reverse, uncurry, curry, head, null, (!!), length, tail)  -- | Heterogeneous vector@@ -66,16 +70,41 @@     a :&: as <= b :&: bs =         a <= b && as <= bs --- todo: use a closed type family once GHC 7.6 compatibility is dropped-type family HVectElim (ts :: [*]) (a :: *) :: *-type instance HVectElim '[] a = a-type instance HVectElim (t ': ts) a = t -> HVectElim ts a+type family HVectElim (ts :: [*]) (a :: *) :: * where+    HVectElim '[] a = a+    HVectElim (t ': ts) a = t -> HVectElim ts a --- todo: use a closed type family once GHC 7.6 compatibility is dropped-type family Append (as :: [*]) (bs :: [*]) :: [*]-type instance Append '[] bs = bs-type instance Append (a ': as) bs = a ': (Append as bs)+type family Append (as :: [*]) (bs :: [*]) :: [*] where+    Append '[] bs = bs+    Append (a ': as) bs = a ': (Append as bs) +type family InList (x :: *) (xs :: [*]) :: Nat where+    InList x (x ': ys) = Zero+    InList x (y ': ys) = Succ (InList x ys)++class SNatRep n where+    getSNat :: SNat n++instance SNatRep Zero where+    getSNat = SZero++instance SNatRep n => SNatRep (Succ n) where+    getSNat = SSucc getSNat++type family NotInList (x :: *) (xs :: [*]) :: Bool where+    NotInList x (x ': ys) = False+    NotInList x (y ': ys) = NotInList x ys+    NotInList x '[] = True++type ListContains n x ts = (SNatRep n, InList x ts ~ n, HVectIdx n ts ~ x)++-- | Find first element in 'HVect' of type x+findFirst :: forall x ts n. (ListContains n x ts) => HVect ts -> x+findFirst vect = idx !! vect+    where+      idx :: SNat n+      idx = getSNat+ singleton :: a -> HVect '[a] singleton el = el :&: HNil @@ -117,25 +146,24 @@ data AnySNat where     AnySNat :: forall n. SNat n -> AnySNat -type family HVectLen (ts :: [*]) :: Nat-type instance HVectLen '[] = Zero-type instance HVectLen (t ': ts) = Succ (HVectLen ts)+type family HVectLen (ts :: [*]) :: Nat where+    HVectLen '[] = Zero+    HVectLen (t ': ts) = Succ (HVectLen ts) -type family HVectIdx (n :: Nat) (ts :: [*]) :: *-type instance HVectIdx Zero (a ': as) = a-type instance HVectIdx (Succ n) (a ': as) = HVectIdx n as-type instance HVectIdx a '[] = ()+type family HVectIdx (n :: Nat) (ts :: [*]) :: * where+    HVectIdx Zero (a ': as) = a+    HVectIdx (Succ n) (a ': as) = HVectIdx n as -type family (m :: Nat) :< (n :: Nat) :: Bool-type instance m :< Zero = False-type instance Zero :< (Succ n) = True-type instance (Succ m) :< (Succ n) = m :< n+type family (m :: Nat) :< (n :: Nat) :: Bool where+    m :< Zero = False+    Zero :< (Succ n) = True+    (Succ m) :< (Succ n) = m :< n -type family (m :: Nat) :- (n :: Nat) :: Nat-type instance n :- Zero = n-type instance (Succ m) :- (Succ n) = m :- n+type family (m :: Nat) :- (n :: Nat) :: Nat where+    n :- Zero = n+    (Succ m) :- (Succ n) = m :- n -(!!) :: ((n :< HVectLen as) ~ True) => SNat n -> HVect as -> HVectIdx n as+(!!) :: SNat n -> HVect as -> HVectIdx n as SZero !! (a :&: as) = a (SSucc s) !! (a :&: as) = s !! as @@ -147,9 +175,9 @@ (<++>) HNil bs = bs (<++>) (a :&: as) bs = a :&: (as <++> bs) -type family ReverseLoop (as :: [*]) (bs :: [*]) :: [*]-type instance ReverseLoop '[] bs = bs-type instance ReverseLoop (a ': as) bs = ReverseLoop as (a ': bs)+type family ReverseLoop (as :: [*]) (bs :: [*]) :: [*] where+    ReverseLoop '[] bs = bs+    ReverseLoop (a ': as) bs = ReverseLoop as (a ': bs)  type Reverse as = ReverseLoop as '[] 

@@ -72,3 +72,11 @@     do assertEqual "foo" (SZero HV.!! ("foo" :&: "bar" :&: empty))        assertEqual "bar" (SSucc SZero HV.!! ("foo" :&: "bar" :&: empty))        assertEqual "bar" (SSucc (SSucc SZero) HV.!! (True :&: "foo" :&: "bar" :&: empty))++test_getFirst :: IO ()+test_getFirst =+    do assertEqual True (findFirst (intOne :&: True :&: False :&: "foo" :&: empty))+       assertEqual intOne (findFirst (intOne :&: True :&: False :&: "foo" :&: empty))+    where+      intOne :: Int+      intOne = 1