{-|

Copyright   : © 2020 Alex Washburn
License     : BSD-3-Clause
Maintainer  : github@recursion.ninja
Stability   : Stable

-}

{-# Language DeriveAnyClass #-}
{-# Language DeriveDataTypeable #-}
{-# Language DeriveGeneric #-}
{-# Language DerivingStrategies #-}
{-# Language FlexibleInstances #-}
{-# Language MultiParamTypeClasses #-}
{-# Language Safe #-}

module Operator.Binary.Logical
    ( BinaryLogicalOperator ()
    , fromBinaryLogicalFunction
    , getBinaryLogicalOperator
    , getBinaryLogicalSymbol
    ) where

import Control.DeepSeq
import Data.Data
import Data.Monoid ()
import GHC.Generics
import Test.QuickCheck hiding (generate)
import Test.SmallCheck.Series


{-|
Representation of all possible /binary/ operators of type @(Bool -> Bool -> Bool)@.
Useful for both property and enumeration based testing.
-}
data BinaryLogicalOperator
    = AlwaysFalse
    | LogicalNOR
    | ConverseNonImplication
    | NotFirstArgument
    | NonImplication
    | NotSecondArgument
    | LogicalXOR
    | LogicalNAND
    | LogicalAND
    | LogicalXNOR
    | SecondArgument
    | Implication
    | FirstArgument
    | ConverseImplication
    | LogicalOR
    | AlwaysTrue
    deriving anyclass (BinaryLogicalOperator -> ()
(BinaryLogicalOperator -> ()) -> NFData BinaryLogicalOperator
forall a. (a -> ()) -> NFData a
$crnf :: BinaryLogicalOperator -> ()
rnf :: BinaryLogicalOperator -> ()
NFData)
    deriving stock (Typeable BinaryLogicalOperator
Typeable BinaryLogicalOperator =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> BinaryLogicalOperator
 -> c BinaryLogicalOperator)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BinaryLogicalOperator)
-> (BinaryLogicalOperator -> Constr)
-> (BinaryLogicalOperator -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BinaryLogicalOperator))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c BinaryLogicalOperator))
-> ((forall b. Data b => b -> b)
    -> BinaryLogicalOperator -> BinaryLogicalOperator)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> BinaryLogicalOperator
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> BinaryLogicalOperator
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> BinaryLogicalOperator -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BinaryLogicalOperator -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> BinaryLogicalOperator -> m BinaryLogicalOperator)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> BinaryLogicalOperator -> m BinaryLogicalOperator)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> BinaryLogicalOperator -> m BinaryLogicalOperator)
-> Data BinaryLogicalOperator
BinaryLogicalOperator -> Constr
BinaryLogicalOperator -> DataType
(forall b. Data b => b -> b)
-> BinaryLogicalOperator -> BinaryLogicalOperator
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> BinaryLogicalOperator -> u
forall u.
(forall d. Data d => d -> u) -> BinaryLogicalOperator -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BinaryLogicalOperator -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BinaryLogicalOperator -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BinaryLogicalOperator -> m BinaryLogicalOperator
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BinaryLogicalOperator -> m BinaryLogicalOperator
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinaryLogicalOperator
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BinaryLogicalOperator
-> c BinaryLogicalOperator
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinaryLogicalOperator)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BinaryLogicalOperator)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BinaryLogicalOperator
-> c BinaryLogicalOperator
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BinaryLogicalOperator
-> c BinaryLogicalOperator
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinaryLogicalOperator
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinaryLogicalOperator
$ctoConstr :: BinaryLogicalOperator -> Constr
toConstr :: BinaryLogicalOperator -> Constr
$cdataTypeOf :: BinaryLogicalOperator -> DataType
dataTypeOf :: BinaryLogicalOperator -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinaryLogicalOperator)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinaryLogicalOperator)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BinaryLogicalOperator)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BinaryLogicalOperator)
$cgmapT :: (forall b. Data b => b -> b)
-> BinaryLogicalOperator -> BinaryLogicalOperator
gmapT :: (forall b. Data b => b -> b)
-> BinaryLogicalOperator -> BinaryLogicalOperator
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BinaryLogicalOperator -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BinaryLogicalOperator -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BinaryLogicalOperator -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BinaryLogicalOperator -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> BinaryLogicalOperator -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> BinaryLogicalOperator -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> BinaryLogicalOperator -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> BinaryLogicalOperator -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BinaryLogicalOperator -> m BinaryLogicalOperator
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BinaryLogicalOperator -> m BinaryLogicalOperator
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BinaryLogicalOperator -> m BinaryLogicalOperator
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BinaryLogicalOperator -> m BinaryLogicalOperator
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BinaryLogicalOperator -> m BinaryLogicalOperator
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BinaryLogicalOperator -> m BinaryLogicalOperator
Data, BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
(BinaryLogicalOperator -> BinaryLogicalOperator -> Bool)
-> (BinaryLogicalOperator -> BinaryLogicalOperator -> Bool)
-> Eq BinaryLogicalOperator
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
== :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
$c/= :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
/= :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
Eq, (forall x. BinaryLogicalOperator -> Rep BinaryLogicalOperator x)
-> (forall x. Rep BinaryLogicalOperator x -> BinaryLogicalOperator)
-> Generic BinaryLogicalOperator
forall x. Rep BinaryLogicalOperator x -> BinaryLogicalOperator
forall x. BinaryLogicalOperator -> Rep BinaryLogicalOperator x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BinaryLogicalOperator -> Rep BinaryLogicalOperator x
from :: forall x. BinaryLogicalOperator -> Rep BinaryLogicalOperator x
$cto :: forall x. Rep BinaryLogicalOperator x -> BinaryLogicalOperator
to :: forall x. Rep BinaryLogicalOperator x -> BinaryLogicalOperator
Generic, Eq BinaryLogicalOperator
Eq BinaryLogicalOperator =>
(BinaryLogicalOperator -> BinaryLogicalOperator -> Ordering)
-> (BinaryLogicalOperator -> BinaryLogicalOperator -> Bool)
-> (BinaryLogicalOperator -> BinaryLogicalOperator -> Bool)
-> (BinaryLogicalOperator -> BinaryLogicalOperator -> Bool)
-> (BinaryLogicalOperator -> BinaryLogicalOperator -> Bool)
-> (BinaryLogicalOperator
    -> BinaryLogicalOperator -> BinaryLogicalOperator)
