diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,13 @@ * Hackage: * GitHub: -* Latest Hackage released version: 0.6, 2015-01-01 +* Latest Hackage released version: 0.7, 2015-06-06 +### Version 0.7, 2016-06-06 + + * Compile with GHC-8.0. Plugin at least requires GHC-8.0.1 and SBV 5.12 + * Fix a few dead links + ### Version 0.6, 2016-01-01 * Support for list expressions of the form [x .. y] and @@ -30,8 +35,8 @@ ### Version 0.3, 2015-12-21 * Added the micro-controller example, adapted from - the original SBV variant by Anthony Cowley - (http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf) + the original SBV variant by Anthony Cowley: + * Add the "skip" option for the plugin itself. Handy when compiling the plugin itself! diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs --- a/Data/SBV/Plugin/Analyze.hs +++ b/Data/SBV/Plugin/Analyze.hs @@ -9,6 +9,7 @@ -- Walk the GHC Core, proving theorems/checking safety as they are found ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE NamedFieldPuns #-} module Data.SBV.Plugin.Analyze (analyzeBind) where @@ -21,7 +22,7 @@ import Data.IORef import Data.Char (isAlpha, isAlphaNum, toLower, isUpper) -import Data.List (intercalate, partition, nub, sort, sortBy, isPrefixOf) +import Data.List (intercalate, partition, nub, nubBy, sort, sortBy, isPrefixOf) import Data.Maybe (listToMaybe, fromMaybe) import Data.Ord (comparing) @@ -101,7 +102,9 @@ print sres -- If proof failed and there are uninterpreted non-input values, print a warning; except for "uninteresting" types - let unintVals = filter ((`notElem` uninteresting cfgEnv) . snd) $ nub $ sortBy (comparing fst) [vt | (vt, (False, _, _)) <- finalUninterps] + 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] unless (success || null unintVals) $ do let plu | length finalUninterps > 1 = "s:" | True = ":" @@ -125,7 +128,12 @@ let marker = "[SBV] " ++ showSpan flags (pickSpan curLoc) tag s = marker ++ " " ++ s tab s = replicate (length marker) ' ' ++ " " ++ s - error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es + msg = concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es +#if MIN_VERSION_base(4,9,0) + errorWithoutStackTrace msg +#else + error msg +#endif res initEnv topLoc = do v <- runReaderT (symEval topExpr) initEnv { curLoc = [topLoc] @@ -331,7 +339,7 @@ -- Case expressions. We take advantage of the core-invariant that each case alternative -- is exhaustive; and DEFAULT (if present) is the first alternative. We turn it into a -- simple if-then-else chain with the last element on the DEFAULT, or whatever comes last. - tgo _ e@(Case ce caseBinder caseType alts) + tgo _ e@(Case ce cBinder caseType alts) = do sce <- go ce let caseTooComplicated w [] = tbd ("Unsupported case-expression (" ++ w ++ ")") [sh e] caseTooComplicated w xs = tbd ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs @@ -346,7 +354,7 @@ (Tick t _, _ ) -> tickSpan t (Var v, _ ) -> varSpan v (_, b:_) -> varSpan b - _ -> varSpan caseBinder + _ -> varSpan cBinder mr <- match eLoc sce p bs case mr of Just (m, bs') -> do let result = local (\env -> env{curLoc = eLoc : curLoc env, envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs @@ -355,8 +363,8 @@ else choose (caseTooComplicated "with-complicated-alternatives-during-merging") m result (walk rest) Nothing -> caseTooComplicated "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs] - k <- getType (getSrcSpan caseBinder) caseType - local (\env -> env{envMap = M.insert (caseBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs) + k <- getType (getSrcSpan cBinder) caseType + local (\env -> env{envMap = M.insert (cBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs) where choose bailOut t tb fb = case S.svAsBool t of Nothing -> do stb <- tb @@ -468,18 +476,18 @@ uninterpret isInput t var = do Env{rUninterpreted, flags} <- ask prevUninterpreted <- liftIO $ readIORef rUninterpreted - case (var, t) `lookup` prevUninterpreted of - Just (_, _, val) -> return val - Nothing -> do let (tvs, t') = splitForAllTys t - (args, res) = splitFunTys t' - sp = getSrcSpan var - argKs <- mapM (getType sp) args - resK <- getType sp res - nm <- mkValidName $ showSDoc flags (ppr var) - body <- walk argKs (nm, resK) [] - let fVal = wrap tvs body - liftIO $ modifyIORef rUninterpreted (((var, t), (isInput, nm, fVal)) :) - return fVal + case [r | ((v, t'), r) <- prevUninterpreted, var == v && t `eqType` t'] of + (_, _, val):_ -> return val + [] -> do let (tvs, t') = splitForAllTys t + (args, res) = splitFunTys t' + sp = getSrcSpan var + argKs <- mapM (getType sp) args + resK <- getType sp res + nm <- mkValidName $ showSDoc flags (ppr var) + body <- walk argKs (nm, resK) [] + let fVal = wrap tvs body + liftIO $ modifyIORef rUninterpreted (((var, t), (isInput, nm, fVal)) :) + return fVal where walk :: [SKind] -> (String, SKind) -> [Val] -> Eval Val walk [] (nm, k) args = do Env{mbListSize, bailOut} <- ask @@ -576,11 +584,11 @@ -- Check if we uninterpreted this before; if so, return it, otherwise create a new one unknown = do Env{flags, rUITypes} <- ask uiTypes <- liftIO $ readIORef rUITypes - case bt `lookup` uiTypes of - Just k -> return k - Nothing -> do nm <- mkValidName $ showSDoc flags (ppr bt) - let k = S.KUserSort nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp) - liftIO $ modifyIORef rUITypes ((bt, k) :) - return k + 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) + liftIO $ modifyIORef rUITypes ((bt, k) :) + return k {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} diff --git a/Data/SBV/Plugin/Env.hs b/Data/SBV/Plugin/Env.hs --- a/Data/SBV/Plugin/Env.hs +++ b/Data/SBV/Plugin/Env.hs @@ -17,7 +17,7 @@ import GhcPlugins import GHC.Prim -import GHC.Types +import GHC.Types hiding (Type, TyCon) import qualified Data.Map as M import qualified Language.Haskell.TH as TH diff --git a/INSTALL b/INSTALL --- a/INSTALL +++ b/INSTALL @@ -4,5 +4,5 @@ This will also install the SBV library if you do not already have it. You should also install an SMT solver, preferably the default solver -used by SBV; i.e., Z3 from Microsoft: http://github.com/Z3Prover/z3. +used by SBV; i.e., Z3 from Microsoft: . Please make sure that the "z3" executable is in your path. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,7 +1,9 @@ ## SBVPlugin: SBV Plugin for GHC -[![Hackage version](https://budueba.com/hackage/sbvPlugin)](https://hackage.haskell.org/package/sbvPlugin) - [![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)](http://travis-ci.org/LeventErkok/sbvPlugin) +[![Hackage version](http://budueba.com/hackage/sbvPlugin)] + (http://hackage.haskell.org/package/sbvPlugin) +[![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)] + (http://travis-ci.org/LeventErkok/sbvPlugin) ### Example diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -1,5 +1,5 @@ Name : sbvPlugin -Version : 0.6 +Version : 0.7 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 @@ -29,7 +29,7 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController , Data.SBV.Plugin.Examples.BitTricks - build-depends : base >= 4.8 && < 5, ghc, ghc-prim, containers, sbv >= 5.8, mtl, template-haskell + build-depends : base >= 4.9 && < 5, ghc, ghc-prim, containers, sbv >= 5.12, mtl, template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Data , Data.SBV.Plugin.Common