{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-|
    Module      :  Numeric.MixedType.Bool
    Description :  Bottom-up typed Boolean operations
    Copyright   :  (c) Michal Konecny
    License     :  BSD3

    Maintainer  :  mikkonecny@gmail.com
    Stability   :  experimental
    Portability :  portable

-}
module Numeric.MixedTypes.Bool
(
  IsBool, specIsBool
  -- * Conversion to/from Bool
  , HasBools, CanTestCertainly(..), specCanTestCertainly, CanTestCertainlyX
  , isNotTrue, isNotFalse
  , stronglyImplies, stronglyEquivalentTo
  , weaklyImplies, weaklyEquivalentTo
  -- * Negation
  , CanNeg(..), not, CanNegSameType
  -- ** Tests
  , specCanNegBool
  -- * And and or
  , CanAndOr, CanAndOrAsymmetric(..), (&&), (||), CanAndOrWith, CanAndOrSameType, and, or
  -- ** Tests
  , specCanAndOr, specCanAndOrNotMixed
)
where

import Numeric.MixedTypes.PreludeHiding
import qualified Prelude as P
import Text.Printf

import qualified Data.List as List

import Control.CollectErrors ( CollectErrors, CanBeErrors )
import qualified Control.CollectErrors as CE

import Numeric.MixedTypes.Literals

import Test.Hspec
-- import qualified Test.QuickCheck as QC
import qualified Test.Hspec.SmallCheck as HSC
import qualified Test.SmallCheck as SC
import qualified Test.SmallCheck.Series as SCS
-- import Control.Exception (evaluate)

type HasBools t = (ConvertibleExactly Bool t)

{-|
  Tests for truth or falsity.  Beware, when @isCertainlyTrue@ returns @False@,
  it does not mean that the proposition is false.  It usually means that
  we failed to prove the proposition.
-}
class (HasBools t) => CanTestCertainly t
  where
    isCertainlyTrue :: t -> Bool
    isCertainlyFalse :: t -> Bool

isNotFalse :: (CanTestCertainly t) => t -> Bool
isNotFalse :: forall t. CanTestCertainly t => t -> Bool
isNotFalse = Bool -> Bool
P.not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse

isNotTrue :: (CanTestCertainly t) => t -> Bool
isNotTrue :: forall t. CanTestCertainly t => t -> Bool
isNotTrue = Bool -> Bool
P.not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue

{-|
  If l is certainly True, then r is also certainly True.
-}
stronglyImplies :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
stronglyImplies :: forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
stronglyImplies t1
l t2
r =
  (Bool -> Bool
P.not (forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t1
l) Bool -> Bool -> Bool
P.|| forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t2
r)

{-|
  If l is certainly True, then r is not certainly False.
-}
weaklyImplies :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
weaklyImplies :: forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
weaklyImplies t1
l t2
r =
  (Bool -> Bool
P.not forall a b. (a -> b) -> a -> b
$ forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t1
l) Bool -> Bool -> Bool
P.|| (Bool -> Bool
P.not forall a b. (a -> b) -> a -> b
$ forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t2
r)

stronglyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
stronglyEquivalentTo :: forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
stronglyEquivalentTo t1
l t2
r =
  forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
stronglyImplies t1
l t2
r Bool -> Bool -> Bool
P.&& forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
stronglyImplies t2
r t1
l

weaklyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
weaklyEquivalentTo :: forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
weaklyEquivalentTo t1
l t2
r =
  forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
weaklyImplies t1
l t2
r Bool -> Bool -> Bool
P.&& forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
weaklyImplies t2
r t1
l

{-|
  HSpec properties that each implementation of CanTestCertainly should satisfy.
 -}
specCanTestCertainly :: (CanTestCertainly t) => T t -> Spec
specCanTestCertainly :: forall t. CanTestCertainly t => T t -> Spec
specCanTestCertainly (T String
typeName :: T t) =
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (forall r. PrintfType r => String -> r
printf String
"CanTestCertainly %s" String
typeName) forall a b. (a -> b) -> a -> b
$ do
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"detects True using isCertainlyTrue" forall a b. (a -> b) -> a -> b
$ do
      forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue (forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True :: t) forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe`  Bool
True
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does not detect False using isCertainlyTrue" forall a b. (a -> b) -> a -> b
$ do
      forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue (forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False :: t) forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe`  Bool
