packages feed

sbvPlugin 0.4 → 0.5

raw patch · 53 files changed

+423/−505 lines, 53 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Data.SBV.Plugin.Examples.BitTricks: conditionalSetClearCorrect :: Bool -> Word32 -> Word32 -> Bool
+ Data.SBV.Plugin.Examples.BitTricks: fastMaxCorrect :: Int -> Int -> Bool
+ Data.SBV.Plugin.Examples.BitTricks: fastMinCorrect :: Int -> Int -> Bool
+ Data.SBV.Plugin.Examples.BitTricks: oneIf :: Num a => Bool -> a
+ Data.SBV.Plugin.Examples.BitTricks: oppositeSignsCorrect :: Int -> Int -> Bool
+ Data.SBV.Plugin.Examples.BitTricks: powerOfTwoCorrect :: Word32 -> Bool
+ Data.SBV.Plugin.Examples.MergeSort: isPermutationOf :: Eq a => [a] -> [a] -> Bool
+ Data.SBV.Plugin.Examples.MergeSort: merge :: Ord a => [a] -> [a] -> [a]
+ Data.SBV.Plugin.Examples.MergeSort: mergeSort :: Ord a => [a] -> [a]
+ Data.SBV.Plugin.Examples.MergeSort: mergeSortCorrect :: [Int] -> Bool
+ Data.SBV.Plugin.Examples.MergeSort: nonDecreasing :: Ord a => [a] -> Bool

Files

