module Grisette.Internal.Core.Data.Class.LogicalOp
  ( LogicalOp (..),
  )
where

import Grisette.Internal.SymPrim.Prim.Term
  ( pevalAndTerm,
    pevalImplyTerm,
    pevalNotTerm,
    pevalOrTerm,
    pevalXorTerm,
  )
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> :set -XDataKinds
-- >>> :set -XBinaryLiterals
-- >>> :set -XFlexibleContexts
-- >>> :set -XFlexibleInstances
-- >>> :set -XFunctionalDependencies

-- | Symbolic logical operators for symbolic booleans.
--
-- >>> let t = con True :: SymBool
-- >>> let f = con False :: SymBool
-- >>> let a = "a" :: SymBool
-- >>> let b = "b" :: SymBool
-- >>> t .|| f
-- true
-- >>> a .|| t
-- true
-- >>> a .|| f
-- a
-- >>> a .|| b
-- (|| a b)
-- >>> t .&& f
-- false
-- >>> a .&& t
-- a
-- >>> a .&& f
-- false
-- >>> a .&& b
-- (&& a b)
-- >>> symNot t
-- false
-- >>> symNot f
-- true
-- >>> symNot a
-- (! a)
-- >>> t `symXor` f
-- true
-- >>> t `symXor` t
-- false
-- >>> a `symXor` t
-- (! a)
-- >>> a `symXor` f
-- a
-- >>> a `symXor` b
-- (|| (&& (! a) b) (&& a (! b)))
class LogicalOp b where
  -- | Symbolic disjunction
  (.||) :: b -> b -> b
  b
a .|| b
b = b -> b
forall b. LogicalOp b => b -> b
symNot (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ b -> b
forall b. LogicalOp b => b -> b
symNot b
a b -> b -> b
forall b. LogicalOp b => b -> b -> b
.&& b -> b
forall b. LogicalOp b => b -> b
symNot b
b
  {-# INLINE (.||) #-}

  infixr 2 .||

  -- | Symbolic conjunction
  (.&&) :: b -> b -> b
  b
a .&& b
b = b -> b
forall b. LogicalOp b => b -> b
symNot (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ b -> b
forall b. LogicalOp b => b -> b
symNot b
a b -> b -> b
forall b. LogicalOp b => b -> b -> b
.|| b -> b
forall b. LogicalOp b => b -> b
symNot b
b
  {-# INLINE (.&&) #-}

  infixr 3 .&&

  -- | Symbolic negation
  symNot :: b -> b

  -- | Symbolic exclusive disjunction
  symXor :: b -> b -> b
  b
a `symXor` b
b = (b
a b -> b -> b
forall b. LogicalOp b => b -> b -> b
.&& b -> b
forall b. LogicalOp b => b -> b
symNot b
b) b -> b -> b
forall b. LogicalOp b => b -> b -> b
.|| (b -> b
forall b. LogicalOp b => b -> b
symNot b
a b -> b -> b
forall b. LogicalOp b => b -> b -> b
.&& b
b)
  {-# INLINE symXor #-}

  -- | Symbolic implication
  symImplies :: b -> b -> b
  b
a `symImplies` b
b = b -> b
forall b. LogicalOp b => b -> b
symNot b
a b -> b -> b
forall b. LogicalOp b => b -> b -> b
.|| b
b
  {-# INLINE symImplies #-}

  {-# MINIMAL (.||), symNot | (.&&), symNot #-}

-- LogicalOp instances
instance LogicalOp Bool where
  .|| :: Bool -> Bool -> Bool
(.||) = Bool -> Bool -> Bool
(||)
  {-# INLINE (.||) #-}
  .&& :: Bool -> Bool -> Bool
(.&&) = Bool -> Bool -> Bool
(&&)
  {-# INLINE (.&&) #-}
  symNot :: Bool -> Bool
symNot = Bool -> Bool
not
  {-# INLINE symNot #-}

instance LogicalOp SymBool where
  (SymBool Term Bool
l) .|| :: SymBool -> SymBool -> SymBool
.|| (SymBool Term Bool
r) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l Term Bool
r
  (SymBool Term Bool
l) .&& :: SymBool -> SymBool -> SymBool
.&& (SymBool Term Bool
r) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l Term Bool
r
  symNot :: SymBool -> SymBool
symNot (SymBool Term Bool
v) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
pevalNotTerm Term Bool
v
  (SymBool Term Bool
l) symXor :: SymBool -> SymBool -> SymBool
`symXor` (SymBool Term Bool
r) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalXorTerm Term Bool
l Term Bool
r
  (SymBool Term Bool
l) symImplies :: SymBool -> SymBool -> SymBool
`symImplies` (SymBool Term Bool
r) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalImplyTerm Term Bool
l Term Bool
r