False
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"detects False using isCertainlyFalse" forall a b. (a -> b) -> a -> b
$ do
      forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse (forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False :: t) forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe`  Bool
True
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does not detect True using isCertainlyFalse" forall a b. (a -> b) -> a -> b
$ do
      forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse (forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True :: t) forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe`  Bool
False

instance ConvertibleExactly Bool Bool where
  safeConvertExactly :: Bool -> ConvertResult Bool
safeConvertExactly Bool
b = forall a b. b -> Either a b
Right Bool
b

instance CanTestCertainly Bool where
  isCertainlyTrue :: Bool -> Bool
isCertainlyTrue = forall a. a -> a
id
  isCertainlyFalse :: Bool -> Bool
isCertainlyFalse = forall t. CanNeg t => t -> NegType t
not

instance (CanTestCertainly t, CanBeErrors es) => CanTestCertainly (CollectErrors es t) where
  isCertainlyTrue :: CollectErrors es t -> Bool
isCertainlyTrue CollectErrors es t
vCE =
    forall es t v.
CanBeErrors es =>
(es -> t) -> (v -> t) -> CollectErrors es v -> t
CE.withErrorOrValue (forall a b. a -> b -> a
const Bool
False) forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue CollectErrors es t
vCE
  isCertainlyFalse :: CollectErrors es t -> Bool
isCertainlyFalse CollectErrors es t
vCE =
    forall es t v.
CanBeErrors es =>
(es -> t) -> (v -> t) -> CollectErrors es v -> t
CE.withErrorOrValue (forall a b. a -> b -> a
const Bool
False) forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse CollectErrors es t
vCE


{---- Negation ----}

{-|
  This is negation is both the numeric negation as well as the Boolean negation.
  Example of non-standard Boolean negation:

  @
  negate (Just True) = Just False
  @
 -}
class CanNeg t where
  type NegType t
  type NegType t = t
  negate :: t -> NegType t

{-| A synonym of 'negate'. -}
not :: (CanNeg t) => t -> NegType t
not :: forall t. CanNeg t => t -> NegType t
not = forall t. CanNeg t => t -> NegType t
negate

type CanNegSameType t =
  (CanNeg t, NegType t ~ t)

{-| Compound type constraint useful for test definition. -}
type CanTestCertainlyX t = (CanTestCertainly t, Show t, SCS.Serial IO t)

{-|
  HSpec properties that each Boolean implementation of CanNeg should satisfy.
 -}
specCanNegBool ::
  _ => T t -> Spec
specCanNegBool :: T t -> Spec
specCanNegBool (T String
typeName :: T t) =
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (forall r. PrintfType r => String -> r
printf String
"CanNeg %s" String
typeName) forall a b. (a -> b) -> a -> b
$ do
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"ignores double negation" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t
x :: t) -> (forall t. CanNeg t => t -> NegType t
not (forall t. CanNeg t => t -> NegType t
not t
x)) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` t
x
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"negates True to False" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t
x :: t) ->
        (forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t
x) forall (m :: * -> *) c a.
(Testable m c, Testable m a) =>
c -> a -> Property m
SC.==> (forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse (forall t. CanNeg t => t -> NegType t
not t
x))
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"negates False to True" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t
x :: t) ->
        (forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t
x) forall (m :: * -> *) c a.
(Testable m c, Testable m a) =>
c -> a -> Property m
SC.==> (forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue (forall t. CanNeg t => t -> NegType t
not t
x))


instance CanNeg Bool where negate :: Bool -> NegType Bool
negate = Bool -> Bool
P.not

instance
  (CanNeg t, CanBeErrors es)
  =>
  CanNeg (CollectErrors es t) where
  type NegType (CollectErrors es t) = CollectErrors es (NegType t)
  negate :: CollectErrors es t -> NegType (CollectErrors es t)
negate = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. CanNeg t => t -> NegType t
negate

{---- And/Or ----}

type CanAndOr t1 t2 =
  (CanAndOrAsymmetric t1 t2, CanAndOrAsymmetric t2 t1,
   AndOrType t1 t2 ~ AndOrType t2 t1)

{-|
  Binary logical `and' and `or' for generalised Booleans.  For example:

  @
  (Just True) && False = Just False
  (Just (Just True)) || False = (Just (Just True))
  @
 -}