-> (BinaryLogicalOperator
    -> BinaryLogicalOperator -> BinaryLogicalOperator)
-> Ord BinaryLogicalOperator
BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
BinaryLogicalOperator -> BinaryLogicalOperator -> Ordering
BinaryLogicalOperator
-> BinaryLogicalOperator -> BinaryLogicalOperator
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BinaryLogicalOperator -> BinaryLogicalOperator -> Ordering
compare :: BinaryLogicalOperator -> BinaryLogicalOperator -> Ordering
$c< :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
< :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
$c<= :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
<= :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
$c> :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
> :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
$c>= :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
>= :: BinaryLogicalOperator -> BinaryLogicalOperator -> Bool
$cmax :: BinaryLogicalOperator
-> BinaryLogicalOperator -> BinaryLogicalOperator
max :: BinaryLogicalOperator
-> BinaryLogicalOperator -> BinaryLogicalOperator
$cmin :: BinaryLogicalOperator
-> BinaryLogicalOperator -> BinaryLogicalOperator
min :: BinaryLogicalOperator
-> BinaryLogicalOperator -> BinaryLogicalOperator
Ord)


instance Arbitrary BinaryLogicalOperator where

    arbitrary :: Gen BinaryLogicalOperator
arbitrary = Gen BinaryLogicalOperator
forall a. (Bounded a, Enum a) => Gen a
arbitraryBoundedEnum


instance Bounded BinaryLogicalOperator where

    minBound :: BinaryLogicalOperator
minBound = BinaryLogicalOperator
AlwaysFalse

    maxBound :: BinaryLogicalOperator
maxBound = BinaryLogicalOperator
AlwaysTrue


