liquid-vector 0.12.3.1 → 0.12.3.1.2
raw patch · 24 files changed
+53/−139 lines, 24 filesdep +basedep −liquid-basedep ~liquidhaskelldep ~vector
Dependencies added: base
Dependencies removed: liquid-base
Dependency ranges changed: liquidhaskell, vector
Files
- liquid-vector.cabal +7/−34
- src/Data/Vector.hs +0/−3
- src/Data/Vector.spec +0/−40
- src/Data/Vector/Fusion/Bundle.hs +0/−3
- src/Data/Vector/Fusion/Bundle/Monadic.hs +0/−3
- src/Data/Vector/Fusion/Bundle/Size.hs +0/−3
- src/Data/Vector/Fusion/Stream/Monadic.hs +0/−3
- src/Data/Vector/Fusion/Util.hs +0/−3
- src/Data/Vector/Generic.hs +0/−3
- src/Data/Vector/Generic/Base.hs +0/−3
- src/Data/Vector/Generic/Mutable.hs +0/−3
- src/Data/Vector/Generic/Mutable/Base.hs +0/−3
- src/Data/Vector/Generic/New.hs +0/−3
- src/Data/Vector/Internal/Check.hs +0/−3
- src/Data/Vector/Mutable.hs +0/−4
- src/Data/Vector/Primitive.hs +0/−3
- src/Data/Vector/Primitive/Mutable.hs +0/−3
- src/Data/Vector/Storable.hs +0/−3
- src/Data/Vector/Storable/Internal.hs +0/−3
- src/Data/Vector/Storable/Mutable.hs +0/−3
- src/Data/Vector/Unboxed.hs +0/−3
- src/Data/Vector/Unboxed/Base.hs +0/−3
- src/Data/Vector/Unboxed/Mutable.hs +0/−4
- src/Data/Vector_LHAssumptions.hs +46/−0
liquid-vector.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.24 name: liquid-vector-version: 0.12.3.1+version: 0.12.3.1.2 synopsis: LiquidHaskell specs for the vector package description: LiquidHaskell specs for the vector package. license: BSD3@@ -12,44 +12,17 @@ homepage: https://github.com/ucsd-progsys/liquidhaskell build-type: Custom -data-files: src/Data/Vector.spec- custom-setup- setup-depends: Cabal<4, base<5, liquidhaskell+ setup-depends: Cabal<4, base<5, liquidhaskell-boot library- exposed-modules: Data.Vector.Internal.Check- Data.Vector.Fusion.Util- Data.Vector.Fusion.Stream.Monadic- Data.Vector.Fusion.Bundle.Size- Data.Vector.Fusion.Bundle.Monadic- Data.Vector.Fusion.Bundle-- Data.Vector.Generic.Mutable.Base- Data.Vector.Generic.Mutable- Data.Vector.Generic.Base- Data.Vector.Generic.New- Data.Vector.Generic-- Data.Vector.Primitive.Mutable- Data.Vector.Primitive-- Data.Vector.Storable.Internal- Data.Vector.Storable.Mutable- Data.Vector.Storable-- Data.Vector.Unboxed.Base- Data.Vector.Unboxed.Mutable- Data.Vector.Unboxed-- Data.Vector.Mutable- Data.Vector+ exposed-modules: Data.Vector_LHAssumptions hs-source-dirs: src- build-depends: liquid-base < 4.16- , vector >= 0.12.3.1 && < 0.13- , liquidhaskell >= 0.9.0.2+ build-depends: base < 5+ , vector >= 0.12.3.1 && < 0.14+ , liquidhaskell >= 0.9.2.5 default-language: Haskell2010 default-extensions: PackageImports if impl(ghc >= 8.10) ghc-options: -fplugin=LiquidHaskell -fplugin-opt=LiquidHaskell:--no-positivity-check- +
− src/Data/Vector.hs
@@ -1,3 +0,0 @@-module Data.Vector ( module Exports ) where--import "vector" Data.Vector as Exports
− src/Data/Vector.spec
@@ -1,40 +0,0 @@-module spec Data.Vector where--import GHC.Base--data variance Data.Vector.Vector covariant---measure vlen :: forall a. (Data.Vector.Vector a) -> Int--invariant {v: Data.Vector.Vector a | 0 <= vlen v } --! :: forall a. x:(Data.Vector.Vector a) -> vec:{v:Nat | v < vlen x } -> a --unsafeIndex :: forall a. x:(Data.Vector.Vector a) -> vec:{v:Nat | v < vlen x } -> a --fromList :: forall a. x:[a] -> {v: Data.Vector.Vector a | vlen v = len x }--length :: forall a. x:(Data.Vector.Vector a) -> {v : Nat | v = vlen x }--replicate :: n:Nat -> a -> {v:Data.Vector.Vector a | vlen v = n} --imap :: (Nat -> a -> b) -> x:(Data.Vector.Vector a) -> {y:Data.Vector.Vector b | vlen y = vlen x }--map :: (a -> b) -> x:(Data.Vector.Vector a) -> {y:Data.Vector.Vector b | vlen y = vlen x }--head :: forall a. {xs: Data.Vector.Vector a | vlen xs > 0} -> a --qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) = 0 -qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) > 0 -qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) >= 0 --qualif Vlen(v:int, x: Data.Vector.Vector a) : (v = vlen x)-qualif Vlen(v:int, x: Data.Vector.Vector a) : (v <= vlen x) -qualif Vlen(v:int, x: Data.Vector.Vector a) : (v < vlen x) --qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v < vlen x) -qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v <= vlen x) -qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v > vlen x) -qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v >= vlen x) -qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v = vlen x)
− src/Data/Vector/Fusion/Bundle.hs
@@ -1,3 +0,0 @@-module Data.Vector.Fusion.Bundle (module Exports) where--import "vector" Data.Vector.Fusion.Bundle as Exports
− src/Data/Vector/Fusion/Bundle/Monadic.hs
@@ -1,3 +0,0 @@-module Data.Vector.Fusion.Bundle.Monadic (module Exports) where--import "vector" Data.Vector.Fusion.Bundle.Monadic as Exports
− src/Data/Vector/Fusion/Bundle/Size.hs
@@ -1,3 +0,0 @@-module Data.Vector.Fusion.Bundle.Size (module Exports) where--import "vector" Data.Vector.Fusion.Bundle.Size as Exports
− src/Data/Vector/Fusion/Stream/Monadic.hs
@@ -1,3 +0,0 @@-module Data.Vector.Fusion.Stream.Monadic (module Exports) where--import "vector" Data.Vector.Fusion.Stream.Monadic as Exports
− src/Data/Vector/Fusion/Util.hs
@@ -1,3 +0,0 @@-module Data.Vector.Fusion.Util (module Exports) where--import "vector" Data.Vector.Fusion.Util as Exports
− src/Data/Vector/Generic.hs
@@ -1,3 +0,0 @@-module Data.Vector.Generic (module Exports) where--import "vector" Data.Vector.Generic as Exports
− src/Data/Vector/Generic/Base.hs
@@ -1,3 +0,0 @@-module Data.Vector.Generic.Base (module Exports) where--import "vector" Data.Vector.Generic.Base as Exports
− src/Data/Vector/Generic/Mutable.hs
@@ -1,3 +0,0 @@-module Data.Vector.Generic.Mutable ( module Exports ) where--import "vector" Data.Vector.Generic.Mutable as Exports
− src/Data/Vector/Generic/Mutable/Base.hs
@@ -1,3 +0,0 @@-module Data.Vector.Generic.Mutable.Base (module Exports) where--import "vector" Data.Vector.Generic.Mutable.Base as Exports
− src/Data/Vector/Generic/New.hs
@@ -1,3 +0,0 @@-module Data.Vector.Generic.New (module Exports) where--import "vector" Data.Vector.Generic.New as Exports
− src/Data/Vector/Internal/Check.hs
@@ -1,3 +0,0 @@-module Data.Vector.Internal.Check (module Exports) where--import "vector" Data.Vector.Internal.Check as Exports
− src/Data/Vector/Mutable.hs
@@ -1,4 +0,0 @@--module Data.Vector.Mutable (module Exports) where--import "vector" Data.Vector.Mutable as Exports
− src/Data/Vector/Primitive.hs
@@ -1,3 +0,0 @@-module Data.Vector.Primitive (module Exports) where--import "vector" Data.Vector.Primitive as Exports
− src/Data/Vector/Primitive/Mutable.hs
@@ -1,3 +0,0 @@-module Data.Vector.Primitive.Mutable (module Exports) where--import "vector" Data.Vector.Primitive.Mutable as Exports
− src/Data/Vector/Storable.hs
@@ -1,3 +0,0 @@-module Data.Vector.Storable (module Exports) where--import "vector" Data.Vector.Storable as Exports
− src/Data/Vector/Storable/Internal.hs
@@ -1,3 +0,0 @@-module Data.Vector.Storable.Internal (module Exports) where--import "vector" Data.Vector.Storable.Internal as Exports
− src/Data/Vector/Storable/Mutable.hs
@@ -1,3 +0,0 @@-module Data.Vector.Storable.Mutable (module Exports) where--import "vector" Data.Vector.Storable.Mutable as Exports
− src/Data/Vector/Unboxed.hs
@@ -1,3 +0,0 @@-module Data.Vector.Unboxed (module Exports) where--import "vector" Data.Vector.Unboxed as Exports
− src/Data/Vector/Unboxed/Base.hs
@@ -1,3 +0,0 @@-module Data.Vector.Unboxed.Base (module Exports) where--import "vector" Data.Vector.Unboxed.Base as Exports
− src/Data/Vector/Unboxed/Mutable.hs
@@ -1,4 +0,0 @@-module Data.Vector.Unboxed.Mutable (module Exports) where--import "vector" Data.Vector.Unboxed.Mutable as Exports-
+ src/Data/Vector_LHAssumptions.hs view
@@ -0,0 +1,46 @@+{-# OPTIONS_GHC -Wno-unused-imports #-}+module Data.Vector_LHAssumptions where++import Data.Vector+import GHC.Base++{-@++data variance Data.Vector.Vector covariant+++measure vlen :: forall a. (Data.Vector.Vector a) -> Int++invariant {v: Data.Vector.Vector a | 0 <= vlen v }++assume Data.Vector.! :: forall a. x:(Data.Vector.Vector a) -> vec:{v:Nat | v < vlen x } -> a++assume Data.Vector.unsafeIndex :: forall a. x:(Data.Vector.Vector a) -> vec:{v:Nat | v < vlen x } -> a++assume Data.Vector.fromList :: forall a. x:[a] -> {v: Data.Vector.Vector a | vlen v = len x }++assume Data.Vector.length :: forall a. x:(Data.Vector.Vector a) -> {v : Nat | v = vlen x }++assume Data.Vector.replicate :: n:Nat -> a -> {v:Data.Vector.Vector a | vlen v = n}++assume Data.Vector.imap :: (Nat -> a -> b) -> x:(Data.Vector.Vector a) -> {y:Data.Vector.Vector b | vlen y = vlen x }++assume Data.Vector.map :: (a -> b) -> x:(Data.Vector.Vector a) -> {y:Data.Vector.Vector b | vlen y = vlen x }++assume Data.Vector.head :: forall a. {xs: Data.Vector.Vector a | vlen xs > 0} -> a++qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) = 0+qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) > 0+qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) >= 0++qualif Vlen(v:int, x: Data.Vector.Vector a) : (v = vlen x)+qualif Vlen(v:int, x: Data.Vector.Vector a) : (v <= vlen x)+qualif Vlen(v:int, x: Data.Vector.Vector a) : (v < vlen x)++qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v < vlen x)+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v <= vlen x)+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v > vlen x)+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v >= vlen x)+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v = vlen x)++@-}