diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,11 @@ * Hackage: * GitHub: -* Latest Hackage released version: 0.11, 2019-01-14 +* Latest Hackage released version: 0.12, 2019-09-05 + +### Version 0.12, 2020-09-05 + * Changes required to compile with GHC 8.10.2 + * Bump up sbv dependence to >= 8.8 ### Version 0.11, 2019-01-14 diff --git a/Data/SBV/Plugin.hs b/Data/SBV/Plugin.hs --- a/Data/SBV/Plugin.hs +++ b/Data/SBV/Plugin.hs @@ -69,14 +69,7 @@ , 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(..)) 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 @@ -227,12 +227,13 @@ tgo t e@(Lit l) = do Env{machWordSize} <- ask case l of - MachChar{} -> unint - MachStr{} -> unint - MachNullAddr -> unint - MachLabel{} -> unint - MachFloat f -> return $ Base $ S.svFloat (fromRational f) - MachDouble d -> return $ Base $ S.svDouble (fromRational d) + LitChar{} -> unint + LitString{} -> unint + LitNullAddr{} -> unint + LitRubbish{} -> unint + LitLabel{} -> unint + LitFloat f -> return $ Base $ S.svFloat (fromRational f) + LitDouble d -> return $ Base $ S.svDouble (fromRational d) LitNumber lt i it -> do k <- getType noSrcSpan it case lt of LitNumInteger -> case k of @@ -452,7 +453,7 @@ Nothing -> "Kind: " ++ sh k Just t -> "Type: " ++ sh t - sym (KBase k) nm = do v <- lift $ S.symbolicEnv >>= liftIO . S.svMkSymVar Nothing k nm + sym (KBase k) nm = do v <- lift $ S.symbolicEnv >>= liftIO . S.svMkSymVar (S.NonQueryVar Nothing) k nm return (Base v) sym (KTup ks) nm = do let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. length ks] @@ -564,7 +565,7 @@ resK <- getComposite res return $ wrap tvs $ foldr KFun resK argKs where wrap ts f = foldr (KFun . mkUninterpreted) f ts - mkUninterpreted v = KBase (S.KUninterpreted (show (occNameFS (occName (varName v)))) (Left "sbvPlugin")) + mkUninterpreted v = KBase $ S.KUserSort (show (occNameFS (occName (varName v)))) Nothing -- | Extract tuples, lists, or base kinds getComposite :: Type -> Eval SKind @@ -579,10 +580,8 @@ getBaseType bt = do Env{tcMap} <- ask case grabTCs (splitTyConApp_maybe bt) of - Just k -> case k `M.lookup` tcMap of - Just knd -> return knd - Nothing -> unknown - _ -> unknown + Just k -> maybe unknown return (k `M.lookup` tcMap) + _ -> unknown where -- allow one level of nesting, essentially to support Haskell's 'Ratio Integer' to map to 'SReal' grabTCs Nothing = Nothing grabTCs (Just (top, ts)) = do as <- walk ts [] @@ -597,7 +596,7 @@ case [k | (bt', k) <- uiTypes, bt `eqType` bt'] of k:_ -> return k [] -> do nm <- mkValidName $ showSDoc flags (ppr bt) - let k = S.KUninterpreted nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp) + let k = S.KUserSort nm Nothing liftIO $ modifyIORef rUITypes ((bt, k) :) return k diff --git a/Data/SBV/Plugin/Common.hs b/Data/SBV/Plugin/Common.hs --- a/Data/SBV/Plugin/Common.hs +++ b/Data/SBV/Plugin/Common.hs @@ -9,10 +9,8 @@ -- Common data-structures/utilities ----------------------------------------------------------------------------- -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -152,19 +150,19 @@ -- | Symbolic if-then-else over values. iteVal :: ([String] -> Eval Val) -> S.SVal -> Val -> Val -> Eval Val -iteVal bailOut t v1 v2 = k v1 v2 +iteVal die t v1 v2 = k v1 v2 where k (Base a) (Base b) = return $ Base $ S.svIte t a b k (Tup as) (Tup bs) | length as == length bs = Tup `fmap` zipWithM k as bs k (Lst as) (Lst bs) | length as == length bs = Lst `fmap` zipWithM k as bs - | True = bailOut [ "Alternatives are producing lists of differing sizes:" - , " Length " ++ show (length as) ++ ": " ++ showSDocUnsafe (ppr (Lst as)) - , "vs Length " ++ show (length bs) ++ ": " ++ showSDocUnsafe (ppr (Lst bs)) - ] + | True = die [ "Alternatives are producing lists of differing sizes:" + , " Length " ++ show (length as) ++ ": " ++ showSDocUnsafe (ppr (Lst as)) + , "vs Length " ++ show (length bs) ++ ": " ++ showSDocUnsafe (ppr (Lst bs)) + ] k (Func n1 f) (Func n2 g) = return $ Func (n1 `mplus` n2) $ \a -> f a >>= \fa -> g a >>= \ga -> k fa ga - k _ _ = bailOut [ "Unsupported if-then-else/case with alternatives:" - , " Value:" ++ showSDocUnsafe (ppr v1) - , " vs:" ++ showSDocUnsafe (ppr v2) - ] + k _ _ = die [ "Unsupported if-then-else/case with alternatives:" + , " Value:" ++ showSDocUnsafe (ppr v1) + , " vs:" ++ showSDocUnsafe (ppr v2) + ] -- | Compute the span given a Tick. Returns the old-span if the tick span useless. tickSpan :: Tickish t -> SrcSpan @@ -186,7 +184,7 @@ -- | Show a GHC span in user-friendly form showSpan :: DynFlags -> SrcSpan -> String -showSpan flags s = showSDoc flags (ppr s) +showSpan fs s = showSDoc fs (ppr s) -- | This comes mighty handy! Wonder why GHC doesn't have it already: instance Show CoreExpr where 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 @@ -113,12 +113,6 @@ ++ [ (op, tlift2 (KBase k), lift2 sOp) | k <- bvKinds, (op, sOp) <- bvBinOps ] ++ [ (op, tlift2ShRot wsz (KBase k), lift2 sOp) | k <- bvKinds, (op, sOp) <- bvShiftRots] - -- bv-splits - ++ [('S.split, tSplit s, liftSplit s) | s <- [16, 32, 64]] - - -- bv-joins - ++ [ ('(S.#), tJoin s, lift2 S.svJoin) | s <- [8, 16, 32]] - -- constructing "fixed-size" lists ++ [ ('enumFromTo, tEnumFromTo (KBase k), sEnumFromTo) | k <- arithKinds ] ++ [ ('enumFromThenTo, tEnumFromThenTo (KBase k), sEnumFromThenTo) | k <- arithKinds ] @@ -278,18 +272,6 @@ tlift2ShRot :: Int -> SKind -> SKind tlift2ShRot wsz k = KFun k (KFun (KBase (S.KBounded True wsz)) k) --- | Construct the type for a split operation -tSplit :: Int -> SKind -tSplit n = KFun a (KTup [r, r]) - where a = KBase (S.KBounded False n) - r = KBase (S.KBounded False (n `div` 2)) - --- | Construct the type for a join operation -tJoin :: Int -> SKind -tJoin n = KFun a (KFun a r) - where a = KBase (S.KBounded False n) - r = KBase (S.KBounded False (n*2)) - -- | Type of enumFromTo: [x .. y] tEnumFromTo :: SKind -> SKind tEnumFromTo a = KFun a (KFun a (KLst a)) @@ -321,16 +303,6 @@ h v = error $ "Impossible happened: lift2 received non-base argument (h): " ++ showSDocUnsafe (ppr v) k a (Base b) = return $ Base $ f a b k _ v = error $ "Impossible happened: lift2 received non-base argument (k): " ++ showSDocUnsafe (ppr v) - --- | Lifting splits -liftSplit :: Int -> Val -liftSplit n = Func Nothing g - where g (Typ _) = return $ Func Nothing g - g (Base a) = do let half = n `div` 2 - f = Base $ S.svExtract (n-1) half a - s = Base $ S.svExtract (half-1) 0 a - return $ Tup [f, s] - g v = error $ "Impossible happened: liftSplit received unexpected argument: " ++ showSDocUnsafe (ppr (n, v)) -- | Lifting an equality is special; since it acts uniformly over tuples. liftEq :: (S.SVal -> S.SVal -> S.SVal) -> Val diff --git a/Data/SBV/Plugin/Examples/MergeSort.hs b/Data/SBV/Plugin/Examples/MergeSort.hs --- a/Data/SBV/Plugin/Examples/MergeSort.hs +++ b/Data/SBV/Plugin/Examples/MergeSort.hs @@ -87,7 +87,7 @@ -- | Asserting correctness of merge-sort for a list of the given size. Note that we can -- only check correctness for fixed-size lists. Also, the proof will get more and more --- complicated for the backend SMT solver as 'n' increases. Here we try it with 4. +-- complicated for the backend SMT solver as @n@ increases. Here we try it with 4. -- -- We have: -- diff --git a/Data/SBV/Plugin/Examples/MicroController.hs b/Data/SBV/Plugin/Examples/MicroController.hs --- a/Data/SBV/Plugin/Examples/MicroController.hs +++ b/Data/SBV/Plugin/Examples/MicroController.hs @@ -33,7 +33,7 @@ -- * The specification ----------------------------------------------------------------------------- --- | Given a last-signal-time calculator, named 'calculate', check that it satisfies the following +-- | Given a last-signal-time calculator, named @calculate@, check that it satisfies the following -- three requirements: We must've just sent a signal if: -- -- * /minRate/: The last-time we sent is strictly less than the 'maxTimeSince' amount @@ -78,7 +78,7 @@ -- @ -- -- We're being told that if the range is 200, and manual override is off, and time-since last is 9, --- then our "calculator" returns 10. But that violates the 'minRate' requirement, since we +-- then our "calculator" returns 10. But that violates the @minRate@ requirement, since we -- never want to go 'maxTimeSince' cycles without sending a signal! {-# ANN checkBad theorem {options = [IgnoreFailure]} #-} checkBad :: Int -> Bool -> Int -> Bool diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,7 @@ ## SBVPlugin: SBV Plugin for GHC -[![Hackage version](http://img.shields.io/hackage/v/sbvPlugin.svg?label=Hackage)](http://hackage.haskell.org/package/sbvPlugin) +On Hackage: 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.11 +Version : 0.12 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,6 +18,8 @@ Cabal-Version : 1.14 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md +Tested-With : GHC==8.10.2 + source-repository head type: git location: git://github.com/LeventErkok/sbvPlugin.git @@ -30,7 +32,13 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController , Data.SBV.Plugin.Examples.BitTricks - build-depends : base >= 4.12 && < 5, ghc >= 8.6.1, ghc-prim >= 0.5.3, containers, sbv >= 8.0, mtl, template-haskell + build-depends : base >= 4.11 && < 5 + , ghc + , ghc-prim + , containers + , sbv >= 8.8 + , mtl + , template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Common , Data.SBV.Plugin.Env @@ -41,6 +49,12 @@ type : exitcode-stdio-1.0 default-language: Haskell2010 ghc-options : -Wall - Build-depends : base >= 4.12 && < 5, sbvPlugin, tasty, tasty-golden, filepath, process, directory + Build-depends : base >= 4.11 && < 5 + , sbvPlugin + , tasty + , tasty-golden + , filepath + , process + , directory Hs-Source-Dirs : tests main-is : Run.hs