class CanAndOrAsymmetric t1 t2 where
  type AndOrType t1 t2
  and2 :: t1 -> t2 -> AndOrType t1 t2
  or2 :: t1 -> t2 -> AndOrType t1 t2

type CanAndOrWith t1 t2 = (CanAndOr t1 t2, AndOrType t1 t2 ~ t1)
type CanAndOrSameType t = (CanAndOrWith t t)

infixr 3  &&
infixr 2  ||

{-| A synonym of 'and2'. -}
(&&) :: (CanAndOrAsymmetric a b) => a -> b -> AndOrType a b
&& :: forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
(&&) = forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
and2
{-| A synonym of 'or2'. -}
(||) :: (CanAndOrAsymmetric a b) => a -> b -> AndOrType a b
|| :: forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
(||) = forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
or2

and :: (CanAndOrSameType t, CanTestCertainly t) => [t] -> t
and :: forall t. (CanAndOrSameType t, CanTestCertainly t) => [t] -> t
and = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
(&&) (forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True)

or :: (CanAndOrSameType t, CanTestCertainly t) => [t] -> t
or :: forall t. (CanAndOrSameType t, CanTestCertainly t) => [t] -> t
or = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
(||) (forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False)

{-|
  HSpec properties that each implementation of CanAndOr should satisfy.
 -}
specCanAndOr :: _ => T t1 -> T t2 -> T t3 -> Spec
specCanAndOr :: T t1 -> T t2 -> T t3 -> Spec
specCanAndOr (T String
typeName1 ::T t1) (T String
typeName2 :: T t2) (T String
typeName3 :: T t3) =
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (forall r. PrintfType r => String -> r
printf String
"CanAndOr %s %s, CanAndOr %s %s" String
typeName1 String
typeName2 String
typeName2 String
typeName3) forall a b. (a -> b) -> a -> b
$ do
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"has idempotent ||" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) -> (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t1
x) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` t1
x
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"has idempotent &&" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) -> (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t1
x) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` t1
x
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"has commutative ||" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) (t2
y :: t2) -> (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t2
y) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` (t2
y forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t1
x)
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"has commutative &&" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) (t2
y :: t2) -> (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t2
y) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` (t2
y forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t1
x)
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"has associative ||" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) (t2
y :: t2) (t3
z :: t3) ->
                      (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (t2
y forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t3
z)) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` ((t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t2
y) forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t3
z)
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"has associative &&" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) (t2
y :: t2) (t3
z :: t3) ->
                      (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& (t2
y forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t3
z)) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` ((t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t2
y) forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t3
z)
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"distributes || over &&" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) (t2
y :: t2) (t3
z :: t3) ->
                      (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (t2
y forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t3
z)) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` ((t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t2
y) forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t3
z))
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"distributes && over ||" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) (t2
y :: t2) (t3
z :: t3) ->
                      (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& (t2
y forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t3
z)) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` ((t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t2
y) forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t3
z))
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"distributes not over ||" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) (t2
y :: t2) -> (forall t. CanNeg t => t -> NegType t
not (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| t2
y)) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` ((forall t. CanNeg t => t -> NegType t
not t1
x) forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& (forall t. CanNeg t => t -> NegType t
not t2
y))
    forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"distributes not over &&" forall a b. (a -> b) -> a -> b
$ do
      forall a. Testable IO a => a -> Property IO
HSC.property forall a b. (a -> b) -> a -> b
$ \ (t1
x :: t1) (t2
y :: t2) -> (forall t. CanNeg t => t -> NegType t
not (t1
x forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& t2
y)) forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` ((forall t. CanNeg t => t -> NegType t
not t1
x) forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (forall t. CanNeg t => t -> NegType t
not t2
y))

{-|
  HSpec properties that each implementation of CanAndOr should satisfy.
 -}
