liquid-bytestring (empty) → 0.10.10.0
raw patch · 25 files changed
+1674/−0 lines, 25 filesdep +bytestringdep +liquid-basedep +liquidhaskellbuild-type:Customsetup-changed
Dependencies added: bytestring, liquid-base, liquidhaskell
Files
- LICENSE +30/−0
- Setup.hs +6/−0
- liquid-bytestring.cabal +56/−0
- src/Data/ByteString.hs +4/−0
- src/Data/ByteString.spec +375/−0
- src/Data/ByteString/Builder.hs +3/−0
- src/Data/ByteString/Builder/Extra.hs +3/−0
- src/Data/ByteString/Builder/Internal.hs +3/−0
- src/Data/ByteString/Builder/Prim.hs +3/−0
- src/Data/ByteString/Builder/Prim/Internal.hs +3/−0
- src/Data/ByteString/Char8.hs +6/−0
- src/Data/ByteString/Char8.spec +402/−0
- src/Data/ByteString/Internal.hs +3/−0
- src/Data/ByteString/Lazy.hs +5/−0
- src/Data/ByteString/Lazy.spec +338/−0
- src/Data/ByteString/Lazy/Builder.hs +3/−0
- src/Data/ByteString/Lazy/Builder/ASCII.hs +3/−0
- src/Data/ByteString/Lazy/Builder/Extras.hs +3/−0
- src/Data/ByteString/Lazy/Char8.spec +355/−0
- src/Data/ByteString/Lazy/Internal.hs +3/−0
- src/Data/ByteString/Short.hs +5/−0
- src/Data/ByteString/Short.spec +25/−0
- src/Data/ByteString/Short/Internal.hs +3/−0
- src/Data/ByteString/Unsafe.hs +5/−0
- src/Data/ByteString/Unsafe.spec +29/−0
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,6 @@+module Main where++import Language.Haskell.Liquid.Cabal (liquidHaskellMain)++main :: IO ()+main = liquidHaskellMain
+ liquid-bytestring.cabal view
@@ -0,0 +1,56 @@+cabal-version: 1.24+name: liquid-bytestring+version: 0.10.10.0+synopsis: LiquidHaskell specs for the bytestring package+description: LiquidHaskell specs for the bytestring 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/ByteString.spec+ src/Data/ByteString/Short.spec+ src/Data/ByteString/Lazy.spec+ src/Data/ByteString/Unsafe.spec+ src/Data/ByteString/Char8.spec+ src/Data/ByteString/Lazy/Char8.spec++custom-setup+ setup-depends: Cabal, base, liquidhaskell++library+ exposed-modules: Data.ByteString+ Data.ByteString.Char8+ Data.ByteString.Unsafe+ Data.ByteString.Internal+ Data.ByteString.Lazy+ Data.ByteString.Lazy.Internal+ Data.ByteString.Short+ Data.ByteString.Short.Internal++ Data.ByteString.Builder+ Data.ByteString.Builder.Extra+ Data.ByteString.Builder.Prim++ Data.ByteString.Builder.Internal+ Data.ByteString.Builder.Prim.Internal+ Data.ByteString.Lazy.Builder+ Data.ByteString.Lazy.Builder.Extras+ Data.ByteString.Lazy.Builder.ASCII++ -- FIXME: This is commented out as unfortunately it doesn't refine+ -- correctly with modern versions of bytestring.+ -- Data.ByteString.Lazy.Char8++ hs-source-dirs: src+ build-depends: liquid-base < 5+ , bytestring >= 0.10.10.0 && < 0.11+ , liquidhaskell >= 0.8.10.1+ default-language: Haskell2010+ default-extensions: PackageImports+ if impl(ghc >= 8.10)+ ghc-options: -fplugin=LiquidHaskell
+ src/Data/ByteString.hs view
@@ -0,0 +1,4 @@+module Data.ByteString ( module Exports ) where++import Data.String+import "bytestring" Data.ByteString as Exports
+ src/Data/ByteString.spec view
@@ -0,0 +1,375 @@+module spec Data.ByteString where++import Data.String++measure bslen :: Data.ByteString.ByteString -> { n : Int | 0 <= n }++invariant { bs : Data.ByteString.ByteString | 0 <= bslen bs }++invariant { bs : Data.ByteString.ByteString | bslen bs == stringlen bs }++empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 }++singleton :: _ -> { bs : Data.ByteString.ByteString | bslen bs == 1 }++pack :: w8s : [_]+ -> { bs : Data.ByteString.ByteString | bslen bs == len w8s }++unpack :: bs : Data.ByteString.ByteString+ -> { w8s : [_] | len w8s == bslen bs }++cons :: _+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }++snoc :: i : Data.ByteString.ByteString+ -> _+ -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }++append :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen l + bslen r }++head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _++unsnoc :: i:Data.ByteString.ByteString + -> (Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, _))++last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _++tail :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _++init + :: {i:Data.ByteString.ByteString | 1 <= bslen i } + -> {o:Data.ByteString.ByteString | bslen o == bslen i - 1 }++null + :: bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | b <=> bslen bs == 0 }++length :: bs : Data.ByteString.ByteString -> { n : Int | bslen bs == n }++map + :: (_ -> _)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++reverse + :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++intersperse + :: _+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) }++intercalate + :: l : Data.ByteString.ByteString+ -> rs : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.ByteString | len rs == 0 ==> bslen o == 0 }++transpose + :: is : [Data.ByteString.ByteString]+ -> { os : [{ bs : Data.ByteString.ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0}++foldl1 + :: (_ -> _ -> _)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> _++foldl1' + :: (_ -> _ -> _)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> _++foldr1 + :: (_ -> _ -> _)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> _++foldr1' + :: (_ -> _ -> _)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> _++concat + :: is : [Data.ByteString.ByteString] + -> { o : Data.ByteString.ByteString | (len is == 0) ==> (bslen o == 0) }++concatMap + :: (_ -> Data.ByteString.ByteString)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 }++any + :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }++all + :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }++maximum :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _++minimum :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _++scanl :: (_ -> _ -> _)+ -> _+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++scanl1 :: (_ -> _ -> _)+ -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++scanr+ :: (_ -> _ -> _)+ -> _+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++scanr1+ :: (_ -> _ -> _)+ -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++mapAccumL+ :: (acc -> _ -> (acc, _))+ -> acc+ -> i : Data.ByteString.ByteString+ -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })++mapAccumR+ :: (acc -> _ -> (acc, _))+ -> acc+ -> i : Data.ByteString.ByteString+ -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })++replicate+ :: n : Int+ -> _+ -> { bs : Data.ByteString.ByteString | bslen bs == n }++unfoldrN+ :: n : Int+ -> (a -> Maybe (_, a))+ -> a+ -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a)++take+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == 0) &&+ ((0 <= n && n <= bslen i) <=> bslen o == n) &&+ (bslen i <= n <=> bslen o = bslen i) }++drop+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == bslen i) &&+ ((0 <= n && n <= bslen i) <=> bslen o == bslen i - n) &&+ (bslen i <= n <=> bslen o == 0) }++splitAt+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | (n <= 0 <=> bslen l == 0) &&+ ((0 <= n && n <= bslen i) <=> bslen l == n) &&+ (bslen i <= n <=> bslen l == bslen i) }+ , { r : Data.ByteString.ByteString | (n <= 0 <=> bslen r == bslen i) &&+ ((0 <= n && n <= bslen i) <=> bslen r == bslen i - n) &&+ (bslen i <= n <=> bslen r == 0) }+ )++takeWhile+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++dropWhile+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++span+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++spanEnd+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++break+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++breakEnd+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++group+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]++groupBy+ :: (_ -> _ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]++inits+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++tails+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++split+ :: _+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++splitWith+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++isPrefixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen l >= bslen r ==> not b }++isSuffixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }++isInfixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }++breakSubstring+ :: il : Data.ByteString.ByteString+ -> ir : Data.ByteString.ByteString+ -> ( { ol : Data.ByteString.ByteString | bslen ol <= bslen ir && (bslen il > bslen ir ==> bslen ol == bslen ir)}+ , { or : Data.ByteString.ByteString | bslen or <= bslen ir && (bslen il > bslen ir ==> bslen or == 0) }+ )++elem+ :: _+ -> bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }++notElem+ :: _+ -> bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }++find+ :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> (Maybe { w8 : _ | bslen bs /= 0 })++filter+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++partition+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++index :: bs : Data.ByteString.ByteString -> { n : Int | 0 <= n && n < bslen bs } -> _++elemIndex+ :: _+ -> bs : Data.ByteString.ByteString+ -> (Maybe { n : Int | 0 <= n && n < bslen bs })++elemIndices+ :: _+ -> bs : Data.ByteString.ByteString+ -> [{ n : Int | 0 <= n && n < bslen bs }]++elemIndexEnd+ :: _+ -> bs : Data.ByteString.ByteString+ -> (Maybe { n : Int | 0 <= n && n < bslen bs })++findIndex+ :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> (Maybe { n : Int | 0 <= n && n < bslen bs })++findIndices+ :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> [{ n : Int | 0 <= n && n < bslen bs }]++count+ :: _+ -> bs : Data.ByteString.ByteString+ -> { n : Int | 0 <= n && n < bslen bs }++zip+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : [(_, _)] | len o <= bslen l && len o <= bslen r }++zipWith+ :: (_ -> _ -> a)+ -> l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : [a] | len o <= bslen l && len o <= bslen r }++unzip+ :: i : [(_, _)]+ -> ( { l : Data.ByteString.ByteString | bslen l == len i }+ , { r : Data.ByteString.ByteString | bslen r == len i }+ )++sort+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++copy+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++hGet+ :: _+ -> n : { n : Int | 0 <= n }+ -> (IO { bs : Data.ByteString.ByteString | bslen bs == n || bslen bs == 0 })++hGetSome+ :: _+ -> n : { n : Int | 0 <= n }+ -> (IO { bs : Data.ByteString.ByteString | bslen bs <= n })++hGetNonBlocking+ :: _+ -> n : { n : Int | 0 <= n }+ -> (IO { bs : Data.ByteString.ByteString | bslen bs <= n })++uncons+ :: i : Data.ByteString.ByteString+ -> (Maybe (_, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 }))+
+ src/Data/ByteString/Builder.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Builder (module Exports) where++import "bytestring" Data.ByteString.Builder as Exports
+ src/Data/ByteString/Builder/Extra.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Builder.Extra (module Exports) where++import "bytestring" Data.ByteString.Builder.Extra as Exports
+ src/Data/ByteString/Builder/Internal.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Builder.Internal (module Exports) where++import "bytestring" Data.ByteString.Builder.Internal as Exports
+ src/Data/ByteString/Builder/Prim.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Builder.Prim (module Exports) where++import "bytestring" Data.ByteString.Builder.Prim as Exports
+ src/Data/ByteString/Builder/Prim/Internal.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Builder.Prim.Internal (module Exports) where++import "bytestring" Data.ByteString.Builder.Prim.Internal as Exports
+ src/Data/ByteString/Char8.hs view
@@ -0,0 +1,6 @@+module Data.ByteString.Char8 ( module Exports ) where++import Data.Int+import Data.ByteString+import GHC.IO.Handle+import "bytestring" Data.ByteString.Char8 as Exports
+ src/Data/ByteString/Char8.spec view
@@ -0,0 +1,402 @@+module spec Data.ByteString.Char8 where++import Data.ByteString ++assume empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 }++assume singleton+ :: Char -> { bs : Data.ByteString.ByteString | bslen bs == 1 }++assume pack+ :: w8s : [Char]+ -> { bs : Data.ByteString.ByteString | bslen bs == len w8s }++assume unpack+ :: bs : Data.ByteString.ByteString+ -> { w8s : [Char] | len w8s == bslen bs }++assume cons+ :: Char+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }++assume snoc+ :: i : Data.ByteString.ByteString+ -> Char+ -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }++assume append+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen l + bslen r }++head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Char++assume uncons+ :: i : Data.ByteString.ByteString+ -> Maybe (Char, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 })++assume unsnoc+ :: i : Data.ByteString.ByteString+ -> Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, Char)++assume last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Char++assume tail :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.ByteString.ByteString++assume init :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.ByteString.ByteString++assume null+ :: bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | b <=> bslen bs == 0 }++assume length :: bs : Data.ByteString.ByteString -> { n : Int | bslen bs == n }++assume map+ :: (Char -> Char)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++assume reverse+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++assume intersperse+ :: Char+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) }++assume intercalate+ :: l : Data.ByteString.ByteString+ -> rs : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.ByteString | len rs == 0 ==> bslen o == 0 }++assume transpose+ :: is : [Data.ByteString.ByteString]+ -> { os : [{ bs : Data.ByteString.ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0}++foldl1+ :: (Char -> Char -> Char)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> Char++foldl1'+ :: (Char -> Char -> Char)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> Char++foldr1+ :: (Char -> Char -> Char)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> Char++foldr1'+ :: (Char -> Char -> Char)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> Char++assume concat+ :: is : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.ByteString | len is == 0 ==> bslen o == 0 }++assume concatMap+ :: (Char -> Data.ByteString.ByteString)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 }++assume any :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }++assume all :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }++maximum+ :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Char++minimum+ :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Char++assume scanl+ :: (Char -> Char -> Char)+ -> Char+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++assume scanl1+ :: (Char -> Char -> Char)+ -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++assume scanr+ :: (Char -> Char -> Char)+ -> Char+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++assume scanr1+ :: (Char -> Char -> Char)+ -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++assume mapAccumL+ :: (acc -> Char -> (acc, Char))+ -> acc+ -> i : Data.ByteString.ByteString+ -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })++assume mapAccumR+ :: (acc -> Char -> (acc, Char))+ -> acc+ -> i : Data.ByteString.ByteString+ -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })++assume replicate+ :: n : Int+ -> Char+ -> { bs : Data.ByteString.ByteString | bslen bs == n }++assume unfoldrN+ :: n : Int+ -> (a -> Maybe (Char, a))+ -> a+ -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a)++assume take+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == 0) &&+ ((0 <= n && n <= bslen i) <=> bslen o == n) &&+ (bslen i <= n <=> bslen o = bslen i) }++assume drop+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == bslen i) &&+ ((0 <= n && n <= bslen i) <=> bslen o == bslen i - n) &&+ (bslen i <= n <=> bslen o == 0) }++assume splitAt+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | (n <= 0 <=> bslen l == 0) &&+ ((0 <= n && n <= bslen i) <=> bslen l == n) &&+ (bslen i <= n <=> bslen l == bslen i) }+ , { r : Data.ByteString.ByteString | (n <= 0 <=> bslen r == bslen i) &&+ ((0 <= n && n <= bslen i) <=> bslen r == bslen i - n) &&+ (bslen i <= n <=> bslen r == 0) }+ )++assume takeWhile+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++assume dropWhile+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++assume span+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++assume spanEnd+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++assume break+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++assume breakEnd+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++assume group+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]++assume groupBy+ :: (Char -> Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]++assume inits+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++assume tails+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++assume split+ :: Char+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++assume splitWith+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++assume lines+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++assume words+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++assume unlines+ :: is : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.ByteString | (len is == 0 <=> bslen o == 0) && bslen o >= len is }++assume unwords+ :: is : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.ByteString | (len is == 0 ==> bslen o == 0) && (1 <= len is ==> bslen o >= len is - 1) }++assume isPrefixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen l >= bslen r ==> not b }++assume isSuffixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }++assume isInfixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }++assume breakSubstring+ :: il : Data.ByteString.ByteString+ -> ir : Data.ByteString.ByteString+ -> ( { ol : Data.ByteString.ByteString | bslen ol <= bslen ir && (bslen il > bslen ir ==> bslen ol == bslen ir)}+ , { or : Data.ByteString.ByteString | bslen or <= bslen ir && (bslen il > bslen ir ==> bslen or == 0) }+ )++assume elem+ :: Char+ -> bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }++assume notElem+ :: Char+ -> bs : Data.ByteString.ByteString+ -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }++assume find+ :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> Maybe { w8 : Char | bslen bs /= 0 }++assume filter+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++index+ :: bs : Data.ByteString.ByteString+ -> { n : Int | 0 <= n && n < bslen bs }+ -> Char++assume elemIndex+ :: Char+ -> bs : Data.ByteString.ByteString+ -> Maybe { n : Int | 0 <= n && n < bslen bs }++assume elemIndices+ :: Char+ -> bs : Data.ByteString.ByteString+ -> [{ n : Int | 0 <= n && n < bslen bs }]++assume elemIndexEnd+ :: Char+ -> bs : Data.ByteString.ByteString+ -> Maybe { n : Int | 0 <= n && n < bslen bs }++assume findIndex+ :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> Maybe { n : Int | 0 <= n && n < bslen bs }++assume findIndices+ :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.ByteString+ -> [{ n : Int | 0 <= n && n < bslen bs }]++assume count+ :: Char+ -> bs : Data.ByteString.ByteString+ -> { n : Int | 0 <= n && n < bslen bs }++assume zip+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : [(Char, Char)] | len o <= bslen l && len o <= bslen r }++assume zipWith+ :: (Char -> Char -> a)+ -> l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : [a] | len o <= bslen l && len o <= bslen r }++assume unzip+ :: i : [(Char, Char)]+ -> ( { l : Data.ByteString.ByteString | bslen l == len i }+ , { r : Data.ByteString.ByteString | bslen r == len i }+ )++assume sort+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++assume readInt+ :: i : Data.ByteString.ByteString+ -> Maybe { p : (Int, { o : Data.ByteString.ByteString | bslen o < bslen i}) | bslen i /= 0 }++assume readInteger+ :: i : Data.ByteString.ByteString+ -> Maybe { p : (Integer, { o : Data.ByteString.ByteString | bslen o < bslen i}) | bslen i /= 0 }++assume copy+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++assume hGet+ :: GHC.IO.Handle+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.ByteString | bslen bs == n || bslen bs == 0 }++assume hGetSome+ :: GHC.IO.Handle+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.ByteString | bslen bs <= n }++assume hGetNonBlocking+ :: GHC.IO.Handle+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.ByteString | bslen bs <= n }++// assume partition+ // :: (Char -> GHC.Types.Bool)+ // -> i : Data.ByteString.ByteString+ // -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ // , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ // )
+ src/Data/ByteString/Internal.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Internal (module Exports) where++import "bytestring" Data.ByteString.Internal as Exports
+ src/Data/ByteString/Lazy.hs view
@@ -0,0 +1,5 @@+module Data.ByteString.Lazy ( module Exports ) where++import Data.String+import Data.ByteString+import "bytestring" Data.ByteString.Lazy as Exports
+ src/Data/ByteString/Lazy.spec view
@@ -0,0 +1,338 @@+module spec Data.ByteString.Lazy where++import Data.String+import Data.ByteString++measure bllen :: Data.ByteString.Lazy.ByteString -> { n : GHC.Int.Int64 | 0 <= n }++invariant { bs : Data.ByteString.Lazy.ByteString | 0 <= bllen bs }++invariant { bs : Data.ByteString.Lazy.ByteString | bllen bs == stringlen bs }++assume empty :: { bs : Data.ByteString.Lazy.ByteString | bllen bs == 0 }++assume singleton+ :: _ -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == 1 }++assume pack+ :: w8s : [_]+ -> { bs : _ | bllen bs == len w8s }++assume unpack+ :: bs : Data.ByteString.Lazy.ByteString+ -> { w8s : [_] | len w8s == bllen bs }++assume fromStrict+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bslen i }++assume toStrict+ :: i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bllen i }++assume fromChunks+ :: i : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.Lazy.ByteString | len i == 0 <=> bllen o == 0 }++assume toChunks+ :: i : Data.ByteString.Lazy.ByteString+ -> { os : [{ o : Data.ByteString.ByteString | bslen o <= bllen i}] | len os == 0 <=> bllen i == 0 }++assume cons+ :: _+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }++assume snoc+ :: i : Data.ByteString.Lazy.ByteString+ -> _+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }++assume append+ :: l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen l + bllen r }++assume head+ :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> _++assume uncons+ :: i : Data.ByteString.Lazy.ByteString+ -> Maybe (_, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 })++assume unsnoc+ :: i : Data.ByteString.Lazy.ByteString+ -> Maybe ({ o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }, _)++assume last :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _++assume tail :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _++assume init :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _++assume null :: bs : Data.ByteString.Lazy.ByteString -> { b : GHC.Types.Bool | b <=> bllen bs == 0 }++assume length+ :: bs : Data.ByteString.Lazy.ByteString -> { n : GHC.Int.Int64 | bllen bs == n }++assume map+ :: (_ -> _)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume reverse+ :: i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume intersperse+ :: _+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) }++assume intercalate+ :: l : Data.ByteString.Lazy.ByteString+ -> rs : [Data.ByteString.Lazy.ByteString]+ -> { o : Data.ByteString.Lazy.ByteString | len rs == 0 ==> bllen o == 0 }++assume transpose+ :: is : [Data.ByteString.Lazy.ByteString]+ -> { os : [{ bs : Data.ByteString.Lazy.ByteString | bllen bs <= len is }] | len is == 0 ==> len os == 0}++assume foldl1+ :: (_ -> _ -> _)+ -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> _++assume foldl1'+ :: (_ -> _ -> _)+ -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> _++assume foldr1+ :: (_ -> _ -> _)+ -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> _++assume concat+ :: is : [Data.ByteString.Lazy.ByteString]+ -> { o : Data.ByteString.Lazy.ByteString | (len is == 0) ==> (bllen o == 0) }++assume concatMap+ :: (_ -> Data.ByteString.Lazy.ByteString)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen i == 0 ==> bllen o == 0 }++assume any :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b }++assume all :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen bs == 0 ==> b }++assume maximum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _++assume minimum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _++assume scanl+ :: (_ -> _ -> _)+ -> _+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume mapAccumL+ :: (acc -> _ -> (acc, _))+ -> acc+ -> i : Data.ByteString.Lazy.ByteString+ -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })++assume mapAccumR+ :: (acc -> _ -> (acc, _))+ -> acc+ -> i : Data.ByteString.Lazy.ByteString+ -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })++assume replicate+ :: n : GHC.Int.Int64+ -> _+ -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n }++assume take+ :: n : GHC.Int.Int64+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 ==> bllen o == 0) &&+ ((0 <= n && n <= bllen i) <=> bllen o == n) &&+ (bllen i <= n <=> bllen o = bllen i) }++assume drop+ :: n : GHC.Int.Int64+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen o == bllen i) &&+ ((0 <= n && n <= bllen i) <=> bllen o == bllen i - n) &&+ (bllen i <= n <=> bllen o == 0) }++assume splitAt+ :: n : GHC.Int.Int64+ -> i : Data.ByteString.Lazy.ByteString+ -> ( { l : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen l == 0) &&+ ((0 <= n && n <= bllen i) <=> bllen l == n) &&+ (bllen i <= n <=> bllen l == bllen i) }+ , { r : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen r == bllen i) &&+ ((0 <= n && n <= bllen i) <=> bllen r == bllen i - n) &&+ (bllen i <= n <=> bllen r == 0) }+ )++assume takeWhile+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }++assume dropWhile+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }++assume span+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }+ , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }+ )++assume break+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }+ , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }+ )++assume group+ :: i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]++assume groupBy+ :: (_ -> _ -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]++assume inits+ :: i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume tails+ :: i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume split+ :: _+ -> i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume splitWith+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume isPrefixOf+ :: l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }++assume isSuffixOf+ :: l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }++assume elem+ :: _+ -> bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | (bllen bs == 0) ==> not b }++assume notElem+ :: _+ -> bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | (bllen bs == 0) ==> b }++assume find+ :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> Maybe { w8 : _ | bllen bs /= 0 }++assume filter+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }++assume partition+ :: (_ -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }+ , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }+ )++assume index+ :: bs : Data.ByteString.Lazy.ByteString+ -> { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }+ -> _++assume elemIndex+ :: _+ -> bs : Data.ByteString.Lazy.ByteString+ -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }++assume elemIndices+ :: _+ -> bs : Data.ByteString.Lazy.ByteString+ -> [{ n : GHC.Int.Int64 | 0 <= n && n < bllen bs }]++assume elemIndexEnd+ :: _+ -> bs : Data.ByteString.Lazy.ByteString+ -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }++assume findIndex+ :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }++assume findIndices+ :: (_ -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> [{ n : GHC.Int.Int64 | 0 <= n && n < bllen bs }]++assume count+ :: _+ -> bs : Data.ByteString.Lazy.ByteString+ -> { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }++assume zip+ :: l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { o : [(_, _)] | len o <= bllen l && len o <= bllen r }++assume zipWith+ :: (_ -> _ -> a)+ -> l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { o : [a] | len o <= bllen l && len o <= bllen r }++assume unzip+ :: i : [(_, _)]+ -> ( { l : Data.ByteString.Lazy.ByteString | bllen l == len i }+ , { r : Data.ByteString.Lazy.ByteString | bllen r == len i }+ )++assume copy+ :: i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume hGet+ :: _+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs == n || bllen bs == 0 }++assume hGetNonBlocking+ :: _+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs <= n }
+ src/Data/ByteString/Lazy/Builder.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Lazy.Builder (module Exports) where++import "bytestring" Data.ByteString.Lazy.Builder as Exports
+ src/Data/ByteString/Lazy/Builder/ASCII.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Lazy.Builder.ASCII (module Exports) where++import "bytestring" Data.ByteString.Lazy.Builder.ASCII as Exports
+ src/Data/ByteString/Lazy/Builder/Extras.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Lazy.Builder.Extras (module Exports) where++import "bytestring" Data.ByteString.Lazy.Builder.Extras as Exports
+ src/Data/ByteString/Lazy/Char8.spec view
@@ -0,0 +1,355 @@+module spec Data.ByteString.Lazy.Char8 where++last :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> Char++assume empty :: { bs : Data.ByteString.Lazy.ByteString | bllen bs == 0 }++assume singleton+ :: Char -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == 1 }++assume pack+ :: w8s : [Char]+ -> { bs : Data.ByteString.ByteString | bllen bs == len w8s }++assume unpack+ :: bs : Data.ByteString.Lazy.ByteString+ -> { w8s : [Char] | len w8s == bllen bs }++assume fromStrict+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bslen i }++assume toStrict+ :: i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bllen i }++assume fromChunks+ :: i : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.Lazy.ByteString | len i == 0 <=> bllen o == 0 }++assume toChunks+ :: i : Data.ByteString.Lazy.ByteString+ -> { os : [{ o : Data.ByteString.ByteString | bslen o <= bllen i}] | len os == 0 <=> bllen i == 0 }++assume cons+ :: Char+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }++assume snoc+ :: i : Data.ByteString.Lazy.ByteString+ -> Char+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }++assume append+ :: l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen l + bllen r }++head+ :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> Char++assume uncons+ :: i : Data.ByteString.Lazy.ByteString+ -> Maybe (Char, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 })++assume unsnoc+ :: i : Data.ByteString.Lazy.ByteString+ -> Maybe ({ o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }, Char)++assume null+ :: bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | b <=> bllen bs == 0 }++assume length+ :: bs : Data.ByteString.Lazy.ByteString -> { n : Int64 | bllen bs == n }++assume map+ :: (Char -> Char)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume reverse+ :: i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume intersperse+ :: Char+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) }++assume intercalate+ :: l : Data.ByteString.Lazy.ByteString+ -> rs : [Data.ByteString.Lazy.ByteString]+ -> { o : Data.ByteString.Lazy.ByteString | len rs == 0 ==> bllen o == 0 }++assume transpose+ :: is : [Data.ByteString.Lazy.ByteString]+ -> { os : [{ bs : Data.ByteString.Lazy.ByteString | bllen bs <= len is }] | len is == 0 ==> len os == 0}++foldl1+ :: (Char -> Char -> Char)+ -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> Char++foldl1'+ :: (Char -> Char -> Char)+ -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> Char++foldr1+ :: (Char -> Char -> Char)+ -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> Char++assume concat+ :: is : [Data.ByteString.Lazy.ByteString]+ -> { o : Data.ByteString.Lazy.ByteString | len is == 0 ==> bllen o }++assume concatMap+ :: (Char -> Data.ByteString.Lazy.ByteString)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen i == 0 ==> bllen o == 0 }++assume any :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b }++assume all :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen bs == 0 ==> b }++maximum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> Char++minimum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> Char++assume scanl+ :: (Char -> Char -> Char)+ -> Char+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume scanl1+ :: (Char -> Char -> Char)+ -> i : { i : Data.ByteString.Lazy.ByteString | 1 <= bllen i }+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume scanr+ :: (Char -> Char -> Char)+ -> Char+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume scanr1+ :: (Char -> Char -> Char)+ -> i : { i : Data.ByteString.Lazy.ByteString | 1 <= bllen i }+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume mapAccumL+ :: (acc -> Char -> (acc, Char))+ -> acc+ -> i : Data.ByteString.Lazy.ByteString+ -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })++assume mapAccumR+ :: (acc -> Char -> (acc, Char))+ -> acc+ -> i : Data.ByteString.Lazy.ByteString+ -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })++assume replicate+ :: n : Int64+ -> Char+ -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n }++assume take+ :: n : Int64+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 ==> bllen o == 0) &&+ ((0 <= n && n <= bllen i) <=> bllen o == n) &&+ (bllen i <= n <=> bllen o = bllen i) }++assume drop+ :: n : Int64+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen o == bllen i) &&+ ((0 <= n && n <= bllen i) <=> bllen o == bllen i - n) &&+ (bllen i <= n <=> bllen o == 0) }++assume splitAt+ :: n : Int64+ -> i : Data.ByteString.Lazy.ByteString+ -> ( { l : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen l == 0) &&+ ((0 <= n && n <= bllen i) <=> bllen l == n) &&+ (bllen i <= n <=> bllen l == bllen i) }+ , { r : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen r == bllen i) &&+ ((0 <= n && n <= bllen i) <=> bllen r == bllen i - n) &&+ (bllen i <= n <=> bllen r == 0) }+ )++assume takeWhile+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }++assume dropWhile+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }++assume span+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }+ , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }+ )++assume break+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }+ , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }+ )++assume group+ :: i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]++assume groupBy+ :: (Char -> Char -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]++assume inits+ :: i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume tails+ :: i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume split+ :: Char+ -> i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume splitWith+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume lines+ :: i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume words+ :: i : Data.ByteString.Lazy.ByteString+ -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]++assume unlines+ :: is : [Data.ByteString.Lazy.ByteString]+ -> { o : Data.ByteString.Lazy.ByteString | (len is == 0 <=> bllen o == 0) && bllen o >= len is }++assume unwords+ :: is : [Data.ByteString.Lazy.ByteString]+ -> { o : Data.ByteString.Lazy.ByteString | (len is == 0 ==> bllen o == 0) && (1 <= len is ==> bllen o >= len is - 1) }++assume isPrefixOf+ :: l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }++assume isSuffixOf+ :: l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }++assume elem+ :: Char+ -> bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen b == 0 ==> not b }++assume notElem+ :: Char+ -> bs : Data.ByteString.Lazy.ByteString+ -> { b : GHC.Types.Bool | bllen b == 0 ==> b }++assume find+ :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> Maybe { w8 : Char | bllen bs /= 0 }++assume filter+ :: (Char -> GHC.Types.Bool)+ -> i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }++index+ :: bs : Data.ByteString.Lazy.ByteString+ -> { n : Int64 | 0 <= n && n < bllen bs }+ -> Char++assume elemIndex+ :: Char+ -> bs : Data.ByteString.Lazy.ByteString+ -> Maybe { n : Int64 | 0 <= n && n < bllen bs }++assume elemIndices+ :: Char+ -> bs : Data.ByteString.Lazy.ByteString+ -> [{ n : Int64 | 0 <= n && n < bllen bs }]++assume findIndex+ :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> Maybe { n : Int64 | 0 <= n && n < bllen bs }++assume findIndices+ :: (Char -> GHC.Types.Bool)+ -> bs : Data.ByteString.Lazy.ByteString+ -> [{ n : Int64 | 0 <= n && n < bllen bs }]++assume count+ :: Char+ -> bs : Data.ByteString.Lazy.ByteString+ -> { n : Int64 | 0 <= n && n < bllen bs }++assume zip+ :: l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { o : [(Char, Char)] | len o <= bllen l && len o <= bllen r }++assume zipWith+ :: (Char -> Char -> a)+ -> l : Data.ByteString.Lazy.ByteString+ -> r : Data.ByteString.Lazy.ByteString+ -> { o : [a] | len o <= bllen l && len o <= bllen r }++assume unzip+ :: i : [(Char, Char)]+ -> ( { l : Data.ByteString.Lazy.ByteString | bllen l == len i }+ , { r : Data.ByteString.Lazy.ByteString | bllen r == len i }+ )++assume readInt+ :: i : Data.ByteString.Lazy.ByteString+ -> Maybe { p : (Int, { o : Data.ByteString.Lazy.ByteString | bllen o < bllen i}) | bllen i /= 0 }++assume readInteger+ :: i : Data.ByteString.Lazy.ByteString+ -> Maybe { p : (Integer, { o : Data.ByteString.Lazy.ByteString | bllen o < bllen i}) | bllen i /= 0 }++assume copy+ :: i : Data.ByteString.Lazy.ByteString+ -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }++assume hGet+ :: GHC.IO.Handle+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs == n || bllen bs == 0 }++assume hGetNonBlocking+ :: GHC.IO.Handle+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs <= n }
+ src/Data/ByteString/Lazy/Internal.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Lazy.Internal (module Exports) where++import "bytestring" Data.ByteString.Lazy.Internal as Exports
+ src/Data/ByteString/Short.hs view
@@ -0,0 +1,5 @@+module Data.ByteString.Short ( module Exports ) where++import Data.ByteString+import Data.Word+import "bytestring" Data.ByteString.Short as Exports
+ src/Data/ByteString/Short.spec view
@@ -0,0 +1,25 @@+module spec Data.ByteString.Short where++import Data.String++measure sbslen :: Data.ByteString.Short.ShortByteString -> { n : Int | 0 <= n }++invariant { bs : Data.ByteString.Short.ShortByteString | 0 <= sbslen bs }++invariant { bs : Data.ByteString.Short.ShortByteString | sbslen bs == stringlen bs }++toShort :: i : Data.ByteString.ByteString -> { o : Data.ByteString.Short.ShortByteString | sbslen o == bslen i }++fromShort :: o : Data.ByteString.Short.ShortByteString -> { i : Data.ByteString.ByteString | bslen i == sbslen o }++pack :: w8s : [Word8] -> { bs : Data.ByteString.Short.ShortByteString | sbslen bs == len w8s }++unpack :: bs : Data.ByteString.Short.ShortByteString -> { w8s : [Word8] | len w8s == sbslen bs }++empty :: { bs : Data.ByteString.Short.ShortByteString | sbslen bs == 0 }++null :: bs : Data.ByteString.Short.ShortByteString -> { b : GHC.Types.Bool | b <=> sbslen bs == 0 }++length :: bs : Data.ByteString.Short.ShortByteString -> { n : Int | sbslen bs == n }++index :: bs : Data.ByteString.Short.ShortByteString -> { n : Int | 0 <= n && n < sbslen bs } -> Word8
+ src/Data/ByteString/Short/Internal.hs view
@@ -0,0 +1,3 @@+module Data.ByteString.Short.Internal (module Exports) where++import "bytestring" Data.ByteString.Short.Internal as Exports
+ src/Data/ByteString/Unsafe.hs view
@@ -0,0 +1,5 @@+module Data.ByteString.Unsafe ( module Exports ) where++import Data.ByteString+import Data.Word+import "bytestring" Data.ByteString.Unsafe as Exports
+ src/Data/ByteString/Unsafe.spec view
@@ -0,0 +1,29 @@+module spec Data.ByteString.Unsafe where++unsafeHead+ :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ ++unsafeTail+ :: bs : { v : Data.ByteString.ByteString | bslen v > 0 }+ -> { v : Data.ByteString.ByteString | bslen v = bslen bs - 1 }++unsafeInit+ :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ ++unsafeLast+ :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ ++unsafeIndex+ :: bs : Data.ByteString.ByteString+ -> { n : Int | 0 <= n && n < bslen bs }+ -> _ ++unsafeTake+ :: n : { n : Int | 0 <= n }+ -> i : { i : Data.ByteString.ByteString | n <= bslen i }+ -> { o : Data.ByteString.ByteString | bslen o == n }++unsafeDrop+ :: n : { n : Int | 0 <= n }+ -> i : { i : Data.ByteString.ByteString | n <= bslen i }+ -> { o : Data.ByteString.ByteString | bslen o == bslen i - n }