diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -59,14 +59,14 @@ ```yaml extra-deps: - - grisette-0.13.0.0 + - grisette-0.13.0.1 ``` and in your `package.yaml` file: ```yaml dependencies: - - grisette >= 0.13 < 0.14 + - grisette >= 0.13.0.1 < 0.14 ``` #### Quick start template with `stack new` diff --git a/grisette.cabal b/grisette.cabal --- 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 @@ , 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 @@ , 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 @@ , 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/src/Grisette/Internal/SymPrim/FP.hs b/src/Grisette/Internal/SymPrim/FP.hs --- a/src/Grisette/Internal/SymPrim/FP.hs +++ b/src/Grisette/Internal/SymPrim/FP.hs @@ -219,6 +219,7 @@ <> " 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 :: @@ -229,6 +230,27 @@ 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 :: + 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 61 == 'EQ) || (CmpNat eb 61 == 'LT)) && ( ((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT)) && ( (CmpNat sb 4611686018427387902 == 'EQ) @@ -239,6 +261,7 @@ ) of Refl -> r else error invalidFPMessage +#endif -- | IEEE 754 floating-point number with @eb@ exponent bits and @sb@ significand -- bits.