{-# 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 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)

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