CHANGES.md view
@@ -1,7 +1,15 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub:  <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 0.4, 2015-12-24+* Latest Hackage released version: 0.5, 2015-12-26++### Version 0.5, 2015-12-26+ +  * Allow higher-order (i.e., function) arguments to theorems.+  * Rework uninterpreted functions, generalize types+  * Simplify cabal file; no need to ship gold-files for tests+  * Add merge-sort example "Data/SBV/Plugin/Examples/MergeSort.hs"+  * Add bit-tricks example "Data/SBV/Plugin/Examples/BitTricks.hs"  ### Version 0.4, 2015-12-24
Data/SBV/Plugin/Analyze.hs view
@@ -44,16 +44,18 @@          bind (b, e) = mapM_ work (sbvAnnotation b)           where work (SBV opts)-                 | Just s <- hasSkip opts  = liftIO $ putStrLn $ "[SBV] " ++ showSpan cfg b topLoc ++ " Skipping " ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ ": " ++ s-                 | Uninterpret `elem` opts = return ()-                 | True                    = liftIO $ prove cfg opts b topLoc e+                   | Just s <- hasSkip opts +                   = liftIO $ putStrLn $ "[SBV] " ++ showSpan cfg (pickSpan [varSpan b]) ++ " Skipping " ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ ": " ++ s+                   | Uninterpret `elem` opts+                   = return ()+                   | True+                   = liftIO $ prove cfg opts b e                 hasSkip opts = listToMaybe [s | Skip s <- opts]-                topLoc       = bindSpan b  -- | Prove an SBVTheorem-prove :: Config -> [SBVOption] -> Var -> SrcSpan -> CoreExpr -> IO ()-prove cfg@Config{isGHCi} opts b topLoc e = do-        success <- safely $ proveIt cfg opts (topLoc, b) e+prove :: Config -> [SBVOption] -> Var -> CoreExpr -> IO ()+prove cfg@Config{isGHCi} opts b e = do+        success <- safely $ proveIt cfg opts b e         unless (success || isGHCi || IgnoreFailure `elem` opts) $ do             putStrLn $ "[SBV] Failed. (Use option '" ++ show IgnoreFailure ++ "' to continue.)"              exitFailure@@ -65,16 +67,24 @@         bad e = do print e                    return False +-- | Sometimes life is hard. Giving up is an option.+die :: Config -> [SrcSpan] -> String -> [String] -> a+die cfg locs w es = error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es+  where marker = "[SBV] " ++ showSpan cfg (pickSpan locs)+        tag s = marker ++ " " ++ s+        tab s = replicate (length marker) ' ' ++  "    " ++ s+ -- | Returns True if proof went thru-proveIt :: Config -> [SBVOption] -> (SrcSpan, Var) -> CoreExpr -> IO Bool-proveIt cfg@Config{cfgEnv, sbvAnnotation} opts (topLoc, topBind) topExpr = do+proveIt :: Config -> [SBVOption] -> Var -> CoreExpr -> IO Bool+proveIt cfg@Config{cfgEnv, sbvAnnotation} opts topBind topExpr = do         solverConfigs <- pickSolvers opts         let verbose = Verbose    `elem` opts             qCheck  = QuickCheck `elem` opts             runProver prop               | qCheck = Left  `fmap` S.svQuickCheck prop               | True   = Right `fmap` S.proveWithAny [s{S.verbose = verbose} | s <- solverConfigs] prop-            loc = "[SBV] " ++ showSpan cfg topBind topLoc+            topLoc = varSpan topBind+            loc = "[SBV] " ++ showSpan cfg topLoc             slvrTag = ", using " ++ tag ++ "."               where tag = case solverConfigs of                             []     -> "no solvers"  -- can't really happen@@ -83,7 +93,7 @@                             xs     -> intercalate ", " (map show (init xs)) ++ ", and " ++ show (last xs)         putStrLn $ "\n" ++ loc ++ (if qCheck then " QuickChecking " else " Proving ") ++ show (sh topBind) ++ slvrTag         (finalResult, finalUninterps) <- do-                        finalResult    <- runProver (res cfgEnv)+                        finalResult    <- runProver (res cfgEnv topLoc)                         finalUninterps <- readIORef (rUninterpreted cfgEnv)                         return (finalResult, finalUninterps)         case finalResult of@@ -97,8 +107,8 @@                 putStr $ "[" ++ show solver ++ "] "                 print sres -                -- If proof failed and there are uninterpreted values, print a warning; except for "uninteresting" types-                let unintVals = filter ((`notElem` uninteresting cfgEnv) . snd) $ nub $ sortBy (comparing fst) [vt | (vt, _) <- finalUninterps]+                -- 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]                 unless (success || null unintVals) $ do                         let plu | length finalUninterps > 1 = "s:"                                 | True                      = ":"@@ -116,21 +126,17 @@    where debug = Debug `elem` opts -        res initEnv = do-               v <- runReaderT (symEval topExpr) initEnv{curLoc = topLoc}+        res initEnv topLoc = do+               v <- runReaderT (symEval topExpr) initEnv { curLoc     = [topLoc]+                                                         , mbListSize = listToMaybe [n | ListSize n <- opts]+                                                         }                case v of                  Base r -> return r                  r      -> error $ "Impossible happened. Final result reduced to a non-base value: " ++ showSDocUnsafe (ppr r) -        die :: SrcSpan -> String -> [String] -> a-        die loc w es = error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es-          where marker = "[SBV] " ++ showSpan cfg topBind loc-                tag s = marker ++ " " ++ s-                tab s = replicate (length marker) ' ' ++  "    " ++ s-         tbd :: String -> [String] -> Eval Val         tbd w ws = do Env{curLoc} <- ask-                      die curLoc w ws+                      die cfg curLoc w ws          sh o = showSDoc (flags cfgEnv) (ppr o) @@ -140,8 +146,7 @@         symEval :: CoreExpr -> Eval Val         symEval e = do let (bs, body) = collectBinders (pushLetLambda e)                        Env{curLoc} <- ask-                       let mbListSize = listToMaybe [n | ListSize n <- opts]-                       bodyType <- getType curLoc (exprType body)+                       bodyType <- getType (pickSpan curLoc) (exprType body)                         -- Figure out if there were some unmentioned variables; happens if the top                        -- level wasn't fully saturated.@@ -152,22 +157,22 @@                        case finalType of                          KBase S.KBool -> do -- First collect the named arguments:                                              argKs <- mapM (\b -> getType (getSrcSpan b) (varType b) >>= \bt -> return (b, bt)) bs-                                             let mkVar ((b, k), mbN) = do sv <- mkSym mbListSize curLoc (Just (idType b)) k (mbN `mplus` Just (sh b))+                                             let mkVar ((b, k), mbN) = do sv <- mkSym cfg (Just b) (varSpan b) (Just (idType b)) k (mbN `mplus` Just (sh b))                                                                           return ((b, k), sv)-                                             bArgs <- mapM (lift . mkVar) (zip argKs (concat [map Just ns | Names ns <- opts] ++ repeat Nothing))+                                             bArgs <- mapM mkVar (zip argKs (concat [map Just ns | Names ns <- opts] ++ repeat Nothing))                                               -- Go ahead and run the body symbolically; on bArgs                                              bRes <- local (\env -> env{envMap = foldr (uncurry M.insert) (envMap env) bArgs}) (go body)                                               -- If there are extraArgs; then create symbolics and apply to the result:                                              let feed []     sres       = return sres-                                                 feed (k:ks) (Func _ f) = do sv <- lift $ mkSym mbListSize curLoc Nothing k Nothing+                                                 feed (k:ks) (Func _ f) = do sv <- mkSym cfg Nothing (pickSpan curLoc) Nothing k Nothing                                                                              f sv >>= feed ks                                                  feed ks     v          = error $ "Impossible! Left with extra args to apply on a non-function: " ++ sh (ks, v)                                               feed extraArgs bRes -                         _             -> die curLoc "Non-boolean property declaration" (concat [ ["Found    : " ++ sh (exprType e)]+                         _             -> die cfg curLoc "Non-boolean property declaration" (concat [ ["Found    : " ++ sh (exprType e)]                                                                                                 , ["Returning: " ++ sh (exprType body) | not (null bs)]                                                                                                 , ["Expected : Bool" ++ if null bs then "" else " result"]                                                                                                 ])@@ -175,39 +180,11 @@                 pushLetLambda (Let b (Lam x bd)) = Lam x (pushLetLambda (Let b bd))                 pushLetLambda o                  = o -                -- Create a symbolic variable:-                mkSym :: Maybe Int -> SrcSpan -> Maybe Type -> SKind -> Maybe String -> S.Symbolic Val-                mkSym mbLs curLoc mbBType = sym-                 where tinfo k = case mbBType of-                                   Nothing -> "Kind: " ++ sh k-                                   Just t  -> "Type: " ++ sh t--                       sym (KBase k) nm  = do v <- S.svMkSymVar Nothing k nm-                                              return (Base v)--                       sym (KTup ks) nm = do let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. length ks]-                                             vs <- zipWithM sym ks ns-                                             return $ Tup vs--                       sym (KLst ks) nm = do let ls  = fromMaybe bad mbLs-                                                 bad = die curLoc "List-argument found, with no size info"-                                                                  [ "Name: " ++ fromMaybe "anonymous" nm-                                                                  , tinfo (KLst ks)-                                                                  , "Hint: Use the \"ListSize\" annotation"-                                                                  ]-                                                 ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. ls]-                                             vs <- zipWithM sym (replicate ls ks) ns-                                             return (Lst vs)--                       sym k         nm = die curLoc "Unsupported symbolic input" [ "Name: " ++ show nm-                                                                                  , tinfo k-                                                                                  ]-         isUninterpretedBinding :: Var -> Bool         isUninterpretedBinding v = any (Uninterpret `elem`) [opt | SBV opt <- sbvAnnotation v]          go :: CoreExpr -> Eval Val-        go (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t (curLoc envMap)}) $ go e+        go (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t : curLoc envMap}) $ go e         go e          = tgo (exprType e) e          debugTrace s w@@ -224,11 +201,11 @@                            case (v, k) `M.lookup` envMap of                              Just b  -> return b                              Nothing -> case v `M.lookup` coreMap of-                                           Just b  -> if isUninterpretedBinding v-                                                      then uninterpret t v-                                                      else go b-                                           Nothing -> debugTrace ("Uninterpreting: " ++ sh (v, k, nub $ sort $ map (fst . fst) (M.toList envMap)))-                                                               $ uninterpret t v+                                           Just (l, b)  -> if isUninterpretedBinding v+                                                           then uninterpret cfg False t v+                                                           else local (\env -> env{curLoc = l : curLoc env}) $ go b+                                           Nothing      -> debugTrace ("Uninterpreting: " ++ sh (v, k, nub $ sort $ map (fst . fst) (M.toList envMap)))+                                                                      $ uninterpret cfg False t v          tgo t e@(Lit l) = do Env{machWordSize} <- ask                              case l of@@ -259,15 +236,21 @@              Env{specials} <- ask               -- handle specials: Equality, tuples, and lists-             let isEq (App (App (Var v) (Type _)) dict) | isReallyADictionary dict, Just f <- isEquality specials v = Just f-                 isEq _                                                                                             = Nothing+             let getVar (Var v)    = Just v+                 getVar (Tick _ e) = getVar e+                 getVar _          = Nothing +                 isEq (App (App ev (Type _)) dict) | Just v <- getVar ev, isReallyADictionary dict, Just f <- isEquality specials v = Just f+                 isEq _                                                                                                             = Nothing+                  isTup (Var v)          = isTuple specials v                  isTup (App f (Type _)) = isTup f+                 isTup (Tick _ e)       = isTup e                  isTup _                = Nothing                   isLst (Var v)          = isList specials v                  isLst (App f (Type _)) = isLst f+                 isLst (Tick _ e)       = isLst e                  isLst _                = Nothing                   isSpecial e = isEq e `mplus` isTup e `mplus` isLst e@@ -275,6 +258,23 @@              case isSpecial reduced of                Just f  -> debugTrace ("Special located: " ++ sh (orig, f)) $ return f                Nothing -> case reduced of++                            -- special case for split and join; there must be a better way to do this+                            App (App (App (Var v) (Type t1)) (Type t2)) dict | isReallyADictionary dict -> do+                                Env{envMap} <- ask+                                let vSpan = getSrcSpan v+                                k1 <- getType vSpan t1+                                k2 <- getType vSpan t2+                                let kSplit = KFun k1 (KTup [k2, k2])+                                    kJoin  = KFun k1 (KFun k1 k2)+                                case ((v, kSplit) `M.lookup` envMap, (v, kJoin) `M.lookup` envMap)  of+                                  (Just b, _) -> debugTrace ("Located split: " ++ sh (reduced, kSplit)) $ return b+                                  (_, Just b) -> debugTrace ("Located join: "  ++ sh (reduced, kJoin))  $ return b+                                  _           -> do Env{coreMap} <- ask+                                                    case v `M.lookup` coreMap of+                                                      Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App (App (App e (Type t1)) (Type t2)) dict)+                                                      Nothing     -> tgo tFun (Var v)+                             App (App (Var v) (Type t)) dict | isReallyADictionary dict -> do                                 Env{envMap} <- ask                                 k <- getType (getSrcSpan v) t@@ -282,14 +282,14 @@                                   Just b  -> return b                                   Nothing -> do Env{coreMap} <- ask                                                 case v `M.lookup` coreMap of-                                                  Just e  -> tgo tFun (App (App e (Type t)) dict)-                                                  Nothing -> tgo tFun (Var v)+                                                  Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App (App e (Type t)) dict)+                                                  Nothing     -> tgo tFun (Var v)                              App (Var v) (Type t) -> do                                 Env{coreMap} <- ask                                 case v `M.lookup` coreMap of-                                  Just e  -> tgo tFun (App e (Type t))-                                  Nothing -> tgo tFun (Var v)+                                  Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App e (Type t))+                                  Nothing     -> tgo tFun (Var v)                              App (Let (Rec bs) f) a -> go (Let (Rec bs) (App f a)) @@ -307,35 +307,38 @@                 Env{envMap} <- ask                 return $ Func (Just (sh b)) $ \s -> local (\env -> env{envMap = M.insert (b, k) s envMap}) (go body) -        tgo _ (Let (NonRec b e) body) = local (\env -> env{coreMap = M.insert b e (coreMap env)}) (go body)+        tgo _ (Let (NonRec b e) body) = local (\env -> env{coreMap = M.insert b (varSpan b, e) (coreMap env)}) (go body) -        tgo _ (Let (Rec bs) body) = local (\env -> env{coreMap = foldr (uncurry M.insert) (coreMap env) bs}) (go body)+        tgo _ (Let (Rec bs) body) = local (\env -> env{coreMap = foldr (\(b, e) m -> M.insert b (varSpan b, e) m) (coreMap env) bs}) (go body)          -- 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)            = do sce <- go ce-                Env{curLoc} <- ask-                let caseTooComplicated l w [] = die l ("Unsupported case-expression (" ++ w ++ ")") [sh e]-                    caseTooComplicated l w xs = die l ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs+                let caseTooComplicated l w [] = die cfg l ("Unsupported case-expression (" ++ w ++ ")") [sh e]+                    caseTooComplicated l w xs = die cfg l ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs                     isDefault (DEFAULT, _, _) = True                     isDefault _               = False                     (defs, nonDefs)           = partition isDefault alts                     walk ((p, bs, rhs) : rest) =                          do -- try to get a "good" location for this alternative, if possible:                             let eLoc = case (rhs, bs) of-                                        (Tick t _, _  ) -> tickSpan t curLoc-                                        (_,        b:_) -> bindSpan b-                                        _               -> curLoc+                                        (Tick t _, _  ) -> tickSpan t+                                        (Var v,    _  ) -> varSpan v+                                        (_,        b:_) -> varSpan b+                                        _               -> varSpan caseBinder                             mr <- match eLoc sce p bs                             case mr of-                              Just (m, bs') -> do let result = local (\env -> env{envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs+                              Just (m, bs') -> do let result = local (\env -> env{curLoc = eLoc : curLoc env, envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs                                                   if null rest                                                      then result-                                                     else choose (caseTooComplicated eLoc "with-complicated-alternatives-during-merging") m result (walk rest)-                              Nothing -> caseTooComplicated eLoc "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs]-                    walk []                   = caseTooComplicated curLoc "with-non-exhaustive-match" []  -- can't really happen+                                                     else do Env{curLoc} <- ask+                                                             choose (caseTooComplicated (eLoc : curLoc) "with-complicated-alternatives-during-merging") m result (walk rest)+                              Nothing -> do Env{curLoc} <- ask+                                            caseTooComplicated (eLoc : curLoc) "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs]+                    walk []                   = do Env{curLoc} <- ask+                                                   caseTooComplicated curLoc "with-non-exhaustive-match" []  -- can't really happen                 k <- getType (getSrcSpan caseBinder) caseType                 local (\env -> env{envMap = M.insert (caseBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs)            where choose bailOut t tb fb = case S.svAsBool t of@@ -363,11 +366,11 @@         tgo t (Cast e c)            = debugTrace ("Going thru a Cast: " ++ sh c) $ tgo t e -        tgo _ (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t (curLoc envMap)}) $ go e+        tgo _ (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t : curLoc envMap}) $ go e          tgo _ (Type t)            = do Env{curLoc} <- ask-                k <- getType curLoc t+                k <- getType (pickSpan curLoc) t                 return (Typ k)          tgo _ e@Coercion{}@@ -384,8 +387,8 @@                    else do let chaseVars :: CoreExpr -> Eval CoreExpr                                chaseVars (Var x)    = do Env{coreMap} <- ask                                                          case x `M.lookup` coreMap of-                                                           Nothing -> return (Var x)-                                                           Just b  -> chaseVars b+                                                           Nothing     -> return (Var x)+                                                           Just (_, b) -> chaseVars b                                chaseVars (Tick _ x) = chaseVars x                                chaseVars x          = return x                            func <- chaseVars rf@@ -405,29 +408,86 @@ isReallyADictionary (Var v)   = "$" `isPrefixOf` unpackFS (occNameFS (occName (varName v))) isReallyADictionary _         = False +-- Create a symbolic variable.+mkSym :: Config -> Maybe Var -> SrcSpan -> Maybe Type -> SKind -> Maybe String -> Eval Val+mkSym cfg@Config{cfgEnv} mbBind curLoc mbBType = sym+ where sh o = showSDoc (flags cfgEnv) (ppr o)++       tinfo k = case mbBType of+                   Nothing -> "Kind: " ++ sh k+                   Just t  -> "Type: " ++ sh t++       sym (KBase k) nm  = do v <- lift $ S.svMkSymVar Nothing k nm+                              return (Base v)++       sym (KTup ks) nm = do let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. length ks]+                             vs <- zipWithM sym ks ns+                             return $ Tup vs++       sym (KLst ks) nm = do Env{mbListSize} <- ask+                             let ls  = fromMaybe bad mbListSize+                                 bad = die cfg [curLoc] "List-argument found, with no size info"+                                                        [ "Name: " ++ fromMaybe "anonymous" nm+                                                        , tinfo (KLst ks)+                                                        , "Hint: Use the \"ListSize\" annotation"+                                                        ]+                                 ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. ls]+                             vs <- zipWithM sym (replicate ls ks) ns+                             return (Lst vs)++       sym k@KFun{}  nm = case mbBind of+                            Just v -> uninterpret cfg True (varType v) v+                            _      -> die cfg [curLoc] "Unsupported unnamed higher-order symbolic input"+                                                       [ "Name: " ++ fromMaybe "<anonymous>" nm+                                                       , tinfo k+                                                       , "Hint: Name all higher-order inputs explicitly"+                                                       ]++ -- | Uninterpret an expression-uninterpret :: Type -> Var -> Eval Val-uninterpret t v = do+uninterpret :: Config -> Bool -> Type -> Var -> Eval Val+uninterpret cfg isInput t var = do           Env{rUninterpreted, flags} <- ask           prevUninterpreted <- liftIO $ readIORef rUninterpreted-          case (v, t) `lookup` prevUninterpreted of-             Just (_, val) -> return val-             Nothing       -> do let (tvs,  t')  = splitForAllTys t-                                     (args, res) = splitFunTys t'-                                     sp          = getSrcSpan v-                                 argKs <- mapM (getType sp) args-                                 resK  <- getType sp res-                                 nm <- mkValidName $ showSDoc flags (ppr v)-                                 let fVal = wrap tvs $ walk argKs (nm, resK) []-                                 liftIO $ modifyIORef rUninterpreted (((v, t), (nm, fVal)) :)-                                 return fVal-  where walk :: [SKind] -> (String, SKind) -> [S.SVal] -> Val-        walk []     (nm, k) args = case k of-                                     KBase b -> Base $ S.svUninterpreted b nm Nothing (reverse args)-                                     _       -> error $ "Not yet supported uninterpreted type with non-base type: " ++ showSDocUnsafe (ppr k)-        walk (_:as) nmk     args = Func Nothing $ \a -> case a of-                                                          Base p -> return (walk as nmk (p:args))-                                                          _      -> return (walk as nmk args)+          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+  where walk :: [SKind] -> (String, SKind) -> [Val] -> Eval Val+        walk []     (nm, k) args = do Env{curLoc, mbListSize} <- ask++                                      let ls  = fromMaybe bad mbListSize+                                          bad = die cfg curLoc "List-argument found in uninterpreted function, with no size info"+                                                               ["Hint: Use the \"ListSize\" annotation"]++                                          mkArg :: Val -> [S.SVal]+                                          mkArg (Base v)  = [v]+                                          mkArg (Tup  vs) = concatMap mkArg vs+                                          mkArg (Lst  vs) = concatMap mkArg vs+                                          mkArg sk        = error $ "Not yet supported uninterpreted function with a higher-order argument: " ++ showSDocUnsafe (ppr sk)++                                          bArgs = concatMap mkArg (reverse args)++                                          mkRes :: String -> SKind -> [S.SVal]+                                          mkRes n (KBase b)  = [S.svUninterpreted b n Nothing bArgs]+                                          mkRes n (KTup  bs) = concat $ zipWith mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) ..   ]] bs+                                          mkRes n (KLst  b)  = concat [mkRes (n ++ "_" ++ show i) b | i <- [(1 :: Int) .. ls]]+                                          mkRes _ sk         = error $ "Not yet supported uninterpreted function with a higher-order result: " ++ showSDocUnsafe (ppr sk)++                                          res = map Base $ mkRes nm k+                                      case res of+                                        [x] -> return x+                                        _   -> return $ Tup res++        walk (_:ks) nmk     args = return $ Func Nothing $ \a -> walk ks nmk (a:args)         wrap []     f = f         wrap (_:ts) f = Func Nothing $ \(Typ _) -> return (wrap ts f) @@ -458,7 +518,7 @@  -- | Convert a Core type to an SBV Type, retaining functions and tuples getType :: SrcSpan -> Type -> Eval SKind-getType sp typ = do let (tvs, typ')   = splitForAllTys typ+getType sp typ = do let (tvs, typ') = splitForAllTys typ                         (args, res) = splitFunTys typ'                     argKs <- mapM (getType sp) args                     resK  <- getComposite res
Data/SBV/Plugin/Common.hs view
@@ -10,6 +10,8 @@ -----------------------------------------------------------------------------  {-# LANGUAGE NamedFieldPuns       #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances    #-} {-# OPTIONS_GHC -fno-warn-orphans #-}  module Data.SBV.Plugin.Common where@@ -36,18 +38,19 @@                          }  -- | Interpreter environment-data Env = Env { curLoc         :: SrcSpan+data Env = Env { curLoc         :: [SrcSpan]                , flags          :: DynFlags                , machWordSize   :: Int+               , mbListSize     :: Maybe Int                , uninteresting  :: [Type]-               , rUninterpreted :: IORef [((Var, Type), (String, Val))]+               , rUninterpreted :: IORef [((Var, Type), (Bool, String, Val))]                , rUsedNames     :: IORef [String]                , rUITypes       :: IORef [(Type, S.Kind)]                , specials       :: Specials                , tcMap          :: M.Map (TyCon, [TyCon]) S.Kind                , envMap         :: M.Map (Var, SKind) Val                , destMap        :: M.Map Var          (Val -> [(Var, SKind)] -> (S.SVal, [((Var, SKind), Val)]))-               , coreMap        :: M.Map Var CoreExpr+               , coreMap        :: M.Map Var          (SrcSpan, CoreExpr)                }  @@ -138,15 +141,38 @@                                                                ]  -- | Compute the span given a Tick. Returns the old-span if the tick span useless.-tickSpan :: Tickish t -> SrcSpan -> SrcSpan-tickSpan (ProfNote cc _ _) _ = cc_loc cc-tickSpan (SourceNote s _)  _ = RealSrcSpan s-tickSpan _                 s = s+tickSpan :: Tickish t -> SrcSpan+tickSpan (ProfNote cc _ _) = cc_loc cc+tickSpan (SourceNote s _)  = RealSrcSpan s+tickSpan _                 = noSrcSpan  -- | Compute the span for a binding.-bindSpan :: Var -> SrcSpan-bindSpan = nameSrcSpan . varName+varSpan :: Var -> SrcSpan+varSpan = nameSrcSpan . varName --- | Show a GHC span in user-friendly form.-showSpan :: Config -> Var -> SrcSpan -> String-showSpan Config{cfgEnv} b s = showSDoc (flags cfgEnv) $ if isGoodSrcSpan s then ppr s else ppr b+-- | Pick the first "good" span, hopefully corresponding to+-- the closest location to where we are in the code+-- when we issue an error message.+pickSpan :: [SrcSpan] -> SrcSpan+pickSpan ss = case filter isGoodSrcSpan ss of+                (s:_) -> s+                []    -> noSrcSpan++-- | Show a GHC span in user-friendly form+showSpan :: Config -> SrcSpan -> String+showSpan Config{cfgEnv} s = showSDoc (flags cfgEnv) (ppr s)++-- | This comes mighty handy! Wonder why GHC doesn't have it already:+instance Show CoreExpr where+  show = go+    where sh x = showSDocUnsafe (ppr x)+          go (Var   i)      = "(Var "  ++ sh i ++ ")"+          go (Lit   l)      = "(Lit "  ++ sh l ++ ")"+          go (App f a)      = "(App "  ++ go f ++ " " ++ go a ++ ")"+          go (Lam b e)      = "(Lam "  ++ sh b ++ " " ++ go e ++ ")"+          go (Let b e)      = "(Let "  ++ sh b ++ " " ++ go e ++ ")"+          go (Case e b t _) = "(Case " ++ go e ++ " " ++ sh b ++ " " ++ sh t ++ "...)"+          go (Cast e _)     = "(Cast " ++ go e ++ " ...)"+          go (Tick _ e)     = "(Tick " ++ go e ++ ")"+          go (Type t)       = "(Type " ++ sh t ++ ")"+          go (Coercion _)   = "(Coercion ...)"
Data/SBV/Plugin/Env.hs view
@@ -32,7 +32,6 @@  import Data.SBV.Plugin.Common - -- | What tuple-sizes we support? We go upto 15, but would be easy to change if necessary supportTupleSizes :: [Int] supportTupleSizes = [2 .. 15]@@ -108,9 +107,15 @@       ++ [ (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]]+  where        -- Bit-vectors-       bvKinds    = [S.KBounded s sz | s <- [False, True], sz <- [8, 16, 32, 64]]+       bvKinds = [S.KBounded s sz | s <- [False, True], sz <- [8, 16, 32, 64]]         -- Those that are "integral"ish        integralKinds = S.KUnbounded : bvKinds@@ -262,6 +267,18 @@ 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))+ -- | Lift a unary SBV function that via kind/integer lift1Int :: (Integer -> S.SVal) -> Val lift1Int f = Func Nothing g@@ -285,6 +302,16 @@          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
+ Data/SBV/Plugin/Examples/BitTricks.hs view
@@ -0,0 +1,73 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Plugin.Examples.BitTricks+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Checks the correctness of a few tricks from the large collection found in:+--      <http://graphics.stanford.edu/~seander/bithacks.html>+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}++module Data.SBV.Plugin.Examples.BitTricks where++import Data.SBV.Plugin++import Data.Bits+import Data.Word++-- | Returns 1 if bool is @True@+oneIf :: Num a => Bool -> a+oneIf True  = 1+oneIf False = 0++-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>+{-# ANN fastMinCorrect theorem #-}+fastMinCorrect :: Int -> Int -> Bool+fastMinCorrect x y = m == fm+  where m  = if x < y then x else y+        fm = y `xor` ((x `xor` y) .&. (-(oneIf (x < y))));++-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>+{-# ANN fastMaxCorrect theorem #-}+fastMaxCorrect :: Int -> Int -> Bool+fastMaxCorrect x y = m == fm+  where m  = if x < y then y else x+        fm = x `xor` ((x `xor` y) .&. (-(oneIf (x < y))));++-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns>+{-# ANN oppositeSignsCorrect theorem #-}+oppositeSignsCorrect :: Int -> Int -> Bool+oppositeSignsCorrect x y = r == os+  where r  = (x < 0 && y >= 0) || (x >= 0 && y < 0)+        os = (x `xor` y) < 0++-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching>+{-# ANN conditionalSetClearCorrect theorem #-}+conditionalSetClearCorrect :: Bool -> Word32 -> Word32 -> Bool+conditionalSetClearCorrect f m w = r == r'+  where r  | f    = w .|. m+           | True = w .&. complement m+        r' = w `xor` ((-(oneIf f) `xor` w) .&. m)++-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>+{-# ANN powerOfTwoCorrect theorem #-}+powerOfTwoCorrect :: Word32 -> Bool+powerOfTwoCorrect v = f == search powers+  where f = (v /= 0) && ((v .&. (v-1)) == 0)++        powers :: [Word32]+        powers = [        1,        2,        4,         8,        16,        32,         64,        128+                 ,      256,      512,     1024,      2048,      4096,      8192,      16384,      32768+                 ,    65536,   131072,   262144,    524288,   1048576,   2097152,    4194304,    8388608+                 , 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648+                 ]++        search :: [Word32] -> Bool+        search []     = False+        search (x:xs)+          | x == v    = True+          | True      = search xs
+ Data/SBV/Plugin/Examples/MergeSort.hs view
@@ -0,0 +1,101 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Plugin.Examples.MergeSort+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- An implementation of merge-sort and its correctness.+-----------------------------------------------------------------------------+--+{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}++module Data.SBV.Plugin.Examples.MergeSort where++import Data.SBV.Plugin++-----------------------------------------------------------------------------+-- * Implementing merge-sort+-- ${mergeSort}+-----------------------------------------------------------------------------+{- $mergeSort+A straightforward implementation of merge sort. We simply divide the input list+in to two halves so long as it has at least two elements, sort each half on its+own, and then merge.+-}++-- | Merging two given sorted lists, preserving the order.+merge :: Ord a => [a] -> [a] -> [a]+merge []     ys           = ys+merge xs     []           = xs+merge xs@(x:xr) ys@(y:yr)+  | x < y                 = x : merge xr ys+  | True                  = y : merge xs yr++-- | Simple merge-sort implementation.+mergeSort :: Ord a => [a] -> [a]+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)++-----------------------------------------------------------------------------+-- * Proving correctness of sorting+-- ${props}+-----------------------------------------------------------------------------+{- $props+There are two main parts to proving that a sorting algorithm is correct:++       * Prove that the output is non-decreasing+ +       * Prove that the output is a permutation of the input+-}++-- | Check whether a given sequence is non-decreasing.+nonDecreasing :: Ord a => [a] -> Bool+nonDecreasing []       = True+nonDecreasing [_]      = True+nonDecreasing (a:b:xs) = a <= b && nonDecreasing (b:xs)++-- | Check whether two given sequences are permutations. We simply check that each sequence+-- is a subset of the other, when considered as a set. The check is slightly complicated+-- for the need to account for possibly duplicated elements.+isPermutationOf :: Eq a => [a] -> [a] -> Bool+isPermutationOf as bs = go as [(b, True) | b <- bs] && go bs [(a, True) | a <- as]+  where go :: Eq a => [a] -> [(a, Bool)] -> Bool+        go []     _  = True+        go (x:xs) ys = found && go xs ys'+           where (found, ys') = mark x ys++        -- Go and mark off an instance of 'x' in the list, if possible. We keep track+        -- of unmarked elements by associating a boolean bit. Note that we have to+        -- keep the lists equal size for the recursive result to merge properly.+        mark :: Eq a => a -> [(a, Bool)] -> (Bool, [(a, Bool)])+        mark _ []            = (False, [])+        mark x ((y, v) : ys)+          | v && x == y      = (True, (y, not v) : ys)+          | True             = (r, (y, v) : ys')+          where (r, ys') = mark x ys++-----------------------------------------------------------------------------+-- * The correctness theorem+-----------------------------------------------------------------------------++-- | 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.+--+-- We have:+--+-- @+--   [SBV] tests/T48.hs:100:1-16 Proving "mergeSortCorrect", using Z3.+--   [Z3] Q.E.D.+-- @+{-# ANN mergeSortCorrect theorem { options = [ListSize 4] } #-}+mergeSortCorrect :: [Int] -> Bool+mergeSortCorrect xs = nonDecreasing ys && isPermutationOf xs ys+   where ys = mergeSort xs
Data/SBV/Plugin/Plugin.hs view
@@ -66,9 +66,10 @@           let cfg = Config { isGHCi        = hscTarget df == HscInterpreted                            , opts          = []                            , sbvAnnotation = lookupWithDefaultUFM anns [] . varUnique-                           , cfgEnv        = Env { curLoc         = noSrcSpan+                           , cfgEnv        = Env { curLoc         = []                                                  , flags          = df                                                  , machWordSize   = wsz+                                                 , mbListSize     = Nothing                                                  , uninteresting  = uninteresting                                                  , rUninterpreted = rUninterpreted                                                  , rUsedNames     = rUsedNames@@ -77,13 +78,13 @@                                                  , tcMap          = baseTCs                                                  , envMap         = baseEnv                                                  , destMap        = baseDests-                                                 , coreMap        = M.fromList (flattenBinds mg_binds)+                                                 , coreMap        = M.fromList [(b, (varSpan b, e)) | (b, e) <- flattenBinds mg_binds]                                                  }                            } -          let bindLoc (NonRec b _)     = bindSpan b+          let bindLoc (NonRec b _)     = varSpan b               bindLoc (Rec [])         = noSrcSpan-              bindLoc (Rec ((b, _):_)) = bindSpan b+              bindLoc (Rec ((b, _):_)) = varSpan b            mapM_ (analyzeBind cfg) $ sortBy (comparing bindLoc) mg_binds
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name              : sbvPlugin-Version           : 0.4+Version           : 0.5 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@@ -16,7 +16,6 @@ Maintainer        : Levent Erkok (erkokl@gmail.com) Build-Type        : Simple Cabal-Version     : >= 1.14-Data-Files        : tests/GoldFiles/*.hs.golden Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md  source-repository head@@ -27,7 +26,9 @@   default-language: Haskell2010   ghc-options     : -Wall -fplugin-opt Data.SBV.Plugin:skip   Exposed-modules : Data.SBV.Plugin+                  , 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.7, mtl, template-haskell   Other-modules   : Data.SBV.Plugin.Analyze                   , Data.SBV.Plugin.Data
− tests/GoldFiles/T00.hs.golden 
@@ -1,8 +0,0 @@--[SBV] tests/T00.hs:12:1 Proving "f", using Z3.-[Z3] Q.E.D.--[SBV] tests/T00.hs:16:1 Proving "g", using Z3.-[Z3] Falsifiable. Counter-example:-  _x =     0 :: Int8-  _y = False :: Bool
− tests/GoldFiles/T01.hs.golden 
@@ -1,7 +0,0 @@--[SBV] tests/T01.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x =  40959.98499298095 :: Double-  y = -73732.00109529495 :: Double-  z =  257.9890136271454 :: Double-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T02.hs.golden 
@@ -1,5 +0,0 @@--[SBV] tests/T02.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = 1 :: Integer-  y = 0 :: Integer
− tests/GoldFiles/T03.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T03.hs:10:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T04.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T04.hs:10:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T05.hs.golden 
@@ -1,5 +0,0 @@--[SBV] tests/T05.hs:9:1 Proving "f", using CVC4.-[CVC4] Falsifiable. Counter-example:-  x =  0 :: Integer-  y = -1 :: Integer
− tests/GoldFiles/T06.hs.golden 
@@ -1,5 +0,0 @@--[SBV] tests/T06.hs:10:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = -128 :: Int8-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T07.hs.golden 
@@ -1,5 +0,0 @@--[SBV] tests/T07.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = NaN :: Double-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T08.hs.golden 
@@ -1,5 +0,0 @@--[SBV] tests/T08.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = 0.0 :: Double-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T09.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T09.hs:10:1 QuickChecking "f", using Z3.-(0 tests)         (1 test)        (2 tests)         (3 tests)         (4 tests)         (5 tests)         (6 tests)         (7 tests)         (8 tests)         (9 tests)         (10 tests)          (11 tests)          (12 tests)          (13 tests)          (14 tests)          (15 tests)          (16 tests)          (17 tests)          (18 tests)          (19 tests)          (20 tests)          (21 tests)          (22 tests)          (23 tests)          (24 tests)          (25 tests)          (26 tests)          (27 tests)          (28 tests)          (29 tests)          (30 tests)          (31 tests)          (32 tests)          (33 tests)          (34 tests)          (35 tests)          (36 tests)          (37 tests)          (38 tests)          (39 tests)          (40 tests)          (41 tests)          (42 tests)          (43 tests)          (44 tests)          (45 tests)          (46 tests)          (47 tests)          (48 tests)          (49 tests)          (50 tests)          (51 tests)          (52 tests)          (53 tests)          (54 tests)          (55 tests)          (56 tests)          (57 tests)          (58 tests)          (59 tests)          (60 tests)          (61 tests)          (62 tests)          (63 tests)          (64 tests)          (65 tests)          (66 tests)          (67 tests)          (68 tests)          (69 tests)          (70 tests)          (71 tests)          (72 tests)          (73 tests)          (74 tests)          (75 tests)          (76 tests)          (77 tests)          (78 tests)          (79 tests)          (80 tests)          (81 tests)          (82 tests)          (83 tests)          (84 tests)          (85 tests)          (86 tests)          (87 tests)          (88 tests)          (89 tests)          (90 tests)          (91 tests)          (92 tests)          (93 tests)          (94 tests)          (95 tests)          (96 tests)          (97 tests)          (98 tests)          (99 tests)          +++ OK, passed 100 tests.
− tests/GoldFiles/T10.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T10.hs:12:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T11.hs.golden 
@@ -1,5 +0,0 @@--[SBV] tests/T11.hs:15:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = 11 :: Integer-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T12.hs.golden 
@@ -1,6 +0,0 @@--[SBV] tests/T12.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  i =     2 :: Integer-  b = False :: Bool-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T13.hs.golden 
@@ -1,7 +0,0 @@--[SBV] tests/T13.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  i =     0 :: Integer-  d =   0.0 :: Double-  b = False :: Bool-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T14.hs.golden 
@@ -1,5 +0,0 @@--[SBV] tests/T14.hs:10:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = 1.0 :: Real-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T15.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T15.hs:11:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T16.hs.golden 
@@ -1,7 +0,0 @@--[SBV] tests/T16.hs:11:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  age = Age!val!0 :: Age-[SBV] Counter-example might be bogus due to uninterpreted constant:-  [<no location info>] ds_d6ck :: Int-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T17.hs.golden 
@@ -1,7 +0,0 @@--[SBV] tests/T17.hs:14:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = 0 :: Int64-[SBV] Counter-example might be bogus due to uninterpreted constant:-  [tests/T17.hs:9:1] g :: Int -> Int-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T18.hs.golden 
@@ -1,59 +0,0 @@--[SBV] tests/T18.hs:11:1 Proving "f", using Z3.-** Starting symbolic simulation..-** Generated symbolic trace:-SORTS-  Age-INPUTS-  s0 :: Age, aliasing "a"-  s1 :: Age, aliasing "b"-CONSTANTS-  s_2 = False :: Bool-  s_1 = True :: Bool-TABLES-ARRAYS-UNINTERPRETED CONSTANTS-USER GIVEN CODE SEGMENTS-AXIOMS-DEFINE-  s2 :: SBool = s0 == s1-CONSTRAINTS-ASSERTIONS-OUTPUTS-  s2-** Translating to SMT-Lib..-** Checking Theoremhood..-** Generated SMTLib program:-; Automatically generated by SBV. Do not edit.-(set-option :produce-models true)-; has user-defined sorts, no logic specified.-; --- uninterpreted sorts ----(declare-sort Age 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T18.hs:11:3-; --- literal constants ----(define-fun s_2 () Bool false)-(define-fun s_1 () Bool true)-; --- skolem constants ----(declare-fun s0 () Age) ; tracks user variable "a"-(declare-fun s1 () Age) ; tracks user variable "b"-; --- constant tables ----; --- skolemized tables ----; --- arrays ----; --- uninterpreted constants ----; --- user given axioms ----; --- formula ----(assert ; no quantifiers-   (let ((s2 (= s0 s1)))-   (not s2)))-** Calling: "z3 -nw -in -smt2"-** Sending the following model extraction commands:-(get-value (s0))-(get-value (s1))-** Z3 output:-sat-((s0 Age!val!0))-((s1 Age!val!1))-** Done..-[Z3] Falsifiable. Counter-example:-  a = Age!val!0 :: Age-  b = Age!val!1 :: Age-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T19.hs.golden 
@@ -1,14 +0,0 @@--[SBV] tests/T19.hs:9:1 Proving "f", using Z3.-[Z3] Q.E.D.--[SBV] tests/T19.hs:15:1 Proving "g", using Z3.-[Z3] Falsifiable. Counter-example:-  s_1 = sbvChar!val!0 :: sbvChar-  s_2 = sbvChar!val!0 :: sbvChar-  s_3 = sbvChar!val!0 :: sbvChar-  s_4 = sbvChar!val!0 :: sbvChar-  s_5 = sbvChar!val!0 :: sbvChar-  s_6 = sbvChar!val!0 :: sbvChar-[SBV] Counter-example might be bogus due to uninterpreted constants:-  [<wired into compiler>] C# :: Char# -> Char
− tests/GoldFiles/T20.hs.golden 
@@ -1,1 +0,0 @@-[SBV] tests/T20.hs:10:1 Skipping "f": Don't want to prove this now.
− tests/GoldFiles/T21.hs.golden 
@@ -1,36 +0,0 @@--[SBV] tests/T21.hs:9:1 Proving "f", using Z3.-** Starting symbolic simulation..-** Generated symbolic trace:-True :: Bool-** Translating to SMT-Lib..-** Checking Theoremhood..-** Generated SMTLib program:-; Automatically generated by SBV. Do not edit.-(set-option :produce-models true)-; has user-defined sorts, no logic specified.-; --- uninterpreted sorts ----(declare-sort sbvChar 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T21.hs:9:3-; --- literal constants ----(define-fun s_2 () Bool false)-(define-fun s_1 () Bool true)-; --- skolem constants ----(declare-fun s0 () sbvChar) ; tracks user variable "c"-(declare-fun s1 () sbvChar) ; tracks user variable "s_1"-(declare-fun s2 () sbvChar) ; tracks user variable "s_2"-(declare-fun s3 () sbvChar) ; tracks user variable "s_3"-(declare-fun s4 () sbvChar) ; tracks user variable "s_4"-(declare-fun s5 () sbvChar) ; tracks user variable "s_5"-; --- constant tables ----; --- skolemized tables ----; --- arrays ----; --- uninterpreted constants ----; --- user given axioms ----; --- formula ----(assert ; no quantifiers-   (not s_1))-** Calling: "z3 -nw -in -smt2"-** Z3 output:-unsat-** Done..-[Z3] Q.E.D.
− tests/GoldFiles/T22.hs.golden 
@@ -1,5 +0,0 @@--[SBV] tests/T22.hs:12:1 Proving "g", using Z3.-[Z3] Falsifiable. Counter-example:-  s0 = -1 :: Int64-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T23.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T23.hs:9:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T24.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T24.hs:10:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T25.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T25.hs:9:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T26.hs.golden 
@@ -1,4 +0,0 @@--[SBV] tests/T26.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T27.hs.golden 
@@ -1,29 +0,0 @@--[SBV] tests/T27.hs:9:1 Proving "g", using Z3.-** Starting symbolic simulation..-** Generated symbolic trace:-True :: Bool-** Translating to SMT-Lib..-** Checking Theoremhood..-** Generated SMTLib program:-; Automatically generated by SBV. Do not edit.-(set-option :produce-models true)-(set-logic QF_BV)-; --- uninterpreted sorts ----; --- literal constants ----(define-fun s_2 () Bool false)-(define-fun s_1 () Bool true)-; --- skolem constants ----; --- constant tables ----; --- skolemized tables ----; --- arrays ----; --- uninterpreted constants ----; --- user given axioms ----; --- formula ----(assert ; no quantifiers-   (not s_1))-** Calling: "z3 -nw -in -smt2"-** Z3 output:-unsat-** Done..-[Z3] Q.E.D.
− tests/GoldFiles/T28.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T28.hs:13:1 Proving "g", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T29.hs.golden 
@@ -1,4 +0,0 @@--[SBV] tests/T29.hs:13:1 Proving "g", using Z3.-[Z3] Falsifiable-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T30.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T30.hs:9:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T31.hs.golden 
@@ -1,19 +0,0 @@--[SBV] tests/T31.hs:9:1 Proving "f", using Z3.--[SBV] tests/T31.hs:9:1 Skipping proof. Non-boolean property declaration:-                          Found    : Int -> Int-                          Returning: Int-                          Expected : Bool result--[SBV] tests/T31.hs:13:1 Proving "g", using Z3.--[SBV] tests/T31.hs:13:1 Skipping proof. Non-boolean property declaration:-                           Found    : Char-                           Expected : Bool--[SBV] tests/T31.hs:17:1 Proving "h", using Z3.--[SBV] tests/T31.hs:17:1 Skipping proof. Non-boolean property declaration:-                           Found    : Double-                           Expected : Bool
− tests/GoldFiles/T32.hs.golden 
@@ -1,7 +0,0 @@--[SBV] tests/T32.hs:11:1 Proving "f", using Z3.-[Z3] Q.E.D.--[SBV] tests/T32.hs:15:1 Proving "g", using Z3.-[Z3] Falsifiable. Counter-example:-  x = 32 :: Word8
− tests/GoldFiles/T33.hs.golden 
@@ -1,7 +0,0 @@--[SBV] tests/T33.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = 0 :: Int64--[SBV] tests/T33.hs:15:1 Proving "g", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T34.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T34.hs:9:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T35.hs.golden 
@@ -1,6 +0,0 @@--[SBV] tests/T35.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  x = -1 :: Int64-  y =  0 :: Int64-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T36.hs.golden 
@@ -1,9 +0,0 @@--[SBV] tests/T36.hs:9:1 Proving "f", using Z3.-[Z3] Q.E.D.--[SBV] tests/T36.hs:14:1 Proving "g", using Z3.-[Z3] Falsifiable. Counter-example:-  a = -65 :: Int64-  b = -65 :: Int64-  c =  64 :: Int64
− tests/GoldFiles/T37.hs.golden 
@@ -1,6 +0,0 @@--[SBV] tests/T37.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  a =   2 :: Int64-  b = 2.3 :: Double-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T38.hs.golden 
@@ -1,7 +0,0 @@--[SBV] tests/T38.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  a = 1 :: Int64-  b = 2 :: Int64-  c = 4 :: Int64-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T39.hs.golden 
@@ -1,6 +0,0 @@--[SBV] tests/T39.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  p_1 = -1 :: Int64-  p_2 =  0 :: Int64-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T40.hs.golden 
@@ -1,3 +0,0 @@--[SBV] tests/T40.hs:9:1 Proving "f", using Z3.-[Z3] Q.E.D.
− tests/GoldFiles/T41.hs.golden 
@@ -1,8 +0,0 @@--[SBV] tests/T41.hs:9:1 Proving "f", using Z3.-[Z3] Q.E.D.--[SBV] tests/T41.hs:13:1 Proving "g", using Z3.-[Z3] Falsifiable. Counter-example:-  x = -1 :: Int64-  y =  0 :: Int64
− tests/GoldFiles/T42.hs.golden 
@@ -1,9 +0,0 @@--[SBV] tests/T42.hs:9:1 Proving "f", using Z3.-[Z3] Falsifiable. Counter-example:-  xs_1 = 10 :: Int64-  xs_2 =  0 :: Int64-  xs_3 =  0 :: Int64-  xs_4 =  0 :: Int64-  xs_5 =  0 :: Int64-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
− tests/GoldFiles/T43.hs.golden 
@@ -1,21 +0,0 @@--[SBV] tests/T43.hs:13:1 Proving "t", using Z3.-[Z3] Q.E.D.--[SBV] tests/T43.hs:19:1 Proving "r", using Z3.--[SBV] tests/T43.hs:19:1 Skipping proof. Unsupported case-expression (with-complicated-alternatives-during-merging):-                           case == @ Int $fEqInt x (I# 0) of _ [Occ=Dead] {-  False ->-    (\ _ [Occ=Dead, OS=OneShot] ->-       : @ Int x (: @ Int x (: @ Int x (: @ Int x ([] @ Int)))))-      void#;-  True -> : @ Int x (: @ Int x (: @ Int x ([] @ Int)))-}-                           While Analyzing:-                           Alternatives are producing lists of differing sizes:-                              Length 4: [<symbolic> :: SInt64,- <symbolic> :: SInt64,- <symbolic> :: SInt64,- <symbolic> :: SInt64]-                           vs Length 3: [<symbolic> :: SInt64, <symbolic> :: SInt64, <symbolic> :: SInt64]
− tests/GoldFiles/T44.hs.golden 
@@ -1,9 +0,0 @@--[SBV] tests/T44.hs:12:1 Proving "t", using Z3.-[Z3] Q.E.D.--[SBV] tests/T44.hs:20:1 Proving "r", using Z3.-[Z3] Falsifiable. Counter-example:-  b = False :: Bool-  x =     0 :: Integer-  y =    -1 :: Integer