diff --git a/liquid-vector.cabal b/liquid-vector.cabal --- a/liquid-vector.cabal +++ b/liquid-vector.cabal @@ -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 - + diff --git a/src/Data/Vector.hs b/src/Data/Vector.hs deleted file mode 100644 --- a/src/Data/Vector.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector ( module Exports ) where - -import "vector" Data.Vector as Exports diff --git a/src/Data/Vector.spec b/src/Data/Vector.spec deleted file mode 100644 --- a/src/Data/Vector.spec +++ /dev/null @@ -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) diff --git a/src/Data/Vector/Fusion/Bundle.hs b/src/Data/Vector/Fusion/Bundle.hs deleted file mode 100644 --- a/src/Data/Vector/Fusion/Bundle.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Fusion.Bundle (module Exports) where - -import "vector" Data.Vector.Fusion.Bundle as Exports diff --git a/src/Data/Vector/Fusion/Bundle/Monadic.hs b/src/Data/Vector/Fusion/Bundle/Monadic.hs deleted file mode 100644 --- a/src/Data/Vector/Fusion/Bundle/Monadic.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Fusion.Bundle.Monadic (module Exports) where - -import "vector" Data.Vector.Fusion.Bundle.Monadic as Exports diff --git a/src/Data/Vector/Fusion/Bundle/Size.hs b/src/Data/Vector/Fusion/Bundle/Size.hs deleted file mode 100644 --- a/src/Data/Vector/Fusion/Bundle/Size.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Fusion.Bundle.Size (module Exports) where - -import "vector" Data.Vector.Fusion.Bundle.Size as Exports diff --git a/src/Data/Vector/Fusion/Stream/Monadic.hs b/src/Data/Vector/Fusion/Stream/Monadic.hs deleted file mode 100644 --- a/src/Data/Vector/Fusion/Stream/Monadic.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Fusion.Stream.Monadic (module Exports) where - -import "vector" Data.Vector.Fusion.Stream.Monadic as Exports diff --git a/src/Data/Vector/Fusion/Util.hs b/src/Data/Vector/Fusion/Util.hs deleted file mode 100644 --- a/src/Data/Vector/Fusion/Util.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Fusion.Util (module Exports) where - -import "vector" Data.Vector.Fusion.Util as Exports diff --git a/src/Data/Vector/Generic.hs b/src/Data/Vector/Generic.hs deleted file mode 100644 --- a/src/Data/Vector/Generic.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Generic (module Exports) where - -import "vector" Data.Vector.Generic as Exports diff --git a/src/Data/Vector/Generic/Base.hs b/src/Data/Vector/Generic/Base.hs deleted file mode 100644 --- a/src/Data/Vector/Generic/Base.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Generic.Base (module Exports) where - -import "vector" Data.Vector.Generic.Base as Exports diff --git a/src/Data/Vector/Generic/Mutable.hs b/src/Data/Vector/Generic/Mutable.hs deleted file mode 100644 --- a/src/Data/Vector/Generic/Mutable.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Generic.Mutable ( module Exports ) where - -import "vector" Data.Vector.Generic.Mutable as Exports diff --git a/src/Data/Vector/Generic/Mutable/Base.hs b/src/Data/Vector/Generic/Mutable/Base.hs deleted file mode 100644 --- a/src/Data/Vector/Generic/Mutable/Base.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Generic.Mutable.Base (module Exports) where - -import "vector" Data.Vector.Generic.Mutable.Base as Exports diff --git a/src/Data/Vector/Generic/New.hs b/src/Data/Vector/Generic/New.hs deleted file mode 100644 --- a/src/Data/Vector/Generic/New.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Generic.New (module Exports) where - -import "vector" Data.Vector.Generic.New as Exports diff --git a/src/Data/Vector/Internal/Check.hs b/src/Data/Vector/Internal/Check.hs deleted file mode 100644 --- a/src/Data/Vector/Internal/Check.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Internal.Check (module Exports) where - -import "vector" Data.Vector.Internal.Check as Exports diff --git a/src/Data/Vector/Mutable.hs b/src/Data/Vector/Mutable.hs deleted file mode 100644 --- a/src/Data/Vector/Mutable.hs +++ /dev/null @@ -1,4 +0,0 @@ - -module Data.Vector.Mutable (module Exports) where - -import "vector" Data.Vector.Mutable as Exports diff --git a/src/Data/Vector/Primitive.hs b/src/Data/Vector/Primitive.hs deleted file mode 100644 --- a/src/Data/Vector/Primitive.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Primitive (module Exports) where - -import "vector" Data.Vector.Primitive as Exports diff --git a/src/Data/Vector/Primitive/Mutable.hs b/src/Data/Vector/Primitive/Mutable.hs deleted file mode 100644 --- a/src/Data/Vector/Primitive/Mutable.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Primitive.Mutable (module Exports) where - -import "vector" Data.Vector.Primitive.Mutable as Exports diff --git a/src/Data/Vector/Storable.hs b/src/Data/Vector/Storable.hs deleted file mode 100644 --- a/src/Data/Vector/Storable.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Storable (module Exports) where - -import "vector" Data.Vector.Storable as Exports diff --git a/src/Data/Vector/Storable/Internal.hs b/src/Data/Vector/Storable/Internal.hs deleted file mode 100644 --- a/src/Data/Vector/Storable/Internal.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Storable.Internal (module Exports) where - -import "vector" Data.Vector.Storable.Internal as Exports diff --git a/src/Data/Vector/Storable/Mutable.hs b/src/Data/Vector/Storable/Mutable.hs deleted file mode 100644 --- a/src/Data/Vector/Storable/Mutable.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Storable.Mutable (module Exports) where - -import "vector" Data.Vector.Storable.Mutable as Exports diff --git a/src/Data/Vector/Unboxed.hs b/src/Data/Vector/Unboxed.hs deleted file mode 100644 --- a/src/Data/Vector/Unboxed.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Unboxed (module Exports) where - -import "vector" Data.Vector.Unboxed as Exports diff --git a/src/Data/Vector/Unboxed/Base.hs b/src/Data/Vector/Unboxed/Base.hs deleted file mode 100644 --- a/src/Data/Vector/Unboxed/Base.hs +++ /dev/null @@ -1,3 +0,0 @@ -module Data.Vector.Unboxed.Base (module Exports) where - -import "vector" Data.Vector.Unboxed.Base as Exports diff --git a/src/Data/Vector/Unboxed/Mutable.hs b/src/Data/Vector/Unboxed/Mutable.hs deleted file mode 100644 --- a/src/Data/Vector/Unboxed/Mutable.hs +++ /dev/null @@ -1,4 +0,0 @@ -module Data.Vector.Unboxed.Mutable (module Exports) where - -import "vector" Data.Vector.Unboxed.Mutable as Exports - diff --git a/src/Data/Vector_LHAssumptions.hs b/src/Data/Vector_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/Data/Vector_LHAssumptions.hs @@ -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) + +@-}