sbvPlugin 9.12.1 → 9.14.1

raw patch · 3 files changed

+12/−8 lines, 3 filesdep ~ghcdep ~sbv

Dependency ranges changed: ghc, sbv

Files

• CHANGES.md +4/−0
• Data/SBV/Plugin/Analyze.hs +2/−2
• sbvPlugin.cabal +6/−6

@@ -1,6 +1,10 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub:  <http://github.com/LeventErkok/sbvPlugin> +### Version 9.14.1, 2026-01-12+  * Changes required to compile with GHC 9.14.1+  * Bump up sbv dependence to >= 13.4+   ### Version 9.12.1, 2025-03-12   * Changes required to compile with GHC 9.12.1   * Add support for CVC5, DReal, OpenSMT, and Bitwuzla as backend solvers

@@ -599,7 +599,7 @@                     resK  <- getComposite res                     return $ wrap tvs $ foldr KFun resK argKs  where wrap ts f         = foldr (KFun . mkUninterpreted) f ts-       mkUninterpreted v = KBase $ S.KUserSort (show (occNameFS (occName (varName v)))) Nothing+       mkUninterpreted v = KBase $ S.KADT (show (occNameFS (occName (varName v)))) [] []         -- | Extract tuples, lists, or base kinds        getComposite :: Type -> Eval SKind@@ -630,7 +630,7 @@                             case [k | (bt', k) <- uiTypes, bt `eqType` bt'] of                               k:_ -> return k                               []  -> do nm <- mkValidName $ showSDoc flags (ppr bt)-                                        let k = S.KUserSort nm Nothing+                                        let k = S.KADT nm [] []                                         liftIO $ modifyIORef rUITypes ((bt, k) :)                                         return k 

@@ -1,6 +1,6 @@ Cabal-Version     : 2.2 Name              : sbvPlugin-Version           : 9.12.1+Version           : 9.14.1 Category          : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis          : Formally prove properties of Haskell programs using SBV/SMT Description       : GHC plugin for proving properties over Haskell functions using SMT solvers, based@@ -18,11 +18,11 @@ Build-Type        : Simple Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With       : GHC==9.12.1+Tested-With       : GHC==9.14.1  source-repository head     type:       git-    location:   git://github.com/LeventErkok/sbvPlugin.git+    location:   https://github.com/LeventErkok/sbvPlugin.git  Library   default-language: Haskell2010@@ -34,13 +34,13 @@                   , Data.SBV.Plugin.Examples.MergeSort                   , Data.SBV.Plugin.Examples.MicroController   build-depends   : base >= 4.19 && < 5-                  , sbv      >= 11.4-                  , ghc      >= 9.12.1+                  , sbv      >= 13.4+                  , ghc      >= 9.14.1                   , ghc-prim                   , containers                   , mtl                   , template-haskell-  Other-modules   : Data.SBV.Plugin.Analyze+  other-modules   : Data.SBV.Plugin.Analyze                   , Data.SBV.Plugin.Common                   , Data.SBV.Plugin.Env                   , Data.SBV.Plugin.Plugin