packages feed

grow-vector 0.1.0.0 → 0.1.1.0

raw patch · 4 files changed

+120/−19 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

CHANGELOG.md view
@@ -1,3 +1,7 @@+# 0.1.1.0++* Add liquid haskell refinements.+ # 0.0.1.0  * Initial release
grow-vector.cabal view
@@ -1,7 +1,7 @@ name:                grow-vector synopsis:            Mutable vector with efficient appends description:         Mutable vector with efficient updates. Simple implementation on partially filled array with capacity tracking and resizing.-version:             0.1.0.0+version:             0.1.1.0 license:             MIT license-file:        LICENSE copyright:           2020 Anton Gushcha@@ -12,6 +12,7 @@ extra-source-files:   README.md   CHANGELOG.md+data-files:           src/Data/Vector/Grow/Unboxed.spec  source-repository head   type: git@@ -36,6 +37,7 @@         liquid-base       , liquid-vector       , liquidhaskell >= 0.8.10+    cpp-options: -DLIQUID   else     build-depends:         base          >= 4.5      && < 4.15
src/Data/Vector/Grow/Unboxed.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -65,18 +66,18 @@ -- | Return current capacity of the vector (amount of elements that it can fit without realloc) capacity :: (Unbox a, PrimMonad m) => GrowVector (PrimState m) a -> m Int capacity v = do-  mv <- readMutVar . growVector $! v+  mv <- readMutVar $ growVector v   pure $ M.length mv {-# INLINE capacity #-}  -- | Return current amount of elements in the vector length :: (Unbox a, PrimMonad m) => GrowVector (PrimState m) a -> m Int-length = readMutVar . growVectorLength+length v = readMutVar $ growVectorLength v {-# INLINE length #-}  -- | Return 'True' if there is no elements inside the vector null :: (Unbox a, PrimMonad m) => GrowVector (PrimState m) a -> m Bool-null = fmap (== 0) . length+null v = fmap (== 0) $ length v {-# INLINE null #-}  -- | Allocation of new growable vector with given capacity.@@ -98,7 +99,7 @@   -> m (GrowVector (PrimState m) a) slice i n v = do   newSize <- newMutVar n-  mv <- readMutVar . growVector $! v+  mv <- readMutVar $ growVector v   newVec <- newMutVar $! M.slice i n mv   pure $! GrowVector newVec newSize {-# INLINABLE slice #-}@@ -117,13 +118,14 @@ -- | Freezing growable vector. It will contain only actual elements of the vector not including capacity -- space, but you should call 'U.force' on resulting vector to not hold the allocated capacity of original -- vector in memory.+ freeze :: (Unbox a, PrimMonad m)   => GrowVector (PrimState m) a   -> m (U.Vector a) freeze v = do   n <- length v-  mv <- readMutVar . growVector $! v-  U.freeze . M.take n $! mv+  mv <- readMutVar $ growVector v+  U.freeze $ M.take n mv {-# INLINABLE freeze #-}  -- | Ensure that grow vector has at least given capacity possibly with reallocation.@@ -134,19 +136,19 @@ ensure v n = do   c <- capacity v   unless (c >= n) $ do-    mv <- readMutVar . growVector $! v+    mv <- readMutVar $ growVector v     writeMutVar (growVector v) =<< M.grow mv (n - c) {-# INLINABLE ensure #-}  -- | Ensure that grow vector has enough space for additonal n elements.--- We grow vector by 1.5 factor or by+-- We grow vector by 1.5 factor or by required elements count * 1.5. ensureAppend :: (Unbox a, PrimMonad m)   => GrowVector (PrimState m) a   -> Int -- ^ Additional n elements   -> m () ensureAppend v i = do-  n <- readMutVar . growVectorLength $! v-  mv <- readMutVar . growVector $! v+  n <- readMutVar $ growVectorLength v+  mv <- readMutVar $ growVector v   let c = M.length mv   unless (c >= n + i) $ do     let growFactor = 1.5@@ -160,9 +162,11 @@   -> Int -- ^ Index of element. Must be in [0 .. length) range   -> m a read v i = do-  n <- readMutVar . growVectorLength $! v+  n <- readMutVar $ growVectorLength v+#ifndef LIQUID   when (i < 0 || i >= n) $ error $ "GrowVector.read: index " <> show i <> " is out bounds " <> show n-  mv <- readMutVar . growVector $! v+#endif+  mv <- readMutVar $ growVector v   M.unsafeRead mv i {-# INLINABLE read #-} @@ -172,7 +176,7 @@   -> Int -- ^ Index of element. Must be in [0 .. length) range   -> m a unsafeRead v i = do-  mv <- readMutVar . growVector $! v+  mv <- readMutVar $ growVector v   M.unsafeRead mv i {-# INLINABLE unsafeRead #-} @@ -183,9 +187,11 @@   -> a   -> m () write v i a = do-  n <- readMutVar . growVectorLength $! v+  n <- readMutVar $ growVectorLength v+#ifndef LIQUID   when (i < 0 || i >= n) $ error $ "GrowVector.write: index " <> show i <> " is out bounds " <> show n-  mv <- readMutVar . growVector $! v+#endif+  mv <- readMutVar $ growVector v   M.unsafeWrite mv i a {-# INLINABLE write #-} @@ -196,7 +202,7 @@   -> a   -> m () unsafeWrite v i a = do-  mv <- readMutVar . growVector $! v+  mv <- readMutVar $ growVector v   M.unsafeWrite mv i a {-# INLINABLE unsafeWrite #-} @@ -217,8 +223,8 @@   -> a   -> m () unsafePushBack v a = do-  n <- readMutVar . growVectorLength $! v-  mv <- readMutVar . growVector $! v+  n <- readMutVar $ growVectorLength v+  mv <- readMutVar $ growVector v   M.write mv n a   writeMutVar (growVectorLength v) (n+1) {-# INLINABLE unsafePushBack #-}
+ src/Data/Vector/Grow/Unboxed.spec view
@@ -0,0 +1,89 @@+module spec Data.Vector.Grow.Unboxed where++import Data.Vector++measure vlen    :: forall a. (U.Vector a) -> Int++invariant       {v: U.Vector a | 0 <= vlen v }++(U.!)           :: forall a. x:(U.Vector a) -> vec:{v:Nat | v < vlen x } -> a++U.unsafeIndex :: forall a. x:(U.Vector a) -> vec:{v:Nat | v < vlen x } -> a++U.fromList  :: forall a. x:[a] -> {v: U.Vector a  | vlen v = len x }++U.length    :: forall a. x:(U.Vector a) -> {v : Nat | v = vlen x }++U.replicate :: n:Nat -> a -> {v:U.Vector a | vlen v = n}++U.imap :: (Nat -> a -> b) -> x:(U.Vector a) -> {y:U.Vector b | vlen y = vlen x }++U.map :: (a -> b) -> x:(U.Vector a) -> {y:U.Vector b | vlen y = vlen x }++U.head :: forall a. {xs: U.Vector a | vlen xs > 0} -> a+++measure gvlen :: GrowVector s a -> Int+measure gvcap :: GrowVector s a -> Int++invariant {v: GrowVector s a | 0 <= gvlen v }+invariant {v: GrowVector s a | 0 <= gvcap v }+invariant {v: GrowVector s a | gvlen v <= gvcap v }++type GrowVectorN s a N = {v:GrowVector s a | gvlen v == N}+type GrowVectorC s a C = {v:GrowVector s a | gvcap v == C}+type GrowVectorNC s a N C = {v:GrowVector s a | gvlen v == N && gvcap v == C}++assume capacity :: (Unbox a, PrimMonad m) => x : GrowVector (PrimState m) a -> m {v:Int | v = gvcap x}++assume length :: (Unbox a, PrimMonad m) => x : GrowVector (PrimState m) a -> m {v:Int | v = gvlen x}++null :: (Unbox a, PrimMonad m) => x : GrowVector (PrimState m) a -> m { v:Bool | v <=> gvlen x = 0}++assume newSized :: (Unbox a, PrimMonad m) => l:Nat -> {c:Nat | c >= l} -> m { v:(GrowVector (PrimState m) a) | l = gvlen v && c = gvcap v }++assume slice :: (Unbox a, PrimMonad m)+  => i:Nat+  -> n:Nat+  -> {x:(GrowVector (PrimState m) a) | i < gvlen x && i + n <= gvlen x }+  -> m {y:(GrowVector (PrimState m) a) | gvlen y = n && gvcap y = n }++assume thaw :: (Unbox a, PrimMonad m)+  => v : U.Vector a+  -> m {gv:(GrowVector (PrimState m) a) | vlen v == gvlen gv && gvcap gv == 0 }++freeze :: (Unbox a, PrimMonad m)+  => gv : GrowVector (PrimState m) a+  -> m {v:(U.Vector a) | vlen v == gvlen gv }++assume ensure :: (Unbox a, PrimMonad m)+  => x : GrowVector (PrimState m) a+  -> c : Nat+  -> m {r:() | gvcap x = c}++assume ensureAppend :: (Unbox a, PrimMonad m)+  => x : GrowVector (PrimState m) a+  -> n : Nat+  -> m {r:() | gvcap x >= gvlen x + n }++read :: (Unbox a, PrimMonad m)+  => x : GrowVector (PrimState m) a+  -> {i:Nat | i < gvlen x}+  -> m a++unsafeRead :: (Unbox a, PrimMonad m)+  => x : GrowVector (PrimState m) a+  -> {i:Nat | i < gvlen x}+  -> m a++write :: (Unbox a, PrimMonad m)+  => x : GrowVector (PrimState m) a+  -> {i:Nat | i < gvlen x}+  -> a+  -> m ()++unsafeWrite :: (Unbox a, PrimMonad m)+  => x : GrowVector (PrimState m) a+  -> {i:Nat | i < gvlen x}+  -> a+  -> m ()