sbvPlugin 0.9 → 0.10

raw patch · 6 files changed

+37/−10 lines, 6 filesdep ~basedep ~ghcdep ~ghc-prim

Dependency ranges changed: base, ghc, ghc-prim

Files

• CHANGES.md +4/−0
• Data/SBV/Plugin/Analyze.hs +1/−1
• Data/SBV/Plugin/Common.hs +24/−1
• Data/SBV/Plugin/Env.hs +2/−2
• Data/SBV/Plugin/Plugin.hs +3/−3
• sbvPlugin.cabal +3/−3

@@ -3,6 +3,10 @@  * Latest Hackage released version: 0.9, 2017-07-19 +### Version 0.10, Not yet released++  * Changes required to compile with GHC 8.2.1.+ ### Version 0.9, 2017-07-19    * Sync-up with recent modifications to SBV. No user visible changes.

@@ -584,7 +584,7 @@          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 []-                                             return (top, as)+                                             return $ TCKey (top, as)                walk []     sofar = Just $ reverse sofar                walk (a:as) sofar = case splitTyConApp_maybe a of                                       Just (ac, []) -> walk as (ac:sofar)

@@ -23,6 +23,8 @@ import CostCentre import GhcPlugins +import Unique (nonDetCmpUnique)+ import Data.Maybe (mapMaybe) import qualified Data.Map as M @@ -39,6 +41,27 @@                          , isList     :: Var -> Maybe Val                          } +-- | TyCon's are no longer Ord in GHC 8.2.1; so we make a newtype+newtype TCKey = TCKey (TyCon, [TyCon])++-- | Extract the unique "key"+tcKeyToUList :: TCKey -> [Unique]+tcKeyToUList (TCKey (a, as)) = map getUnique (a:as)++-- | Make a rudimentary Eq instance for TCKey+instance Eq TCKey where+  k1 == k2 = tcKeyToUList k1 == tcKeyToUList k2++-- | Make a rudimentary Ord instance for TCKey+instance Ord TCKey where+  k1 `compare` k2 = tcKeyToUList k1 `cmp` tcKeyToUList k2+    where []     `cmp` []     = EQ+          []     `cmp` _      = LT+          _      `cmp` []     = GT+          (a:as) `cmp` (b:bs) = case a `nonDetCmpUnique` b of+                                   EQ -> as `cmp` bs+                                   r  -> r+ -- | Interpreter environment data Env = Env { curLoc         :: [SrcSpan]                , flags          :: DynFlags@@ -49,7 +72,7 @@                , rUsedNames     :: IORef [String]                , rUITypes       :: IORef [(Type, S.Kind)]                , specials       :: Specials-               , tcMap          :: M.Map (TyCon, [TyCon]) S.Kind+               , tcMap          :: M.Map TCKey S.Kind                , envMap         :: M.Map (Var, SKind) Val                , destMap        :: M.Map Var          (Val -> [(Var, SKind)] -> (S.SVal, [((Var, SKind), Val)]))                , coreMap        :: M.Map Var          (SrcSpan, CoreExpr)

@@ -40,10 +40,10 @@ supportTupleSizes = [2 .. 15]  -- | Build the initial environment containing types-buildTCEnv :: Int -> CoreM (M.Map (TyCon, [TyCon]) S.Kind)+buildTCEnv :: Int -> CoreM (M.Map TCKey S.Kind) buildTCEnv wsz = do xs <- mapM grabTyCon basics                     ys <- mapM grabTyApp apps-                    return $ M.fromList $ xs ++ ys+                    return $ M.fromList [(TCKey k, v) | (k, v) <- xs ++ ys]    where grab = grabTH lookupTyCon 

@@ -33,9 +33,9 @@ plugin :: Plugin plugin = defaultPlugin {installCoreToDos = install}  where install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]-       install []          todos = reinitializeGlobals >> return (sbvPass : todos)-       install ["skip"]    todos = reinitializeGlobals >> return todos-       install ["runLast"] todos = reinitializeGlobals >> return (todos ++ [sbvPass])+       install []          todos = return (sbvPass : todos)+       install ["skip"]    todos = return todos+       install ["runLast"] todos = return (todos ++ [sbvPass])        install opts        _     = do liftIO $ putStrLn $ "[SBV] Unexpected command line options: " ++ show opts                                       liftIO $ putStrLn   ""                                       liftIO $ putStrLn   "Options:"

@@ -1,5 +1,5 @@ Name              : sbvPlugin-Version           : 0.9+Version           : 0.10 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 >= 7.0, mtl, template-haskell+  build-depends   : base >= 4.10 && < 5, ghc >= 8.2.1, ghc-prim >= 0.5.1, containers, sbv >= 7.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.8 && < 5, sbvPlugin, tasty, tasty-golden, filepath, process, directory+  Build-depends   : base >= 4.10 && < 5, sbvPlugin, tasty, tasty-golden, filepath, process, directory   Hs-Source-Dirs  : tests   main-is         : Run.hs