{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module Grisette.Internal.SymPrim.SymBool (SymBool (SymBool)) where
import Control.DeepSeq (NFData)
import Data.Hashable (Hashable (hashWithSalt))
import Data.String (IsString (fromString))
import GHC.Generics (Generic)
import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))
import Grisette.Internal.Core.Data.Class.Solvable
( Solvable (con, conView, ssym, sym),
)
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSymsS), SomeSym (SomeSym))
import Grisette.Internal.SymPrim.Prim.Term
( ConRep (ConType),
LinkedRep (underlyingTerm, wrapTerm),
SymRep (SymType),
Term (ConTerm),
conTerm,
pformatTerm,
symTerm,
)
import Language.Haskell.TH.Syntax (Lift)
newtype SymBool = SymBool {SymBool -> Term Bool
underlyingBoolTerm :: Term Bool}
deriving ((forall (m :: * -> *). Quote m => SymBool -> m Exp)
-> (forall (m :: * -> *). Quote m => SymBool -> Code m SymBool)
-> Lift SymBool
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymBool -> m Exp
forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
$clift :: forall (m :: * -> *). Quote m => SymBool -> m Exp
lift :: forall (m :: * -> *). Quote m => SymBool -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
liftTyped :: forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
Lift, SymBool -> ()
(SymBool -> ()) -> NFData SymBool
forall a. (a -> ()) -> NFData a
$crnf :: SymBool -> ()
rnf :: SymBool -> ()
NFData, (forall x. SymBool -> Rep SymBool x)
-> (forall x. Rep SymBool x -> SymBool) -> Generic SymBool
forall x. Rep SymBool x -> SymBool
forall x. SymBool -> Rep SymBool x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymBool -> Rep SymBool x
from :: forall x. SymBool -> Rep SymBool x
$cto :: forall x. Rep SymBool x -> SymBool
to :: forall x. Rep SymBool x -> SymBool
Generic)
instance ConRep SymBool where
type ConType SymBool = Bool
instance SymRep Bool where
type SymType Bool = SymBool
instance LinkedRep Bool SymBool where
underlyingTerm :: SymBool -> Term Bool
underlyingTerm (SymBool Term Bool
a) = Term Bool
a
wrapTerm :: Term Bool -> SymBool
wrapTerm = Term Bool -> SymBool
SymBool
instance Apply SymBool where
type FunType SymBool = SymBool
apply :: SymBool -> FunType SymBool
apply = SymBool -> FunType SymBool
SymBool -> SymBool
forall a. a -> a
id
instance Eq SymBool where
SymBool Term Bool
l == :: SymBool -> SymBool -> Bool
== SymBool Term Bool
r = Term Bool
l Term Bool -> Term Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Term Bool
r
instance Hashable SymBool where
hashWithSalt :: Int -> SymBool -> Int
hashWithSalt Int
s (SymBool Term Bool
v) = Int
s Int -> Term Bool -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term Bool
v
instance Solvable Bool SymBool where
con :: Bool -> SymBool
con = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> (Bool -> Term Bool) -> Bool -> SymBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
sym :: Symbol -> SymBool
sym = Term Bool -> SymBool
SymBool (Term Bool -> SymBool)
-> (Symbol -> Term Bool) -> Symbol -> SymBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Term Bool
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
conView :: SymBool -> Maybe Bool
conView (SymBool (ConTerm Int
_ Bool
t)) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
t
conView SymBool
_ = Maybe Bool
forall a. Maybe a
Nothing
instance IsString SymBool where
fromString :: String -> SymBool
fromString = Identifier -> SymBool
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> SymBool)
-> (String -> Identifier) -> String -> SymBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString
instance Show SymBool where
show :: SymBool -> String
show (SymBool Term Bool
t) = Term Bool -> String
forall t. SupportedPrim t => Term t -> String
pformatTerm Term Bool
t
instance AllSyms SymBool where
allSymsS :: SymBool -> [SomeSym] -> [SomeSym]
allSymsS SymBool
v = (SymBool -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymBool
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)