-----------------------------------------------------------------------------
-- |
-- 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 #-}

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 x y = sAssert (Just ?loc)
                         "Divisor should not be 0"
                         (y ./= 0)
                         (x `sDiv` 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:36:14:checkedDiv: Divisor should not be 0: Violated. Model:
--   s0 = 0 :: Int32
--   s1 = 0 :: Int32]
--
test1 :: IO [SafeResult]
test1 = safe checkedDiv

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