specCanAndOrNotMixed :: _ => T t -> Spec
specCanAndOrNotMixed :: T t -> Spec
specCanAndOrNotMixed T t
t = forall t1 t2 t3.
(Serial IO t1, Serial IO t2, Serial IO t3, Show t1, Show t2,
 Show t3, Show (AndOrType t2 t1), Show (AndOrType t1 t1),
 Show (AndOrType t1 t2), Show (AndOrType t1 (AndOrType t2 t3)),
 Show (AndOrType (AndOrType t1 t2) t3),
 Show (AndOrType (AndOrType t1 t2) (AndOrType t1 t3)),
 Show (AndOrType (NegType t1) (NegType t2)),
 Show (NegType (AndOrType t1 t2)), CanTestCertainly t1,
 CanTestCertainly (AndOrType t2 t1),
 CanTestCertainly (AndOrType t1 t1),
 CanTestCertainly (AndOrType t1 t2),
 CanTestCertainly (AndOrType t1 (AndOrType t2 t3)),
 CanTestCertainly (AndOrType (AndOrType t1 t2) t3),
 CanTestCertainly (AndOrType (AndOrType t1 t2) (AndOrType t1 t3)),
 CanTestCertainly (AndOrType (NegType t1) (NegType t2)),
 CanTestCertainly (NegType (AndOrType t1 t2)),
 CanAndOrAsymmetric t2 t1, CanAndOrAsymmetric t2 t3,
 CanAndOrAsymmetric t1 t1, CanAndOrAsymmetric t1 t2,
 CanAndOrAsymmetric t1 t3, CanAndOrAsymmetric t1 (AndOrType t2 t3),
 CanAndOrAsymmetric (AndOrType t1 t2) t3,
 CanAndOrAsymmetric (AndOrType t1 t2) (AndOrType t1 t3),
 CanAndOrAsymmetric (NegType t1) (NegType t2), CanNeg t1, CanNeg t2,
 CanNeg (AndOrType t1 t2)) =>
T t1 -> T t2 -> T t3 -> Spec
specCanAndOr T t
t T t
t T t
t

instance CanAndOrAsymmetric Bool Bool where
  type AndOrType Bool Bool = Bool
  and2 :: Bool -> Bool -> AndOrType Bool Bool
and2 = Bool -> Bool -> Bool
(P.&&)
  or2 :: Bool -> Bool -> AndOrType Bool Bool
or2 = Bool -> Bool -> Bool
(P.||)

instance
  (CanAndOrAsymmetric t1 t2, CanBeErrors es,
  HasBools t2, CanTestCertainly t1)
  =>
  CanAndOrAsymmetric (CollectErrors es t1) (CollectErrors es t2)
  where
  type AndOrType (CollectErrors es t1) (CollectErrors es t2) = CollectErrors es (AndOrType t1 t2)
  and2 :: CollectErrors es t1
-> CollectErrors es t2
-> AndOrType (CollectErrors es t1) (CollectErrors es t2)
and2 CollectErrors es t1
b1CE (CollectErrors es t2
b2CE::b2T) = 
    case CollectErrors es t1
b1CE of
      CE.CollectErrors (Just t1
b1) es
_ | forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t1
b1 -> 
        forall es a b c.
Monoid es =>
(a -> b -> c)
-> CollectErrors es a -> CollectErrors es b -> CollectErrors es c
CE.lift2 forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
and2 CollectErrors es t1
b1CE (forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False :: b2T) -- avoid evaluating b2CE
      CollectErrors es t1
_ -> forall es a b c.
Monoid es =>
(a -> b -> c)
-> CollectErrors es a -> CollectErrors es b -> CollectErrors es c
CE.lift2 forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
and2 CollectErrors es t1
b1CE CollectErrors es t2
b2CE
  or2 :: CollectErrors es t1
-> CollectErrors es t2
-> AndOrType (CollectErrors es t1) (CollectErrors es t2)
or2 CollectErrors es t1
b1CE (CollectErrors es t2
b2CE::b2T) = 
    case CollectErrors es t1
b1CE of
      CE.CollectErrors (Just t1
b1) es
_ | forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t1
b1 -> 
        forall es a b c.
Monoid es =>
(a -> b -> c)
-> CollectErrors es a -> CollectErrors es b -> CollectErrors es c
CE.lift2 forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
or2 CollectErrors es t1
b1CE (forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True :: b2T) -- avoid evaluating b2CE
      CollectErrors es t1
_ -> forall es a b c.
Monoid es =>
(a -> b -> c)
-> CollectErrors es a -> CollectErrors es b -> CollectErrors es c
CE.lift2 forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
or2 CollectErrors es t1
b1CE CollectErrors es t2
b2CE

instance
  (CanAndOrAsymmetric t1 Bool, CanBeErrors es)
  =>
  CanAndOrAsymmetric (CollectErrors es t1) Bool
  where
  type AndOrType (CollectErrors es t1) Bool = CollectErrors es (AndOrType t1 Bool)
  and2 :: CollectErrors es t1 -> Bool -> AndOrType (CollectErrors es t1) Bool
