sbvPlugin 0.8 → 0.9
raw patch · 4 files changed
+17/−14 lines, 4 filesdep ~sbv
Dependency ranges changed: sbv
Files
- CHANGES.md +6/−1
- Data/SBV/Plugin/Analyze.hs +4/−4
- README.md +5/−7
- sbvPlugin.cabal +2/−2
CHANGES.md view
@@ -1,7 +1,12 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 0.8, 2017-01-12+* Latest Hackage released version: 0.9, 2017-07-19++### Version 0.9, 2017-07-19++ * Sync-up with recent modifications to SBV. No user visible changes.+ * Bump up sbv dependence to >= 7.0 ### Version 0.8, 2017-01-12
Data/SBV/Plugin/Analyze.hs view
@@ -88,7 +88,7 @@ topLoc = varSpan topBind loc = "[SBV] " ++ showSpan (flags cfgEnv) topLoc slvrTag = ", using " ++ tag ++ "."- where tag = case solverConfigs of+ where tag = case map (S.name . S.solver) solverConfigs of [] -> "no solvers" -- can't really happen [x] -> show x [x, y] -> show x ++ " and " ++ show y@@ -99,13 +99,13 @@ finalUninterps <- readIORef (rUninterpreted cfgEnv) return (finalResult, finalUninterps) case finalResult of- Right (solver, sres@(S.ThmResult smtRes)) -> do+ Right (solver, _, sres@(S.ThmResult smtRes)) -> do let success = case smtRes of S.Unsatisfiable{} -> True S.Satisfiable{} -> False S.Unknown{} -> False -- conservative S.ProofError{} -> False -- conservative- S.TimeOut{} -> False -- conservative+ S.SatExtField{} -> False -- conservative putStr $ "[" ++ show solver ++ "] " print sres @@ -450,7 +450,7 @@ Nothing -> "Kind: " ++ sh k Just t -> "Type: " ++ sh t - sym (KBase k) nm = do v <- lift $ S.svMkSymVar Nothing k nm+ sym (KBase k) nm = do v <- lift $ ask >>= 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]
README.md view
@@ -1,9 +1,7 @@ ## SBVPlugin: SBV Plugin for GHC -[]- (http://hackage.haskell.org/package/sbvPlugin)-[]- (http://travis-ci.org/LeventErkok/sbvPlugin)+[](http://hackage.haskell.org/package/sbvPlugin)+[](http://travis-ci.org/LeventErkok/sbvPlugin) ### Example @@ -54,9 +52,9 @@ test x y = x == y -- clearly not True! ``` -The above, for instance, tells the plugin to ignore failed commands (`IgnoreFailure`). This would be useful when you-have a failing theorem that you are still working on, to make sure GHC continues compilation instead of stopping at-that point.+The above, for instance, tells the plugin to ignore failed proofs (`IgnoreFailure`). This is useful when you+have a failing theorem that you are still working on, to make sure GHC continues compilation instead of stopping+compilation and erroring out at that point. ### Available options
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name : sbvPlugin-Version : 0.8+Version : 0.9 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@@ -30,7 +30,7 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController , Data.SBV.Plugin.Examples.BitTricks- build-depends : base >= 4.9 && < 5, ghc, ghc-prim, containers, sbv >= 5.14, mtl, template-haskell+ build-depends : base >= 4.9 && < 5, ghc, ghc-prim, containers, sbv >= 7.0, mtl, template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Common , Data.SBV.Plugin.Env