instance CoArbitrary BinaryLogicalOperator where

    coarbitrary :: forall b. BinaryLogicalOperator -> Gen b -> Gen b
coarbitrary = BinaryLogicalOperator -> Gen b -> Gen b
forall a b. Enum a => a -> Gen b -> Gen b
coarbitraryEnum


instance Enum BinaryLogicalOperator where

    toEnum :: Int -> BinaryLogicalOperator
toEnum Int
n = case Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`rem` Int
16 of
        Int
0  -> BinaryLogicalOperator
AlwaysFalse
        Int
1  -> BinaryLogicalOperator
LogicalNOR
        Int
2  -> BinaryLogicalOperator
ConverseNonImplication
        Int
3  -> BinaryLogicalOperator
NotFirstArgument
        Int
4  -> BinaryLogicalOperator
NonImplication
        Int
5  -> BinaryLogicalOperator
NotSecondArgument
        Int
6  -> BinaryLogicalOperator
LogicalXOR
        Int
7  -> BinaryLogicalOperator
LogicalNAND
        Int
8  -> BinaryLogicalOperator
LogicalAND
        Int
9  -> BinaryLogicalOperator
LogicalXNOR
        Int
10 -> BinaryLogicalOperator
SecondArgument
        Int
11 -> BinaryLogicalOperator
Implication
        Int
12 -> BinaryLogicalOperator
FirstArgument
        Int
13 -> BinaryLogicalOperator
ConverseImplication
        Int
14 -> BinaryLogicalOperator
LogicalOR
        Int
_  -> BinaryLogicalOperator
AlwaysTrue

    fromEnum :: BinaryLogicalOperator -> Int
fromEnum BinaryLogicalOperator
x = case BinaryLogicalOperator
x of
        BinaryLogicalOperator
AlwaysFalse            -> Int
0
        BinaryLogicalOperator
LogicalNOR             -> Int
1
        BinaryLogicalOperator
ConverseNonImplication -> Int
2
        BinaryLogicalOperator
NotFirstArgument       -> Int
3
        BinaryLogicalOperator
NonImplication         -> Int
4
        BinaryLogicalOperator
NotSecondArgument      -> Int
5
        BinaryLogicalOperator
LogicalXOR             -> Int
6
        BinaryLogicalOperator
LogicalNAND            -> Int
7
        BinaryLogicalOperator
LogicalAND             -> Int
8
        BinaryLogicalOperator
LogicalXNOR            -> Int
9
        BinaryLogicalOperator
SecondArgument         -> Int
10
        BinaryLogicalOperator
Implication            -> Int
11
        BinaryLogicalOperator
FirstArgument          -> Int
12
        BinaryLogicalOperator
ConverseImplication    -> Int
13
        BinaryLogicalOperator
LogicalOR              -> Int
14
        BinaryLogicalOperator
AlwaysTrue             -> Int
15

    succ :: BinaryLogicalOperator -> BinaryLogicalOperator
succ BinaryLogicalOperator
x = case BinaryLogicalOperator
x of
        BinaryLogicalOperator
AlwaysFalse            -> BinaryLogicalOperator
LogicalNOR
        BinaryLogicalOperator
LogicalNOR             -> BinaryLogicalOperator
ConverseNonImplication
        BinaryLogicalOperator
ConverseNonImplication -> BinaryLogicalOperator
NotFirstArgument
        BinaryLogicalOperator
NotFirstArgument       -> BinaryLogicalOperator
NonImplication
        BinaryLogicalOperator
NonImplication         -> BinaryLogicalOperator
NotSecondArgument
        BinaryLogicalOperator
NotSecondArgument      -> BinaryLogicalOperator
LogicalXOR
        BinaryLogicalOperator
LogicalXOR             -> BinaryLogicalOperator
LogicalNAND
        BinaryLogicalOperator
LogicalNAND            -> BinaryLogicalOperator
LogicalAND
        BinaryLogicalOperator
LogicalAND             -> BinaryLogicalOperator
LogicalXNOR
        BinaryLogicalOperator
