{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm
-- 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.PEvalFractionalTerm () 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
  ( PEvalFractionalTerm
      ( pevalFdivTerm,
        pevalRecipTerm,
        withSbvFractionalTermConstraint
      ),
    SupportedPrim (withPrim),
    Term (ConTerm),
    conTerm,
    fdivTerm,
    recipTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
  ( binaryUnfoldOnce,
    generalBinaryUnfolded,
    generalUnaryUnfolded,
    unaryUnfoldOnce,
  )

instance (ValidFP eb sb) => PEvalFractionalTerm (FP eb sb) where
  pevalFdivTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFdivTerm = (FP eb sb -> FP eb sb -> 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 c.
(Typeable a, Typeable b, SupportedPrim c) =>
(a -> b -> c)
-> (Term a -> Term b -> Term c) -> Term a -> Term b -> Term c
generalBinaryUnfolded FP eb sb -> FP eb sb -> FP eb sb
forall a. Fractional a => a -> a -> a
(/) Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalFractionalTerm a => Term a -> Term a -> Term a
fdivTerm
  pevalRecipTerm :: Term (FP eb sb) -> Term (FP eb sb)
pevalRecipTerm = (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. Fractional a => a -> a
recip Term (FP eb sb) -> Term (FP eb sb)
forall a. PEvalFractionalTerm a => Term a -> Term a
recipTerm
  withSbvFractionalTermConstraint :: forall r. (Fractional (SBVType (FP eb sb)) => r) -> r
withSbvFractionalTermConstraint Fractional (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
Fractional (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

pevalDefaultFdivTerm ::
  (PEvalFractionalTerm a) => Term a -> Term a -> Term a
pevalDefaultFdivTerm :: forall a. PEvalFractionalTerm a => Term a -> Term a -> Term a
pevalDefaultFdivTerm =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
PEvalFractionalTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultFdivTerm TotalRuleBinary a a a
forall a. PEvalFractionalTerm a => Term a -> Term a -> Term a
fdivTerm

doPevalDefaultFdivTerm ::
  (PEvalFractionalTerm a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultFdivTerm :: forall a.
PEvalFractionalTerm a =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultFdivTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b)
  | a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
b
doPevalDefaultFdivTerm Term a
a (ConTerm Id
_ a
1) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalDefaultFdivTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

pevalDefaultRecipTerm ::
  (PEvalFractionalTerm a) => Term a -> Term a
pevalDefaultRecipTerm :: forall a. PEvalFractionalTerm a => Term a -> Term a
pevalDefaultRecipTerm = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall a. PEvalFractionalTerm a => Term a -> Maybe (Term a)
doPevalDefaultRecipTerm TotalRuleUnary a a
forall a. PEvalFractionalTerm a => Term a -> Term a
recipTerm

doPevalDefaultRecipTerm ::
  (PEvalFractionalTerm a) => Term a -> Maybe (Term a)
doPevalDefaultRecipTerm :: forall a. PEvalFractionalTerm a => Term a -> Maybe (Term a)
doPevalDefaultRecipTerm (ConTerm Id
_ a
n) | a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Fractional a => a -> a
recip a
n
doPevalDefaultRecipTerm Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

instance PEvalFractionalTerm AlgReal where
  pevalFdivTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal
pevalFdivTerm = Term AlgReal -> Term AlgReal -> Term AlgReal
forall a. PEvalFractionalTerm a => Term a -> Term a -> Term a
pevalDefaultFdivTerm
  pevalRecipTerm :: Term AlgReal -> Term AlgReal
pevalRecipTerm = Term AlgReal -> Term AlgReal
forall a. PEvalFractionalTerm a => Term a -> Term a
pevalDefaultRecipTerm
  withSbvFractionalTermConstraint :: forall r. (Fractional (SBVType AlgReal) => r) -> r
withSbvFractionalTermConstraint Fractional (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
Fractional (SBVType AlgReal) => r
(PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
 Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
r
r