SymAlgReal.hs

{-# 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 {underlyingAlgRealTerm :: Term AlgReal}
  deriving (Lift, Generic)
  deriving anyclass (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 = underlyingAlgRealTerm
  wrapTerm = SymAlgReal

instance Apply SymAlgReal where
  type FunType SymAlgReal = SymAlgReal
  apply = 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
  (==) = shouldUseAsKeyHasSymbolicVersionError "SymAlgReal" "(==)" "(.==)"

instance KeyEq SymAlgReal where
  keyEq (SymAlgReal l) (SymAlgReal r) = l == 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
  (<) = shouldUseSymbolicVersionError "SymAlgReal" "(<)" "(.<)"
  (<=) = shouldUseSymbolicVersionError "SymAlgReal" "(<=)" "(.<=)"
  (>=) = shouldUseSymbolicVersionError "SymAlgReal" "(>=)" "(.>=)"
  (>) = shouldUseSymbolicVersionError "SymAlgReal" "(>)" "(.>)"
  max (SymAlgReal l) (SymAlgReal r) =
    SymAlgReal $ pevalITETerm (pevalLeOrdTerm l r) r l
  min (SymAlgReal l) (SymAlgReal r) =
    SymAlgReal $ pevalITETerm (pevalLeOrdTerm l r) l r
  compare = shouldUseSymbolicVersionError "SymAlgReal" "compare" "symCompare"

instance Real SymAlgReal where
  toRational = error "toRational: toRational isn't supported for SymAlgReal"

instance KeyHashable SymAlgReal where
  keyHashWithSalt s (SymAlgReal v) = s `hashWithSalt` v

instance IsString SymAlgReal where
  fromString = ssym . fromString

instance Solvable AlgReal SymAlgReal where
  con = SymAlgReal . conTerm
  sym = SymAlgReal . symTerm . typedConstantSymbol
  conView (SymAlgReal (ConTerm t)) = Just t
  conView _ = Nothing

instance Show SymAlgReal where
  show (SymAlgReal t) = pformatTerm t

instance AllSyms SymAlgReal where
  allSymsS v = (SomeSym v :)

instance Num SymAlgReal where
  (SymAlgReal l) + (SymAlgReal r) = SymAlgReal $ pevalAddNumTerm l r
  (SymAlgReal l) - (SymAlgReal r) = SymAlgReal $ pevalSubNumTerm l r
  (SymAlgReal l) * (SymAlgReal r) = SymAlgReal $ pevalMulNumTerm l r
  negate (SymAlgReal v) = SymAlgReal $ pevalNegNumTerm v
  abs (SymAlgReal v) = SymAlgReal $ pevalAbsNumTerm v
  signum (SymAlgReal v) = SymAlgReal $ pevalSignumNumTerm v
  fromInteger = con . 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 = con . fromRational
  (SymAlgReal l) / (SymAlgReal r) = SymAlgReal $ pevalFdivTerm l r
  recip (SymAlgReal l) = SymAlgReal $ pevalRecipTerm 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 = fromRational $ toRational pi
  exp (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingExp v
  log (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingLog v
  sqrt (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingSqrt v
  sin (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingSin v
  cos (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingCos v
  tan (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingTan v
  sinh (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingSinh v
  cosh (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingCosh v
  tanh (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingTanh v
  asin (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingAsin v
  acos (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingAcos v
  atan (SymAlgReal v) = SymAlgReal $ pevalFloatingUnaryTerm FloatingAtan v
  asinh = error "asinh isn't supported by the underlying sbv library"
  acosh = error "acosh isn't supported by the underlying sbv library"
  atanh = error "atanh isn't supported by the underlying sbv library"
  SymAlgReal l ** SymAlgReal r = SymAlgReal $ pevalPowerTerm l r
  logBase (SymAlgReal baset) (SymAlgReal at) =
    SymAlgReal $
      pevalFdivTerm
        (pevalFloatingUnaryTerm FloatingLog at)
        (pevalFloatingUnaryTerm FloatingLog baset)

instance Serial SymAlgReal where
  serialize = serialize . underlyingAlgRealTerm
  deserialize = SymAlgReal <$> deserialize

instance Cereal.Serialize SymAlgReal where
  put = serialize
  get = deserialize

instance Binary.Binary SymAlgReal where
  put = serialize
  get = deserialize