LogicalXNOR            -> BinaryLogicalOperator
SecondArgument
        BinaryLogicalOperator
SecondArgument         -> BinaryLogicalOperator
Implication
        BinaryLogicalOperator
Implication            -> BinaryLogicalOperator
FirstArgument
        BinaryLogicalOperator
FirstArgument          -> BinaryLogicalOperator
ConverseImplication
        BinaryLogicalOperator
ConverseImplication    -> BinaryLogicalOperator
LogicalOR
        BinaryLogicalOperator
LogicalOR              -> BinaryLogicalOperator
AlwaysTrue
        BinaryLogicalOperator
AlwaysTrue             -> BinaryLogicalOperator
AlwaysFalse

    pred :: BinaryLogicalOperator -> BinaryLogicalOperator
pred BinaryLogicalOperator
x = case BinaryLogicalOperator
x of
        BinaryLogicalOperator
AlwaysFalse            -> BinaryLogicalOperator
AlwaysTrue
        BinaryLogicalOperator
LogicalNOR             -> BinaryLogicalOperator
AlwaysFalse
        BinaryLogicalOperator
ConverseNonImplication -> BinaryLogicalOperator
LogicalNOR
        BinaryLogicalOperator
NotFirstArgument       -> BinaryLogicalOperator
ConverseNonImplication
        BinaryLogicalOperator
NonImplication         -> BinaryLogicalOperator
NotFirstArgument
        BinaryLogicalOperator
NotSecondArgument      -> BinaryLogicalOperator
NonImplication
        BinaryLogicalOperator
LogicalXOR             -> BinaryLogicalOperator
NotSecondArgument
        BinaryLogicalOperator
LogicalNAND            -> BinaryLogicalOperator
LogicalXOR
        BinaryLogicalOperator
LogicalAND             -> BinaryLogicalOperator
LogicalNAND
        BinaryLogicalOperator
LogicalXNOR            -> BinaryLogicalOperator
LogicalAND
        BinaryLogicalOperator
SecondArgument         -> BinaryLogicalOperator
LogicalXNOR
        BinaryLogicalOperator
Implication            -> BinaryLogicalOperator
SecondArgument
        BinaryLogicalOperator
FirstArgument          -> BinaryLogicalOperator
Implication
        BinaryLogicalOperator
ConverseImplication    -> BinaryLogicalOperator
FirstArgument
        BinaryLogicalOperator
LogicalOR              -> BinaryLogicalOperator
ConverseImplication
        BinaryLogicalOperator
AlwaysTrue             -> BinaryLogicalOperator
LogicalOR


--    enumFrom x = toEnum <$> [fromEnum x .. 15]


--    enumFromTo x y =


instance Monad m => Serial m BinaryLogicalOperator where

    series :: Series m BinaryLogicalOperator
series = (Int -> [BinaryLogicalOperator]) -> Series m BinaryLogicalOperator
forall a (m :: * -> *). (Int -> [a]) -> Series m a
generate ((Int -> [BinaryLogicalOperator])
 -> Series m BinaryLogicalOperator)
-> (Int -> [BinaryLogicalOperator])
-> Series m BinaryLogicalOperator
forall a b. (a -> b) -> a -> b
$ [BinaryLogicalOperator] -> Int -> [BinaryLogicalOperator]
forall a b. a -> b -> a
const [BinaryLogicalOperator
forall a. Bounded a => a
minBound .. BinaryLogicalOperator
forall a. Bounded a => a
maxBound]


instance Show BinaryLogicalOperator where

    show :: BinaryLogicalOperator -> String
show BinaryLogicalOperator
x = String
"f p q = " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
s
        where
            s :: String
s = case BinaryLogicalOperator
x of
                BinaryLogicalOperator
AlwaysFalse            -> String
"False (Contradiction)"
                BinaryLogicalOperator
LogicalNOR             -> String
"¬p ∧ ¬q (Logical NOR)"
                BinaryLogicalOperator
ConverseNonImplication -> String
"¬p ∧ q (Converse Non-Implication)"
                BinaryLogicalOperator
