diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 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.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 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 @@ -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 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 @@ -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 @-} 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,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() diff --git a/src/Data/Int_LHAssumptions.hs b/src/Data/Int_LHAssumptions.hs deleted file mode 100644 --- a/src/Data/Int_LHAssumptions.hs +++ /dev/null @@ -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 - -@-} 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,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 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 @@ -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 } @-} 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 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 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,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() 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.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 @-} 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 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))) @-} 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 @@ -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` 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 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 @-} 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 @@ -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 () 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,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

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.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() 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,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 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 @@ -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)) @-} 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 @@ -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}) @-} 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.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} @-} diff --git a/src/GHC/Internal/Base_LHAssumptions.hs b/src/GHC/Internal/Base_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Internal/Base_LHAssumptions.hs @@ -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

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 new file mode 100644 --- /dev/null +++ b/src/GHC/Internal/Data/Foldable_LHAssumptions.hs @@ -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)} +@-} diff --git a/src/GHC/Internal/Data/Maybe_LHAssumptions.hs b/src/GHC/Internal/Data/Maybe_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Internal/Data/Maybe_LHAssumptions.hs @@ -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 +@-} diff --git a/src/GHC/Internal/Float_LHAssumptions.hs b/src/GHC/Internal/Float_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Internal/Float_LHAssumptions.hs @@ -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 +@-} diff --git a/src/GHC/Internal/Int_LHAssumptions.hs b/src/GHC/Internal/Int_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Internal/Int_LHAssumptions.hs @@ -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 + +@-} diff --git a/src/GHC/Internal/List_LHAssumptions.hs b/src/GHC/Internal/List_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Internal/List_LHAssumptions.hs @@ -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 +@-} diff --git a/src/GHC/Internal/Num_LHAssumptions.hs b/src/GHC/Internal/Num_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Internal/Num_LHAssumptions.hs @@ -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 } +@-} diff --git a/src/GHC/Internal/Word_LHAssumptions.hs b/src/GHC/Internal/Word_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Internal/Word_LHAssumptions.hs @@ -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 } +@-} 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,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() 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 @@ -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 @-} 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,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() 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.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 @-} 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 @@ -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) } 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,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() 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 @@ -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} @-} 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 @@ -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 @-} diff --git a/src/Prelude_LHAssumptions.hs b/src/Prelude_LHAssumptions.hs --- a/src/Prelude_LHAssumptions.hs +++ b/src/Prelude_LHAssumptions.hs @@ -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