diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -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 diff --git a/src/Data/ByteString/Char8_LHAssumptions.hs b/src/Data/ByteString/Char8_LHAssumptions.hs --- a/src/Data/ByteString/Char8_LHAssumptions.hs +++ b/src/Data/ByteString/Char8_LHAssumptions.hs @@ -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 } @-} diff --git a/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs b/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs --- a/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs +++ b/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs @@ -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 } @-} diff --git a/src/Data/ByteString/Lazy_LHAssumptions.hs b/src/Data/ByteString/Lazy_LHAssumptions.hs --- a/src/Data/ByteString/Lazy_LHAssumptions.hs +++ b/src/Data/ByteString/Lazy_LHAssumptions.hs @@ -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 } @-} diff --git a/src/Data/ByteString/Short_LHAssumptions.hs b/src/Data/ByteString/Short_LHAssumptions.hs --- a/src/Data/ByteString/Short_LHAssumptions.hs +++ b/src/Data/ByteString/Short_LHAssumptions.hs @@ -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 @-} diff --git a/src/Data/ByteString/Unsafe_LHAssumptions.hs b/src/Data/ByteString/Unsafe_LHAssumptions.hs --- a/src/Data/ByteString/Unsafe_LHAssumptions.hs +++ b/src/Data/ByteString/Unsafe_LHAssumptions.hs @@ -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 } @-} diff --git a/src/Data/ByteString_LHAssumptions.hs b/src/Data/ByteString_LHAssumptions.hs --- a/src/Data/ByteString_LHAssumptions.hs +++ b/src/Data/ByteString_LHAssumptions.hs @@ -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 })) @-} diff --git a/src/Data/Either_LHAssumptions.hs b/src/Data/Either_LHAssumptions.hs --- a/src/Data/Either_LHAssumptions.hs +++ b/src/Data/Either_LHAssumptions.hs @@ -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 @-} diff --git a/src/Data/Foldable_LHAssumptions.hs b/src/Data/Foldable_LHAssumptions.hs --- a/src/Data/Foldable_LHAssumptions.hs +++ b/src/Data/Foldable_LHAssumptions.hs @@ -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)} +@-} diff --git a/src/Data/List_LHAssumptions.hs b/src/Data/List_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/Data/List_LHAssumptions.hs @@ -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() diff --git a/src/Data/Maybe_LHAssumptions.hs b/src/Data/Maybe_LHAssumptions.hs --- a/src/Data/Maybe_LHAssumptions.hs +++ b/src/Data/Maybe_LHAssumptions.hs @@ -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 +@-} diff --git a/src/Data/Set_LHAssumptions.hs b/src/Data/Set_LHAssumptions.hs --- a/src/Data/Set_LHAssumptions.hs +++ b/src/Data/Set_LHAssumptions.hs @@ -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) @-} diff --git a/src/Data/String_LHAssumptions.hs b/src/Data/String_LHAssumptions.hs --- a/src/Data/String_LHAssumptions.hs +++ b/src/Data/String_LHAssumptions.hs @@ -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 } @-} diff --git a/src/Data/Tuple_LHAssumptions.hs b/src/Data/Tuple_LHAssumptions.hs --- a/src/Data/Tuple_LHAssumptions.hs +++ b/src/Data/Tuple_LHAssumptions.hs @@ -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 diff --git a/src/Data/Word_LHAssumptions.hs b/src/Data/Word_LHAssumptions.hs --- a/src/Data/Word_LHAssumptions.hs +++ b/src/Data/Word_LHAssumptions.hs @@ -1,4 +1,4 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} module Data.Word_LHAssumptions where -import GHC.Internal.Word_LHAssumptions() +import GHC.Word_LHAssumptions() diff --git a/src/Foreign/C/String_LHAssumptions.hs b/src/Foreign/C/String_LHAssumptions.hs --- a/src/Foreign/C/String_LHAssumptions.hs +++ b/src/Foreign/C/String_LHAssumptions.hs @@ -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 @-} diff --git a/src/Foreign/C/Types_LHAssumptions.hs b/src/Foreign/C/Types_LHAssumptions.hs --- a/src/Foreign/C/Types_LHAssumptions.hs +++ b/src/Foreign/C/Types_LHAssumptions.hs @@ -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 @-} diff --git a/src/Foreign/Concurrent_LHAssumptions.hs b/src/Foreign/Concurrent_LHAssumptions.hs --- a/src/Foreign/Concurrent_LHAssumptions.hs +++ b/src/Foreign/Concurrent_LHAssumptions.hs @@ -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))) @-} diff --git a/src/Foreign/ForeignPtr_LHAssumptions.hs b/src/Foreign/ForeignPtr_LHAssumptions.hs --- a/src/Foreign/ForeignPtr_LHAssumptions.hs +++ b/src/Foreign/ForeignPtr_LHAssumptions.hs @@ -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` diff --git a/src/Foreign/Marshal/Alloc_LHAssumptions.hs b/src/Foreign/Marshal/Alloc_LHAssumptions.hs --- a/src/Foreign/Marshal/Alloc_LHAssumptions.hs +++ b/src/Foreign/Marshal/Alloc_LHAssumptions.hs @@ -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 @-} diff --git a/src/Foreign/Ptr_LHAssumptions.hs b/src/Foreign/Ptr_LHAssumptions.hs --- a/src/Foreign/Ptr_LHAssumptions.hs +++ b/src/Foreign/Ptr_LHAssumptions.hs @@ -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 } @-} diff --git a/src/Foreign/Storable_LHAssumptions.hs b/src/Foreign/Storable_LHAssumptions.hs --- a/src/Foreign/Storable_LHAssumptions.hs +++ b/src/Foreign/Storable_LHAssumptions.hs @@ -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 () @-} diff --git a/src/GHC/Base_LHAssumptions.hs b/src/GHC/Base_LHAssumptions.hs --- a/src/GHC/Base_LHAssumptions.hs +++ b/src/GHC/Base_LHAssumptions.hs @@ -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

c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>. + {xcmp::a, wcmp::b |- c

<: c} + (ycmp:b -> c

) + -> (zcmp:a -> b) + -> xcmp:a -> c + +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) + +@-} diff --git a/src/GHC/CString_LHAssumptions.hs b/src/GHC/CString_LHAssumptions.hs --- a/src/GHC/CString_LHAssumptions.hs +++ b/src/GHC/CString_LHAssumptions.hs @@ -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 @-} diff --git a/src/GHC/Classes_LHAssumptions.hs b/src/GHC/Classes_LHAssumptions.hs --- a/src/GHC/Classes_LHAssumptions.hs +++ b/src/GHC/Classes_LHAssumptions.hs @@ -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) } @-} diff --git a/src/GHC/Exts_LHAssumptions.hs b/src/GHC/Exts_LHAssumptions.hs --- a/src/GHC/Exts_LHAssumptions.hs +++ b/src/GHC/Exts_LHAssumptions.hs @@ -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} @-} diff --git a/src/GHC/Float_LHAssumptions.hs b/src/GHC/Float_LHAssumptions.hs --- a/src/GHC/Float_LHAssumptions.hs +++ b/src/GHC/Float_LHAssumptions.hs @@ -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 +@-} diff --git a/src/GHC/ForeignPtr_LHAssumptions.hs b/src/GHC/ForeignPtr_LHAssumptions.hs --- a/src/GHC/ForeignPtr_LHAssumptions.hs +++ b/src/GHC/ForeignPtr_LHAssumptions.hs @@ -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)) @-} diff --git a/src/GHC/IO/Handle_LHAssumptions.hs b/src/GHC/IO/Handle_LHAssumptions.hs --- a/src/GHC/IO/Handle_LHAssumptions.hs +++ b/src/GHC/IO/Handle_LHAssumptions.hs @@ -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}) @-} diff --git a/src/GHC/Int_LHAssumptions.hs b/src/GHC/Int_LHAssumptions.hs --- a/src/GHC/Int_LHAssumptions.hs +++ b/src/GHC/Int_LHAssumptions.hs @@ -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} @-} diff --git a/src/GHC/Internal/Base_LHAssumptions.hs b/src/GHC/Internal/Base_LHAssumptions.hs deleted file mode 100644 --- a/src/GHC/Internal/Base_LHAssumptions.hs +++ /dev/null @@ -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

c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>. - {xcmp::a, wcmp::b |- c

<: c} - (ycmp:b -> c

) - -> (zcmp:a -> b) - -> xcmp:a -> c - -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) - -@-} diff --git a/src/GHC/Internal/Data/Foldable_LHAssumptions.hs b/src/GHC/Internal/Data/Foldable_LHAssumptions.hs deleted file mode 100644 --- a/src/GHC/Internal/Data/Foldable_LHAssumptions.hs +++ /dev/null @@ -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)} -@-} diff --git a/src/GHC/Internal/Data/Maybe_LHAssumptions.hs b/src/GHC/Internal/Data/Maybe_LHAssumptions.hs deleted file mode 100644 --- a/src/GHC/Internal/Data/Maybe_LHAssumptions.hs +++ /dev/null @@ -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 -@-} diff --git a/src/GHC/Internal/Float_LHAssumptions.hs b/src/GHC/Internal/Float_LHAssumptions.hs deleted file mode 100644 --- a/src/GHC/Internal/Float_LHAssumptions.hs +++ /dev/null @@ -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 -@-} diff --git a/src/GHC/Internal/Int_LHAssumptions.hs b/src/GHC/Internal/Int_LHAssumptions.hs deleted file mode 100644 --- a/src/GHC/Internal/Int_LHAssumptions.hs +++ /dev/null @@ -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 - -@-} diff --git a/src/GHC/Internal/List_LHAssumptions.hs b/src/GHC/Internal/List_LHAssumptions.hs deleted file mode 100644 --- a/src/GHC/Internal/List_LHAssumptions.hs +++ /dev/null @@ -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 -@-} diff --git a/src/GHC/Internal/Num_LHAssumptions.hs b/src/GHC/Internal/Num_LHAssumptions.hs deleted file mode 100644 --- a/src/GHC/Internal/Num_LHAssumptions.hs +++ /dev/null @@ -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 } -@-} diff --git a/src/GHC/Internal/Word_LHAssumptions.hs b/src/GHC/Internal/Word_LHAssumptions.hs deleted file mode 100644 --- a/src/GHC/Internal/Word_LHAssumptions.hs +++ /dev/null @@ -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 } -@-} diff --git a/src/GHC/List_LHAssumptions.hs b/src/GHC/List_LHAssumptions.hs --- a/src/GHC/List_LHAssumptions.hs +++ b/src/GHC/List_LHAssumptions.hs @@ -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 +@-} diff --git a/src/GHC/Num/Integer_LHAssumptions.hs b/src/GHC/Num/Integer_LHAssumptions.hs --- a/src/GHC/Num/Integer_LHAssumptions.hs +++ b/src/GHC/Num/Integer_LHAssumptions.hs @@ -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 @-} diff --git a/src/GHC/Num_LHAssumptions.hs b/src/GHC/Num_LHAssumptions.hs --- a/src/GHC/Num_LHAssumptions.hs +++ b/src/GHC/Num_LHAssumptions.hs @@ -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 } +@-} diff --git a/src/GHC/Ptr_LHAssumptions.hs b/src/GHC/Ptr_LHAssumptions.hs --- a/src/GHC/Ptr_LHAssumptions.hs +++ b/src/GHC/Ptr_LHAssumptions.hs @@ -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 @-} diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs --- a/src/GHC/Real_LHAssumptions.hs +++ b/src/GHC/Real_LHAssumptions.hs @@ -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) + @-} diff --git a/src/GHC/Types_LHAssumptions.hs b/src/GHC/Types_LHAssumptions.hs --- a/src/GHC/Types_LHAssumptions.hs +++ b/src/GHC/Types_LHAssumptions.hs @@ -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 + @-} diff --git a/src/GHC/Word_LHAssumptions.hs b/src/GHC/Word_LHAssumptions.hs --- a/src/GHC/Word_LHAssumptions.hs +++ b/src/GHC/Word_LHAssumptions.hs @@ -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 } +@-} diff --git a/src/Liquid/Prelude/Real_LHAssumptions.hs b/src/Liquid/Prelude/Real_LHAssumptions.hs --- a/src/Liquid/Prelude/Real_LHAssumptions.hs +++ b/src/Liquid/Prelude/Real_LHAssumptions.hs @@ -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} @-} diff --git a/src/Liquid/Prelude/Totality_LHAssumptions.hs b/src/Liquid/Prelude/Totality_LHAssumptions.hs --- a/src/Liquid/Prelude/Totality_LHAssumptions.hs +++ b/src/Liquid/Prelude/Totality_LHAssumptions.hs @@ -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 @-} diff --git a/src/Prelude_LHAssumptions.hs b/src/Prelude_LHAssumptions.hs --- a/src/Prelude_LHAssumptions.hs +++ b/src/Prelude_LHAssumptions.hs @@ -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)