NotFirstArgument       -> String
"¬p (Not First)"
                BinaryLogicalOperator
NonImplication         -> String
"p ∧ ¬q (Non-Implication)"
                BinaryLogicalOperator
NotSecondArgument      -> String
"¬q (Not Second)"
                BinaryLogicalOperator
LogicalXOR             -> String
"(p ∧ ¬q) ∨ (¬p ∧ q) (Logical XOR)"
                BinaryLogicalOperator
LogicalNAND            -> String
"¬p ∨ ¬q (Logical NAND)"
                BinaryLogicalOperator
LogicalAND             -> String
"p ∧ q (Logical AND)"
                BinaryLogicalOperator
LogicalXNOR            -> String
"(p ∧ q) ∨ (¬p ∧ ¬q) (Logical XNOR)"
                BinaryLogicalOperator
SecondArgument         -> String
"q (Second)"
                BinaryLogicalOperator
Implication            -> String
"¬p ∨ q (Implication)"
                BinaryLogicalOperator
FirstArgument          -> String
"p (First)"
                BinaryLogicalOperator
ConverseImplication    -> String
"p ∨ ¬q (Converse Implication)"
                BinaryLogicalOperator
LogicalOR              -> String
"p ∧ q (Logical OR)"
                BinaryLogicalOperator
AlwaysTrue             -> String
"True (Tautology)"


{-|
Convert from a closed, binary function over 'Bool' to a 'BinaryLogicalOperator'.
-}
fromBinaryLogicalFunction :: (Bool -> Bool -> Bool) -> BinaryLogicalOperator
fromBinaryLogicalFunction :: (Bool -> Bool -> Bool) -> BinaryLogicalOperator
fromBinaryLogicalFunction Bool -> Bool -> Bool
f = case (Bool -> Bool -> Bool
f Bool
True Bool
True, Bool -> Bool -> Bool
f Bool
True Bool
False, Bool -> Bool -> Bool
f Bool
False Bool
True, Bool -> Bool -> Bool
f Bool
False Bool
False) of
    (Bool
False, Bool
False, Bool
False, Bool
False) -> BinaryLogicalOperator
AlwaysFalse
    (Bool
False, Bool
False, Bool
False, Bool
True ) -> BinaryLogicalOperator
LogicalNOR
    (Bool
False, Bool
False, Bool
True , Bool
False) -> BinaryLogicalOperator
ConverseNonImplication
    (Bool
False, Bool
False, Bool
True , Bool
True ) -> BinaryLogicalOperator
NotFirstArgument
    (Bool
False, Bool
True , Bool
False, Bool
False) -> BinaryLogicalOperator
NonImplication
    (Bool
False, Bool
True , Bool
False, Bool
True ) -> BinaryLogicalOperator
NotSecondArgument
    (Bool
False, Bool
True , Bool
True , Bool
False) -> BinaryLogicalOperator
LogicalXOR
    (Bool
False, Bool
True , Bool
True , Bool
True ) -> BinaryLogicalOperator
LogicalNAND
    (Bool
True , Bool
False, Bool
False, Bool
False) -> BinaryLogicalOperator
LogicalAND
    (Bool
True , Bool
False, Bool
False, Bool
True ) -> BinaryLogicalOperator
LogicalXNOR
    (Bool
True , Bool
False, Bool
True , Bool
False) -> BinaryLogicalOperator
SecondArgument
    (Bool
True , Bool
False, Bool
True , Bool
True ) -> BinaryLogicalOperator
Implication
    (Bool
True , Bool
True , Bool
False, Bool
False) -> BinaryLogicalOperator
FirstArgument
    (Bool
True , Bool
True , Bool
False, Bool
True ) -> BinaryLogicalOperator
ConverseImplication
    (Bool
True , Bool
True , Bool
True , Bool
False) -> BinaryLogicalOperator
LogicalOR
    (Bool
True , Bool
True , Bool
True , Bool
True ) -> BinaryLogicalOperator
AlwaysTrue


