{-# LANGUAGE PatternSynonyms #-}
{-# 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,
    fdivTerm,
    recipTerm,
    pattern ConTerm,
    pattern SupportedTerm,
  )
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, Eq a) => Term a -> Term a -> Term a
pevalDefaultFdivTerm :: forall a.
(PEvalFractionalTerm a, Eq a) =>
Term a -> Term a -> Term a
pevalDefaultFdivTerm l :: Term a
l@Term a
SupportedTerm Term a
r =
  PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
(PEvalFractionalTerm a, Eq a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultFdivTerm TotalRuleBinary a a a
forall a. PEvalFractionalTerm a => Term a -> Term a -> Term a
fdivTerm Term a
l Term a
r

doPevalDefaultFdivTerm ::
  (PEvalFractionalTerm a, Eq a) => Term a -> Term a -> Maybe (Term a)
doPevalDefaultFdivTerm :: forall a.
(PEvalFractionalTerm a, Eq a) =>
Term a -> Term a -> Maybe (Term a)
doPevalDefaultFdivTerm (ConTerm a
a) (ConTerm 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 => 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 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, Eq a) => Term a -> Term a
pevalDefaultRecipTerm :: forall a. (PEvalFractionalTerm a, Eq a) => Term a -> Term a
pevalDefaultRecipTerm l :: Term a
l@Term a
SupportedTerm =
  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, Eq a) => Term a -> Maybe (Term a)
doPevalDefaultRecipTerm TotalRuleUnary a a
forall a. PEvalFractionalTerm a => Term a -> Term a
recipTerm Term a
l

doPevalDefaultRecipTerm ::
  (PEvalFractionalTerm a, Eq a) => Term a -> Maybe (Term a)
doPevalDefaultRecipTerm :: forall a. (PEvalFractionalTerm a, Eq a) => Term a -> Maybe (Term a)
doPevalDefaultRecipTerm (ConTerm 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 => 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, Eq a) =>
Term a -> Term a -> Term a
pevalDefaultFdivTerm
  pevalRecipTerm :: Term AlgReal -> Term AlgReal
pevalRecipTerm = Term AlgReal -> Term AlgReal
forall a. (PEvalFractionalTerm a, Eq 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