{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal)) 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.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSymsS), SomeSym (SomeSym))
import Grisette.Internal.SymPrim.Prim.Internal.Term
( FloatingUnaryOp
( FloatingAcos,
FloatingAsin,
FloatingAtan,
FloatingCos,
FloatingCosh,
FloatingExp,
FloatingLog,
FloatingSin,
FloatingSinh,
FloatingSqrt,
FloatingTan,
FloatingTanh
),
PEvalFloatingTerm (pevalFloatingUnaryTerm, pevalPowerTerm),
PEvalNumTerm
( pevalAbsNumTerm,
pevalMulNumTerm,
pevalNegNumTerm,
pevalSignumNumTerm
),
pevalSubNumTerm,
)
import Grisette.Internal.SymPrim.Prim.Term
( ConRep (ConType),
LinkedRep (underlyingTerm, wrapTerm),
PEvalNumTerm (pevalAddNumTerm),
SymRep (SymType),
Term (ConTerm),
conTerm,
pformatTerm,
symTerm,
)
import Language.Haskell.TH.Syntax (Lift)
newtype SymAlgReal = SymAlgReal {SymAlgReal -> Term AlgReal
underlyingAlgRealTerm :: Term AlgReal}
deriving ((forall (m :: * -> *). Quote m => SymAlgReal -> m Exp)
-> (forall (m :: * -> *).
Quote m =>
SymAlgReal -> Code m SymAlgReal)
-> Lift SymAlgReal
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymAlgReal -> m Exp
forall (m :: * -> *). Quote m => SymAlgReal -> Code m SymAlgReal
$clift :: forall (m :: * -> *). Quote m => SymAlgReal -> m Exp
lift :: forall (m :: * -> *). Quote m => SymAlgReal -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => SymAlgReal -> Code m SymAlgReal
liftTyped :: forall (m :: * -> *). Quote m => SymAlgReal -> Code m SymAlgReal
Lift, (forall x. SymAlgReal -> Rep SymAlgReal x)
-> (forall x. Rep SymAlgReal x -> SymAlgReal) -> Generic SymAlgReal
forall x. Rep SymAlgReal x -> SymAlgReal
forall x. SymAlgReal -> Rep SymAlgReal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymAlgReal -> Rep SymAlgReal x
from :: forall x. SymAlgReal -> Rep SymAlgReal x
$cto :: forall x. Rep SymAlgReal x -> SymAlgReal
to :: forall x. Rep SymAlgReal x -> SymAlgReal
Generic)
deriving anyclass (SymAlgReal -> ()
(SymAlgReal -> ()) -> NFData SymAlgReal
forall a. (a -> ()) -> NFData a
$crnf :: SymAlgReal -> ()
rnf :: SymAlgReal -> ()
NFData)
instance ConRep SymAlgReal where
type ConType SymAlgReal = AlgReal
instance SymRep AlgReal where
type SymType AlgReal = SymAlgReal
instance LinkedRep AlgReal SymAlgReal where
underlyingTerm :: SymAlgReal -> Term AlgReal
underlyingTerm = SymAlgReal -> Term AlgReal
underlyingAlgRealTerm
wrapTerm :: Term AlgReal -> SymAlgReal
wrapTerm = Term AlgReal -> SymAlgReal
SymAlgReal
instance Apply SymAlgReal where
type FunType SymAlgReal = SymAlgReal
apply :: SymAlgReal -> FunType SymAlgReal
apply = SymAlgReal -> FunType SymAlgReal
SymAlgReal -> SymAlgReal
forall a. a -> a
id
instance Eq SymAlgReal where
SymAlgReal Term AlgReal
a == :: SymAlgReal -> SymAlgReal -> Bool
== SymAlgReal Term AlgReal
b = Term AlgReal
a Term AlgReal -> Term AlgReal -> Bool
forall a. Eq a => a -> a -> Bool
== Term AlgReal
b
instance Hashable SymAlgReal where
hashWithSalt :: Int -> SymAlgReal -> Int
hashWithSalt Int
s (SymAlgReal Term AlgReal
a) = Int -> Term AlgReal -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Term AlgReal
a
instance IsString SymAlgReal where
fromString :: String -> SymAlgReal
fromString = Identifier -> SymAlgReal
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> SymAlgReal)
-> (String -> Identifier) -> String -> SymAlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString
instance Solvable AlgReal SymAlgReal where
con :: AlgReal -> SymAlgReal
con = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal)
-> (AlgReal -> Term AlgReal) -> AlgReal -> SymAlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlgReal -> Term AlgReal
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
sym :: Symbol -> SymAlgReal
sym = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal)
-> (Symbol -> Term AlgReal) -> Symbol -> SymAlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Term AlgReal
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
conView :: SymAlgReal -> Maybe AlgReal
conView (SymAlgReal (ConTerm Int
_ AlgReal
t)) = AlgReal -> Maybe AlgReal
forall a. a -> Maybe a
Just AlgReal
t
conView SymAlgReal
_ = Maybe AlgReal
forall a. Maybe a
Nothing
instance Show SymAlgReal where
show :: SymAlgReal -> String
show (SymAlgReal Term AlgReal
t) = Term AlgReal -> String
forall t. SupportedPrim t => Term t -> String
pformatTerm Term AlgReal
t
instance AllSyms SymAlgReal where
allSymsS :: SymAlgReal -> [SomeSym] -> [SomeSym]
allSymsS SymAlgReal
v = (SymAlgReal -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymAlgReal
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)
instance Num SymAlgReal where
(SymAlgReal Term AlgReal
l) + :: SymAlgReal -> SymAlgReal -> SymAlgReal
+ (SymAlgReal Term AlgReal
r) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal -> Term AlgReal -> Term AlgReal
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm Term AlgReal
l Term AlgReal
r
(SymAlgReal Term AlgReal
l) - :: SymAlgReal -> SymAlgReal -> SymAlgReal
- (SymAlgReal Term AlgReal
r) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal -> Term AlgReal -> Term AlgReal
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalSubNumTerm Term AlgReal
l Term AlgReal
r
(SymAlgReal Term AlgReal
l) * :: SymAlgReal -> SymAlgReal -> SymAlgReal
* (SymAlgReal Term AlgReal
r) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal -> Term AlgReal -> Term AlgReal
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm Term AlgReal
l Term AlgReal
r
negate :: SymAlgReal -> SymAlgReal
negate (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal -> Term AlgReal
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term AlgReal
v
abs :: SymAlgReal -> SymAlgReal
abs (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal -> Term AlgReal
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm Term AlgReal
v
signum :: SymAlgReal -> SymAlgReal
signum (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal -> Term AlgReal
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm Term AlgReal
v
fromInteger :: Integer -> SymAlgReal
fromInteger = AlgReal -> SymAlgReal
forall c t. Solvable c t => c -> t
con (AlgReal -> SymAlgReal)
-> (Integer -> AlgReal) -> Integer -> SymAlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> AlgReal
forall a. Num a => Integer -> a
fromInteger
instance Fractional SymAlgReal where
fromRational :: Rational -> SymAlgReal
fromRational = AlgReal -> SymAlgReal
forall c t. Solvable c t => c -> t
con (AlgReal -> SymAlgReal)
-> (Rational -> AlgReal) -> Rational -> SymAlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> AlgReal
forall a. Fractional a => Rational -> a
fromRational
/ :: SymAlgReal -> SymAlgReal -> SymAlgReal
(/) = String -> SymAlgReal -> SymAlgReal -> SymAlgReal
forall a. HasCallStack => String -> a
error String
"consider using safeFdiv instead of (/) for SymAlgReal"
recip :: SymAlgReal -> SymAlgReal
recip = String -> SymAlgReal -> SymAlgReal
forall a. HasCallStack => String -> a
error String
"consider using safeRecip instead of recip for SymAlgReal"
instance Floating SymAlgReal where
pi :: SymAlgReal
pi = Rational -> SymAlgReal
forall a. Fractional a => Rational -> a
fromRational (Rational -> SymAlgReal) -> Rational -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Double -> Rational
forall a. Real a => a -> Rational
toRational Double
forall a. Floating a => a
pi
exp :: SymAlgReal -> SymAlgReal
exp (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingExp Term AlgReal
v
log :: SymAlgReal -> SymAlgReal
log (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingLog Term AlgReal
v
sqrt :: SymAlgReal -> SymAlgReal
sqrt (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingSqrt Term AlgReal
v
sin :: SymAlgReal -> SymAlgReal
sin (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingSin Term AlgReal
v
cos :: SymAlgReal -> SymAlgReal
cos (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingCos Term AlgReal
v
tan :: SymAlgReal -> SymAlgReal
tan (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingTan Term AlgReal
v
sinh :: SymAlgReal -> SymAlgReal
sinh (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingSinh Term AlgReal
v
cosh :: SymAlgReal -> SymAlgReal
cosh (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingCosh Term AlgReal
v
tanh :: SymAlgReal -> SymAlgReal
tanh (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingTanh Term AlgReal
v
asin :: SymAlgReal -> SymAlgReal
asin (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingAsin Term AlgReal
v
acos :: SymAlgReal -> SymAlgReal
acos (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingAcos Term AlgReal
v
atan :: SymAlgReal -> SymAlgReal
atan (SymAlgReal Term AlgReal
v) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingAtan Term AlgReal
v
asinh :: SymAlgReal -> SymAlgReal
asinh = String -> SymAlgReal -> SymAlgReal
forall a. HasCallStack => String -> a
error String
"asinh isn't supported by the underlying sbv library"
acosh :: SymAlgReal -> SymAlgReal
acosh = String -> SymAlgReal -> SymAlgReal
forall a. HasCallStack => String -> a
error String
"acosh isn't supported by the underlying sbv library"
atanh :: SymAlgReal -> SymAlgReal
atanh = String -> SymAlgReal -> SymAlgReal
forall a. HasCallStack => String -> a
error String
"atanh isn't supported by the underlying sbv library"
SymAlgReal Term AlgReal
l ** :: SymAlgReal -> SymAlgReal -> SymAlgReal
** SymAlgReal Term AlgReal
r = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal -> Term AlgReal -> Term AlgReal
forall t. PEvalFloatingTerm t => Term t -> Term t -> Term t
pevalPowerTerm Term AlgReal
l Term AlgReal
r
logBase :: SymAlgReal -> SymAlgReal -> SymAlgReal
logBase = String -> SymAlgReal -> SymAlgReal -> SymAlgReal
forall a. HasCallStack => String -> a
error String
"consider using safeLogBase instead of logBase for AlgReal"