{-|
    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 Numeric.CollectErrors
import Control.CollectErrors

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 :: t -> Bool
isNotFalse = Bool -> Bool
P.not (Bool -> Bool) -> (t -> Bool) -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse

isNotTrue :: (CanTestCertainly t) => t -> Bool
isNotTrue :: t -> Bool
isNotTrue = Bool -> Bool
P.not (Bool -> Bool) -> (t -> Bool) -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Bool
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 :: t1 -> t2 -> Bool
stronglyImplies t1
l t2
r =
  (Bool -> Bool
P.not (t1 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t1
l) Bool -> Bool -> Bool
P.|| t2 -> Bool
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 :: t1 -> t2 -> Bool
weaklyImplies t1
l t2
r =
  (Bool -> Bool
P.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ t1 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t1
l) Bool -> Bool -> Bool
P.|| (Bool -> Bool
P.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ t2 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t2
r)

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

weaklyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool
weaklyEquivalentTo :: t1 -> t2 -> Bool
weaklyEquivalentTo t1
l t2
r =
  t1 -> t2 -> Bool
forall t1 t2.
(CanTestCertainly t1, CanTestCertainly t2) =>
t1 -> t2 -> Bool
weaklyImplies t1
l t2
r Bool -> Bool -> Bool
P.&& t2 -> t1 -> Bool
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 :: T t -> Spec
specCanTestCertainly (T String
typeName :: T t) =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"CanTestCertainly %s" String
typeName) (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Expectation -> SpecWith (Arg Expectation)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"detects True using isCertainlyTrue" (Expectation -> SpecWith (Arg Expectation))
-> Expectation -> SpecWith (Arg Expectation)
forall a b. (a -> b) -> a -> b
$ do
      t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue (Bool -> t
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True :: t) Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe`  Bool
True
    String -> Expectation -> SpecWith (Arg Expectation)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does not detect False using isCertainlyTrue" (Expectation -> SpecWith (Arg Expectation))
-> Expectation -> SpecWith (Arg Expectation)
forall a b. (a -> b) -> a -> b
$ do
      t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue (Bool -> t
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False :: t) Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe`  Bool
False
    String -> Expectation -> SpecWith (Arg Expectation)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"detects False using isCertainlyFalse" (Expectation -> SpecWith (Arg Expectation))
-> Expectation -> SpecWith (Arg Expectation)
forall a b. (a -> b) -> a -> b
$ do
      t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse (Bool -> t
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False :: t) Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe`  Bool
True
    String -> Expectation -> SpecWith (Arg Expectation)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does not detect True using isCertainlyFalse" (Expectation -> SpecWith (Arg Expectation))
-> Expectation -> SpecWith (Arg Expectation)
forall a b. (a -> b) -> a -> b
$ do
      t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse (Bool -> t
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True :: t) Bool -> Bool -> Expectation
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 = Bool -> ConvertResult Bool
forall a b. b -> Either a b
Right Bool
b

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

instance (ConvertibleExactly Bool t) => ConvertibleExactly Bool (Maybe t) where
  safeConvertExactly :: Bool -> ConvertResult (Maybe t)
safeConvertExactly Bool
b =
    case (Bool -> ConvertResult t
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> ConvertResult t2
safeConvertExactly Bool
b) of
      Left ConvertError
_ -> Maybe t -> ConvertResult (Maybe t)
forall a b. b -> Either a b
Right Maybe t
forall a. Maybe a
Nothing
      Right t
r -> Maybe t -> ConvertResult (Maybe t)
forall a b. b -> Either a b
Right (t -> Maybe t
forall a. a -> Maybe a
Just t
r)

instance (CanTestCertainly t) => CanTestCertainly (Maybe t) where
  isCertainlyTrue :: Maybe t -> Bool
isCertainlyTrue (Just t
b) = t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t
b
  isCertainlyTrue Maybe t
_ = Bool
False
  isCertainlyFalse :: Maybe t -> Bool
isCertainlyFalse (Just t
b) = t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t
b
  isCertainlyFalse Maybe t
_ = Bool
False

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


{---- 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 :: t -> NegType t
not = t -> NegType t
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 ::
  (Show t, Show (NegType (NegType t)), SCS.Serial IO t,
   CanTestCertainly t, CanTestCertainly (NegType t),
   CanTestCertainly (NegType (NegType t)), CanNeg t,
   CanNeg (NegType t))
  =>
  T t -> Spec
specCanNegBool :: T t -> Spec
specCanNegBool (T String
typeName :: T t) =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"CanNeg %s" String
typeName) (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property IO -> SpecWith (Arg (Property IO))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"ignores double negation" (Property IO -> SpecWith (Arg (Property IO)))
-> Property IO -> SpecWith (Arg (Property IO))
forall a b. (a -> b) -> a -> b
$ do
      (t -> Either String String) -> Property IO
forall a. Testable IO a => a -> Property IO
HSC.property ((t -> Either String String) -> Property IO)
-> (t -> Either String String) -> Property IO
forall a b. (a -> b) -> a -> b
$ \ (t
x :: t) -> (NegType t -> NegType (NegType t)
forall t. CanNeg t => t -> NegType t
not (t -> NegType t
forall t. CanNeg t => t -> NegType t
not t
x)) NegType (NegType t) -> t -> Either String String
forall t1 t2.
(Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) =>
t1 -> t2 -> Either String String
`scEquals` t
x
    String -> Property IO -> SpecWith (Arg (Property IO))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"negates True to False" (Property IO -> SpecWith (Arg (Property IO)))
-> Property IO -> SpecWith (Arg (Property IO))
forall a b. (a -> b) -> a -> b
$ do
      (t -> Property IO) -> Property IO
forall a. Testable IO a => a -> Property IO
HSC.property ((t -> Property IO) -> Property IO)
-> (t -> Property IO) -> Property IO
forall a b. (a -> b) -> a -> b
$ \ (t
x :: t) ->
        (t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t
x) Bool -> Bool -> Property IO
forall (m :: * -> *) c a.
(Testable m c, Testable m a) =>
c -> a -> Property m
SC.==> (NegType t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse (t -> NegType t
forall t. CanNeg t => t -> NegType t
not t
x))
    String -> Property IO -> SpecWith (Arg (Property IO))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"negates False to True" (Property IO -> SpecWith (Arg (Property IO)))
-> Property IO -> SpecWith (Arg (Property IO))
forall a b. (a -> b) -> a -> b
$ do
      (t -> Property IO) -> Property IO
forall a. Testable IO a => a -> Property IO
HSC.property ((t -> Property IO) -> Property IO)
-> (t -> Property IO) -> Property IO
forall a b. (a -> b) -> a -> b
$ \ (t
x :: t) ->
        (t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t
x) Bool -> Bool -> Property IO
forall (m :: * -> *) c a.
(Testable m c, Testable m a) =>
c -> a -> Property m
SC.==> (NegType t -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue (t -> NegType t
forall t. CanNeg t => t -> NegType t
not t
x))


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

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

_testNeg1 :: Maybe Bool
_testNeg1 :: Maybe Bool
_testNeg1 = Maybe Bool -> NegType (Maybe Bool)
forall t. CanNeg t => t -> NegType t
not (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)

instance
  (CanNeg t, SuitableForCE es, CanEnsureCE es t, CanEnsureCE es (NegType t))
  =>
  CanNeg (CollectErrors es t) where
  type NegType (CollectErrors es t) = EnsureCE es (NegType t)
  negate :: CollectErrors es t -> NegType (CollectErrors es t)
negate = (t -> NegType t) -> CollectErrors es t -> EnsureCE es (NegType t)
forall es a c.
(SuitableForCE es, CanEnsureCE es a, CanEnsureCE es c) =>
(a -> c) -> CollectErrors es a -> EnsureCE es c
lift1CE t -> NegType t
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
&& :: a -> b -> AndOrType a b
(&&) = a -> b -> AndOrType a b
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
{-| A synonym of 'or2'. -}
(||) :: (CanAndOrAsymmetric a b) => a -> b -> AndOrType a b
|| :: a -> b -> AndOrType a b
(||) = a -> b -> AndOrType a b
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2

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

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

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

{-|
  HSpec properties that each implementation of CanAndOr should satisfy.
 -}
specCanAndOrNotMixed ::
  (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 (NegType (AndOrType t t)),
   Show (AndOrType (NegType t) (NegType t)), SCS.Serial IO 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 (NegType (AndOrType t t)),
   CanTestCertainly (AndOrType (NegType t) (NegType t)), CanNeg t,
   CanNeg (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))
  =>
  T t -> Spec
specCanAndOrNotMixed :: T t -> Spec
specCanAndOrNotMixed T t
t = T t -> T t -> T t -> Spec
forall t1 t2 t3.
(Show t1, Show t2, Show t3, Show (AndOrType t1 t1),
 Show (AndOrType t1 t2), Show (AndOrType t2 t1),
 Show (AndOrType t1 (AndOrType t2 t3)),
 Show (AndOrType (AndOrType t1 t2) t3),
 Show (AndOrType (AndOrType t1 t2) (AndOrType t1 t3)),
 Show (NegType (AndOrType t1 t2)),
 Show (AndOrType (NegType t1) (NegType t2)), Serial IO t1,
 Serial IO t2, Serial IO t3, CanTestCertainly t1,
 CanTestCertainly (AndOrType t1 t1),
 CanTestCertainly (AndOrType t1 t2),
 CanTestCertainly (AndOrType t2 t1),
 CanTestCertainly (AndOrType t1 (AndOrType t2 t3)),
 CanTestCertainly (AndOrType (AndOrType t1 t2) t3),
 CanTestCertainly (AndOrType (AndOrType t1 t2) (AndOrType t1 t3)),
 CanTestCertainly (NegType (AndOrType t1 t2)),
 CanTestCertainly (AndOrType (NegType t1) (NegType t2)), CanNeg t1,
 CanNeg t2, CanNeg (AndOrType t1 t2), CanAndOrAsymmetric t1 t1,
 CanAndOrAsymmetric t1 t2, CanAndOrAsymmetric t1 t3,
 CanAndOrAsymmetric t1 (AndOrType t2 t3), CanAndOrAsymmetric t2 t1,
 CanAndOrAsymmetric t2 t3, CanAndOrAsymmetric (AndOrType t1 t2) t3,
 CanAndOrAsymmetric (AndOrType t1 t2) (AndOrType t1 t3),
 CanAndOrAsymmetric (NegType t1) (NegType 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
Bool -> Bool -> AndOrType Bool Bool
(P.&&)
  or2 :: Bool -> Bool -> AndOrType Bool Bool
or2 = Bool -> Bool -> Bool
Bool -> Bool -> AndOrType Bool Bool
(P.||)

instance (CanAndOrAsymmetric t1 t2, CanTestCertainly t1, CanTestCertainly t2, CanTestCertainly (AndOrType t1 t2)) =>
  CanAndOrAsymmetric (Maybe t1) (Maybe t2)
  where
  type AndOrType (Maybe t1) (Maybe t2) = Maybe (AndOrType t1 t2)
  and2 :: Maybe t1 -> Maybe t2 -> AndOrType (Maybe t1) (Maybe t2)
and2 (Just t1
b1) Maybe t2
_ | t1 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t1
b1 = AndOrType t1 t2 -> Maybe (AndOrType t1 t2)
forall a. a -> Maybe a
Just (Bool -> AndOrType t1 t2
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False)
  and2 Maybe t1
_ (Just t2
b2) | t2 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t2
b2 = AndOrType t1 t2 -> Maybe (AndOrType t1 t2)
forall a. a -> Maybe a
Just (Bool -> AndOrType t1 t2
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False)
  and2 (Just t1
b1) (Just t2
b2) = AndOrType t1 t2 -> Maybe (AndOrType t1 t2)
forall a. a -> Maybe a
Just (t1
b1 t1 -> t2 -> AndOrType t1 t2
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
&& t2
b2)
  and2 Maybe t1
_ Maybe t2
_ = AndOrType (Maybe t1) (Maybe t2)
forall a. Maybe a
Nothing
  or2 :: Maybe t1 -> Maybe t2 -> AndOrType (Maybe t1) (Maybe t2)
or2 (Just t1
b1) Maybe t2
_ | t1 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t1
b1 = AndOrType t1 t2 -> Maybe (AndOrType t1 t2)
forall a. a -> Maybe a
Just (Bool -> AndOrType t1 t2
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True)
  or2 Maybe t1
_ (Just t2
b2) | t2 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t2
b2 = AndOrType t1 t2 -> Maybe (AndOrType t1 t2)
forall a. a -> Maybe a
Just (Bool -> AndOrType t1 t2
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True)
  or2 (Just t1
b1) (Just t2
b2) = AndOrType t1 t2 -> Maybe (AndOrType t1 t2)
forall a. a -> Maybe a
Just (t1
b1 t1 -> t2 -> AndOrType t1 t2
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
|| t2
b2)
  or2 Maybe t1
_ Maybe t2
_ = AndOrType (Maybe t1) (Maybe t2)
forall a. Maybe a
Nothing

instance (CanAndOrAsymmetric Bool t2, CanTestCertainly t2, CanTestCertainly (AndOrType Bool t2)) =>
  CanAndOrAsymmetric Bool (Maybe t2)
  where
  type AndOrType Bool (Maybe t2) = Maybe (AndOrType Bool t2)
  and2 :: Bool -> Maybe t2 -> AndOrType Bool (Maybe t2)
and2 Bool
False Maybe t2
_ = AndOrType Bool t2 -> Maybe (AndOrType Bool t2)
forall a. a -> Maybe a
Just (Bool -> AndOrType Bool t2
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False)
  and2 Bool
_ (Just t2
b2) | t2 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t2
b2 = AndOrType Bool t2 -> Maybe (AndOrType Bool t2)
forall a. a -> Maybe a
Just (Bool -> AndOrType Bool t2
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False)
  and2 Bool
b1 (Just t2
b2) = AndOrType Bool t2 -> Maybe (AndOrType Bool t2)
forall a. a -> Maybe a
Just (Bool
b1 Bool -> t2 -> AndOrType Bool t2
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
&& t2
b2)
  and2 Bool
_ Maybe t2
_ = AndOrType Bool (Maybe t2)
forall a. Maybe a
Nothing
  or2 :: Bool -> Maybe t2 -> AndOrType Bool (Maybe t2)
or2 Bool
True Maybe t2
_ = AndOrType Bool t2 -> Maybe (AndOrType Bool t2)
forall a. a -> Maybe a
Just (Bool -> AndOrType Bool t2
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True)
  or2 Bool
_ (Just t2
b2) | t2 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t2
b2 = AndOrType Bool t2 -> Maybe (AndOrType Bool t2)
forall a. a -> Maybe a
Just (Bool -> AndOrType Bool t2
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True)
  or2 Bool
b1 (Just t2
b2) = AndOrType Bool t2 -> Maybe (AndOrType Bool t2)
forall a. a -> Maybe a
Just (Bool
b1 Bool -> t2 -> AndOrType Bool t2
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
|| t2
b2)
  or2 Bool
_ Maybe t2
_ = AndOrType Bool (Maybe t2)
forall a. Maybe a
Nothing

instance (CanAndOrAsymmetric t1 Bool, CanTestCertainly t1, CanTestCertainly (AndOrType t1 Bool)) =>
  CanAndOrAsymmetric (Maybe t1) Bool
  where
  type AndOrType (Maybe t1) Bool = Maybe (AndOrType t1 Bool)
  and2 :: Maybe t1 -> Bool -> AndOrType (Maybe t1) Bool
and2 Maybe t1
_ Bool
False = AndOrType t1 Bool -> Maybe (AndOrType t1 Bool)
forall a. a -> Maybe a
Just (Bool -> AndOrType t1 Bool
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False)
  and2 (Just t1
b1) Bool
_ | t1 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyFalse t1
b1 = AndOrType t1 Bool -> Maybe (AndOrType t1 Bool)
forall a. a -> Maybe a
Just (Bool -> AndOrType t1 Bool
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
False)
  and2 (Just t1
b1) Bool
b2 = AndOrType t1 Bool -> Maybe (AndOrType t1 Bool)
forall a. a -> Maybe a
Just (t1
b1 t1 -> Bool -> AndOrType t1 Bool
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
&& Bool
b2)
  and2 Maybe t1
_ Bool
_ = AndOrType (Maybe t1) Bool
forall a. Maybe a
Nothing
  or2 :: Maybe t1 -> Bool -> AndOrType (Maybe t1) Bool
or2 Maybe t1
_ Bool
True = AndOrType t1 Bool -> Maybe (AndOrType t1 Bool)
forall a. a -> Maybe a
Just (Bool -> AndOrType t1 Bool
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True)
  or2 (Just t1
b1) Bool
_ | t1 -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue t1
b1 = AndOrType t1 Bool -> Maybe (AndOrType t1 Bool)
forall a. a -> Maybe a
Just (Bool -> AndOrType t1 Bool
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Bool
True)
  or2 (Just t1
b1) Bool
b2 = AndOrType t1 Bool -> Maybe (AndOrType t1 Bool)
forall a. a -> Maybe a
Just (t1
b1 t1 -> Bool -> AndOrType t1 Bool
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
|| Bool
b2)
  or2 Maybe t1
_ Bool
_ = AndOrType (Maybe t1) Bool
forall a. Maybe a
Nothing

_testAndOr1 :: Maybe Bool
_testAndOr1 :: Maybe Bool
_testAndOr1 = (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) Maybe Bool -> Bool -> AndOrType (Maybe Bool) Bool
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
&& Bool
False

_testAndOr2 :: Maybe (Maybe Bool)
_testAndOr2 :: Maybe (Maybe Bool)
_testAndOr2 = (Maybe Bool -> Maybe (Maybe Bool)
forall a. a -> Maybe a
Just (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)) Maybe (Maybe Bool) -> Bool -> AndOrType (Maybe (Maybe Bool)) Bool
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
|| Bool
False

_testAndOr3 :: Maybe Bool
_testAndOr3 :: Maybe Bool
_testAndOr3 = [Maybe Bool] -> Maybe Bool
forall t. (CanAndOrSameType t, CanTestCertainly t) => [t] -> t
and [Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, Maybe Bool
forall a. Maybe a
Nothing, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False]

instance
  (CanAndOrAsymmetric t1 t2, SuitableForCE es
  , CanEnsureCE es t1, CanEnsureCE es t2, CanEnsureCE es (AndOrType t1 t2))
  =>
  CanAndOrAsymmetric (CollectErrors es t1) (CollectErrors es t2)
  where
  type AndOrType (CollectErrors es t1) (CollectErrors es t2) = EnsureCE es (AndOrType t1 t2)
  and2 :: CollectErrors es t1
-> CollectErrors es t2
-> AndOrType (CollectErrors es t1) (CollectErrors es t2)
and2 = (t1 -> t2 -> AndOrType t1 t2)
-> CollectErrors es t1
-> CollectErrors es t2
-> EnsureCE es (AndOrType t1 t2)
forall es a b c.
(SuitableForCE es, CanEnsureCE es a, CanEnsureCE es b,
 CanEnsureCE es c) =>
(a -> b -> c)
-> CollectErrors es a -> CollectErrors es b -> EnsureCE es c
lift2CE t1 -> t2 -> AndOrType t1 t2
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: CollectErrors es t1
-> CollectErrors es t2
-> AndOrType (CollectErrors es t1) (CollectErrors es t2)
or2 = (t1 -> t2 -> AndOrType t1 t2)
-> CollectErrors es t1
-> CollectErrors es t2
-> EnsureCE es (AndOrType t1 t2)
forall es a b c.
(SuitableForCE es, CanEnsureCE es a, CanEnsureCE es b,
 CanEnsureCE es c) =>
(a -> b -> c)
-> CollectErrors es a -> CollectErrors es b -> EnsureCE es c
lift2CE t1 -> t2 -> AndOrType t1 t2
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2

instance
  (CanAndOrAsymmetric t1 Bool, SuitableForCE es
  , CanEnsureCE es t1, CanEnsureCE es (AndOrType t1 Bool))
  =>
  CanAndOrAsymmetric (CollectErrors es t1) Bool
  where
  type AndOrType (CollectErrors es t1) Bool = EnsureCE es (AndOrType t1 Bool)
  and2 :: CollectErrors es t1 -> Bool -> AndOrType (CollectErrors es t1) Bool
and2 = (t1 -> Bool -> AndOrType t1 Bool)
-> CollectErrors es t1 -> Bool -> EnsureCE es (AndOrType t1 Bool)
forall es a c b.
(SuitableForCE es, CanEnsureCE es a, CanEnsureCE es c) =>
(a -> b -> c) -> CollectErrors es a -> b -> EnsureCE es c
lift2TCE t1 -> Bool -> AndOrType t1 Bool
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: CollectErrors es t1 -> Bool -> AndOrType (CollectErrors es t1) Bool
or2 = (t1 -> Bool -> AndOrType t1 Bool)
-> CollectErrors es t1 -> Bool -> EnsureCE es (AndOrType t1 Bool)
forall es a c b.
(SuitableForCE es, CanEnsureCE es a, CanEnsureCE es c) =>
(a -> b -> c) -> CollectErrors es a -> b -> EnsureCE es c
lift2TCE t1 -> Bool -> AndOrType t1 Bool
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2

instance
  (CanAndOrAsymmetric Bool t2, SuitableForCE es
  , CanEnsureCE es t2, CanEnsureCE es (AndOrType Bool t2))
  =>
  CanAndOrAsymmetric Bool (CollectErrors es t2)
  where
  type AndOrType Bool (CollectErrors es t2) = EnsureCE es (AndOrType Bool t2)
  and2 :: Bool -> CollectErrors es t2 -> AndOrType Bool (CollectErrors es t2)
and2 = (Bool -> t2 -> AndOrType Bool t2)
-> Bool -> CollectErrors es t2 -> EnsureCE es (AndOrType Bool t2)
forall es b c a.
(SuitableForCE es, CanEnsureCE es b, CanEnsureCE es c) =>
(a -> b -> c) -> a -> CollectErrors es b -> EnsureCE es c
lift2TLCE Bool -> t2 -> AndOrType Bool t2
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: Bool -> CollectErrors es t2 -> AndOrType Bool (CollectErrors es t2)
or2 = (Bool -> t2 -> AndOrType Bool t2)
-> Bool -> CollectErrors es t2 -> EnsureCE es (AndOrType Bool t2)
forall es b c a.
(SuitableForCE es, CanEnsureCE es b, CanEnsureCE es c) =>
(a -> b -> c) -> a -> CollectErrors es b -> EnsureCE es c
lift2TLCE Bool -> t2 -> AndOrType Bool t2
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
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.

  Examples: @Bool@, @Maybe Bool@, @Maybe (Maybe Bool)@, @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 :: T t -> Spec
specIsBool t :: T t
t@(T String
typeName :: T t) =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"IsBool %s" String
typeName) (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    T t -> Spec
forall t. CanTestCertainly t => T t -> Spec
specCanTestCertainly T t
t
    T t -> Spec
forall t.
(Show t, Show (NegType (NegType t)), Serial IO t,
 CanTestCertainly t, CanTestCertainly (NegType t),
 CanTestCertainly (NegType (NegType t)), CanNeg t,
 CanNeg (NegType t)) =>
T t -> Spec
specCanNegBool T t
t
    T t -> Spec
forall 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 (NegType (AndOrType t t)),
 Show (AndOrType (NegType t) (NegType t)), Serial IO 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 (NegType (AndOrType t t)),
 CanTestCertainly (AndOrType (NegType t) (NegType t)), CanNeg t,
 CanNeg (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)) =>
T t -> Spec
specCanAndOrNotMixed T t
t

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