module Grisette.Core.Data.Class.LogicalOp
( LogicalOp (..),
)
where
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
( pevalAndTerm,
pevalImplyTerm,
pevalNotTerm,
pevalOrTerm,
pevalXorTerm,
)
import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool))
class LogicalOp b where
(.||) :: 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 .||
(.&&) :: 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 .&&
symNot :: b -> b
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 #-}
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 #-}
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