sbvPlugin 9.6.1 → 9.8.1
raw patch · 5 files changed
+32/−17 lines, 5 filesdep ~basedep ~ghcdep ~sbvPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, ghc, sbv
API changes (from Hackage documentation)
- Data.SBV.Plugin.Examples.BitTricks: elem :: Eq a => a -> [a] -> Bool
+ Data.SBV.Plugin.Examples.BitTricks: elem :: Word32 -> [Word32] -> Bool
- Data.SBV.Plugin.Examples.MergeSort: isPermutationOf :: Eq a => [a] -> [a] -> Bool
+ Data.SBV.Plugin.Examples.MergeSort: isPermutationOf :: [Int] -> [Int] -> Bool
- Data.SBV.Plugin.Examples.MergeSort: merge :: Ord a => [a] -> [a] -> [a]
+ Data.SBV.Plugin.Examples.MergeSort: merge :: [Int] -> [Int] -> [Int]
- Data.SBV.Plugin.Examples.MergeSort: mergeSort :: Ord a => [a] -> [a]
+ Data.SBV.Plugin.Examples.MergeSort: mergeSort :: [Int] -> [Int]
- Data.SBV.Plugin.Examples.MergeSort: nonDecreasing :: Ord a => [a] -> Bool
+ Data.SBV.Plugin.Examples.MergeSort: nonDecreasing :: [Int] -> Bool
Files
- CHANGES.md +5/−1
- COPYRIGHT +1/−1
- Data/SBV/Plugin/Analyze.hs +17/−6
- LICENSE +1/−1
- sbvPlugin.cabal +8/−8
CHANGES.md view
@@ -1,7 +1,11 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 9.6.1, 2023-04-14+* Latest Hackage released version: 9.8.1, 2024-01-05++### Version 9.8.1, 2024-01-05+ * Changes required to compile with GHC 9.8.1+ * Bump up sbv dependence to >= 10.3 ### Version 9.6.1, 2023-04-14 * Changes required to compile with GHC 9.6.1
COPYRIGHT view
@@ -1,4 +1,4 @@-Copyright (c) 2015-2023, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2015-2024, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbvPlugin is distributed with the BSD3 license. See the LICENSE file
Data/SBV/Plugin/Analyze.hs view
@@ -265,7 +265,7 @@ k <- getType noSrcSpan t nm <- mkValidName (showSDoc flags (ppr e)) case k of- KBase b -> return $ Base $ S.svUninterpreted b nm S.UINone []+ KBase b -> return $ Base $ S.svUninterpreted b nm (S.UINone True) [] _ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k) tgo tFun orig@App{} = do@@ -533,7 +533,7 @@ bArgs = concatMap mkArg (reverse args) mkRes :: String -> SKind -> Eval [S.SVal]- mkRes n (KBase b) = return [S.svUninterpreted b n S.UINone bArgs]+ mkRes n (KBase b) = return [S.svUninterpreted b n (S.UINone True) bArgs] mkRes n (KTup bs) = concat `fmap` zipWithM mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ]] bs mkRes n (KLst b) = do ls <- case mbListSize of Just i -> return i@@ -564,21 +564,32 @@ liftIO $ modifyIORef rUsedNames (unm :) return $ escape unm where genSym bad nm- | nm `elem` bad = head [nm' | i <- [(0::Int) ..], let nm' = nm ++ "_" ++ show i, nm' `notElem` bad]+ | nm `elem` bad = hd ("genSym: " ++ nm) [nm' | i <- [(0::Int) ..], let nm' = nm ++ "_" ++ show i, nm' `notElem` bad] | True = nm+ unSMT nm | map toLower nm `elem` S.smtLibReservedNames- = if not (null nm) && isUpper (head nm)+ = if not (null nm) && isUpper (hd "unSMT" nm) then "sbv" ++ nm else "sbv_" ++ nm | True = nm- escape nm | isAlpha (head nm) && all isGood (tail nm) = nm- | True = "|" ++ map tr nm ++ "|"++ escape nm | isAlpha (hd "escape" nm) && all isGood (tl "escape" nm) = nm+ | True = "|" ++ map tr nm ++ "|"+ isGood c = isAlphaNum c || c == '_' tr '|' = '_' tr '\\' = '_' tr c = c++hd :: String -> [a] -> a+hd _ (x:_) = x+hd n [] = error $ "Impossible happened: hd received empty list while running " ++ show n++tl :: String -> [a] -> [a]+tl _ (_:xs) = xs+tl n [] = error $ "Impossible happened: hd received empty list while running " ++ show n -- | Convert a Core type to an SBV Type, retaining functions and tuples getType :: SrcSpan -> Type -> Eval SKind
LICENSE view
@@ -1,6 +1,6 @@ sbvPlugin: SMT based theorem prover for Haskell -Copyright (c) 2015-2023, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2015-2024, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without
sbvPlugin.cabal view
@@ -1,5 +1,6 @@+Cabal-Version : 2.2 Name : sbvPlugin-Version : 9.6.1+Version : 9.8.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@@ -7,7 +8,7 @@ . See "Data.SBV.Plugin" for a quick example, or the modules under 'Data.SBV.Plugin.Examples' for more details.-License : BSD3+License : BSD-3-Clause License-file : LICENSE Stability : Experimental Author : Levent Erkok@@ -15,10 +16,9 @@ Bug-reports : http://github.com/LeventErkok/sbvPlugin/issues Maintainer : Levent Erkok (erkokl@gmail.com) Build-Type : Simple-Cabal-Version : 1.14 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With : GHC==9.6.1+Tested-With : GHC==9.8.1 source-repository head type: git@@ -33,9 +33,9 @@ , Data.SBV.Plugin.Examples.Maximum , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController- build-depends : base >= 4.11 && < 5- , sbv >= 10.1- , ghc >= 9.6.1+ build-depends : base >= 4.19 && < 5+ , sbv >= 10.3+ , ghc >= 9.8.1 , ghc-prim , containers , mtl@@ -50,7 +50,7 @@ type : exitcode-stdio-1.0 default-language: Haskell2010 ghc-options : -Wall- Build-depends : base >= 4.11 && < 5+ Build-depends : base >= 4.19 && < 5 , sbvPlugin , tasty , tasty-golden