{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Eta reduce" #-}
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