diff --git a/grisette.cabal b/grisette.cabal index 9cdb393b..5ce70c77 100644 --- a/grisette.cabal +++ b/grisette.cabal @@ -1,37 +1,37 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.38.0. +-- This file has been generated from package.yaml by hpack version 0.37.0. -- -- see: https://github.com/sol/hpack -name: grisette -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 - program reasoning tools, including verification, synthesis, and more. - . - The "Grisette" module exports all the core APIs for building a symbolic - evaluation tool. A high-level overview of the module structures are available - there. - . - A detailed introduction to Grisette is available at "Grisette.Core". More - lifted libraries are provided in @Grisette.Lib.*@ modules. - . - The "Grisette.Unified" module offers an experimental unified interface for - symbolic and concrete evaluation. This module should be imported qualified. - . - For more details, please checkout the README and - [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials). -category: Formal Methods, Theorem Provers, Symbolic Computation, SMT -homepage: https://github.com/lsrcz/grisette#readme -bug-reports: https://github.com/lsrcz/grisette/issues -author: Sirui Lu, Rastislav Bodík -maintainer: Sirui Lu (siruilu@cs.washington.edu) -copyright: 2021-2024 Sirui Lu -license: BSD3 -license-file: LICENSE -build-type: Simple +name: grisette +version: 0.13.0.1 +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 + program reasoning tools, including verification, synthesis, and more. + . + The "Grisette" module exports all the core APIs for building a symbolic + evaluation tool. A high-level overview of the module structures are available + there. + . + A detailed introduction to Grisette is available at "Grisette.Core". More + lifted libraries are provided in @Grisette.Lib.*@ modules. + . + The "Grisette.Unified" module offers an experimental unified interface for + symbolic and concrete evaluation. This module should be imported qualified. + . + For more details, please checkout the README and + [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials). +category: Formal Methods, Theorem Provers, Symbolic Computation, SMT +homepage: https://github.com/lsrcz/grisette#readme +bug-reports: https://github.com/lsrcz/grisette/issues +author: Sirui Lu, Rastislav Bodík +maintainer: Sirui Lu (siruilu@cs.washington.edu) +copyright: 2021-2024 Sirui Lu +license: BSD3 +license-file: LICENSE +build-type: Simple tested-with: GHC == 8.10.7 , GHC == 9.0.2 @@ -329,7 +329,7 @@ library , mtl >=2.2.2 && <2.4 , parallel >=3.2.2 && <3.3 , prettyprinter >=1.5.0 && <1.8 - , sbv >=8.17 && <12 + , sbv >=8.17 && <13 , stm ==2.5.* , template-haskell >=2.16 && <2.24 , text >=1.2.4.1 && <2.2 @@ -378,7 +378,7 @@ test-suite doctest , mtl >=2.2.2 && <2.4 , parallel >=3.2.2 && <3.3 , prettyprinter >=1.5.0 && <1.8 - , sbv >=8.17 && <12 + , sbv >=8.17 && <13 , stm ==2.5.* , template-haskell >=2.16 && <2.24 , text >=1.2.4.1 && <2.2 @@ -499,7 +499,7 @@ test-suite spec , mtl >=2.2.2 && <2.4 , parallel >=3.2.2 && <3.3 , prettyprinter >=1.5.0 && <1.8 - , sbv >=8.17 && <12 + , sbv >=8.17 && <13 , stm ==2.5.* , template-haskell >=2.16 && <2.24 , test-framework >=0.8.2 && <0.9 diff --git a/package.yaml b/package.yaml index 4df6d974..f3f65e63 100644 --- a/package.yaml +++ b/package.yaml @@ -1,5 +1,5 @@ name: grisette -version: 0.13.0.0 +version: 0.13.0.1 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 @@ -36,7 +36,7 @@ dependencies: - th-compat >= 0.1.2 && < 0.2 - th-abstraction >= 0.4 && < 0.8 - array >= 0.5.4 && < 0.6 - - sbv >= 8.17 && < 12 + - sbv >= 8.17 && < 13 - parallel >= 3.2.2 && < 3.3 - text >= 1.2.4.1 && < 2.2 - QuickCheck >= 2.14 && < 2.17 diff --git a/src/Grisette/Internal/SymPrim/FP.hs b/src/Grisette/Internal/SymPrim/FP.hs index 679c902d..30f003a5 100644 --- a/src/Grisette/Internal/SymPrim/FP.hs +++ b/src/Grisette/Internal/SymPrim/FP.hs @@ -219,6 +219,28 @@ invalidFPMessage = <> " sb `elem` [2 .. 4611686018427387902]\n\n" <> " Given type falls outside of this range, or the sizes are not known naturals." +#if MIN_VERSION_sbv(12,0,0) +-- | Provide an (unsafe) type-level proof that the given floating-point type is +-- valid. +withUnsafeValidFP :: + forall eb sb r. (KnownNat eb, KnownNat sb) => ((ValidFP eb sb) => r) -> r +withUnsafeValidFP r = + let eb = natVal (Proxy @eb) + sb = natVal (Proxy @sb) + in if checkDynamicValidFP eb sb + then case unsafeAxiom @True + @( ((CmpNat eb 2 == 'EQ) || (CmpNat eb 2 == 'GT)) + && ( ((CmpNat eb 29 == 'EQ) || (CmpNat eb 29 == 'LT)) + && ( ((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT)) + && ( (CmpNat sb 1073741822 == 'EQ) + || (CmpNat sb 1073741822 == 'LT) + ) + ) + ) + ) of + Refl -> r + else error invalidFPMessage +#else -- | Provide an (unsafe) type-level proof that the given floating-point type is -- valid. withUnsafeValidFP :: @@ -239,6 +261,7 @@ withUnsafeValidFP r = ) of Refl -> r else error invalidFPMessage +#endif -- | IEEE 754 floating-point number with @eb@ exponent bits and @sb@ significand -- bits. diff --git a/stack-9.10.yaml b/stack-9.10.yaml index 27081471..bb503c62 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-07-03 +resolver: nightly-2025-07-14 # 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 59a41518..a1b57cf9 100644 --- a/stack-9.10.yaml.lock +++ b/stack-9.10.yaml.lock @@ -6,7 +6,7 @@ packages: [] snapshots: - completed: - sha256: 1e879c64480ca43c6b796e6d48f64fa07072cbed80c1b802b48db3265510df50 - size: 722394 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/3.yaml - original: nightly-2025-07-03 + sha256: 7a26eba54b469fc72b1e37b881dfec480a2c1cb0636136f96aec7d81be6c762f + size: 724509 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/14.yaml + original: nightly-2025-07-14 diff --git a/stack-9.8.yaml b/stack-9.8.yaml index 6468cdbb..87f83630 100644 --- a/stack-9.8.yaml +++ b/stack-9.8.yaml @@ -16,7 +16,7 @@ # # resolver: ./custom-snapshot.yaml # resolver: https://example.com/snapshots/2018-01-01.yaml -resolver: lts-23.18 +resolver: lts-23.27 # User packages to be built. # Various formats can be used as shown in the example below. # diff --git a/stack-9.8.yaml.lock b/stack-9.8.yaml.lock index 2b897faa..67e8a10d 100644 --- a/stack-9.8.yaml.lock +++ b/stack-9.8.yaml.lock @@ -1,12 +1,19 @@ # 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: [] +packages: +- completed: + hackage: sbv-12.0@sha256:91e8297e444e43921d5a628408d5469894bbe3616c5236a6ebaae5e2a0650e8a,25606 + pantry-tree: + sha256: 8e0feaff1d152467ac4641c3a9e6b82ee5e3741121d41ca06f4a393ffcb52715 + size: 77084 + original: + hackage: sbv-12.0 snapshots: - completed: - sha256: d133abe75e408a407cce3f032c96ac1bbadf474a93b5156ebf4135b53382d56b - size: 683827 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/23/18.yaml - original: lts-23.18 + sha256: 069c8189232279d04bd107557d3a62132c04ae5ce3c710649e6b40f67f10b9d5 + size: 684285 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/23/27.yaml + original: lts-23.27 diff --git a/stack.yaml.lock b/stack.yaml.lock index 59a41518..a1b57cf9 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -6,7 +6,7 @@ packages: [] snapshots: - completed: - sha256: 1e879c64480ca43c6b796e6d48f64fa07072cbed80c1b802b48db3265510df50 - size: 722394 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/3.yaml - original: nightly-2025-07-03 + sha256: 7a26eba54b469fc72b1e37b881dfec480a2c1cb0636136f96aec7d81be6c762f + size: 724509 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/14.yaml + original: nightly-2025-07-14