sbvPlugin 0.10 → 0.11
raw patch · 7 files changed
+64/−34 lines, 7 filesdep ~basedep ~ghcdep ~ghc-prim
Dependency ranges changed: base, ghc, ghc-prim, sbv
Files
- CHANGES.md +11/−4
- Data/SBV/Plugin.hs +7/−0
- Data/SBV/Plugin/Analyze.hs +18/−16
- Data/SBV/Plugin/Env.hs +18/−3
- Data/SBV/Plugin/Examples/MergeSort.hs +4/−4
- Data/SBV/Plugin/Plugin.hs +2/−3
- sbvPlugin.cabal +4/−4
CHANGES.md view
@@ -1,12 +1,19 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 0.9, 2017-07-19+* Latest Hackage released version: 0.11, 2019-01-14 -### Version 0.10, Not yet released+### Version 0.11, 2019-01-14 - * Changes required to compile with GHC 8.2.1.+ * Changes required to compile with GHC 8.6.3+ * Bump up sbv dependence to >= 8.0+ * Clean-up/improve test cases +### Version 0.10, 2017-07-29++ * Changes required to compile with GHC 8.2.1/8.2.2.+ * Bump up sbv dependence to >= 7.4+ ### Version 0.9, 2017-07-19 * Sync-up with recent modifications to SBV. No user visible changes.@@ -18,7 +25,7 @@ * Add the 'Proved' type, which allows for easily tagging a type for proof, without the need for an explicit annotation. Thanks to Nickolas Fotopoulos for the patch.- * Bump up sbv dependence to >5.14+ * Bump up sbv dependence to > 5.14 ### Version 0.7, 2016-06-06
Data/SBV/Plugin.hs view
@@ -69,7 +69,14 @@ , SBVOption(..) -- * The 'Proved' type , Proved+ -- * The splittable class+ , Splittable(..) ) where import Data.SBV.Plugin.Plugin import Data.SBV.Plugin.Data++-- TODO: Unfortunately we need to export the Splittable class directly+-- from the plugin, due to issues arising from https://ghc.haskell.org/trac/ghc/ticket/16104+-- Hopefully this is temporary and this export can be removed later.+import Data.SBV (Splittable(..))
Data/SBV/Plugin/Analyze.hs view
@@ -23,13 +23,12 @@ import Data.IORef import Data.Char (isAlpha, isAlphaNum, toLower, isUpper)-import Data.List (intercalate, partition, nub, nubBy, sort, sortBy, isPrefixOf)+import Data.List (intercalate, partition, nub, nubBy, sort, sortOn, isPrefixOf) import Data.Maybe (listToMaybe, fromMaybe)-import Data.Ord (comparing) import qualified Data.Map as M -import qualified Data.SBV as S hiding (proveWith, proveWithAny)+import qualified Data.SBV as S hiding (proveWithAny) import qualified Data.SBV.Dynamic as S import qualified Data.SBV.Internals as S @@ -112,7 +111,7 @@ -- If proof failed and there are uninterpreted non-input values, print a warning; except for "uninteresting" types let ok t = not . any (eqType t) eq (a, b) (c, d) = a == c && b `eqType` d- unintVals = filter ((`ok` uninteresting cfgEnv) . snd) $ nubBy eq $ sortBy (comparing fst) [vt | (vt, (False, _, _)) <- finalUninterps]+ unintVals = filter ((`ok` uninteresting cfgEnv) . snd) $ nubBy eq $ sortOn fst [vt | (vt, (False, _, _)) <- finalUninterps] unless (success || null unintVals) $ do let plu | length finalUninterps > 1 = "s:" | True = ":"@@ -232,16 +231,19 @@ MachStr{} -> unint MachNullAddr -> unint MachLabel{} -> unint- MachInt i -> return $ Base $ S.svInteger (S.KBounded True machWordSize) i- MachInt64 i -> return $ Base $ S.svInteger (S.KBounded True 64 ) i- MachWord i -> return $ Base $ S.svInteger (S.KBounded False machWordSize) i- MachWord64 i -> return $ Base $ S.svInteger (S.KBounded False 64 ) i MachFloat f -> return $ Base $ S.svFloat (fromRational f) MachDouble d -> return $ Base $ S.svDouble (fromRational d)- LitInteger i it -> do k <- getType noSrcSpan it- case k of- KBase b -> return $ Base $ S.svInteger b i- _ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k)+ LitNumber lt i it -> do k <- getType noSrcSpan it+ case lt of+ LitNumInteger -> case k of+ KBase b -> return $ Base $ S.svInteger b i+ _ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k)+ LitNumNatural -> unint+ LitNumInt -> return $ Base $ S.svInteger (S.KBounded True machWordSize) i+ LitNumInt64 -> return $ Base $ S.svInteger (S.KBounded True 64 ) i+ LitNumWord -> return $ Base $ S.svInteger (S.KBounded False machWordSize) i+ LitNumWord64 -> return $ Base $ S.svInteger (S.KBounded False 64 ) i+ where unint = do Env{flags} <- ask k <- getType noSrcSpan t nm <- mkValidName (showSDoc flags (ppr e))@@ -450,7 +452,7 @@ Nothing -> "Kind: " ++ sh k Just t -> "Type: " ++ sh t - sym (KBase k) nm = do v <- lift $ ask >>= liftIO . S.svMkSymVar Nothing k nm+ sym (KBase k) nm = do v <- lift $ S.symbolicEnv >>= liftIO . S.svMkSymVar Nothing k nm return (Base v) sym (KTup ks) nm = do let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. length ks]@@ -561,8 +563,8 @@ argKs <- mapM (getType sp) args resK <- getComposite res return $ wrap tvs $ foldr KFun resK argKs- where wrap ts f = foldr (KFun . mkUserSort) f ts- mkUserSort v = KBase (S.KUserSort (show (occNameFS (occName (varName v)))) (Left "sbvPlugin"))+ where wrap ts f = foldr (KFun . mkUninterpreted) f ts+ mkUninterpreted v = KBase (S.KUninterpreted (show (occNameFS (occName (varName v)))) (Left "sbvPlugin")) -- | Extract tuples, lists, or base kinds getComposite :: Type -> Eval SKind@@ -595,7 +597,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 $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp)+ let k = S.KUninterpreted nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp) liftIO $ modifyIORef rUITypes ((bt, k) :) return k
Data/SBV/Plugin/Env.hs view
@@ -19,6 +19,9 @@ import GHC.Prim import GHC.Types hiding (Type, TyCon) +import Finder+import IfaceEnv+ import qualified Data.Map as M import qualified Language.Haskell.TH as TH @@ -30,8 +33,8 @@ import Data.Maybe (fromMaybe, isJust) import Data.Ratio -import qualified Data.SBV as S hiding (proveWith, proveWithAny)-import qualified Data.SBV.Dynamic as S+import qualified Data.SBV as S+import qualified Data.SBV.Dynamic as S import Data.SBV.Plugin.Common @@ -373,8 +376,20 @@ thToGHC (n, k, sfn) = do f <- grabTH lookupId n return ((f, k), sfn) +-- TODO: Starting with GHC 8.6, we no longer get the names available unless the+-- user code explicitly imports them. See: https://ghc.haskell.org/trac/ghc/ticket/16104+-- I was able to get the workaround it as in below, but it seems really fragile and+-- it also requires me to export the splittable class from the plugin. Surely there+-- must be a better way. grabTH :: (Name -> CoreM b) -> TH.Name -> CoreM b grabTH f n = do mbN <- thNameToGhcName n case mbN of Just gn -> f gn- Nothing -> error $ "[SBV] Impossible happened, while trying to locate GHC name for: " ++ show n+ Nothing -> f =<< lookInModule (TH.nameModule n) (TH.nameBase n)+ where lookInModule Nothing _ = error $ "[SBV] Impossible happened, while trying to locate GHC name for: " ++ show n+ lookInModule (Just inModule) bn = do+ env <- getHscEnv+ liftIO $ do r <- findImportedModule env (mkModuleName inModule) Nothing+ case r of+ Found _ mdl -> lookupOrigIO env mdl (mkVarOcc bn)+ _ -> error $ "[SBV] Impossible happened, can't find " ++ show bn ++ " in module " ++ show inModule
Data/SBV/Plugin/Examples/MergeSort.hs view
@@ -38,10 +38,10 @@ mergeSort [] = [] mergeSort [x] = [x] mergeSort xs = merge (mergeSort th) (mergeSort bh)- where (th, bh) = split xs ([], [])- split :: [a] -> ([a], [a]) -> ([a], [a])- split [] sofar = sofar- split (a:as) (fs, ss) = split as (ss, a:fs)+ where (th, bh) = halve xs ([], [])+ halve :: [a] -> ([a], [a]) -> ([a], [a])+ halve [] sofar = sofar+ halve (a:as) (fs, ss) = halve as (ss, a:fs) ----------------------------------------------------------------------------- -- * Proving correctness of sorting
Data/SBV/Plugin/Plugin.hs view
@@ -17,8 +17,7 @@ import System.Exit import Data.Maybe (fromJust)-import Data.List (sortBy)-import Data.Ord (comparing)+import Data.List (sortOn) import Data.Bits (bitSizeMaybe) import Data.IORef@@ -87,6 +86,6 @@ bindLoc (Rec []) = noSrcSpan bindLoc (Rec ((b, _):_)) = varSpan b - mapM_ (analyzeBind cfg) $ sortBy (comparing bindLoc) mg_binds+ mapM_ (analyzeBind cfg) $ sortOn bindLoc mg_binds return guts
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name : sbvPlugin-Version : 0.10+Version : 0.11 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@@ -15,7 +15,7 @@ Bug-reports : http://github.com/LeventErkok/sbvPlugin/issues Maintainer : Levent Erkok (erkokl@gmail.com) Build-Type : Simple-Cabal-Version : >= 1.14+Cabal-Version : 1.14 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md source-repository head@@ -30,7 +30,7 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController , Data.SBV.Plugin.Examples.BitTricks- build-depends : base >= 4.10 && < 5, ghc >= 8.2.1, ghc-prim >= 0.5.1, containers, sbv >= 7.0, mtl, template-haskell+ build-depends : base >= 4.12 && < 5, ghc >= 8.6.1, ghc-prim >= 0.5.3, containers, sbv >= 8.0, mtl, template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Common , Data.SBV.Plugin.Env@@ -41,6 +41,6 @@ type : exitcode-stdio-1.0 default-language: Haskell2010 ghc-options : -Wall- Build-depends : base >= 4.10 && < 5, sbvPlugin, tasty, tasty-golden, filepath, process, directory+ Build-depends : base >= 4.12 && < 5, sbvPlugin, tasty, tasty-golden, filepath, process, directory Hs-Source-Dirs : tests main-is : Run.hs