-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.NoDiv0
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates SBV's assertion checking facilities
-----------------------------------------------------------------------------

{-# LANGUAGE ImplicitParams #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Misc.NoDiv0 where

import Data.SBV
import GHC.Stack

-- | A simple variant of division, where we explicitly require the
-- caller to make sure the divisor is not 0.
checkedDiv :: (?loc :: CallStack) => SInt32 -> SInt32 -> SInt32
checkedDiv :: SInt32 -> SInt32 -> SInt32
checkedDiv SInt32
x SInt32
y = Maybe CallStack -> String -> SBool -> SInt32 -> SInt32
forall a.
HasKind a =>
Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert (CallStack -> Maybe CallStack
forall a. a -> Maybe a
Just ?loc::CallStack
CallStack
?loc)
                         String
"Divisor should not be 0"
                         (SInt32
y SInt32 -> SInt32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInt32
0)
                         (SInt32
x SInt32 -> SInt32 -> SInt32
forall a. SDivisible a => a -> a -> a
`sDiv` SInt32
y)

-- | Check whether an arbitrary call to 'checkedDiv' is safe. Clearly, we do not expect
-- this to be safe:
--
-- >>> test1
-- [./Documentation/SBV/Examples/Misc/NoDiv0.hs:38:14:checkedDiv: Divisor should not be 0: Violated. Model:
--   s0 = 0 :: Int32
--   s1 = 0 :: Int32]
--
test1 :: IO [SafeResult]
test1 :: IO [SafeResult]
test1 = (SInt32 -> SInt32 -> SInt32) -> IO [SafeResult]
forall a. SExecutable IO a => a -> IO [SafeResult]
safe (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
SInt32 -> SInt32 -> SInt32
checkedDiv

-- | Repeat the test, except this time we explicitly protect against the bad case. We have:
--
-- >>> test2
-- [./Documentation/SBV/Examples/Misc/NoDiv0.hs:46:41:checkedDiv: Divisor should not be 0: No violations detected]
--
test2 :: IO [SafeResult]
test2 :: IO [SafeResult]
test2 = (SInt32 -> SInt32 -> SInt32) -> IO [SafeResult]
forall a. SExecutable IO a => a -> IO [SafeResult]
safe ((SInt32 -> SInt32 -> SInt32) -> IO [SafeResult])
-> (SInt32 -> SInt32 -> SInt32) -> IO [SafeResult]
forall a b. (a -> b) -> a -> b
$ \SInt32
x SInt32
y -> SBool -> SInt32 -> SInt32 -> SInt32
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInt32
y SInt32 -> SInt32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInt32
0) SInt32
3 ((?loc::CallStack) => SInt32 -> SInt32 -> SInt32
SInt32 -> SInt32 -> SInt32
checkedDiv SInt32
x SInt32
y)