and2 = forall es a b c.
Monoid es =>
(a -> b -> c) -> CollectErrors es a -> b -> CollectErrors es c
CE.lift1T forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
and2
  or2 :: CollectErrors es t1 -> Bool -> AndOrType (CollectErrors es t1) Bool
or2 = forall es a b c.
Monoid es =>
(a -> b -> c) -> CollectErrors es a -> b -> CollectErrors es c
CE.lift1T forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
or2

instance
  (CanAndOrAsymmetric Bool t2, CanBeErrors es)
  =>
  CanAndOrAsymmetric Bool (CollectErrors es t2)
  where
  type AndOrType Bool (CollectErrors es t2) = CollectErrors es (AndOrType Bool t2)
  and2 :: Bool -> CollectErrors es t2 -> AndOrType Bool (CollectErrors es t2)
and2 = forall es a b c.
Monoid es =>
(a -> b -> c) -> a -> CollectErrors es b -> CollectErrors es c
CE.liftT1 forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
and2
  or2 :: Bool -> CollectErrors es t2 -> AndOrType Bool (CollectErrors es t2)
or2 = forall es a b c.
Monoid es =>
(a -> b -> c) -> a -> CollectErrors es b -> CollectErrors es c
CE.liftT1 forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
or2

{-|
  A type constraint synonym that stipulates that the type behaves very
  much like Bool, except it does not necessarily satisfy the law of excluded middle,
  which means that the type can contain a "do-not-know" value or an error.

  Examples: @Bool@, @Kleenean@, @CollectErrors Bool@
-}
type IsBool t =
  (HasBools t, CanNegSameType t, CanAndOrSameType t)

{-|
  HSpec properties that each implementation of IsBool should satisfy.
 -}
specIsBool :: (IsBool t, CanTestCertainly t, Show t, SCS.Serial IO t) => T t -> Spec
specIsBool :: forall t.
(IsBool t, CanTestCertainly t, Show t, Serial IO t) =>
T t -> Spec
specIsBool t :: T t
t@(T String
typeName :: T t) =
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (forall r. PrintfType r => String -> r
printf String
"IsBool %s" String
typeName) forall a b. (a -> b) -> a -> b
$ do
    forall t. CanTestCertainly t => T t -> Spec
specCanTestCertainly T t
t
    forall t.
(CanTestCertainly t, CanTestCertainly (NegType t),
 CanTestCertainly (NegType (NegType t)), Serial IO t, Show t,
 Show (NegType (NegType t)), CanNeg t, CanNeg (NegType t)) =>
T t -> Spec
specCanNegBool T t
t
    forall t.
(Serial IO t, Show t, Show (AndOrType t t),
 Show (AndOrType t (AndOrType t t)),
 Show (AndOrType (AndOrType t t) t),
 Show (AndOrType (AndOrType t t) (AndOrType t t)),
 Show (AndOrType (NegType t) (NegType t)),
 Show (NegType (AndOrType t t)), CanTestCertainly t,
 CanTestCertainly (AndOrType t t),
 CanTestCertainly (AndOrType t (AndOrType t t)),
 CanTestCertainly (AndOrType (AndOrType t t) t),
 CanTestCertainly (AndOrType (AndOrType t t) (AndOrType t t)),
 CanTestCertainly (AndOrType (NegType t) (NegType t)),
 CanTestCertainly (NegType (AndOrType t t)), CanAndOrAsymmetric t t,
 CanAndOrAsymmetric t (AndOrType t t),
 CanAndOrAsymmetric (AndOrType t t) t,
 CanAndOrAsymmetric (AndOrType t t) (AndOrType t t),
 CanAndOrAsymmetric (NegType t) (NegType t), CanNeg t,
 CanNeg (AndOrType t t)) =>
T t -> Spec
specCanAndOrNotMixed T t
t

scEquals ::
  (Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
  t1 -> t2 -> Either String String
scEquals :: forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
scEquals t1
l t2
r
  | t1
l forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
`stronglyEquivalentTo` t2
r = forall a b. b -> Either a b
Right String
"OK"
  | Bool
otherwise = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"(%s) /= (%s)" (forall a. Show a => a -> String
show t1
l) (forall a. Show a => a -> String
show t2
r)