{-# LANGUAGE CPP #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.LogicalOp
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.LogicalOp
  ( LogicalOp (..),
  )
where

#if !MIN_VERSION_base(4,18,0)
import Control.Applicative (liftA2)
#endif

import Control.Monad.Identity (Identity)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
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

-- | Symbolic logical operators for symbolic booleans.
--
-- >>> let t = true :: SymBool
-- >>> let f = 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
  -- | Constant true
  true :: b
  true = b -> b
forall b. LogicalOp b => b -> b
symNot b
forall b. LogicalOp b => b
false

  -- | Constant false
  false :: b
  false = b -> b
forall b. LogicalOp b => b -> b
symNot b
forall b. LogicalOp b => b
true

  -- | 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 (true | false), ((.||), symNot | (.&&), symNot) #-}

-- LogicalOp instances
instance LogicalOp Bool where
  true :: Bool
true = Bool
True
  false :: Bool
false = Bool
False
  .|| :: 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
  true :: SymBool
true = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  false :: SymBool
false = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  (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

instance (LogicalOp a) => LogicalOp (Identity a) where
  true :: Identity a
true = a -> Identity a
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
forall b. LogicalOp b => b
true
  false :: Identity a
false = a -> Identity a
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
forall b. LogicalOp b => b
false
  .|| :: Identity a -> Identity a -> Identity a
(.||) = (a -> a -> a) -> Identity a -> Identity a -> Identity a
forall a b c.
(a -> b -> c) -> Identity a -> Identity b -> Identity c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall b. LogicalOp b => b -> b -> b
(.||)
  .&& :: Identity a -> Identity a -> Identity a
(.&&) = (a -> a -> a) -> Identity a -> Identity a -> Identity a
forall a b c.
(a -> b -> c) -> Identity a -> Identity b -> Identity c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall b. LogicalOp b => b -> b -> b
(.&&)
  symNot :: Identity a -> Identity a
symNot = (a -> a) -> Identity a -> Identity a
forall a b. (a -> b) -> Identity a -> Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall b. LogicalOp b => b -> b
symNot
  symXor :: Identity a -> Identity a -> Identity a
symXor = (a -> a -> a) -> Identity a -> Identity a -> Identity a
forall a b c.
(a -> b -> c) -> Identity a -> Identity b -> Identity c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall b. LogicalOp b => b -> b -> b
symXor
  symImplies :: Identity a -> Identity a -> Identity a
symImplies = (a -> a -> a) -> Identity a -> Identity a -> Identity a
forall a b c.
(a -> b -> c) -> Identity a -> Identity b -> Identity c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall b. LogicalOp b => b -> b -> b
symImplies