packages feed

liquidhaskell 0.9.12.2 → 0.9.12.2.1

raw patch · 13 files changed

+193/−82 lines, 13 filesdep ~liquidhaskell-bootPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: liquidhaskell-boot

API changes (from Hackage documentation)

Files

CHANGES.md view
@@ -2,6 +2,30 @@  ## Next +## 0.9.12.2.1 (2026-01-14)++- Disable LH when collecting Haddock comments and the noBackend is set [#2611](https:://github.com/ucsd-progsys/liquidhaskell/pull/2611)+- Make assume reflect error sensitive to dflags [#2607](https:://github.com/ucsd-progsys/liquidhaskell/pull/2607)+- Add a flag to dump the a-normalized core [#2605](https:://github.com/ucsd-progsys/liquidhaskell/pull/2605)+- Show solutions of non-cut kvars in error messages [#2596](https:://github.com/ucsd-progsys/liquidhaskell/pull/2596)+- Remove question marks as a distinction of predicates from other expressions [#2595](https:://github.com/ucsd-progsys/liquidhaskell/pull/2595)+- Require braces when declaring qualifier [#2594](https:://github.com/ucsd-progsys/liquidhaskell/pull/2594)+- Retire implementation of gradual refinement types [#2588](https:://github.com/ucsd-progsys/liquidhaskell/pull/2588)+- Remove old versions of PLE [#2587](https:://github.com/ucsd-progsys/liquidhaskell/pull/2587)+- Add new syntax for indexed types (Ix instead of Prop) [#2586](https:://github.com/ucsd-progsys/liquidhaskell/pull/2586)+- Handle `ByteArray#` as int in the logic [#2581](https:://github.com/ucsd-progsys/liquidhaskell/pull/2581)+- Do not ignore user qualifiers when using `--reflection` [#2580](https:://github.com/ucsd-progsys/liquidhaskell/pull/2580)+- Add set cardinality support when using cvc5 [#2577](https:://github.com/ucsd-progsys/liquidhaskell/pull/2577)+- Support the finite field theory when using cvc5 [#2571](https:://github.com/ucsd-progsys/liquidhaskell/pull/2571) [#2614](https:://github.com/ucsd-progsys/liquidhaskell/pull/2614)+- Allow to qualify predicate aliases [#2566](https:://github.com/ucsd-progsys/liquidhaskell/pull/2566)+- Implement stratified types [#2559](https:://github.com/ucsd-progsys/liquidhaskell/pull/2559)+- Resolve occurrences of imported opaquely-reflected functions [#2548](https:://github.com/ucsd-progsys/liquidhaskell/pull/2548)+- Allow to qualify type aliases [#2550](https:://github.com/ucsd-progsys/liquidhaskell/pull/2550)+- Print the amount of checked constraints when verification fails [#2545](https:://github.com/ucsd-progsys/liquidhaskell/pull/2545)+- Fix SMT crashes on reflected functions on polymorphic data types [#2542](https://github.com/ucsd-progsys/liquidhaskell/pull/2542)+- Look for cvc5 before cvc4 [#2513](https://github.com/ucsd-progsys/liquidhaskell/pull/2513)+- Change `--cores` default to 1 [#2564](https://github.com/ucsd-progsys/liquidhaskell/pull/2564)+ ## 0.9.12.2 (2025-03-22)  - Simplify kvar solutions in fqout files [liquid-fixpoint#741](https://github.com/ucsd-progsys/liquid-fixpoint/pull/741).
README.md view
@@ -7,6 +7,41 @@  If you're a LiquidHaskell **user** (or just curious), you probably want to go to [the documentation website](https://ucsd-progsys.github.io/liquidhaskell/) instead. +## Trying it from Hackage++Assuming the [Z3](https://github.com/Z3Prover/z3) SMT solver is installed and+available in your `PATH`, you can run++```+cabal install --lib liquidhaskell liquid-prelude liquid-vector --package-env . --force-reinstalls+ghc -fplugin=LiquidHaskell FILE.hs+```++`--package-env .` creates a `.ghc.environment*` file in the current folder that makes+`ghc` find the `LiquidHaskell` plugin only when invoking it from there.+Otherwise, global user configuration would be affected.++Note that the installation step is influenced by the dependencies that are+already installed in your system, so different results may be obtained by+different users.++## Trying it from GitHub++The github repo only builds with GHC 9.12.2, which must be in your `PATH`.++```+git clone https://github.com/ucsd-progsys/liquidhaskell.git+cd liquidhaskell+git submodule update --init+cabal build liquidhaskell liquid-prelude liquid-vector++cabal exec -- ghc -fplugin=LiquidHaskell FILE.hs+```++## Asking for Help++If you have questions or you just need help, you can always reach out on our [slack channel](https://join.slack.com/t/liquidhaskell/shared_invite/enQtMjY4MTk3NDkwODE3LTFmZGFkNGEzYWRkNDJmZDQ0ZGU1MzBiZWZiZDhhNmY3YTJiMjUzYTRlNjMyZDk1NDU3ZGIxYzhlOTIzN2UxNWE), [google groups mailing list](https://groups.google.com/forum/#!forum/liquidhaskell), [GitHub issue tracker](https://github.com/ucsd-progsys/liquidhaskell/issues), or by emailing [Ranjit Jhala](https://github.com/ranjitjhala), [Niki Vazou](https://github.com/nikivazou).+ # Contributing  This is an open-source project, and we love getting feedback (and patches)!@@ -36,30 +71,11 @@  Pull requests don't just have to be about code: documentation can often be improved too! -## Ask for Help--If you have further questions or you just need help, you can always reach out on our [slack channel](https://join.slack.com/t/liquidhaskell/shared_invite/enQtMjY4MTk3NDkwODE3LTFmZGFkNGEzYWRkNDJmZDQ0ZGU1MzBiZWZiZDhhNmY3YTJiMjUzYTRlNjMyZDk1NDU3ZGIxYzhlOTIzN2UxNWE), [google groups mailing list](https://groups.google.com/forum/#!forum/liquidhaskell), [GitHub issue tracker](https://github.com/ucsd-progsys/liquidhaskell/issues), or by emailing [Ranjit Jhala](https://github.com/ranjitjhala), [Niki Vazou](https://github.com/nikivazou).- # General Development Guide  For those diving into the implementation of LiquidHaskell, here are a few tips: -## Running the pluging on individual files--```-cabal build liquidhaskell-cabal exec ghc -- -fplugin=LiquidHaskell FILE.hs-```--## Building--### Cabal--```-cabal build-```--### Faster recompilation+## Faster recompilation  When changing the `liquidhaskell-boot` library, sometimes we don't want to rebuild `liquidhaskell` or `liquid-vector` when testing the changes.@@ -114,6 +130,15 @@  ## How to create performance comparison charts +Firstly, make sure to remove previous compilation artifacts of tests before measuring performance,+or GHC will skip running Liquid Haskell on modules that don't need recompilation. Unfortunately,+using `-fforce-recomp` is not ideal (see [#2565](https://github.com/ucsd-progsys/liquidhaskell/pull/2565)+for more details). At the time of writing, previous compilation artifacts of tests can be removed with++```bash+find dist-newstyle -name "tests-*" -o -name "prover-ple-lib-*" | xargs rm -r+```+ When `liquidhaskell` tests run, we can collect timing information with      $ ./scripts/test/test_plugin.sh --measure-timings@@ -128,21 +153,26 @@  which will produce `tmp/*.json` files. -Then a csv report can be generated from this json files with+Then a csv report can be generated from the json files with ```-cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskell -o summary.csv+cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskellCPU -o summary.csv ```-On each line, the report will contain the time taken by each test.+On each line, the report will contain the the wall-clock time taken by each test.+Use `--phase LiquidHaskell` to get the wall-clock time instead. Although in that+case you need to use the `--measure-timings-j1` option when running the tests,+which validates modules one at a time.  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"+cabal v2-run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50 ``` -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) in the-current directory. The `-f` and `-s` options can be used/omitted independently. If both are omitted, a single `perf.svg`+This will generate two files `top.svg` and `bot.svg` containing the top 50 speedups and slowdowns+over the entire test set, both enabled by the `-s` option) in the current directory. Alternatively,+a subset of the tests can be selected by a prefix of their names with `-f <prefix>`, for instance+`-f benchmarks`. `-f` will generate a file `filtered.svg` containing the comparisons of the selected tests.+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.@@ -315,3 +345,51 @@ [processTargetModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L483 [processModule]:       liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L509 +# Module Verification Process++The following graph summarizes the verification process of a module by showing+its specification life cycle.+See [Specs.hs](./liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs)+for detailed documentation on the specification stages.+There are many moving parts hidden within each graph link,+but some places worth noticing here are+[Liquid.hs](./liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs)+—which implements constraint generation— and+[SpecFinder.hs](./liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs)+—that deals with the gathering of dependencies and `LHAssumptions`—.++```mermaid+flowchart LR+  subgraph Liquid Haskell++    subgraph Inputs+      direction TB+      LiftedDeps[+        Dependencies of A+        LifttedSpecs+        ]+      CoreBinds[CoreBinds]+      Bare[BarseSpec]+    end++    subgraph Outputs+      direction TB+      T[TargetSpec] --> Constraints[Verification+                                    Constraints]+      L[LiftedSpec]+    end++    Inputs --> Outputs++  end++  A>DepsOfA_LHAssumptions] --> LiftedDeps+  Deps>DepsOfA.hi] --> LiftedDeps+  Mod(A.hs) --> CoreBinds & Bare+  Constraints -->|checked by| fixpoint([liquid-fixpoint])+  L ---> |if verified:+           serialize| File>A.hi]+```++Reference:+[Implementing a GHC Plugin for Liquid Haskell](https://well-typed.com/blog/2020/08/implementing-a-ghc-plugin-for-liquid-haskell/).
liquidhaskell.cabal view
@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquidhaskell-version:            0.9.12.2+version:            0.9.12.2.1 synopsis:           Liquid Types for Haskell description:        Liquid Types for Haskell. license:            BSD-3-Clause@@ -37,6 +37,7 @@                       Data.Bits_LHAssumptions                       Data.Either_LHAssumptions                       Data.Foldable_LHAssumptions+                      Data.Int_LHAssumptions                       Data.List_LHAssumptions                       Data.Maybe_LHAssumptions                       Data.String_LHAssumptions@@ -78,7 +79,7 @@   hs-source-dirs:     src    build-depends:      base                 >= 4.11.1.0 && < 5,-                      liquidhaskell-boot   == 0.9.12.2,+                      liquidhaskell-boot   == 0.9.12.2.1,                       bytestring,                       containers,                       ghc-prim@@ -87,3 +88,4 @@    if flag(devel)     ghc-options:      -Werror+
+ src/Data/Int_LHAssumptions.hs view
@@ -0,0 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}+module Data.Int_LHAssumptions where++import GHC.Int_LHAssumptions()
src/Data/Set_LHAssumptions.hs view
@@ -3,7 +3,6 @@ module Data.Set_LHAssumptions where  import Data.Set-import Data.Set.Internal as I import GHC.Types_LHAssumptions() import Prelude hiding (null) @@ -18,6 +17,7 @@ assume isSubsetOf    :: (Ord a) => x:(Set a) -> y:(Set a) -> {v:Bool | v <=> Set_sub x y} assume member        :: Ord a => x:a -> xs:(Set a) -> {v:Bool | v <=> Set_mem x xs} assume null          :: Ord a => xs:(Set a) -> {v:Bool | v <=> Set_emp xs}+assume size          :: xs:(Set a) -> {v:Nat | v = Set_card xs}  assume empty         :: {v:(Set a) | Set_emp v} assume singleton     :: x:a -> {v:(Set a) | v = (Set_sng x)}@@ -45,18 +45,9 @@ define difference x y   = (Set_dif x y) define empty            = (Set_empty 0) define null x           = (Set_emp x)+define size x           = (Set_card x) define member x xs      = (Set_mem x xs) define isSubsetOf x y   = (Set_sub x y) define fromList xs      = (Data.Set_LHAssumptions.listElts xs)--define I.singleton x      = (Set_sng x)-define I.union x y        = (Set_cup x y)-define I.intersection x y = (Set_cap x y)-define I.difference x y   = (Set_dif x y)-define I.empty            = (Set_empty 0)-define I.null x           = (Set_emp x)-define I.member x xs      = (Set_mem x xs)-define I.isSubsetOf x y   = (Set_sub x y)-define I.fromList xs      = (Data.Set_LHAssumptions.listElts xs)  @-}
src/Data/Tuple_LHAssumptions.hs view
@@ -14,6 +14,6 @@ measure snd :: (a, b) -> b   snd (a, b) = b -qualif Fst(__v:a, __y:b): (__v = (fst __y))-qualif Snd(__v:a, __y:b): (__v = (snd __y))+qualif Fst(__v:a, __y:b) { __v = (fst __y) }+qualif Snd(__v:a, __y:b) { __v = (snd __y) } @-}
src/GHC/Base_LHAssumptions.hs view
@@ -41,24 +41,24 @@  assume id        :: x:a -> {v:a | v = x} -qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs > 0))-qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs = 0))+qualif IsEmp(v:Bool, xs: [a])  { v <=> (len xs > 0) }+qualif IsEmp(v:Bool, xs: [a])  { v <=> (len xs = 0) } -qualif ListZ(v: [a])          : (len v =  0)-qualif ListZ(v: [a])          : (len v >= 0)-qualif ListZ(v: [a])          : (len v >  0)+qualif 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 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 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)+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/List_LHAssumptions.hs view
@@ -52,8 +52,8 @@ assume reverse      :: xs:[a] -> {v: [a] | len(v) = len(xs)}  //  Copy-pasted from len.hquals-qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys]))-qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))+qualif LenSum(v:[a], xs:[b], ys:[c]) { len([v]) = (len([xs]) + len([ys])) }+qualif LenSum(v:[a], xs:[b], ys:[c]) { len([v]) = (len([xs]) - len([ys])) }  assume !! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a
src/GHC/Num/Integer_LHAssumptions.hs view
@@ -10,5 +10,7 @@ {-@ assume GHC.Num.Integer.IS :: x:Int# -> {v: Integer | v = (x :: int) } +define GHC.Num.Integer.IS x = (x)+ embed Integer as int @-}
src/GHC/Num_LHAssumptions.hs view
@@ -14,6 +14,8 @@  assume abs :: (Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) } +define abs x = if x >=0 then x else -x+ assume + :: x:a -> y:a -> {v:a | v = x + y } assume - :: (Num a) => x:a -> y:a -> {v:a | v = x - y } @-}
src/GHC/Real_LHAssumptions.hs view
@@ -5,6 +5,7 @@  import GHC.Real import GHC.Types_LHAssumptions()+import GHC.Num_LHAssumptions()  {-@ assume (^) :: x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 && y /= 0) <=> z == 0)}@@ -49,6 +50,12 @@  define div x y        = (x / y) define mod x y        = (x mod y)+define quot x y =  if x >= 0+                   then (if y >= 0 then x / y else -(x / -y))+                   else -(-x / y)+define rem x y = if x >= 0+                 then (if y >= 0 then x mod y else x mod -y)+                 else - (-x mod y) define fromIntegral x = (x)  @-}
src/GHC/Types_LHAssumptions.hs view
@@ -26,6 +26,7 @@ embed Char    as Char embed Char#    as Char embed Addr#    as Str+embed ByteArray# as int  embed Integer as int
src/Prelude_LHAssumptions.hs view
@@ -25,38 +25,38 @@  // BOT: Do not delete EVER! -qualif Bot(v:@(0))    : (0 = 1)-qualif Bot(v:obj)     : (0 = 1)-qualif Bot(v:a)       : (0 = 1)-qualif Bot(v:bool)    : (0 = 1)-qualif Bot(v:int)     : (0 = 1)+qualif Bot(v:@(0))     { 0 = 1 }+qualif Bot(v:obj)      { 0 = 1 }+qualif Bot(v:a)        { 0 = 1 }+qualif Bot(v:bool)     { 0 = 1 }+qualif Bot(v:int)      { 0 = 1 } -qualif CmpZ(v:a)      : (v <  0)-qualif CmpZ(v:a)      : (v <= 0)-qualif CmpZ(v:a)      : (v >  0)-qualif CmpZ(v:a)      : (v >= 0)-qualif CmpZ(v:a)      : (v  = 0)-qualif CmpZ(v:a)      : (v != 0)+qualif CmpZ(v:a)       { v <  0 }+qualif CmpZ(v:a)       { v <= 0 }+qualif CmpZ(v:a)       { v >  0 }+qualif CmpZ(v:a)       { v >= 0 }+qualif CmpZ(v:a)       { v  = 0 }+qualif CmpZ(v:a)       { v != 0 } -qualif Cmp(v:a, x:a)  : (v <  x)-qualif Cmp(v:a, x:a)  : (v <= x)-qualif Cmp(v:a, x:a)  : (v >  x)-qualif Cmp(v:a, x:a)  : (v >= x)-qualif Cmp(v:a, x:a)  : (v  = x)-qualif Cmp(v:a, x:a)  : (v != x)+qualif Cmp(v:a, x:a)   { v <  x }+qualif Cmp(v:a, x:a)   { v <= x }+qualif Cmp(v:a, x:a)   { v >  x }+qualif Cmp(v:a, x:a)   { v >= x }+qualif Cmp(v:a, x:a)   { v  = x }+qualif Cmp(v:a, x:a)   { v != x } -qualif One(v:int)     : v = 1-qualif True1(v:Bool)   : (v)-qualif False1(v:Bool)  : (~ v)+qualif One(v:int)      { v = 1 }+qualif True1(v:Bool)    { v }+qualif False1(v:Bool)   { ~ v }  //  REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])-qualif Papp(v:a, p:Pred a) : (papp1 p v)+qualif Papp(v:a, p:Pred a)  { papp1 p v }  //  REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])-qualif Papp2(v:a, x:b, p:Pred a b) : (papp2 p v x)+qualif Papp2(v:a, x:b, p:Pred a b)  { papp2 p v x }  //  REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])-qualif Papp3(v:a, x:b, y:c, p:Pred a b c) : (papp3 p v x y)+qualif Papp3(v:a, x:b, y:c, p:Pred a b c)  { papp3 p v x y }  //  qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z) //  REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])