liquidhaskell 0.9.2.5.0 → 0.9.2.8.0
raw patch · 5 files changed
+28/−23 lines, 5 filesdep ~bytestringdep ~liquidhaskell-boot
Dependency ranges changed: bytestring, liquidhaskell-boot
Files
- CHANGES.md +5/−1
- README.md +11/−10
- liquidhaskell.cabal +7/−7
- src/Data/ByteString_LHAssumptions.hs +1/−1
- src/GHC/Types_LHAssumptions.hs +4/−4
CHANGES.md view
@@ -1,6 +1,10 @@ # Changes -## NEXT 0.9.XX+## 0.9.2.8.0++- Support for GHC 9.2.8+- Fix A normalization when type binder and lets are mixed in the input (#2236)+- Move KMeansHelper from liquid-prelude to tests ## 0.9.2.5
README.md view
@@ -165,14 +165,15 @@ Comparison charts in `svg` format can be generated by invoking ```-cabal v2-run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50 -f "benchmark" -o outdir+cabal v2-run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50 -f "benchmark" ``` This will generate three files `filtered.svg` (a subset of tests with a `benchmark` prefix, enabled by the `-f` option),-`top.svg` and `bot.svg` (top 50 speedups and slowdowns over the entire test set, both enabled by the `-s` option) under-the `outdir` directory. The `-f` and `-s` options can be used/omitted independently. If both are omitted, a single-`perf.svg` will be produced covering the full input test set. Additionally, their effects can be combined by providing-a third `-c` option (this will produce 2 files `filtered-top.svg` and `filtered-bot.svg` instead of 3).+`top.svg` and `bot.svg` (top 50 speedups and slowdowns over the entire test set, both enabled by the `-s` option) in the+current directory. The `-f` and `-s` options can be used/omitted independently. If both are omitted, a single `perf.svg`+will be produced covering the full input test set. Additionally, their effects can be combined by providing a third `-c`+option (this will produce 2 files `filtered-top.svg` and `filtered-bot.svg` instead of 3). An optional key `-o` can be+supplied to specify an output directory for the generated files. There is also a legacy script `scripts/plot-performance/chart_perf.sh` that can be used to generate comparison charts in both `svg` and `png` formats. It requires [gnuplot](http://www.gnuplot.info/) to run and assumes both files contain@@ -357,14 +358,14 @@ [BareSpec]: liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L362 [LiftedSpec]: liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L559 [TargetSrc]: liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L158-[Ghc monad]: https://hackage.haskell.org/package/ghc-9.2.5/docs/GHC.html#t:Ghc-[HscEnv]: https://hackage.haskell.org/package/ghc-9.2.5/docs/GHC.html#t:HscEnv-[DynFlags]: https://hackage.haskell.org/package/ghc-9.2.5/docs/GHC.html#t:DynFlags-[GhcMonad]: https://hackage.haskell.org/package/ghc-9.2.5/docs/GHC.html#t:GhcMonad+[Ghc monad]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:Ghc+[HscEnv]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:HscEnv+[DynFlags]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:DynFlags+[GhcMonad]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:GhcMonad [typechecking phase]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L211-L226 [ghcide]: https://github.com/haskell/ghcide [findRelevantSpecs]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs#L65-[core binds]: https://hackage.haskell.org/package/ghc-9.2.5/docs/CoreSyn.html#t:CoreBind+[core binds]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC-Core.html#t:CoreBind [configureGhcTargets]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L254 [processTargetModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L483 [processModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L509
liquidhaskell.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-version: 0.9.2.5.0+version: 0.9.2.8.0 synopsis: Liquid Types for Haskell description: Liquid Types for Haskell. license: BSD-3-Clause@@ -11,9 +11,9 @@ category: Language homepage: https://github.com/ucsd-progsys/liquidhaskell build-type: Custom-tested-with: GHC == 9.2.5-extra-source-files: CHANGES.md- README.md+tested-with: GHC == 9.2.8+extra-doc-files: CHANGES.md+ README.md source-repository head type: git@@ -77,9 +77,9 @@ hs-source-dirs: src build-depends: base >= 4.11.1.0 && < 5,- liquidhaskell-boot == 0.9.2.5.0,- bytestring == 0.11.3.1,- containers == 0.6.5.1,+ liquidhaskell-boot == 0.9.2.8.0,+ bytestring == 0.11.4.0,+ containers == 0.6.5.1, ghc-prim default-language: Haskell98 ghc-options: -Wall -fplugin=LiquidHaskellBoot
src/Data/ByteString_LHAssumptions.hs view
@@ -12,7 +12,7 @@ invariant { bs : Data.ByteString.ByteString | bslen bs == stringlen bs } -assume Data.ByteString.Internal.empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 }+assume Data.ByteString.Internal.Type.empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 } assume Data.ByteString.singleton :: _ -> { bs : Data.ByteString.ByteString | bslen bs == 1 }
src/GHC/Types_LHAssumptions.hs view
@@ -26,15 +26,15 @@ embed GHC.Integer.Type.Integer as int embed GHC.Num.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 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 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:_ -> {v:GHC.Types.Word | v == w }+assume GHC.Types.W# :: w:GHC.Prim.Word# -> {v:GHC.Types.Word | v == w } measure addrLen :: GHC.Prim.Addr# -> GHC.Types.Int