From 28ad5d1dfe3631565601f70bcab71c88facaf9db Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Thu, 3 Jul 2025 01:03:19 -0700 Subject: [PATCH] :arrow_up: Bump version to 0.13.0.0, update dependencies --- .github/workflows/test.yml | 6 +- CHANGELOG.md | 130 ++++++++++++------------ README.md | 6 +- examples/grisette-examples.cabal | 8 +- examples/package.yaml | 6 +- flake.lock | 36 +++---- flake.nix | 10 +- grisette.cabal | 14 +-- hie.yaml | 4 - package.yaml | 8 +- src/Grisette/Internal/SymPrim/SomeBV.hs | 17 ++-- stack-9.10.yaml | 2 +- stack-9.10.yaml.lock | 10 +- stack.yaml.lock | 8 +- 14 files changed, 135 insertions(+), 130 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index cf3d588f..44ab59ca 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -23,11 +23,11 @@ jobs: - {build: nix, arg: "", ismain: false, experimental: false, ghc: "948", cachekey: "nix-948"} - {build: nix, arg: "", ismain: false, experimental: false, ghc: "966", cachekey: "nix-966"} - {build: nix, arg: "", ismain: false, experimental: false, ghc: "984", cachekey: "nix-984"} - - {build: nix, arg: "", ismain: true, experimental: false, ghc: "9101", cachekey: "nix-9101"} - - {build: cabal, arg: "", ismain: false, experimental: false, ghc: "9121", cachekey: "cabal-9121"} + - {build: nix, arg: "", ismain: true, experimental: false, ghc: "9102", cachekey: "nix-9102"} + - {build: nix, arg: "", ismain: false, experimental: false, ghc: "9122", cachekey: "nix-9122"} include: - os: macOS-latest - plan: {build: nix, arg: "", ismain: true, experimental: false, ghc: "9101", cachekey: "nix-9101"} + plan: {build: nix, arg: "", ismain: true, experimental: false, ghc: "9102", cachekey: "nix-9102"} runs-on: ${{ matrix.os }} continue-on-error: ${{ matrix.plan.experimental }} steps: diff --git a/CHANGELOG.md b/CHANGELOG.md index 1d191ac1..c504d875 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,13 +6,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [Unreleased] +## [0.13.0.0] -- 2025-07-03 ### Added - Added missing instances for `ArithException`. ([#292](https://github.com/lsrcz/grisette/pull/292)) -- \[Breaking\] Added `Integral` instances for `SymInteger`, `SymIntN`, and +- [Breaking] Added `Integral` instances for `SymInteger`, `SymIntN`, and `SymWordN`. Also make `(/)`, `recip` and `logBase` no longer throw errors for `SymAlgReal`. These functions are "unsafe" and should be used with caution as they expose undefined behavior for some inputs. @@ -32,14 +32,14 @@ and this project adheres to - Removed `Show` constraints for merging indices. ([#294](https://github.com/lsrcz/grisette/pull/294)) -- \[Breaking\] Removed `Hashable` instances for `SymBool`, and also, `Eq` now +- [Breaking] Removed `Hashable` instances for `SymBool`, and also, `Eq` now errors when called. Added `AsKey` wrapper to recover the original behavior. ([#299](https://github.com/lsrcz/grisette/pull/299)) - Make `GetData` now accept one parameter instead of two so that `GetData mode` can be used as a type in a context where we want a monad. The `BaseMonad` is now a type alias of `GetData`. ([#302](https://github.com/lsrcz/grisette/pull/302)) -- \[Breaking\] Renamed `PlainUnion` to `UnionView`. +- [Breaking] Renamed `PlainUnion` to `UnionView`. ([#302](https://github.com/lsrcz/grisette/pull/302)) - Implemented `UnionView` for `Identity`. ([#302](https://github.com/lsrcz/grisette/pull/302)) @@ -81,7 +81,7 @@ and this project adheres to guards. ([#283](https://github.com/lsrcz/grisette/pull/283)) - `EvalModeConvertible` is now reflexive. ([#284](https://github.com/lsrcz/grisette/pull/284)) -- \[Breaking\] Renamed `deriveGADT` to `derive`. +- [Breaking] Renamed `deriveGADT` to `derive`. ([#286](https://github.com/lsrcz/grisette/pull/286)) ### Fixed @@ -101,11 +101,11 @@ and this project adheres to ### Changed -- \[Breaking\] We no longer support direct `toCon` from a union to a single - value or `toSym` from a single value to a union. These should now be done - through `mrgToSym`, `toUnionSym`, and `unionToCon`. +- [Breaking] We no longer support direct `toCon` from a union to a single value + or `toSym` from a single value to a union. These should now be done through + `mrgToSym`, `toUnionSym`, and `unionToCon`. ([#267](https://github.com/lsrcz/grisette/pull/267)) -- \[Breaking\] Changed the `EvalMode` tag for `Con` to `C` and `Sym` to `S`. +- [Breaking] Changed the `EvalMode` tag for `Con` to `C` and `Sym` to `S`. ([#267](https://github.com/lsrcz/grisette/pull/267)) ### Fixed @@ -137,13 +137,13 @@ and this project adheres to ### Changed -- \[Breaking\] Improved the `SymFiniteBits` interface. +- [Breaking] Improved the `SymFiniteBits` interface. ([#262](https://github.com/lsrcz/grisette/pull/262)) -- \[Breaking\] Changed the smart constructor generation Template Haskell - procedure name to `makeSmartCtorWith`, `makePrefixedSmartCtorWith`, +- [Breaking] Changed the smart constructor generation Template Haskell procedure + name to `makeSmartCtorWith`, `makePrefixedSmartCtorWith`, `makeNamedSmartCtor`, and `makeSmartCtor`. ([#263](https://github.com/lsrcz/grisette/pull/263)) -- \[Breaking\] Renamed the evaluation mode tags `Con` and `Sym` to `C` and `S`. +- [Breaking] Renamed the evaluation mode tags `Con` and `Sym` to `C` and `S`. ([#264](https://github.com/lsrcz/grisette/pull/264)) ## [0.9.0.0] -- 2024-11-07 @@ -165,20 +165,20 @@ and this project adheres to ### Changed -- \[Breaking\] Moved the constraints for the general and tabular functions and +- [Breaking] Moved the constraints for the general and tabular functions and simplified their instances declaration. ([#249](https://github.com/lsrcz/grisette/pull/249)) -- \[Breaking\] Renamed `EvalMode` to `EvalModeAll`, renamed `MonadWithMode` to +- [Breaking] Renamed `EvalMode` to `EvalModeAll`, renamed `MonadWithMode` to `MonadEvalModeAll`. ([#250](https://github.com/lsrcz/grisette/pull/250)) - Improved parallel symbolic evaluation performance. ([#252](https://github.com/lsrcz/grisette/pull/252)) -- \[Breaking\] Changed the metadata for identifiers from existential arguments - to s-expressions. ([#253](https://github.com/lsrcz/grisette/pull/253)) -- \[Breaking\] Changed the solving/cegis results from maintaining the exception +- [Breaking] Changed the metadata for identifiers from existential arguments to + s-expressions. ([#253](https://github.com/lsrcz/grisette/pull/253)) +- [Breaking] Changed the solving/cegis results from maintaining the exception themselves to maintaining a textual representation of them. ([#253](https://github.com/lsrcz/grisette/pull/253)) -- \[Breaking\] Changed the 'VerifierResult' type for CEGIS to allow it report - that the verifier cannot find a counter example. +- [Breaking] Changed the 'VerifierResult' type for CEGIS to allow it report that + the verifier cannot find a counter example. ([#257](https://github.com/lsrcz/grisette/pull/257)) ### Fixed @@ -238,19 +238,19 @@ and this project adheres to ### Changed -- \[Breaking\] Changed the operand order for `liftPFormatPrec2` and +- [Breaking] Changed the operand order for `liftPFormatPrec2` and `liftPFormatList2`. ([#225](https://github.com/lsrcz/grisette/pull/225)) -- \[Breaking\] Changed the term representation with a compile-time tag for its +- [Breaking] Changed the term representation with a compile-time tag for its kind (`AnyKind` for all symbols and `ConstantKind` for symbols other than uninterpreted functions). This also affects the 'ExtractSym'. A new `extractSymMaybe` will regard this tag if not all symbols can be casted to that tag. `extractSym` will always succeed, returning a set with `AnyKind`. ([#230](https://github.com/lsrcz/grisette/pull/230)) -- \[Breaking\] `SafeDivision` renamed to `SafeDiv`. +- [Breaking] `SafeDivision` renamed to `SafeDiv`. ([#231](https://github.com/lsrcz/grisette/pull/231)) - Refined the template-haskell-based derivation mechanism. ([#238](https://github.com/lsrcz/grisette/pull/238)) -- \[Breaking\] `GetData` is made injective by giving `Identity` wrapped type for +- [Breaking] `GetData` is made injective by giving `Identity` wrapped type for concrete evaluation instead of the type itself. ([#242](https://github.com/lsrcz/grisette/pull/242)) - Changed pprint for `Identity` to not to print the constructor. @@ -296,35 +296,35 @@ and this project adheres to ### Changed -- \[Breaking\] Relaxed constraints for type classes, according to +- [Breaking] Relaxed constraints for type classes, according to https://github.com/haskell/core-libraries-committee/issues/10. One problem this causes is that the instances for `Union` will no longer be able to always merge the results. This is unfortunate, but should not be critical. ([#213](https://github.com/lsrcz/grisette/pull/213), [#214](https://github.com/lsrcz/grisette/pull/214), [#221](https://github.com/lsrcz/grisette/pull/221)) -- \[Breaking\] Rewritten the generic derivation mechanism. +- [Breaking] Rewritten the generic derivation mechanism. ([#213](https://github.com/lsrcz/grisette/pull/213), [#214](https://github.com/lsrcz/grisette/pull/214), [#216](https://github.com/lsrcz/grisette/pull/216)) -- \[Breaking\] Changed the type class hierarchy for operations for functors, - e.g. `SEq1`, as described in +- [Breaking] Changed the type class hierarchy for operations for functors, e.g. + `SEq1`, as described in https://github.com/haskell/core-libraries-committee/issues/10. ([#216](https://github.com/lsrcz/grisette/pull/216)) -- \[Breaking\] Renamed `UnionMergeable1` to `SymBranching`. Renamed `Union` to +- [Breaking] Renamed `UnionMergeable1` to `SymBranching`. Renamed `Union` to `UnionBase`, and `UnionM` to `Union`. ([#214](https://github.com/lsrcz/grisette/pull/214), [#217](https://github.com/lsrcz/grisette/pull/217)) -- \[Breaking\] Renamed `EvaluateSym` to `EvalSym`. Renamed `SubstituteSym` to +- [Breaking] Renamed `EvaluateSym` to `EvalSym`. Renamed `SubstituteSym` to `SubstSym`. Renamed `ExtractSymbolics` to `ExtractSym`. ([#217](https://github.com/lsrcz/grisette/pull/217)) -- \[Breaking\] Renamed `SEq` to `SymEq`. Renamed `SOrd` to `SymOrd`. +- [Breaking] Renamed `SEq` to `SymEq`. Renamed `SOrd` to `SymOrd`. ([#217](https://github.com/lsrcz/grisette/pull/217)) -- \[Breaking\] Renamed `GPretty` to `PPrint`. +- [Breaking] Renamed `GPretty` to `PPrint`. ([#217](https://github.com/lsrcz/grisette/pull/217), [#224](https://github.com/lsrcz/grisette/pull/224)) -- \[Breaking\] Discourage the use of approximation with `approx`. `precise` is - now the default and we do not require `precise` to be used everytime we call a +- [Breaking] Discourage the use of approximation with `approx`. `precise` is now + the default and we do not require `precise` to be used everytime we call a solver. ([#218](https://github.com/lsrcz/grisette/pull/218)) ## [0.6.0.0] -- 2024-06-07 @@ -353,14 +353,14 @@ and this project adheres to ### Changed -- \[Breaking\] Equality test for `SomeBV` with different bit widths will now +- [Breaking] Equality test for `SomeBV` with different bit widths will now return false rather than crash. ([#200](https://github.com/lsrcz/grisette/pull/200)) -- \[Breaking\] More intuitive CEGIS interface. +- [Breaking] More intuitive CEGIS interface. ([#201](https://github.com/lsrcz/grisette/pull/201)) -- \[Breaking\] Changed the low-level solver interface. +- [Breaking] Changed the low-level solver interface. ([#206](https://github.com/lsrcz/grisette/pull/206)) -- \[Breaking\] Changed the CEGIS interface. +- [Breaking] Changed the CEGIS interface. ([#206](https://github.com/lsrcz/grisette/pull/206)) - Bumped the minimum supported sbv version to 8.17. ([#207](https://github.com/lsrcz/grisette/pull/207)) @@ -408,32 +408,32 @@ and this project adheres to ### Changed -- \[Breaking\] Removed the `UnionLike` and `UnionPrjOp` interface, added the +- [Breaking] Removed the `UnionLike` and `UnionPrjOp` interface, added the `TryMerge` and `PlainUnion` interface. This allows `mrg*` operations to be used with non-union programs. ([#170](https://github.com/lsrcz/grisette/pull/170)) -- \[Breaking\] Refined the safe operations interface using `TryMerge`. +- [Breaking] Refined the safe operations interface using `TryMerge`. ([#172](https://github.com/lsrcz/grisette/pull/172)) -- \[Breaking\] Renamed `safeMinus` to `safeSub` to be more consistent. +- [Breaking] Renamed `safeMinus` to `safeSub` to be more consistent. ([#172](https://github.com/lsrcz/grisette/pull/172)) -- \[Breaking\] Unifies the implementation for all symbolic non-indexed +- [Breaking] Unifies the implementation for all symbolic non-indexed bit-vectors. The legacy types are now type and pattern synonyms. ([#174](https://github.com/lsrcz/grisette/pull/174), [#179](https://github.com/lsrcz/grisette/pull/179), [#180](https://github.com/lsrcz/grisette/pull/180)) -- \[Breaking\] Use functional dependency instead of type family for the - `Function` class. ([#178](https://github.com/lsrcz/grisette/pull/178)) -- \[Breaking\] Added `Mergeable` constraints to some `mrg*` list operators +- [Breaking] Use functional dependency instead of type family for the `Function` + class. ([#178](https://github.com/lsrcz/grisette/pull/178)) +- [Breaking] Added `Mergeable` constraints to some `mrg*` list operators ([#182](https://github.com/lsrcz/grisette/pull/182)) -- \[Breaking\] Refactored the `mrg*` constructor related template haskell code. +- [Breaking] Refactored the `mrg*` constructor related template haskell code. ([#185](https://github.com/lsrcz/grisette/pull/185)) -- \[Breaking\] Dropped symbols with extra information. +- [Breaking] Dropped symbols with extra information. ([#188](https://github.com/lsrcz/grisette/pull/188)) -- \[Breaking\] The `FreshIdent` is removed. It is now changed to `Identifier` - and `Symbol` types. ([#192](https://github.com/lsrcz/grisette/pull/192)) +- [Breaking] The `FreshIdent` is removed. It is now changed to `Identifier` and + `Symbol` types. ([#192](https://github.com/lsrcz/grisette/pull/192)) - Changed the internal representation of the terms. ([#193](https://github.com/lsrcz/grisette/pull/193)) -- \[Breaking\] Refactored the project structures. +- [Breaking] Refactored the project structures. ([#194](https://github.com/lsrcz/grisette/pull/194)) ## [0.4.1.0] -- 2024-01-10 @@ -474,11 +474,11 @@ and this project adheres to ### Removed -- \[Breaking\] Removed the `Grisette.Lib.Mtl` module. +- [Breaking] Removed the `Grisette.Lib.Mtl` module. ([#132](https://github.com/lsrcz/grisette/pull/132)) -- \[Breaking\] Removed `SymBoolOp` and `SymIntegerOp`. +- [Breaking] Removed `SymBoolOp` and `SymIntegerOp`. ([#146](https://github.com/lsrcz/grisette/pull/146)) -- \[Breaking\] Removed `ExtractSymbolics` instance for `SymbolSet`. +- [Breaking] Removed `ExtractSymbolics` instance for `SymbolSet`. ([#146](https://github.com/lsrcz/grisette/pull/146)) ### Fixed @@ -504,33 +504,33 @@ and this project adheres to - Reorganized the files for `MonadTrans`. ([#132](https://github.com/lsrcz/grisette/pull/132)) -- \[Breaking\] Changed the name of `Union` constructors and patterns. +- [Breaking] Changed the name of `Union` constructors and patterns. ([#133](https://github.com/lsrcz/grisette/pull/133)) - The `Union` patterns, when used as constructors, now merges the result. ([#133](https://github.com/lsrcz/grisette/pull/133)) - Changed the symbolic identifier type from `String` to `Data.Text.Text`. ([#141](https://github.com/lsrcz/grisette/pull/141)) -- \[Breaking\] `Grisette.Data.Class.BitVector.BVSignConversion` is now +- [Breaking] `Grisette.Data.Class.BitVector.BVSignConversion` is now `Grisette.Data.Class.SignConversion.SignConversion`. ([#142](https://github.com/lsrcz/grisette/pull/142)) -- \[Breaking\] Moved the `ITEOp`, `LogicalOp`, and `SEq` type classes to - dedicated modules. ([#146](https://github.com/lsrcz/grisette/pull/146)) -- \[Breaking\] Moved `Grisette.Data.Class.Evaluate` to +- [Breaking] Moved the `ITEOp`, `LogicalOp`, and `SEq` type classes to dedicated + modules. ([#146](https://github.com/lsrcz/grisette/pull/146)) +- [Breaking] Moved `Grisette.Data.Class.Evaluate` to `Grisette.Data.Class.EvaluateSym`. ([#146](https://github.com/lsrcz/grisette/pull/146)) -- \[Breaking\] Moved `Grisette.Data.Class.Substitute` to +- [Breaking] Moved `Grisette.Data.Class.Substitute` to `Grisette.Data.Class.SubstituteSym`. ([#146](https://github.com/lsrcz/grisette/pull/146)) -- \[Breaking\] Split the `Grisette.Data.Class.SafeArith` module to +- [Breaking] Split the `Grisette.Data.Class.SafeArith` module to `Grisette.Data.Class.SafeDivision` and `Grisette.Data.Class.SafeLinearArith`. ([#146](https://github.com/lsrcz/grisette/pull/146)) -- \[Breaking\] Changed the API to `MonadFresh`. +- [Breaking] Changed the API to `MonadFresh`. ([#156](https://github.com/lsrcz/grisette/pull/156)) -- \[Breaking\] Renamed multiple symbolic operators. +- [Breaking] Renamed multiple symbolic operators. ([#158](https://github.com/lsrcz/grisette/pull/158)) -- \[Breaking\] Changed the solver interface. +- [Breaking] Changed the solver interface. ([#159](https://github.com/lsrcz/grisette/pull/159)) -- \[Breaking\] Changed the CEGIS solver interface. +- [Breaking] Changed the CEGIS solver interface. ([#159](https://github.com/lsrcz/grisette/pull/159)) ## [0.3.1.1] -- 2023-09-29 @@ -644,6 +644,7 @@ No user-facing changes. [0.10.0.0]: https://github.com/lsrcz/grisette/compare/v0.9.0.0...v0.10.0.0 [0.11.0.0]: https://github.com/lsrcz/grisette/compare/v0.10.0.0...v0.11.0.0 [0.12.0.0]: https://github.com/lsrcz/grisette/compare/v0.11.0.0...v0.12.0.0 +[0.13.0.0]: https://github.com/lsrcz/grisette/compare/v0.12.0.0...v0.13.0.0 [0.2.0.0]: https://github.com/lsrcz/grisette/compare/v0.1.0.0...v0.2.0.0 [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0 @@ -656,4 +657,3 @@ No user-facing changes. [0.7.0.0]: https://github.com/lsrcz/grisette/compare/v0.6.0.0...v0.7.0.0 [0.8.0.0]: https://github.com/lsrcz/grisette/compare/v0.7.0.0...v0.8.0.0 [0.9.0.0]: https://github.com/lsrcz/grisette/compare/v0.8.0.0...v0.9.0.0 -[unreleased]: https://github.com/lsrcz/grisette/compare/v0.12.0.0...HEAD diff --git a/README.md b/README.md index c588922d..efcc3a64 100644 --- a/README.md +++ b/README.md @@ -48,7 +48,7 @@ can add it to your project's `.cabal` file: ```cabal library ... - build-depends: grisette >= 0.12 < 0.13 + build-depends: grisette >= 0.13 < 0.14 ``` #### Using stack @@ -59,14 +59,14 @@ Note: Grisette on Stackage is currently outdated. Please make sure to use ```yaml extra-deps: - - grisette-0.12.0.0 + - grisette-0.13.0.0 ``` and in your `package.yaml` file: ```yaml dependencies: - - grisette >= 0.12 < 0.13 + - grisette >= 0.13 < 0.14 ``` #### Quick start template with `stack new` diff --git a/examples/grisette-examples.cabal b/examples/grisette-examples.cabal index 7488e8aa..bad6f13f 100644 --- a/examples/grisette-examples.cabal +++ b/examples/grisette-examples.cabal @@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.37.0. +-- This file has been generated from package.yaml by hpack version 0.38.0. -- -- see: https://github.com/sol/hpack name: grisette-examples -version: 0.12.0.0 +version: 0.13.0.0 synopsis: Examples for Grisette description: More examples are available in the [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials) of @@ -32,5 +32,7 @@ executable basic basic build-depends: base >=4.14 && <5 - , grisette ==0.12.* + , grisette ==0.13.* + , mtl + , text default-language: Haskell2010 diff --git a/examples/package.yaml b/examples/package.yaml index c6292a9c..658fb74c 100644 --- a/examples/package.yaml +++ b/examples/package.yaml @@ -1,5 +1,5 @@ name: grisette-examples -version: 0.12.0.0 +version: 0.13.0.0 synopsis: Examples for Grisette description: | More examples are available in the @@ -14,7 +14,9 @@ extra-source-files: - README.md dependencies: - base >= 4.14 && < 5 - - grisette >= 0.12 && < 0.13 + - grisette >= 0.13 && < 0.14 + - mtl + - text executables: basic: source-dirs: basic diff --git a/flake.lock b/flake.lock index 27c38590..2d4bc704 100644 --- a/flake.lock +++ b/flake.lock @@ -82,11 +82,11 @@ "treefmt-nix": "treefmt-nix" }, "locked": { - "lastModified": 1740925102, - "narHash": "sha256-tzlaVLYIMLRnGko5Nw2ZgXxpFfQFtcnVwy6qBP4g2fs=", + "lastModified": 1751528475, + "narHash": "sha256-wBJ1MFK6zMpj9eUfMrxw4OBeMq8rXNpSPQK1hngkOsE=", "owner": "lsrcz", "repo": "grisette-nix-build-env", - "rev": "b7f089e9f2a7d19e766b7a478d7b89005f44b56c", + "rev": "f7a5e9842f8c669105845c0b1832c1b659c97d7f", "type": "github" }, "original": { @@ -98,11 +98,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1740828860, - "narHash": "sha256-cjbHI+zUzK5CPsQZqMhE3npTyYFt9tJ3+ohcfaOF/WM=", + "lastModified": 1751271578, + "narHash": "sha256-P/SQmKDu06x8yv7i0s8bvnnuJYkxVGBWLWHaU+tt4YY=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "303bd8071377433a2d8f76e684ec773d70c5b642", + "rev": "3016b4b15d13f3089db8a41ef937b13a9e33a8df", "type": "github" }, "original": { @@ -130,11 +130,11 @@ }, "nixpkgs_3": { "locked": { - "lastModified": 1735554305, - "narHash": "sha256-zExSA1i/b+1NMRhGGLtNfFGXgLtgo+dcuzHzaWA6w3Q=", + "lastModified": 1747958103, + "narHash": "sha256-qmmFCrfBwSHoWw7cVK4Aj+fns+c54EBP8cGqp/yK410=", "owner": "nixos", "repo": "nixpkgs", - "rev": "0e82ab234249d8eee3e8c91437802b32c74bb3fd", + "rev": "fe51d34885f7b5e3e7b59572796e1bcb427eccb1", "type": "github" }, "original": { @@ -146,11 +146,11 @@ }, "nixpkgs_4": { "locked": { - "lastModified": 1749285348, - "narHash": "sha256-frdhQvPbmDYaScPFiCnfdh3B/Vh81Uuoo0w5TkWmmjU=", + "lastModified": 1751271578, + "narHash": "sha256-P/SQmKDu06x8yv7i0s8bvnnuJYkxVGBWLWHaU+tt4YY=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "3e3afe5174c561dee0df6f2c2b2236990146329f", + "rev": "3016b4b15d13f3089db8a41ef937b13a9e33a8df", "type": "github" }, "original": { @@ -167,11 +167,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1740915799, - "narHash": "sha256-JvQvtaphZNmeeV+IpHgNdiNePsIpHD5U/7QN5AeY44A=", + "lastModified": 1750779888, + "narHash": "sha256-wibppH3g/E2lxU43ZQHC5yA/7kIKLGxVEnsnVK1BtRg=", "owner": "cachix", "repo": "pre-commit-hooks.nix", - "rev": "42b1ba089d2034d910566bf6b40830af6b8ec732", + "rev": "16ec914f6fb6f599ce988427d9d94efddf25fe6d", "type": "github" }, "original": { @@ -222,11 +222,11 @@ "nixpkgs": "nixpkgs_3" }, "locked": { - "lastModified": 1739829690, - "narHash": "sha256-mL1szCeIsjh6Khn3nH2cYtwO5YXG6gBiTw1A30iGeDU=", + "lastModified": 1750931469, + "narHash": "sha256-0IEdQB1nS+uViQw4k3VGUXntjkDp7aAlqcxdewb/hAc=", "owner": "numtide", "repo": "treefmt-nix", - "rev": "3d0579f5cc93436052d94b73925b48973a104204", + "rev": "ac8e6f32e11e9c7f153823abc3ab007f2a65d3e1", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 479e47fc..64bf9a88 100644 --- a/flake.nix +++ b/flake.nix @@ -66,22 +66,22 @@ pname = "grisette"; extraOutputs = pkgs: haskellPackages: devShellWithVersion: { devShells = { - "9101" = devShellWithVersion { - ghcVersion = "9101"; + "9102" = devShellWithVersion { + ghcVersion = "9102"; config = { isDevelopmentEnvironment = true; bitwuzla = true; }; }; default = devShellWithVersion { - ghcVersion = "9101"; + ghcVersion = "9102"; config = { isDevelopmentEnvironment = true; bitwuzla = true; }; }; - "9121" = devShellWithVersion { - ghcVersion = "9121"; + "9122" = devShellWithVersion { + ghcVersion = "9122"; config = { isDevelopmentEnvironment = false; bitwuzla = true; diff --git a/grisette.cabal b/grisette.cabal index 0d064ec3..9cdb393b 100644 --- a/grisette.cabal +++ b/grisette.cabal @@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.37.0. +-- This file has been generated from package.yaml by hpack version 0.38.0. -- -- see: https://github.com/sol/hpack name: grisette -version: 0.12.0.0 +version: 0.13.0.0 synopsis: Symbolic evaluation as a library description: Grisette is a reusable symbolic evaluation library for Haskell. By translating programs into constraints, Grisette can help the development of @@ -39,8 +39,8 @@ tested-with: , GHC == 9.4.8 , GHC == 9.6.6 , GHC == 9.8.4 - , GHC == 9.10.1 - , GHC == 9.12.1 + , GHC == 9.10.2 + , GHC == 9.12.2 extra-source-files: CHANGELOG.md README.md @@ -310,7 +310,7 @@ library src ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags build-depends: - QuickCheck >=2.14 && <2.16 + QuickCheck >=2.14 && <2.17 , array >=0.5.4 && <0.6 , async >=2.2.2 && <2.3 , atomic-primops >=0.8.3 && <0.9 @@ -357,7 +357,7 @@ test-suite doctest doctest ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags -threaded -rtsopts -with-rtsopts=-N build-depends: - QuickCheck >=2.14 && <2.16 + QuickCheck >=2.14 && <2.17 , array >=0.5.4 && <0.6 , async >=2.2.2 && <2.3 , atomic-primops >=0.8.3 && <0.9 @@ -479,7 +479,7 @@ test-suite spec ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags -threaded -rtsopts -with-rtsopts=-N -Wredundant-constraints build-depends: HUnit ==1.6.* - , QuickCheck >=2.14 && <2.16 + , QuickCheck >=2.14 && <2.17 , array >=0.5.4 && <0.6 , async >=2.2.2 && <2.3 , atomic-primops >=0.8.3 && <0.9 diff --git a/hie.yaml b/hie.yaml index 50afa8ba..dce4d3ef 100644 --- a/hie.yaml +++ b/hie.yaml @@ -10,7 +10,3 @@ cradle: component: "grisette-examples:exe:basic" - path: "examples/basic/Paths_grisette_examples.hs" component: "grisette-examples:exe:basic" - - path: "examples/exception/Main.hs" - component: "grisette-examples:exe:exception" - - path: "examples/exception/Paths_grisette_examples.hs" - component: "grisette-examples:exe:exception" diff --git a/package.yaml b/package.yaml index 8aeeb997..4df6d974 100644 --- a/package.yaml +++ b/package.yaml @@ -1,5 +1,5 @@ name: grisette -version: 0.12.0.0 +version: 0.13.0.0 synopsis: Symbolic evaluation as a library description: "Grisette is a reusable symbolic evaluation library for Haskell. By\ntranslating programs into constraints, Grisette can help the development of\nprogram reasoning tools, including verification, synthesis, and more.\n.\nThe \"Grisette\" module exports all the core APIs for building a symbolic\nevaluation tool. A high-level overview of the module structures are available\nthere.\n.\nA detailed introduction to Grisette is available at \"Grisette.Core\". More\nlifted libraries are provided in @Grisette.Lib.*@ modules.\n.\nThe \"Grisette.Unified\" module offers an experimental unified interface for\nsymbolic and concrete evaluation. This module should be imported qualified.\n.\nFor more details, please checkout the README and \n[tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials).\n" category: Formal Methods, Theorem Provers, Symbolic Computation, SMT @@ -19,8 +19,8 @@ tested-with: - GHC == 9.4.8 - GHC == 9.6.6 - GHC == 9.8.4 - - GHC == 9.10.1 - - GHC == 9.12.1 + - GHC == 9.10.2 + - GHC == 9.12.2 dependencies: - base >= 4.14 && < 5 - hashable >= 1.3 && < 1.6 @@ -39,7 +39,7 @@ dependencies: - sbv >= 8.17 && < 12 - parallel >= 3.2.2 && < 3.3 - text >= 1.2.4.1 && < 2.2 - - QuickCheck >= 2.14 && < 2.16 + - QuickCheck >= 2.14 && < 2.17 - prettyprinter >= 1.5.0 && < 1.8 - async >= 2.2.2 && < 2.3 - stm >= 2.5 && < 2.6 diff --git a/src/Grisette/Internal/SymPrim/SomeBV.hs b/src/Grisette/Internal/SymPrim/SomeBV.hs index 1bbee974..e97d8a55 100644 --- a/src/Grisette/Internal/SymPrim/SomeBV.hs +++ b/src/Grisette/Internal/SymPrim/SomeBV.hs @@ -234,7 +234,7 @@ import Unsafe.Coerce (unsafeCoerce) -- | An exception that would be thrown when operations are performed on -- incompatible bit widths. data SomeBVException = BitwidthMismatch | UndeterminedBitwidth T.Text - deriving (Show, Eq, Ord, Generic) + deriving (Eq, Ord, Generic) deriving anyclass (Hashable, NFData) deriving ( Mergeable, @@ -249,11 +249,14 @@ data SomeBVException = BitwidthMismatch | UndeterminedBitwidth T.Text ) via (Default (SomeBVException)) -instance Exception SomeBVException where - displayException BitwidthMismatch = "Bit width does not match" - displayException (UndeterminedBitwidth msg) = +instance Show SomeBVException where + show BitwidthMismatch = "Bit width does not match" + show (UndeterminedBitwidth msg) = "Cannot determine bit-width for literals: " <> T.unpack msg +instance Exception SomeBVException where + displayException = show + class MaySomeBV bv where assignLitBitWidth :: (KnownNat n, 1 <= n) => SomeBVLit -> bv n @@ -359,7 +362,8 @@ instance -- >>> bv 4 0x3 + bv 4 0x3 :: SomeBV IntN -- 0x6 -- >>> bv 4 0x3 + bv 8 0x3 :: SomeBV IntN --- *** Exception: BitwidthMismatch +-- *** Exception: Bit width does not match +-- ... -- -- One exception is that the equality testing (both concrete and symbolic via -- 'SymEq') does not require the bitwidths to be the same. Different bitwidths @@ -382,7 +386,8 @@ instance -- >>> 3 * bv 4 0x1 :: SomeBV IntN -- 0x3 -- >>> 3 * 3 :: SomeBV IntN --- *** Exception: UndeterminedBitwidth "(*)" +-- *** Exception: Cannot determine bit-width for literals: (*) +-- ... -- -- Some operations allows the literals to be used without the bit-width, such as -- '(+)', '(-)', 'negate', 'toUnsigned', 'toSigned', '.&.', '.|.', 'xor', diff --git a/stack-9.10.yaml b/stack-9.10.yaml index 8ce3bf02..27081471 100644 --- a/stack-9.10.yaml +++ b/stack-9.10.yaml @@ -16,7 +16,7 @@ # # resolver: ./custom-snapshot.yaml # resolver: https://example.com/snapshots/2018-01-01.yaml -resolver: nightly-2025-05-05 +resolver: nightly-2025-07-03 # User packages to be built. # Various formats can be used as shown in the example below. # diff --git a/stack-9.10.yaml.lock b/stack-9.10.yaml.lock index 717f87d9..59a41518 100644 --- a/stack-9.10.yaml.lock +++ b/stack-9.10.yaml.lock @@ -1,12 +1,12 @@ # This file was autogenerated by Stack. # You should not edit this file by hand. # For more information, please see the documentation at: -# https://docs.haskellstack.org/en/stable/lock_files +# https://docs.haskellstack.org/en/stable/topics/lock_files packages: [] snapshots: - completed: - sha256: 5c7ae8619fe0a6b36ab11931ec13248f9731722d32da7f1baae982277e086d05 - size: 681591 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/4/12.yaml - original: nightly-2025-04-12 + sha256: 1e879c64480ca43c6b796e6d48f64fa07072cbed80c1b802b48db3265510df50 + size: 722394 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/3.yaml + original: nightly-2025-07-03 diff --git a/stack.yaml.lock b/stack.yaml.lock index 13acc6fb..59a41518 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -6,7 +6,7 @@ packages: [] snapshots: - completed: - sha256: bcbc80a081dbf9d701bb8c46f0212b251acbe6cf64332e6e3c8b108c13794841 - size: 685947 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/5/5.yaml - original: nightly-2025-05-05 + sha256: 1e879c64480ca43c6b796e6d48f64fa07072cbed80c1b802b48db3265510df50 + size: 722394 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/3.yaml + original: nightly-2025-07-03