{-|
Convert from a 'BinaryLogicalOperator' to a closed, binary function over 'Bool'.
-}
getBinaryLogicalOperator :: BinaryLogicalOperator -> Bool -> Bool -> Bool
getBinaryLogicalOperator :: BinaryLogicalOperator -> Bool -> Bool -> Bool
getBinaryLogicalOperator BinaryLogicalOperator
x = case BinaryLogicalOperator
x of
    BinaryLogicalOperator
AlwaysFalse            -> (Bool -> Bool) -> Bool -> Bool -> Bool
forall a b. a -> b -> a
const (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
False)
    BinaryLogicalOperator
LogicalNOR             -> \Bool
p Bool
q -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool
p Bool -> Bool -> Bool
|| Bool
q
    BinaryLogicalOperator
ConverseNonImplication -> \Bool
p Bool
q -> Bool -> Bool
not Bool
p Bool -> Bool -> Bool
&& Bool
q
    BinaryLogicalOperator
NotFirstArgument       -> \Bool
p Bool
_ -> Bool -> Bool
not Bool
p
    BinaryLogicalOperator
NonImplication         -> \Bool
p Bool
q -> Bool
p Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
q
    BinaryLogicalOperator
NotSecondArgument      -> \Bool
_ Bool
q -> Bool -> Bool
not Bool
q
    BinaryLogicalOperator
LogicalXOR             -> Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
    BinaryLogicalOperator
LogicalNAND            -> \Bool
p Bool
q -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool
p Bool -> Bool -> Bool
&& Bool
q
    BinaryLogicalOperator
LogicalAND             -> Bool -> Bool -> Bool
(&&)
    BinaryLogicalOperator
LogicalXNOR            -> Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==)
    BinaryLogicalOperator
SecondArgument         -> \Bool
_ Bool
q -> Bool
q
    BinaryLogicalOperator
Implication            -> \Bool
p Bool
q -> Bool -> Bool
not Bool
p Bool -> Bool -> Bool
|| Bool
q
    BinaryLogicalOperator
FirstArgument          -> Bool -> Bool -> Bool
forall a b. a -> b -> a
const
    BinaryLogicalOperator
ConverseImplication    -> \Bool
p Bool
q -> Bool
p Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
q
    BinaryLogicalOperator
LogicalOR              -> Bool -> Bool -> Bool
(||)
    BinaryLogicalOperator
AlwaysTrue             -> (Bool -> Bool) -> Bool -> Bool -> Bool
forall a b. a -> b -> a
const (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True)


{-|
Query the Haskell expression of a 'BinaryLogicalOperator' representation symbolically as a 'String'.
-}
getBinaryLogicalSymbol :: BinaryLogicalOperator -> String
getBinaryLogicalSymbol :: BinaryLogicalOperator -> String
getBinaryLogicalSymbol BinaryLogicalOperator
x = case BinaryLogicalOperator
x of
    BinaryLogicalOperator
AlwaysFalse            -> String
"(const False)"
    BinaryLogicalOperator
LogicalNOR             -> String
"(not . (||))"
    BinaryLogicalOperator
ConverseNonImplication -> String
"(</=)"
    BinaryLogicalOperator
NotFirstArgument       -> String
"(not . fst)"
    BinaryLogicalOperator
NonImplication         -> String
"(=/>)"
    BinaryLogicalOperator
NotSecondArgument      -> String
"(not . snd)"
    BinaryLogicalOperator
LogicalXOR             -> String
"(/=)"
    BinaryLogicalOperator
LogicalNAND            -> String
"(not . (&&))"
    BinaryLogicalOperator
LogicalAND             -> String
"(&&)"
    BinaryLogicalOperator
LogicalXNOR            -> String
"(==)"
    BinaryLogicalOperator
SecondArgument         -> String
"(snd)"
    BinaryLogicalOperator
Implication            -> String
"(==>)"
    BinaryLogicalOperator
FirstArgument          -> String
"(fst)"
    BinaryLogicalOperator
ConverseImplication    -> String
"(<==)"
    BinaryLogicalOperator
LogicalOR              -> String
"(||)"
    BinaryLogicalOperator
AlwaysTrue             -> String
"(const True)"