liquidhaskell 0.9.8.2 → 0.9.10.1
raw patch · 38 files changed
+334/−329 lines, 38 filesdep +ghc-internaldep ~bytestringdep ~containersdep ~liquidhaskell-boot
Dependencies added: ghc-internal
Dependency ranges changed: bytestring, containers, liquidhaskell-boot
Files
- CHANGES.md +4/−0
- README.md +4/−36
- liquidhaskell.cabal +13/−5
- src/Data/ByteString/Lazy_LHAssumptions.hs +13/−13
- src/Data/Either_LHAssumptions.hs +1/−1
- src/Data/Foldable_LHAssumptions.hs +1/−6
- src/Data/Int_LHAssumptions.hs +0/−10
- src/Data/Maybe_LHAssumptions.hs +1/−17
- src/Data/String_LHAssumptions.hs +2/−2
- src/Data/Tuple_LHAssumptions.hs +2/−2
- src/Data/Word_LHAssumptions.hs +1/−10
- src/Foreign/C/String_LHAssumptions.hs +5/−5
- src/Foreign/Concurrent_LHAssumptions.hs +1/−1
- src/Foreign/ForeignPtr_LHAssumptions.hs +2/−2
- src/Foreign/Marshal/Alloc_LHAssumptions.hs +1/−1
- src/Foreign/Storable_LHAssumptions.hs +8/−8
- src/GHC/Base_LHAssumptions.hs +1/−52
- src/GHC/Float_LHAssumptions.hs +3/−26
- src/GHC/ForeignPtr_LHAssumptions.hs +5/−5
- src/GHC/IO/Handle_LHAssumptions.hs +3/−3
- src/GHC/Int_LHAssumptions.hs +5/−5
- src/GHC/Internal/Base_LHAssumptions.hs +55/−0
- src/GHC/Internal/Data/Foldable_LHAssumptions.hs +9/−0
- src/GHC/Internal/Data/Maybe_LHAssumptions.hs +21/−0
- src/GHC/Internal/Float_LHAssumptions.hs +28/−0
- src/GHC/Internal/Int_LHAssumptions.hs +10/−0
- src/GHC/Internal/List_LHAssumptions.hs +70/−0
- src/GHC/Internal/Num_LHAssumptions.hs +17/−0
- src/GHC/Internal/Word_LHAssumptions.hs +13/−0
- src/GHC/List_LHAssumptions.hs +1/−66
- src/GHC/Num/Integer_LHAssumptions.hs +2/−1
- src/GHC/Num_LHAssumptions.hs +1/−14
- src/GHC/Ptr_LHAssumptions.hs +8/−8
- src/GHC/Real_LHAssumptions.hs +14/−14
- src/GHC/Word_LHAssumptions.hs +1/−7
- src/Liquid/Prelude/Real_LHAssumptions.hs +1/−1
- src/Liquid/Prelude/Totality_LHAssumptions.hs +5/−5
- src/Prelude_LHAssumptions.hs +2/−3
CHANGES.md view
@@ -2,6 +2,10 @@ ## Next +## 0.9.10.1 (2024-08-21)++- Add support for GHC 9.10.1.+ ## 0.9.8.2 (2024-08-21) - Support for GHC 9.8.2.
README.md view
@@ -47,36 +47,16 @@ ## Running the pluging on individual files ```-stack build liquidhaskell-stack exec ghc -- -fplugin=LiquidHaskell FILE.hs-```--``` cabal build liquidhaskell cabal exec ghc -- -fplugin=LiquidHaskell FILE.hs ``` ## Building -### Stack--```-stack build-```--If on NixOS--```-stack --no-nix-pure build-```--With the above, `stack` will unregister and re-register the libraries,-but hopefully it won't rebuild any modules.- ### Cabal ```-cabal v2-build+cabal build ``` ### Faster recompilation@@ -84,7 +64,7 @@ When changing the `liquidhaskell-boot` library, sometimes we don't want to rebuild `liquidhaskell` or `liquid-vector` when testing the changes. In these cases we can set the environment variable `LIQUID_DEV_MODE=true`-when running `stack` or `cabal` to skip rebuilding those packages.+when running `cabal` to skip rebuilding those packages. DANGER: Note that this can give an invalid result if the changes to `liquidhaskell-boot` do require rebuilding other `liquid*` packages.@@ -92,8 +72,7 @@ ## How To Run Regression Tests For documentation on the `test-driver` executable itself, please refer to the-`README.md` in `tests/` or run `cabal run tests:test-driver -- --help` or `stack-run test-driver -- --help`+`README.md` in `tests/` or run `cabal run tests:test-driver -- --help` You can run *all* the tests by @@ -191,17 +170,6 @@ [ghc-users-guide]: https://downloads.haskell.org/ghc/latest/docs/users_guide/ [git-documentation]: https://git-scm.com/doc -## Releasing on Hackage--*NOTE: The following section is relevant only for few developers, i.e. the ones which are directly involved-in the release process. Most contributors can skip this section.*--We provide a convenience script to upload all the `liquid-*` packages (**including** `liquid-fixpoint`) on-Hackage, in a lockstep fashion. To do so, it's possible to simply run the `scripts/release_to_hackage.sh`-Bash script. The script doesn't accept any argument and it tries to determine the packages-to upload by scanning the `$PWD` for packages named appropriately. It will ask the user for confirmation-before proceeding, and `stack upload` will be used under the hood.- ## GHC support policy LH supports only one version of GHC at any given time. This is because LH depends heavily on the `ghc` library@@ -315,7 +283,7 @@ ## A new version of GHC is out. How do I support it? -Typically the first thing you might want to do is to run a "clean" `cabal v2-build` or `stack build` using+Typically the first thing you might want to do is to run a "clean" `cabal build` using the latest compiler and "check the damage". If you are lucky, everything works out of the box, otherwise compilation might fail with an error, typically because some `ghc` API function has been removed/moved/renamed. The way to fix it is to modify the [GHC.API][] shim module and perform any required change, likely by
liquidhaskell.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-version: 0.9.8.2+version: 0.9.10.1 synopsis: Liquid Types for Haskell description: Liquid Types for Haskell. license: BSD-3-Clause@@ -11,7 +11,7 @@ category: Language homepage: https://github.com/ucsd-progsys/liquidhaskell build-type: Custom-tested-with: GHC == 9.8.2+tested-with: GHC == 9.10.1 extra-doc-files: CHANGES.md README.md @@ -37,7 +37,6 @@ Data.Bits_LHAssumptions Data.Either_LHAssumptions Data.Foldable_LHAssumptions- Data.Int_LHAssumptions Data.Maybe_LHAssumptions Data.String_LHAssumptions Data.Tuple_LHAssumptions@@ -55,6 +54,14 @@ 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@@ -78,10 +85,11 @@ hs-source-dirs: src build-depends: base >= 4.11.1.0 && < 5,- liquidhaskell-boot == 0.9.8.2,+ liquidhaskell-boot == 0.9.10.1, bytestring == 0.12.1.0,- containers == 0.6.8,+ containers == 0.7, ghc-bignum,+ ghc-internal, ghc-prim default-language: Haskell98 ghc-options: -Wall
src/Data/ByteString/Lazy_LHAssumptions.hs view
@@ -9,7 +9,7 @@ import GHC.Int_LHAssumptions() {-@-measure bllen :: Data.ByteString.Lazy.ByteString -> { n : GHC.Int.Int64 | 0 <= n }+measure bllen :: Data.ByteString.Lazy.ByteString -> { n : GHC.Internal.Int.Int64 | 0 <= n } invariant { bs : Data.ByteString.Lazy.ByteString | 0 <= bllen bs } @@ -80,7 +80,7 @@ assume Data.ByteString.Lazy.null :: bs : Data.ByteString.Lazy.ByteString -> { b : GHC.Types.Bool | b <=> bllen bs == 0 } assume Data.ByteString.Lazy.length- :: bs : Data.ByteString.Lazy.ByteString -> { n : GHC.Int.Int64 | bllen bs == n }+ :: bs : Data.ByteString.Lazy.ByteString -> { n : GHC.Internal.Int.Int64 | bllen bs == n } assume Data.ByteString.Lazy.map :: (_ -> _)@@ -160,26 +160,26 @@ -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.replicate- :: n : GHC.Int.Int64+ :: n : GHC.Internal.Int.Int64 -> _ -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n } assume Data.ByteString.Lazy.take- :: n : GHC.Int.Int64+ :: n : GHC.Internal.Int.Int64 -> i : Data.ByteString.Lazy.ByteString -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 ==> bllen o == 0) && ((0 <= n && n <= bllen i) <=> bllen o == n) && (bllen i <= n <=> bllen o = bllen i) } assume Data.ByteString.Lazy.drop- :: n : GHC.Int.Int64+ :: n : GHC.Internal.Int.Int64 -> i : Data.ByteString.Lazy.ByteString -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen o == bllen i) && ((0 <= n && n <= bllen i) <=> bllen o == bllen i - n) && (bllen i <= n <=> bllen o == 0) } assume Data.ByteString.Lazy.splitAt- :: n : GHC.Int.Int64+ :: n : GHC.Internal.Int.Int64 -> i : Data.ByteString.Lazy.ByteString -> ( { l : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen l == 0) && ((0 <= n && n <= bllen i) <=> bllen l == n) &&@@ -279,38 +279,38 @@ assume Data.ByteString.Lazy.index :: bs : Data.ByteString.Lazy.ByteString- -> { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }+ -> { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } -> _ assume Data.ByteString.Lazy.elemIndex :: _ -> bs : Data.ByteString.Lazy.ByteString- -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }+ -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.elemIndices :: _ -> bs : Data.ByteString.Lazy.ByteString- -> [{ n : GHC.Int.Int64 | 0 <= n && n < bllen bs }]+ -> [{ n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.elemIndexEnd :: _ -> bs : Data.ByteString.Lazy.ByteString- -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }+ -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.findIndex :: (_ -> GHC.Types.Bool) -> bs : Data.ByteString.Lazy.ByteString- -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }+ -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.findIndices :: (_ -> GHC.Types.Bool) -> bs : Data.ByteString.Lazy.ByteString- -> [{ n : GHC.Int.Int64 | 0 <= n && n < bllen bs }]+ -> [{ n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.count :: _ -> bs : Data.ByteString.Lazy.ByteString- -> { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }+ -> { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.zip :: l : Data.ByteString.Lazy.ByteString
src/Data/Either_LHAssumptions.hs view
@@ -4,7 +4,7 @@ import GHC.Types_LHAssumptions() {-@-measure isLeft :: Data.Either.Either a b -> Bool+measure isLeft :: GHC.Internal.Data.Either.Either a b -> Bool isLeft (Left x) = true isLeft (Right x) = false @-}
src/Data/Foldable_LHAssumptions.hs view
@@ -1,9 +1,4 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} module Data.Foldable_LHAssumptions where -import GHC.Types_LHAssumptions()--{-@-assume Data.Foldable.length :: Data.Foldable.Foldable f => forall a. xs:f a -> {v:Nat | v = len xs}-assume Data.Foldable.null :: Data.Foldable.Foldable f => forall a. v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)}-@-}+import GHC.Internal.Data.Foldable_LHAssumptions()
− src/Data/Int_LHAssumptions.hs
@@ -1,10 +0,0 @@-{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-module Data.Int_LHAssumptions where--{-@-embed Data.Int.Int8 as int-embed Data.Int.Int16 as int-embed Data.Int.Int32 as int-embed Data.Int.Int64 as int--@-}
src/Data/Maybe_LHAssumptions.hs view
@@ -2,20 +2,4 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module Data.Maybe_LHAssumptions where -import GHC.Types_LHAssumptions()-import Data.Maybe--{-@-assume Data.Maybe.maybe :: v:b -> (a -> b) -> u:(GHC.Maybe.Maybe a) -> {w:b | not (isJust u) => w == v}-assume Data.Maybe.isNothing :: v:(GHC.Maybe.Maybe a) -> {b:Bool | not (isJust v) == b}-assume Data.Maybe.fromMaybe :: v:a -> u:(GHC.Maybe.Maybe a) -> {x:a | not (isJust u) => x == v}--assume Data.Maybe.isJust :: v:(GHC.Maybe.Maybe a) -> {b:Bool | b == isJust v}-measure isJust :: GHC.Maybe.Maybe a -> Bool- isJust (GHC.Maybe.Just x) = true- isJust (GHC.Maybe.Nothing) = false--assume Data.Maybe.fromJust :: {v:(GHC.Maybe.Maybe a) | isJust v} -> a-measure fromJust :: GHC.Maybe.Maybe a -> a- fromJust (GHC.Maybe.Just x) = x-@-}+import GHC.Internal.Data.Maybe_LHAssumptions
src/Data/String_LHAssumptions.hs view
@@ -8,8 +8,8 @@ {-@ measure stringlen :: a -> GHC.Types.Int -assume Data.String.fromString- :: forall a. Data.String.IsString a+assume GHC.Internal.Data.String.fromString+ :: forall a. GHC.Internal.Data.String.IsString a => i : [GHC.Types.Char] -> { o : a | i ~~ o && len i == stringlen o } @-}
src/Data/Tuple_LHAssumptions.hs view
@@ -5,8 +5,8 @@ import Data.Tuple {-@-assume Data.Tuple.fst :: {f:(x:(a,b) -> {v:a | v = (fst x)}) | f == fst }-assume Data.Tuple.snd :: {f:(x:(a,b) -> {v:b | v = (snd x)}) | f == snd }+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 } measure fst :: (a, b) -> a fst (a, b) = a
src/Data/Word_LHAssumptions.hs view
@@ -1,13 +1,4 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} module Data.Word_LHAssumptions where -{-@-embed GHC.Word.Word as int-embed GHC.Word.Word8 as int-embed GHC.Word.Word16 as int-embed GHC.Word.Word32 as int-embed GHC.Word.Word64 as int--invariant {v : GHC.Word.Word32 | 0 <= v }-invariant {v : GHC.Word.Word16 | 0 <= v }-@-}+import GHC.Internal.Word_LHAssumptions()
src/Foreign/C/String_LHAssumptions.hs view
@@ -8,12 +8,12 @@ import GHC.Types_LHAssumptions() {-@-type CStringLen = ((GHC.Ptr.Ptr Foreign.C.Types.CChar), Nat)<{\p v -> (v <= (plen p))}>-type CStringLenN N = ((GHC.Ptr.Ptr Foreign.C.Types.CChar), {v:Nat | v = N})<{\p v -> (v <= (plen p))}>+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))}> -// measure cStringLen :: Foreign.C.String.CStringLen -> GHC.Types.Int-measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int+// 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 :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int +// measure cStringLen :: ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int // cStringLen (c, n) = n @-}
src/Foreign/Concurrent_LHAssumptions.hs view
@@ -6,5 +6,5 @@ import GHC.ForeignPtr_LHAssumptions() {-@-assume Foreign.Concurrent.newForeignPtr :: p:(PtrV a) -> GHC.Types.IO () -> (GHC.Types.IO (ForeignPtrN a (plen p)))+assume GHC.Internal.Foreign.Concurrent.newForeignPtr :: p:(PtrV a) -> GHC.Types.IO () -> (GHC.Types.IO (ForeignPtrN a (plen p))) @-}
src/Foreign/ForeignPtr_LHAssumptions.hs view
@@ -8,11 +8,11 @@ {-@ -assume GHC.ForeignPtr.withForeignPtr :: forall a b. fp:(GHC.ForeignPtr.ForeignPtr a)+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 Foreign.ForeignPtr.Imp.newForeignPtr :: _ -> p:(PtrV a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))+assume GHC.Internal.Foreign.ForeignPtr.Imp.newForeignPtr :: _ -> p:(PtrV a) -> (GHC.Types.IO (ForeignPtrN a (plen p))) // this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`
src/Foreign/Marshal/Alloc_LHAssumptions.hs view
@@ -7,5 +7,5 @@ import Foreign.Marshal.Alloc {-@-assume Foreign.Marshal.Alloc.allocaBytes :: n:Nat -> (PtrN a n -> IO b) -> IO b+assume GHC.Internal.Foreign.Marshal.Alloc.allocaBytes :: n:Nat -> (PtrN a n -> IO b) -> IO b @-}
src/Foreign/Storable_LHAssumptions.hs view
@@ -8,22 +8,22 @@ {-@ predicate PValid P N = ((0 <= N) && (N < (plen P))) -assume Foreign.Storable.poke :: (Foreign.Storable.Storable a)- => {v: (GHC.Ptr.Ptr a) | 0 < (plen v)}+assume GHC.Internal.Foreign.Storable.poke :: (GHC.Internal.Foreign.Storable.Storable a)+ => {v: (GHC.Internal.Ptr.Ptr a) | 0 < (plen v)} -> a -> (GHC.Types.IO ()) -assume Foreign.Storable.peek :: (Foreign.Storable.Storable a)- => p:{v: (GHC.Ptr.Ptr a) | 0 < (plen v)}+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 Foreign.Storable.peekByteOff :: (Foreign.Storable.Storable a)- => forall b. p:(GHC.Ptr.Ptr b)+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 Foreign.Storable.pokeByteOff :: (Foreign.Storable.Storable a)- => forall b. p:(GHC.Ptr.Ptr b)+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)} -> a -> GHC.Types.IO ()
src/GHC/Base_LHAssumptions.hs view
@@ -1,55 +1,4 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Base_LHAssumptions where -import GHC.CString_LHAssumptions()-import GHC.Exts_LHAssumptions()-import GHC.Types_LHAssumptions()-import GHC.Base-import Data.Tuple_LHAssumptions()--{-@--assume GHC.Base.. :: forall <p :: b -> c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>.- {xcmp::a, wcmp::b<q xcmp> |- c<p wcmp> <: c<r xcmp>}- (ycmp:b -> c<p ycmp>)- -> (zcmp:a -> b<q zcmp>)- -> xcmp:a -> c<r xcmp>--measure autolen :: forall a. a -> GHC.Types.Int--// Useless as compiled into GHC primitive, which is ignored-assume GHC.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.Base.map :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}-assume GHC.Base.++ :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}--assume (GHC.Base.$) :: (a -> b) -> a -> b-assume GHC.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)--@-}+import GHC.Internal.Base_LHAssumptions()
src/GHC/Float_LHAssumptions.hs view
@@ -1,28 +1,5 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}-module GHC.Float_LHAssumptions(Floating(..)) where+{-# OPTIONS_GHC -Wno-unused-imports #-}+module GHC.Float_LHAssumptions where -{-@-class (GHC.Real.Fractional a) => GHC.Float.Floating a where- GHC.Float.pi :: a- GHC.Float.exp :: a -> {y:a | y > 0}- GHC.Float.log :: {x:a | x > 0} -> a- GHC.Float.sqrt :: {x:a | x >= 0} -> {y:a | y >= 0}- (GHC.Float.**) :: x:a -> {y:a | x = 0 => y >= 0} -> a- GHC.Float.logBase :: {b:a | b > 0 && b /= 1} -> {x:a | x > 0} -> a- GHC.Float.sin :: a -> {y:a | -1 <= y && y <= 1}- GHC.Float.cos :: a -> {y:a | -1 <= y && y <= 1}- GHC.Float.tan :: a -> a- GHC.Float.asin :: {x:a | -1 <= x && x <= 1} -> a- GHC.Float.acos :: {x:a | -1 <= x && x <= 1} -> a- GHC.Float.atan :: a -> a- GHC.Float.sinh :: a -> a- GHC.Float.cosh :: a -> {y:a | y >= 1}- GHC.Float.tanh :: a -> {y:a | -1 < y && y < 1}- GHC.Float.asinh :: a -> a- GHC.Float.acosh :: {y:a | y >= 1} -> a- GHC.Float.atanh :: {y:a | -1 < y && y < 1} -> a- GHC.Float.log1p :: a -> a- GHC.Float.expm1 :: a -> a- GHC.Float.log1pexp :: a -> a- GHC.Float.log1mexp :: a -> a-@-}+import GHC.Internal.Float_LHAssumptions
src/GHC/ForeignPtr_LHAssumptions.hs view
@@ -6,11 +6,11 @@ import GHC.Ptr_LHAssumptions() {-@-measure fplen :: GHC.ForeignPtr.ForeignPtr a -> GHC.Types.Int+measure fplen :: GHC.Internal.ForeignPtr.ForeignPtr a -> GHC.Types.Int -type ForeignPtrV a = {v: GHC.ForeignPtr.ForeignPtr a | 0 <= fplen v}-type ForeignPtrN a N = {v: GHC.ForeignPtr.ForeignPtr a | 0 <= fplen v && fplen v == N }+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 } -assume GHC.ForeignPtr.newForeignPtr_ :: p:(GHC.Ptr.Ptr a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))-assume GHC.ForeignPtr.mallocPlainForeignPtrBytes :: n:{v:GHC.Types.Int | v >= 0 } -> (GHC.Types.IO (ForeignPtrN a 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)) @-}
src/GHC/IO/Handle_LHAssumptions.hs view
@@ -6,12 +6,12 @@ import GHC.Types_LHAssumptions() {-@-assume GHC.IO.Handle.Text.hGetBuf :: GHC.IO.Handle.Handle -> GHC.Ptr.Ptr a -> n:Nat+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 GHC.IO.Handle.Text.hGetBufNonBlocking :: GHC.IO.Handle.Handle -> GHC.Ptr.Ptr a -> n:Nat+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 GHC.IO.Handle.hFileSize :: GHC.IO.Handle.Handle+assume GHC.Internal.IO.Handle.hFileSize :: GHC.Internal.IO.Handle.Handle -> (GHC.Types.IO {v:Integer | v >= 0}) @-}
src/GHC/Int_LHAssumptions.hs view
@@ -5,10 +5,10 @@ import GHC.Int {-@-embed GHC.Int.Int8 as int-embed GHC.Int.Int16 as int-embed GHC.Int.Int32 as int-embed GHC.Int.Int64 as 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 -type Nat64 = {v:GHC.Int.Int64 | v >= 0}+type Nat64 = {v:GHC.Internal.Int.Int64 | v >= 0} @-}
+ src/GHC/Internal/Base_LHAssumptions.hs view
@@ -0,0 +1,55 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-}+module GHC.Internal.Base_LHAssumptions where++import GHC.CString_LHAssumptions()+import GHC.Exts_LHAssumptions()+import GHC.Types_LHAssumptions()+import GHC.Internal.Base+import Data.Tuple_LHAssumptions()++{-@++assume GHC.Internal.Base.. :: forall <p :: b -> c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>.+ {xcmp::a, wcmp::b<q xcmp> |- c<p wcmp> <: c<r xcmp>}+ (ycmp:b -> c<p ycmp>)+ -> (zcmp:a -> b<q zcmp>)+ -> xcmp:a -> c<r xcmp>++measure autolen :: forall a. a -> GHC.Types.Int++// Useless as compiled into GHC primitive, which is ignored+assume GHC.Internal.Base.assert :: {v:Bool | v } -> a -> a++instance measure len :: forall a. [a] -> GHC.Types.Int+ len [] = 0+ len (y:ys) = 1 + len ys++invariant {v: [a] | len v >= 0 }+assume GHC.Internal.Base.map :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}+assume GHC.Internal.Base.++ :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}++assume (GHC.Internal.Base.$) :: (a -> b) -> a -> b+assume GHC.Internal.Base.id :: x:a -> {v:a | v = x}++qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs > 0))+qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs = 0))++qualif ListZ(v: [a]) : (len v = 0)+qualif ListZ(v: [a]) : (len v >= 0)+qualif ListZ(v: [a]) : (len v > 0)++qualif CmpLen(v:[a], xs:[b]) : (len v = len xs )+qualif CmpLen(v:[a], xs:[b]) : (len v >= len xs )+qualif CmpLen(v:[a], xs:[b]) : (len v > len xs )+qualif CmpLen(v:[a], xs:[b]) : (len v <= len xs )+qualif CmpLen(v:[a], xs:[b]) : (len v < len xs )++qualif EqLen(v:int, xs: [a]) : (v = len xs )+qualif LenEq(v:[a], x: int) : (x = len v )++qualif LenDiff(v:[a], x:int) : (len v = x + 1)+qualif LenDiff(v:[a], x:int) : (len v = x - 1)+qualif LenAcc(v:int, xs:[a], n: int): (v = len xs + n)++@-}
+ src/GHC/Internal/Data/Foldable_LHAssumptions.hs view
@@ -0,0 +1,9 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+module GHC.Internal.Data.Foldable_LHAssumptions where++import GHC.Types_LHAssumptions()++{-@+assume GHC.Internal.Data.Foldable.length :: GHC.Internal.Data.Foldable.Foldable f => forall a. xs:f a -> {v:Nat | v = len xs}+assume GHC.Internal.Data.Foldable.null :: GHC.Internal.Data.Foldable.Foldable f => forall a. v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)}+@-}
+ src/GHC/Internal/Data/Maybe_LHAssumptions.hs view
@@ -0,0 +1,21 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-}+module GHC.Internal.Data.Maybe_LHAssumptions where++import GHC.Types_LHAssumptions()+import Data.Maybe++{-@+assume GHC.Internal.Data.Maybe.maybe :: v:b -> (a -> b) -> u:(GHC.Internal.Maybe.Maybe a) -> {w:b | not (isJust u) => w == v}+assume GHC.Internal.Data.Maybe.isNothing :: v:(GHC.Internal.Maybe.Maybe a) -> {b:Bool | not (isJust v) == b}+assume GHC.Internal.Data.Maybe.fromMaybe :: v:a -> u:(GHC.Internal.Maybe.Maybe a) -> {x:a | not (isJust u) => x == v}++assume GHC.Internal.Data.Maybe.isJust :: v:(GHC.Internal.Maybe.Maybe a) -> {b:Bool | b == isJust v}+measure isJust :: GHC.Internal.Maybe.Maybe a -> Bool+ isJust (GHC.Internal.Maybe.Just x) = true+ isJust (GHC.Internal.Maybe.Nothing) = false++assume GHC.Internal.Data.Maybe.fromJust :: {v:(GHC.Internal.Maybe.Maybe a) | isJust v} -> a+measure fromJust :: GHC.Internal.Maybe.Maybe a -> a+ fromJust (GHC.Internal.Maybe.Just x) = x+@-}
+ src/GHC/Internal/Float_LHAssumptions.hs view
@@ -0,0 +1,28 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+module GHC.Internal.Float_LHAssumptions(Floating(..)) where++{-@+class (GHC.Internal.Real.Fractional a) => GHC.Internal.Float.Floating a where+ GHC.Internal.Float.pi :: a+ GHC.Internal.Float.exp :: a -> {y:a | y > 0}+ GHC.Internal.Float.log :: {x:a | x > 0} -> a+ GHC.Internal.Float.sqrt :: {x:a | x >= 0} -> {y:a | y >= 0}+ (GHC.Internal.Float.**) :: x:a -> {y:a | x = 0 => y >= 0} -> a+ GHC.Internal.Float.logBase :: {b:a | b > 0 && b /= 1} -> {x:a | x > 0} -> a+ GHC.Internal.Float.sin :: a -> {y:a | -1 <= y && y <= 1}+ GHC.Internal.Float.cos :: a -> {y:a | -1 <= y && y <= 1}+ GHC.Internal.Float.tan :: a -> a+ GHC.Internal.Float.asin :: {x:a | -1 <= x && x <= 1} -> a+ GHC.Internal.Float.acos :: {x:a | -1 <= x && x <= 1} -> a+ GHC.Internal.Float.atan :: a -> a+ GHC.Internal.Float.sinh :: a -> a+ GHC.Internal.Float.cosh :: a -> {y:a | y >= 1}+ GHC.Internal.Float.tanh :: a -> {y:a | -1 < y && y < 1}+ GHC.Internal.Float.asinh :: a -> a+ GHC.Internal.Float.acosh :: {y:a | y >= 1} -> a+ GHC.Internal.Float.atanh :: {y:a | -1 < y && y < 1} -> a+ GHC.Internal.Float.log1p :: a -> a+ GHC.Internal.Float.expm1 :: a -> a+ GHC.Internal.Float.log1pexp :: a -> a+ GHC.Internal.Float.log1mexp :: a -> a+@-}
+ src/GHC/Internal/Int_LHAssumptions.hs view
@@ -0,0 +1,10 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+module GHC.Internal.Int_LHAssumptions where++{-@+embed GHC.Internal.Int.Int8 as int+embed GHC.Internal.Int.Int16 as int+embed GHC.Internal.Int.Int32 as int+embed GHC.Internal.Int.Int64 as int++@-}
+ src/GHC/Internal/List_LHAssumptions.hs view
@@ -0,0 +1,70 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+{-# OPTIONS_GHC -Wno-unused-imports #-}+module GHC.Internal.List_LHAssumptions where++import GHC.List+import GHC.Types_LHAssumptions()++{-@++assume GHC.Internal.List.head :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs}+assume GHC.Internal.List.tail :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs}++assume GHC.Internal.List.last :: xs:{v: [a] | len v > 0} -> a+assume GHC.Internal.List.init :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1}+assume GHC.Internal.List.null :: xs:[a] -> {v: GHC.Types.Bool | ((v) <=> len(xs) = 0) }+assume GHC.Internal.List.length :: xs:[a] -> {v: GHC.Types.Int | v = len(xs)}+assume GHC.Internal.List.filter :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}+assume GHC.Internal.List.scanl :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) }+assume GHC.Internal.List.scanl1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }+assume GHC.Internal.List.foldr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a+assume GHC.Internal.List.scanr :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) }+assume GHC.Internal.List.scanr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }++lazy GHC.Internal.List.iterate+assume GHC.Internal.List.iterate :: (a -> a) -> a -> [a]++assume GHC.Internal.List.repeat :: a -> [a]+lazy GHC.Internal.List.repeat++assume GHC.Internal.List.replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n}++assume GHC.Internal.List.cycle :: {v: [a] | len(v) > 0 } -> [a]+lazy GHC.Internal.List.cycle++assume GHC.Internal.List.takeWhile :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}+assume GHC.Internal.List.dropWhile :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}++assume GHC.Internal.List.take :: n:GHC.Types.Int+ -> xs:[a]+ -> {v:[a] | if n >= 0 then (len v = (if (len xs) < n then (len xs) else n)) else (len v = 0)}+assume GHC.Internal.List.drop :: n:GHC.Types.Int+ -> xs:[a]+ -> {v:[a] | (if (n >= 0) then (len(v) = (if (len(xs) < n) then 0 else len(xs) - n)) else ((len v) = (len xs)))}++assume GHC.Internal.List.splitAt :: n:_ -> x:[a] -> ({v:[a] | (if (n >= 0) then (if (len x) < n then (len v) = (len x) else (len v) = n) else ((len v) = 0))},[a])<{\x1 x2 -> (len x2) = (len x) - (len x1)}>+assume GHC.Internal.List.span :: (a -> GHC.Types.Bool)+ -> xs:[a]+ -> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))})++assume GHC.Internal.List.break :: (a -> GHC.Types.Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}>++assume GHC.Internal.List.reverse :: xs:[a] -> {v: [a] | len(v) = len(xs)}++// Copy-pasted from len.hquals+qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys]))+qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))++assume GHC.Internal.List.!! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a+++assume GHC.Internal.List.zip :: xs : [a] -> ys:[b]+ -> {v : [(a, b)] | ((((len v) <= (len xs)) && ((len v) <= (len ys)))+ && (((len xs) = (len ys)) => ((len v) = (len xs))) )}++assume GHC.Internal.List.zipWith :: (a -> b -> c)+ -> xs : [a] -> ys:[b]+ -> {v : [c] | (((len v) <= (len xs)) && ((len v) <= (len ys)))}++assume GHC.Internal.List.errorEmptyList :: {v: _ | false} -> a+@-}
+ src/GHC/Internal/Num_LHAssumptions.hs view
@@ -0,0 +1,17 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+module GHC.Internal.Num_LHAssumptions where++import GHC.Num.Integer_LHAssumptions()++{-@+assume GHC.Internal.Num.fromInteger :: x:GHC.Num.Integer.Integer -> {v:a | v = x }++assume GHC.Internal.Num.negate :: (GHC.Internal.Num.Num a)+ => x:a+ -> {v:a | v = -x}++assume GHC.Internal.Num.abs :: (GHC.Internal.Num.Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) }++assume GHC.Internal.Num.+ :: x:a -> y:a -> {v:a | v = x + y }+assume GHC.Internal.Num.- :: (GHC.Internal.Num.Num a) => x:a -> y:a -> {v:a | v = x - y }+@-}
+ src/GHC/Internal/Word_LHAssumptions.hs view
@@ -0,0 +1,13 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+module GHC.Internal.Word_LHAssumptions where++{-@+embed GHC.Internal.Word.Word as int+embed GHC.Internal.Word.Word8 as int+embed GHC.Internal.Word.Word16 as int+embed GHC.Internal.Word.Word32 as int+embed GHC.Internal.Word.Word64 as int++invariant {v : GHC.Internal.Word.Word32 | 0 <= v }+invariant {v : GHC.Internal.Word.Word16 | 0 <= v }+@-}
src/GHC/List_LHAssumptions.hs view
@@ -2,69 +2,4 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.List_LHAssumptions where -import GHC.List-import GHC.Types_LHAssumptions()--{-@--assume GHC.List.head :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs}-assume GHC.List.tail :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs}--assume GHC.List.last :: xs:{v: [a] | len v > 0} -> a-assume GHC.List.init :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1}-assume GHC.List.null :: xs:[a] -> {v: GHC.Types.Bool | ((v) <=> len(xs) = 0) }-assume GHC.List.length :: xs:[a] -> {v: GHC.Types.Int | v = len(xs)}-assume GHC.List.filter :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}-assume GHC.List.scanl :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) }-assume GHC.List.scanl1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }-assume GHC.List.foldr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a-assume GHC.List.scanr :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) }-assume GHC.List.scanr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }--lazy GHC.List.iterate-assume GHC.List.iterate :: (a -> a) -> a -> [a]--assume GHC.List.repeat :: a -> [a]-lazy GHC.List.repeat--assume GHC.List.replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n}--assume GHC.List.cycle :: {v: [a] | len(v) > 0 } -> [a]-lazy GHC.List.cycle--assume GHC.List.takeWhile :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}-assume GHC.List.dropWhile :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}--assume GHC.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.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.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.List.span :: (a -> GHC.Types.Bool)- -> xs:[a]- -> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))})--assume GHC.List.break :: (a -> GHC.Types.Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}>--assume GHC.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.List.!! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a---assume GHC.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.List.zipWith :: (a -> b -> c)- -> xs : [a] -> ys:[b]- -> {v : [c] | (((len v) <= (len xs)) && ((len v) <= (len ys)))}--assume GHC.List.errorEmptyList :: {v: _ | false} -> a-@-}+import GHC.Internal.List_LHAssumptions()
src/GHC/Num/Integer_LHAssumptions.hs view
@@ -7,7 +7,8 @@ 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) }++embed GHC.Num.Integer.Integer as int @-}
src/GHC/Num_LHAssumptions.hs view
@@ -1,17 +1,4 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} module GHC.Num_LHAssumptions where -{-@-embed GHC.Num.Integer.Integer as int--assume GHC.Num.fromInteger :: (GHC.Num.Num a) => x:GHC.Num.Integer.Integer -> {v:a | v = x }--assume GHC.Num.negate :: (GHC.Num.Num a)- => x:a- -> {v:a | v = -x}--assume GHC.Num.abs :: (GHC.Num.Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) }--assume GHC.Num.+ :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x + y }-assume GHC.Num.- :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x - y }-@-}+import GHC.Internal.Num_LHAssumptions()
src/GHC/Ptr_LHAssumptions.hs view
@@ -6,22 +6,22 @@ import GHC.Types_LHAssumptions() {-@-measure pbase :: GHC.Ptr.Ptr a -> GHC.Types.Int-measure plen :: GHC.Ptr.Ptr a -> GHC.Types.Int-measure isNullPtr :: GHC.Ptr.Ptr a -> Bool +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 type PtrN a N = {v: PtrV a | plen v == N }-type PtrV a = {v: GHC.Ptr.Ptr a | 0 <= plen v }+type PtrV a = {v: GHC.Internal.Ptr.Ptr a | 0 <= plen v } -assume GHC.Ptr.castPtr :: p:(PtrV a) -> (PtrN b (plen p))+assume GHC.Internal.Ptr.castPtr :: p:(PtrV a) -> (PtrN b (plen p)) -assume GHC.Ptr.plusPtr :: base:(PtrV a)+assume GHC.Internal.Ptr.plusPtr :: base:(PtrV a) -> off:{v:GHC.Types.Int | v <= plen base } -> {v:(PtrV b) | pbase v = pbase base && plen v = plen base - off} -assume GHC.Ptr.minusPtr :: q:(PtrV a)+assume GHC.Internal.Ptr.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.Ptr.Ptr a -> a+measure deref :: GHC.Internal.Ptr.Ptr a -> a @-}
src/GHC/Real_LHAssumptions.hs view
@@ -5,38 +5,38 @@ import GHC.Types_LHAssumptions() {-@-assume (GHC.Real.^) :: (GHC.Num.Num a, GHC.Real.Integral b) => x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 && y /= 0) <=> z == 0)}+assume (GHC.Internal.Real.^) :: x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 && y /= 0) <=> z == 0)} -assume GHC.Real.fromIntegral :: (GHC.Real.Integral a, GHC.Num.Num b) => x:a -> {v:b|v=x}+assume GHC.Internal.Real.fromIntegral :: x:a -> {v:b|v=x} -class (GHC.Num.Num a) => GHC.Real.Fractional a where- (GHC.Real./) :: x:a -> y:{v:a | v /= 0} -> {v:a | v == x / y}- GHC.Real.recip :: a -> a- GHC.Real.fromRational :: GHC.Real.Ratio Integer -> a+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 (GHC.Real.Real a, GHC.Enum.Enum a) => GHC.Real.Integral a where- GHC.Real.quot :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) &&+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)) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x) }- GHC.Real.rem :: x:a -> y:{v:a | v /= 0} -> {v:a | ((v >= 0) && (v < y))}- GHC.Real.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.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))} - GHC.Real.div :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) &&+ GHC.Internal.Real.div :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x) && ((1 < y) => v < x ) && ((y >= 1) => v <= x) }- GHC.Real.quotRem :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) &&+ GHC.Internal.Real.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.Real.divMod :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) &&+ GHC.Internal.Real.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.Real.toInteger :: x:a -> {v:Integer | v = x}+ GHC.Internal.Real.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) }
src/GHC/Word_LHAssumptions.hs view
@@ -1,10 +1,4 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} module GHC.Word_LHAssumptions where -{-@-embed GHC.Word.Word as int-embed GHC.Word.Word8 as int-embed GHC.Word.Word16 as int-embed GHC.Word.Word32 as int-embed GHC.Word.Word64 as int-@-}+import GHC.Internal.Word_LHAssumptions()
src/Liquid/Prelude/Real_LHAssumptions.hs view
@@ -4,5 +4,5 @@ import GHC.Num() {-@-assume GHC.Num.* :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x * y} +assume GHC.Internal.Num.* :: (GHC.Internal.Num.Num a) => x:a -> y:a -> {v:a | v = x * y} @-}
src/Liquid/Prelude/Totality_LHAssumptions.hs view
@@ -7,13 +7,13 @@ {-@ measure totalityError :: a -> Bool -assume Control.Exception.Base.patError :: {v:GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a+assume GHC.Internal.Control.Exception.Base.patError :: {v:GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a -assume Control.Exception.Base.recSelError :: {v:GHC.Prim.Addr# | totalityError "Use of partial record field selector"} -> a+assume GHC.Internal.Control.Exception.Base.recSelError :: {v:GHC.Prim.Addr# | totalityError "Use of partial record field selector"} -> a -assume Control.Exception.Base.nonExhaustiveGuardsError :: {v:GHC.Prim.Addr# | totalityError "Guards are non-exhaustive"} -> a+assume GHC.Internal.Control.Exception.Base.nonExhaustiveGuardsError :: {v:GHC.Prim.Addr# | totalityError "Guards are non-exhaustive"} -> a -assume Control.Exception.Base.noMethodBindingError :: {v:GHC.Prim.Addr# | totalityError "Missing method(s) on instance declaration"} -> a+assume GHC.Internal.Control.Exception.Base.noMethodBindingError :: {v:GHC.Prim.Addr# | totalityError "Missing method(s) on instance declaration"} -> a -assume Control.Exception.Base.recConError :: {v:GHC.Prim.Addr# | totalityError "Missing field in record construction"} -> a+assume GHC.Internal.Control.Exception.Base.recConError :: {v:GHC.Prim.Addr# | totalityError "Missing field in record construction"} -> a @-}
src/Prelude_LHAssumptions.hs view
@@ -6,15 +6,14 @@ import GHC.Maybe_LHAssumptions() import GHC.Num_LHAssumptions() import GHC.Num.Integer_LHAssumptions()+import GHC.Num.Integer() import GHC.Real_LHAssumptions() import Liquid.Prelude.Real_LHAssumptions() import Liquid.Prelude.Totality_LHAssumptions() {-@ -assume GHC.Err.error :: {v:_ | false} -> a--embed Integer as int+assume GHC.Internal.Err.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