{-# LANGUAGE ScopedTypeVariables #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm
-- 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.Prim.Internal.Instances.PEvalFloatingTerm () where

import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( FloatingUnaryOp (FloatingAcosh, FloatingAsinh, FloatingAtanh, FloatingSqrt),
    PEvalFloatingTerm
      ( pevalFloatingUnaryTerm,
        pevalPowerTerm,
        withSbvFloatingTermConstraint
      ),
    SupportedPrim (withPrim),
    floatingUnaryTerm,
    powerTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
  ( generalUnaryUnfolded,
  )

instance (ValidFP eb sb) => PEvalFloatingTerm (FP eb sb) where
  pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
pevalFloatingUnaryTerm FloatingUnaryOp
op =
    case FloatingUnaryOp
op of
      FloatingUnaryOp
FloatingSqrt -> (FP eb sb -> FP eb sb)
-> (Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> Term (FP eb sb)
forall a b.
(Typeable a, SupportedPrim b) =>
(a -> b) -> (Term a -> Term b) -> Term a -> Term b
generalUnaryUnfolded FP eb sb -> FP eb sb
forall a. Floating a => a -> a
sqrt ((Term (FP eb sb) -> Term (FP eb sb))
 -> Term (FP eb sb) -> Term (FP eb sb))
-> (Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FloatingUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
forall a.
PEvalFloatingTerm a =>
FloatingUnaryOp -> Term a -> Term a
floatingUnaryTerm FloatingUnaryOp
op
      FloatingUnaryOp
_ -> [Char] -> Term (FP eb sb) -> Term (FP eb sb)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term (FP eb sb) -> Term (FP eb sb))
-> [Char] -> Term (FP eb sb) -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ [Char]
"operation " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> FloatingUnaryOp -> [Char]
forall a. Show a => a -> [Char]
show FloatingUnaryOp
op [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" not supported for FP"
  pevalPowerTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalPowerTerm = [Char] -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. HasCallStack => [Char] -> a
error [Char]
"power operation not supported for FP"
  withSbvFloatingTermConstraint :: forall r. (Floating (SBVType (FP eb sb)) => r) -> r
withSbvFloatingTermConstraint Floating (SBVType (FP eb sb)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FP eb sb) r
Floating (SBVType (FP eb sb)) => r
(PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
 Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
r
r

instance PEvalFloatingTerm AlgReal where
  pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term AlgReal -> Term AlgReal
pevalFloatingUnaryTerm FloatingUnaryOp
op =
    case FloatingUnaryOp
op of
      FloatingUnaryOp
FloatingAsinh ->
        [Char] -> Term AlgReal -> Term AlgReal
forall a. HasCallStack => [Char] -> a
error [Char]
"operation asinh not supported by sbv for AlgReal"
      FloatingUnaryOp
FloatingAcosh ->
        [Char] -> Term AlgReal -> Term AlgReal
forall a. HasCallStack => [Char] -> a
error [Char]
"operation acosh not supported by sbv for AlgReal"
      FloatingUnaryOp
FloatingAtanh ->
        [Char] -> Term AlgReal -> Term AlgReal
forall a. HasCallStack => [Char] -> a
error [Char]
"operation atanh not supported by sbv for AlgReal"
      FloatingUnaryOp
_ -> FloatingUnaryOp -> Term AlgReal -> Term AlgReal
forall a.
PEvalFloatingTerm a =>
FloatingUnaryOp -> Term a -> Term a
floatingUnaryTerm FloatingUnaryOp
op
  pevalPowerTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal
pevalPowerTerm = Term AlgReal -> Term AlgReal -> Term AlgReal
forall a. PEvalFloatingTerm a => Term a -> Term a -> Term a
powerTerm
  withSbvFloatingTermConstraint :: forall r. (Floating (SBVType AlgReal) => r) -> r
withSbvFloatingTermConstraint Floating (SBVType AlgReal) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @AlgReal r
Floating (SBVType AlgReal) => r
(PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
 Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
r
r