verifiable-expressions 0.6.1 → 0.6.2
raw patch · 3 files changed
+16/−11 lines, 3 filesdep ~lensdep ~sbvdep ~transformersPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: lens, sbv, transformers, union, vinyl
API changes (from Hackage documentation)
+ Language.Verification: [crackNum] :: SMTConfig -> Bool
- Language.Verification: SMTConfig :: Bool -> Timing -> Int -> Int -> String -> Maybe Int -> Bool -> Bool -> (Text -> Bool) -> Bool -> Bool -> Maybe FilePath -> SMTLibVersion -> Maybe Double -> SMTSolver -> [String] -> Bool -> RoundingMode -> [SMTOption] -> Bool -> Maybe FilePath -> SMTConfig
+ Language.Verification: SMTConfig :: Bool -> Timing -> Int -> Int -> Bool -> String -> Maybe Int -> Bool -> Bool -> (String -> Bool) -> Bool -> Bool -> Maybe FilePath -> SMTLibVersion -> Maybe Double -> SMTSolver -> [String] -> Bool -> RoundingMode -> [SMTOption] -> Bool -> Maybe FilePath -> SMTConfig
- Language.Verification: [isNonModelVar] :: SMTConfig -> Text -> Bool
+ Language.Verification: [isNonModelVar] :: SMTConfig -> String -> Bool
Files
- CHANGELOG.md +4/−1
- Language/Expression/Scope.hs +8/−4
- verifiable-expressions.cabal +4/−6
CHANGELOG.md view
@@ -1,3 +1,6 @@-## 0.6.1 (2021-03-03)+## 0.6.2 (16 Jun 2021)+* Support GHC 9.0++## 0.6.1 (03 Mar 2021) * Require at least Vinyl 0.9 (`RMap` etc. via type classes) * Support at least GHC 8.6, 8.8, 8.10
Language/Expression/Scope.hs view
@@ -45,8 +45,12 @@ -- instance (HFoldableAt k g) => HFoldableAt k (BV g) where -- hfoldMap = hbifoldMap . hfoldMap +-- Note that since GHC 9.0, a handful of these instances must be eta-expanded+-- manually due to simplified subsumption. So if you see an @f@ or @g@ that+-- looks like it could be omitted with a pointfree-er definition, that's likely+-- the reason. instance HTraversable (BV g) where- htraverse = hbitraverseBV pure+ htraverse f = hbitraverseBV pure f foldBV :: (w a -> r) -> (v a -> r) -> BV w v a -> r foldBV f g = \case@@ -54,10 +58,10 @@ F y -> g y instance HBifunctor BV where- hbimap = hbimapBV+ hbimap f g = hbimapBV f g instance HBitraversable BV where- hbitraverse = hbitraverseBV+ hbitraverse f g = hbitraverseBV f g hbitraverseBV :: (Functor t) => (g a -> t (g' b)) -> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b) hbitraverseBV f g = foldBV (fmap B . f) (fmap F . g)@@ -66,7 +70,7 @@ hbimapBV f g = foldBV (B . f) (F . g) instance HBifoldableAt k BV where- hbifoldMap = foldBV+ hbifoldMap f g = foldBV f g -------------------------------------------------------------------------------- -- Scopes
verifiable-expressions.cabal view
@@ -1,13 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.33.0.+-- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack------ hash: b61cc1fb115270326d22ec5fbcdd0a38b0aed4c1489d119b344cf4e41c987188 name: verifiable-expressions-version: 0.6.1+version: 0.6.2 synopsis: An intermediate language for Hoare logic style verification. description: A typed intermediate language for Hoare logic style verification. It defines the intermediate language and combinators to interact it. category: Language@@ -49,10 +47,10 @@ build-depends: base >=4.9 && <5 , containers >=0.5.7 && <0.7- , lens >=4.16.1 && <5+ , lens >=4.16.1 && <5.1 , mtl >=2.0 && <3 , sbv >=8.0 && <9- , transformers >=0.5 && <0.6+ , transformers ==0.5.* , union >=0.1.1 && <0.2 , vinyl >=0.9 && <0.14 default-language: Haskell2010