diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,12 +1,19 @@ * Hackage: * GitHub: -* 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 diff --git a/Data/SBV/Plugin.hs b/Data/SBV/Plugin.hs --- a/Data/SBV/Plugin.hs +++ b/Data/SBV/Plugin.hs @@ -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(..)) 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 @@ -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 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 @@ -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 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 @@ -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 diff --git a/Data/SBV/Plugin/Plugin.hs b/Data/SBV/Plugin/Plugin.hs --- a/Data/SBV/Plugin/Plugin.hs +++ b/Data/SBV/Plugin/Plugin.hs @@ -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 diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -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