{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# 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),
    SymAlgRealKey,
  )
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.AsKey
  ( AsKey,
    KeyEq (keyEq),
    KeyHashable (keyHashWithSalt),
    shouldUseAsKeyHasSymbolicVersionError,
    shouldUseSymbolicVersionError,
  )
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),
    PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),
    PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    PEvalOrdTerm (pevalLeOrdTerm),
    SupportedPrim (pevalITETerm),
    pevalSubNumTerm,
    typedConstantSymbol,
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( ConRep (ConType),
    LinkedRep (underlyingTerm, wrapTerm),
    PEvalNumTerm (pevalAddNumTerm),
    SymRep (SymType),
    Term,
    conTerm,
    pformatTerm,
    symTerm,
    pattern ConTerm,
  )
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)

-- | t'SymAlgReal' type with identity equality.
type SymAlgRealKey = AsKey SymAlgReal

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

-- | This will crash the program.
--
-- 'SymAlgReal' cannot be compared concretely.
--
-- If you want to use the type as keys in hash maps based on term equality, say
-- memo table, you should use @'AsKey' 'SymAlgReal'@ instead.
--
-- If you want symbolic version of the equality operator, use
-- t'Grisette.Core.SymEq' instead.
instance Eq SymAlgReal where
  == :: SymAlgReal -> SymAlgReal -> Bool
(==) = String -> String -> String -> SymAlgReal -> SymAlgReal -> Bool
forall a. HasCallStack => String -> String -> String -> a
shouldUseAsKeyHasSymbolicVersionError String
"SymAlgReal" String
"(==)" String
"(.==)"

instance KeyEq SymAlgReal where
  keyEq :: SymAlgReal -> SymAlgReal -> Bool
keyEq (SymAlgReal Term AlgReal
l) (SymAlgReal Term AlgReal
r) = Term AlgReal
l Term AlgReal -> Term AlgReal -> Bool
forall a. Eq a => a -> a -> Bool
== Term AlgReal
r

-- | This will crash the program.
--
-- 'SymAlgReal' cannot be compared concretely.
--
-- If you want symbolic version of the comparison operators, use
-- t'Grisette.Core.SymOrd' instead.
instance Ord SymAlgReal where
  < :: SymAlgReal -> SymAlgReal -> Bool
(<) = String -> String -> String -> SymAlgReal -> SymAlgReal -> Bool
forall a. HasCallStack => String -> String -> String -> a
shouldUseSymbolicVersionError String
"SymAlgReal" String
"(<)" String
"(.<)"
  <= :: SymAlgReal -> SymAlgReal -> Bool
(<=) = String -> String -> String -> SymAlgReal -> SymAlgReal -> Bool
forall a. HasCallStack => String -> String -> String -> a
shouldUseSymbolicVersionError String
"SymAlgReal" String
"(<=)" String
"(.<=)"
  >= :: SymAlgReal -> SymAlgReal -> Bool
(>=) = String -> String -> String -> SymAlgReal -> SymAlgReal -> Bool
forall a. HasCallStack => String -> String -> String -> a
shouldUseSymbolicVersionError String
"SymAlgReal" String
"(>=)" String
"(.>=)"
  > :: SymAlgReal -> SymAlgReal -> Bool
(>) = String -> String -> String -> SymAlgReal -> SymAlgReal -> Bool
forall a. HasCallStack => String -> String -> String -> a
shouldUseSymbolicVersionError String
"SymAlgReal" String
"(>)" String
"(.>)"
  max :: SymAlgReal -> SymAlgReal -> SymAlgReal
max (SymAlgReal Term AlgReal
l) (SymAlgReal Term AlgReal
r) =
    Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm (Term AlgReal -> Term AlgReal -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLeOrdTerm Term AlgReal
l Term AlgReal
r) Term AlgReal
r Term AlgReal
l
  min :: SymAlgReal -> SymAlgReal -> SymAlgReal
min (SymAlgReal Term AlgReal
l) (SymAlgReal Term AlgReal
r) =
    Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm (Term AlgReal -> Term AlgReal -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLeOrdTerm Term AlgReal
l Term AlgReal
r) Term AlgReal
l Term AlgReal
r
  compare :: SymAlgReal -> SymAlgReal -> Ordering
compare = String -> String -> String -> SymAlgReal -> SymAlgReal -> Ordering
forall a. HasCallStack => String -> String -> String -> a
shouldUseSymbolicVersionError String
"SymAlgReal" String
"compare" String
"symCompare"

instance Real SymAlgReal where
  toRational :: SymAlgReal -> Rational
toRational = String -> SymAlgReal -> Rational
forall a. HasCallStack => String -> a
error String
"toRational: toRational isn't supported for SymAlgReal"

instance KeyHashable SymAlgReal where
  keyHashWithSalt :: Int -> SymAlgReal -> Int
keyHashWithSalt Int
s (SymAlgReal Term AlgReal
v) = Int
s Int -> Term AlgReal -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term AlgReal
v

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 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

-- | The function is total and will not throw errors. The result is considered
-- undefined if the divisor is 0.
--
-- It is the responsibility of the caller to ensure that the divisor is not
-- zero with the symbolic constraints, or use the t'Grisette.Core.FdivOr' or
-- t'Grisette.Core.SafeFdiv' classes.
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 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. PEvalFractionalTerm t => Term t -> Term t -> Term t
pevalFdivTerm Term AlgReal
l Term AlgReal
r
  recip :: SymAlgReal -> SymAlgReal
recip (SymAlgReal Term AlgReal
l) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal -> Term AlgReal
forall t. PEvalFractionalTerm t => Term t -> Term t
pevalRecipTerm Term AlgReal
l

-- | The functions are total and will not throw errors. The result for 'logBase'
-- is considered undefined if the base is 1.
--
-- It is the responsibility of the caller to ensure that the base is not 1
-- with the symbolic constraints, or use the t'Grisette.Core.LogBaseOr' or
-- t'Grisette.Core.SafeLogBase' classes.
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 (SymAlgReal Term AlgReal
baset) (SymAlgReal Term AlgReal
at) =
    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. PEvalFractionalTerm t => Term t -> Term t -> Term t
pevalFdivTerm
        (FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingLog Term AlgReal
at)
        (FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingLog Term AlgReal
baset)

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