liquid-vector (empty) → 0.12.1.2

raw patch · 25 files changed

+195/−0 lines, 25 filesdep +liquid-basedep +liquidhaskelldep +vectorbuild-type:Customsetup-changed

Dependencies added: liquid-base, liquidhaskell, vector

Files

• LICENSE +30/−0
• Setup.hs +6/−0
• liquid-vector.cabal +54/−0
• src/Data/Vector.hs +3/−0
• src/Data/Vector.spec +40/−0
• src/Data/Vector/Fusion/Bundle.hs +3/−0
• src/Data/Vector/Fusion/Bundle/Monadic.hs +3/−0
• src/Data/Vector/Fusion/Bundle/Size.hs +3/−0
• src/Data/Vector/Fusion/Stream/Monadic.hs +3/−0
• src/Data/Vector/Fusion/Util.hs +3/−0
• src/Data/Vector/Generic.hs +3/−0
• src/Data/Vector/Generic/Base.hs +3/−0
• src/Data/Vector/Generic/Mutable.hs +3/−0
• src/Data/Vector/Generic/Mutable/Base.hs +3/−0
• src/Data/Vector/Generic/New.hs +3/−0
• src/Data/Vector/Internal/Check.hs +3/−0
• src/Data/Vector/Mutable.hs +4/−0
• src/Data/Vector/Primitive.hs +3/−0
• src/Data/Vector/Primitive/Mutable.hs +3/−0
• src/Data/Vector/Storable.hs +3/−0
• src/Data/Vector/Storable/Internal.hs +3/−0
• src/Data/Vector/Storable/Mutable.hs +3/−0
• src/Data/Vector/Unboxed.hs +3/−0
• src/Data/Vector/Unboxed/Base.hs +3/−0
• src/Data/Vector/Unboxed/Mutable.hs +4/−0

@@ -0,0 +1,30 @@+Copyright (c) 2013-2014, Ranjit Jhala++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Ranjit Jhala nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,6 @@+module Main where++import Language.Haskell.Liquid.Cabal (liquidHaskellMain)++main :: IO ()+main = liquidHaskellMain

@@ -0,0 +1,54 @@+cabal-version:      1.24+name:               liquid-vector+version:            0.12.1.2+synopsis:           LiquidHaskell specs for the vector package+description:        LiquidHaskell specs for the vector package.+license:            BSD3+license-file:       LICENSE+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.+author:             Ranjit Jhala, Niki Vazou, Eric Seidel+maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>+category:           Language+homepage:           https://github.com/ucsd-progsys/liquidhaskell+build-type:         Custom++data-files:           src/Data/Vector.spec++custom-setup+  setup-depends: Cabal, base, liquidhaskell++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+  hs-source-dirs:     src+  build-depends:      liquid-base          < 4.15+                    , vector               >= 0.12.1.2 && < 0.13+                    , liquidhaskell        >= 0.8.10.1+  default-language:   Haskell2010+  default-extensions: PackageImports+  if impl(ghc >= 8.10)+    ghc-options: -fplugin=LiquidHaskell

@@ -0,0 +1,3 @@+module Data.Vector ( module Exports ) where++import "vector" Data.Vector as Exports

@@ -0,0 +1,40 @@+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) 

@@ -0,0 +1,3 @@+module Data.Vector.Fusion.Bundle (module Exports) where++import "vector" Data.Vector.Fusion.Bundle as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Fusion.Bundle.Monadic (module Exports) where++import "vector" Data.Vector.Fusion.Bundle.Monadic as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Fusion.Bundle.Size (module Exports) where++import "vector" Data.Vector.Fusion.Bundle.Size as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Fusion.Stream.Monadic (module Exports) where++import "vector" Data.Vector.Fusion.Stream.Monadic as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Fusion.Util (module Exports) where++import "vector" Data.Vector.Fusion.Util as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Generic (module Exports) where++import "vector" Data.Vector.Generic as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Generic.Base (module Exports) where++import "vector" Data.Vector.Generic.Base as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Generic.Mutable ( module Exports ) where++import "vector" Data.Vector.Generic.Mutable as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Generic.Mutable.Base (module Exports) where++import "vector" Data.Vector.Generic.Mutable.Base as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Generic.New (module Exports) where++import "vector" Data.Vector.Generic.New as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Internal.Check (module Exports) where++import "vector" Data.Vector.Internal.Check as Exports

@@ -0,0 +1,4 @@++module Data.Vector.Mutable (module Exports) where++import "vector" Data.Vector.Mutable as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Primitive (module Exports) where++import "vector" Data.Vector.Primitive as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Primitive.Mutable (module Exports) where++import "vector" Data.Vector.Primitive.Mutable as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Storable (module Exports) where++import "vector" Data.Vector.Storable as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Storable.Internal (module Exports) where++import "vector" Data.Vector.Storable.Internal as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Storable.Mutable (module Exports) where++import "vector" Data.Vector.Storable.Mutable as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Unboxed (module Exports) where++import "vector" Data.Vector.Unboxed as Exports

@@ -0,0 +1,3 @@+module Data.Vector.Unboxed.Base (module Exports) where++import "vector" Data.Vector.Unboxed.Base as Exports

@@ -0,0 +1,4 @@+module Data.Vector.Unboxed.Mutable (module Exports) where++import "vector" Data.Vector.Unboxed.Mutable as Exports+