{-# LANGUAGE CPP #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Core.Data.Class.Bool
(
SEq (..),
SEq' (..),
LogicalOp (..),
SymBoolOp,
ITEOp (..),
)
where
import Control.Monad.Except
import Control.Monad.Identity
( Identity (Identity),
IdentityT (IdentityT),
)
import Control.Monad.Trans.Maybe
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.ByteString as B
import Data.Functor.Sum
import Data.Int
import Data.Word
import Generics.Deriving
import {-# SOURCE #-} Grisette.Core.Data.Class.SimpleMergeable
import Grisette.Core.Data.Class.Solvable
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
class SEq' f where
(==~~) :: f a -> f a -> SymBool
infix 4 ==~~
instance SEq' U1 where
U1 a
_ ==~~ :: forall a. U1 a -> U1 a -> SymBool
==~~ U1 a
_ = forall c t. Solvable c t => c -> t
con Bool
True
{-# INLINE (==~~) #-}
instance SEq' V1 where
V1 a
_ ==~~ :: forall a. V1 a -> V1 a -> SymBool
==~~ V1 a
_ = forall c t. Solvable c t => c -> t
con Bool
True
{-# INLINE (==~~) #-}
instance SEq c => SEq' (K1 i c) where
(K1 c
a) ==~~ :: forall a. K1 i c a -> K1 i c a -> SymBool
==~~ (K1 c
b) = c
a forall a. SEq a => a -> a -> SymBool
==~ c
b
{-# INLINE (==~~) #-}
instance SEq' a => SEq' (M1 i c a) where
(M1 a a
a) ==~~ :: forall a. M1 i c a a -> M1 i c a a -> SymBool
==~~ (M1 a a
b) = a a
a forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
b
{-# INLINE (==~~) #-}
instance (SEq' a, SEq' b) => SEq' (a :+: b) where
(L1 a a
a) ==~~ :: forall a. (:+:) a b a -> (:+:) a b a -> SymBool
==~~ (L1 a a
b) = a a
a forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
b
(R1 b a
a) ==~~ (R1 b a
b) = b a
a forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ b a
b
(:+:) a b a
_ ==~~ (:+:) a b a
_ = forall c t. Solvable c t => c -> t
con Bool
False
{-# INLINE (==~~) #-}
instance (SEq' a, SEq' b) => SEq' (a :*: b) where
(a a
a1 :*: b a
b1) ==~~ :: forall a. (:*:) a b a -> (:*:) a b a -> SymBool
==~~ (a a
a2 :*: b a
b2) = (a a
a1 forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ b a
b2)
{-# INLINE (==~~) #-}
class SEq a where
(==~) :: a -> a -> SymBool
a
a ==~ a
b = forall b. LogicalOp b => b -> b
nots forall a b. (a -> b) -> a -> b
$ a
a forall a. SEq a => a -> a -> SymBool
/=~ a
b
{-# INLINE (==~) #-}
infix 4 ==~
(/=~) :: a -> a -> SymBool
a
a /=~ a
b = forall b. LogicalOp b => b -> b
nots forall a b. (a -> b) -> a -> b
$ a
a forall a. SEq a => a -> a -> SymBool
==~ a
b
{-# INLINE (/=~) #-}
infix 4 /=~
{-# MINIMAL (==~) | (/=~) #-}
instance (Generic a, SEq' (Rep a)) => SEq (Default a) where
Default a
l ==~ :: Default a -> Default a -> SymBool
==~ Default a
r = forall a x. Generic a => a -> Rep a x
from a
l forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ forall a x. Generic a => a -> Rep a x
from a
r
{-# INLINE (==~) #-}
class LogicalOp b where
(||~) :: b -> b -> b
b
a ||~ b
b = forall b. LogicalOp b => b -> b
nots forall a b. (a -> b) -> a -> b
$ forall b. LogicalOp b => b -> b
nots b
a forall b. LogicalOp b => b -> b -> b
&&~ forall b. LogicalOp b => b -> b
nots b
b
{-# INLINE (||~) #-}
infixr 2 ||~
(&&~) :: b -> b -> b
b
a &&~ b
b = forall b. LogicalOp b => b -> b
nots forall a b. (a -> b) -> a -> b
$ forall b. LogicalOp b => b -> b
nots b
a forall b. LogicalOp b => b -> b -> b
||~ forall b. LogicalOp b => b -> b
nots b
b
{-# INLINE (&&~) #-}
infixr 3 &&~
nots :: b -> b
xors :: b -> b -> b
b
a `xors` b
b = (b
a forall b. LogicalOp b => b -> b -> b
&&~ forall b. LogicalOp b => b -> b
nots b
b) forall b. LogicalOp b => b -> b -> b
||~ (forall b. LogicalOp b => b -> b
nots b
a forall b. LogicalOp b => b -> b -> b
&&~ b
b)
{-# INLINE xors #-}
implies :: b -> b -> b
b
a `implies` b
b = forall b. LogicalOp b => b -> b
nots b
a forall b. LogicalOp b => b -> b -> b
||~ b
b
{-# INLINE implies #-}
{-# MINIMAL (||~), nots | (&&~), nots #-}
instance LogicalOp Bool where
||~ :: Bool -> Bool -> Bool
(||~) = Bool -> Bool -> Bool
(||)
{-# INLINE (||~) #-}
&&~ :: Bool -> Bool -> Bool
(&&~) = Bool -> Bool -> Bool
(&&)
{-# INLINE (&&~) #-}
nots :: Bool -> Bool
nots = Bool -> Bool
not
{-# INLINE nots #-}
class ITEOp v where
ites :: SymBool -> v -> v -> v
class (SimpleMergeable b, SEq b, Eq b, LogicalOp b, Solvable Bool b, ITEOp b) => SymBoolOp b
#define CONCRETE_SEQ(type) \
instance SEq type where \
l ==~ r = con $ l == r; \
{-# INLINE (==~) #-}
#if 1
CONCRETE_SEQ(Bool)
CONCRETE_SEQ(Integer)
CONCRETE_SEQ(Char)
CONCRETE_SEQ(Int)
CONCRETE_SEQ(Int8)
CONCRETE_SEQ(Int16)
CONCRETE_SEQ(Int32)
CONCRETE_SEQ(Int64)
CONCRETE_SEQ(Word)
CONCRETE_SEQ(Word8)
CONCRETE_SEQ(Word16)
CONCRETE_SEQ(Word32)
CONCRETE_SEQ(Word64)
CONCRETE_SEQ(B.ByteString)
#endif
deriving via (Default [a]) instance (SEq a) => SEq [a]
deriving via (Default (Maybe a)) instance (SEq a) => SEq (Maybe a)
deriving via (Default (Either e a)) instance (SEq e, SEq a) => SEq (Either e a)
instance (SEq (m (Either e a))) => SEq (ExceptT e m a) where
(ExceptT m (Either e a)
a) ==~ :: ExceptT e m a -> ExceptT e m a -> SymBool
==~ (ExceptT m (Either e a)
b) = m (Either e a)
a forall a. SEq a => a -> a -> SymBool
==~ m (Either e a)
b
{-# INLINE (==~) #-}
instance (SEq (m (Maybe a))) => SEq (MaybeT m a) where
(MaybeT m (Maybe a)
a) ==~ :: MaybeT m a -> MaybeT m a -> SymBool
==~ (MaybeT m (Maybe a)
b) = m (Maybe a)
a forall a. SEq a => a -> a -> SymBool
==~ m (Maybe a)
b
{-# INLINE (==~) #-}
instance SEq () where
()
_ ==~ :: () -> () -> SymBool
==~ ()
_ = forall c t. Solvable c t => c -> t
con Bool
True
{-# INLINE (==~) #-}
deriving via (Default (a, b)) instance (SEq a, SEq b) => SEq (a, b)
deriving via (Default (a, b, c)) instance (SEq a, SEq b, SEq c) => SEq (a, b, c)
deriving via
(Default (a, b, c, d))
instance
(SEq a, SEq b, SEq c, SEq d) =>
SEq (a, b, c, d)
deriving via
(Default (a, b, c, d, e))
instance
(SEq a, SEq b, SEq c, SEq d, SEq e) =>
SEq (a, b, c, d, e)
deriving via
(Default (a, b, c, d, e, f))
instance
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) =>
SEq (a, b, c, d, e, f)
deriving via
(Default (a, b, c, d, e, f, g))
instance
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) =>
SEq (a, b, c, d, e, f, g)
deriving via
(Default (a, b, c, d, e, f, g, h))
instance
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g, SEq h) =>
SEq (a, b, c, d, e, f, g, h)
deriving via
(Default (Sum f g a))
instance
(SEq (f a), SEq (g a)) => SEq (Sum f g a)
instance (SEq (m (a, s))) => SEq (WriterLazy.WriterT s m a) where
(WriterLazy.WriterT m (a, s)
l) ==~ :: WriterT s m a -> WriterT s m a -> SymBool
==~ (WriterLazy.WriterT m (a, s)
r) = m (a, s)
l forall a. SEq a => a -> a -> SymBool
==~ m (a, s)
r
{-# INLINE (==~) #-}
instance (SEq (m (a, s))) => SEq (WriterStrict.WriterT s m a) where
(WriterStrict.WriterT m (a, s)
l) ==~ :: WriterT s m a -> WriterT s m a -> SymBool
==~ (WriterStrict.WriterT m (a, s)
r) = m (a, s)
l forall a. SEq a => a -> a -> SymBool
==~ m (a, s)
r
{-# INLINE (==~) #-}
instance (SEq a) => SEq (Identity a) where
(Identity a
l) ==~ :: Identity a -> Identity a -> SymBool
==~ (Identity a
r) = a
l forall a. SEq a => a -> a -> SymBool
==~ a
r
{-# INLINE (==~) #-}
instance (SEq (m a)) => SEq (IdentityT m a) where
(IdentityT m a
l) ==~ :: IdentityT m a -> IdentityT m a -> SymBool
==~ (IdentityT m a
r) = m a
l forall a. SEq a => a -> a -> SymBool
==~ m a
r
{-# INLINE (==~) #-}
instance (SupportedPrim a) => ITEOp (Sym a) where
ites :: SymBool -> Sym a -> Sym a -> Sym a
ites (Sym Term Bool
c) (Sym Term a
t) (Sym Term a
f) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
c Term a
t Term a
f
instance LogicalOp (Sym Bool) where
(Sym Term Bool
l) ||~ :: SymBool -> SymBool -> SymBool
||~ (Sym Term Bool
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l Term Bool
r
(Sym Term Bool
l) &&~ :: SymBool -> SymBool -> SymBool
&&~ (Sym Term Bool
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l Term Bool
r
nots :: SymBool -> SymBool
nots (Sym Term Bool
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
pevalNotTerm Term Bool
v
(Sym Term Bool
l) xors :: SymBool -> SymBool -> SymBool
`xors` (Sym Term Bool
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalXorTerm Term Bool
l Term Bool
r
(Sym Term Bool
l) implies :: SymBool -> SymBool -> SymBool
`implies` (Sym Term Bool
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalImplyTerm Term Bool
l Term Bool
r