{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.SymAlgReal
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal)) where

import Control.DeepSeq (NFData)
import qualified Data.Binary as Binary
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Hashable (Hashable (hashWithSalt))
import qualified Data.Serialize as Cereal
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.Internal.Decl.SymPrim.AllSyms
  ( AllSyms (allSymsS),
    SomeSym (SomeSym),
  )
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
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,
    typedConstantSymbol,
  )
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)

-- | Symbolic representation of algebraic real numbers.
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 => 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
. TypedSymbol 'ConstantKind AlgReal -> Term AlgReal
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm (TypedSymbol 'ConstantKind AlgReal -> Term AlgReal)
-> (Symbol -> TypedSymbol 'ConstantKind AlgReal)
-> Symbol
-> Term AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> TypedSymbol 'ConstantKind AlgReal
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol
  conView :: SymAlgReal -> Maybe AlgReal
conView (SymAlgReal (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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. 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"

instance Serial SymAlgReal where
  serialize :: forall (m :: * -> *). MonadPut m => SymAlgReal -> m ()
serialize = Term AlgReal -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => Term AlgReal -> m ()
serialize (Term AlgReal -> m ())
-> (SymAlgReal -> Term AlgReal) -> SymAlgReal -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymAlgReal -> Term AlgReal
underlyingAlgRealTerm
  deserialize :: forall (m :: * -> *). MonadGet m => m SymAlgReal
deserialize = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> m (Term AlgReal) -> m SymAlgReal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Term AlgReal)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (Term AlgReal)
deserialize

instance Cereal.Serialize SymAlgReal where
  put :: Putter SymAlgReal
put = Putter SymAlgReal
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => SymAlgReal -> m ()
serialize
  get :: Get SymAlgReal
get = Get SymAlgReal
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m SymAlgReal
deserialize

instance Binary.Binary SymAlgReal where
  put :: SymAlgReal -> Put
put = SymAlgReal -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => SymAlgReal -> m ()
serialize
  get :: Get SymAlgReal
get = Get SymAlgReal
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m SymAlgReal
deserialize