{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) 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),
PEvalNumTerm
( pevalAbsNumTerm,
pevalAddNumTerm,
pevalMulNumTerm,
pevalNegNumTerm,
pevalSignumNumTerm
),
SymRep (SymType),
Term (ConTerm),
conTerm,
pevalSubNumTerm,
pformat,
symTerm,
)
import Language.Haskell.TH.Syntax (Lift)
newtype SymInteger = SymInteger {SymInteger -> Term Integer
underlyingIntegerTerm :: Term Integer}
deriving ((forall (m :: * -> *). Quote m => SymInteger -> m Exp)
-> (forall (m :: * -> *).
Quote m =>
SymInteger -> Code m SymInteger)
-> Lift SymInteger
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymInteger -> m Exp
forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
$clift :: forall (m :: * -> *). Quote m => SymInteger -> m Exp
lift :: forall (m :: * -> *). Quote m => SymInteger -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
liftTyped :: forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
Lift, SymInteger -> ()
(SymInteger -> ()) -> NFData SymInteger
forall a. (a -> ()) -> NFData a
$crnf :: SymInteger -> ()
rnf :: SymInteger -> ()
NFData, (forall x. SymInteger -> Rep SymInteger x)
-> (forall x. Rep SymInteger x -> SymInteger) -> Generic SymInteger
forall x. Rep SymInteger x -> SymInteger
forall x. SymInteger -> Rep SymInteger x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymInteger -> Rep SymInteger x
from :: forall x. SymInteger -> Rep SymInteger x
$cto :: forall x. Rep SymInteger x -> SymInteger
to :: forall x. Rep SymInteger x -> SymInteger
Generic)
instance ConRep SymInteger where
type ConType SymInteger = Integer
instance SymRep Integer where
type SymType Integer = SymInteger
instance LinkedRep Integer SymInteger where
underlyingTerm :: SymInteger -> Term Integer
underlyingTerm (SymInteger Term Integer
a) = Term Integer
a
wrapTerm :: Term Integer -> SymInteger
wrapTerm = Term Integer -> SymInteger
SymInteger
instance Apply SymInteger where
type FunType SymInteger = SymInteger
apply :: SymInteger -> FunType SymInteger
apply = SymInteger -> FunType SymInteger
SymInteger -> SymInteger
forall a. a -> a
id
instance Num SymInteger where
(SymInteger Term Integer
l) + :: SymInteger -> SymInteger -> SymInteger
+ (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm Term Integer
l Term Integer
r
(SymInteger Term Integer
l) - :: SymInteger -> SymInteger -> SymInteger
- (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalSubNumTerm Term Integer
l Term Integer
r
(SymInteger Term Integer
l) * :: SymInteger -> SymInteger -> SymInteger
* (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm Term Integer
l Term Integer
r
negate :: SymInteger -> SymInteger
negate (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term Integer
v
abs :: SymInteger -> SymInteger
abs (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm Term Integer
v
signum :: SymInteger -> SymInteger
signum (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm Term Integer
v
fromInteger :: Integer -> SymInteger
fromInteger = Integer -> SymInteger
forall c t. Solvable c t => c -> t
con
instance Eq SymInteger where
SymInteger Term Integer
l == :: SymInteger -> SymInteger -> Bool
== SymInteger Term Integer
r = Term Integer
l Term Integer -> Term Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Term Integer
r
instance Hashable SymInteger where
hashWithSalt :: Int -> SymInteger -> Int
hashWithSalt Int
s (SymInteger Term Integer
v) = Int
s Int -> Term Integer -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term Integer
v
instance Solvable Integer SymInteger where
con :: Integer -> SymInteger
con = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger)
-> (Integer -> Term Integer) -> Integer -> SymInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
sym :: Symbol -> SymInteger
sym = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger)
-> (Symbol -> Term Integer) -> Symbol -> SymInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Term Integer
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
conView :: SymInteger -> Maybe Integer
conView (SymInteger (ConTerm Int
_ Integer
t)) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
t
conView SymInteger
_ = Maybe Integer
forall a. Maybe a
Nothing
instance IsString SymInteger where
fromString :: String -> SymInteger
fromString = Identifier -> SymInteger
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> SymInteger)
-> (String -> Identifier) -> String -> SymInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString
instance Show SymInteger where
show :: SymInteger -> String
show (SymInteger Term Integer
t) = Term Integer -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Integer
t
instance AllSyms SymInteger where
allSymsS :: SymInteger -> [SomeSym] -> [SomeSym]
allSymsS SymInteger
v = (SymInteger -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymInteger
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)