liquidhaskell 0.9.10.1 → 0.9.10.1.2
raw patch · 50 files changed
+1060/−1016 lines, 50 filesdep −ghc-bignumdep −ghc-internaldep ~liquidhaskell-bootPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies removed: ghc-bignum, ghc-internal
Dependency ranges changed: liquidhaskell-boot
API changes (from Hackage documentation)
- GHC.Internal.Float_LHAssumptions: (**) :: Floating a => a -> a -> a
- GHC.Internal.Float_LHAssumptions: acos :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: acosh :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: asin :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: asinh :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: atan :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: atanh :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: class Fractional a => Floating a
- GHC.Internal.Float_LHAssumptions: cos :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: cosh :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: exp :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: infixr 8 **
- GHC.Internal.Float_LHAssumptions: log :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: logBase :: Floating a => a -> a -> a
- GHC.Internal.Float_LHAssumptions: pi :: Floating a => a
- GHC.Internal.Float_LHAssumptions: sin :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: sinh :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: sqrt :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: tan :: Floating a => a -> a
- GHC.Internal.Float_LHAssumptions: tanh :: Floating a => a -> a
+ GHC.Base_LHAssumptions: comp :: (b -> c) -> (a -> b) -> a -> c
+ GHC.Float_LHAssumptions: (**) :: Floating a => a -> a -> a
+ GHC.Float_LHAssumptions: acos :: Floating a => a -> a
+ GHC.Float_LHAssumptions: acosh :: Floating a => a -> a
+ GHC.Float_LHAssumptions: asin :: Floating a => a -> a
+ GHC.Float_LHAssumptions: asinh :: Floating a => a -> a
+ GHC.Float_LHAssumptions: atan :: Floating a => a -> a
+ GHC.Float_LHAssumptions: atanh :: Floating a => a -> a
+ GHC.Float_LHAssumptions: class Fractional a => Floating a
+ GHC.Float_LHAssumptions: cos :: Floating a => a -> a
+ GHC.Float_LHAssumptions: cosh :: Floating a => a -> a
+ GHC.Float_LHAssumptions: exp :: Floating a => a -> a
+ GHC.Float_LHAssumptions: expm1 :: Floating a => a -> a
+ GHC.Float_LHAssumptions: infixr 8 **
+ GHC.Float_LHAssumptions: log :: Floating a => a -> a
+ GHC.Float_LHAssumptions: log1mexp :: Floating a => a -> a
+ GHC.Float_LHAssumptions: log1p :: Floating a => a -> a
+ GHC.Float_LHAssumptions: log1pexp :: Floating a => a -> a
+ GHC.Float_LHAssumptions: logBase :: Floating a => a -> a -> a
+ GHC.Float_LHAssumptions: pi :: Floating a => a
+ GHC.Float_LHAssumptions: sin :: Floating a => a -> a
+ GHC.Float_LHAssumptions: sinh :: Floating a => a -> a
+ GHC.Float_LHAssumptions: sqrt :: Floating a => a -> a
+ GHC.Float_LHAssumptions: tan :: Floating a => a -> a
+ GHC.Float_LHAssumptions: tanh :: Floating a => a -> a
Files
- CHANGES.md +30/−0
- README.md +5/−1
- liquidhaskell.cabal +3/−12
- src/Data/ByteString/Char8_LHAssumptions.hs +97/−96
- src/Data/ByteString/Lazy/Char8_LHAssumptions.hs +137/−136
- src/Data/ByteString/Lazy_LHAssumptions.hs +154/−153
- src/Data/ByteString/Short_LHAssumptions.hs +13/−12
- src/Data/ByteString/Unsafe_LHAssumptions.hs +11/−10
- src/Data/ByteString_LHAssumptions.hs +159/−159
- src/Data/Either_LHAssumptions.hs +2/−1
- src/Data/Foldable_LHAssumptions.hs +9/−1
- src/Data/List_LHAssumptions.hs +9/−0
- src/Data/Maybe_LHAssumptions.hs +17/−1
- src/Data/Set_LHAssumptions.hs +36/−43
- src/Data/String_LHAssumptions.hs +4/−4
- src/Data/Tuple_LHAssumptions.hs +2/−2
- src/Data/Word_LHAssumptions.hs +1/−1
- src/Foreign/C/String_LHAssumptions.hs +5/−5
- src/Foreign/C/Types_LHAssumptions.hs +5/−3
- src/Foreign/Concurrent_LHAssumptions.hs +1/−1
- src/Foreign/ForeignPtr_LHAssumptions.hs +5/−4
- src/Foreign/Marshal/Alloc_LHAssumptions.hs +1/−1
- src/Foreign/Ptr_LHAssumptions.hs +5/−2
- src/Foreign/Storable_LHAssumptions.hs +15/−14
- src/GHC/Base_LHAssumptions.hs +61/−1
- src/GHC/CString_LHAssumptions.hs +6/−4
- src/GHC/Classes_LHAssumptions.hs +26/−25
- src/GHC/Exts_LHAssumptions.hs +8/−7
- src/GHC/Float_LHAssumptions.hs +28/−2
- src/GHC/ForeignPtr_LHAssumptions.hs +6/−5
- src/GHC/IO/Handle_LHAssumptions.hs +7/−6
- src/GHC/Int_LHAssumptions.hs +5/−5
- src/GHC/Internal/Base_LHAssumptions.hs +0/−55
- src/GHC/Internal/Data/Foldable_LHAssumptions.hs +0/−9
- src/GHC/Internal/Data/Maybe_LHAssumptions.hs +0/−21
- src/GHC/Internal/Float_LHAssumptions.hs +0/−28
- src/GHC/Internal/Int_LHAssumptions.hs +0/−10
- src/GHC/Internal/List_LHAssumptions.hs +0/−70
- src/GHC/Internal/Num_LHAssumptions.hs +0/−17
- src/GHC/Internal/Word_LHAssumptions.hs +0/−13
- src/GHC/List_LHAssumptions.hs +66/−1
- src/GHC/Num/Integer_LHAssumptions.hs +3/−3
- src/GHC/Num_LHAssumptions.hs +16/−1
- src/GHC/Ptr_LHAssumptions.hs +9/−9
- src/GHC/Real_LHAssumptions.hs +28/−17
- src/GHC/Types_LHAssumptions.hs +37/−32
- src/GHC/Word_LHAssumptions.hs +13/−1
- src/Liquid/Prelude/Real_LHAssumptions.hs +2/−3
- src/Liquid/Prelude/Totality_LHAssumptions.hs +6/−5
- src/Prelude_LHAssumptions.hs +7/−4
CHANGES.md view
@@ -2,6 +2,36 @@ ## Next +## 0.9.10.1.2 (2025-03-06)++- Implement opaque reflection, a feature to allow reflecting functions which+ call to non-reflected functions [#2323](https://github.com/ucsd-progsys/liquidhaskell/pull/2323).+- Implement reflection from interface files, which can reflect functions from+ their unfoldings [#2326](https://github.com/ucsd-progsys/liquidhaskell/pull/2326).+ The feature is limited at the moment by the constraints that affect reflecting+ functions in general. But we hope it becomes more interesting as reflection is+ made more flexible.+- Operators in the logic cannot be shadowed locally anymore since+ [#2327](https://github.com/ucsd-progsys/liquidhaskell/pull/2327).+- Added a flag `--dump-pre-normalized-core` to show core before A normalization+ and constraint generation [#2336](https://github.com/ucsd-progsys/liquidhaskell/pull/2336).+- Augmented the context of error messages [#2350](https://github.com/ucsd-progsys/liquidhaskell/pull/2350).+- Add a new flag `--etabeta` to reason with lambdas in PLE [#2356](https://github.com/ucsd-progsys/liquidhaskell/pull/2356)+- Add a new flag `--dependentcase` to expand support for higher-order reasoning [#2384](https://github.com/ucsd-progsys/liquidhaskell/pull/2384)+- Add support for reflecting lambda expressions [#2465](https://github.com/ucsd-progsys/liquidhaskell/pull/2465).+- Enabling the LiquidHaskell plugin now enables `-fno-ignore-interface-pragmas` ([#2326](https://github.com/ucsd-progsys/liquidhaskell/pull/2326))+ and `-dkeep-comments` ([#2367](https://github.com/ucsd-progsys/liquidhaskell/pull/2367)).+- LiquidHaskell earned a new `--minimal` verbosity level as default that prints the banner with the+ amount of constraints checked ([#2395](https://github.com/ucsd-progsys/liquidhaskell/pull/2395)).+ This banner is now suppressed when the verbosity is set to `--quiet` ([#2391](https://github.com/ucsd-progsys/liquidhaskell/pull/2391)).+- Avoid reparsing and retypechecking when verifying modules [#2389](https://github.com/ucsd-progsys/liquidhaskell/pull/2389).+- Name resolution is done only when verifying a module. It is no longer done when+ importing it [#2169](https://github.com/ucsd-progsys/liquidhaskell/issues/2169). One+ side effect of this change is that LH can now pick up names in scope using import aliases+ in most places (but see [#2481](https://github.com/ucsd-progsys/liquidhaskell/issues/2481)).+- Allow to link Haskell definitions with logical primitives via `define` declarations [#2463](https://github.com/ucsd-progsys/liquidhaskell/pull/2463).+- CVC5 solver is now supported for all logical theories, including Sets/Bags [#2483](https://github.com/ucsd-progsys/liquidhaskell/pull/2483)+ ## 0.9.10.1 (2024-08-21) - Add support for GHC 9.10.1.
README.md view
@@ -98,7 +98,11 @@ $ cabal build tests:unit-neg --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination -Or your favorite number of threads, depending on cores etc.+Another useful option is to change the underlying solver:++ $ cabal build tests:unit-pos --ghc-options=-fplugin-opt=LiquidHaskell:--smtsolver=cvc5++You can also modify the number of used threads, depending on cores etc. You can directly extend and run the tests by modifying the files in
liquidhaskell.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-version: 0.9.10.1+version: 0.9.10.1.2 synopsis: Liquid Types for Haskell description: Liquid Types for Haskell. license: BSD-3-Clause@@ -37,6 +37,7 @@ Data.Bits_LHAssumptions Data.Either_LHAssumptions Data.Foldable_LHAssumptions+ Data.List_LHAssumptions Data.Maybe_LHAssumptions Data.String_LHAssumptions Data.Tuple_LHAssumptions@@ -54,14 +55,6 @@ GHC.ForeignPtr_LHAssumptions GHC.Int_LHAssumptions GHC.IO.Handle_LHAssumptions- GHC.Internal.Base_LHAssumptions- GHC.Internal.Data.Foldable_LHAssumptions- GHC.Internal.Data.Maybe_LHAssumptions- GHC.Internal.Float_LHAssumptions- GHC.Internal.Int_LHAssumptions- GHC.Internal.List_LHAssumptions- GHC.Internal.Num_LHAssumptions- GHC.Internal.Word_LHAssumptions GHC.List_LHAssumptions GHC.Num_LHAssumptions GHC.Num.Integer_LHAssumptions@@ -85,11 +78,9 @@ hs-source-dirs: src build-depends: base >= 4.11.1.0 && < 5,- liquidhaskell-boot == 0.9.10.1,+ liquidhaskell-boot == 0.9.10.1.2, bytestring == 0.12.1.0, containers == 0.7,- ghc-bignum,- ghc-internal, ghc-prim default-language: Haskell98 ghc-options: -Wall
src/Data/ByteString/Char8_LHAssumptions.hs view
@@ -5,282 +5,283 @@ import Data.ByteString_LHAssumptions() import Data.ByteString import Data.ByteString.Char8+import GHC.Types {-@ assume Data.ByteString.Char8.singleton- :: GHC.Types.Char -> { bs : Data.ByteString.ByteString | bslen bs == 1 }+ :: GHC.Types.Char -> { bs : ByteString | bslen bs == 1 } assume Data.ByteString.Char8.pack :: w8s : [GHC.Types.Char]- -> { bs : Data.ByteString.ByteString | bslen bs == len w8s }+ -> { bs : ByteString | bslen bs == len w8s } assume Data.ByteString.Char8.unpack- :: bs : Data.ByteString.ByteString+ :: bs : ByteString -> { w8s : [GHC.Types.Char] | len w8s == bslen bs } assume Data.ByteString.Char8.cons :: GHC.Types.Char- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }+ -> i : ByteString+ -> { o : ByteString | bslen o == bslen i + 1 } assume Data.ByteString.Char8.snoc- :: i : Data.ByteString.ByteString+ :: i : ByteString -> GHC.Types.Char- -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }+ -> { o : ByteString | bslen o == bslen i + 1 } -assume Data.ByteString.Char8.head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> GHC.Types.Char+assume Data.ByteString.Char8.head :: { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.uncons- :: i : Data.ByteString.ByteString- -> Maybe (GHC.Types.Char, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 })+ :: i : ByteString+ -> Maybe (GHC.Types.Char, { o : ByteString | bslen o == bslen i - 1 }) assume Data.ByteString.Char8.unsnoc- :: i : Data.ByteString.ByteString- -> Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, GHC.Types.Char)+ :: i : ByteString+ -> Maybe ({ o : ByteString | bslen o == bslen i - 1 }, GHC.Types.Char) -assume Data.ByteString.Char8.last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> GHC.Types.Char+assume Data.ByteString.Char8.last :: { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.map :: (GHC.Types.Char -> GHC.Types.Char)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.intersperse :: GHC.Types.Char- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) }+ -> i : ByteString+ -> { o : ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) } assume Data.ByteString.Char8.foldl1 :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> { bs : ByteString | 1 <= bslen bs } -> Char assume Data.ByteString.Char8.foldl1' :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.foldr1 :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> { bs : ByteString | 1 <= bslen bs } -> Char assume Data.ByteString.Char8.foldr1' :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.concatMap- :: (GHC.Types.Char -> Data.ByteString.ByteString)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 }+ :: (GHC.Types.Char -> ByteString)+ -> i : ByteString+ -> { o : ByteString | bslen i == 0 ==> bslen o == 0 } assume Data.ByteString.Char8.any :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b } assume Data.ByteString.Char8.all :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> { b : GHC.Types.Bool | bslen bs == 0 ==> b } assume Data.ByteString.Char8.maximum- :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> GHC.Types.Char+ :: { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.minimum- :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> GHC.Types.Char+ :: { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.scanl :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) -> GHC.Types.Char- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.scanl1 :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : { i : ByteString | 1 <= bslen i }+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.scanr :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) -> GHC.Types.Char- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.scanr1 :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : { i : ByteString | 1 <= bslen i }+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.mapAccumL :: (acc -> GHC.Types.Char -> (acc, GHC.Types.Char)) -> acc- -> i : Data.ByteString.ByteString- -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })+ -> i : ByteString+ -> (acc, { o : ByteString | bslen o == bslen i }) assume Data.ByteString.Char8.mapAccumR :: (acc -> GHC.Types.Char -> (acc, GHC.Types.Char)) -> acc- -> i : Data.ByteString.ByteString- -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })+ -> i : ByteString+ -> (acc, { o : ByteString | bslen o == bslen i }) assume Data.ByteString.Char8.replicate :: n : Int -> GHC.Types.Char- -> { bs : Data.ByteString.ByteString | bslen bs == n }+ -> { bs : ByteString | bslen bs == n } assume Data.ByteString.Char8.unfoldrN :: n : Int -> (a -> Maybe (GHC.Types.Char, a)) -> a- -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a)+ -> ({ bs : ByteString | bslen bs <= n }, Maybe a) assume Data.ByteString.Char8.takeWhile :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o <= bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.Char8.dropWhile :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o <= bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.Char8.span :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.Char8.spanEnd :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.Char8.break :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.Char8.breakEnd :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.Char8.groupBy :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]+ -> i : ByteString+ -> [{ o : ByteString | 1 <= bslen o && bslen o <= bslen i }] assume Data.ByteString.Char8.split :: GHC.Types.Char- -> i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]+ -> i : ByteString+ -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.Char8.splitWith :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]+ -> i : ByteString+ -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.Char8.lines- :: i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]+ :: i : ByteString+ -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.Char8.words- :: i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]+ :: i : ByteString+ -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.Char8.unlines- :: is : [Data.ByteString.ByteString]- -> { o : Data.ByteString.ByteString | (len is == 0 <=> bslen o == 0) && bslen o >= len is }+ :: is : [ByteString]+ -> { o : ByteString | (len is == 0 <=> bslen o == 0) && bslen o >= len is } assume Data.ByteString.Char8.unwords- :: is : [Data.ByteString.ByteString]- -> { o : Data.ByteString.ByteString | (len is == 0 ==> bslen o == 0) && (1 <= len is ==> bslen o >= len is - 1) }+ :: is : [ByteString]+ -> { o : ByteString | (len is == 0 ==> bslen o == 0) && (1 <= len is ==> bslen o >= len is - 1) } assume Data.ByteString.Char8.elem :: GHC.Types.Char- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b } assume Data.ByteString.Char8.notElem :: GHC.Types.Char- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> { b : GHC.Types.Bool | bslen bs == 0 ==> b } assume Data.ByteString.Char8.find :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> Maybe { w8 : GHC.Types.Char | bslen bs /= 0 } assume Data.ByteString.Char8.filter :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o <= bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.Char8.index- :: bs : Data.ByteString.ByteString+ :: bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.elemIndex :: GHC.Types.Char- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> Maybe { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.Char8.elemIndices :: GHC.Types.Char- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> [{ n : Int | 0 <= n && n < bslen bs }] assume Data.ByteString.Char8.elemIndexEnd :: GHC.Types.Char- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> Maybe { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.Char8.findIndex :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> Maybe { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.Char8.findIndices :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> [{ n : Int | 0 <= n && n < bslen bs }] assume Data.ByteString.Char8.count :: GHC.Types.Char- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.Char8.zip- :: l : Data.ByteString.ByteString- -> r : Data.ByteString.ByteString+ :: l : ByteString+ -> r : ByteString -> { o : [(GHC.Types.Char, GHC.Types.Char)] | len o <= bslen l && len o <= bslen r } assume Data.ByteString.Char8.zipWith :: (GHC.Types.Char -> GHC.Types.Char -> a)- -> l : Data.ByteString.ByteString- -> r : Data.ByteString.ByteString+ -> l : ByteString+ -> r : ByteString -> { o : [a] | len o <= bslen l && len o <= bslen r } assume Data.ByteString.Char8.unzip :: i : [(GHC.Types.Char, GHC.Types.Char)]- -> ( { l : Data.ByteString.ByteString | bslen l == len i }- , { r : Data.ByteString.ByteString | bslen r == len i }+ -> ( { l : ByteString | bslen l == len i }+ , { r : ByteString | bslen r == len i } ) -assume Data.ByteString.ReadInt.readInt- :: i : Data.ByteString.ByteString- -> Maybe { p : (Int, { o : Data.ByteString.ByteString | bslen o < bslen i}) | bslen i /= 0 }+assume readInt+ :: i : ByteString+ -> Maybe { p : (Int, { o : ByteString | bslen o < bslen i}) | bslen i /= 0 } -assume Data.ByteString.ReadNat.readInteger- :: i : Data.ByteString.ByteString- -> Maybe { p : (Integer, { o : Data.ByteString.ByteString | bslen o < bslen i}) | bslen i /= 0 }+assume readInteger+ :: i : ByteString+ -> Maybe { p : (Integer, { o : ByteString | bslen o < bslen i}) | bslen i /= 0 } @-}
src/Data/ByteString/Lazy/Char8_LHAssumptions.hs view
@@ -5,252 +5,253 @@ import Data.ByteString.Lazy hiding (hGetNonBlocking, scanl) import Data.ByteString.Lazy.Char8 import Data.ByteString.Lazy_LHAssumptions()+import Data.Int {-@-assume Data.ByteString.Lazy.Char8.last :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> GHC.Types.Char+assume Data.ByteString.Lazy.Char8.last :: { bs : ByteString | 1 <= bllen bs } -> Char assume Data.ByteString.Lazy.Char8.singleton- :: GHC.Types.Char -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == 1 }+ :: Char -> { bs : ByteString | bllen bs == 1 } assume Data.ByteString.Lazy.Char8.pack- :: w8s : [GHC.Types.Char]- -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == len w8s }+ :: w8s : [Char]+ -> { bs : ByteString | bllen bs == len w8s } assume Data.ByteString.Lazy.Char8.unpack- :: bs : Data.ByteString.Lazy.ByteString- -> { w8s : [GHC.Types.Char] | len w8s == bllen bs }+ :: bs : ByteString+ -> { w8s : [Char] | len w8s == bllen bs } assume Data.ByteString.Lazy.Char8.cons- :: GHC.Types.Char- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }+ :: Char+ -> i : ByteString+ -> { o : ByteString | bllen o == bllen i + 1 } assume Data.ByteString.Lazy.Char8.snoc- :: i : Data.ByteString.Lazy.ByteString- -> GHC.Types.Char- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }+ :: i : ByteString+ -> Char+ -> { o : ByteString | bllen o == bllen i + 1 } assume Data.ByteString.Lazy.Char8.head- :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }- -> GHC.Types.Char+ :: { bs : ByteString | 1 <= bllen bs }+ -> Char assume Data.ByteString.Lazy.Char8.uncons- :: i : Data.ByteString.Lazy.ByteString- -> Maybe (GHC.Types.Char, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 })+ :: i : ByteString+ -> Maybe (Char, { o : ByteString | bllen o == bllen i - 1 }) assume Data.ByteString.Lazy.Char8.unsnoc- :: i : Data.ByteString.Lazy.ByteString- -> Maybe ({ o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }, GHC.Types.Char)+ :: i : ByteString+ -> Maybe ({ o : ByteString | bllen o == bllen i - 1 }, Char) assume Data.ByteString.Lazy.Char8.map- :: (GHC.Types.Char -> GHC.Types.Char)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ :: (Char -> Char)+ -> i : ByteString+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.intersperse- :: GHC.Types.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) }+ :: Char+ -> i : ByteString+ -> { o : ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) } assume Data.ByteString.Lazy.Char8.foldl1- :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }- -> GHC.Types.Char+ :: (Char -> Char -> Char)+ -> { bs : ByteString | 1 <= bllen bs }+ -> Char assume Data.ByteString.Lazy.Char8.foldl1'- :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }- -> GHC.Types.Char+ :: (Char -> Char -> Char)+ -> { bs : ByteString | 1 <= bllen bs }+ -> Char assume Data.ByteString.Lazy.Char8.foldr1- :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }- -> GHC.Types.Char+ :: (Char -> Char -> Char)+ -> { bs : ByteString | 1 <= bllen bs }+ -> Char assume Data.ByteString.Lazy.Char8.concatMap- :: (GHC.Types.Char -> Data.ByteString.Lazy.ByteString)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen i == 0 ==> bllen o == 0 }+ :: (Char -> ByteString)+ -> i : ByteString+ -> { o : ByteString | bllen i == 0 ==> bllen o == 0 } -assume Data.ByteString.Lazy.Char8.any :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b }+assume Data.ByteString.Lazy.Char8.any :: (Char -> Bool)+ -> bs : ByteString+ -> { b : Bool | bllen bs == 0 ==> not b } -assume Data.ByteString.Lazy.Char8.all :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | bllen bs == 0 ==> b }+assume Data.ByteString.Lazy.Char8.all :: (Char -> Bool)+ -> bs : ByteString+ -> { b : Bool | bllen bs == 0 ==> b } -assume Data.ByteString.Lazy.Char8.maximum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> GHC.Types.Char+assume Data.ByteString.Lazy.Char8.maximum :: { bs : ByteString | 1 <= bllen bs } -> Char -assume Data.ByteString.Lazy.Char8.minimum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> GHC.Types.Char+assume Data.ByteString.Lazy.Char8.minimum :: { bs : ByteString | 1 <= bllen bs } -> Char assume Data.ByteString.Lazy.Char8.scanl- :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> GHC.Types.Char- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ :: (Char -> Char -> Char)+ -> Char+ -> i : ByteString+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.scanl1- :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> i : { i : Data.ByteString.Lazy.ByteString | 1 <= bllen i }- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ :: (Char -> Char -> Char)+ -> i : { i : ByteString | 1 <= bllen i }+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.scanr- :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> GHC.Types.Char- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ :: (Char -> Char -> Char)+ -> Char+ -> i : ByteString+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.scanr1- :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char)- -> i : { i : Data.ByteString.Lazy.ByteString | 1 <= bllen i }- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ :: (Char -> Char -> Char)+ -> i : { i : ByteString | 1 <= bllen i }+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.mapAccumL- :: (acc -> GHC.Types.Char -> (acc, GHC.Types.Char))+ :: (acc -> Char -> (acc, Char)) -> acc- -> i : Data.ByteString.Lazy.ByteString- -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })+ -> i : ByteString+ -> (acc, { o : ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.Char8.mapAccumR- :: (acc -> GHC.Types.Char -> (acc, GHC.Types.Char))+ :: (acc -> Char -> (acc, Char)) -> acc- -> i : Data.ByteString.Lazy.ByteString- -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })+ -> i : ByteString+ -> (acc, { o : ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.Char8.replicate :: n : Int64- -> GHC.Types.Char- -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n }+ -> Char+ -> { bs : ByteString | bllen bs == n } assume Data.ByteString.Lazy.Char8.takeWhile- :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }+ :: (Char -> Bool)+ -> i : ByteString+ -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.Char8.dropWhile- :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }+ :: (Char -> Bool)+ -> i : ByteString+ -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.Char8.span- :: (GHC.Types.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 }+ :: (Char -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bllen l <= bllen i }+ , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.Char8.break- :: (GHC.Types.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 }+ :: (Char -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bllen l <= bllen i }+ , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.Char8.groupBy- :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]+ :: (Char -> Char -> Bool)+ -> i : ByteString+ -> [{ o : ByteString | 1 <= bllen o && bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.split- :: GHC.Types.Char- -> i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]+ :: Char+ -> i : ByteString+ -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.splitWith- :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]+ :: (Char -> Bool)+ -> i : ByteString+ -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.lines- :: i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]+ :: i : ByteString+ -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.words- :: i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]+ :: i : ByteString+ -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.unlines- :: is : [Data.ByteString.Lazy.ByteString]- -> { o : Data.ByteString.Lazy.ByteString | (len is == 0 <=> bllen o == 0) && bllen o >= len is }+ :: is : [ByteString]+ -> { o : ByteString | (len is == 0 <=> bllen o == 0) && bllen o >= len is } assume Data.ByteString.Lazy.Char8.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) }+ :: is : [ByteString]+ -> { o : ByteString | (len is == 0 ==> bllen o == 0) && (1 <= len is ==> bllen o >= len is - 1) } assume Data.ByteString.Lazy.Char8.elem- :: GHC.Types.Char- -> bs : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b }+ :: Char+ -> bs : ByteString+ -> { b : Bool | bllen bs == 0 ==> not b } assume Data.ByteString.Lazy.Char8.notElem- :: GHC.Types.Char- -> bs : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | bllen bs == 0 ==> b }+ :: Char+ -> bs : ByteString+ -> { b : Bool | bllen bs == 0 ==> b } assume Data.ByteString.Lazy.Char8.find- :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString- -> Maybe { w8 : GHC.Types.Char | bllen bs /= 0 }+ :: (Char -> Bool)+ -> bs : ByteString+ -> Maybe { w8 : Char | bllen bs /= 0 } assume Data.ByteString.Lazy.Char8.filter- :: (GHC.Types.Char -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }+ :: (Char -> Bool)+ -> i : ByteString+ -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.Char8.index- :: bs : Data.ByteString.Lazy.ByteString+ :: bs : ByteString -> { n : Int64 | 0 <= n && n < bllen bs }- -> GHC.Types.Char+ -> Char assume Data.ByteString.Lazy.Char8.elemIndex- :: GHC.Types.Char- -> bs : Data.ByteString.Lazy.ByteString+ :: Char+ -> bs : ByteString -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.Char8.elemIndices- :: GHC.Types.Char- -> bs : Data.ByteString.Lazy.ByteString+ :: Char+ -> bs : ByteString -> [{ n : Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.Char8.findIndex- :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString+ :: (Char -> Bool)+ -> bs : ByteString -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.Char8.findIndices- :: (GHC.Types.Char -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString+ :: (Char -> Bool)+ -> bs : ByteString -> [{ n : Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.Char8.count- :: GHC.Types.Char- -> bs : Data.ByteString.Lazy.ByteString+ :: Char+ -> bs : ByteString -> { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.Char8.zip- :: l : Data.ByteString.Lazy.ByteString- -> r : Data.ByteString.Lazy.ByteString- -> { o : [(GHC.Types.Char, GHC.Types.Char)] | len o <= bllen l && len o <= bllen r }+ :: l : ByteString+ -> r : ByteString+ -> { o : [(Char, Char)] | len o <= bllen l && len o <= bllen r } assume Data.ByteString.Lazy.Char8.zipWith- :: (GHC.Types.Char -> GHC.Types.Char -> a)- -> l : Data.ByteString.Lazy.ByteString- -> r : Data.ByteString.Lazy.ByteString+ :: (Char -> Char -> a)+ -> l : ByteString+ -> r : ByteString -> { o : [a] | len o <= bllen l && len o <= bllen r } assume Data.ByteString.Lazy.Char8.unzip- :: i : [(GHC.Types.Char, GHC.Types.Char)]- -> ( { l : Data.ByteString.Lazy.ByteString | bllen l == len i }- , { r : Data.ByteString.Lazy.ByteString | bllen r == len i }+ :: i : [(Char, Char)]+ -> ( { l : ByteString | bllen l == len i }+ , { r : ByteString | bllen r == len i } ) -assume Data.ByteString.Lazy.ReadInt.readInt- :: i : Data.ByteString.Lazy.ByteString- -> Maybe { p : (Int, { o : Data.ByteString.Lazy.ByteString | bllen o < bllen i}) | bllen i /= 0 }+assume readInt+ :: i : ByteString+ -> Maybe { p : (Int, { o : ByteString | bllen o < bllen i}) | bllen i /= 0 } -assume Data.ByteString.Lazy.ReadNat.readInteger- :: i : Data.ByteString.Lazy.ByteString- -> Maybe { p : (Integer, { o : Data.ByteString.Lazy.ByteString | bllen o < bllen i}) | bllen i /= 0 }+assume readInteger+ :: i : ByteString+ -> Maybe { p : (Integer, { o : ByteString | bllen o < bllen i}) | bllen i /= 0 } @-}
src/Data/ByteString/Lazy_LHAssumptions.hs view
@@ -2,344 +2,345 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module Data.ByteString.Lazy_LHAssumptions where -import Data.ByteString+import qualified Data.ByteString import Data.ByteString_LHAssumptions() import Data.ByteString.Lazy+import Data.Int import Data.String_LHAssumptions() import GHC.Int_LHAssumptions() {-@-measure bllen :: Data.ByteString.Lazy.ByteString -> { n : GHC.Internal.Int.Int64 | 0 <= n }+measure bllen :: ByteString -> { n : Int64 | 0 <= n } -invariant { bs : Data.ByteString.Lazy.ByteString | 0 <= bllen bs }+invariant { bs : ByteString | 0 <= bllen bs } -invariant { bs : Data.ByteString.Lazy.ByteString | bllen bs == stringlen bs }+invariant { bs : ByteString | bllen bs == stringlen bs } -assume Data.ByteString.Lazy.empty :: { bs : Data.ByteString.Lazy.ByteString | bllen bs == 0 }+assume empty :: { bs : ByteString | bllen bs == 0 } -assume Data.ByteString.Lazy.singleton- :: _ -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == 1 }+assume singleton+ :: _ -> { bs : ByteString | bllen bs == 1 } -assume Data.ByteString.Lazy.pack+assume pack :: w8s : [_] -> { bs : _ | bllen bs == len w8s } -assume Data.ByteString.Lazy.unpack- :: bs : Data.ByteString.Lazy.ByteString+assume unpack+ :: bs : ByteString -> { w8s : [_] | len w8s == bllen bs } -assume Data.ByteString.Lazy.Internal.fromStrict+assume fromStrict :: i : Data.ByteString.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bslen i }+ -> { o : ByteString | bllen o == bslen i } -assume Data.ByteString.Lazy.Internal.toStrict- :: i : Data.ByteString.Lazy.ByteString+assume toStrict+ :: i : ByteString -> { o : Data.ByteString.ByteString | bslen o == bllen i } -assume Data.ByteString.Lazy.fromChunks+assume fromChunks :: i : [Data.ByteString.ByteString]- -> { o : Data.ByteString.Lazy.ByteString | len i == 0 <=> bllen o == 0 }+ -> { o : ByteString | len i == 0 <=> bllen o == 0 } -assume Data.ByteString.Lazy.toChunks- :: i : Data.ByteString.Lazy.ByteString+assume toChunks+ :: i : ByteString -> { os : [{ o : Data.ByteString.ByteString | bslen o <= bllen i}] | len os == 0 <=> bllen i == 0 } assume Data.ByteString.Lazy.cons :: _- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }+ -> i : ByteString+ -> { o : ByteString | bllen o == bllen i + 1 } assume Data.ByteString.Lazy.snoc- :: i : Data.ByteString.Lazy.ByteString+ :: i : ByteString -> _- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }+ -> { o : ByteString | bllen o == bllen i + 1 } assume Data.ByteString.Lazy.append- :: l : Data.ByteString.Lazy.ByteString- -> r : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen l + bllen r }+ :: l : ByteString+ -> r : ByteString+ -> { o : ByteString | bllen o == bllen l + bllen r } assume Data.ByteString.Lazy.head- :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ :: { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.uncons- :: i : Data.ByteString.Lazy.ByteString- -> Maybe (_, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 })+ :: i : ByteString+ -> Maybe (_, { o : ByteString | bllen o == bllen i - 1 }) assume Data.ByteString.Lazy.unsnoc- :: i : Data.ByteString.Lazy.ByteString- -> Maybe ({ o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }, _)+ :: i : ByteString+ -> Maybe ({ o : ByteString | bllen o == bllen i - 1 }, _) -assume Data.ByteString.Lazy.last :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _+assume Data.ByteString.Lazy.last :: { bs : ByteString | 1 <= bllen bs } -> _ -assume Data.ByteString.Lazy.tail :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _+assume Data.ByteString.Lazy.tail :: { bs : ByteString | 1 <= bllen bs } -> _ -assume Data.ByteString.Lazy.init :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _+assume Data.ByteString.Lazy.init :: { bs : ByteString | 1 <= bllen bs } -> _ -assume Data.ByteString.Lazy.null :: bs : Data.ByteString.Lazy.ByteString -> { b : GHC.Types.Bool | b <=> bllen bs == 0 }+assume Data.ByteString.Lazy.null :: bs : ByteString -> { b : Bool | b <=> bllen bs == 0 } assume Data.ByteString.Lazy.length- :: bs : Data.ByteString.Lazy.ByteString -> { n : GHC.Internal.Int.Int64 | bllen bs == n }+ :: bs : ByteString -> { n : Int64 | bllen bs == n } assume Data.ByteString.Lazy.map :: (_ -> _)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ -> i : ByteString+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.reverse- :: i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ :: i : ByteString+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.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) }+ -> i : ByteString+ -> { o : ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) } assume Data.ByteString.Lazy.intercalate- :: l : Data.ByteString.Lazy.ByteString- -> rs : [Data.ByteString.Lazy.ByteString]- -> { o : Data.ByteString.Lazy.ByteString | len rs == 0 ==> bllen o == 0 }+ :: l : ByteString+ -> rs : [ByteString]+ -> { o : ByteString | len rs == 0 ==> bllen o == 0 } assume Data.ByteString.Lazy.transpose- :: is : [Data.ByteString.Lazy.ByteString]- -> { os : [{ bs : Data.ByteString.Lazy.ByteString | bllen bs <= len is }] | len is == 0 ==> len os == 0}+ :: is : [ByteString]+ -> { os : [{ bs : ByteString | bllen bs <= len is }] | len is == 0 ==> len os == 0} assume Data.ByteString.Lazy.foldl1 :: (_ -> _ -> _)- -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.foldl1' :: (_ -> _ -> _)- -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.foldr1 :: (_ -> _ -> _)- -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }+ -> { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.concat- :: is : [Data.ByteString.Lazy.ByteString]- -> { o : Data.ByteString.Lazy.ByteString | (len is == 0) ==> (bllen o == 0) }+ :: is : [ByteString]+ -> { o : ByteString | (len is == 0) ==> (bllen o == 0) } assume Data.ByteString.Lazy.concatMap- :: (_ -> Data.ByteString.Lazy.ByteString)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen i == 0 ==> bllen o == 0 }+ :: (_ -> ByteString)+ -> i : ByteString+ -> { o : ByteString | bllen i == 0 ==> bllen o == 0 } -assume Data.ByteString.Lazy.any :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b }+assume Data.ByteString.Lazy.any :: (_ -> Bool)+ -> bs : ByteString+ -> { b : Bool | bllen bs == 0 ==> not b } -assume Data.ByteString.Lazy.all :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | bllen bs == 0 ==> b }+assume Data.ByteString.Lazy.all :: (_ -> Bool)+ -> bs : ByteString+ -> { b : Bool | bllen bs == 0 ==> b } -assume Data.ByteString.Lazy.maximum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _+assume Data.ByteString.Lazy.maximum :: { bs : ByteString | 1 <= bllen bs } -> _ -assume Data.ByteString.Lazy.minimum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _+assume Data.ByteString.Lazy.minimum :: { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.scanl :: (_ -> _ -> _) -> _- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ -> i : ByteString+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.mapAccumL :: (acc -> _ -> (acc, _)) -> acc- -> i : Data.ByteString.Lazy.ByteString- -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })+ -> i : ByteString+ -> (acc, { o : ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.mapAccumR :: (acc -> _ -> (acc, _)) -> acc- -> i : Data.ByteString.Lazy.ByteString- -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })+ -> i : ByteString+ -> (acc, { o : ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.replicate- :: n : GHC.Internal.Int.Int64+ :: n : Int64 -> _- -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n }+ -> { bs : ByteString | bllen bs == n } assume Data.ByteString.Lazy.take- :: n : GHC.Internal.Int.Int64- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 ==> bllen o == 0) &&+ :: n : Int64+ -> i : ByteString+ -> { o : ByteString | (n <= 0 ==> bllen o == 0) && ((0 <= n && n <= bllen i) <=> bllen o == n) && (bllen i <= n <=> bllen o = bllen i) } assume Data.ByteString.Lazy.drop- :: n : GHC.Internal.Int.Int64- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen o == bllen i) &&+ :: n : Int64+ -> i : ByteString+ -> { o : ByteString | (n <= 0 <=> bllen o == bllen i) && ((0 <= n && n <= bllen i) <=> bllen o == bllen i - n) && (bllen i <= n <=> bllen o == 0) } assume Data.ByteString.Lazy.splitAt- :: n : GHC.Internal.Int.Int64- -> i : Data.ByteString.Lazy.ByteString- -> ( { l : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen l == 0) &&+ :: n : Int64+ -> i : ByteString+ -> ( { l : 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) &&+ , { r : ByteString | (n <= 0 <=> bllen r == bllen i) && ((0 <= n && n <= bllen i) <=> bllen r == bllen i - n) && (bllen i <= n <=> bllen r == 0) } ) assume Data.ByteString.Lazy.takeWhile- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.dropWhile- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.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 }+ :: (_ -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bllen l <= bllen i }+ , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.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 }+ :: (_ -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bllen l <= bllen i }+ , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.group- :: i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]+ :: i : ByteString+ -> [{ o : ByteString | 1 <= bllen o && bllen o <= bllen i }] assume Data.ByteString.Lazy.groupBy- :: (_ -> _ -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]+ :: (_ -> _ -> Bool)+ -> i : ByteString+ -> [{ o : ByteString | 1 <= bllen o && bllen o <= bllen i }] assume Data.ByteString.Lazy.inits- :: i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]+ :: i : ByteString+ -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.tails- :: i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]+ :: i : ByteString+ -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.split :: _- -> i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]+ -> i : ByteString+ -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.splitWith- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]+ :: (_ -> Bool)+ -> i : ByteString+ -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.isPrefixOf- :: l : Data.ByteString.Lazy.ByteString- -> r : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }+ :: l : ByteString+ -> r : ByteString+ -> { b : Bool | bllen l >= bllen r ==> not b } assume Data.ByteString.Lazy.isSuffixOf- :: l : Data.ByteString.Lazy.ByteString- -> r : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }+ :: l : ByteString+ -> r : ByteString+ -> { b : Bool | bllen l >= bllen r ==> not b } assume Data.ByteString.Lazy.elem :: _- -> bs : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | (bllen bs == 0) ==> not b }+ -> bs : ByteString+ -> { b : Bool | (bllen bs == 0) ==> not b } assume Data.ByteString.Lazy.notElem :: _- -> bs : Data.ByteString.Lazy.ByteString- -> { b : GHC.Types.Bool | (bllen bs == 0) ==> b }+ -> bs : ByteString+ -> { b : Bool | (bllen bs == 0) ==> b } assume Data.ByteString.Lazy.find- :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString+ :: (_ -> Bool)+ -> bs : ByteString -> Maybe { w8 : _ | bllen bs /= 0 } assume Data.ByteString.Lazy.filter- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.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 }+ :: (_ -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bllen l <= bllen i }+ , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.index- :: bs : Data.ByteString.Lazy.ByteString- -> { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }+ :: bs : ByteString+ -> { n : Int64 | 0 <= n && n < bllen bs } -> _ assume Data.ByteString.Lazy.elemIndex :: _- -> bs : Data.ByteString.Lazy.ByteString- -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }+ -> bs : ByteString+ -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.elemIndices :: _- -> bs : Data.ByteString.Lazy.ByteString- -> [{ n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }]+ -> bs : ByteString+ -> [{ n : Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.elemIndexEnd :: _- -> bs : Data.ByteString.Lazy.ByteString- -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }+ -> bs : ByteString+ -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.findIndex- :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString- -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }+ :: (_ -> Bool)+ -> bs : ByteString+ -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.findIndices- :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.Lazy.ByteString- -> [{ n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }]+ :: (_ -> Bool)+ -> bs : ByteString+ -> [{ n : Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.count :: _- -> bs : Data.ByteString.Lazy.ByteString- -> { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }+ -> bs : ByteString+ -> { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.zip- :: l : Data.ByteString.Lazy.ByteString- -> r : Data.ByteString.Lazy.ByteString+ :: l : ByteString+ -> r : ByteString -> { o : [(_, _)] | len o <= bllen l && len o <= bllen r } assume Data.ByteString.Lazy.zipWith :: (_ -> _ -> a)- -> l : Data.ByteString.Lazy.ByteString- -> r : Data.ByteString.Lazy.ByteString+ -> l : ByteString+ -> r : ByteString -> { o : [a] | len o <= bllen l && len o <= bllen r } assume Data.ByteString.Lazy.unzip :: i : [(_, _)]- -> ( { l : Data.ByteString.Lazy.ByteString | bllen l == len i }- , { r : Data.ByteString.Lazy.ByteString | bllen r == len i }+ -> ( { l : ByteString | bllen l == len i }+ , { r : ByteString | bllen r == len i } ) assume Data.ByteString.Lazy.copy- :: i : Data.ByteString.Lazy.ByteString- -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }+ :: i : ByteString+ -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.hGet :: _ -> n : { n : Int | 0 <= n }- -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs == n || bllen bs == 0 }+ -> IO { bs : ByteString | bllen bs == n || bllen bs == 0 } assume Data.ByteString.Lazy.hGetNonBlocking :: _ -> n : { n : Int | 0 <= n }- -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs <= n }+ -> IO { bs : ByteString | bllen bs <= n } @-}
src/Data/ByteString/Short_LHAssumptions.hs view
@@ -2,31 +2,32 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module Data.ByteString.Short_LHAssumptions where -import Data.ByteString+import Data.ByteString (ByteString) import Data.ByteString_LHAssumptions() import Data.ByteString.Short import Data.String_LHAssumptions()+import Data.Word {-@-measure sbslen :: Data.ByteString.Short.ShortByteString -> { n : Int | 0 <= n }+measure sbslen :: ShortByteString -> { n : Int | 0 <= n } -invariant { bs : Data.ByteString.Short.ShortByteString | 0 <= sbslen bs }+invariant { bs : ShortByteString | 0 <= sbslen bs } -invariant { bs : Data.ByteString.Short.ShortByteString | sbslen bs == stringlen bs }+invariant { bs : ShortByteString | sbslen bs == stringlen bs } -assume Data.ByteString.Short.Internal.toShort :: i : Data.ByteString.ByteString -> { o : Data.ByteString.Short.ShortByteString | sbslen o == bslen i }+assume toShort :: i : ByteString -> { o : ShortByteString | sbslen o == bslen i } -assume Data.ByteString.Short.Internal.fromShort :: o : Data.ByteString.Short.ShortByteString -> { i : Data.ByteString.ByteString | bslen i == sbslen o }+assume fromShort :: o : ShortByteString -> { i : ByteString | bslen i == sbslen o } -assume Data.ByteString.Short.Internal.pack :: w8s : [Word8] -> { bs : Data.ByteString.Short.ShortByteString | sbslen bs == len w8s }+assume pack :: w8s : [Word8] -> { bs : ShortByteString | sbslen bs == len w8s } -assume Data.ByteString.Short.Internal.unpack :: bs : Data.ByteString.Short.ShortByteString -> { w8s : [Word8] | len w8s == sbslen bs }+assume unpack :: bs : ShortByteString -> { w8s : [Word8] | len w8s == sbslen bs } -assume Data.ByteString.Short.Internal.empty :: { bs : Data.ByteString.Short.ShortByteString | sbslen bs == 0 }+assume empty :: { bs : ShortByteString | sbslen bs == 0 } -assume Data.ByteString.Short.Internal.null :: bs : Data.ByteString.Short.ShortByteString -> { b : GHC.Types.Bool | b <=> sbslen bs == 0 }+assume Data.ByteString.Short.null :: bs : ShortByteString -> { b : Bool | b <=> sbslen bs == 0 } -assume Data.ByteString.Short.Internal.length :: bs : Data.ByteString.Short.ShortByteString -> { n : Int | sbslen bs == n }+assume Data.ByteString.Short.length :: bs : ShortByteString -> { n : Int | sbslen bs == n } -assume Data.ByteString.Short.Internal.index :: bs : Data.ByteString.Short.ShortByteString -> { n : Int | 0 <= n && n < sbslen bs } -> Word8+assume index :: bs : ShortByteString -> { n : Int | 0 <= n && n < sbslen bs } -> Word8 @-}
src/Data/ByteString/Unsafe_LHAssumptions.hs view
@@ -2,36 +2,37 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module Data.ByteString.Unsafe_LHAssumptions where +import Data.ByteString import Data.ByteString.Unsafe import Data.ByteString_LHAssumptions() import GHC.Types_LHAssumptions() {-@ assume Data.ByteString.Unsafe.unsafeHead- :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _+ :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.Unsafe.unsafeTail- :: bs : { v : Data.ByteString.ByteString | bslen v > 0 }- -> { v : Data.ByteString.ByteString | bslen v = bslen bs - 1 }+ :: bs : { v : ByteString | bslen v > 0 }+ -> { v : ByteString | bslen v = bslen bs - 1 } assume Data.ByteString.Unsafe.unsafeInit- :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _+ :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.Unsafe.unsafeLast- :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _+ :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.Unsafe.unsafeIndex- :: bs : Data.ByteString.ByteString+ :: bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } -> _ assume Data.ByteString.Unsafe.unsafeTake :: n : { n : Int | 0 <= n }- -> i : { i : Data.ByteString.ByteString | n <= bslen i }- -> { o : Data.ByteString.ByteString | bslen o == n }+ -> i : { i : ByteString | n <= bslen i }+ -> { o : ByteString | bslen o == n } assume Data.ByteString.Unsafe.unsafeDrop :: n : { n : Int | 0 <= n }- -> i : { i : Data.ByteString.ByteString | n <= bslen i }- -> { o : Data.ByteString.ByteString | bslen o == bslen i - n }+ -> i : { i : ByteString | n <= bslen i }+ -> { o : ByteString | bslen o == bslen i - n } @-}
src/Data/ByteString_LHAssumptions.hs view
@@ -7,374 +7,374 @@ import GHC.Word {-@-measure bslen :: Data.ByteString.ByteString -> { n : Int | 0 <= n }+measure bslen :: ByteString -> { n : Int | 0 <= n } -invariant { bs : Data.ByteString.ByteString | 0 <= bslen bs }+invariant { bs : ByteString | 0 <= bslen bs } -invariant { bs : Data.ByteString.ByteString | bslen bs == stringlen bs }+invariant { bs : ByteString | bslen bs == stringlen bs } -assume Data.ByteString.Internal.Type.empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 }+assume empty :: { bs : ByteString | bslen bs == 0 } -assume Data.ByteString.singleton :: _ -> { bs : Data.ByteString.ByteString | bslen bs == 1 }+assume Data.ByteString.singleton :: _ -> { bs : ByteString | bslen bs == 1 } assume Data.ByteString.pack :: w8s : [_]- -> { bs : Data.ByteString.ByteString | bslen bs == len w8s }+ -> { bs : ByteString | bslen bs == len w8s } -assume Data.ByteString.unpack :: bs : Data.ByteString.ByteString+assume Data.ByteString.unpack :: bs : ByteString -> { w8s : [_] | len w8s == bslen bs } assume Data.ByteString.cons :: _- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }+ -> i : ByteString+ -> { o : ByteString | bslen o == bslen i + 1 } -assume Data.ByteString.snoc :: i : Data.ByteString.ByteString+assume Data.ByteString.snoc :: i : ByteString -> _- -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }+ -> { o : ByteString | bslen o == bslen i + 1 } -assume Data.ByteString.append :: l : Data.ByteString.ByteString- -> r : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen l + bslen r }+assume Data.ByteString.append :: l : ByteString+ -> r : ByteString+ -> { o : ByteString | bslen o == bslen l + bslen r } -assume Data.ByteString.head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _+assume Data.ByteString.head :: { bs : ByteString | 1 <= bslen bs } -> _ -assume Data.ByteString.unsnoc :: i:Data.ByteString.ByteString- -> (Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, _))+assume Data.ByteString.unsnoc :: i:ByteString+ -> (Maybe ({ o : ByteString | bslen o == bslen i - 1 }, _)) -assume Data.ByteString.last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _+assume Data.ByteString.last :: { bs : ByteString | 1 <= bslen bs } -> _ -assume Data.ByteString.tail :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _+assume Data.ByteString.tail :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.init- :: {i:Data.ByteString.ByteString | 1 <= bslen i }- -> {o:Data.ByteString.ByteString | bslen o == bslen i - 1 }+ :: {i:ByteString | 1 <= bslen i }+ -> {o:ByteString | bslen o == bslen i - 1 } assume Data.ByteString.null- :: bs : Data.ByteString.ByteString- -> { b : GHC.Types.Bool | b <=> bslen bs == 0 }+ :: bs : ByteString+ -> { b : Bool | b <=> bslen bs == 0 } -assume Data.ByteString.length :: bs : Data.ByteString.ByteString -> { n : Int | bslen bs == n }+assume Data.ByteString.length :: bs : ByteString -> { n : Int | bslen bs == n } assume Data.ByteString.map :: (_ -> _)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.reverse- :: i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ :: i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.intersperse :: _- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) }+ -> i : ByteString+ -> { o : ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) } assume Data.ByteString.intercalate- :: l : Data.ByteString.ByteString- -> rs : [Data.ByteString.ByteString]- -> { o : Data.ByteString.ByteString | len rs == 0 ==> bslen o == 0 }+ :: l : ByteString+ -> rs : [ByteString]+ -> { o : ByteString | len rs == 0 ==> bslen o == 0 } assume Data.ByteString.transpose- :: is : [Data.ByteString.ByteString]- -> { os : [{ bs : Data.ByteString.ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0}+ :: is : [ByteString]+ -> { os : [{ bs : ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0} assume Data.ByteString.foldl1 :: (_ -> _ -> _)- -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.foldl1' :: (_ -> _ -> _)- -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.foldr1 :: (_ -> _ -> _)- -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.foldr1' :: (_ -> _ -> _)- -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.concat- :: is : [Data.ByteString.ByteString]- -> { o : Data.ByteString.ByteString | (len is == 0) ==> (bslen o == 0) }+ :: is : [ByteString]+ -> { o : ByteString | (len is == 0) ==> (bslen o == 0) } assume Data.ByteString.concatMap- :: (_ -> Data.ByteString.ByteString)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 }+ :: (_ -> ByteString)+ -> i : ByteString+ -> { o : ByteString | bslen i == 0 ==> bslen o == 0 } assume Data.ByteString.any- :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString- -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }+ :: (_ -> Bool)+ -> bs : ByteString+ -> { b : Bool | bslen bs == 0 ==> not b } assume Data.ByteString.all- :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString- -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }+ :: (_ -> Bool)+ -> bs : ByteString+ -> { b : Bool | bslen bs == 0 ==> b } -assume Data.ByteString.maximum :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _+assume Data.ByteString.maximum :: { bs : ByteString | 1 <= bslen bs } -> _ -assume Data.ByteString.minimum :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _+assume Data.ByteString.minimum :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.scanl :: (_ -> _ -> _) -> _- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.scanl1 :: (_ -> _ -> _)- -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : { i : ByteString | 1 <= bslen i }+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.scanr :: (_ -> _ -> _) -> _- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.scanr1 :: (_ -> _ -> _)- -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ -> i : { i : ByteString | 1 <= bslen i }+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.mapAccumL :: (acc -> _ -> (acc, _)) -> acc- -> i : Data.ByteString.ByteString- -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })+ -> i : ByteString+ -> (acc, { o : ByteString | bslen o == bslen i }) assume Data.ByteString.mapAccumR :: (acc -> _ -> (acc, _)) -> acc- -> i : Data.ByteString.ByteString- -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })+ -> i : ByteString+ -> (acc, { o : ByteString | bslen o == bslen i }) assume Data.ByteString.replicate :: n : Int -> _- -> { bs : Data.ByteString.ByteString | bslen bs == n }+ -> { bs : ByteString | bslen bs == n } assume Data.ByteString.unfoldrN :: n : Int -> (a -> Maybe (_, a)) -> a- -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a)+ -> ({ bs : ByteString | bslen bs <= n }, Maybe a) assume Data.ByteString.take :: n : Int- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == 0) &&+ -> i : ByteString+ -> { o : ByteString | (n <= 0 <=> bslen o == 0) && ((0 <= n && n <= bslen i) <=> bslen o == n) && (bslen i <= n <=> bslen o = bslen i) } assume Data.ByteString.drop :: n : Int- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == bslen i) &&+ -> i : ByteString+ -> { o : ByteString | (n <= 0 <=> bslen o == bslen i) && ((0 <= n && n <= bslen i) <=> bslen o == bslen i - n) && (bslen i <= n <=> bslen o == 0) } assume Data.ByteString.splitAt :: n : Int- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | (n <= 0 <=> bslen l == 0) &&+ -> i : ByteString+ -> ( { l : 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) &&+ , { r : ByteString | (n <= 0 <=> bslen r == bslen i) && ((0 <= n && n <= bslen i) <=> bslen r == bslen i - n) && (bslen i <= n <=> bslen r == 0) } ) assume Data.ByteString.takeWhile- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o <= bslen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.dropWhile- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o <= bslen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.span- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.spanEnd- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.break- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.breakEnd- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.group- :: i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]+ :: i : ByteString+ -> [{ o : ByteString | 1 <= bslen o && bslen o <= bslen i }] assume Data.ByteString.groupBy- :: (_ -> _ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]+ :: (_ -> _ -> Bool)+ -> i : ByteString+ -> [{ o : ByteString | 1 <= bslen o && bslen o <= bslen i }] assume Data.ByteString.inits- :: i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]+ :: i : ByteString+ -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.tails- :: i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]+ :: i : ByteString+ -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.split :: _- -> i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]+ -> i : ByteString+ -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.splitWith- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]+ :: (_ -> Bool)+ -> i : ByteString+ -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.isPrefixOf- :: l : Data.ByteString.ByteString- -> r : Data.ByteString.ByteString- -> { b : GHC.Types.Bool | bslen l >= bslen r ==> not b }+ :: l : ByteString+ -> r : ByteString+ -> { b : Bool | bslen l >= bslen r ==> not b } assume Data.ByteString.isSuffixOf- :: l : Data.ByteString.ByteString- -> r : Data.ByteString.ByteString- -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }+ :: l : ByteString+ -> r : ByteString+ -> { b : Bool | bslen l > bslen r ==> not b } assume Data.ByteString.isInfixOf- :: l : Data.ByteString.ByteString- -> r : Data.ByteString.ByteString- -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }+ :: l : ByteString+ -> r : ByteString+ -> { b : Bool | bslen l > bslen r ==> not b } assume Data.ByteString.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) }+ :: il : ByteString+ -> ir : ByteString+ -> ( { ol : ByteString | bslen ol <= bslen ir && (bslen il > bslen ir ==> bslen ol == bslen ir)}+ , { or : ByteString | bslen or <= bslen ir && (bslen il > bslen ir ==> bslen or == 0) } ) assume Data.ByteString.elem :: _- -> bs : Data.ByteString.ByteString- -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }+ -> bs : ByteString+ -> { b : Bool | bslen bs == 0 ==> not b } assume Data.ByteString.notElem :: _- -> bs : Data.ByteString.ByteString- -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }+ -> bs : ByteString+ -> { b : Bool | bslen bs == 0 ==> b } assume Data.ByteString.find- :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString+ :: (_ -> Bool)+ -> bs : ByteString -> (Maybe { w8 : _ | bslen bs /= 0 }) assume Data.ByteString.filter- :: (_ -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o <= bslen i }+ :: (_ -> Bool)+ -> i : ByteString+ -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.partition- :: (Word8 -> GHC.Types.Bool)- -> i : Data.ByteString.ByteString- -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }- , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ :: (Word8 -> Bool)+ -> i : ByteString+ -> ( { l : ByteString | bslen l <= bslen i }+ , { r : ByteString | bslen r <= bslen i } ) -assume Data.ByteString.index :: bs : Data.ByteString.ByteString -> { n : Int | 0 <= n && n < bslen bs } -> _+assume Data.ByteString.index :: bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } -> _ assume Data.ByteString.elemIndex :: _- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> (Maybe { n : Int | 0 <= n && n < bslen bs }) assume Data.ByteString.elemIndices :: _- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> [{ n : Int | 0 <= n && n < bslen bs }] assume Data.ByteString.elemIndexEnd :: _- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> (Maybe { n : Int | 0 <= n && n < bslen bs }) assume Data.ByteString.findIndex- :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString+ :: (_ -> Bool)+ -> bs : ByteString -> (Maybe { n : Int | 0 <= n && n < bslen bs }) assume Data.ByteString.findIndices- :: (_ -> GHC.Types.Bool)- -> bs : Data.ByteString.ByteString+ :: (_ -> Bool)+ -> bs : ByteString -> [{ n : Int | 0 <= n && n < bslen bs }] assume Data.ByteString.count :: _- -> bs : Data.ByteString.ByteString+ -> bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.zip- :: l : Data.ByteString.ByteString- -> r : Data.ByteString.ByteString+ :: l : ByteString+ -> r : ByteString -> { o : [(_, _)] | len o <= bslen l && len o <= bslen r } assume Data.ByteString.zipWith :: (_ -> _ -> a)- -> l : Data.ByteString.ByteString- -> r : Data.ByteString.ByteString+ -> l : ByteString+ -> r : ByteString -> { o : [a] | len o <= bslen l && len o <= bslen r } assume Data.ByteString.unzip :: i : [(_, _)]- -> ( { l : Data.ByteString.ByteString | bslen l == len i }- , { r : Data.ByteString.ByteString | bslen r == len i }+ -> ( { l : ByteString | bslen l == len i }+ , { r : ByteString | bslen r == len i } ) assume Data.ByteString.sort- :: i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ :: i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.copy- :: i : Data.ByteString.ByteString- -> { o : Data.ByteString.ByteString | bslen o == bslen i }+ :: i : ByteString+ -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.hGet :: _ -> n : { n : Int | 0 <= n }- -> (IO { bs : Data.ByteString.ByteString | bslen bs == n || bslen bs == 0 })+ -> (IO { bs : ByteString | bslen bs == n || bslen bs == 0 }) assume Data.ByteString.hGetSome :: _ -> n : { n : Int | 0 <= n }- -> (IO { bs : Data.ByteString.ByteString | bslen bs <= n })+ -> (IO { bs : ByteString | bslen bs <= n }) assume Data.ByteString.hGetNonBlocking :: _ -> n : { n : Int | 0 <= n }- -> (IO { bs : Data.ByteString.ByteString | bslen bs <= n })+ -> (IO { bs : ByteString | bslen bs <= n }) assume Data.ByteString.uncons- :: i : Data.ByteString.ByteString- -> (Maybe (_, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 }))+ :: i : ByteString+ -> (Maybe (_, { o : ByteString | bslen o == bslen i - 1 })) @-}
src/Data/Either_LHAssumptions.hs view
@@ -1,10 +1,11 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module Data.Either_LHAssumptions where import GHC.Types_LHAssumptions() {-@-measure isLeft :: GHC.Internal.Data.Either.Either a b -> Bool+measure isLeft :: Either a b -> Bool isLeft (Left x) = true isLeft (Right x) = false @-}
src/Data/Foldable_LHAssumptions.hs view
@@ -1,4 +1,12 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module Data.Foldable_LHAssumptions where -import GHC.Internal.Data.Foldable_LHAssumptions()+import Data.Foldable+import GHC.Types_LHAssumptions()+import Prelude hiding (length, null)++{-@+assume length :: Foldable f => forall a. xs:f a -> {v:Nat | v = len xs}+assume null :: Foldable f => forall a. v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)}+@-}
+ src/Data/List_LHAssumptions.hs view
@@ -0,0 +1,9 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+module Data.List_LHAssumptions where++-- TODO: For some reason, the specifications of GHC.List have+-- a role when verifying functions from Data.List. e.g+-- basic/pos/AssmReflFilter.hs+--+-- Needs to be investigated.+import GHC.List_LHAssumptions()
src/Data/Maybe_LHAssumptions.hs view
@@ -2,4 +2,20 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module Data.Maybe_LHAssumptions where -import GHC.Internal.Data.Maybe_LHAssumptions+import Data.Maybe+import GHC.Types_LHAssumptions ()++{-@+assume maybe :: v:b -> (a -> b) -> u:(Maybe a) -> {w:b | not (isJust u) => w == v}+assume isNothing :: v:(Maybe a) -> {b:Bool | not (isJust v) == b}+assume fromMaybe :: v:a -> u:(Maybe a) -> {x:a | not (isJust u) => x == v}++assume isJust :: v:(Maybe a) -> {b:Bool | b == isJust v}+measure isJust :: Maybe a -> Bool+ isJust (Just x) = true+ isJust (Nothing) = false++assume fromJust :: {v:(Maybe a) | isJust v} -> a+measure fromJust :: Maybe a -> a+ fromJust (Just x) = x+@-}
src/Data/Set_LHAssumptions.hs view
@@ -3,67 +3,60 @@ module Data.Set_LHAssumptions where import Data.Set+import Data.Set.Internal as I import GHC.Types_LHAssumptions()+import Prelude hiding (null) {-@ -embed Data.Set.Internal.Set as Set_Set--// -----------------------------------------------------------------------------------------------// -- | Logical Set Operators: Interpreted "natively" by the SMT solver --------------------------// -------------------------------------------------------------------------------------------------// union-measure Set_cup :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)--// intersection-measure Set_cap :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)--// difference-measure Set_dif :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)--// singleton-measure Set_sng :: a -> (Data.Set.Internal.Set a)--// emptiness test-measure Set_emp :: (Data.Set.Internal.Set a) -> GHC.Types.Bool--// empty set-measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Internal.Set a)--// membership test-measure Set_mem :: a -> (Data.Set.Internal.Set a) -> GHC.Types.Bool--// inclusion test-measure Set_sub :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> GHC.Types.Bool+embed Set as Set_Set // --------------------------------------------------------------------------------------------- // -- | Refined Types for Data.Set Operations -------------------------------------------------- // --------------------------------------------------------------------------------------------- -assume Data.Set.Internal.isSubsetOf :: (GHC.Classes.Ord a) => x:(Data.Set.Internal.Set a) -> y:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_sub x y}-assume Data.Set.Internal.member :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_mem x xs}-assume Data.Set.Internal.null :: (GHC.Classes.Ord a) => xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_emp xs}+assume isSubsetOf :: (Ord a) => x:(Set a) -> y:(Set a) -> {v:Bool | v <=> Set_sub x y}+assume member :: Ord a => x:a -> xs:(Set a) -> {v:Bool | v <=> Set_mem x xs}+assume null :: Ord a => xs:(Set a) -> {v:Bool | v <=> Set_emp xs} -assume Data.Set.Internal.empty :: {v:(Data.Set.Internal.Set a) | Set_emp v}-assume Data.Set.Internal.singleton :: x:a -> {v:(Data.Set.Internal.Set a) | v = (Set_sng x)}-assume Data.Set.Internal.insert :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cup xs (Set_sng x)}-assume Data.Set.Internal.delete :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_dif xs (Set_sng x)}+assume empty :: {v:(Set a) | Set_emp v}+assume singleton :: x:a -> {v:(Set a) | v = (Set_sng x)}+assume insert :: Ord a => x:a -> xs:(Set a) -> {v:(Set a) | v = Set_cup xs (Set_sng x)}+assume delete :: (Ord a) => x:a -> xs:(Set a) -> {v:(Set a) | v = Set_dif xs (Set_sng x)} -assume Data.Set.Internal.union :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cup xs ys}-assume Data.Set.Internal.intersection :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cap xs ys}-assume Data.Set.Internal.difference :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_dif xs ys}+assume union :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_cup xs ys}+assume intersection :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_cap xs ys}+assume difference :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_dif xs ys} -assume Data.Set.Internal.fromList :: GHC.Classes.Ord a => xs:[a] -> {v:Data.Set.Internal.Set a | v = listElts xs}-assume Data.Set.Internal.toList :: GHC.Classes.Ord a => s:Data.Set.Internal.Set a -> {xs:[a] | s = listElts xs}+assume fromList :: Ord a => xs:[a] -> {v:Set a | v = listElts xs}+assume toList :: Ord a => s:Set a -> {xs:[a] | s = listElts xs} // --------------------------------------------------------------------------------------------- // -- | The set of elements in a list ---------------------------------------------------------- // --------------------------------------------------------------------------------------------- -measure listElts :: [a] -> (Data.Set.Internal.Set a)+measure listElts :: [a] -> Set a listElts [] = {v | (Set_emp v)} listElts (x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }++define singleton x = (Set_sng x)+define union x y = (Set_cup x y)+define intersection x y = (Set_cap x y)+define difference x y = (Set_dif x y)+define empty = (Set_empty 0)+define null x = (Set_emp x)+define member x xs = (Set_mem x xs)+define isSubsetOf x y = (Set_sub x y)+define fromList xs = (Data.Set_LHAssumptions.listElts xs)++define I.singleton x = (Set_sng x)+define I.union x y = (Set_cup x y)+define I.intersection x y = (Set_cap x y)+define I.difference x y = (Set_dif x y)+define I.empty = (Set_empty 0)+define I.null x = (Set_emp x)+define I.member x xs = (Set_mem x xs)+define I.isSubsetOf x y = (Set_sub x y)+define I.fromList xs = (Data.Set_LHAssumptions.listElts xs) @-}
src/Data/String_LHAssumptions.hs view
@@ -6,10 +6,10 @@ import GHC.Types_LHAssumptions() {-@-measure stringlen :: a -> GHC.Types.Int+measure stringlen :: a -> Int -assume GHC.Internal.Data.String.fromString- :: forall a. GHC.Internal.Data.String.IsString a- => i : [GHC.Types.Char]+assume fromString+ :: forall a. IsString a+ => i : [Char] -> { o : a | i ~~ o && len i == stringlen o } @-}
src/Data/Tuple_LHAssumptions.hs view
@@ -5,8 +5,8 @@ import Data.Tuple {-@-assume GHC.Internal.Data.Tuple.fst :: {f:(x:(a,b) -> {v:a | v = (fst x)}) | f == fst }-assume GHC.Internal.Data.Tuple.snd :: {f:(x:(a,b) -> {v:b | v = (snd x)}) | f == snd }+assume fst :: {f:(x:(a,b) -> {v:a | v = (fst x)}) | f == fst }+assume snd :: {f:(x:(a,b) -> {v:b | v = (snd x)}) | f == snd } measure fst :: (a, b) -> a fst (a, b) = a
src/Data/Word_LHAssumptions.hs view
@@ -1,4 +1,4 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} module Data.Word_LHAssumptions where -import GHC.Internal.Word_LHAssumptions()+import GHC.Word_LHAssumptions()
src/Foreign/C/String_LHAssumptions.hs view
@@ -8,12 +8,12 @@ import GHC.Types_LHAssumptions() {-@-type CStringLen = ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), Nat)<{\p v -> (v <= (plen p))}>-type CStringLenN N = ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), {v:Nat | v = N})<{\p v -> (v <= (plen p))}>+type CStringLen = ((Ptr CChar), Nat)<{\p v -> (v <= (plen p))}>+type CStringLenN N = ((Ptr CChar), {v:Nat | v = N})<{\p v -> (v <= (plen p))}> -// measure cStringLen :: GHC.Internal.Foreign.C.String.CStringLen -> GHC.Types.Int-measure cStringLen :: ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int+// measure cStringLen :: CStringLen -> Int+measure cStringLen :: ((Ptr CChar), Int) -> Int -// measure cStringLen :: ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int +// measure cStringLen :: ((Ptr CChar), Int) -> Int // cStringLen (c, n) = n @-}
src/Foreign/C/Types_LHAssumptions.hs view
@@ -1,12 +1,14 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module Foreign.C.Types_LHAssumptions where +import Foreign.C.Types import GHC.Int_LHAssumptions() {-@ -embed Foreign.C.Types.CInt as int-embed Foreign.C.Types.CSize as int-embed Foreign.C.Types.CULong as int+embed CInt as int+embed CSize as int+embed CULong as int @-}
src/Foreign/Concurrent_LHAssumptions.hs view
@@ -6,5 +6,5 @@ import GHC.ForeignPtr_LHAssumptions() {-@-assume GHC.Internal.Foreign.Concurrent.newForeignPtr :: p:(PtrV a) -> GHC.Types.IO () -> (GHC.Types.IO (ForeignPtrN a (plen p)))+assume newForeignPtr :: p:(PtrV a) -> IO () -> (IO (ForeignPtrN a (plen p))) @-}
src/Foreign/ForeignPtr_LHAssumptions.hs view
@@ -4,15 +4,16 @@ import Foreign.Concurrent_LHAssumptions() import Foreign.ForeignPtr+import GHC.ForeignPtr import GHC.ForeignPtr_LHAssumptions() {-@ -assume GHC.Internal.ForeignPtr.withForeignPtr :: forall a b. fp:(GHC.Internal.ForeignPtr.ForeignPtr a)- -> ((PtrN a (fplen fp)) -> GHC.Types.IO b)- -> (GHC.Types.IO b)+assume withForeignPtr :: forall a b. fp:(ForeignPtr a)+ -> ((PtrN a (fplen fp)) -> IO b)+ -> IO b -assume GHC.Internal.Foreign.ForeignPtr.Imp.newForeignPtr :: _ -> p:(PtrV a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))+assume newForeignPtr :: _ -> p:(PtrV a) -> (IO (ForeignPtrN a (plen p))) // this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`
src/Foreign/Marshal/Alloc_LHAssumptions.hs view
@@ -7,5 +7,5 @@ import Foreign.Marshal.Alloc {-@-assume GHC.Internal.Foreign.Marshal.Alloc.allocaBytes :: n:Nat -> (PtrN a n -> IO b) -> IO b+assume allocaBytes :: n:Nat -> (PtrN a n -> IO b) -> IO b @-}
src/Foreign/Ptr_LHAssumptions.hs view
@@ -1,10 +1,13 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module Foreign.Ptr_LHAssumptions where +import Foreign.Ptr+import GHC.Ptr_LHAssumptions () {-@ -invariant {v:Foreign.Ptr.Ptr a | 0 <= plen v }-invariant {v:Foreign.Ptr.Ptr a | 0 <= pbase v }+invariant {v:Ptr a | 0 <= plen v }+invariant {v:Ptr a | 0 <= pbase v } @-}
src/Foreign/Storable_LHAssumptions.hs view
@@ -4,27 +4,28 @@ import GHC.Ptr_LHAssumptions() import Foreign.Storable+import GHC.Ptr {-@ predicate PValid P N = ((0 <= N) && (N < (plen P))) -assume GHC.Internal.Foreign.Storable.poke :: (GHC.Internal.Foreign.Storable.Storable a)- => {v: (GHC.Internal.Ptr.Ptr a) | 0 < (plen v)}+assume poke :: (Storable a)+ => {v: (Ptr a) | 0 < (plen v)} -> a- -> (GHC.Types.IO ())+ -> (IO ()) -assume GHC.Internal.Foreign.Storable.peek :: (GHC.Internal.Foreign.Storable.Storable a)- => p:{v: (GHC.Internal.Ptr.Ptr a) | 0 < (plen v)}- -> (GHC.Types.IO {v:a | v = (deref p)})+assume peek :: (Storable a)+ => p:{v: (Ptr a) | 0 < (plen v)}+ -> (IO {v:a | v = (deref p)}) -assume GHC.Internal.Foreign.Storable.peekByteOff :: (GHC.Internal.Foreign.Storable.Storable a)- => forall b. p:(GHC.Internal.Ptr.Ptr b)- -> {v:GHC.Types.Int | (PValid p v)}- -> (GHC.Types.IO a)+assume peekByteOff :: (Storable a)+ => forall b. p:(Ptr b)+ -> {v:Int | (PValid p v)}+ -> (IO a) -assume GHC.Internal.Foreign.Storable.pokeByteOff :: (GHC.Internal.Foreign.Storable.Storable a)- => forall b. p:(GHC.Internal.Ptr.Ptr b)- -> {v:GHC.Types.Int | (PValid p v)}+assume pokeByteOff :: (Storable a)+ => forall b. p:(Ptr b)+ -> {v:Int | (PValid p v)} -> a- -> GHC.Types.IO ()+ -> IO () @-}
src/GHC/Base_LHAssumptions.hs view
@@ -1,4 +1,64 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Base_LHAssumptions where -import GHC.Internal.Base_LHAssumptions()+import GHC.Base (assert)+import GHC.CString_LHAssumptions()+import GHC.Exts_LHAssumptions()+import GHC.Types_LHAssumptions()+import Data.Tuple_LHAssumptions()++{-@ LIQUID "--higherorder" @-}+{-@ reflect comp @-}+{-@ assume reflect . as comp @-}+comp :: (b -> c) -> (a -> b) -> a -> c+comp f g x = f (g x)+++{-@++assume . :: forall <p :: b -> c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>.+ {xcmp::a, wcmp::b<q xcmp> |- c<p wcmp> <: c<r xcmp>}+ (ycmp:b -> c<p ycmp>)+ -> (zcmp:a -> b<q zcmp>)+ -> xcmp:a -> c<r xcmp>++measure autolen :: forall a. a -> Int++// Useless as compiled into GHC primitive, which is ignored+assume assert :: {v:Bool | v } -> a -> a++instance measure len :: forall a. [a] -> Int+ len [] = 0+ len (y:ys) = 1 + len ys++invariant {v: [a] | len v >= 0 }+assume map :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}+assume ++ :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}++assume $ :: (a -> b) -> a -> b+define $ f x = (f x)++assume id :: x:a -> {v:a | v = x}++qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs > 0))+qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs = 0))++qualif ListZ(v: [a]) : (len v = 0)+qualif ListZ(v: [a]) : (len v >= 0)+qualif ListZ(v: [a]) : (len v > 0)++qualif CmpLen(v:[a], xs:[b]) : (len v = len xs )+qualif CmpLen(v:[a], xs:[b]) : (len v >= len xs )+qualif CmpLen(v:[a], xs:[b]) : (len v > len xs )+qualif CmpLen(v:[a], xs:[b]) : (len v <= len xs )+qualif CmpLen(v:[a], xs:[b]) : (len v < len xs )++qualif EqLen(v:int, xs: [a]) : (v = len xs )+qualif LenEq(v:[a], x: int) : (x = len v )++qualif LenDiff(v:[a], x:int) : (len v = x + 1)+qualif LenDiff(v:[a], x:int) : (len v = x - 1)+qualif LenAcc(v:int, xs:[a], n: int): (v = len xs + n)++@-}
src/GHC/CString_LHAssumptions.hs view
@@ -1,17 +1,19 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} {-# LANGUAGE MagicHash #-} {-# OPTIONS_GHC -Wno-missing-signatures #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.CString_LHAssumptions() where import GHC.CString+import GHC.Prim import GHC.Types_LHAssumptions() _f = unpackCString# {-@-measure strLen :: Addr# -> GHC.Types.Int- assume GHC.CString.unpackCString#- :: x:GHC.Prim.Addr#- -> {v:[GHC.Types.Char] | v ~~ x && len v == strLen x}+ :: x:Addr#+ -> {v:[Char] | v ~~ x && len v == strLen x}++define unpackCString# x = x @-}
src/GHC/Classes_LHAssumptions.hs view
@@ -1,36 +1,37 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Classes_LHAssumptions where -import GHC.Classes()-import GHC.Types() import GHC.Types_LHAssumptions() {-@ -assume GHC.Classes.not :: x:GHC.Types.Bool -> {v:GHC.Types.Bool | ((v) <=> ~(x))}-assume (GHC.Classes.&&) :: x:GHC.Types.Bool -> y:GHC.Types.Bool- -> {v:GHC.Types.Bool | ((v) <=> ((x) && (y)))}-assume (GHC.Classes.||) :: x:GHC.Types.Bool -> y:GHC.Types.Bool- -> {v:GHC.Types.Bool | ((v) <=> ((x) || (y)))}-assume (GHC.Classes.==) :: (GHC.Classes.Eq a) => x:a -> y:a- -> {v:GHC.Types.Bool | ((v) <=> x = y)}-assume (GHC.Classes./=) :: (GHC.Classes.Eq a) => x:a -> y:a- -> {v:GHC.Types.Bool | ((v) <=> x != y)}-assume (GHC.Classes.>) :: (GHC.Classes.Ord a) => x:a -> y:a- -> {v:GHC.Types.Bool | ((v) <=> x > y)}-assume (GHC.Classes.>=) :: (GHC.Classes.Ord a) => x:a -> y:a- -> {v:GHC.Types.Bool | ((v) <=> x >= y)}-assume (GHC.Classes.<) :: (GHC.Classes.Ord a) => x:a -> y:a- -> {v:GHC.Types.Bool | ((v) <=> x < y)}-assume (GHC.Classes.<=) :: (GHC.Classes.Ord a) => x:a -> y:a- -> {v:GHC.Types.Bool | ((v) <=> x <= y)}+assume not :: x:Bool -> {v:Bool | ((v) <=> ~(x))}+define not x = (~ x) -assume GHC.Classes.compare :: (GHC.Classes.Ord a) => x:a -> y:a- -> {v:GHC.Types.Ordering | (((v = GHC.Types.EQ) <=> (x = y)) &&- ((v = GHC.Types.LT) <=> (x < y)) &&- ((v = GHC.Types.GT) <=> (x > y))) }+assume && :: x:Bool -> y:Bool+ -> {v:Bool | ((v) <=> ((x) && (y)))}+assume || :: x:Bool -> y:Bool+ -> {v:Bool | ((v) <=> ((x) || (y)))}+assume == :: (Eq a) => x:a -> y:a+ -> {v:Bool | ((v) <=> x = y)}+assume /= :: (Eq a) => x:a -> y:a+ -> {v:Bool | ((v) <=> x != y)}+assume > :: (Ord a) => x:a -> y:a+ -> {v:Bool | ((v) <=> x > y)}+assume >= :: (Ord a) => x:a -> y:a+ -> {v:Bool | ((v) <=> x >= y)}+assume < :: (Ord a) => x:a -> y:a+ -> {v:Bool | ((v) <=> x < y)}+assume <= :: (Ord a) => x:a -> y:a+ -> {v:Bool | ((v) <=> x <= y)} -assume GHC.Classes.max :: (GHC.Classes.Ord a) => x:a -> y:a -> {v:a | v = (if x > y then x else y) }-assume GHC.Classes.min :: (GHC.Classes.Ord a) => x:a -> y:a -> {v:a | v = (if x < y then x else y) }+assume compare :: (Ord a) => x:a -> y:a+ -> {v:Ordering | (((v = EQ) <=> (x = y)) &&+ ((v = LT) <=> (x < y)) &&+ ((v = GT) <=> (x > y))) }++assume max :: (Ord a) => x:a -> y:a -> {v:a | v = (if x > y then x else y) }+assume min :: (Ord a) => x:a -> y:a -> {v:a | v = (if x < y then x else y) } @-}
src/GHC/Exts_LHAssumptions.hs view
@@ -3,16 +3,17 @@ module GHC.Exts_LHAssumptions where import GHC.Base+import GHC.Prim import GHC.Types_LHAssumptions() {-@ -assume GHC.Prim.+# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x + y}-assume GHC.Prim.-# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x - y}-assume GHC.Prim.==# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x = y}-assume GHC.Prim.>=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x >= y}-assume GHC.Prim.<=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x <= y}-assume GHC.Prim.<# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x < y}-assume GHC.Prim.># :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x > y}+assume GHC.Prim.+# :: x:Int# -> y:Int# -> {v: Int# | v = x + y}+assume GHC.Prim.-# :: x:Int# -> y:Int# -> {v: Int# | v = x - y}+assume GHC.Prim.==# :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x = y}+assume GHC.Prim.>=# :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x >= y}+assume GHC.Prim.<=# :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x <= y}+assume GHC.Prim.<# :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x < y}+assume GHC.Prim.># :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x > y} @-}
src/GHC/Float_LHAssumptions.hs view
@@ -1,5 +1,31 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} {-# OPTIONS_GHC -Wno-unused-imports #-}-module GHC.Float_LHAssumptions where+module GHC.Float_LHAssumptions(Floating(..)) where -import GHC.Internal.Float_LHAssumptions+import GHC.Float++{-@+class Fractional a => Floating a where+ pi :: a+ exp :: a -> {y:a | y > 0}+ log :: {x:a | x > 0} -> a+ sqrt :: {x:a | x >= 0} -> {y:a | y >= 0}+ (**) :: x:a -> {y:a | x = 0 => y >= 0} -> a+ logBase :: {b:a | b > 0 && b /= 1} -> {x:a | x > 0} -> a+ sin :: a -> {y:a | -1 <= y && y <= 1}+ cos :: a -> {y:a | -1 <= y && y <= 1}+ tan :: a -> a+ asin :: {x:a | -1 <= x && x <= 1} -> a+ acos :: {x:a | -1 <= x && x <= 1} -> a+ atan :: a -> a+ sinh :: a -> a+ cosh :: a -> {y:a | y >= 1}+ tanh :: a -> {y:a | -1 < y && y < 1}+ asinh :: a -> a+ acosh :: {y:a | y >= 1} -> a+ atanh :: {y:a | -1 < y && y < 1} -> a+ log1p :: a -> a+ expm1 :: a -> a+ log1pexp :: a -> a+ log1mexp :: a -> a+@-}
src/GHC/ForeignPtr_LHAssumptions.hs view
@@ -3,14 +3,15 @@ module GHC.ForeignPtr_LHAssumptions where import GHC.ForeignPtr+import GHC.Ptr import GHC.Ptr_LHAssumptions() {-@-measure fplen :: GHC.Internal.ForeignPtr.ForeignPtr a -> GHC.Types.Int+measure fplen :: ForeignPtr a -> Int -type ForeignPtrV a = {v: GHC.Internal.ForeignPtr.ForeignPtr a | 0 <= fplen v}-type ForeignPtrN a N = {v: GHC.Internal.ForeignPtr.ForeignPtr a | 0 <= fplen v && fplen v == N }+type ForeignPtrV a = {v: ForeignPtr a | 0 <= fplen v}+type ForeignPtrN a N = {v: ForeignPtr a | 0 <= fplen v && fplen v == N } -assume GHC.Internal.ForeignPtr.newForeignPtr_ :: p:(GHC.Internal.Ptr.Ptr a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))-assume GHC.Internal.ForeignPtr.mallocPlainForeignPtrBytes :: n:{v:GHC.Types.Int | v >= 0 } -> (GHC.Types.IO (ForeignPtrN a n))+assume newForeignPtr_ :: p:(Ptr a) -> (IO (ForeignPtrN a (plen p)))+assume mallocPlainForeignPtrBytes :: n:{v:Int | v >= 0 } -> (IO (ForeignPtrN a n)) @-}
src/GHC/IO/Handle_LHAssumptions.hs view
@@ -3,15 +3,16 @@ module GHC.IO.Handle_LHAssumptions where import GHC.IO.Handle+import GHC.Ptr import GHC.Types_LHAssumptions() {-@-assume GHC.Internal.IO.Handle.Text.hGetBuf :: GHC.Internal.IO.Handle.Handle -> GHC.Internal.Ptr.Ptr a -> n:Nat- -> (GHC.Types.IO {v:Nat | v <= n})+assume hGetBuf :: Handle -> Ptr a -> n:Nat+ -> (IO {v:Nat | v <= n}) -assume GHC.Internal.IO.Handle.Text.hGetBufNonBlocking :: GHC.Internal.IO.Handle.Handle -> GHC.Internal.Ptr.Ptr a -> n:Nat- -> (GHC.Types.IO {v:Nat | v <= n})+assume hGetBufNonBlocking :: Handle -> Ptr a -> n:Nat+ -> (IO {v:Nat | v <= n}) -assume GHC.Internal.IO.Handle.hFileSize :: GHC.Internal.IO.Handle.Handle- -> (GHC.Types.IO {v:Integer | v >= 0})+assume hFileSize :: Handle+ -> (IO {v:Integer | v >= 0}) @-}
src/GHC/Int_LHAssumptions.hs view
@@ -5,10 +5,10 @@ import GHC.Int {-@-embed GHC.Internal.Int.Int8 as int-embed GHC.Internal.Int.Int16 as int-embed GHC.Internal.Int.Int32 as int-embed GHC.Internal.Int.Int64 as int+embed Int8 as int+embed Int16 as int+embed Int32 as int+embed Int64 as int -type Nat64 = {v:GHC.Internal.Int.Int64 | v >= 0}+type Nat64 = {v:Int64 | v >= 0} @-}
− src/GHC/Internal/Base_LHAssumptions.hs
@@ -1,55 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-{-# OPTIONS_GHC -Wno-unused-imports #-}-module GHC.Internal.Base_LHAssumptions where--import GHC.CString_LHAssumptions()-import GHC.Exts_LHAssumptions()-import GHC.Types_LHAssumptions()-import GHC.Internal.Base-import Data.Tuple_LHAssumptions()--{-@--assume GHC.Internal.Base.. :: forall <p :: b -> c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>.- {xcmp::a, wcmp::b<q xcmp> |- c<p wcmp> <: c<r xcmp>}- (ycmp:b -> c<p ycmp>)- -> (zcmp:a -> b<q zcmp>)- -> xcmp:a -> c<r xcmp>--measure autolen :: forall a. a -> GHC.Types.Int--// Useless as compiled into GHC primitive, which is ignored-assume GHC.Internal.Base.assert :: {v:Bool | v } -> a -> a--instance measure len :: forall a. [a] -> GHC.Types.Int- len [] = 0- len (y:ys) = 1 + len ys--invariant {v: [a] | len v >= 0 }-assume GHC.Internal.Base.map :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}-assume GHC.Internal.Base.++ :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}--assume (GHC.Internal.Base.$) :: (a -> b) -> a -> b-assume GHC.Internal.Base.id :: x:a -> {v:a | v = x}--qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs > 0))-qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs = 0))--qualif ListZ(v: [a]) : (len v = 0)-qualif ListZ(v: [a]) : (len v >= 0)-qualif ListZ(v: [a]) : (len v > 0)--qualif CmpLen(v:[a], xs:[b]) : (len v = len xs )-qualif CmpLen(v:[a], xs:[b]) : (len v >= len xs )-qualif CmpLen(v:[a], xs:[b]) : (len v > len xs )-qualif CmpLen(v:[a], xs:[b]) : (len v <= len xs )-qualif CmpLen(v:[a], xs:[b]) : (len v < len xs )--qualif EqLen(v:int, xs: [a]) : (v = len xs )-qualif LenEq(v:[a], x: int) : (x = len v )--qualif LenDiff(v:[a], x:int) : (len v = x + 1)-qualif LenDiff(v:[a], x:int) : (len v = x - 1)-qualif LenAcc(v:int, xs:[a], n: int): (v = len xs + n)--@-}
− src/GHC/Internal/Data/Foldable_LHAssumptions.hs
@@ -1,9 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-module GHC.Internal.Data.Foldable_LHAssumptions where--import GHC.Types_LHAssumptions()--{-@-assume GHC.Internal.Data.Foldable.length :: GHC.Internal.Data.Foldable.Foldable f => forall a. xs:f a -> {v:Nat | v = len xs}-assume GHC.Internal.Data.Foldable.null :: GHC.Internal.Data.Foldable.Foldable f => forall a. v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)}-@-}
− src/GHC/Internal/Data/Maybe_LHAssumptions.hs
@@ -1,21 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-{-# OPTIONS_GHC -Wno-unused-imports #-}-module GHC.Internal.Data.Maybe_LHAssumptions where--import GHC.Types_LHAssumptions()-import Data.Maybe--{-@-assume GHC.Internal.Data.Maybe.maybe :: v:b -> (a -> b) -> u:(GHC.Internal.Maybe.Maybe a) -> {w:b | not (isJust u) => w == v}-assume GHC.Internal.Data.Maybe.isNothing :: v:(GHC.Internal.Maybe.Maybe a) -> {b:Bool | not (isJust v) == b}-assume GHC.Internal.Data.Maybe.fromMaybe :: v:a -> u:(GHC.Internal.Maybe.Maybe a) -> {x:a | not (isJust u) => x == v}--assume GHC.Internal.Data.Maybe.isJust :: v:(GHC.Internal.Maybe.Maybe a) -> {b:Bool | b == isJust v}-measure isJust :: GHC.Internal.Maybe.Maybe a -> Bool- isJust (GHC.Internal.Maybe.Just x) = true- isJust (GHC.Internal.Maybe.Nothing) = false--assume GHC.Internal.Data.Maybe.fromJust :: {v:(GHC.Internal.Maybe.Maybe a) | isJust v} -> a-measure fromJust :: GHC.Internal.Maybe.Maybe a -> a- fromJust (GHC.Internal.Maybe.Just x) = x-@-}
− src/GHC/Internal/Float_LHAssumptions.hs
@@ -1,28 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-module GHC.Internal.Float_LHAssumptions(Floating(..)) where--{-@-class (GHC.Internal.Real.Fractional a) => GHC.Internal.Float.Floating a where- GHC.Internal.Float.pi :: a- GHC.Internal.Float.exp :: a -> {y:a | y > 0}- GHC.Internal.Float.log :: {x:a | x > 0} -> a- GHC.Internal.Float.sqrt :: {x:a | x >= 0} -> {y:a | y >= 0}- (GHC.Internal.Float.**) :: x:a -> {y:a | x = 0 => y >= 0} -> a- GHC.Internal.Float.logBase :: {b:a | b > 0 && b /= 1} -> {x:a | x > 0} -> a- GHC.Internal.Float.sin :: a -> {y:a | -1 <= y && y <= 1}- GHC.Internal.Float.cos :: a -> {y:a | -1 <= y && y <= 1}- GHC.Internal.Float.tan :: a -> a- GHC.Internal.Float.asin :: {x:a | -1 <= x && x <= 1} -> a- GHC.Internal.Float.acos :: {x:a | -1 <= x && x <= 1} -> a- GHC.Internal.Float.atan :: a -> a- GHC.Internal.Float.sinh :: a -> a- GHC.Internal.Float.cosh :: a -> {y:a | y >= 1}- GHC.Internal.Float.tanh :: a -> {y:a | -1 < y && y < 1}- GHC.Internal.Float.asinh :: a -> a- GHC.Internal.Float.acosh :: {y:a | y >= 1} -> a- GHC.Internal.Float.atanh :: {y:a | -1 < y && y < 1} -> a- GHC.Internal.Float.log1p :: a -> a- GHC.Internal.Float.expm1 :: a -> a- GHC.Internal.Float.log1pexp :: a -> a- GHC.Internal.Float.log1mexp :: a -> a-@-}
− src/GHC/Internal/Int_LHAssumptions.hs
@@ -1,10 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-module GHC.Internal.Int_LHAssumptions where--{-@-embed GHC.Internal.Int.Int8 as int-embed GHC.Internal.Int.Int16 as int-embed GHC.Internal.Int.Int32 as int-embed GHC.Internal.Int.Int64 as int--@-}
− src/GHC/Internal/List_LHAssumptions.hs
@@ -1,70 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-{-# OPTIONS_GHC -Wno-unused-imports #-}-module GHC.Internal.List_LHAssumptions where--import GHC.List-import GHC.Types_LHAssumptions()--{-@--assume GHC.Internal.List.head :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs}-assume GHC.Internal.List.tail :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs}--assume GHC.Internal.List.last :: xs:{v: [a] | len v > 0} -> a-assume GHC.Internal.List.init :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1}-assume GHC.Internal.List.null :: xs:[a] -> {v: GHC.Types.Bool | ((v) <=> len(xs) = 0) }-assume GHC.Internal.List.length :: xs:[a] -> {v: GHC.Types.Int | v = len(xs)}-assume GHC.Internal.List.filter :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}-assume GHC.Internal.List.scanl :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) }-assume GHC.Internal.List.scanl1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }-assume GHC.Internal.List.foldr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a-assume GHC.Internal.List.scanr :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) }-assume GHC.Internal.List.scanr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }--lazy GHC.Internal.List.iterate-assume GHC.Internal.List.iterate :: (a -> a) -> a -> [a]--assume GHC.Internal.List.repeat :: a -> [a]-lazy GHC.Internal.List.repeat--assume GHC.Internal.List.replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n}--assume GHC.Internal.List.cycle :: {v: [a] | len(v) > 0 } -> [a]-lazy GHC.Internal.List.cycle--assume GHC.Internal.List.takeWhile :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}-assume GHC.Internal.List.dropWhile :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}--assume GHC.Internal.List.take :: n:GHC.Types.Int- -> xs:[a]- -> {v:[a] | if n >= 0 then (len v = (if (len xs) < n then (len xs) else n)) else (len v = 0)}-assume GHC.Internal.List.drop :: n:GHC.Types.Int- -> xs:[a]- -> {v:[a] | (if (n >= 0) then (len(v) = (if (len(xs) < n) then 0 else len(xs) - n)) else ((len v) = (len xs)))}--assume GHC.Internal.List.splitAt :: n:_ -> x:[a] -> ({v:[a] | (if (n >= 0) then (if (len x) < n then (len v) = (len x) else (len v) = n) else ((len v) = 0))},[a])<{\x1 x2 -> (len x2) = (len x) - (len x1)}>-assume GHC.Internal.List.span :: (a -> GHC.Types.Bool)- -> xs:[a]- -> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))})--assume GHC.Internal.List.break :: (a -> GHC.Types.Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}>--assume GHC.Internal.List.reverse :: xs:[a] -> {v: [a] | len(v) = len(xs)}--// Copy-pasted from len.hquals-qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys]))-qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))--assume GHC.Internal.List.!! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a---assume GHC.Internal.List.zip :: xs : [a] -> ys:[b]- -> {v : [(a, b)] | ((((len v) <= (len xs)) && ((len v) <= (len ys)))- && (((len xs) = (len ys)) => ((len v) = (len xs))) )}--assume GHC.Internal.List.zipWith :: (a -> b -> c)- -> xs : [a] -> ys:[b]- -> {v : [c] | (((len v) <= (len xs)) && ((len v) <= (len ys)))}--assume GHC.Internal.List.errorEmptyList :: {v: _ | false} -> a-@-}
− src/GHC/Internal/Num_LHAssumptions.hs
@@ -1,17 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-module GHC.Internal.Num_LHAssumptions where--import GHC.Num.Integer_LHAssumptions()--{-@-assume GHC.Internal.Num.fromInteger :: x:GHC.Num.Integer.Integer -> {v:a | v = x }--assume GHC.Internal.Num.negate :: (GHC.Internal.Num.Num a)- => x:a- -> {v:a | v = -x}--assume GHC.Internal.Num.abs :: (GHC.Internal.Num.Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) }--assume GHC.Internal.Num.+ :: x:a -> y:a -> {v:a | v = x + y }-assume GHC.Internal.Num.- :: (GHC.Internal.Num.Num a) => x:a -> y:a -> {v:a | v = x - y }-@-}
− src/GHC/Internal/Word_LHAssumptions.hs
@@ -1,13 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-module GHC.Internal.Word_LHAssumptions where--{-@-embed GHC.Internal.Word.Word as int-embed GHC.Internal.Word.Word8 as int-embed GHC.Internal.Word.Word16 as int-embed GHC.Internal.Word.Word32 as int-embed GHC.Internal.Word.Word64 as int--invariant {v : GHC.Internal.Word.Word32 | 0 <= v }-invariant {v : GHC.Internal.Word.Word16 | 0 <= v }-@-}
src/GHC/List_LHAssumptions.hs view
@@ -2,4 +2,69 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.List_LHAssumptions where -import GHC.Internal.List_LHAssumptions()+import GHC.List+import GHC.Types_LHAssumptions()+import Prelude hiding (foldr1, length, null)++{-@+assume head :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs}+assume tail :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs}++assume last :: xs:{v: [a] | len v > 0} -> a+assume init :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1}+assume null :: xs:[a] -> {v: Bool | ((v) <=> len(xs) = 0) }+assume length :: xs:[a] -> {v: Int | v = len(xs)}+assume filter :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}+assume scanl :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) }+assume scanl1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }+assume foldr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a+assume scanr :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) }+assume scanr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }++lazy iterate+assume iterate :: (a -> a) -> a -> [a]++assume repeat :: a -> [a]+lazy repeat++assume replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n}++assume cycle :: {v: [a] | len(v) > 0 } -> [a]+lazy cycle++assume takeWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}+assume dropWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}++assume take :: n:Int+ -> xs:[a]+ -> {v:[a] | if n >= 0 then (len v = (if (len xs) < n then (len xs) else n)) else (len v = 0)}+assume drop :: n:Int+ -> xs:[a]+ -> {v:[a] | (if (n >= 0) then (len(v) = (if (len(xs) < n) then 0 else len(xs) - n)) else ((len v) = (len xs)))}++assume splitAt :: n:_ -> x:[a] -> ({v:[a] | (if (n >= 0) then (if (len x) < n then (len v) = (len x) else (len v) = n) else ((len v) = 0))},[a])<{\x1 x2 -> (len x2) = (len x) - (len x1)}>+assume span :: (a -> Bool)+ -> xs:[a]+ -> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))})++assume break :: (a -> Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}>++assume reverse :: xs:[a] -> {v: [a] | len(v) = len(xs)}++// Copy-pasted from len.hquals+qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys]))+qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))++assume !! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a+++assume zip :: xs : [a] -> ys:[b]+ -> {v : [(a, b)] | ((((len v) <= (len xs)) && ((len v) <= (len ys)))+ && (((len xs) = (len ys)) => ((len v) = (len xs))) )}++assume zipWith :: (a -> b -> c)+ -> xs : [a] -> ys:[b]+ -> {v : [c] | (((len v) <= (len xs)) && ((len v) <= (len ys)))}++assume errorEmptyList :: {v: _ | false} -> a+@-}
src/GHC/Num/Integer_LHAssumptions.hs view
@@ -3,12 +3,12 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Num.Integer_LHAssumptions() where -import GHC.Types+import GHC.Prim import GHC.Num.Integer import GHC.Types_LHAssumptions() {-@-assume GHC.Num.Integer.IS :: x:GHC.Prim.Int# -> {v: GHC.Num.Integer.Integer | v = (x :: int) }+assume GHC.Num.Integer.IS :: x:Int# -> {v: Integer | v = (x :: int) } -embed GHC.Num.Integer.Integer as int+embed Integer as int @-}
src/GHC/Num_LHAssumptions.hs view
@@ -1,4 +1,19 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Num_LHAssumptions where -import GHC.Internal.Num_LHAssumptions()+import GHC.Num+import GHC.Num.Integer_LHAssumptions()++{-@+assume fromInteger :: x:Integer -> {v:a | v = x }++assume negate :: (Num a)+ => x:a+ -> {v:a | v = -x}++assume abs :: (Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) }++assume + :: x:a -> y:a -> {v:a | v = x + y }+assume - :: (Num a) => x:a -> y:a -> {v:a | v = x - y }+@-}
src/GHC/Ptr_LHAssumptions.hs view
@@ -6,22 +6,22 @@ import GHC.Types_LHAssumptions() {-@-measure pbase :: GHC.Internal.Ptr.Ptr a -> GHC.Types.Int-measure plen :: GHC.Internal.Ptr.Ptr a -> GHC.Types.Int-measure isNullPtr :: GHC.Internal.Ptr.Ptr a -> Bool +measure pbase :: Ptr a -> Int+measure plen :: Ptr a -> Int+measure isNullPtr :: Ptr a -> Bool type PtrN a N = {v: PtrV a | plen v == N }-type PtrV a = {v: GHC.Internal.Ptr.Ptr a | 0 <= plen v }+type PtrV a = {v: Ptr a | 0 <= plen v } -assume GHC.Internal.Ptr.castPtr :: p:(PtrV a) -> (PtrN b (plen p))+assume castPtr :: p:(PtrV a) -> (PtrN b (plen p)) -assume GHC.Internal.Ptr.plusPtr :: base:(PtrV a)- -> off:{v:GHC.Types.Int | v <= plen base }+assume plusPtr :: base:(PtrV a)+ -> off:{v:Int | v <= plen base } -> {v:(PtrV b) | pbase v = pbase base && plen v = plen base - off} -assume GHC.Internal.Ptr.minusPtr :: q:(PtrV a)+assume minusPtr :: q:(PtrV a) -> p:{v:(PtrV b) | pbase v == pbase q && plen v >= plen q} -> {v:Nat | v == plen p - plen q} -measure deref :: GHC.Internal.Ptr.Ptr a -> a+measure deref :: Ptr a -> a @-}
src/GHC/Real_LHAssumptions.hs view
@@ -1,43 +1,54 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} -- Reexports are necessary for LH to expose specs of type classes module GHC.Real_LHAssumptions(Integral(..), Fractional(..)) where +import GHC.Real import GHC.Types_LHAssumptions() {-@-assume (GHC.Internal.Real.^) :: x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 && y /= 0) <=> z == 0)}+assume (^) :: x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 && y /= 0) <=> z == 0)} -assume GHC.Internal.Real.fromIntegral :: x:a -> {v:b|v=x}+assume fromIntegral :: x:a -> {v:b|v=x} -class (GHC.Internal.Num.Num a) => GHC.Internal.Real.Fractional a where- (GHC.Internal.Real./) :: x:a -> y:{v:a | v /= 0} -> {v:a | v == x / y}- GHC.Internal.Real.recip :: a -> a- GHC.Internal.Real.fromRational :: GHC.Internal.Real.Ratio Integer -> a+class Num a => Fractional a where+ (/) :: x:a -> y:{v:a | v /= 0} -> {v:a | v == x / y}+ recip :: a -> a+ fromRational :: Ratio Integer -> a -class (GHC.Internal.Real.Real a, GHC.Internal.Enum.Enum a) => GHC.Internal.Real.Integral a where- GHC.Internal.Real.quot :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) &&+class (Real a, Enum a) => Integral a where+ quot :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x) }- GHC.Internal.Real.rem :: x:a -> y:{v:a | v /= 0} -> {v:a | ((v >= 0) && (v < y))}- GHC.Internal.Real.mod :: x:a -> y:{v:a | v /= 0} -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))}+ rem :: x:a -> y:{v:a | v /= 0} -> {v:a | ((v >= 0) && (v < y))}+ mod :: x:a -> y:{v:a | v /= 0} -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))} - GHC.Internal.Real.div :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) &&+ div :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = div x y) && ((x >= 0 && y >= 0) => v >= 0) &&- ((x >= 0 && y >= 1) => v <= x) && - ((1 < y) => v < x ) && - ((y >= 1) => v <= x) + ((x >= 0 && y >= 1) => v <= x) &&+ ((1 < y && x >= 0) => v < x) &&+ ((1 < y && x < 0) => v > x) &&+ ((y >= 1 && x >= 0) => v <= x) &&+ ((x < 0 && y > 0) => v <= 0) &&+ ((x > 0 && y < 0) => v <= 0) &&+ ((x < 0 && y < 0) => v >= 0) }- GHC.Internal.Real.quotRem :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) &&+ quotRem :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x)} , {v:a | ((v >= 0) && (v < y))})- GHC.Internal.Real.divMod :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) &&+ divMod :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x) } , {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))} )- GHC.Internal.Real.toInteger :: x:a -> {v:Integer | v = x}+ toInteger :: x:a -> {v:Integer | v = x} // fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here // mod :: x:a -> y:a -> {v:a | v = (x mod y) }++define div x y = (x / y)+define mod x y = (x mod y)+define fromIntegral x = (x)+ @-}
src/GHC/Types_LHAssumptions.hs view
@@ -1,8 +1,10 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} {-# LANGUAGE MagicHash #-} {-# OPTIONS_GHC -Wno-missing-signatures #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Types_LHAssumptions() where +import GHC.Prim import GHC.Types -- This definition is needed to make the listed data constructors@@ -11,43 +13,46 @@ {-@ // Boxed types-embed GHC.Types.Double as real-embed GHC.Prim.Double# as real-embed GHC.Types.Float as real-embed GHC.Prim.Float# as real-embed GHC.Types.Word as int-embed GHC.Prim.Word# as int-embed GHC.Prim.Word64# as int-embed GHC.Types.Int as int-embed GHC.Prim.Int# as int-embed GHC.Types.Bool as bool-embed GHC.Types.Char as Char-embed GHC.Prim.Char# as Char-embed GHC.Prim.Addr# as Str+embed Double as real+embed Double# as real+embed Float as real+embed Float# as real+embed Word as int+embed Word# as int+embed Word64# as int+embed Int as int+embed Int# as int+embed Bool as bool+embed Char as Char+embed Char# as Char+embed Addr# as Str -embed GHC.Num.Integer.Integer as int+embed Integer as int -assume GHC.Types.True :: {v:GHC.Types.Bool | v }-assume GHC.Types.False :: {v:GHC.Types.Bool | (~ v) }-assume GHC.Types.isTrue# :: n:_ -> {v:GHC.Types.Bool | (n = 1 <=> v)}+assume True :: {v:Bool | v }+assume False :: {v:Bool | (~ v) }+assume GHC.Types.isTrue# :: n:_ -> {v:Bool | (n = 1 <=> v)} -assume GHC.Types.D# :: x:GHC.Prim.Double# -> {v: GHC.Types.Double | v = (x :: real) }-assume GHC.Types.F# :: x:GHC.Prim.Float# -> {v: GHC.Types.Float | v = (x :: real) }-assume GHC.Types.I# :: x:GHC.Prim.Int# -> {v: GHC.Types.Int | v = (x :: int) }-assume GHC.Types.C# :: x:GHC.Prim.Char# -> {v: GHC.Types.Char | v = (x :: Char) }-assume GHC.Types.W# :: w:GHC.Prim.Word# -> {v:GHC.Types.Word | v == w }+define True = (true) -measure addrLen :: GHC.Prim.Addr# -> GHC.Types.Int+assume GHC.Types.D# :: x:Double# -> {v: Double | v = (x :: real) }+assume GHC.Types.F# :: x:Float# -> {v: Float | v = (x :: real) }+assume GHC.Types.I# :: x:Int# -> {v: Int | v = (x :: int) }+assume GHC.Types.C# :: x:Char# -> {v: Char | v = (x :: Char) }+assume GHC.Types.W# :: w:Word# -> {v:Word | v == w } -type GeInt N = {v: GHC.Types.Int | v >= N }-type LeInt N = {v: GHC.Types.Int | v <= N }-type Nat = {v: GHC.Types.Int | v >= 0 }-type Even = {v: GHC.Types.Int | (v mod 2) = 0 }-type Odd = {v: GHC.Types.Int | (v mod 2) = 1 }+measure addrLen :: GHC.Prim.Addr# -> Int++type GeInt N = {v: Int | v >= N }+type LeInt N = {v: Int | v <= N }+type Nat = {v: Int | v >= 0 }+type Even = {v: Int | (v mod 2) = 0 }+type Odd = {v: Int | (v mod 2) = 1 } type BNat N = {v: Nat | v <= N }-type TT = {v: GHC.Types.Bool | v}-type FF = {v: GHC.Types.Bool | not v}-type String = [GHC.Types.Char]+type TT = {v: Bool | v}+type FF = {v: Bool | not v}+type String = [Char] -class measure len :: forall f a. f a -> GHC.Types.Int+class measure len :: forall f a. f a -> Int+ @-}
src/GHC/Word_LHAssumptions.hs view
@@ -1,4 +1,16 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Word_LHAssumptions where -import GHC.Internal.Word_LHAssumptions()+import GHC.Word++{-@+embed Word as int+embed Word8 as int+embed Word16 as int+embed Word32 as int+embed Word64 as int++invariant {v : Word32 | 0 <= v }+invariant {v : Word16 | 0 <= v }+@-}
src/Liquid/Prelude/Real_LHAssumptions.hs view
@@ -1,8 +1,7 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-} module Liquid.Prelude.Real_LHAssumptions where -import GHC.Num()- {-@-assume GHC.Internal.Num.* :: (GHC.Internal.Num.Num a) => x:a -> y:a -> {v:a | v = x * y} +assume * :: Num a => x:a -> y:a -> {v:a | v = x * y} @-}
src/Liquid/Prelude/Totality_LHAssumptions.hs view
@@ -3,17 +3,18 @@ module Liquid.Prelude.Totality_LHAssumptions where import Control.Exception.Base+import GHC.Prim {-@ measure totalityError :: a -> Bool -assume GHC.Internal.Control.Exception.Base.patError :: {v:GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a+assume patError :: {v:Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a -assume GHC.Internal.Control.Exception.Base.recSelError :: {v:GHC.Prim.Addr# | totalityError "Use of partial record field selector"} -> a+assume recSelError :: {v:Addr# | totalityError "Use of partial record field selector"} -> a -assume GHC.Internal.Control.Exception.Base.nonExhaustiveGuardsError :: {v:GHC.Prim.Addr# | totalityError "Guards are non-exhaustive"} -> a+assume nonExhaustiveGuardsError :: {v:Addr# | totalityError "Guards are non-exhaustive"} -> a -assume GHC.Internal.Control.Exception.Base.noMethodBindingError :: {v:GHC.Prim.Addr# | totalityError "Missing method(s) on instance declaration"} -> a+assume noMethodBindingError :: {v:Addr# | totalityError "Missing method(s) on instance declaration"} -> a -assume GHC.Internal.Control.Exception.Base.recConError :: {v:GHC.Prim.Addr# | totalityError "Missing field in record construction"} -> a+assume recConError :: {v:Addr# | totalityError "Missing field in record construction"} -> a @-}
src/Prelude_LHAssumptions.hs view
@@ -1,7 +1,10 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} module Prelude_LHAssumptions where +import Data.Foldable_LHAssumptions()+import Data.List_LHAssumptions() import GHC.Base_LHAssumptions()+import GHC.Classes_LHAssumptions() import GHC.Float_LHAssumptions() import GHC.Maybe_LHAssumptions() import GHC.Num_LHAssumptions()@@ -13,12 +16,12 @@ {-@ -assume GHC.Internal.Err.error :: {v:_ | false} -> a+assume error :: {v:_ | false} -> a predicate Max V X Y = if X > Y then V = X else V = Y predicate Min V X Y = if X < Y then V = X else V = Y -type IncrListD a = [a]<{\x y -> (x+D) <= y}>+type IncrListD a D = [a]<{\x y -> (x+D) <= y}> // BOT: Do not delete EVER! @@ -43,8 +46,8 @@ qualif Cmp(v:a, x:a) : (v != x) qualif One(v:int) : v = 1-qualif True1(v:GHC.Types.Bool) : (v)-qualif False1(v:GHC.Types.Bool) : (~ v)+qualif True1(v:Bool) : (v)+qualif False1(v:Bool) : (~ v) // REBARE constant papp1 : func(1, [Pred @(0); @(0); bool]) qualif Papp(v:a, p:Pred a) : (papp1 p v)