    -----------------------------------------------------------------------------
    -- |
    -- 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 :: (?loc::CallStack) => 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)